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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-sctap2.opb
MD5SUM	c56066a13a725fcc9c143db3d9f8cc06
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	24450007
Optimality of the best value was proved	NO
Number of terms in the objective function	28200
Biggest coefficient in the objective function	41943040
Number of bits for the biggest coefficient in the objective function	26
Sum of the numbers in the objective function	25763487750
Number of bits of the sum of numbers in the objective function	35
Biggest number in a constraint	41943040
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	25763487750
Number of bits of the biggest sum of numbers	35
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.2
Number of variables	37600
Total number of constraints	1090
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1090
Minimum length of a constraint	60
Maximum length of a constraint	480
Trace number 19618

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        333032 kB
Buffers:         31840 kB
Cached:         640456 kB
SwapCached:         20 kB
Active:         147000 kB
Inactive:       527908 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        332780 kB
SwapTotal:     2097892 kB
SwapFree:      2097664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            21064 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:45:30 (client local time) WITH STATUS 0 IN 1200.45 SECONDS
stats: 16325 7 1200.45 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1503 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssss
c ---[1507]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1506]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1505]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1504]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1503]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1502]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1501]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1500]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1499]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1498]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1497]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1496]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1495]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1494]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1493]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1492]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1491]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1490]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1489]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1488]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1487]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1486]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1485]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1484]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1483]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1482]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1481]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1480]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1479]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1478]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1477]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1476]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1475]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1474]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1473]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1472]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1471]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1470]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1469]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1468]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1467]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1466]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1465]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1464]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1463]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1462]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1461]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1460]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1459]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1458]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1457]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1456]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1455]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1454]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1453]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1452]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1451]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1450]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1449]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1448]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1447]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1446]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1445]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1444]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1443]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1442]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1441]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1440]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1439]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1438]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1437]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1436]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1435]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1434]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1433]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1432]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1431]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1430]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1429]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1428]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1427]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1426]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1425]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1424]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1423]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1422]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1421]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1420]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1419]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1418]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1417]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1416]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1415]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1414]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1413]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1412]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1411]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1410]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1409]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1408]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1407]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1406]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1405]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1404]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1403]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1402]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1401]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1400]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1399]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1398]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1397]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1396]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1395]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1394]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1393]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1392]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1391]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1390]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1389]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1388]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1387]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1386]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1385]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1384]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1383]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1382]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1381]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1380]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1379]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1378]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1377]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1376]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1375]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1374]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1373]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1372]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1371]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1370]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1369]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1368]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1367]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1366]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1365]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1364]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1363]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1362]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1361]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1360]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1359]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1358]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1357]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1356]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1355]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1354]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1353]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1352]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1351]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1350]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1349]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1348]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1347]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1346]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1345]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1344]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1343]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1342]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1341]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1340]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1339]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1338]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1337]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1336]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1335]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1334]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1333]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1332]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1331]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1330]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1329]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1328]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1327]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1326]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1325]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1324]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1323]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1322]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1321]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1320]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1319]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[1318]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1317]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1316]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1315]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1314]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1313]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1312]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1311]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1310]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1309]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1308]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1307]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1306]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1305]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1304]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1303]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1302]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1301]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1300]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1299]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1298]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1297]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1296]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1295]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1294]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1293]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1292]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1291]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1290]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1289]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1288]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1287]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1286]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1285]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1284]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1283]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1282]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1281]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1280]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1279]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1278]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1277]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1276]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1275]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1274]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1273]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1272]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1271]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1270]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1269]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1268]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1267]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1266]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1265]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1264]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1263]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1262]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1261]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1260]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1259]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1258]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1257]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1256]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1255]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1254]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1253]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1252]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1251]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1250]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1249]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1248]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1247]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1246]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1245]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1244]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1243]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1242]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1241]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1240]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1239]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1238]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1237]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1236]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1235]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1234]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1233]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1232]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1231]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1230]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1229]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1228]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1227]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1226]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1225]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1224]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1223]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1222]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1221]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1220]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1219]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1218]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1217]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1216]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1215]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1214]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1213]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1212]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1211]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1210]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1209]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1208]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1207]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1206]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1205]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1204]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1203]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1202]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1201]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1200]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1199]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1198]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1197]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1196]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1195]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1194]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1193]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[1192]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1191]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1190]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1189]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1188]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1187]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1186]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1185]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1184]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1183]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1182]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1181]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1180]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1179]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1178]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1177]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1176]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1175]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1174]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1173]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1172]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1171]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1170]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1169]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1168]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1167]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1166]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[1165]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1164]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1163]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1162]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1161]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1160]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1159]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1158]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1157]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1156]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1155]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1154]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1153]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1152]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1151]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1150]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1149]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1148]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1147]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1146]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1145]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1144]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1143]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1142]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1141]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1140]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1139]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1138]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1137]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1136]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1135]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1134]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1133]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1132]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1131]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1130]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1129]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1128]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1127]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1126]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1125]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1124]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1123]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1122]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1121]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1120]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1119]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1118]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1117]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1116]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1115]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1114]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1113]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1112]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1111]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1110]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1109]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1108]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1107]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1106]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1105]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1104]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1103]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1102]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1101]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1100]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1099]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1098]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1097]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1096]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1095]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1094]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1093]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1092]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1091]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1090]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1089]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1088]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1087]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1086]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1085]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[1083]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1081]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1079]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1077]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1075]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1073]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1071]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1069]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1067]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1065]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1063]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1061]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1059]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1057]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1055]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1053]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1051]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1049]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1047]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1045]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1043]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1041]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1039]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1037]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1035]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1033]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1031]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1029]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1027]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1025]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1023]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1021]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1019]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1017]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1015]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1013]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1011]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1009]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1007]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1005]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1003]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1001]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 999]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 997]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 995]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 993]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 991]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 989]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 987]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 985]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 983]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 981]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 979]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 977]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 975]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 973]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 971]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 969]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 967]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 965]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 963]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 961]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 959]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 957]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 955]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 953]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 951]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 949]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 947]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 945]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 943]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 941]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 939]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 937]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 935]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 933]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 931]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 929]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 927]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 925]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 923]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 921]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 919]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 917]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 915]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 913]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 911]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 909]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 907]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 905]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 903]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 901]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 899]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 897]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 895]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 893]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 891]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 889]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 887]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 885]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 883]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 881]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 879]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 877]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 875]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 873]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 871]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 869]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 867]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 865]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 863]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 861]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 859]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 857]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 855]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 853]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 851]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 849]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 847]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 845]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 843]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 841]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 839]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 837]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 835]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 833]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 831]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 829]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 827]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 825]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 823]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 821]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 819]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 817]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 815]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 813]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 811]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 809]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 807]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 805]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 803]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 801]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 799]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 797]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 795]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 793]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 791]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 789]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 787]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 785]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 783]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 781]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 779]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 777]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 775]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 773]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 771]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 769]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 767]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 765]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 763]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 761]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 759]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 757]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 755]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 753]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 751]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 749]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 747]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 745]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 743]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 741]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 739]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 737]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 735]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 733]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 731]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 729]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 727]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 725]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 723]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 721]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 719]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 717]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 715]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 713]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 711]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 709]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 707]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 705]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 703]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 701]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 699]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 697]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 695]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 693]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 691]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 689]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 687]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 685]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 683]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 681]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 679]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 677]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 675]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 673]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 671]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 669]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 667]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 665]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 663]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 661]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 659]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 657]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 655]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 653]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 651]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 649]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 647]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 645]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 643]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 641]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 639]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 637]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 635]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 633]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 631]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 629]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 627]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 625]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 623]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 621]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 619]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 617]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 615]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 613]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 611]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 609]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 607]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 605]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 603]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 601]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 599]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 597]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 595]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 593]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 591]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 589]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 587]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 585]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 583]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 581]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 579]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 577]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 575]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 573]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 571]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 569]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 567]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 565]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 563]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 561]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 559]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 557]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 555]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 553]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 551]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 549]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 547]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 545]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 543]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 541]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 539]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 537]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 535]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 533]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 531]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 529]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 527]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 525]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 523]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 521]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 519]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 517]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 515]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 513]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 511]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 509]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 507]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 505]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 503]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 501]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 499]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 497]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 495]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 493]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 491]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 489]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 487]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 485]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 483]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 481]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 479]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 477]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 475]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 473]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 471]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 469]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 467]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 465]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 463]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 461]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 459]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 457]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 455]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 453]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 451]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 449]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 447]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 445]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 443]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 441]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 439]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 437]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 435]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 433]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 431]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 429]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 427]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 425]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 423]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 421]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 419]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 417]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 415]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 413]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 411]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 409]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 407]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 405]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 403]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 401]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 399]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 397]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 395]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 393]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 391]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 389]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 387]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 385]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 383]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 381]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 379]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 377]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 375]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 373]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 371]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 369]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 367]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 365]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 363]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 361]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 359]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 357]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 355]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 353]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 351]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 349]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 347]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 345]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 343]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 341]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 339]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 337]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 335]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 333]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 331]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 329]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 327]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 325]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 323]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 321]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 319]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 317]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 315]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 313]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 311]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 309]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 307]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 305]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 303]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 301]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 299]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 297]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 295]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 293]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 291]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 289]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 287]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 285]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 283]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 281]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 279]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 277]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 275]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 273]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 271]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 269]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 267]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 265]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 263]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 261]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 259]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 257]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 255]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 253]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 251]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 249]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 247]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 245]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 243]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 241]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 239]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 237]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 235]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 233]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 231]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 229]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 227]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 225]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 223]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 221]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 219]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 217]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 215]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 213]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 211]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 209]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 207]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 205]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 203]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 201]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 199]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 197]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 195]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 193]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 191]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 189]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 187]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 185]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 183]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 181]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 179]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 177]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 175]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 173]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 171]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 169]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 167]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 165]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 163]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 161]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 159]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 157]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 155]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 153]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 151]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 149]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 147]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 145]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 144]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 143]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 142]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 141]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 140]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 139]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 138]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 137]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 136]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 135]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 134]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 133]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 132]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 131]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 130]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 129]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 128]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 127]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 126]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 125]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 124]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 123]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 122]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 121]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 120]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 119]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 118]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 117]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 115]---> Adder-cost: 974   maxlim: 4217009   bits: 24/23
c ---[ 114]---> Adder-cost: 972   maxlim: 4218289   bits: 24/23
c ---[ 113]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[ 112]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[ 111]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 110]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 109]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 108]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[ 107]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 106]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 105]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 104]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 103]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 102]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 101]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 100]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[  99]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[  98]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  96]---> Adder-cost: 974   maxlim: 4214449   bits: 24/23
c ---[  95]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  94]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  93]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  92]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  91]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  90]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  89]---> Adder-cost: 970   maxlim: 4213809   bits: 24/23
c ---[  88]---> Adder-cost: 712   maxlim: 3162809   bits: 23/22
c ---[  86]---> Adder-cost: 712   maxlim: 3164089   bits: 23/22
c ---[  85]---> Adder-cost: 672   maxlim: 3164729   bits: 23/22
c ---[  84]---> Adder-cost: 672   maxlim: 3165369   bits: 23/22
c ---[  83]---> Adder-cost: 672   maxlim: 3165369   bits: 23/22
c ---[  82]---> Adder-cost: 672   maxlim: 3165369   bits: 23/22
c ---[  81]---> Adder-cost: 672   maxlim: 3164089   bits: 23/22
c ---[  80]---> Adder-cost: 672   maxlim: 3164089   bits: 23/22
c ---[  79]---> Adder-cost: 632   maxlim: 3162809   bits: 23/22
c ---[  78]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  76]---> Adder-cost: 974   maxlim: 4213809   bits: 24/23
c ---[  75]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  74]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  73]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  72]---> Adder-cost: 972   maxlim: 4215089   bits: 24/23
c ---[  71]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  70]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[  69]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[  68]---> Adder-cost: 712   maxlim: 3162809   bits: 23/22
c ---[  67]---> Adder-cost: 712   maxlim: 3163449   bits: 23/22
c ---[  66]---> Adder-cost: 672   maxlim: 3164089   bits: 23/22
c ---[  65]---> Adder-cost: 672   maxlim: 3165369   bits: 23/22
c ---[  64]---> Adder-cost: 672   maxlim: 3166649   bits: 23/22
c ---[  63]---> Adder-cost: 672   maxlim: 3164089   bits: 23/22
c ---[  62]---> Adder-cost: 672   maxlim: 3163449   bits: 23/22
c ---[  61]---> Adder-cost: 672   maxlim: 3162809   bits: 23/22
c ---[  60]---> Adder-cost: 632   maxlim: 3162809   bits: 23/22
c ---[  59]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[  58]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[  57]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  56]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  55]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  54]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  53]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  52]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  51]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[  50]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  49]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  48]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  47]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  46]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  45]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  44]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  43]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  42]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  41]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  40]---> Adder-cost: 974   maxlim: 4214449   bits: 24/23
c ---[  39]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  38]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  37]---> Adder-cost: 972   maxlim: 4219569   bits: 24/23
c ---[  36]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  35]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  34]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  33]---> Adder-cost: 970   maxlim: 4213809   bits: 24/23
c ---[  32]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  31]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  30]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  29]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  28]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  27]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  26]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  25]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  24]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  23]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  22]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  21]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  20]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  19]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  18]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  17]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  16]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  15]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  14]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  12]---> Adder-cost: 974   maxlim: 4213809   bits: 24/23
c ---[  11]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[  10]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   9]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[   8]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   7]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   6]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[   5]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[   4]---> Adder-cost: 333   maxlim: 1279   bits: 12/11
c ---[   3]---> Adder-cost: 333   maxlim: 1279   bits: 12/11
c ---[   2]---> Adder-cost: 186   maxlim: 639   bits: 11/10
c ---[   1]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c ---[   0]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1414840  5055343 |  471613       0        0     nan |  0.000 % |
c |       100 | 1414840  5055343 |  518774     100      313     3.1 | 11.976 % |
c |       250 | 1414840  5055343 |  570651     250      767     3.1 | 11.976 % |
c |       475 | 1414840  5055343 |  627716     475     1528     3.2 | 11.976 % |
c |       812 | 1414840  5055343 |  690488     812     2759     3.4 | 11.976 % |
c |      1320 | 1414840  5055343 |  759537    1320     4957     3.8 | 11.976 % |
c |      2079 | 1414840  5055343 |  835491    2079     8176     3.9 | 11.976 % |
c |      3218 | 1414840  5055343 |  919040    3218    13740     4.3 | 11.976 % |
c |      4927 | 1414840  5055343 | 1010944    4927    31616     6.4 | 11.976 % |
c |      7489 | 1414840  5055343 | 1112038    7489    46098     6.2 | 11.976 % |
c |     11333 | 1414840  5055343 | 1223242   11333    79128     7.0 | 11.976 % |
c |     17099 | 1414840  5055343 | 1345566   17099   120912     7.1 | 11.976 % |
c |     25748 | 1414840  5055343 | 1480123   25748   192983     7.5 | 11.976 % |
c |     38722 | 1414840  5055343 | 1628135   38722   301120     7.8 | 11.976 % |
c |     58183 | 1414840  5055343 | 1790949   58183   641526    11.0 | 11.976 % |
c |     87375 | 1414840  5055343 | 1970044   87375  1236538    14.2 | 11.976 % |
c |    131164 | 1414840  5055343 | 2167048  131164  1877211    14.3 | 11.976 % |
c |    196850 | 1414840  5055343 | 2383753  196850  3834965    19.5 | 11.976 % |
c |    295376 | 1414840  5055343 | 2622129  295376 10074741    34.1 | 11.976 % |
c |    443165 | 1414840  5055343 | 2884342  443165 16283626    36.7 | 11.976 % |
c |    664848 | 1414840  5055343 | 3172776  664848 23906829    36.0 | 11.976 % |
#### 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.97 0.92 2/54 6647
Raw data (stat): 6647 (runsolver) R 6646 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547581942 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.0012 s]
Raw data (loadavg): 0.87 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 29021 0 0 0 929 69 0 0 25 0 1 0 547581942 121593856 27499 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29686 27499 603 41 0 29645 0
vsize: 118744
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 29418 0 0 0 1927 71 0 0 25 0 1 0 547581942 123224064 27896 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30084 27896 603 41 0 30043 0
vsize: 120336
[startup+30.002 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 29834 0 0 0 2927 72 0 0 25 0 1 0 547581942 124882944 28312 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30489 28312 603 41 0 30448 0
vsize: 121956
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 30061 0 0 0 3926 72 0 0 25 0 1 0 547581942 125829120 28539 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30720 28539 603 41 0 30679 0
vsize: 122880
[startup+50.0014 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 30303 0 0 0 4925 73 0 0 25 0 1 0 547581942 126902272 28781 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30982 28781 603 41 0 30941 0
vsize: 123928
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 30703 0 0 0 5924 74 0 0 25 0 1 0 547581942 128524288 29181 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31378 29181 603 41 0 31337 0
vsize: 125512
[startup+70.0009 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 30880 0 0 0 6923 75 0 0 25 0 1 0 547581942 129200128 29358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31543 29358 603 41 0 31502 0
vsize: 126172
[startup+80.0016 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 31087 0 0 0 7923 76 0 0 25 0 1 0 547581942 130011136 29565 4294967295 134512640 134672761 3221224544 3221223680 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31741 29565 603 41 0 31700 0
vsize: 126964
[startup+90.0013 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 31269 0 0 0 8922 77 0 0 25 0 1 0 547581942 130949120 29747 4294967295 134512640 134672761 3221224544 3221223680 134560569 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31970 29747 603 41 0 31929 0
vsize: 127880
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 31486 0 0 0 9921 77 0 0 25 0 1 0 547581942 131760128 29964 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32168 29964 603 41 0 32127 0
vsize: 128672
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 32130 0 0 0 10920 79 0 0 25 0 1 0 547581942 134316032 30608 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32792 30608 603 41 0 32751 0
vsize: 131168
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 32338 0 0 0 11920 80 0 0 25 0 1 0 547581942 135262208 30816 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33023 30816 603 41 0 32982 0
vsize: 132092
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 32770 0 0 0 12919 81 0 0 25 0 1 0 547581942 136884224 31248 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33419 31248 603 41 0 33378 0
vsize: 133676
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 32984 0 0 0 13919 81 0 0 25 0 1 0 547581942 137830400 31462 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33650 31462 603 41 0 33609 0
vsize: 134600
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 33203 0 0 0 14918 82 0 0 25 0 1 0 547581942 138641408 31681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33848 31681 603 41 0 33807 0
vsize: 135392
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 33317 0 0 0 15918 82 0 0 25 0 1 0 547581942 139046912 31795 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33947 31795 603 41 0 33906 0
vsize: 135788
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 33472 0 0 0 16918 82 0 0 25 0 1 0 547581942 140247040 31950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34240 31950 603 41 0 34199 0
vsize: 136960
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 33621 0 0 0 17917 83 0 0 25 0 1 0 547581942 140787712 32099 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34372 32099 603 41 0 34331 0
vsize: 137488
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 33740 0 0 0 18917 83 0 0 25 0 1 0 547581942 141328384 32218 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34504 32218 603 41 0 34463 0
vsize: 138016
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 33837 0 0 0 19916 84 0 0 25 0 1 0 547581942 141598720 32315 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34570 32315 603 41 0 34529 0
vsize: 138280
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 33957 0 0 0 20916 84 0 0 25 0 1 0 547581942 142139392 32435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34702 32435 603 41 0 34661 0
vsize: 138808
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 34189 0 0 0 21915 85 0 0 25 0 1 0 547581942 143085568 32667 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34933 32667 603 41 0 34892 0
vsize: 139732
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 34775 0 0 0 22914 87 0 0 25 0 1 0 547581942 145371136 33253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35491 33253 603 41 0 35450 0
vsize: 141964
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 35197 0 0 0 23913 88 0 0 25 0 1 0 547581942 147124224 33675 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35919 33675 603 41 0 35878 0
vsize: 143676
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 35517 0 0 0 24913 88 0 0 25 0 1 0 547581942 148475904 33995 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36249 33995 603 41 0 36208 0
vsize: 144996
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 35787 0 0 0 25913 89 0 0 25 0 1 0 547581942 149569536 34265 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36516 34265 603 41 0 36475 0
vsize: 146064
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 36029 0 0 0 26912 91 0 0 25 0 1 0 547581942 150519808 34507 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36748 34507 603 41 0 36707 0
vsize: 146992
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 36348 0 0 0 27911 92 0 0 25 0 1 0 547581942 151732224 34826 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37044 34826 603 41 0 37003 0
vsize: 148176
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 36596 0 0 0 28909 93 0 0 25 0 1 0 547581942 152809472 35074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37307 35074 603 41 0 37266 0
vsize: 149228
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 37248 0 0 0 29908 94 0 0 25 0 1 0 547581942 155369472 35726 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35726 603 41 0 37891 0
vsize: 151728
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 37959 0 0 0 30906 97 0 0 25 0 1 0 547581942 158302208 36437 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38648 36437 603 41 0 38607 0
vsize: 154592
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 38517 0 0 0 31904 98 0 0 25 0 1 0 547581942 160452608 36995 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39173 36995 603 41 0 39132 0
vsize: 156692
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 38943 0 0 0 32904 99 0 0 25 0 1 0 547581942 162189312 37421 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39597 37421 603 41 0 39556 0
vsize: 158388
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 39319 0 0 0 33903 100 0 0 25 0 1 0 547581942 163794944 37797 4294967295 134512640 134672761 3221224544 3221223728 134559609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39989 37797 603 41 0 39948 0
vsize: 159956
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 39677 0 0 0 34902 101 0 0 25 0 1 0 547581942 165314560 38155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40360 38155 603 41 0 40319 0
vsize: 161440
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 39989 0 0 0 35902 102 0 0 25 0 1 0 547581942 166547456 38467 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40661 38467 603 41 0 40620 0
vsize: 162644
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 40292 0 0 0 36901 102 0 0 25 0 1 0 547581942 167755776 38770 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40956 38770 603 41 0 40915 0
vsize: 163824
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 40584 0 0 0 37900 103 0 0 25 0 1 0 547581942 170012672 39062 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41507 39062 603 41 0 41466 0
vsize: 166028
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 40867 0 0 0 38899 104 0 0 25 0 1 0 547581942 171245568 39345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41808 39345 603 41 0 41767 0
vsize: 167232
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 41149 0 0 0 39899 105 0 0 25 0 1 0 547581942 172314624 39627 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42069 39627 603 41 0 42028 0
vsize: 168276
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 41415 0 0 0 40898 106 0 0 25 0 1 0 547581942 173387776 39893 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42331 39893 603 41 0 42290 0
vsize: 169324
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 41676 0 0 0 41897 107 0 0 25 0 1 0 547581942 174452736 40154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42591 40154 603 41 0 42550 0
vsize: 170364
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 41903 0 0 0 42897 108 0 0 25 0 1 0 547581942 175407104 40381 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42824 40381 603 41 0 42783 0
vsize: 171296
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 42113 0 0 0 43897 108 0 0 25 0 1 0 547581942 176214016 40591 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43021 40591 603 41 0 42980 0
vsize: 172084
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 42324 0 0 0 44896 109 0 0 25 0 1 0 547581942 177233920 40802 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43270 40802 603 41 0 43229 0
vsize: 173080
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 42524 0 0 0 45895 110 0 0 25 0 1 0 547581942 178057216 41002 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43471 41002 603 41 0 43430 0
vsize: 173884
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 42712 0 0 0 46895 111 0 0 25 0 1 0 547581942 178741248 41190 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43638 41190 603 41 0 43597 0
vsize: 174552
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 42907 0 0 0 47895 111 0 0 25 0 1 0 547581942 179548160 41385 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43835 41385 603 41 0 43794 0
vsize: 175340
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 43112 0 0 0 48894 112 0 0 25 0 1 0 547581942 180494336 41590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44066 41590 603 41 0 44025 0
vsize: 176264
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 43301 0 0 0 49894 113 0 0 25 0 1 0 547581942 181166080 41779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44230 41779 603 41 0 44189 0
vsize: 176920
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 43589 0 0 0 50892 113 0 0 25 0 1 0 547581942 182374400 42067 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44525 42067 603 41 0 44484 0
vsize: 178100
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 44513 0 0 0 51890 116 0 0 25 0 1 0 547581942 186134528 42991 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45443 42991 603 41 0 45402 0
vsize: 181772
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 45064 0 0 0 52889 117 0 0 25 0 1 0 547581942 188280832 43542 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45967 43542 603 41 0 45926 0
vsize: 183868
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 45602 0 0 0 53888 119 0 0 25 0 1 0 547581942 190443520 44080 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46495 44080 603 41 0 46454 0
vsize: 185980
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 46136 0 0 0 54887 120 0 0 25 0 1 0 547581942 192602112 44614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47022 44614 603 41 0 46981 0
vsize: 188088
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 46734 0 0 0 55885 122 0 0 25 0 1 0 547581942 195026944 45212 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47614 45212 603 41 0 47573 0
vsize: 190456
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 47120 0 0 0 56883 124 0 0 25 0 1 0 547581942 196648960 45598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48010 45598 603 41 0 47969 0
vsize: 192040
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 47458 0 0 0 57883 124 0 0 25 0 1 0 547581942 197865472 45936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48307 45936 603 41 0 48266 0
vsize: 193228
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 47797 0 0 0 58882 126 0 0 25 0 1 0 547581942 199446528 46275 4294967295 134512640 134672761 3221224544 3221223728 134559569 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48693 46275 603 41 0 48652 0
vsize: 194772
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 48073 0 0 0 59881 127 0 0 25 0 1 0 547581942 200597504 46551 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48974 46551 603 41 0 48933 0
vsize: 195896
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 48362 0 0 0 60880 128 0 0 25 0 1 0 547581942 201715712 46840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49247 46840 603 41 0 49206 0
vsize: 196988
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 48567 0 0 0 61879 129 0 0 25 0 1 0 547581942 202731520 47045 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49495 47045 603 41 0 49454 0
vsize: 197980
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 48763 0 0 0 62879 129 0 0 25 0 1 0 547581942 203403264 47241 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49659 47241 603 41 0 49618 0
vsize: 198636
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 48950 0 0 0 63878 130 0 0 25 0 1 0 547581942 204275712 47428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49872 47428 603 41 0 49831 0
vsize: 199488
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 49123 0 0 0 64878 130 0 0 25 0 1 0 547581942 204951552 47601 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50037 47601 603 41 0 49996 0
vsize: 200148
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 49309 0 0 0 65877 131 0 0 25 0 1 0 547581942 205623296 47787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50201 47787 603 41 0 50160 0
vsize: 200804
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 49498 0 0 0 66877 132 0 0 25 0 1 0 547581942 206393344 47976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50389 47976 603 41 0 50348 0
vsize: 201556
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 49653 0 0 0 67877 132 0 0 25 0 1 0 547581942 207065088 48131 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50553 48131 603 41 0 50512 0
vsize: 202212
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 49823 0 0 0 68877 133 0 0 25 0 1 0 547581942 207732736 48301 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50716 48301 603 41 0 50675 0
vsize: 202864
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 50005 0 0 0 69876 133 0 0 25 0 1 0 547581942 208453632 48483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50892 48483 603 41 0 50851 0
vsize: 203568
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 50146 0 0 0 70876 134 0 0 25 0 1 0 547581942 209137664 48624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51059 48624 603 41 0 51018 0
vsize: 204236
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 50292 0 0 0 71875 135 0 0 25 0 1 0 547581942 209690624 48770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51194 48770 603 41 0 51153 0
vsize: 204776
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 50459 0 0 0 72875 135 0 0 25 0 1 0 547581942 210370560 48937 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51360 48937 603 41 0 51319 0
vsize: 205440
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 50635 0 0 0 73875 135 0 0 25 0 1 0 547581942 211070976 49113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51531 49113 603 41 0 51490 0
vsize: 206124
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 50806 0 0 0 74875 136 0 0 25 0 1 0 547581942 211738624 49284 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51694 49284 603 41 0 51653 0
vsize: 206776
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 50969 0 0 0 75875 136 0 0 25 0 1 0 547581942 212414464 49447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51859 49447 603 41 0 51818 0
vsize: 207436
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 51090 0 0 0 76874 137 0 0 25 0 1 0 547581942 212955136 49568 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51991 49568 603 41 0 51950 0
vsize: 207964
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 51295 0 0 0 77874 137 0 0 25 0 1 0 547581942 213770240 49773 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52190 49773 603 41 0 52149 0
vsize: 208760
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 51519 0 0 0 78873 138 0 0 25 0 1 0 547581942 214708224 49997 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52419 49997 603 41 0 52378 0
vsize: 209676
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 51793 0 0 0 79872 139 0 0 25 0 1 0 547581942 215818240 50271 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52690 50271 603 41 0 52649 0
vsize: 210760
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 51960 0 0 0 80872 140 0 0 25 0 1 0 547581942 216498176 50438 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52856 50438 603 41 0 52815 0
vsize: 211424
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 52138 0 0 0 81872 140 0 0 25 0 1 0 547581942 217174016 50616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53021 50616 603 41 0 52980 0
vsize: 212084
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 52358 0 0 0 82871 141 0 0 25 0 1 0 547581942 218116096 50836 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53251 50836 603 41 0 53210 0
vsize: 213004
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 52592 0 0 0 83870 142 0 0 25 0 1 0 547581942 219066368 51070 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53483 51070 603 41 0 53442 0
vsize: 213932
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 52858 0 0 0 84870 143 0 0 25 0 1 0 547581942 220164096 51336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53751 51336 603 41 0 53710 0
vsize: 215004
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 53153 0 0 0 85869 144 0 0 25 0 1 0 547581942 221380608 51631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54048 51631 603 41 0 54007 0
vsize: 216192
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 53510 0 0 0 86867 145 0 0 25 0 1 0 547581942 222801920 51988 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54395 51988 603 41 0 54354 0
vsize: 217580
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 54119 0 0 0 87866 147 0 0 25 0 1 0 547581942 225222656 52597 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54986 52597 603 41 0 54945 0
vsize: 219944
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 54920 0 0 0 88864 150 0 0 25 0 1 0 547581942 228466688 53398 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55778 53398 603 41 0 55737 0
vsize: 223112
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 55489 0 0 0 89862 152 0 0 25 0 1 0 547581942 230887424 53967 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56369 53967 603 41 0 56328 0
vsize: 225476
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 55677 0 0 0 90862 152 0 0 25 0 1 0 547581942 231571456 54155 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56536 54155 603 41 0 56495 0
vsize: 226144
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 55785 0 0 0 91861 153 0 0 25 0 1 0 547581942 234074112 54263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57147 54263 603 41 0 57106 0
vsize: 228588
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 56027 0 0 0 92861 153 0 0 25 0 1 0 547581942 235151360 54505 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57410 54505 603 41 0 57369 0
vsize: 229640
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 56671 0 0 0 93859 155 0 0 25 0 1 0 547581942 237707264 55149 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58034 55149 603 41 0 57993 0
vsize: 232136
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 57042 0 0 0 94858 156 0 0 25 0 1 0 547581942 239185920 55520 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58395 55520 603 41 0 58354 0
vsize: 233580
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 57363 0 0 0 95858 157 0 0 25 0 1 0 547581942 240533504 55841 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58724 55841 603 41 0 58683 0
vsize: 234896
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 57472 0 0 0 96857 157 0 0 25 0 1 0 547581942 240939008 55950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58823 55950 603 41 0 58782 0
vsize: 235292
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 57601 0 0 0 97857 158 0 0 25 0 1 0 547581942 241475584 56079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58954 56079 603 41 0 58913 0
vsize: 235816
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 57728 0 0 0 98857 158 0 0 25 0 1 0 547581942 241876992 56206 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59052 56206 603 41 0 59011 0
vsize: 236208
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 57870 0 0 0 99857 158 0 0 25 0 1 0 547581942 242413568 56348 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59183 56348 603 41 0 59142 0
vsize: 236732
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 57962 0 0 0 100857 159 0 0 25 0 1 0 547581942 242814976 56440 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59281 56440 603 41 0 59240 0
vsize: 237124
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 58044 0 0 0 101857 159 0 0 25 0 1 0 547581942 243085312 56522 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59347 56522 603 41 0 59306 0
vsize: 237388
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 58174 0 0 0 102856 160 0 0 25 0 1 0 547581942 243625984 56652 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59479 56652 603 41 0 59438 0
vsize: 237916
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 58371 0 0 0 103856 160 0 0 25 0 1 0 547581942 244432896 56849 4294967295 134512640 134672761 3221224544 3221223696 134565094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59676 56849 603 41 0 59635 0
vsize: 238704
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 58785 0 0 0 104855 161 0 0 25 0 1 0 547581942 246046720 57263 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60070 57263 603 41 0 60029 0
vsize: 240280
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 59656 0 0 0 105852 165 0 0 25 0 1 0 547581942 249532416 58134 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60921 58135 603 41 0 60880 0
vsize: 243684
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 60103 0 0 0 106850 167 0 0 25 0 1 0 547581942 251432960 58581 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61385 58581 603 41 0 61344 0
vsize: 245540
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 60404 0 0 0 107849 168 0 0 25 0 1 0 547581942 252649472 58882 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61682 58882 603 41 0 61641 0
vsize: 246728
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 60834 0 0 0 108849 169 0 0 25 0 1 0 547581942 254283776 59312 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62081 59312 603 41 0 62040 0
vsize: 248324
[startup+1100.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 61151 0 0 0 109858 171 0 0 25 0 1 0 547581942 255627264 59629 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62409 59629 603 41 0 62368 0
vsize: 249636
[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 61445 0 0 0 110857 172 0 0 25 0 1 0 547581942 256835584 59923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62704 59923 603 41 0 62663 0
vsize: 250816
[startup+1120.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 61866 0 0 0 111855 173 0 0 25 0 1 0 547581942 258445312 60344 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63097 60344 603 41 0 63056 0
vsize: 252388
[startup+1130.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 62252 0 0 0 112854 175 0 0 25 0 1 0 547581942 260063232 60730 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63492 60730 603 41 0 63451 0
vsize: 253968
[startup+1140.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 62560 0 0 0 113853 176 0 0 25 0 1 0 547581942 261267456 61038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63786 61038 603 41 0 63745 0
vsize: 255144
[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 62933 0 0 0 114852 178 0 0 25 0 1 0 547581942 262750208 61411 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64148 61411 603 41 0 64107 0
vsize: 256592
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 63468 0 0 0 115851 179 0 0 25 0 1 0 547581942 265043968 61946 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64708 61946 603 41 0 64667 0
vsize: 258832
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 63912 0 0 0 116849 181 0 0 25 0 1 0 547581942 266797056 62390 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65136 62390 603 41 0 65095 0
vsize: 260544
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 64306 0 0 0 117847 183 0 0 25 0 1 0 547581942 268410880 62784 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65530 62784 603 41 0 65489 0
vsize: 262120
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 64606 0 0 0 118848 184 0 0 25 0 1 0 547581942 269611008 63084 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65823 63084 603 41 0 65782 0
vsize: 263292
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6647
Raw data (stat): 6647 (minisat+) R 6646 26298 26297 0 -1 0 64864 0 0 0 119847 185 0 0 25 0 1 0 547581942 270671872 63342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66082 63342 603 41 0 66041 0
vsize: 264328
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.29 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 6647
Raw data (stat): 6647 (minisat+) Z 6646 26298 26297 0 -1 12 64866 0 0 0 119847 197 0 0 25 0 1 0 547581942 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.29
CPU time (s): 1200.45
CPU user time (s): 1198.47
CPU system time (s): 1.9767
CPU usage (%): 100.013
Max. virtual memory (Kb): 264328
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####