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/miplib/normalized-mps-v2-20-10-air04.opb
MD5SUM	eb0734273e24196dd14c6f237b52fa81
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.12098
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 17156

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        739616 kB
Buffers:         30796 kB
Cached:         242972 kB
SwapCached:          0 kB
Active:         102884 kB
Inactive:       173664 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        739364 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12760 kB
Committed_AS:    63452 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 10:05:24 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 11658 7 1200.18 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: 62   maxlim: 32   bits: 6/6
c ---[1640]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[1638]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[1636]---> Adder-cost: 10   maxlim: 11   bits: 4/4
c ---[1634]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1632]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1628]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1626]---> Adder-cost: 56   maxlim: 34   bits: 6/6
c ---[1624]---> Adder-cost: 208   maxlim: 107   bits: 7/7
c ---[1622]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1620]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[1618]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1616]---> Adder-cost: 42   maxlim: 32   bits: 6/6
c ---[1614]---> Adder-cost: 144   maxlim: 120   bits: 7/7
c ---[1612]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1610]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1606]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1604]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[1602]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[1600]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1598]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[1596]---> Adder-cost: 256   maxlim: 130   bits: 8/8
c ---[1594]---> Adder-cost: 188   maxlim: 97   bits: 7/7
c ---[1592]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1588]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1586]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1582]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[1580]---> Adder-cost: 138   maxlim: 118   bits: 7/7
c ---[1578]---> Adder-cost: 276   maxlim: 142   bits: 8/8
c ---[1576]---> Adder-cost: 92   maxlim: 50   bits: 6/6
c ---[1574]---> Adder-cost: 48   maxlim: 48   bits: 6/6
c ---[1572]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1570]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[1568]---> Adder-cost: 226   maxlim: 119   bits: 7/7
c ---[1566]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[1564]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1562]---> Adder-cost: 114   maxlim: 77   bits: 7/7
c ---[1560]---> Adder-cost: 50   maxlim: 77   bits: 7/7
c ---[1558]---> Adder-cost: 156   maxlim: 79   bits: 7/7
c ---[1556]---> Adder-cost: 110   maxlim: 89   bits: 7/7
c ---[1554]---> Adder-cost: 100   maxlim: 72   bits: 7/7
c ---[1550]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[1548]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[1546]---> Adder-cost: 96   maxlim: 52   bits: 6/6
c ---[1544]---> Adder-cost: 106   maxlim: 59   bits: 6/6
c ---[1542]---> Adder-cost: 178   maxlim: 94   bits: 7/7
c ---[1540]---> Adder-cost: 172   maxlim: 104   bits: 7/7
c ---[1538]---> Adder-cost: 166   maxlim: 87   bits: 7/7
c ---[1536]---> Adder-cost: 126   maxlim: 68   bits: 7/7
c ---[1534]---> Adder-cost: 72   maxlim: 63   bits: 7/6
c ---[1532]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[1530]---> Adder-cost: 140   maxlim: 72   bits: 7/7
c ---[1528]---> Adder-cost: 110   maxlim: 68   bits: 7/7
c ---[1526]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[1524]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[1522]---> Adder-cost: 148   maxlim: 80   bits: 7/7
c ---[1520]---> Adder-cost: 142   maxlim: 78   bits: 7/7
c ---[1518]---> Adder-cost: 178   maxlim: 108   bits: 7/7
c ---[1516]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[1514]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1512]---> Adder-cost: 78   maxlim: 44   bits: 6/6
c ---[1510]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[1508]---> Adder-cost: 106   maxlim: 57   bits: 6/6
c ---[1506]---> Adder-cost: 122   maxlim: 64   bits: 7/7
c ---[1504]---> Adder-cost: 240   maxlim: 125   bits: 7/7
c ---[1502]---> Adder-cost: 186   maxlim: 129   bits: 8/8
c ---[1500]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[1498]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[1496]---> Adder-cost: 68   maxlim: 41   bits: 6/6
c ---[1494]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[1492]---> Adder-cost: 86   maxlim: 49   bits: 6/6
c ---[1490]---> Adder-cost: 136   maxlim: 73   bits: 7/7
c ---[1488]---> Adder-cost: 94   maxlim: 67   bits: 7/7
c ---[1486]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1484]---> Adder-cost: 164   maxlim: 85   bits: 7/7
c ---[1482]---> Adder-cost: 142   maxlim: 96   bits: 7/7
c ---[1480]---> Adder-cost: 148   maxlim: 77   bits: 7/7
c ---[1478]---> Adder-cost: 92   maxlim: 67   bits: 7/7
c ---[1476]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1474]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[1472]---> Adder-cost: 44   maxlim: 25   bits: 5/5
c ---[1470]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1468]---> Adder-cost: 98   maxlim: 55   bits: 6/6
c ---[1464]---> Adder-cost: 48   maxlim: 30   bits: 5/5
c ---[1460]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1458]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[1456]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[1452]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1450]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[1448]---> Adder-cost: 268   maxlim: 143   bits: 8/8
c ---[1446]---> Adder-cost: 246   maxlim: 152   bits: 8/8
c ---[1444]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[1442]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[1440]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[1438]---> Adder-cost: 232   maxlim: 120   bits: 7/7
c ---[1436]---> Adder-cost: 168   maxlim: 113   bits: 7/7
c ---[1434]---> Adder-cost: 46   maxlim: 30   bits: 5/5
c ---[1432]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1430]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1428]---> Adder-cost: 62   maxlim: 41   bits: 6/6
c ---[1426]---> Adder-cost: 66   maxlim: 37   bits: 6/6
c ---[1424]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1422]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[1420]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1416]---> Adder-cost: 174   maxlim: 94   bits: 7/7
c ---[1414]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[1412]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1410]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[1408]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1406]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1404]---> Adder-cost: 142   maxlim: 75   bits: 7/7
c ---[1402]---> Adder-cost: 98   maxlim: 69   bits: 7/7
c ---[1400]---> Adder-cost: 190   maxlim: 98   bits: 7/7
c ---[1398]---> Adder-cost: 108   maxlim: 83   bits: 7/7
c ---[1396]---> Adder-cost: 152   maxlim: 79   bits: 7/7
c ---[1394]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[1392]---> Adder-cost: 200   maxlim: 120   bits: 7/7
c ---[1390]---> Adder-cost: 208   maxlim: 113   bits: 7/7
c ---[1388]---> Adder-cost: 232   maxlim: 124   bits: 7/7
c ---[1386]---> Adder-cost: 156   maxlim: 93   bits: 7/7
c ---[1384]---> Adder-cost: 220   maxlim: 113   bits: 7/7
c ---[1382]---> Adder-cost: 228   maxlim: 123   bits: 7/7
c ---[1380]---> Adder-cost: 162   maxlim: 114   bits: 7/7
c ---[1378]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[1376]---> Adder-cost: 50   maxlim: 34   bits: 6/6
c ---[1374]---> Adder-cost: 84   maxlim: 50   bits: 6/6
c ---[1372]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1370]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1368]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1366]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[1364]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[1362]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[1360]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[1358]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1356]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1354]---> Adder-cost: 62   maxlim: 34   bits: 6/6
c ---[1352]---> Adder-cost: 74   maxlim: 47   bits: 6/6
c ---[1350]---> Adder-cost: 108   maxlim: 63   bits: 7/6
c ---[1346]---> Adder-cost: 202   maxlim: 106   bits: 7/7
c ---[1342]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1340]---> Adder-cost: 108   maxlim: 59   bits: 6/6
c ---[1338]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1336]---> Adder-cost: 62   maxlim: 35   bits: 6/6
c ---[1334]---> Adder-cost: 50   maxlim: 38   bits: 6/6
c ---[1332]---> Adder-cost: 430   maxlim: 220   bits: 8/8
c ---[1330]---> Adder-cost: 422   maxlim: 215   bits: 8/8
c ---[1328]---> Adder-cost: 284   maxlim: 145   bits: 8/8
c ---[1326]---> Adder-cost: 218   maxlim: 129   bits: 8/8
c ---[1324]---> Adder-cost: 188   maxlim: 98   bits: 7/7
c ---[1322]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1320]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[1318]---> Adder-cost: 350   maxlim: 180   bits: 8/8
c ---[1316]---> Adder-cost: 322   maxlim: 195   bits: 8/8
c ---[1312]---> Adder-cost: 152   maxlim: 85   bits: 7/7
c ---[1310]---> Adder-cost: 146   maxlim: 86   bits: 7/7
c ---[1308]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[1306]---> Adder-cost: 218   maxlim: 113   bits: 7/7
c ---[1304]---> Adder-cost: 156   maxlim: 114   bits: 7/7
c ---[1302]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[1300]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[1298]---> Adder-cost: 114   maxlim: 68   bits: 7/7
c ---[1296]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[1294]---> Adder-cost: 58   maxlim: 46   bits: 6/6
c ---[1292]---> Adder-cost: 54   maxlim: 47   bits: 6/6
c ---[1288]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1286]---> Adder-cost: 70   maxlim: 44   bits: 6/6
c ---[1284]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1282]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1280]---> Adder-cost: 38   maxlim: 35   bits: 6/6
c ---[1278]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1276]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[1274]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1272]---> Adder-cost: 104   maxlim: 71   bits: 7/7
c ---[1270]---> Adder-cost: 146   maxlim: 84   bits: 7/7
c ---[1268]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[1266]---> Adder-cost: 56   maxlim: 61   bits: 6/6
c ---[1264]---> Adder-cost: 78   maxlim: 44   bits: 6/6
c ---[1262]---> Adder-cost: 144   maxlim: 78   bits: 7/7
c ---[1260]---> Adder-cost: 158   maxlim: 86   bits: 7/7
c ---[1258]---> Adder-cost: 192   maxlim: 106   bits: 7/7
c ---[1256]---> Adder-cost: 222   maxlim: 117   bits: 7/7
c ---[1254]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[1252]---> Adder-cost: 128   maxlim: 70   bits: 7/7
c ---[1250]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[1248]---> Adder-cost: 50   maxlim: 31   bits: 6/5
c ---[1246]---> Adder-cost: 88   maxlim: 50   bits: 6/6
c ---[1244]---> Adder-cost: 316   maxlim: 163   bits: 8/8
c ---[1242]---> Adder-cost: 324   maxlim: 168   bits: 8/8
c ---[1240]---> Adder-cost: 204   maxlim: 156   bits: 8/8
c ---[1238]---> Adder-cost: 260   maxlim: 136   bits: 8/8
c ---[1236]---> Adder-cost: 142   maxlim: 135   bits: 8/8
c ---[1234]---> Adder-cost: 404   maxlim: 207   bits: 8/8
c ---[1232]---> Adder-cost: 342   maxlim: 202   bits: 8/8
c ---[1230]---> Adder-cost: 120   maxlim: 65   bits: 7/7
c ---[1228]---> Adder-cost: 98   maxlim: 61   bits: 6/6
c ---[1226]---> Adder-cost: 220   maxlim: 127   bits: 8/7
c ---[1224]---> Adder-cost: 48   maxlim: 29   bits: 5/5
c ---[1222]---> Adder-cost: 212   maxlim: 119   bits: 7/7
c ---[1220]---> Adder-cost: 158   maxlim: 98   bits: 7/7
c ---[1218]---> Adder-cost: 104   maxlim: 61   bits: 6/6
c ---[1216]---> Adder-cost: 70   maxlim: 73   bits: 7/7
c ---[1214]---> Adder-cost: 136   maxlim: 72   bits: 7/7
c ---[1212]---> Adder-cost: 98   maxlim: 68   bits: 7/7
c ---[1210]---> Adder-cost: 108   maxlim: 62   bits: 6/6
c ---[1208]---> Adder-cost: 82   maxlim: 57   bits: 6/6
c ---[1206]---> Adder-cost: 96   maxlim: 53   bits: 6/6
c ---[1204]---> Adder-cost: 76   maxlim: 53   bits: 6/6
c ---[1202]---> Adder-cost: 62   maxlim: 41   bits: 6/6
c ---[1200]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1198]---> Adder-cost: 130   maxlim: 69   bits: 7/7
c ---[1196]---> Adder-cost: 168   maxlim: 106   bits: 7/7
c ---[1194]---> Adder-cost: 254   maxlim: 134   bits: 8/8
c ---[1192]---> Adder-cost: 210   maxlim: 115   bits: 7/7
c ---[1190]---> Adder-cost: 216   maxlim: 116   bits: 7/7
c ---[1188]---> Adder-cost: 216   maxlim: 129   bits: 8/8
c ---[1186]---> Adder-cost: 224   maxlim: 121   bits: 7/7
c ---[1184]---> Adder-cost: 202   maxlim: 115   bits: 7/7
c ---[1182]---> Adder-cost: 46   maxlim: 35   bits: 6/6
c ---[1180]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[1178]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[1176]---> Adder-cost: 178   maxlim: 120   bits: 7/7
c ---[1174]---> Adder-cost: 260   maxlim: 144   bits: 8/8
c ---[1172]---> Adder-cost: 134   maxlim: 97   bits: 7/7
c ---[1170]---> Adder-cost: 204   maxlim: 108   bits: 7/7
c ---[1168]---> Adder-cost: 138   maxlim: 104   bits: 7/7
c ---[1166]---> Adder-cost: 234   maxlim: 123   bits: 7/7
c ---[1164]---> Adder-cost: 192   maxlim: 130   bits: 8/8
c ---[1162]---> Adder-cost: 258   maxlim: 145   bits: 8/8
c ---[1160]---> Adder-cost: 210   maxlim: 120   bits: 7/7
c ---[1158]---> Adder-cost: 186   maxlim: 102   bits: 7/7
c ---[1156]---> Adder-cost: 138   maxlim: 72   bits: 7/7
c ---[1154]---> Adder-cost: 194   maxlim: 110   bits: 7/7
c ---[1152]---> Adder-cost: 126   maxlim: 66   bits: 7/7
c ---[1150]---> Adder-cost: 230   maxlim: 124   bits: 7/7
c ---[1148]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[1146]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[1144]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[1142]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[1140]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1138]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[1136]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1134]---> Adder-cost: 40   maxlim: 29   bits: 5/5
c ---[1132]---> Adder-cost: 174   maxlim: 95   bits: 7/7
c ---[1130]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1128]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[1126]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[1124]---> Adder-cost: 102   maxlim: 57   bits: 6/6
c ---[1122]---> Adder-cost: 98   maxlim: 58   bits: 6/6
c ---[1120]---> Adder-cost: 48   maxlim: 42   bits: 6/6
c ---[1118]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1116]---> Adder-cost: 90   maxlim: 53   bits: 6/6
c ---[1114]---> Adder-cost: 96   maxlim: 51   bits: 6/6
c ---[1112]---> Adder-cost: 90   maxlim: 52   bits: 6/6
c ---[1110]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[1108]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1106]---> Adder-cost: 88   maxlim: 47   bits: 6/6
c ---[1104]---> Adder-cost: 74   maxlim: 46   bits: 6/6
c ---[1102]---> Adder-cost: 42   maxlim: 45   bits: 6/6
c ---[1100]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1098]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1096]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[1094]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[1092]---> Adder-cost: 178   maxlim: 93   bits: 7/7
c ---[1090]---> Adder-cost: 234   maxlim: 127   bits: 8/7
c ---[1088]---> Adder-cost: 300   maxlim: 158   bits: 8/8
c ---[1086]---> Adder-cost: 236   maxlim: 130   bits: 8/8
c ---[1084]---> Adder-cost: 140   maxlim: 89   bits: 7/7
c ---[1082]---> Adder-cost: 256   maxlim: 132   bits: 8/8
c ---[1080]---> Adder-cost: 162   maxlim: 84   bits: 7/7
c ---[1078]---> Adder-cost: 148   maxlim: 84   bits: 7/7
c ---[1076]---> Adder-cost: 142   maxlim: 77   bits: 7/7
c ---[1074]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1072]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[1070]---> Adder-cost: 90   maxlim: 49   bits: 6/6
c ---[1068]---> Adder-cost: 140   maxlim: 71   bits: 7/7
c ---[1066]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[1064]---> Adder-cost: 118   maxlim: 84   bits: 7/7
c ---[1062]---> Adder-cost: 108   maxlim: 92   bits: 7/7
c ---[1060]---> Adder-cost: 166   maxlim: 93   bits: 7/7
c ---[1058]---> Adder-cost: 246   maxlim: 137   bits: 8/8
c ---[1056]---> Adder-cost: 60   maxlim: 33   bits: 6/6
c ---[1054]---> Adder-cost: 42   maxlim: 25   bits: 5/5
c ---[1052]---> Adder-cost: 30   maxlim: 24   bits: 5/5
c ---[1050]---> Adder-cost: 94   maxlim: 51   bits: 6/6
c ---[1048]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1046]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1044]---> Adder-cost: 28   maxlim: 24   bits: 5/5
c ---[1042]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[1040]---> Adder-cost: 46   maxlim: 38   bits: 6/6
c ---[1038]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1036]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[1034]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[1032]---> Adder-cost: 92   maxlim: 50   bits: 6/6
c ---[1030]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1028]---> Adder-cost: 76   maxlim: 55   bits: 6/6
c ---[1026]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[1024]---> Adder-cost: 138   maxlim: 87   bits: 7/7
c ---[1022]---> Adder-cost: 368   maxlim: 206   bits: 8/8
c ---[1020]---> Adder-cost: 292   maxlim: 186   bits: 8/8
c ---[1018]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[1016]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1014]---> Adder-cost: 68   maxlim: 45   bits: 6/6
c ---[1012]---> Adder-cost: 68   maxlim: 40   bits: 6/6
c ---[1010]---> Adder-cost: 74   maxlim: 42   bits: 6/6
c ---[1008]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[1006]---> Adder-cost: 118   maxlim: 85   bits: 7/7
c ---[1004]---> Adder-cost: 196   maxlim: 105   bits: 7/7
c ---[1002]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1000]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 998]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[ 994]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[ 992]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 990]---> Adder-cost: 68   maxlim: 49   bits: 6/6
c ---[ 988]---> Adder-cost: 84   maxlim: 50   bits: 6/6
c ---[ 986]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 984]---> Adder-cost: 112   maxlim: 69   bits: 7/7
c ---[ 982]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[ 980]---> Adder-cost: 106   maxlim: 60   bits: 6/6
c ---[ 978]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 976]---> Adder-cost: 76   maxlim: 47   bits: 6/6
c ---[ 974]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 972]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 970]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 968]---> Adder-cost: 50   maxlim: 38   bits: 6/6
c ---[ 964]---> Adder-cost: 174   maxlim: 92   bits: 7/7
c ---[ 962]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 960]---> Adder-cost: 90   maxlim: 49   bits: 6/6
c ---[ 958]---> Adder-cost: 214   maxlim: 113   bits: 7/7
c ---[ 956]---> Adder-cost: 254   maxlim: 141   bits: 8/8
c ---[ 952]---> Adder-cost: 150   maxlim: 80   bits: 7/7
c ---[ 950]---> Adder-cost: 200   maxlim: 105   bits: 7/7
c ---[ 948]---> Adder-cost: 140   maxlim: 109   bits: 7/7
c ---[ 946]---> Adder-cost: 222   maxlim: 119   bits: 7/7
c ---[ 944]---> Adder-cost: 114   maxlim: 96   bits: 7/7
c ---[ 942]---> Adder-cost: 358   maxlim: 185   bits: 8/8
c ---[ 940]---> Adder-cost: 318   maxlim: 185   bits: 8/8
c ---[ 938]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[ 936]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[ 934]---> Adder-cost: 276   maxlim: 145   bits: 8/8
c ---[ 932]---> Adder-cost: 244   maxlim: 140   bits: 8/8
c ---[ 930]---> Adder-cost: 328   maxlim: 174   bits: 8/8
c ---[ 928]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 926]---> Adder-cost: 78   maxlim: 49   bits: 6/6
c ---[ 924]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 922]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[ 920]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 918]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[ 916]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[ 914]---> Adder-cost: 142   maxlim: 75   bits: 7/7
c ---[ 912]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[ 910]---> Adder-cost: 56   maxlim: 54   bits: 6/6
c ---[ 908]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[ 906]---> Adder-cost: 98   maxlim: 57   bits: 6/6
c ---[ 904]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 902]---> Adder-cost: 224   maxlim: 117   bits: 7/7
c ---[ 900]---> Adder-cost: 184   maxlim: 98   bits: 7/7
c ---[ 898]---> Adder-cost: 150   maxlim: 88   bits: 7/7
c ---[ 896]---> Adder-cost: 214   maxlim: 125   bits: 7/7
c ---[ 894]---> Adder-cost: 380   maxlim: 194   bits: 8/8
c ---[ 892]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 890]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 888]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 886]---> Adder-cost: 132   maxlim: 74   bits: 7/7
c ---[ 884]---> Adder-cost: 132   maxlim: 75   bits: 7/7
c ---[ 882]---> Adder-cost: 258   maxlim: 138   bits: 8/8
c ---[ 880]---> Adder-cost: 198   maxlim: 109   bits: 7/7
c ---[ 878]---> Adder-cost: 156   maxlim: 90   bits: 7/7
c ---[ 876]---> Adder-cost: 214   maxlim: 120   bits: 7/7
c ---[ 874]---> Adder-cost: 282   maxlim: 154   bits: 8/8
c ---[ 872]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 870]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 868]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[ 866]---> Adder-cost: 100   maxlim: 58   bits: 6/6
c ---[ 864]---> Adder-cost: 92   maxlim: 58   bits: 6/6
c ---[ 862]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[ 860]---> Adder-cost: 322   maxlim: 165   bits: 8/8
c ---[ 858]---> Adder-cost: 282   maxlim: 155   bits: 8/8
c ---[ 856]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 854]---> Adder-cost: 76   maxlim: 47   bits: 6/6
c ---[ 852]---> Adder-cost: 272   maxlim: 159   bits: 8/8
c ---[ 850]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[ 848]---> Adder-cost: 68   maxlim: 41   bits: 6/6
c ---[ 846]---> Adder-cost: 64   maxlim: 43   bits: 6/6
c ---[ 844]---> Adder-cost: 80   maxlim: 44   bits: 6/6
c ---[ 842]---> Adder-cost: 58   maxlim: 45   bits: 6/6
c ---[ 840]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 836]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 834]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[ 832]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[ 828]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 826]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[ 824]---> Adder-cost: 236   maxlim: 123   bits: 7/7
c ---[ 822]---> Adder-cost: 196   maxlim: 113   bits: 7/7
c ---[ 820]---> Adder-cost: 104   maxlim: 56   bits: 6/6
c ---[ 818]---> Adder-cost: 108   maxlim: 64   bits: 7/7
c ---[ 816]---> Adder-cost: 122   maxlim: 69   bits: 7/7
c ---[ 814]---> Adder-cost: 124   maxlim: 70   bits: 7/7
c ---[ 812]---> Adder-cost: 240   maxlim: 130   bits: 8/8
c ---[ 810]---> Adder-cost: 238   maxlim: 131   bits: 8/8
c ---[ 808]---> Adder-cost: 254   maxlim: 138   bits: 8/8
c ---[ 806]---> Adder-cost: 170   maxlim: 141   bits: 8/8
c ---[ 804]---> Adder-cost: 254   maxlim: 134   bits: 8/8
c ---[ 802]---> Adder-cost: 158   maxlim: 86   bits: 7/7
c ---[ 800]---> Adder-cost: 80   maxlim: 55   bits: 6/6
c ---[ 796]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 794]---> Adder-cost: 160   maxlim: 93   bits: 7/7
c ---[ 792]---> Adder-cost: 104   maxlim: 93   bits: 7/7
c ---[ 790]---> Adder-cost: 272   maxlim: 146   bits: 8/8
c ---[ 788]---> Adder-cost: 182   maxlim: 151   bits: 8/8
c ---[ 786]---> Adder-cost: 316   maxlim: 168   bits: 8/8
c ---[ 784]---> Adder-cost: 350   maxlim: 197   bits: 8/8
c ---[ 782]---> Adder-cost: 232   maxlim: 128   bits: 8/8
c ---[ 780]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[ 778]---> Adder-cost: 64   maxlim: 45   bits: 6/6
c ---[ 776]---> Adder-cost: 86   maxlim: 52   bits: 6/6
c ---[ 774]---> Adder-cost: 172   maxlim: 101   bits: 7/7
c ---[ 772]---> Adder-cost: 354   maxlim: 194   bits: 8/8
c ---[ 770]---> Adder-cost: 316   maxlim: 165   bits: 8/8
c ---[ 768]---> Adder-cost: 224   maxlim: 161   bits: 8/8
c ---[ 766]---> Adder-cost: 126   maxlim: 65   bits: 7/7
c ---[ 764]---> Adder-cost: 86   maxlim: 50   bits: 6/6
c ---[ 762]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 760]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[ 758]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[ 756]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 754]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 752]---> Adder-cost: 126   maxlim: 72   bits: 7/7
c ---[ 750]---> Adder-cost: 356   maxlim: 189   bits: 8/8
c ---[ 748]---> Adder-cost: 168   maxlim: 177   bits: 8/8
c ---[ 744]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 742]---> Adder-cost: 98   maxlim: 61   bits: 6/6
c ---[ 740]---> Adder-cost: 132   maxlim: 76   bits: 7/7
c ---[ 738]---> Adder-cost: 208   maxlim: 111   bits: 7/7
c ---[ 736]---> Adder-cost: 156   maxlim: 91   bits: 7/7
c ---[ 732]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 730]---> Adder-cost: 128   maxlim: 74   bits: 7/7
c ---[ 728]---> Adder-cost: 272   maxlim: 150   bits: 8/8
c ---[ 726]---> Adder-cost: 304   maxlim: 166   bits: 8/8
c ---[ 722]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 720]---> Adder-cost: 200   maxlim: 103   bits: 7/7
c ---[ 718]---> Adder-cost: 236   maxlim: 131   bits: 8/8
c ---[ 716]---> Adder-cost: 340   maxlim: 175   bits: 8/8
c ---[ 714]---> Adder-cost: 272   maxlim: 177   bits: 8/8
c ---[ 712]---> Adder-cost: 156   maxlim: 83   bits: 7/7
c ---[ 710]---> Adder-cost: 138   maxlim: 86   bits: 7/7
c ---[ 708]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[ 706]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[ 704]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[ 702]---> Adder-cost: 58   maxlim: 54   bits: 6/6
c ---[ 700]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[ 698]---> Adder-cost: 150   maxlim: 80   bits: 7/7
c ---[ 696]---> Adder-cost: 136   maxlim: 75   bits: 7/7
c ---[ 694]---> Adder-cost: 136   maxlim: 76   bits: 7/7
c ---[ 692]---> Adder-cost: 152   maxlim: 83   bits: 7/7
c ---[ 690]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 688]---> Adder-cost: 242   maxlim: 127   bits: 8/7
c ---[ 686]---> Adder-cost: 142   maxlim: 129   bits: 8/8
c ---[ 684]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 682]---> Adder-cost: 138   maxlim: 71   bits: 7/7
c ---[ 680]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[ 678]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 676]---> Adder-cost: 68   maxlim: 38   bits: 6/6
c ---[ 674]---> Adder-cost: 90   maxlim: 56   bits: 6/6
c ---[ 672]---> Adder-cost: 144   maxlim: 76   bits: 7/7
c ---[ 670]---> Adder-cost: 128   maxlim: 69   bits: 7/7
c ---[ 668]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[ 666]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 664]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 662]---> Adder-cost: 18   maxlim: 18   bits: 5/5
c ---[ 660]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 658]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 654]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[ 652]---> Adder-cost: 186   maxlim: 99   bits: 7/7
c ---[ 650]---> Adder-cost: 78   maxlim: 99   bits: 7/7
c ---[ 648]---> Adder-cost: 120   maxlim: 63   bits: 7/6
c ---[ 646]---> Adder-cost: 156   maxlim: 89   bits: 7/7
c ---[ 642]---> Adder-cost: 90   maxlim: 48   bits: 6/6
c ---[ 640]---> Adder-cost: 60   maxlim: 47   bits: 6/6
c ---[ 638]---> Adder-cost: 292   maxlim: 161   bits: 8/8
c ---[ 636]---> Adder-cost: 196   maxlim: 158   bits: 8/8
c ---[ 634]---> Adder-cost: 144   maxlim: 84   bits: 7/7
c ---[ 628]---> Adder-cost: 116   maxlim: 78   bits: 7/7
c ---[ 626]---> Adder-cost: 234   maxlim: 127   bits: 8/7
c ---[ 624]---> Adder-cost: 332   maxlim: 196   bits: 8/8
c ---[ 622]---> Adder-cost: 324   maxlim: 174   bits: 8/8
c ---[ 620]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 616]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 614]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[ 612]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 610]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 608]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[ 606]---> Adder-cost: 76   maxlim: 43   bits: 6/6
c ---[ 604]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 602]---> Adder-cost: 318   maxlim: 182   bits: 8/8
c ---[ 600]---> Adder-cost: 216   maxlim: 187   bits: 8/8
c ---[ 598]---> Adder-cost: 280   maxlim: 177   bits: 8/8
c ---[ 596]---> Adder-cost: 338   maxlim: 175   bits: 8/8
c ---[ 594]---> Adder-cost: 232   maxlim: 160   bits: 8/8
c ---[ 592]---> Adder-cost: 282   maxlim: 160   bits: 8/8
c ---[ 590]---> Adder-cost: 230   maxlim: 175   bits: 8/8
c ---[ 588]---> Adder-cost: 134   maxlim: 77   bits: 7/7
c ---[ 586]---> Adder-cost: 94   maxlim: 57   bits: 6/6
c ---[ 584]---> Adder-cost: 88   maxlim: 56   bits: 6/6
c ---[ 582]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[ 580]---> Adder-cost: 34   maxlim: 25   bits: 5/5
c ---[ 578]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 576]---> Adder-cost: 12   maxlim: 14   bits: 4/4
c ---[ 574]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 570]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 566]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 564]---> Adder-cost: 122   maxlim: 74   bits: 7/7
c ---[ 562]---> Adder-cost: 144   maxlim: 81   bits: 7/7
c ---[ 560]---> Adder-cost: 374   maxlim: 198   bits: 8/8
c ---[ 558]---> Adder-cost: 214   maxlim: 199   bits: 8/8
c ---[ 556]---> Adder-cost: 376   maxlim: 197   bits: 8/8
c ---[ 554]---> Adder-cost: 286   maxlim: 177   bits: 8/8
c ---[ 552]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 550]---> Adder-cost: 322   maxlim: 197   bits: 8/8
c ---[ 548]---> Adder-cost: 256   maxlim: 134   bits: 8/8
c ---[ 546]---> Adder-cost: 190   maxlim: 130   bits: 8/8
c ---[ 544]---> Adder-cost: 226   maxlim: 133   bits: 8/8
c ---[ 542]---> Adder-cost: 252   maxlim: 132   bits: 8/8
c ---[ 540]---> Adder-cost: 210   maxlim: 136   bits: 8/8
c ---[ 538]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 536]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 534]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 532]---> Adder-cost: 104   maxlim: 59   bits: 6/6
c ---[ 530]---> Adder-cost: 56   maxlim: 36   bits: 6/6
c ---[ 528]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[ 526]---> Adder-cost: 106   maxlim: 91   bits: 7/7
c ---[ 524]---> Adder-cost: 196   maxlim: 108   bits: 7/7
c ---[ 522]---> Adder-cost: 138   maxlim: 110   bits: 7/7
c ---[ 520]---> Adder-cost: 178   maxlim: 103   bits: 7/7
c ---[ 518]---> Adder-cost: 316   maxlim: 173   bits: 8/8
c ---[ 516]---> Adder-cost: 242   maxlim: 138   bits: 8/8
c ---[ 514]---> Adder-cost: 162   maxlim: 89   bits: 7/7
c ---[ 512]---> Adder-cost: 116   maxlim: 76   bits: 7/7
c ---[ 510]---> Adder-cost: 248   maxlim: 134   bits: 8/8
c ---[ 508]---> Adder-cost: 224   maxlim: 144   bits: 8/8
c ---[ 506]---> Adder-cost: 104   maxlim: 55   bits: 6/6
c ---[ 504]---> Adder-cost: 112   maxlim: 64   bits: 7/7
c ---[ 502]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 500]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[ 498]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 496]---> Adder-cost: 94   maxlim: 60   bits: 6/6
c ---[ 494]---> Adder-cost: 64   maxlim: 50   bits: 6/6
c ---[ 492]---> Adder-cost: 74   maxlim: 54   bits: 6/6
c ---[ 490]---> Adder-cost: 248   maxlim: 132   bits: 8/8
c ---[ 488]---> Adder-cost: 148   maxlim: 126   bits: 7/7
c ---[ 486]---> Adder-cost: 250   maxlim: 143   bits: 8/8
c ---[ 484]---> Adder-cost: 352   maxlim: 195   bits: 8/8
c ---[ 482]---> Adder-cost: 274   maxlim: 170   bits: 8/8
c ---[ 480]---> Adder-cost: 296   maxlim: 179   bits: 8/8
c ---[ 478]---> Adder-cost: 290   maxlim: 178   bits: 8/8
c ---[ 476]---> Adder-cost: 238   maxlim: 133   bits: 8/8
c ---[ 474]---> Adder-cost: 166   maxlim: 128   bits: 8/8
c ---[ 472]---> Adder-cost: 264   maxlim: 148   bits: 8/8
c ---[ 468]---> Adder-cost: 398   maxlim: 210   bits: 8/8
c ---[ 466]---> Adder-cost: 366   maxlim: 221   bits: 8/8
c ---[ 464]---> Adder-cost: 400   maxlim: 237   bits: 8/8
c ---[ 462]---> Adder-cost: 416   maxlim: 239   bits: 8/8
c ---[ 460]---> Adder-cost: 338   maxlim: 204   bits: 8/8
c ---[ 458]---> Adder-cost: 214   maxlim: 121   bits: 7/7
c ---[ 456]---> Adder-cost: 190   maxlim: 108   bits: 7/7
c ---[ 454]---> Adder-cost: 276   maxlim: 157   bits: 8/8
c ---[ 452]---> Adder-cost: 330   maxlim: 187   bits: 8/8
c ---[ 450]---> Adder-cost: 362   maxlim: 196   bits: 8/8
c ---[ 448]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 446]---> Adder-cost: 184   maxlim: 121   bits: 7/7
c ---[ 444]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[ 442]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 440]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 438]---> Adder-cost: 112   maxlim: 76   bits: 7/7
c ---[ 436]---> Adder-cost: 250   maxlim: 130   bits: 8/8
c ---[ 434]---> Adder-cost: 262   maxlim: 137   bits: 8/8
c ---[ 432]---> Adder-cost: 304   maxlim: 156   bits: 8/8
c ---[ 430]---> Adder-cost: 284   maxlim: 173   bits: 8/8
c ---[ 428]---> Adder-cost: 368   maxlim: 194   bits: 8/8
c ---[ 426]---> Adder-cost: 284   maxlim: 194   bits: 8/8
c ---[ 424]---> Adder-cost: 278   maxlim: 148   bits: 8/8
c ---[ 422]---> Adder-cost: 116   maxlim: 139   bits: 8/8
c ---[ 420]---> Adder-cost: 342   maxlim: 178   bits: 8/8
c ---[ 418]---> Adder-cost: 208   maxlim: 184   bits: 8/8
c ---[ 416]---> Adder-cost: 420   maxlim: 222   bits: 8/8
c ---[ 414]---> Adder-cost: 586   maxlim: 327   bits: 9/9
c ---[ 412]---> Adder-cost: 658   maxlim: 353   bits: 9/9
c ---[ 410]---> Adder-cost: 462   maxlim: 346   bits: 9/9
c ---[ 408]---> Adder-cost: 394   maxlim: 221   bits: 8/8
c ---[ 406]---> Adder-cost: 364   maxlim: 224   bits: 8/8
c ---[ 404]---> Adder-cost: 260   maxlim: 145   bits: 8/8
c ---[ 402]---> Adder-cost: 256   maxlim: 140   bits: 8/8
c ---[ 400]---> Adder-cost: 222   maxlim: 121   bits: 7/7
c ---[ 398]---> Adder-cost: 118   maxlim: 130   bits: 8/8
c ---[ 396]---> Adder-cost: 296   maxlim: 155   bits: 8/8
c ---[ 394]---> Adder-cost: 280   maxlim: 144   bits: 8/8
c ---[ 392]---> Adder-cost: 156   maxlim: 89   bits: 7/7
c ---[ 390]---> Adder-cost: 138   maxlim: 78   bits: 7/7
c ---[ 388]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 386]---> Adder-cost: 70   maxlim: 62   bits: 6/6
c ---[ 384]---> Adder-cost: 180   maxlim: 95   bits: 7/7
c ---[ 382]---> Adder-cost: 204   maxlim: 112   bits: 7/7
c ---[ 378]---> Adder-cost: 254   maxlim: 134   bits: 8/8
c ---[ 376]---> Adder-cost: 124   maxlim: 68   bits: 7/7
c ---[ 374]---> Adder-cost: 80   maxlim: 54   bits: 6/6
c ---[ 372]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 370]---> Adder-cost: 52   maxlim: 38   bits: 6/6
c ---[ 368]---> Adder-cost: 112   maxlim: 61   bits: 6/6
c ---[ 366]---> Adder-cost: 80   maxlim: 61   bits: 6/6
c ---[ 360]---> Adder-cost: 184   maxlim: 95   bits: 7/7
c ---[ 358]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 356]---> Adder-cost: 64   maxlim: 41   bits: 6/6
c ---[ 354]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 352]---> Adder-cost: 86   maxlim: 50   bits: 6/6
c ---[ 350]---> Adder-cost: 306   maxlim: 164   bits: 8/8
c ---[ 348]---> Adder-cost: 210   maxlim: 147   bits: 8/8
c ---[ 346]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 344]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 342]---> Adder-cost: 252   maxlim: 128   bits: 8/8
c ---[ 340]---> Adder-cost: 260   maxlim: 143   bits: 8/8
c ---[ 338]---> Adder-cost: 176   maxlim: 96   bits: 7/7
c ---[ 336]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 334]---> Adder-cost: 76   maxlim: 46   bits: 6/6
c ---[ 332]---> Adder-cost: 186   maxlim: 106   bits: 7/7
c ---[ 330]---> Adder-cost: 140   maxlim: 80   bits: 7/7
c ---[ 328]---> Adder-cost: 102   maxlim: 69   bits: 7/7
c ---[ 326]---> Adder-cost: 50   maxlim: 45   bits: 6/6
c ---[ 324]---> Adder-cost: 98   maxlim: 58   bits: 6/6
c ---[ 322]---> Adder-cost: 128   maxlim: 74   bits: 7/7
c ---[ 318]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 316]---> Adder-cost: 312   maxlim: 161   bits: 8/8
c ---[ 314]---> Adder-cost: 228   maxlim: 172   bits: 8/8
c ---[ 312]---> Adder-cost: 584   maxlim: 302   bits: 9/9
c ---[ 310]---> Adder-cost: 434   maxlim: 302   bits: 9/9
c ---[ 308]---> Adder-cost: 348   maxlim: 196   bits: 8/8
c ---[ 306]---> Adder-cost: 312   maxlim: 200   bits: 8/8
c ---[ 304]---> Adder-cost: 278   maxlim: 145   bits: 8/8
c ---[ 302]---> Adder-cost: 230   maxlim: 139   bits: 8/8
c ---[ 300]---> Adder-cost: 284   maxlim: 155   bits: 8/8
c ---[ 298]---> Adder-cost: 208   maxlim: 122   bits: 7/7
c ---[ 296]---> Adder-cost: 198   maxlim: 124   bits: 7/7
c ---[ 294]---> Adder-cost: 234   maxlim: 143   bits: 8/8
c ---[ 292]---> Adder-cost: 148   maxlim: 84   bits: 7/7
c ---[ 290]---> Adder-cost: 120   maxlim: 96   bits: 7/7
c ---[ 288]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 286]---> Adder-cost: 40   maxlim: 23   bits: 5/5
c ---[ 284]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 282]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[ 278]---> Adder-cost: 170   maxlim: 89   bits: 7/7
c ---[ 276]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 274]---> Adder-cost: 146   maxlim: 109   bits: 7/7
c ---[ 272]---> Adder-cost: 118   maxlim: 69   bits: 7/7
c ---[ 270]---> Adder-cost: 88   maxlim: 56   bits: 6/6
c ---[ 268]---> Adder-cost: 172   maxlim: 92   bits: 7/7
c ---[ 266]---> Adder-cost: 188   maxlim: 103   bits: 7/7
c ---[ 264]---> Adder-cost: 260   maxlim: 143   bits: 8/8
c ---[ 262]---> Adder-cost: 190   maxlim: 131   bits: 8/8
c ---[ 260]---> Adder-cost: 162   maxlim: 89   bits: 7/7
c ---[ 258]---> Adder-cost: 168   maxlim: 106   bits: 7/7
c ---[ 254]---> Adder-cost: 144   maxlim: 79   bits: 7/7
c ---[ 252]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 250]---> Adder-cost: 90   maxlim: 54   bits: 6/6
c ---[ 246]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[ 244]---> Adder-cost: 266   maxlim: 141   bits: 8/8
c ---[ 242]---> Adder-cost: 246   maxlim: 134   bits: 8/8
c ---[ 240]---> Adder-cost: 152   maxlim: 86   bits: 7/7
c ---[ 238]---> Adder-cost: 154   maxlim: 88   bits: 7/7
c ---[ 236]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[ 234]---> Adder-cost: 146   maxlim: 84   bits: 7/7
c ---[ 230]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 228]---> Adder-cost: 262   maxlim: 144   bits: 8/8
c ---[ 226]---> Adder-cost: 238   maxlim: 139   bits: 8/8
c ---[ 224]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 222]---> Adder-cost: 180   maxlim: 98   bits: 7/7
c ---[ 220]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[ 218]---> Adder-cost: 114   maxlim: 65   bits: 7/7
c ---[ 216]---> Adder-cost: 310   maxlim: 159   bits: 8/8
c ---[ 214]---> Adder-cost: 342   maxlim: 207   bits: 8/8
c ---[ 212]---> Adder-cost: 222   maxlim: 118   bits: 7/7
c ---[ 210]---> Adder-cost: 220   maxlim: 136   bits: 8/8
c ---[ 208]---> Adder-cost: 256   maxlim: 142   bits: 8/8
c ---[ 206]---> Adder-cost: 236   maxlim: 137   bits: 8/8
c ---[ 204]---> Adder-cost: 260   maxlim: 150   bits: 8/8
c ---[ 202]---> Adder-cost: 268   maxlim: 144   bits: 8/8
c ---[ 200]---> Adder-cost: 178   maxlim: 101   bits: 7/7
c ---[ 198]---> Adder-cost: 218   maxlim: 117   bits: 7/7
c ---[ 196]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[ 194]---> Adder-cost: 138   maxlim: 81   bits: 7/7
c ---[ 192]---> Adder-cost: 92   maxlim: 74   bits: 7/7
c ---[ 188]---> Adder-cost: 132   maxlim: 68   bits: 7/7
c ---[ 186]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[ 184]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 182]---> Adder-cost: 170   maxlim: 109   bits: 7/7
c ---[ 180]---> Adder-cost: 266   maxlim: 138   bits: 8/8
c ---[ 178]---> Adder-cost: 214   maxlim: 134   bits: 8/8
c ---[ 176]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 174]---> Adder-cost: 14   maxlim: 14   bits: 4/4
c ---[ 172]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 170]---> Adder-cost: 26   maxlim: 20   bits: 5/5
c ---[ 168]---> Adder-cost: 212   maxlim: 114   bits: 7/7
c ---[ 166]---> Adder-cost: 142   maxlim: 122   bits: 7/7
c ---[ 164]---> Adder-cost: 352   maxlim: 193   bits: 8/8
c ---[ 162]---> Adder-cost: 276   maxlim: 193   bits: 8/8
c ---[ 160]---> Adder-cost: 66   maxlim: 37   bits: 6/6
c ---[ 158]---> Adder-cost: 78   maxlim: 46   bits: 6/6
c ---[ 154]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 152]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 150]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 148]---> Adder-cost: 104   maxlim: 59   bits: 6/6
c ---[ 146]---> Adder-cost: 94   maxlim: 56   bits: 6/6
c ---[ 144]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[ 142]---> Adder-cost: 112   maxlim: 68   bits: 7/7
c ---[ 140]---> Adder-cost: 224   maxlim: 122   bits: 7/7
c ---[ 138]---> Adder-cost: 182   maxlim: 121   bits: 7/7
c ---[ 136]---> Adder-cost: 138   maxlim: 75   bits: 7/7
c ---[ 134]---> Adder-cost: 100   maxlim: 58   bits: 6/6
c ---[ 132]---> Adder-cost: 132   maxlim: 87   bits: 7/7
c ---[ 130]---> Adder-cost: 224   maxlim: 126   bits: 7/7
c ---[ 128]---> Adder-cost: 120   maxlim: 105   bits: 7/7
c ---[ 126]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[ 124]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 122]---> Adder-cost: 72   maxlim: 50   bits: 6/6
c ---[ 120]---> Adder-cost: 112   maxlim: 63   bits: 7/6
c ---[ 118]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[ 116]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[ 114]---> Adder-cost: 124   maxlim: 64   bits: 7/7
c ---[ 112]---> Adder-cost: 104   maxlim: 68   bits: 7/7
c ---[ 110]---> Adder-cost: 146   maxlim: 81   bits: 7/7
c ---[ 108]---> Adder-cost: 138   maxlim: 82   bits: 7/7
c ---[ 106]---> Adder-cost: 386   maxlim: 219   bits: 8/8
c ---[ 104]---> Adder-cost: 302   maxlim: 171   bits: 8/8
c ---[ 102]---> Adder-cost: 212   maxlim: 172   bits: 8/8
c ---[ 100]---> Adder-cost: 378   maxlim: 247   bits: 8/8
c ---[  98]---> Adder-cost: 456   maxlim: 245   bits: 8/8
c ---[  96]---> Adder-cost: 376   maxlim: 247   bits: 8/8
c ---[  94]---> Adder-cost: 412   maxlim: 229   bits: 8/8
c ---[  92]---> Adder-cost: 366   maxlim: 234   bits: 8/8
c ---[  90]---> Adder-cost: 400   maxlim: 211   bits: 8/8
c ---[  88]---> Adder-cost: 324   maxlim: 210   bits: 8/8
c ---[  86]---> Adder-cost: 400   maxlim: 217   bits: 8/8
c ---[  84]---> Adder-cost: 338   maxlim: 204   bits: 8/8
c ---[  82]---> Adder-cost: 316   maxlim: 207   bits: 8/8
c ---[  80]---> Adder-cost: 632   maxlim: 337   bits: 9/9
c ---[  78]---> Adder-cost: 612   maxlim: 367   bits: 9/9
c ---[  76]---> Adder-cost: 364   maxlim: 194   bits: 8/8
c ---[  74]---> Adder-cost: 258   maxlim: 152   bits: 8/8
c ---[  72]---> Adder-cost: 308   maxlim: 174   bits: 8/8
c ---[  70]---> Adder-cost: 334   maxlim: 185   bits: 8/8
c ---[  68]---> Adder-cost: 290   maxlim: 203   bits: 8/8
c ---[  66]---> Adder-cost: 280   maxlim: 157   bits: 8/8
c ---[  64]---> Adder-cost: 242   maxlim: 151   bits: 8/8
c ---[  62]---> Adder-cost: 234   maxlim: 129   bits: 8/8
c ---[  60]---> Adder-cost: 222   maxlim: 127   bits: 8/7
c ---[  58]---> Adder-cost: 290   maxlim: 160   bits: 8/8
c ---[  56]---> Adder-cost: 192   maxlim: 169   bits: 8/8
c ---[  54]---> Adder-cost: 252   maxlim: 174   bits: 8/8
c ---[  52]---> Adder-cost: 216   maxlim: 122   bits: 7/7
c ---[  50]---> Adder-cost: 204   maxlim: 124   bits: 7/7
c ---[  46]---> Adder-cost: 228   maxlim: 120   bits: 7/7
c ---[  44]---> Adder-cost: 140   maxlim: 75   bits: 7/7
c ---[  40]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[  38]---> Adder-cost: 110   maxlim: 74   bits: 7/7
c ---[  36]---> Adder-cost: 94   maxlim: 55   bits: 6/6
c ---[  34]---> Adder-cost: 68   maxlim: 50   bits: 6/6
c ---[  32]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[  30]---> Adder-cost: 74   maxlim: 40   bits: 6/6
c ---[  28]---> Adder-cost: 68   maxlim: 43   bits: 6/6
c ---[  26]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[  24]---> Adder-cost: 134   maxlim: 76   bits: 7/7
c ---[  22]---> Adder-cost: 158   maxlim: 89   bits: 7/7
c ---[  20]---> Adder-cost: 140   maxlim: 88   bits: 7/7
c ---[  18]---> Adder-cost: 120   maxlim: 75   bits: 7/7
c ---[  16]---> Adder-cost: 140   maxlim: 79   bits: 7/7
c ---[  14]---> Adder-cost: 196   maxlim: 108   bits: 7/7
c ---[  12]---> Adder-cost: 162   maxlim: 108   bits: 7/7
c ---[  10]---> Adder-cost: 208   maxlim: 118   bits: 7/7
c ---[   8]---> Adder-cost: 146   maxlim: 83   bits: 7/7
c ---[   6]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   4]---> Adder-cost: 54   maxlim: 36   bits: 6/6
c ---[   2]---> Adder-cost: 134   maxlim: 71   bits: 7/7
c ---[   0]---> Adder-cost: 86   maxlim: 70   bits: 7/7
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 |       101 |  793926  2825448 |  291380      27       94     3.5 |  8.594 % |
c |       251 |  793081  2822517 |  320518      82      291     3.5 |  8.699 % |
c |       477 |  791736  2817804 |  352569     158      582     3.7 |  8.882 % |
c |       816 |  789367  2809549 |  387826     245      891     3.6 |  9.182 % |
c |      1324 |  786208  2798570 |  426609     419     1684     4.0 |  9.592 % |
c |      2083 |  781691  2782963 |  469270     702     2852     4.1 | 10.182 % |
c |      3222 |  777251  2767505 |  516197    1379     6473     4.7 | 10.756 % |
c |      4931 |  769972  2742122 |  567817    2281    10886     4.8 | 11.696 % |
c |      7494 |  762191  2714907 |  624599    3936    20767     5.3 | 12.687 % |
c |     11342 |  752725  2681775 |  687059    6675    36966     5.5 | 13.899 % |
c |     17108 |  737586  2628156 |  755764   10422    60973     5.9 | 15.796 % |
#### 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.84 0.94 0.90 2/54 32174
Raw data (stat): 32174 (runsolver) R 32173 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485878554 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.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14588 0 0 0 963 34 0 0 25 0 1 0 485878554 71577600 14230 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14230 603 41 0 17434 0
vsize: 69900
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14598 0 0 0 1963 34 0 0 25 0 1 0 485878554 71577600 14240 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14240 603 41 0 17434 0
vsize: 69900
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14600 0 0 0 2962 34 0 0 25 0 1 0 485878554 71577600 14242 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14242 603 41 0 17434 0
vsize: 69900
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14600 0 0 0 3962 34 0 0 25 0 1 0 485878554 71577600 14242 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14242 603 41 0 17434 0
vsize: 69900
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14601 0 0 0 4963 34 0 0 25 0 1 0 485878554 71577600 14243 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14243 603 41 0 17434 0
vsize: 69900
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14618 0 0 0 5963 35 0 0 25 0 1 0 485878554 71712768 14260 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17508 14260 603 41 0 17467 0
vsize: 70032
[startup+70.0012 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14634 0 0 0 6963 35 0 0 25 0 1 0 485878554 71712768 14276 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17508 14276 603 41 0 17467 0
vsize: 70032
[startup+80.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14662 0 0 0 7963 35 0 0 25 0 1 0 485878554 71847936 14304 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 14304 603 41 0 17500 0
vsize: 70164
[startup+90.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14680 0 0 0 8963 35 0 0 25 0 1 0 485878554 71983104 14322 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17574 14322 603 41 0 17533 0
vsize: 70296
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14700 0 0 0 9963 35 0 0 25 0 1 0 485878554 71983104 14342 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 14342 603 41 0 17533 0
vsize: 70296
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14726 0 0 0 10963 35 0 0 25 0 1 0 485878554 72118272 14368 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17607 14368 603 41 0 17566 0
vsize: 70428
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14744 0 0 0 11962 35 0 0 25 0 1 0 485878554 72253440 14386 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17640 14386 603 41 0 17599 0
vsize: 70560
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14772 0 0 0 12963 35 0 0 25 0 1 0 485878554 72388608 14414 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17673 14414 603 41 0 17632 0
vsize: 70692
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14786 0 0 0 13963 35 0 0 25 0 1 0 485878554 72388608 14428 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17673 14428 603 41 0 17632 0
vsize: 70692
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14804 0 0 0 14963 35 0 0 25 0 1 0 485878554 72388608 14446 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17673 14446 603 41 0 17632 0
vsize: 70692
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14825 0 0 0 15963 35 0 0 25 0 1 0 485878554 72523776 14467 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17706 14467 603 41 0 17665 0
vsize: 70824
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14850 0 0 0 16963 35 0 0 25 0 1 0 485878554 72708096 14492 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17751 14492 603 41 0 17710 0
vsize: 71004
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14864 0 0 0 17963 35 0 0 25 0 1 0 485878554 72708096 14506 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17751 14506 603 41 0 17710 0
vsize: 71004
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14877 0 0 0 18963 35 0 0 25 0 1 0 485878554 72708096 14519 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17751 14519 603 41 0 17710 0
vsize: 71004
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14884 0 0 0 19963 35 0 0 25 0 1 0 485878554 72843264 14526 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17784 14526 603 41 0 17743 0
vsize: 71136
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14908 0 0 0 20964 35 0 0 25 0 1 0 485878554 72843264 14550 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17784 14550 603 41 0 17743 0
vsize: 71136
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14924 0 0 0 21964 35 0 0 25 0 1 0 485878554 72978432 14566 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17817 14566 603 41 0 17776 0
vsize: 71268
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14942 0 0 0 22964 35 0 0 25 0 1 0 485878554 72978432 14584 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17817 14584 603 41 0 17776 0
vsize: 71268
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14958 0 0 0 23964 35 0 0 25 0 1 0 485878554 73113600 14600 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17850 14600 603 41 0 17809 0
vsize: 71400
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14973 0 0 0 24964 35 0 0 25 0 1 0 485878554 73113600 14615 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17850 14615 603 41 0 17809 0
vsize: 71400
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14983 0 0 0 25964 35 0 0 25 0 1 0 485878554 73248768 14625 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17883 14625 603 41 0 17842 0
vsize: 71532
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 14994 0 0 0 26964 35 0 0 25 0 1 0 485878554 73248768 14636 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17883 14636 603 41 0 17842 0
vsize: 71532
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15008 0 0 0 27964 36 0 0 25 0 1 0 485878554 73248768 14650 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17883 14650 603 41 0 17842 0
vsize: 71532
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15020 0 0 0 28964 36 0 0 25 0 1 0 485878554 73383936 14662 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 14662 603 41 0 17875 0
vsize: 71664
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15029 0 0 0 29965 36 0 0 25 0 1 0 485878554 73383936 14671 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 14671 603 41 0 17875 0
vsize: 71664
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15038 0 0 0 30965 36 0 0 25 0 1 0 485878554 73383936 14680 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 14680 603 41 0 17875 0
vsize: 71664
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15047 0 0 0 31965 36 0 0 25 0 1 0 485878554 73383936 14689 4294967295 134512640 134672761 3221224544 3221223696 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 14689 603 41 0 17875 0
vsize: 71664
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15053 0 0 0 32965 36 0 0 25 0 1 0 485878554 73519104 14695 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14695 603 41 0 17908 0
vsize: 71796
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15057 0 0 0 33965 36 0 0 25 0 1 0 485878554 73519104 14699 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14699 603 41 0 17908 0
vsize: 71796
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15063 0 0 0 34965 36 0 0 25 0 1 0 485878554 73519104 14705 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14705 603 41 0 17908 0
vsize: 71796
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15076 0 0 0 35965 36 0 0 25 0 1 0 485878554 73519104 14718 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14718 603 41 0 17908 0
vsize: 71796
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15083 0 0 0 36965 36 0 0 25 0 1 0 485878554 73519104 14725 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14725 603 41 0 17908 0
vsize: 71796
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15089 0 0 0 37966 36 0 0 25 0 1 0 485878554 73654272 14731 4294967295 134512640 134672761 3221224544 3221223712 134564436 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14731 603 41 0 17941 0
vsize: 71928
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15090 0 0 0 38966 36 0 0 25 0 1 0 485878554 73654272 14732 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14732 603 41 0 17941 0
vsize: 71928
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15094 0 0 0 39966 36 0 0 25 0 1 0 485878554 73654272 14736 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14736 603 41 0 17941 0
vsize: 71928
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15102 0 0 0 40966 36 0 0 25 0 1 0 485878554 73654272 14744 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14744 603 41 0 17941 0
vsize: 71928
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15106 0 0 0 41966 36 0 0 25 0 1 0 485878554 73654272 14748 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14748 603 41 0 17941 0
vsize: 71928
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15112 0 0 0 42967 36 0 0 25 0 1 0 485878554 73654272 14754 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14754 603 41 0 17941 0
vsize: 71928
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15117 0 0 0 43967 36 0 0 25 0 1 0 485878554 73654272 14759 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14759 603 41 0 17941 0
vsize: 71928
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15120 0 0 0 44967 36 0 0 25 0 1 0 485878554 73654272 14762 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14762 603 41 0 17941 0
vsize: 71928
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15124 0 0 0 45967 36 0 0 25 0 1 0 485878554 73654272 14766 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14766 603 41 0 17941 0
vsize: 71928
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15124 0 0 0 46967 36 0 0 25 0 1 0 485878554 73654272 14766 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14766 603 41 0 17941 0
vsize: 71928
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15126 0 0 0 47967 36 0 0 25 0 1 0 485878554 73789440 14768 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14768 603 41 0 17974 0
vsize: 72060
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15129 0 0 0 48967 36 0 0 25 0 1 0 485878554 73789440 14771 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14771 603 41 0 17974 0
vsize: 72060
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15129 0 0 0 49968 36 0 0 25 0 1 0 485878554 73789440 14771 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14771 603 41 0 17974 0
vsize: 72060
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15131 0 0 0 50967 36 0 0 25 0 1 0 485878554 73789440 14773 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14773 603 41 0 17974 0
vsize: 72060
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15132 0 0 0 51967 36 0 0 25 0 1 0 485878554 73789440 14774 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14774 603 41 0 17974 0
vsize: 72060
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15133 0 0 0 52967 36 0 0 25 0 1 0 485878554 73789440 14775 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14775 603 41 0 17974 0
vsize: 72060
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15136 0 0 0 53967 36 0 0 25 0 1 0 485878554 73789440 14778 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14778 603 41 0 17974 0
vsize: 72060
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15138 0 0 0 54968 36 0 0 25 0 1 0 485878554 73789440 14780 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14780 603 41 0 17974 0
vsize: 72060
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15140 0 0 0 55968 36 0 0 25 0 1 0 485878554 73789440 14782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14782 603 41 0 17974 0
vsize: 72060
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15142 0 0 0 56968 36 0 0 25 0 1 0 485878554 73789440 14784 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14784 603 41 0 17974 0
vsize: 72060
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15144 0 0 0 57968 36 0 0 25 0 1 0 485878554 73789440 14786 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14786 603 41 0 17974 0
vsize: 72060
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15144 0 0 0 58968 36 0 0 25 0 1 0 485878554 73789440 14786 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14786 603 41 0 17974 0
vsize: 72060
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15147 0 0 0 59969 36 0 0 25 0 1 0 485878554 73789440 14789 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14789 603 41 0 17974 0
vsize: 72060
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15147 0 0 0 60969 36 0 0 25 0 1 0 485878554 73789440 14789 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14789 603 41 0 17974 0
vsize: 72060
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15148 0 0 0 61969 36 0 0 25 0 1 0 485878554 73789440 14790 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14790 603 41 0 17974 0
vsize: 72060
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15148 0 0 0 62970 36 0 0 25 0 1 0 485878554 73789440 14790 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14790 603 41 0 17974 0
vsize: 72060
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15150 0 0 0 63970 36 0 0 25 0 1 0 485878554 73789440 14792 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14792 603 41 0 17974 0
vsize: 72060
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15150 0 0 0 64970 36 0 0 25 0 1 0 485878554 73789440 14792 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14792 603 41 0 17974 0
vsize: 72060
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15151 0 0 0 65971 36 0 0 25 0 1 0 485878554 73789440 14793 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14793 603 41 0 17974 0
vsize: 72060
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15153 0 0 0 66969 37 0 0 25 0 1 0 485878554 73789440 14795 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14795 603 41 0 17974 0
vsize: 72060
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15158 0 0 0 67968 37 0 0 25 0 1 0 485878554 73789440 14800 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14800 603 41 0 17974 0
vsize: 72060
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15160 0 0 0 68969 37 0 0 25 0 1 0 485878554 73789440 14802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15160 0 0 0 69969 37 0 0 25 0 1 0 485878554 73789440 14802 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15160 0 0 0 70969 37 0 0 25 0 1 0 485878554 73789440 14802 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15161 0 0 0 71969 37 0 0 25 0 1 0 485878554 73789440 14803 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14803 603 41 0 17974 0
vsize: 72060
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15163 0 0 0 72970 37 0 0 25 0 1 0 485878554 73789440 14805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14805 603 41 0 17974 0
vsize: 72060
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15164 0 0 0 73970 37 0 0 25 0 1 0 485878554 73789440 14806 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14806 603 41 0 17974 0
vsize: 72060
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15166 0 0 0 74970 37 0 0 25 0 1 0 485878554 73789440 14808 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14808 603 41 0 17974 0
vsize: 72060
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15166 0 0 0 75970 37 0 0 25 0 1 0 485878554 73789440 14808 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14808 603 41 0 17974 0
vsize: 72060
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15168 0 0 0 76970 37 0 0 25 0 1 0 485878554 73789440 14810 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14810 603 41 0 17974 0
vsize: 72060
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15171 0 0 0 77970 37 0 0 25 0 1 0 485878554 73789440 14813 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14813 603 41 0 17974 0
vsize: 72060
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15174 0 0 0 78971 37 0 0 25 0 1 0 485878554 73789440 14816 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14816 603 41 0 17974 0
vsize: 72060
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15175 0 0 0 79971 37 0 0 25 0 1 0 485878554 73924608 14817 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14817 603 41 0 18007 0
vsize: 72192
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15175 0 0 0 80971 37 0 0 25 0 1 0 485878554 73924608 14817 4294967295 134512640 134672761 3221224544 3221223696 134564780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14817 603 41 0 18007 0
vsize: 72192
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15176 0 0 0 81971 37 0 0 25 0 1 0 485878554 73924608 14818 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14818 603 41 0 18007 0
vsize: 72192
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15176 0 0 0 82971 37 0 0 25 0 1 0 485878554 73924608 14818 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14818 603 41 0 18007 0
vsize: 72192
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15178 0 0 0 83972 37 0 0 25 0 1 0 485878554 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15178 0 0 0 84972 37 0 0 25 0 1 0 485878554 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15178 0 0 0 85972 37 0 0 25 0 1 0 485878554 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15178 0 0 0 86971 37 0 0 25 0 1 0 485878554 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32174
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15179 0 0 0 87971 37 0 0 25 0 1 0 485878554 73924608 14821 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14821 603 41 0 18007 0
vsize: 72192
[startup+890.026 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32227
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15179 0 0 0 88970 38 0 0 25 0 1 0 485878554 73924608 14821 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14821 603 41 0 18007 0
vsize: 72192
[startup+900.027 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32227
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15180 0 0 0 89970 38 0 0 25 0 1 0 485878554 73924608 14822 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+910.026 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32227
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15180 0 0 0 90970 39 0 0 25 0 1 0 485878554 73924608 14822 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+920.027 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32227
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15181 0 0 0 91970 39 0 0 25 0 1 0 485878554 73924608 14823 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+930.027 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32227
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15181 0 0 0 92970 39 0 0 25 0 1 0 485878554 73924608 14823 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+940.027 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32227
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15181 0 0 0 93970 39 0 0 25 0 1 0 485878554 73924608 14823 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+950.028 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32227
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15181 0 0 0 94970 40 0 0 25 0 1 0 485878554 73924608 14823 4294967295 134512640 134672761 3221224544 3221223760 134561950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+960.028 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15181 0 0 0 95970 40 0 0 25 0 1 0 485878554 73924608 14823 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+970.027 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15181 0 0 0 96970 40 0 0 25 0 1 0 485878554 73924608 14823 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+980.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15190 0 0 0 97969 41 0 0 25 0 1 0 485878554 73924608 14832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14832 603 41 0 18007 0
vsize: 72192
[startup+990.032 s]
Raw data (loadavg): 1.01 0.99 0.91 3/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15190 0 0 0 98970 41 0 0 25 0 1 0 485878554 73924608 14832 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14832 603 41 0 18007 0
vsize: 72192
[startup+1000.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15191 0 0 0 99970 41 0 0 25 0 1 0 485878554 73924608 14833 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14833 603 41 0 18007 0
vsize: 72192
[startup+1010.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15191 0 0 0 100970 41 0 0 25 0 1 0 485878554 73924608 14833 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14833 603 41 0 18007 0
vsize: 72192
[startup+1020.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15192 0 0 0 101970 41 0 0 25 0 1 0 485878554 73924608 14834 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15192 0 0 0 102971 41 0 0 25 0 1 0 485878554 73924608 14834 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15192 0 0 0 103971 41 0 0 25 0 1 0 485878554 73924608 14834 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15194 0 0 0 104971 41 0 0 25 0 1 0 485878554 73924608 14836 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14836 603 41 0 18007 0
vsize: 72192
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15195 0 0 0 105971 41 0 0 25 0 1 0 485878554 73924608 14837 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14837 603 41 0 18007 0
vsize: 72192
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15196 0 0 0 106971 41 0 0 25 0 1 0 485878554 73924608 14838 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14838 603 41 0 18007 0
vsize: 72192
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15197 0 0 0 107972 41 0 0 25 0 1 0 485878554 73924608 14839 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14839 603 41 0 18007 0
vsize: 72192
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15199 0 0 0 108972 41 0 0 25 0 1 0 485878554 73924608 14841 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14841 603 41 0 18007 0
vsize: 72192
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15199 0 0 0 109972 41 0 0 25 0 1 0 485878554 73924608 14841 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14841 603 41 0 18007 0
vsize: 72192
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15200 0 0 0 110972 41 0 0 25 0 1 0 485878554 73924608 14842 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15200 0 0 0 111972 41 0 0 25 0 1 0 485878554 73924608 14842 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15201 0 0 0 112973 41 0 0 25 0 1 0 485878554 73924608 14843 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14843 603 41 0 18007 0
vsize: 72192
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15202 0 0 0 113972 41 0 0 25 0 1 0 485878554 73924608 14844 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14844 603 41 0 18007 0
vsize: 72192
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15203 0 0 0 114972 41 0 0 25 0 1 0 485878554 73924608 14845 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14845 603 41 0 18007 0
vsize: 72192
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15203 0 0 0 115972 41 0 0 25 0 1 0 485878554 73924608 14845 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14845 603 41 0 18007 0
vsize: 72192
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15204 0 0 0 116973 41 0 0 25 0 1 0 485878554 73924608 14846 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14846 603 41 0 18007 0
vsize: 72192
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15205 0 0 0 117973 41 0 0 25 0 1 0 485878554 73924608 14847 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14847 603 41 0 18007 0
vsize: 72192
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15205 0 0 0 118973 41 0 0 25 0 1 0 485878554 73924608 14847 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14847 603 41 0 18007 0
vsize: 72192
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32229
Raw data (stat): 32174 (minisat+) R 32173 32461 32460 0 -1 0 15206 0 0 0 119973 41 0 0 25 0 1 0 485878554 73924608 14848 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14848 603 41 0 18007 0
vsize: 72192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32229
Raw data (stat): 32174 (minisat+) Z 32173 32461 32460 0 -1 12 15208 0 0 0 119973 44 0 0 25 0 1 0 485878554 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.18
CPU user time (s): 1199.74
CPU system time (s): 0.445932
CPU usage (%): 100.008
Max. virtual memory (Kb): 72192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####