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/submitted/een/normalized-air04.opb
MD5SUM	80cb01878488e5fe06c52c88c5a85bdd
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.9507
Number of variables	8904
Total number of constraints	1646
Number of constraints which are clauses	825
Number of constraints which are cardinality constraints (but not clauses)	821
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	368
Trace number 7134

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        816104 kB
Buffers:         41632 kB
Cached:         151828 kB
SwapCached:          0 kB
Active:         116720 kB
Inactive:        79864 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        815852 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           7204 kB
Slab:            16192 kB
Committed_AS:    92816 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:50:46 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 5184 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================
c   -- Clauses(.)/Splits(s): ..................................................
c ---[1640]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1638]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1636]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1634]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1632]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1630]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1628]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1626]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1624]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1621]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1618]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1616]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1614]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1612]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1610]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1606]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1604]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1603]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1601]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1599]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[1597]---> Adder-cost: 12   maxlim: 13   bits: 4/4
c ---[1592]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1590]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1588]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1586]---> Adder-cost: 20   maxlim: 15   bits: 5/4
c ---[1584]---> Adder-cost: 22   maxlim: 15   bits: 5/4
c ---[1582]---> Adder-cost: 22   maxlim: 16   bits: 5/5
c ---[1580]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[1578]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[1576]---> Adder-cost: 0   maxlim: 16   bits: 5/5
c ---[1574]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1572]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[1570]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1568]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1566]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1564]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1562]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1560]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1558]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[1556]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1554]---> Adder-cost: 0   maxlim: 19   bits: 5/5
c ---[1552]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1550]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1548]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1546]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1544]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[1541]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1539]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[1537]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1536]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1534]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1532]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1530]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1528]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[1526]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1524]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[1522]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1520]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1518]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1514]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1512]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1510]---> Adder-cost: 42   maxlim: 24   bits: 5/5
c ---[1508]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1503]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1501]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1499]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1497]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1495]---> Adder-cost: 38   maxlim: 25   bits: 5/5
c ---[1493]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1491]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1490]---> Adder-cost: 44   maxlim: 25   bits: 5/5
c ---[1488]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1485]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1483]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1481]---> Adder-cost: 48   maxlim: 27   bits: 5/5
c ---[1479]---> Adder-cost: 32   maxlim: 27   bits: 5/5
c ---[1478]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1476]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1474]---> Adder-cost: 34   maxlim: 27   bits: 5/5
c ---[1472]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1470]---> Adder-cost: 44   maxlim: 27   bits: 5/5
c ---[1467]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[1465]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[1463]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[1461]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1459]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1457]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[1455]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[1453]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[1452]---> Adder-cost: 46   maxlim: 28   bits: 5/5
c ---[1448]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1446]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[1442]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[1440]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1438]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1436]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1434]---> Adder-cost: 62   maxlim: 30   bits: 6/5
c ---[1432]---> Adder-cost: 62   maxlim: 30   bits: 6/5
c ---[1430]---> Adder-cost: 60   maxlim: 30   bits: 6/5
c ---[1428]---> Adder-cost: 62   maxlim: 30   bits: 6/5
c ---[1427]---> Adder-cost: 56   maxlim: 30   bits: 6/5
c ---[1425]---> Adder-cost: 62   maxlim: 30   bits: 6/5
c ---[1422]---> Adder-cost: 42   maxlim: 31   bits: 6/5
c ---[1420]---> Adder-cost: 58   maxlim: 31   bits: 6/5
c ---[1418]---> Adder-cost: 58   maxlim: 31   bits: 6/5
c ---[1416]---> Adder-cost: 58   maxlim: 31   bits: 6/5
c ---[1414]---> Adder-cost: 50   maxlim: 31   bits: 6/5
c ---[1412]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1410]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[1408]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[1406]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1402]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1400]---> Adder-cost: 52   maxlim: 32   bits: 6/6
c ---[1398]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1396]---> Adder-cost: 56   maxlim: 33   bits: 6/6
c ---[1394]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1392]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[1390]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1388]---> Adder-cost: 52   maxlim: 33   bits: 6/6
c ---[1386]---> Adder-cost: 46   maxlim: 34   bits: 6/6
c ---[1384]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[1382]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[1380]---> Adder-cost: 58   maxlim: 34   bits: 6/6
c ---[1378]---> Adder-cost: 62   maxlim: 34   bits: 6/6
c ---[1376]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[1374]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[1372]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1370]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[1368]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1366]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1364]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[1362]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1360]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1358]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1356]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1354]---> Adder-cost: 64   maxlim: 35   bits: 6/6
c ---[1352]---> Adder-cost: 54   maxlim: 35   bits: 6/6
c ---[1350]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[1348]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[1346]---> Adder-cost: 58   maxlim: 36   bits: 6/6
c ---[1344]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[1343]---> Adder-cost: 58   maxlim: 36   bits: 6/6
c ---[1339]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[1337]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[1334]---> Adder-cost: 52   maxlim: 37   bits: 6/6
c ---[1332]---> Adder-cost: 50   maxlim: 37   bits: 6/6
c ---[1330]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1327]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1325]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1324]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1323]---> Adder-cost: 60   maxlim: 37   bits: 6/6
c ---[1320]---> Adder-cost: 74   maxlim: 38   bits: 6/6
c ---[1318]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[1316]---> Adder-cost: 72   maxlim: 38   bits: 6/6
c ---[1314]---> Adder-cost: 0   maxlim: 38   bits: 6/6
c ---[1312]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[1310]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[1308]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[1306]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1304]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1302]---> Adder-cost: 74   maxlim: 39   bits: 6/6
c ---[1300]---> Adder-cost: 66   maxlim: 39   bits: 6/6
c ---[1298]---> Adder-cost: 56   maxlim: 39   bits: 6/6
c ---[1296]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1294]---> Adder-cost: 46   maxlim: 39   bits: 6/6
c ---[1292]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[1290]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[1288]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[1286]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1284]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[1283]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[1278]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[1277]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[1276]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[1272]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[1270]---> Adder-cost: 74   maxlim: 40   bits: 6/6
c ---[1268]---> Adder-cost: 68   maxlim: 40   bits: 6/6
c ---[1265]---> Adder-cost: 74   maxlim: 41   bits: 6/6
c ---[1263]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1262]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[1261]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1258]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1256]---> Adder-cost: 0   maxlim: 41   bits: 6/6
c ---[1254]---> Adder-cost: 80   maxlim: 42   bits: 6/6
c ---[1252]---> Adder-cost: 70   maxlim: 42   bits: 6/6
c ---[1250]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[1248]---> Adder-cost: 64   maxlim: 42   bits: 6/6
c ---[1246]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[1244]---> Adder-cost: 80   maxlim: 42   bits: 6/6
c ---[1242]---> Adder-cost: 58   maxlim: 43   bits: 6/6
c ---[1240]---> Adder-cost: 70   maxlim: 43   bits: 6/6
c ---[1238]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[1236]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[1234]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[1232]---> Adder-cost: 58   maxlim: 44   bits: 6/6
c ---[1230]---> Adder-cost: 78   maxlim: 44   bits: 6/6
c ---[1228]---> Adder-cost: 84   maxlim: 44   bits: 6/6
c ---[1226]---> Adder-cost: 80   maxlim: 44   bits: 6/6
c ---[1224]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[1222]---> Adder-cost: 80   maxlim: 44   bits: 6/6
c ---[1220]---> Adder-cost: 76   maxlim: 45   bits: 6/6
c ---[1218]---> Adder-cost: 44   maxlim: 45   bits: 6/6
c ---[1216]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[1214]---> Adder-cost: 76   maxlim: 45   bits: 6/6
c ---[1212]---> Adder-cost: 78   maxlim: 45   bits: 6/6
c ---[1210]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[1208]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[1206]---> Adder-cost: 58   maxlim: 45   bits: 6/6
c ---[1205]---> Adder-cost: 90   maxlim: 46   bits: 6/6
c ---[1203]---> Adder-cost: 88   maxlim: 46   bits: 6/6
c ---[1201]---> Adder-cost: 54   maxlim: 46   bits: 6/6
c ---[1199]---> Adder-cost: 92   maxlim: 46   bits: 6/6
c ---[1197]---> Adder-cost: 76   maxlim: 46   bits: 6/6
c ---[1195]---> Adder-cost: 76   maxlim: 46   bits: 6/6
c ---[1193]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[1191]---> Adder-cost: 74   maxlim: 46   bits: 6/6
c ---[1189]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[1186]---> Adder-cost: 76   maxlim: 47   bits: 6/6
c ---[1184]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1182]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1178]---> Adder-cost: 60   maxlim: 47   bits: 6/6
c ---[1176]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[1174]---> Adder-cost: 84   maxlim: 48   bits: 6/6
c ---[1172]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[1170]---> Adder-cost: 86   maxlim: 48   bits: 6/6
c ---[1168]---> Adder-cost: 78   maxlim: 48   bits: 6/6
c ---[1166]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1164]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[1162]---> Adder-cost: 84   maxlim: 49   bits: 6/6
c ---[1160]---> Adder-cost: 50   maxlim: 49   bits: 6/6
c ---[1158]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[1156]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[1154]---> Adder-cost: 72   maxlim: 49   bits: 6/6
c ---[1152]---> Adder-cost: 88   maxlim: 49   bits: 6/6
c ---[1150]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[1148]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[1146]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[1144]---> Adder-cost: 96   maxlim: 50   bits: 6/6
c ---[1142]---> Adder-cost: 98   maxlim: 50   bits: 6/6
c ---[1140]---> Adder-cost: 98   maxlim: 50   bits: 6/6
c ---[1138]---> Adder-cost: 94   maxlim: 50   bits: 6/6
c ---[1136]---> Adder-cost: 98   maxlim: 50   bits: 6/6
c ---[1132]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1130]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1128]---> Adder-cost: 96   maxlim: 51   bits: 6/6
c ---[1126]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1124]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1122]---> Adder-cost: 96   maxlim: 51   bits: 6/6
c ---[1120]---> Adder-cost: 90   maxlim: 52   bits: 6/6
c ---[1118]---> Adder-cost: 100   maxlim: 52   bits: 6/6
c ---[1116]---> Adder-cost: 76   maxlim: 52   bits: 6/6
c ---[1114]---> Adder-cost: 100   maxlim: 52   bits: 6/6
c ---[1112]---> Adder-cost: 88   maxlim: 52   bits: 6/6
c ---[1110]---> Adder-cost: 94   maxlim: 52   bits: 6/6
c ---[1108]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[1105]---> Adder-cost: 98   maxlim: 53   bits: 6/6
c ---[1104]---> Adder-cost: 86   maxlim: 53   bits: 6/6
c ---[1101]---> Adder-cost: 98   maxlim: 53   bits: 6/6
c ---[1099]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[1097]---> Adder-cost: 56   maxlim: 53   bits: 6/6
c ---[1095]---> Adder-cost: 98   maxlim: 53   bits: 6/6
c ---[1093]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[1090]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[1089]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[1088]---> Adder-cost: 0   maxlim: 53   bits: 6/6
c ---[1085]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1083]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[1081]---> Adder-cost: 98   maxlim: 54   bits: 6/6
c ---[1079]---> Adder-cost: 104   maxlim: 54   bits: 6/6
c ---[1075]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[1074]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[1071]---> Adder-cost: 76   maxlim: 54   bits: 6/6
c ---[1069]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[1067]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[1065]---> Adder-cost: 102   maxlim: 54   bits: 6/6
c ---[1064]---> Adder-cost: 76   maxlim: 54   bits: 6/6
c ---[1063]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[1060]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[1058]---> Adder-cost: 100   maxlim: 55   bits: 6/6
c ---[1056]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1054]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1050]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1048]---> Adder-cost: 92   maxlim: 55   bits: 6/6
c ---[1046]---> Adder-cost: 94   maxlim: 55   bits: 6/6
c ---[1045]---> Adder-cost: 96   maxlim: 56   bits: 6/6
c ---[1043]---> Adder-cost: 98   maxlim: 56   bits: 6/6
c ---[1041]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[1039]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[1036]---> Adder-cost: 96   maxlim: 56   bits: 6/6
c ---[1034]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[1032]---> Adder-cost: 104   maxlim: 56   bits: 6/6
c ---[1029]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[1027]---> Adder-cost: 100   maxlim: 57   bits: 6/6
c ---[1026]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[1024]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[1022]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[1016]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[1014]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[1013]---> Adder-cost: 82   maxlim: 57   bits: 6/6
c ---[1011]---> Adder-cost: 66   maxlim: 57   bits: 6/6
c ---[1010]---> Adder-cost: 72   maxlim: 57   bits: 6/6
c ---[1008]---> Adder-cost: 108   maxlim: 58   bits: 6/6
c ---[1006]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[1004]---> Adder-cost: 108   maxlim: 58   bits: 6/6
c ---[1002]---> Adder-cost: 98   maxlim: 58   bits: 6/6
c ---[1000]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[ 998]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[ 996]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 994]---> Adder-cost: 82   maxlim: 59   bits: 6/6
c ---[ 992]---> Adder-cost: 108   maxlim: 59   bits: 6/6
c ---[ 990]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 988]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 986]---> Adder-cost: 80   maxlim: 60   bits: 6/6
c ---[ 984]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 982]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 980]---> Adder-cost: 110   maxlim: 60   bits: 6/6
c ---[ 978]---> Adder-cost: 110   maxlim: 60   bits: 6/6
c ---[ 976]---> Adder-cost: 114   maxlim: 60   bits: 6/6
c ---[ 974]---> Adder-cost: 108   maxlim: 60   bits: 6/6
c ---[ 972]---> Adder-cost: 84   maxlim: 61   bits: 6/6
c ---[ 970]---> Adder-cost: 54   maxlim: 61   bits: 6/6
c ---[ 969]---> Adder-cost: 110   maxlim: 61   bits: 6/6
c ---[ 967]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 965]---> Adder-cost: 110   maxlim: 61   bits: 6/6
c ---[ 962]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 959]---> Adder-cost: 108   maxlim: 62   bits: 7/6
c ---[ 957]---> Adder-cost: 114   maxlim: 62   bits: 7/6
c ---[ 956]---> Adder-cost: 124   maxlim: 62   bits: 7/6
c ---[ 954]---> Adder-cost: 100   maxlim: 63   bits: 7/6
c ---[ 952]---> Adder-cost: 118   maxlim: 63   bits: 7/6
c ---[ 950]---> Adder-cost: 122   maxlim: 63   bits: 7/6
c ---[ 948]---> Adder-cost: 114   maxlim: 63   bits: 7/6
c ---[ 946]---> Adder-cost: 124   maxlim: 63   bits: 7/6
c ---[ 944]---> Adder-cost: 126   maxlim: 63   bits: 7/6
c ---[ 942]---> Adder-cost: 0   maxlim: 63   bits: 7/6
c ---[ 940]---> Adder-cost: 122   maxlim: 63   bits: 7/6
c ---[ 938]---> Adder-cost: 110   maxlim: 63   bits: 7/6
c ---[ 936]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 934]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 932]---> Adder-cost: 120   maxlim: 64   bits: 7/7
c ---[ 930]---> Adder-cost: 128   maxlim: 64   bits: 7/7
c ---[ 928]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[ 926]---> Adder-cost: 84   maxlim: 65   bits: 7/7
c ---[ 925]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[ 923]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[ 920]---> Adder-cost: 0   maxlim: 65   bits: 7/7
c ---[ 918]---> Adder-cost: 132   maxlim: 66   bits: 7/7
c ---[ 916]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 914]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 910]---> Adder-cost: 132   maxlim: 66   bits: 7/7
c ---[ 908]---> Adder-cost: 132   maxlim: 66   bits: 7/7
c ---[ 906]---> Adder-cost: 78   maxlim: 66   bits: 7/7
c ---[ 904]---> Adder-cost: 106   maxlim: 67   bits: 7/7
c ---[ 902]---> Adder-cost: 112   maxlim: 67   bits: 7/7
c ---[ 900]---> Adder-cost: 114   maxlim: 67   bits: 7/7
c ---[ 898]---> Adder-cost: 112   maxlim: 67   bits: 7/7
c ---[ 896]---> Adder-cost: 122   maxlim: 67   bits: 7/7
c ---[ 893]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 892]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[ 890]---> Adder-cost: 118   maxlim: 67   bits: 7/7
c ---[ 888]---> Adder-cost: 0   maxlim: 67   bits: 7/7
c ---[ 886]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[ 884]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 881]---> Adder-cost: 134   maxlim: 68   bits: 7/7
c ---[ 879]---> Adder-cost: 134   maxlim: 68   bits: 7/7
c ---[ 878]---> Adder-cost: 0   maxlim: 68   bits: 7/7
c ---[ 876]---> Adder-cost: 130   maxlim: 68   bits: 7/7
c ---[ 874]---> Adder-cost: 134   maxlim: 68   bits: 7/7
c ---[ 872]---> Adder-cost: 124   maxlim: 68   bits: 7/7
c ---[ 870]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[ 869]---> Adder-cost: 130   maxlim: 68   bits: 7/7
c ---[ 867]---> Adder-cost: 100   maxlim: 68   bits: 7/7
c ---[ 865]---> Adder-cost: 132   maxlim: 68   bits: 7/7
c ---[ 862]---> Adder-cost: 130   maxlim: 69   bits: 7/7
c ---[ 860]---> Adder-cost: 116   maxlim: 69   bits: 7/7
c ---[ 858]---> Adder-cost: 132   maxlim: 69   bits: 7/7
c ---[ 856]---> Adder-cost: 128   maxlim: 69   bits: 7/7
c ---[ 854]---> Adder-cost: 124   maxlim: 69   bits: 7/7
c ---[ 852]---> Adder-cost: 136   maxlim: 70   bits: 7/7
c ---[ 850]---> Adder-cost: 138   maxlim: 70   bits: 7/7
c ---[ 848]---> Adder-cost: 102   maxlim: 70   bits: 7/7
c ---[ 846]---> Adder-cost: 94   maxlim: 70   bits: 7/7
c ---[ 844]---> Adder-cost: 138   maxlim: 71   bits: 7/7
c ---[ 842]---> Adder-cost: 130   maxlim: 71   bits: 7/7
c ---[ 840]---> Adder-cost: 116   maxlim: 71   bits: 7/7
c ---[ 838]---> Adder-cost: 100   maxlim: 71   bits: 7/7
c ---[ 836]---> Adder-cost: 106   maxlim: 71   bits: 7/7
c ---[ 834]---> Adder-cost: 118   maxlim: 72   bits: 7/7
c ---[ 832]---> Adder-cost: 142   maxlim: 72   bits: 7/7
c ---[ 830]---> Adder-cost: 142   maxlim: 72   bits: 7/7
c ---[ 828]---> Adder-cost: 70   maxlim: 72   bits: 7/7
c ---[ 826]---> Adder-cost: 134   maxlim: 72   bits: 7/7
c ---[ 824]---> Adder-cost: 104   maxlim: 72   bits: 7/7
c ---[ 822]---> Adder-cost: 136   maxlim: 73   bits: 7/7
c ---[ 820]---> Adder-cost: 138   maxlim: 73   bits: 7/7
c ---[ 818]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[ 816]---> Adder-cost: 132   maxlim: 73   bits: 7/7
c ---[ 814]---> Adder-cost: 132   maxlim: 73   bits: 7/7
c ---[ 812]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 810]---> Adder-cost: 124   maxlim: 73   bits: 7/7
c ---[ 808]---> Adder-cost: 138   maxlim: 73   bits: 7/7
c ---[ 806]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[ 804]---> Adder-cost: 136   maxlim: 73   bits: 7/7
c ---[ 802]---> Adder-cost: 128   maxlim: 73   bits: 7/7
c ---[ 800]---> Adder-cost: 138   maxlim: 73   bits: 7/7
c ---[ 798]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[ 796]---> Adder-cost: 106   maxlim: 74   bits: 7/7
c ---[ 794]---> Adder-cost: 142   maxlim: 74   bits: 7/7
c ---[ 792]---> Adder-cost: 144   maxlim: 74   bits: 7/7
c ---[ 790]---> Adder-cost: 144   maxlim: 74   bits: 7/7
c ---[ 788]---> Adder-cost: 110   maxlim: 74   bits: 7/7
c ---[ 786]---> Adder-cost: 142   maxlim: 74   bits: 7/7
c ---[ 784]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[ 780]---> Adder-cost: 126   maxlim: 74   bits: 7/7
c ---[ 778]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 776]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 774]---> Adder-cost: 138   maxlim: 75   bits: 7/7
c ---[ 772]---> Adder-cost: 134   maxlim: 75   bits: 7/7
c ---[ 770]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 768]---> Adder-cost: 142   maxlim: 75   bits: 7/7
c ---[ 766]---> Adder-cost: 140   maxlim: 75   bits: 7/7
c ---[ 764]---> Adder-cost: 138   maxlim: 75   bits: 7/7
c ---[ 762]---> Adder-cost: 114   maxlim: 76   bits: 7/7
c ---[ 760]---> Adder-cost: 132   maxlim: 76   bits: 7/7
c ---[ 758]---> Adder-cost: 50   maxlim: 76   bits: 7/7
c ---[ 756]---> Adder-cost: 146   maxlim: 76   bits: 7/7
c ---[ 754]---> Adder-cost: 112   maxlim: 76   bits: 7/7
c ---[ 750]---> Adder-cost: 146   maxlim: 77   bits: 7/7
c ---[ 748]---> Adder-cost: 138   maxlim: 77   bits: 7/7
c ---[ 746]---> Adder-cost: 144   maxlim: 77   bits: 7/7
c ---[ 744]---> Adder-cost: 144   maxlim: 77   bits: 7/7
c ---[ 742]---> Adder-cost: 0   maxlim: 77   bits: 7/7
c ---[ 740]---> Adder-cost: 156   maxlim: 78   bits: 7/7
c ---[ 738]---> Adder-cost: 142   maxlim: 78   bits: 7/7
c ---[ 735]---> Adder-cost: 152   maxlim: 78   bits: 7/7
c ---[ 733]---> Adder-cost: 154   maxlim: 78   bits: 7/7
c ---[ 730]---> Adder-cost: 150   maxlim: 79   bits: 7/7
c ---[ 728]---> Adder-cost: 134   maxlim: 79   bits: 7/7
c ---[ 724]---> Adder-cost: 152   maxlim: 79   bits: 7/7
c ---[ 722]---> Adder-cost: 134   maxlim: 79   bits: 7/7
c ---[ 720]---> Adder-cost: 144   maxlim: 80   bits: 7/7
c ---[ 718]---> Adder-cost: 104   maxlim: 80   bits: 7/7
c ---[ 716]---> Adder-cost: 156   maxlim: 80   bits: 7/7
c ---[ 714]---> Adder-cost: 142   maxlim: 81   bits: 7/7
c ---[ 712]---> Adder-cost: 160   maxlim: 82   bits: 7/7
c ---[ 710]---> Adder-cost: 162   maxlim: 82   bits: 7/7
c ---[ 708]---> Adder-cost: 160   maxlim: 82   bits: 7/7
c ---[ 706]---> Adder-cost: 158   maxlim: 82   bits: 7/7
c ---[ 703]---> Adder-cost: 154   maxlim: 83   bits: 7/7
c ---[ 701]---> Adder-cost: 154   maxlim: 83   bits: 7/7
c ---[ 699]---> Adder-cost: 106   maxlim: 83   bits: 7/7
c ---[ 697]---> Adder-cost: 160   maxlim: 83   bits: 7/7
c ---[ 695]---> Adder-cost: 152   maxlim: 83   bits: 7/7
c ---[ 693]---> Adder-cost: 144   maxlim: 83   bits: 7/7
c ---[ 692]---> Adder-cost: 158   maxlim: 83   bits: 7/7
c ---[ 690]---> Adder-cost: 128   maxlim: 83   bits: 7/7
c ---[ 688]---> Adder-cost: 148   maxlim: 83   bits: 7/7
c ---[ 686]---> Adder-cost: 150   maxlim: 84   bits: 7/7
c ---[ 684]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[ 682]---> Adder-cost: 154   maxlim: 84   bits: 7/7
c ---[ 680]---> Adder-cost: 116   maxlim: 84   bits: 7/7
c ---[ 678]---> Adder-cost: 0   maxlim: 84   bits: 7/7
c ---[ 676]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[ 674]---> Adder-cost: 140   maxlim: 85   bits: 7/7
c ---[ 672]---> Adder-cost: 142   maxlim: 85   bits: 7/7
c ---[ 670]---> Adder-cost: 152   maxlim: 85   bits: 7/7
c ---[ 668]---> Adder-cost: 132   maxlim: 85   bits: 7/7
c ---[ 666]---> Adder-cost: 132   maxlim: 86   bits: 7/7
c ---[ 664]---> Adder-cost: 160   maxlim: 86   bits: 7/7
c ---[ 662]---> Adder-cost: 134   maxlim: 86   bits: 7/7
c ---[ 660]---> Adder-cost: 154   maxlim: 87   bits: 7/7
c ---[ 658]---> Adder-cost: 146   maxlim: 87   bits: 7/7
c ---[ 656]---> Adder-cost: 168   maxlim: 87   bits: 7/7
c ---[ 654]---> Adder-cost: 110   maxlim: 88   bits: 7/7
c ---[ 652]---> Adder-cost: 162   maxlim: 88   bits: 7/7
c ---[ 650]---> Adder-cost: 140   maxlim: 88   bits: 7/7
c ---[ 648]---> Adder-cost: 140   maxlim: 88   bits: 7/7
c ---[ 646]---> Adder-cost: 160   maxlim: 88   bits: 7/7
c ---[ 644]---> Adder-cost: 172   maxlim: 88   bits: 7/7
c ---[ 642]---> Adder-cost: 166   maxlim: 88   bits: 7/7
c ---[ 640]---> Adder-cost: 0   maxlim: 88   bits: 7/7
c ---[ 638]---> Adder-cost: 164   maxlim: 88   bits: 7/7
c ---[ 636]---> Adder-cost: 166   maxlim: 89   bits: 7/7
c ---[ 634]---> Adder-cost: 106   maxlim: 90   bits: 7/7
c ---[ 632]---> Adder-cost: 172   maxlim: 90   bits: 7/7
c ---[ 630]---> Adder-cost: 158   maxlim: 90   bits: 7/7
c ---[ 628]---> Adder-cost: 176   maxlim: 90   bits: 7/7
c ---[ 626]---> Adder-cost: 170   maxlim: 90   bits: 7/7
c ---[ 624]---> Adder-cost: 164   maxlim: 90   bits: 7/7
c ---[ 622]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[ 618]---> Adder-cost: 168   maxlim: 91   bits: 7/7
c ---[ 616]---> Adder-cost: 92   maxlim: 91   bits: 7/7
c ---[ 613]---> Adder-cost: 178   maxlim: 92   bits: 7/7
c ---[ 611]---> Adder-cost: 168   maxlim: 92   bits: 7/7
c ---[ 609]---> Adder-cost: 170   maxlim: 92   bits: 7/7
c ---[ 607]---> Adder-cost: 168   maxlim: 92   bits: 7/7
c ---[ 606]---> Adder-cost: 96   maxlim: 92   bits: 7/7
c ---[ 602]---> Adder-cost: 174   maxlim: 93   bits: 7/7
c ---[ 600]---> Adder-cost: 178   maxlim: 93   bits: 7/7
c ---[ 598]---> Adder-cost: 144   maxlim: 93   bits: 7/7
c ---[ 596]---> Adder-cost: 178   maxlim: 93   bits: 7/7
c ---[ 594]---> Adder-cost: 180   maxlim: 94   bits: 7/7
c ---[ 592]---> Adder-cost: 186   maxlim: 94   bits: 7/7
c ---[ 591]---> Adder-cost: 186   maxlim: 94   bits: 7/7
c ---[ 589]---> Adder-cost: 0   maxlim: 94   bits: 7/7
c ---[ 587]---> Adder-cost: 170   maxlim: 94   bits: 7/7
c ---[ 584]---> Adder-cost: 0   maxlim: 94   bits: 7/7
c ---[ 582]---> Adder-cost: 188   maxlim: 95   bits: 7/7
c ---[ 580]---> Adder-cost: 122   maxlim: 95   bits: 7/7
c ---[ 578]---> Adder-cost: 140   maxlim: 95   bits: 7/7
c ---[ 576]---> Adder-cost: 184   maxlim: 95   bits: 7/7
c ---[ 574]---> Adder-cost: 182   maxlim: 96   bits: 7/7
c ---[ 572]---> Adder-cost: 188   maxlim: 96   bits: 7/7
c ---[ 570]---> Adder-cost: 178   maxlim: 97   bits: 7/7
c ---[ 568]---> Adder-cost: 188   maxlim: 97   bits: 7/7
c ---[ 566]---> Adder-cost: 124   maxlim: 97   bits: 7/7
c ---[ 564]---> Adder-cost: 172   maxlim: 97   bits: 7/7
c ---[ 562]---> Adder-cost: 188   maxlim: 97   bits: 7/7
c ---[ 560]---> Adder-cost: 186   maxlim: 98   bits: 7/7
c ---[ 558]---> Adder-cost: 182   maxlim: 98   bits: 7/7
c ---[ 556]---> Adder-cost: 78   maxlim: 98   bits: 7/7
c ---[ 554]---> Adder-cost: 194   maxlim: 100   bits: 7/7
c ---[ 552]---> Adder-cost: 184   maxlim: 100   bits: 7/7
c ---[ 550]---> Adder-cost: 194   maxlim: 101   bits: 7/7
c ---[ 548]---> Adder-cost: 192   maxlim: 102   bits: 7/7
c ---[ 546]---> Adder-cost: 202   maxlim: 102   bits: 7/7
c ---[ 544]---> Adder-cost: 198   maxlim: 102   bits: 7/7
c ---[ 542]---> Adder-cost: 172   maxlim: 103   bits: 7/7
c ---[ 540]---> Adder-cost: 182   maxlim: 103   bits: 7/7
c ---[ 538]---> Adder-cost: 196   maxlim: 104   bits: 7/7
c ---[ 536]---> Adder-cost: 192   maxlim: 104   bits: 7/7
c ---[ 534]---> Adder-cost: 190   maxlim: 104   bits: 7/7
c ---[ 532]---> Adder-cost: 166   maxlim: 105   bits: 7/7
c ---[ 530]---> Adder-cost: 164   maxlim: 105   bits: 7/7
c ---[ 526]---> Adder-cost: 198   maxlim: 105   bits: 7/7
c ---[ 524]---> Adder-cost: 186   maxlim: 105   bits: 7/7
c ---[ 522]---> Adder-cost: 196   maxlim: 105   bits: 7/7
c ---[ 520]---> Adder-cost: 202   maxlim: 106   bits: 7/7
c ---[ 518]---> Adder-cost: 202   maxlim: 107   bits: 7/7
c ---[ 516]---> Adder-cost: 162   maxlim: 107   bits: 7/7
c ---[ 514]---> Adder-cost: 172   maxlim: 107   bits: 7/7
c ---[ 512]---> Adder-cost: 188   maxlim: 107   bits: 7/7
c ---[ 510]---> Adder-cost: 146   maxlim: 107   bits: 7/7
c ---[ 508]---> Adder-cost: 206   maxlim: 107   bits: 7/7
c ---[ 506]---> Adder-cost: 170   maxlim: 108   bits: 7/7
c ---[ 504]---> Adder-cost: 140   maxlim: 108   bits: 7/7
c ---[ 502]---> Adder-cost: 194   maxlim: 108   bits: 7/7
c ---[ 500]---> Adder-cost: 204   maxlim: 108   bits: 7/7
c ---[ 498]---> Adder-cost: 136   maxlim: 109   bits: 7/7
c ---[ 496]---> Adder-cost: 186   maxlim: 109   bits: 7/7
c ---[ 494]---> Adder-cost: 208   maxlim: 110   bits: 7/7
c ---[ 492]---> Adder-cost: 210   maxlim: 111   bits: 7/7
c ---[ 490]---> Adder-cost: 152   maxlim: 111   bits: 7/7
c ---[ 488]---> Adder-cost: 210   maxlim: 111   bits: 7/7
c ---[ 486]---> Adder-cost: 218   maxlim: 112   bits: 7/7
c ---[ 484]---> Adder-cost: 214   maxlim: 112   bits: 7/7
c ---[ 482]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 480]---> Adder-cost: 208   maxlim: 112   bits: 7/7
c ---[ 478]---> Adder-cost: 212   maxlim: 112   bits: 7/7
c ---[ 476]---> Adder-cost: 214   maxlim: 112   bits: 7/7
c ---[ 475]---> Adder-cost: 190   maxlim: 113   bits: 7/7
c ---[ 473]---> Adder-cost: 212   maxlim: 113   bits: 7/7
c ---[ 470]---> Adder-cost: 154   maxlim: 113   bits: 7/7
c ---[ 468]---> Adder-cost: 220   maxlim: 114   bits: 7/7
c ---[ 466]---> Adder-cost: 214   maxlim: 114   bits: 7/7
c ---[ 464]---> Adder-cost: 212   maxlim: 115   bits: 7/7
c ---[ 462]---> Adder-cost: 220   maxlim: 116   bits: 7/7
c ---[ 460]---> Adder-cost: 222   maxlim: 116   bits: 7/7
c ---[ 457]---> Adder-cost: 214   maxlim: 116   bits: 7/7
c ---[ 455]---> Adder-cost: 202   maxlim: 116   bits: 7/7
c ---[ 454]---> Adder-cost: 212   maxlim: 116   bits: 7/7
c ---[ 452]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[ 450]---> Adder-cost: 212   maxlim: 117   bits: 7/7
c ---[ 448]---> Adder-cost: 212   maxlim: 117   bits: 7/7
c ---[ 446]---> Adder-cost: 216   maxlim: 118   bits: 7/7
c ---[ 444]---> Adder-cost: 158   maxlim: 118   bits: 7/7
c ---[ 442]---> Adder-cost: 182   maxlim: 118   bits: 7/7
c ---[ 440]---> Adder-cost: 190   maxlim: 119   bits: 7/7
c ---[ 438]---> Adder-cost: 214   maxlim: 119   bits: 7/7
c ---[ 436]---> Adder-cost: 144   maxlim: 119   bits: 7/7
c ---[ 434]---> Adder-cost: 170   maxlim: 119   bits: 7/7
c ---[ 432]---> Adder-cost: 180   maxlim: 119   bits: 7/7
c ---[ 430]---> Adder-cost: 222   maxlim: 119   bits: 7/7
c ---[ 426]---> Adder-cost: 230   maxlim: 119   bits: 7/7
c ---[ 424]---> Adder-cost: 198   maxlim: 120   bits: 7/7
c ---[ 422]---> Adder-cost: 230   maxlim: 120   bits: 7/7
c ---[ 420]---> Adder-cost: 226   maxlim: 120   bits: 7/7
c ---[ 418]---> Adder-cost: 232   maxlim: 120   bits: 7/7
c ---[ 416]---> Adder-cost: 186   maxlim: 120   bits: 7/7
c ---[ 414]---> Adder-cost: 230   maxlim: 121   bits: 7/7
c ---[ 412]---> Adder-cost: 232   maxlim: 121   bits: 7/7
c ---[ 410]---> Adder-cost: 146   maxlim: 121   bits: 7/7
c ---[ 408]---> Adder-cost: 188   maxlim: 121   bits: 7/7
c ---[ 406]---> Adder-cost: 194   maxlim: 122   bits: 7/7
c ---[ 404]---> Adder-cost: 226   maxlim: 122   bits: 7/7
c ---[ 402]---> Adder-cost: 220   maxlim: 122   bits: 7/7
c ---[ 400]---> Adder-cost: 222   maxlim: 123   bits: 7/7
c ---[ 398]---> Adder-cost: 224   maxlim: 123   bits: 7/7
c ---[ 396]---> Adder-cost: 214   maxlim: 123   bits: 7/7
c ---[ 394]---> Adder-cost: 222   maxlim: 123   bits: 7/7
c ---[ 392]---> Adder-cost: 238   maxlim: 124   bits: 7/7
c ---[ 390]---> Adder-cost: 214   maxlim: 124   bits: 7/7
c ---[ 388]---> Adder-cost: 150   maxlim: 125   bits: 7/7
c ---[ 386]---> Adder-cost: 232   maxlim: 125   bits: 7/7
c ---[ 384]---> Adder-cost: 242   maxlim: 126   bits: 8/7
c ---[ 382]---> Adder-cost: 238   maxlim: 126   bits: 8/7
c ---[ 380]---> Adder-cost: 244   maxlim: 126   bits: 8/7
c ---[ 378]---> Adder-cost: 250   maxlim: 126   bits: 8/7
c ---[ 376]---> Adder-cost: 228   maxlim: 126   bits: 8/7
c ---[ 374]---> Adder-cost: 246   maxlim: 127   bits: 8/7
c ---[ 372]---> Adder-cost: 242   maxlim: 127   bits: 8/7
c ---[ 370]---> Adder-cost: 248   maxlim: 127   bits: 8/7
c ---[ 368]---> Adder-cost: 186   maxlim: 128   bits: 8/8
c ---[ 366]---> Adder-cost: 142   maxlim: 128   bits: 8/8
c ---[ 364]---> Adder-cost: 218   maxlim: 128   bits: 8/8
c ---[ 362]---> Adder-cost: 230   maxlim: 128   bits: 8/8
c ---[ 360]---> Adder-cost: 250   maxlim: 128   bits: 8/8
c ---[ 358]---> Adder-cost: 250   maxlim: 129   bits: 8/8
c ---[ 356]---> Adder-cost: 210   maxlim: 129   bits: 8/8
c ---[ 354]---> Adder-cost: 232   maxlim: 129   bits: 8/8
c ---[ 353]---> Adder-cost: 168   maxlim: 129   bits: 8/8
c ---[ 351]---> Adder-cost: 250   maxlim: 129   bits: 8/8
c ---[ 349]---> Adder-cost: 118   maxlim: 129   bits: 8/8
c ---[ 347]---> Adder-cost: 184   maxlim: 129   bits: 8/8
c ---[ 344]---> Adder-cost: 236   maxlim: 130   bits: 8/8
c ---[ 342]---> Adder-cost: 232   maxlim: 130   bits: 8/8
c ---[ 340]---> Adder-cost: 232   maxlim: 130   bits: 8/8
c ---[ 338]---> Adder-cost: 254   maxlim: 131   bits: 8/8
c ---[ 336]---> Adder-cost: 252   maxlim: 131   bits: 8/8
c ---[ 334]---> Adder-cost: 166   maxlim: 131   bits: 8/8
c ---[ 332]---> Adder-cost: 176   maxlim: 132   bits: 8/8
c ---[ 330]---> Adder-cost: 248   maxlim: 132   bits: 8/8
c ---[ 328]---> Adder-cost: 248   maxlim: 133   bits: 8/8
c ---[ 326]---> Adder-cost: 256   maxlim: 133   bits: 8/8
c ---[ 324]---> Adder-cost: 244   maxlim: 133   bits: 8/8
c ---[ 322]---> Adder-cost: 238   maxlim: 133   bits: 8/8
c ---[ 320]---> Adder-cost: 262   maxlim: 133   bits: 8/8
c ---[ 318]---> Adder-cost: 246   maxlim: 133   bits: 8/8
c ---[ 316]---> Adder-cost: 0   maxlim: 133   bits: 8/8
c ---[ 314]---> Adder-cost: 168   maxlim: 133   bits: 8/8
c ---[ 312]---> Adder-cost: 258   maxlim: 134   bits: 8/8
c ---[ 310]---> Adder-cost: 208   maxlim: 135   bits: 8/8
c ---[ 308]---> Adder-cost: 226   maxlim: 135   bits: 8/8
c ---[ 306]---> Adder-cost: 142   maxlim: 135   bits: 8/8
c ---[ 304]---> Adder-cost: 264   maxlim: 136   bits: 8/8
c ---[ 302]---> Adder-cost: 240   maxlim: 136   bits: 8/8
c ---[ 300]---> Adder-cost: 264   maxlim: 136   bits: 8/8
c ---[ 298]---> Adder-cost: 252   maxlim: 137   bits: 8/8
c ---[ 296]---> Adder-cost: 218   maxlim: 137   bits: 8/8
c ---[ 294]---> Adder-cost: 242   maxlim: 137   bits: 8/8
c ---[ 292]---> Adder-cost: 254   maxlim: 137   bits: 8/8
c ---[ 290]---> Adder-cost: 258   maxlim: 138   bits: 8/8
c ---[ 288]---> Adder-cost: 244   maxlim: 138   bits: 8/8
c ---[ 286]---> Adder-cost: 268   maxlim: 138   bits: 8/8
c ---[ 284]---> Adder-cost: 264   maxlim: 139   bits: 8/8
c ---[ 282]---> Adder-cost: 266   maxlim: 139   bits: 8/8
c ---[ 280]---> Adder-cost: 248   maxlim: 140   bits: 8/8
c ---[ 278]---> Adder-cost: 170   maxlim: 140   bits: 8/8
c ---[ 276]---> Adder-cost: 250   maxlim: 140   bits: 8/8
c ---[ 274]---> Adder-cost: 264   maxlim: 141   bits: 8/8
c ---[ 272]---> Adder-cost: 252   maxlim: 141   bits: 8/8
c ---[ 270]---> Adder-cost: 268   maxlim: 142   bits: 8/8
c ---[ 268]---> Adder-cost: 252   maxlim: 142   bits: 8/8
c ---[ 266]---> Adder-cost: 262   maxlim: 142   bits: 8/8
c ---[ 264]---> Adder-cost: 204   maxlim: 142   bits: 8/8
c ---[ 262]---> Adder-cost: 256   maxlim: 142   bits: 8/8
c ---[ 260]---> Adder-cost: 214   maxlim: 143   bits: 8/8
c ---[ 258]---> Adder-cost: 220   maxlim: 143   bits: 8/8
c ---[ 256]---> Adder-cost: 280   maxlim: 143   bits: 8/8
c ---[ 254]---> Adder-cost: 242   maxlim: 143   bits: 8/8
c ---[ 252]---> Adder-cost: 256   maxlim: 143   bits: 8/8
c ---[ 250]---> Adder-cost: 252   maxlim: 144   bits: 8/8
c ---[ 248]---> Adder-cost: 256   maxlim: 144   bits: 8/8
c ---[ 246]---> Adder-cost: 252   maxlim: 144   bits: 8/8
c ---[ 244]---> Adder-cost: 240   maxlim: 144   bits: 8/8
c ---[ 242]---> Adder-cost: 260   maxlim: 144   bits: 8/8
c ---[ 240]---> Adder-cost: 264   maxlim: 145   bits: 8/8
c ---[ 238]---> Adder-cost: 274   maxlim: 146   bits: 8/8
c ---[ 236]---> Adder-cost: 278   maxlim: 147   bits: 8/8
c ---[ 234]---> Adder-cost: 130   maxlim: 147   bits: 8/8
c ---[ 232]---> Adder-cost: 264   maxlim: 149   bits: 8/8
c ---[ 230]---> Adder-cost: 260   maxlim: 149   bits: 8/8
c ---[ 228]---> Adder-cost: 266   maxlim: 150   bits: 8/8
c ---[ 226]---> Adder-cost: 178   maxlim: 150   bits: 8/8
c ---[ 224]---> Adder-cost: 240   maxlim: 151   bits: 8/8
c ---[ 222]---> Adder-cost: 290   maxlim: 151   bits: 8/8
c ---[ 220]---> Adder-cost: 274   maxlim: 153   bits: 8/8
c ---[ 219]---> Adder-cost: 296   maxlim: 154   bits: 8/8
c ---[ 217]---> Adder-cost: 240   maxlim: 154   bits: 8/8
c ---[ 214]---> Adder-cost: 292   maxlim: 154   bits: 8/8
c ---[ 212]---> Adder-cost: 300   maxlim: 155   bits: 8/8
c ---[ 210]---> Adder-cost: 294   maxlim: 155   bits: 8/8
c ---[ 208]---> Adder-cost: 280   maxlim: 156   bits: 8/8
c ---[ 206]---> Adder-cost: 248   maxlim: 156   bits: 8/8
c ---[ 204]---> Adder-cost: 286   maxlim: 157   bits: 8/8
c ---[ 202]---> Adder-cost: 288   maxlim: 157   bits: 8/8
c ---[ 200]---> Adder-cost: 270   maxlim: 158   bits: 8/8
c ---[ 198]---> Adder-cost: 300   maxlim: 158   bits: 8/8
c ---[ 195]---> Adder-cost: 308   maxlim: 159   bits: 8/8
c ---[ 194]---> Adder-cost: 304   maxlim: 159   bits: 8/8
c ---[ 192]---> Adder-cost: 286   maxlim: 159   bits: 8/8
c ---[ 190]---> Adder-cost: 308   maxlim: 160   bits: 8/8
c ---[ 187]---> Adder-cost: 210   maxlim: 160   bits: 8/8
c ---[ 186]---> Adder-cost: 308   maxlim: 160   bits: 8/8
c ---[ 184]---> Adder-cost: 288   maxlim: 162   bits: 8/8
c ---[ 182]---> Adder-cost: 240   maxlim: 163   bits: 8/8
c ---[ 180]---> Adder-cost: 236   maxlim: 164   bits: 8/8
c ---[ 178]---> Adder-cost: 298   maxlim: 164   bits: 8/8
c ---[ 176]---> Adder-cost: 296   maxlim: 165   bits: 8/8
c ---[ 174]---> Adder-cost: 224   maxlim: 167   bits: 8/8
c ---[ 172]---> Adder-cost: 304   maxlim: 167   bits: 8/8
c ---[ 170]---> Adder-cost: 190   maxlim: 168   bits: 8/8
c ---[ 168]---> Adder-cost: 306   maxlim: 169   bits: 8/8
c ---[ 166]---> Adder-cost: 320   maxlim: 170   bits: 8/8
c ---[ 164]---> Adder-cost: 224   maxlim: 171   bits: 8/8
c ---[ 162]---> Adder-cost: 240   maxlim: 171   bits: 8/8
c ---[ 160]---> Adder-cost: 282   maxlim: 172   bits: 8/8
c ---[ 158]---> Adder-cost: 298   maxlim: 172   bits: 8/8
c ---[ 156]---> Adder-cost: 326   maxlim: 173   bits: 8/8
c ---[ 154]---> Adder-cost: 322   maxlim: 173   bits: 8/8
c ---[ 152]---> Adder-cost: 252   maxlim: 173   bits: 8/8
c ---[ 150]---> Adder-cost: 326   maxlim: 173   bits: 8/8
c ---[ 148]---> Adder-cost: 228   maxlim: 174   bits: 8/8
c ---[ 146]---> Adder-cost: 262   maxlim: 174   bits: 8/8
c ---[ 144]---> Adder-cost: 330   maxlim: 174   bits: 8/8
c ---[ 142]---> Adder-cost: 334   maxlim: 176   bits: 8/8
c ---[ 140]---> Adder-cost: 314   maxlim: 176   bits: 8/8
c ---[ 138]---> Adder-cost: 334   maxlim: 176   bits: 8/8
c ---[ 136]---> Adder-cost: 270   maxlim: 176   bits: 8/8
c ---[ 134]---> Adder-cost: 344   maxlim: 177   bits: 8/8
c ---[ 132]---> Adder-cost: 298   maxlim: 177   bits: 8/8
c ---[ 130]---> Adder-cost: 294   maxlim: 178   bits: 8/8
c ---[ 128]---> Adder-cost: 306   maxlim: 179   bits: 8/8
c ---[ 126]---> Adder-cost: 294   maxlim: 181   bits: 8/8
c ---[ 124]---> Adder-cost: 210   maxlim: 183   bits: 8/8
c ---[ 122]---> Adder-cost: 340   maxlim: 184   bits: 8/8
c ---[ 120]---> Adder-cost: 318   maxlim: 184   bits: 8/8
c ---[ 118]---> Adder-cost: 342   maxlim: 184   bits: 8/8
c ---[ 116]---> Adder-cost: 320   maxlim: 185   bits: 8/8
c ---[ 114]---> Adder-cost: 332   maxlim: 186   bits: 8/8
c ---[ 112]---> Adder-cost: 216   maxlim: 186   bits: 8/8
c ---[ 110]---> Adder-cost: 354   maxlim: 187   bits: 8/8
c ---[ 108]---> Adder-cost: 336   maxlim: 187   bits: 8/8
c ---[ 106]---> Adder-cost: 0   maxlim: 187   bits: 8/8
c ---[ 104]---> Adder-cost: 182   maxlim: 188   bits: 8/8
c ---[ 102]---> Adder-cost: 348   maxlim: 192   bits: 8/8
c ---[ 100]---> Adder-cost: 276   maxlim: 192   bits: 8/8
c ---[  97]---> Adder-cost: 368   maxlim: 193   bits: 8/8
c ---[  95]---> Adder-cost: 326   maxlim: 193   bits: 8/8
c ---[  94]---> Adder-cost: 350   maxlim: 193   bits: 8/8
c ---[  92]---> Adder-cost: 344   maxlim: 193   bits: 8/8
c ---[  90]---> Adder-cost: 274   maxlim: 193   bits: 8/8
c ---[  88]---> Adder-cost: 300   maxlim: 194   bits: 8/8
c ---[  86]---> Adder-cost: 280   maxlim: 194   bits: 8/8
c ---[  84]---> Adder-cost: 330   maxlim: 195   bits: 8/8
c ---[  82]---> Adder-cost: 366   maxlim: 195   bits: 8/8
c ---[  80]---> Adder-cost: 356   maxlim: 195   bits: 8/8
c ---[  78]---> Adder-cost: 318   maxlim: 196   bits: 8/8
c ---[  76]---> Adder-cost: 318   maxlim: 196   bits: 8/8
c ---[  74]---> Adder-cost: 316   maxlim: 196   bits: 8/8
c ---[  72]---> Adder-cost: 356   maxlim: 197   bits: 8/8
c ---[  70]---> Adder-cost: 214   maxlim: 198   bits: 8/8
c ---[  68]---> Adder-cost: 318   maxlim: 199   bits: 8/8
c ---[  66]---> Adder-cost: 382   maxlim: 201   bits: 8/8
c ---[  64]---> Adder-cost: 298   maxlim: 202   bits: 8/8
c ---[  62]---> Adder-cost: 380   maxlim: 203   bits: 8/8
c ---[  60]---> Adder-cost: 378   maxlim: 203   bits: 8/8
c ---[  58]---> Adder-cost: 322   maxlim: 205   bits: 8/8
c ---[  56]---> Adder-cost: 344   maxlim: 206   bits: 8/8
c ---[  54]---> Adder-cost: 316   maxlim: 206   bits: 8/8
c ---[  52]---> Adder-cost: 334   maxlim: 206   bits: 8/8
c ---[  48]---> Adder-cost: 376   maxlim: 209   bits: 8/8
c ---[  46]---> Adder-cost: 400   maxlim: 209   bits: 8/8
c ---[  44]---> Adder-cost: 324   maxlim: 210   bits: 8/8
c ---[  42]---> Adder-cost: 400   maxlim: 214   bits: 8/8
c ---[  40]---> Adder-cost: 344   maxlim: 216   bits: 8/8
c ---[  38]---> Adder-cost: 350   maxlim: 218   bits: 8/8
c ---[  36]---> Adder-cost: 414   maxlim: 219   bits: 8/8
c ---[  34]---> Adder-cost: 392   maxlim: 220   bits: 8/8
c ---[  32]---> Adder-cost: 348   maxlim: 220   bits: 8/8
c ---[  30]---> Adder-cost: 400   maxlim: 221   bits: 8/8
c ---[  28]---> Adder-cost: 372   maxlim: 223   bits: 8/8
c ---[  26]---> Adder-cost: 412   maxlim: 228   bits: 8/8
c ---[  24]---> Adder-cost: 374   maxlim: 233   bits: 8/8
c ---[  22]---> Adder-cost: 384   maxlim: 236   bits: 8/8
c ---[  20]---> Adder-cost: 388   maxlim: 238   bits: 8/8
c ---[  18]---> Adder-cost: 452   maxlim: 244   bits: 8/8
c ---[  16]---> Adder-cost: 376   maxlim: 246   bits: 8/8
c ---[  14]---> Adder-cost: 370   maxlim: 246   bits: 8/8
c ---[  12]---> Adder-cost: 570   maxlim: 301   bits: 9/9
c ---[  10]---> Adder-cost: 416   maxlim: 301   bits: 9/9
c ---[   8]---> Adder-cost: 570   maxlim: 326   bits: 9/9
c ---[   6]---> Adder-cost: 628   maxlim: 336   bits: 9/9
c ---[   4]---> Adder-cost: 608   maxlim: 345   bits: 9/9
c ---[   2]---> Adder-cost: 480   maxlim: 352   bits: 9/9
c ---[   0]---> Adder-cost: 608   maxlim: 366   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  794863  2834588 |  264954       0        0     nan |  0.000 % |
c |       100 |  794622  2833751 |  291449      60      183     3.0 |  4.769 % |
c |       250 |  793789  2830823 |  320594     108      366     3.4 |  4.890 % |
c |       475 |  792534  2826376 |  352653     189      597     3.2 |  5.075 % |
c |       812 |  789966  2817353 |  387919     269      840     3.1 |  5.471 % |
c |      1318 |  786623  2805702 |  426711     413     1364     3.3 |  5.981 % |
c |      2077 |  781095  2786282 |  469382     565     1937     3.4 |  6.813 % |
c |      3216 |  774751  2763961 |  516320     920     3204     3.5 |  7.706 % |
c |      4926 |  766757  2735948 |  567952    1627     6091     3.7 |  8.806 % |
c |      7491 |  757096  2702099 |  624747    2927    11898     4.1 | 10.095 % |
c |     11335 |  750661  2679572 |  687222    5883    26644     4.5 | 10.947 % |
#### 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.70 0.90 0.89 2/56 27113
Raw data (stat): 27113 (runsolver) R 27112 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 372770927 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.75 0.90 0.89 2/56 27113
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14378 0 0 0 966 32 0 0 25 0 1 0 372770927 63041536 14002 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15391 14002 603 41 0 15350 0
vsize: 61564
[startup+20.0004 s]
Raw data (loadavg): 0.79 0.90 0.89 2/56 27113
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14381 0 0 0 1966 33 0 0 25 0 1 0 372770927 63176704 14005 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14005 603 41 0 15383 0
vsize: 61696
[startup+30.0012 s]
Raw data (loadavg): 0.82 0.90 0.89 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14387 0 0 0 2966 33 0 0 25 0 1 0 372770927 63176704 14011 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14011 603 41 0 15383 0
vsize: 61696
[startup+40.001 s]
Raw data (loadavg): 0.85 0.91 0.89 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14411 0 0 0 3966 33 0 0 25 0 1 0 372770927 63176704 14035 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15424 14035 603 41 0 15383 0
vsize: 61696
[startup+50.0017 s]
Raw data (loadavg): 0.87 0.91 0.89 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14432 0 0 0 4966 33 0 0 25 0 1 0 372770927 63311872 14056 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15457 14056 603 41 0 15416 0
vsize: 61828
[startup+60.0018 s]
Raw data (loadavg): 0.89 0.91 0.89 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14461 0 0 0 5966 33 0 0 25 0 1 0 372770927 63447040 14085 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15490 14085 603 41 0 15449 0
vsize: 61960
[startup+70.0012 s]
Raw data (loadavg): 0.90 0.91 0.89 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14489 0 0 0 6966 33 0 0 25 0 1 0 372770927 63582208 14113 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15523 14113 603 41 0 15482 0
vsize: 62092
[startup+80.002 s]
Raw data (loadavg): 0.92 0.92 0.89 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14506 0 0 0 7966 34 0 0 25 0 1 0 372770927 63582208 14130 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15523 14130 603 41 0 15482 0
vsize: 62092
[startup+90.0018 s]
Raw data (loadavg): 0.93 0.92 0.89 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14527 0 0 0 8967 34 0 0 25 0 1 0 372770927 63717376 14151 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15556 14151 603 41 0 15515 0
vsize: 62224
[startup+100.002 s]
Raw data (loadavg): 0.94 0.92 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14546 0 0 0 9967 34 0 0 25 0 1 0 372770927 63852544 14170 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15589 14170 603 41 0 15548 0
vsize: 62356
[startup+110.002 s]
Raw data (loadavg): 0.95 0.92 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14564 0 0 0 10967 34 0 0 25 0 1 0 372770927 63852544 14188 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15589 14188 603 41 0 15548 0
vsize: 62356
[startup+120.003 s]
Raw data (loadavg): 0.96 0.92 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14583 0 0 0 11967 34 0 0 25 0 1 0 372770927 63987712 14207 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15622 14207 603 41 0 15581 0
vsize: 62488
[startup+130.003 s]
Raw data (loadavg): 0.96 0.93 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14607 0 0 0 12967 34 0 0 25 0 1 0 372770927 63987712 14231 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15622 14231 603 41 0 15581 0
vsize: 62488
[startup+140.003 s]
Raw data (loadavg): 0.97 0.93 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14625 0 0 0 13966 34 0 0 25 0 1 0 372770927 64122880 14249 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15655 14249 603 41 0 15614 0
vsize: 62620
[startup+150.004 s]
Raw data (loadavg): 0.97 0.93 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14643 0 0 0 14967 35 0 0 25 0 1 0 372770927 64258048 14267 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15688 14267 603 41 0 15647 0
vsize: 62752
[startup+160.003 s]
Raw data (loadavg): 0.98 0.93 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14659 0 0 0 15966 35 0 0 25 0 1 0 372770927 64258048 14283 4294967295 134512640 134672761 3221224576 3221223748 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15688 14283 603 41 0 15647 0
vsize: 62752
[startup+170.003 s]
Raw data (loadavg): 0.98 0.93 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14676 0 0 0 16966 35 0 0 25 0 1 0 372770927 64393216 14300 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14300 603 41 0 15680 0
vsize: 62884
[startup+180.003 s]
Raw data (loadavg): 0.98 0.94 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14694 0 0 0 17966 36 0 0 25 0 1 0 372770927 64393216 14318 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14318 603 41 0 15680 0
vsize: 62884
[startup+190.004 s]
Raw data (loadavg): 0.98 0.94 0.90 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14709 0 0 0 18966 36 0 0 25 0 1 0 372770927 64393216 14333 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14333 603 41 0 15680 0
vsize: 62884
[startup+200.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14723 0 0 0 19965 36 0 0 25 0 1 0 372770927 64528384 14347 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15754 14347 603 41 0 15713 0
vsize: 63016
[startup+210.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14735 0 0 0 20965 36 0 0 25 0 1 0 372770927 64528384 14359 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15754 14359 603 41 0 15713 0
vsize: 63016
[startup+220.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14743 0 0 0 21965 36 0 0 25 0 1 0 372770927 64663552 14367 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15787 14367 603 41 0 15746 0
vsize: 63148
[startup+230.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14759 0 0 0 22965 37 0 0 25 0 1 0 372770927 64663552 14383 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15787 14383 603 41 0 15746 0
vsize: 63148
[startup+240.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14768 0 0 0 23965 37 0 0 25 0 1 0 372770927 64663552 14392 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15787 14392 603 41 0 15746 0
vsize: 63148
[startup+250.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14778 0 0 0 24965 37 0 0 25 0 1 0 372770927 64798720 14402 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15820 14402 603 41 0 15779 0
vsize: 63280
[startup+260.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14792 0 0 0 25965 37 0 0 25 0 1 0 372770927 64798720 14416 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15820 14416 603 41 0 15779 0
vsize: 63280
[startup+270.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14802 0 0 0 26965 37 0 0 25 0 1 0 372770927 64798720 14426 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15820 14426 603 41 0 15779 0
vsize: 63280
[startup+280.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14812 0 0 0 27965 37 0 0 25 0 1 0 372770927 64933888 14436 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15853 14436 603 41 0 15812 0
vsize: 63412
[startup+290.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14827 0 0 0 28965 38 0 0 25 0 1 0 372770927 64933888 14451 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15853 14451 603 41 0 15812 0
vsize: 63412
[startup+300.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14837 0 0 0 29965 38 0 0 25 0 1 0 372770927 65069056 14461 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15886 14461 603 41 0 15845 0
vsize: 63544
[startup+310.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14850 0 0 0 30965 38 0 0 25 0 1 0 372770927 65069056 14474 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15886 14474 603 41 0 15845 0
vsize: 63544
[startup+320.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27115
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14858 0 0 0 31965 38 0 0 25 0 1 0 372770927 65069056 14482 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15886 14482 603 41 0 15845 0
vsize: 63544
[startup+330.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14865 0 0 0 32965 39 0 0 25 0 1 0 372770927 65069056 14489 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15886 14489 603 41 0 15845 0
vsize: 63544
[startup+340.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14871 0 0 0 33965 39 0 0 25 0 1 0 372770927 65204224 14495 4294967295 134512640 134672761 3221224576 3221223744 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15919 14495 603 41 0 15878 0
vsize: 63676
[startup+350.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14877 0 0 0 34965 39 0 0 25 0 1 0 372770927 65204224 14501 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15919 14501 603 41 0 15878 0
vsize: 63676
[startup+360.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14886 0 0 0 35965 39 0 0 25 0 1 0 372770927 65204224 14510 4294967295 134512640 134672761 3221224576 3221223792 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15919 14510 603 41 0 15878 0
vsize: 63676
[startup+370.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14895 0 0 0 36965 39 0 0 25 0 1 0 372770927 65204224 14519 4294967295 134512640 134672761 3221224576 3221223748 134556604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15919 14519 603 41 0 15878 0
vsize: 63676
[startup+380.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14905 0 0 0 37965 39 0 0 25 0 1 0 372770927 65204224 14529 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15919 14529 603 41 0 15878 0
vsize: 63676
[startup+390.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14908 0 0 0 38965 39 0 0 25 0 1 0 372770927 65339392 14532 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14532 603 41 0 15911 0
vsize: 63808
[startup+400.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14914 0 0 0 39965 39 0 0 25 0 1 0 372770927 65339392 14538 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14538 603 41 0 15911 0
vsize: 63808
[startup+410.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14921 0 0 0 40965 40 0 0 25 0 1 0 372770927 65339392 14545 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15952 14545 603 41 0 15911 0
vsize: 63808
[startup+420.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14928 0 0 0 41965 40 0 0 25 0 1 0 372770927 65339392 14552 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15952 14552 603 41 0 15911 0
vsize: 63808
[startup+430.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14935 0 0 0 42965 40 0 0 25 0 1 0 372770927 65339392 14559 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14559 603 41 0 15911 0
vsize: 63808
[startup+440.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14943 0 0 0 43965 40 0 0 25 0 1 0 372770927 65339392 14567 4294967295 134512640 134672761 3221224576 3221223768 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14567 603 41 0 15911 0
vsize: 63808
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14945 0 0 0 44965 40 0 0 25 0 1 0 372770927 65474560 14569 4294967295 134512640 134672761 3221224576 3221223748 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14569 603 41 0 15944 0
vsize: 63940
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14949 0 0 0 45965 40 0 0 25 0 1 0 372770927 65474560 14573 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14573 603 41 0 15944 0
vsize: 63940
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14955 0 0 0 46965 40 0 0 25 0 1 0 372770927 65474560 14579 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14579 603 41 0 15944 0
vsize: 63940
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14961 0 0 0 47965 40 0 0 25 0 1 0 372770927 65474560 14585 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14585 603 41 0 15944 0
vsize: 63940
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14966 0 0 0 48965 40 0 0 25 0 1 0 372770927 65474560 14590 4294967295 134512640 134672761 3221224576 3221223764 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14590 603 41 0 15944 0
vsize: 63940
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14974 0 0 0 49965 41 0 0 25 0 1 0 372770927 65474560 14598 4294967295 134512640 134672761 3221224576 3221223820 134561422 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14598 603 41 0 15944 0
vsize: 63940
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14979 0 0 0 50965 41 0 0 25 0 1 0 372770927 65474560 14603 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14603 603 41 0 15944 0
vsize: 63940
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14981 0 0 0 51965 41 0 0 25 0 1 0 372770927 65474560 14605 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 14605 603 41 0 15944 0
vsize: 63940
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14983 0 0 0 52966 41 0 0 25 0 1 0 372770927 65609728 14607 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16018 14607 603 41 0 15977 0
vsize: 64072
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14987 0 0 0 53966 41 0 0 25 0 1 0 372770927 65609728 14611 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16018 14611 603 41 0 15977 0
vsize: 64072
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14989 0 0 0 54966 41 0 0 25 0 1 0 372770927 65609728 14613 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16018 14613 603 41 0 15977 0
vsize: 64072
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14990 0 0 0 55966 41 0 0 25 0 1 0 372770927 65609728 14614 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16018 14614 603 41 0 15977 0
vsize: 64072
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14992 0 0 0 56966 41 0 0 25 0 1 0 372770927 65609728 14616 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16018 14616 603 41 0 15977 0
vsize: 64072
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 14993 0 0 0 57966 41 0 0 25 0 1 0 372770927 65609728 14617 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16018 14617 603 41 0 15977 0
vsize: 64072
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15012 0 0 0 58966 41 0 0 25 0 1 0 372770927 65765376 14636 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14636 603 41 0 16015 0
vsize: 64224
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15014 0 0 0 59966 41 0 0 25 0 1 0 372770927 65765376 14638 4294967295 134512640 134672761 3221224576 3221223784 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14638 603 41 0 16015 0
vsize: 64224
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15015 0 0 0 60967 41 0 0 25 0 1 0 372770927 65765376 14639 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14639 603 41 0 16015 0
vsize: 64224
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27117
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15016 0 0 0 61966 41 0 0 25 0 1 0 372770927 65765376 14640 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14640 603 41 0 16015 0
vsize: 64224
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15017 0 0 0 62966 42 0 0 25 0 1 0 372770927 65765376 14641 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14641 603 41 0 16015 0
vsize: 64224
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15018 0 0 0 63966 42 0 0 25 0 1 0 372770927 65765376 14642 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14642 603 41 0 16015 0
vsize: 64224
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15020 0 0 0 64966 42 0 0 25 0 1 0 372770927 65765376 14644 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14644 603 41 0 16015 0
vsize: 64224
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15021 0 0 0 65966 42 0 0 25 0 1 0 372770927 65765376 14645 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14645 603 41 0 16015 0
vsize: 64224
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15023 0 0 0 66966 43 0 0 25 0 1 0 372770927 65765376 14647 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14647 603 41 0 16015 0
vsize: 64224
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15024 0 0 0 67966 43 0 0 25 0 1 0 372770927 65765376 14648 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14648 603 41 0 16015 0
vsize: 64224
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15026 0 0 0 68966 43 0 0 25 0 1 0 372770927 65765376 14650 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14650 603 41 0 16015 0
vsize: 64224
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15028 0 0 0 69966 43 0 0 25 0 1 0 372770927 65765376 14652 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14652 603 41 0 16015 0
vsize: 64224
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15029 0 0 0 70966 43 0 0 25 0 1 0 372770927 65765376 14653 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14653 603 41 0 16015 0
vsize: 64224
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15032 0 0 0 71966 44 0 0 25 0 1 0 372770927 65765376 14656 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14656 603 41 0 16015 0
vsize: 64224
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15034 0 0 0 72966 44 0 0 25 0 1 0 372770927 65765376 14658 4294967295 134512640 134672761 3221224576 3221223700 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14658 603 41 0 16015 0
vsize: 64224
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15035 0 0 0 73966 44 0 0 25 0 1 0 372770927 65765376 14659 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14659 603 41 0 16015 0
vsize: 64224
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15037 0 0 0 74967 44 0 0 25 0 1 0 372770927 65765376 14661 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14661 603 41 0 16015 0
vsize: 64224
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15038 0 0 0 75966 44 0 0 25 0 1 0 372770927 65765376 14662 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14662 603 41 0 16015 0
vsize: 64224
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15040 0 0 0 76966 44 0 0 25 0 1 0 372770927 65765376 14664 4294967295 134512640 134672761 3221224576 3221223728 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14664 603 41 0 16015 0
vsize: 64224
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15044 0 0 0 77966 44 0 0 25 0 1 0 372770927 65765376 14668 4294967295 134512640 134672761 3221224576 3221223748 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14668 603 41 0 16015 0
vsize: 64224
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15045 0 0 0 78966 44 0 0 25 0 1 0 372770927 65765376 14669 4294967295 134512640 134672761 3221224576 3221223792 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14669 603 41 0 16015 0
vsize: 64224
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15047 0 0 0 79966 45 0 0 25 0 1 0 372770927 65765376 14671 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14671 603 41 0 16015 0
vsize: 64224
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15053 0 0 0 80966 45 0 0 25 0 1 0 372770927 65765376 14677 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15054 0 0 0 81966 45 0 0 25 0 1 0 372770927 65765376 14678 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14678 603 41 0 16015 0
vsize: 64224
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15054 0 0 0 82966 45 0 0 25 0 1 0 372770927 65765376 14678 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14678 603 41 0 16015 0
vsize: 64224
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15056 0 0 0 83966 45 0 0 25 0 1 0 372770927 65765376 14680 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14680 603 41 0 16015 0
vsize: 64224
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15056 0 0 0 84966 45 0 0 25 0 1 0 372770927 65765376 14680 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14680 603 41 0 16015 0
vsize: 64224
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15057 0 0 0 85966 46 0 0 25 0 1 0 372770927 65765376 14681 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14681 603 41 0 16015 0
vsize: 64224
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15057 0 0 0 86966 46 0 0 25 0 1 0 372770927 65765376 14681 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14681 603 41 0 16015 0
vsize: 64224
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15058 0 0 0 87966 46 0 0 25 0 1 0 372770927 65765376 14682 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14682 603 41 0 16015 0
vsize: 64224
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15059 0 0 0 88966 46 0 0 25 0 1 0 372770927 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134564499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15065 0 0 0 89967 46 0 0 25 0 1 0 372770927 65765376 14689 4294967295 134512640 134672761 3221224576 3221223744 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14689 603 41 0 16015 0
vsize: 64224
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15066 0 0 0 90966 46 0 0 25 0 1 0 372770927 65765376 14690 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14690 603 41 0 16015 0
vsize: 64224
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27119
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15071 0 0 0 91966 46 0 0 25 0 1 0 372770927 65765376 14695 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14695 603 41 0 16015 0
vsize: 64224
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15073 0 0 0 92966 46 0 0 25 0 1 0 372770927 65765376 14697 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14697 603 41 0 16015 0
vsize: 64224
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15074 0 0 0 93966 47 0 0 25 0 1 0 372770927 65765376 14698 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14698 603 41 0 16015 0
vsize: 64224
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15075 0 0 0 94966 47 0 0 25 0 1 0 372770927 65765376 14699 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14699 603 41 0 16015 0
vsize: 64224
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15075 0 0 0 95967 47 0 0 25 0 1 0 372770927 65765376 14699 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14699 603 41 0 16015 0
vsize: 64224
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15076 0 0 0 96966 47 0 0 25 0 1 0 372770927 65765376 14700 4294967295 134512640 134672761 3221224576 3221223764 134557974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14700 603 41 0 16015 0
vsize: 64224
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15076 0 0 0 97966 47 0 0 25 0 1 0 372770927 65765376 14700 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14700 603 41 0 16015 0
vsize: 64224
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15077 0 0 0 98966 47 0 0 25 0 1 0 372770927 65765376 14701 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14701 603 41 0 16015 0
vsize: 64224
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15077 0 0 0 99966 47 0 0 25 0 1 0 372770927 65765376 14701 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14701 603 41 0 16015 0
vsize: 64224
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15077 0 0 0 100967 47 0 0 25 0 1 0 372770927 65765376 14701 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14701 603 41 0 16015 0
vsize: 64224
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15078 0 0 0 101967 48 0 0 25 0 1 0 372770927 65765376 14702 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14702 603 41 0 16015 0
vsize: 64224
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15079 0 0 0 102967 48 0 0 25 0 1 0 372770927 65765376 14703 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14703 603 41 0 16015 0
vsize: 64224
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15084 0 0 0 103966 48 0 0 25 0 1 0 372770927 65765376 14708 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14708 603 41 0 16015 0
vsize: 64224
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15085 0 0 0 104967 48 0 0 25 0 1 0 372770927 65765376 14709 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14709 603 41 0 16015 0
vsize: 64224
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15087 0 0 0 105967 48 0 0 25 0 1 0 372770927 65765376 14711 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14711 603 41 0 16015 0
vsize: 64224
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15087 0 0 0 106967 48 0 0 25 0 1 0 372770927 65765376 14711 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14711 603 41 0 16015 0
vsize: 64224
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15088 0 0 0 107967 48 0 0 25 0 1 0 372770927 65765376 14712 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14712 603 41 0 16015 0
vsize: 64224
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15088 0 0 0 108967 48 0 0 25 0 1 0 372770927 65765376 14712 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14712 603 41 0 16015 0
vsize: 64224
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15088 0 0 0 109967 49 0 0 25 0 1 0 372770927 65765376 14712 4294967295 134512640 134672761 3221224576 3221223700 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14712 603 41 0 16015 0
vsize: 64224
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15088 0 0 0 110967 49 0 0 25 0 1 0 372770927 65765376 14712 4294967295 134512640 134672761 3221224576 3221223792 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14712 603 41 0 16015 0
vsize: 64224
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15088 0 0 0 111967 49 0 0 25 0 1 0 372770927 65765376 14712 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14712 603 41 0 16015 0
vsize: 64224
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15089 0 0 0 112967 49 0 0 25 0 1 0 372770927 65765376 14713 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14713 603 41 0 16015 0
vsize: 64224
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15098 0 0 0 113967 49 0 0 25 0 1 0 372770927 65921024 14722 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14722 603 41 0 16053 0
vsize: 64376
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15098 0 0 0 114967 50 0 0 25 0 1 0 372770927 65921024 14722 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14722 603 41 0 16053 0
vsize: 64376
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15098 0 0 0 115967 50 0 0 25 0 1 0 372770927 65921024 14722 4294967295 134512640 134672761 3221224576 3221223700 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14722 603 41 0 16053 0
vsize: 64376
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15098 0 0 0 116967 50 0 0 25 0 1 0 372770927 65921024 14722 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14722 603 41 0 16053 0
vsize: 64376
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15098 0 0 0 117967 50 0 0 25 0 1 0 372770927 65921024 14722 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14722 603 41 0 16053 0
vsize: 64376
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15099 0 0 0 118967 50 0 0 25 0 1 0 372770927 65921024 14723 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14723 603 41 0 16053 0
vsize: 64376
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27121
Raw data (stat): 27113 (minisat+) R 27112 12452 12451 0 -1 0 15099 0 0 0 119967 50 0 0 25 0 1 0 372770927 65921024 14723 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14723 603 41 0 16053 0
vsize: 64376
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 27121
Raw data (stat): 27113 (minisat+) Z 27112 12452 12451 0 -1 12 15101 0 0 0 119967 53 0 0 25 0 1 0 372770927 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.06
CPU time (s): 1200.21
CPU user time (s): 1199.68
CPU system time (s): 0.534918
CPU usage (%): 100.012
Max. virtual memory (Kb): 64376
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####