PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-air04.opb
MD5SUM	26490113618ae9605b5ebe6370b5910b
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.120981
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 18361

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        420572 kB
Buffers:         28380 kB
Cached:         560936 kB
SwapCached:        516 kB
Active:          57360 kB
Inactive:       533952 kB
HighTotal:      131008 kB
HighFree:        25592 kB
LowTotal:       903652 kB
LowFree:        394980 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            16864 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:51:10 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 18171 7 1200.25 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.85 0.94 0.90 2/54 8406
Raw data (stat): 8406 (runsolver) R 8405 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545816604 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.0001 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14588 0 0 0 960 39 0 0 25 0 1 0 545816604 71577600 14230 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14230 603 41 0 17434 0
vsize: 69900
[startup+19.9994 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14598 0 0 0 1959 39 0 0 25 0 1 0 545816604 71577600 14240 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14240 603 41 0 17434 0
vsize: 69900
[startup+30.0005 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14600 0 0 0 2959 40 0 0 25 0 1 0 545816604 71577600 14242 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14242 603 41 0 17434 0
vsize: 69900
[startup+40.0002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14600 0 0 0 3959 40 0 0 25 0 1 0 545816604 71577600 14242 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14242 603 41 0 17434 0
vsize: 69900
[startup+50.0006 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14601 0 0 0 4958 40 0 0 25 0 1 0 545816604 71577600 14243 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14243 603 41 0 17434 0
vsize: 69900
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14617 0 0 0 5958 41 0 0 25 0 1 0 545816604 71712768 14259 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17508 14259 603 41 0 17467 0
vsize: 70032
[startup+70.0004 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14634 0 0 0 6957 42 0 0 25 0 1 0 545816604 71712768 14276 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17508 14276 603 41 0 17467 0
vsize: 70032
[startup+80.0007 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14659 0 0 0 7957 42 0 0 25 0 1 0 545816604 71847936 14301 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 14301 603 41 0 17500 0
vsize: 70164
[startup+90.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14678 0 0 0 8957 42 0 0 25 0 1 0 545816604 71983104 14320 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 14320 603 41 0 17533 0
vsize: 70296
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14699 0 0 0 9957 43 0 0 25 0 1 0 545816604 71983104 14341 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 14341 603 41 0 17533 0
vsize: 70296
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14723 0 0 0 10956 43 0 0 25 0 1 0 545816604 72118272 14365 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17607 14365 603 41 0 17566 0
vsize: 70428
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14742 0 0 0 11957 43 0 0 25 0 1 0 545816604 72253440 14384 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17640 14384 603 41 0 17599 0
vsize: 70560
[startup+130.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14771 0 0 0 12957 43 0 0 25 0 1 0 545816604 72253440 14413 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17640 14413 603 41 0 17599 0
vsize: 70560
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14785 0 0 0 13957 43 0 0 25 0 1 0 545816604 72388608 14427 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17673 14427 603 41 0 17632 0
vsize: 70692
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14804 0 0 0 14957 43 0 0 25 0 1 0 545816604 72388608 14446 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14822 0 0 0 15957 44 0 0 25 0 1 0 545816604 72523776 14464 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17706 14464 603 41 0 17665 0
vsize: 70824
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14850 0 0 0 16957 44 0 0 25 0 1 0 545816604 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.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14863 0 0 0 17958 44 0 0 25 0 1 0 545816604 72708096 14505 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17751 14505 603 41 0 17710 0
vsize: 71004
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14876 0 0 0 18958 44 0 0 25 0 1 0 545816604 72708096 14518 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17751 14518 603 41 0 17710 0
vsize: 71004
[startup+200.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14882 0 0 0 19958 44 0 0 25 0 1 0 545816604 72843264 14524 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17784 14524 603 41 0 17743 0
vsize: 71136
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14904 0 0 0 20958 44 0 0 25 0 1 0 545816604 72843264 14546 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17784 14546 603 41 0 17743 0
vsize: 71136
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14921 0 0 0 21958 44 0 0 25 0 1 0 545816604 72978432 14563 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17817 14563 603 41 0 17776 0
vsize: 71268
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14941 0 0 0 22958 44 0 0 25 0 1 0 545816604 72978432 14583 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17817 14583 603 41 0 17776 0
vsize: 71268
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14956 0 0 0 23958 44 0 0 25 0 1 0 545816604 73113600 14598 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17850 14598 603 41 0 17809 0
vsize: 71400
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14970 0 0 0 24958 44 0 0 25 0 1 0 545816604 73113600 14612 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17850 14612 603 41 0 17809 0
vsize: 71400
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14982 0 0 0 25958 44 0 0 25 0 1 0 545816604 73113600 14624 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17850 14624 603 41 0 17809 0
vsize: 71400
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 14992 0 0 0 26959 44 0 0 25 0 1 0 545816604 73248768 14634 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17883 14634 603 41 0 17842 0
vsize: 71532
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15005 0 0 0 27959 45 0 0 25 0 1 0 545816604 73248768 14647 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17883 14647 603 41 0 17842 0
vsize: 71532
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15020 0 0 0 28959 45 0 0 25 0 1 0 545816604 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15028 0 0 0 29959 45 0 0 25 0 1 0 545816604 73383936 14670 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 14670 603 41 0 17875 0
vsize: 71664
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15036 0 0 0 30959 45 0 0 25 0 1 0 545816604 73383936 14678 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 14678 603 41 0 17875 0
vsize: 71664
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15046 0 0 0 31959 45 0 0 25 0 1 0 545816604 73383936 14688 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 14688 603 41 0 17875 0
vsize: 71664
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15053 0 0 0 32959 45 0 0 25 0 1 0 545816604 73519104 14695 4294967295 134512640 134672761 3221224544 3221223716 134556680 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15056 0 0 0 33959 45 0 0 25 0 1 0 545816604 73519104 14698 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14698 603 41 0 17908 0
vsize: 71796
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15062 0 0 0 34960 45 0 0 25 0 1 0 545816604 73519104 14704 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14704 603 41 0 17908 0
vsize: 71796
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15074 0 0 0 35960 45 0 0 25 0 1 0 545816604 73519104 14716 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14716 603 41 0 17908 0
vsize: 71796
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15082 0 0 0 36960 45 0 0 25 0 1 0 545816604 73519104 14724 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17949 14724 603 41 0 17908 0
vsize: 71796
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15089 0 0 0 37960 45 0 0 25 0 1 0 545816604 73654272 14731 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15090 0 0 0 38960 45 0 0 25 0 1 0 545816604 73654272 14732 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14732 603 41 0 17941 0
vsize: 71928
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15093 0 0 0 39959 46 0 0 25 0 1 0 545816604 73654272 14735 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14735 603 41 0 17941 0
vsize: 71928
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15101 0 0 0 40959 46 0 0 25 0 1 0 545816604 73654272 14743 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14743 603 41 0 17941 0
vsize: 71928
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15105 0 0 0 41959 46 0 0 25 0 1 0 545816604 73654272 14747 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14747 603 41 0 17941 0
vsize: 71928
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15111 0 0 0 42960 46 0 0 25 0 1 0 545816604 73654272 14753 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14753 603 41 0 17941 0
vsize: 71928
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15116 0 0 0 43960 46 0 0 25 0 1 0 545816604 73654272 14758 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17982 14758 603 41 0 17941 0
vsize: 71928
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15120 0 0 0 44960 46 0 0 25 0 1 0 545816604 73654272 14762 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15124 0 0 0 45960 46 0 0 25 0 1 0 545816604 73654272 14766 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.015 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15124 0 0 0 46960 46 0 0 25 0 1 0 545816604 73654272 14766 4294967295 134512640 134672761 3221224544 3221223668 134566043 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.015 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15126 0 0 0 47960 46 0 0 25 0 1 0 545816604 73789440 14768 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.015 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15127 0 0 0 48960 46 0 0 25 0 1 0 545816604 73789440 14769 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14769 603 41 0 17974 0
vsize: 72060
[startup+500.015 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15129 0 0 0 49961 46 0 0 25 0 1 0 545816604 73789440 14771 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.015 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15131 0 0 0 50960 46 0 0 25 0 1 0 545816604 73789440 14773 4294967295 134512640 134672761 3221224544 3221223808 134562218 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.015 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15132 0 0 0 51959 46 0 0 25 0 1 0 545816604 73789440 14774 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.016 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15133 0 0 0 52960 46 0 0 25 0 1 0 545816604 73789440 14775 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.016 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15134 0 0 0 53960 46 0 0 25 0 1 0 545816604 73789440 14776 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14776 603 41 0 17974 0
vsize: 72060
[startup+550.017 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15138 0 0 0 54960 46 0 0 25 0 1 0 545816604 73789440 14780 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.017 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15140 0 0 0 55960 47 0 0 25 0 1 0 545816604 73789440 14782 4294967295 134512640 134672761 3221224544 3221223716 134556680 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.016 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15141 0 0 0 56960 47 0 0 25 0 1 0 545816604 73789440 14783 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14783 603 41 0 17974 0
vsize: 72060
[startup+580.017 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15143 0 0 0 57960 47 0 0 25 0 1 0 545816604 73789440 14785 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14785 603 41 0 17974 0
vsize: 72060
[startup+590.017 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15144 0 0 0 58961 47 0 0 25 0 1 0 545816604 73789440 14786 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15147 0 0 0 59961 47 0 0 25 0 1 0 545816604 73789440 14789 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15147 0 0 0 60961 47 0 0 25 0 1 0 545816604 73789440 14789 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.018 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15148 0 0 0 61961 47 0 0 25 0 1 0 545816604 73789440 14790 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.018 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15148 0 0 0 62961 47 0 0 25 0 1 0 545816604 73789440 14790 4294967295 134512640 134672761 3221224544 3221223696 134565076 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.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15149 0 0 0 63962 47 0 0 25 0 1 0 545816604 73789440 14791 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 14791 603 41 0 17974 0
vsize: 72060
[startup+650.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15150 0 0 0 64962 47 0 0 25 0 1 0 545816604 73789440 14792 4294967295 134512640 134672761 3221224544 3221223760 134561997 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.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15151 0 0 0 65962 47 0 0 25 0 1 0 545816604 73789440 14793 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15153 0 0 0 66961 47 0 0 25 0 1 0 545816604 73789440 14795 4294967295 134512640 134672761 3221224544 3221223712 134560806 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.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15158 0 0 0 67961 47 0 0 25 0 1 0 545816604 73789440 14800 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14800 603 41 0 17974 0
vsize: 72060
[startup+690.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15160 0 0 0 68961 47 0 0 25 0 1 0 545816604 73789440 14802 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+700.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15160 0 0 0 69961 48 0 0 25 0 1 0 545816604 73789440 14802 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+710.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15160 0 0 0 70960 48 0 0 25 0 1 0 545816604 73789440 14802 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+720.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15161 0 0 0 71960 48 0 0 25 0 1 0 545816604 73789440 14803 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14803 603 41 0 17974 0
vsize: 72060
[startup+730.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15163 0 0 0 72960 49 0 0 25 0 1 0 545816604 73789440 14805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14805 603 41 0 17974 0
vsize: 72060
[startup+740.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15164 0 0 0 73959 49 0 0 25 0 1 0 545816604 73789440 14806 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14806 603 41 0 17974 0
vsize: 72060
[startup+750.023 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15166 0 0 0 74959 50 0 0 25 0 1 0 545816604 73789440 14808 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14808 603 41 0 17974 0
vsize: 72060
[startup+760.027 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15166 0 0 0 75959 50 0 0 25 0 1 0 545816604 73789440 14808 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14808 603 41 0 17974 0
vsize: 72060
[startup+770.027 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15168 0 0 0 76959 51 0 0 25 0 1 0 545816604 73789440 14810 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14810 603 41 0 17974 0
vsize: 72060
[startup+780.033 s]
Raw data (loadavg): 1.12 1.03 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15169 0 0 0 77959 51 0 0 25 0 1 0 545816604 73789440 14811 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14811 603 41 0 17974 0
vsize: 72060
[startup+790.036 s]
Raw data (loadavg): 1.10 1.03 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15172 0 0 0 78958 52 0 0 25 0 1 0 545816604 73789440 14814 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14814 603 41 0 17974 0
vsize: 72060
[startup+800.044 s]
Raw data (loadavg): 1.09 1.03 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15174 0 0 0 79959 52 0 0 25 0 1 0 545816604 73789440 14816 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14816 603 41 0 17974 0
vsize: 72060
[startup+810.057 s]
Raw data (loadavg): 1.07 1.03 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15175 0 0 0 80960 52 0 0 25 0 1 0 545816604 73924608 14817 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14817 603 41 0 18007 0
vsize: 72192
[startup+820.063 s]
Raw data (loadavg): 1.06 1.03 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15176 0 0 0 81961 53 0 0 25 0 1 0 545816604 73924608 14818 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14818 603 41 0 18007 0
vsize: 72192
[startup+830.063 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15176 0 0 0 82961 53 0 0 25 0 1 0 545816604 73924608 14818 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14818 603 41 0 18007 0
vsize: 72192
[startup+840.063 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15177 0 0 0 83960 53 0 0 25 0 1 0 545816604 73924608 14819 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14819 603 41 0 18007 0
vsize: 72192
[startup+850.064 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15178 0 0 0 84960 54 0 0 25 0 1 0 545816604 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+860.065 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15178 0 0 0 85960 54 0 0 25 0 1 0 545816604 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+870.064 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15178 0 0 0 86959 54 0 0 25 0 1 0 545816604 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.065 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15178 0 0 0 87959 54 0 0 25 0 1 0 545816604 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+890.066 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15179 0 0 0 88959 55 0 0 25 0 1 0 545816604 73924608 14821 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14821 603 41 0 18007 0
vsize: 72192
[startup+900.067 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15180 0 0 0 89959 55 0 0 25 0 1 0 545816604 73924608 14822 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+910.067 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15180 0 0 0 90959 55 0 0 25 0 1 0 545816604 73924608 14822 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+920.068 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15180 0 0 0 91959 56 0 0 25 0 1 0 545816604 73924608 14822 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+930.069 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15181 0 0 0 92959 56 0 0 25 0 1 0 545816604 73924608 14823 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+940.069 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15181 0 0 0 93959 56 0 0 25 0 1 0 545816604 73924608 14823 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+950.07 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15181 0 0 0 94958 56 0 0 25 0 1 0 545816604 73924608 14823 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+960.071 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15181 0 0 0 95958 57 0 0 25 0 1 0 545816604 73924608 14823 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+970.07 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15181 0 0 0 96958 57 0 0 25 0 1 0 545816604 73924608 14823 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.071 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15181 0 0 0 97958 57 0 0 25 0 1 0 545816604 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+990.072 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15190 0 0 0 98958 57 0 0 25 0 1 0 545816604 73924608 14832 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.08 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15191 0 0 0 99959 57 0 0 25 0 1 0 545816604 73924608 14833 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14833 603 41 0 18007 0
vsize: 72192
[startup+1010.08 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15191 0 0 0 100959 57 0 0 25 0 1 0 545816604 73924608 14833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14833 603 41 0 18007 0
vsize: 72192
[startup+1020.08 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15192 0 0 0 101959 57 0 0 25 0 1 0 545816604 73924608 14834 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15192 0 0 0 102959 57 0 0 25 0 1 0 545816604 73924608 14834 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15192 0 0 0 103959 57 0 0 25 0 1 0 545816604 73924608 14834 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15193 0 0 0 104960 57 0 0 25 0 1 0 545816604 73924608 14835 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14835 603 41 0 18007 0
vsize: 72192
[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15194 0 0 0 105960 57 0 0 25 0 1 0 545816604 73924608 14836 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14836 603 41 0 18007 0
vsize: 72192
[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15195 0 0 0 106960 57 0 0 25 0 1 0 545816604 73924608 14837 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14837 603 41 0 18007 0
vsize: 72192
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15196 0 0 0 107961 57 0 0 25 0 1 0 545816604 73924608 14838 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14838 603 41 0 18007 0
vsize: 72192
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15197 0 0 0 108962 57 0 0 25 0 1 0 545816604 73924608 14839 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14839 603 41 0 18007 0
vsize: 72192
[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15199 0 0 0 109962 58 0 0 25 0 1 0 545816604 73924608 14841 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14841 603 41 0 18007 0
vsize: 72192
[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15200 0 0 0 110962 58 0 0 25 0 1 0 545816604 73924608 14842 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15200 0 0 0 111962 58 0 0 25 0 1 0 545816604 73924608 14842 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15200 0 0 0 112962 58 0 0 25 0 1 0 545816604 73924608 14842 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15201 0 0 0 113962 58 0 0 25 0 1 0 545816604 73924608 14843 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14843 603 41 0 18007 0
vsize: 72192
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15202 0 0 0 114961 58 0 0 25 0 1 0 545816604 73924608 14844 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14844 603 41 0 18007 0
vsize: 72192
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15203 0 0 0 115961 58 0 0 25 0 1 0 545816604 73924608 14845 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14845 603 41 0 18007 0
vsize: 72192
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15204 0 0 0 116961 58 0 0 25 0 1 0 545816604 73924608 14846 4294967295 134512640 134672761 3221224544 3221223716 134553588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14846 603 41 0 18007 0
vsize: 72192
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15205 0 0 0 117961 58 0 0 25 0 1 0 545816604 73924608 14847 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14847 603 41 0 18007 0
vsize: 72192
[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15205 0 0 0 118962 58 0 0 25 0 1 0 545816604 73924608 14847 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14847 603 41 0 18007 0
vsize: 72192
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8406
Raw data (stat): 8406 (minisat+) R 8405 27565 27564 0 -1 0 15205 0 0 0 119963 58 0 0 25 0 1 0 545816604 73924608 14847 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14847 603 41 0 18007 0
vsize: 72192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 8406
Raw data (stat): 8406 (minisat+) Z 8405 27565 27564 0 -1 12 15207 0 0 0 119963 61 0 0 25 0 1 0 545816604 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.13
CPU time (s): 1200.25
CPU user time (s): 1199.63
CPU system time (s): 0.614906
CPU usage (%): 100.009
Max. virtual memory (Kb): 72192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####