PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-air06.opb
MD5SUM	f85d0079133f298b06c25764b03ff228
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50233
Optimality of the best value was proved	NO
Number of terms in the objective function	8627
Biggest coefficient in the objective function	1859
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	4587852
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	1859
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	4587852
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	1182.3
Number of variables	8627
Total number of constraints	9452
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9452
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	461
Trace number 22328

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        290816 kB
Buffers:         25404 kB
Cached:         696156 kB
SwapCached:        328 kB
Active:          67412 kB
Inactive:       656768 kB
HighTotal:      131008 kB
HighFree:        19796 kB
LowTotal:       903652 kB
LowFree:        271020 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6460 kB
Slab:            13912 kB
Committed_AS:    63576 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:16:01 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 11684 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1628 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1626]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[1622]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1618]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[1616]---> Adder-cost: 46   maxlim: 34   bits: 6/6
c ---[1614]---> Adder-cost: 86   maxlim: 55   bits: 6/6
c ---[1612]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[1610]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1608]---> Adder-cost: 26   maxlim: 29   bits: 5/5
c ---[1604]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1602]---> Adder-cost: 76   maxlim: 55   bits: 6/6
c ---[1600]---> Adder-cost: 142   maxlim: 74   bits: 7/7
c ---[1598]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1596]---> Adder-cost: 34   maxlim: 30   bits: 5/5
c ---[1594]---> Adder-cost: 136   maxlim: 75   bits: 7/7
c ---[1592]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1590]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1588]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1586]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1584]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[1582]---> Adder-cost: 70   maxlim: 42   bits: 6/6
c ---[1580]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1578]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1576]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1574]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1572]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[1570]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[1566]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1564]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1562]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[1560]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[1558]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[1556]---> Adder-cost: 294   maxlim: 154   bits: 8/8
c ---[1554]---> Adder-cost: 230   maxlim: 150   bits: 8/8
c ---[1552]---> Adder-cost: 152   maxlim: 90   bits: 7/7
c ---[1550]---> Adder-cost: 110   maxlim: 66   bits: 7/7
c ---[1548]---> Adder-cost: 76   maxlim: 45   bits: 6/6
c ---[1546]---> Adder-cost: 60   maxlim: 48   bits: 6/6
c ---[1544]---> Adder-cost: 54   maxlim: 33   bits: 6/6
c ---[1542]---> Adder-cost: 148   maxlim: 80   bits: 7/7
c ---[1540]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[1538]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1536]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[1534]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[1532]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[1530]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1528]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[1526]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1524]---> Adder-cost: 42   maxlim: 24   bits: 5/5
c ---[1522]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1520]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1518]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[1516]---> Adder-cost: 254   maxlim: 127   bits: 8/7
c ---[1514]---> Adder-cost: 182   maxlim: 98   bits: 7/7
c ---[1512]---> Adder-cost: 140   maxlim: 106   bits: 7/7
c ---[1510]---> Adder-cost: 172   maxlim: 128   bits: 8/8
c ---[1508]---> Adder-cost: 58   maxlim: 37   bits: 6/6
c ---[1506]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[1504]---> Adder-cost: 348   maxlim: 179   bits: 8/8
c ---[1502]---> Adder-cost: 332   maxlim: 197   bits: 8/8
c ---[1500]---> Adder-cost: 348   maxlim: 181   bits: 8/8
c ---[1498]---> Adder-cost: 192   maxlim: 130   bits: 8/8
c ---[1496]---> Adder-cost: 260   maxlim: 132   bits: 8/8
c ---[1494]---> Adder-cost: 262   maxlim: 149   bits: 8/8
c ---[1492]---> Adder-cost: 66   maxlim: 46   bits: 6/6
c ---[1488]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1486]---> Adder-cost: 16   maxlim: 11   bits: 4/4
c ---[1484]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1478]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1476]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1474]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1472]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1470]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1468]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1466]---> Adder-cost: 96   maxlim: 52   bits: 6/6
c ---[1464]---> Adder-cost: 196   maxlim: 102   bits: 7/7
c ---[1462]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1460]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1458]---> Adder-cost: 20   maxlim: 26   bits: 5/5
c ---[1456]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1452]---> Adder-cost: 46   maxlim: 28   bits: 5/5
c ---[1450]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1448]---> Adder-cost: 88   maxlim: 51   bits: 6/6
c ---[1446]---> Adder-cost: 98   maxlim: 53   bits: 6/6
c ---[1444]---> Adder-cost: 98   maxlim: 62   bits: 6/6
c ---[1442]---> Adder-cost: 64   maxlim: 40   bits: 6/6
c ---[1440]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1438]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[1436]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1434]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1428]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[1426]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1424]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[1422]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[1420]---> Adder-cost: 188   maxlim: 98   bits: 7/7
c ---[1418]---> Adder-cost: 168   maxlim: 99   bits: 7/7
c ---[1416]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[1414]---> Adder-cost: 162   maxlim: 88   bits: 7/7
c ---[1412]---> Adder-cost: 170   maxlim: 89   bits: 7/7
c ---[1410]---> Adder-cost: 156   maxlim: 100   bits: 7/7
c ---[1408]---> Adder-cost: 112   maxlim: 80   bits: 7/7
c ---[1406]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1404]---> Adder-cost: 256   maxlim: 129   bits: 8/8
c ---[1402]---> Adder-cost: 244   maxlim: 147   bits: 8/8
c ---[1400]---> Adder-cost: 164   maxlim: 88   bits: 7/7
c ---[1398]---> Adder-cost: 106   maxlim: 65   bits: 7/7
c ---[1396]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[1394]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[1392]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[1390]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1386]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[1384]---> Adder-cost: 26   maxlim: 22   bits: 5/5
c ---[1382]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1380]---> Adder-cost: 46   maxlim: 29   bits: 5/5
c ---[1378]---> Adder-cost: 164   maxlim: 85   bits: 7/7
c ---[1376]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[1374]---> Adder-cost: 84   maxlim: 48   bits: 6/6
c ---[1372]---> Adder-cost: 214   maxlim: 112   bits: 7/7
c ---[1370]---> Adder-cost: 246   maxlim: 138   bits: 8/8
c ---[1368]---> Adder-cost: 106   maxlim: 57   bits: 6/6
c ---[1366]---> Adder-cost: 54   maxlim: 56   bits: 6/6
c ---[1364]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[1362]---> Adder-cost: 380   maxlim: 195   bits: 8/8
c ---[1360]---> Adder-cost: 300   maxlim: 196   bits: 8/8
c ---[1358]---> Adder-cost: 172   maxlim: 96   bits: 7/7
c ---[1356]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[1354]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1352]---> Adder-cost: 78   maxlim: 50   bits: 6/6
c ---[1350]---> Adder-cost: 192   maxlim: 101   bits: 7/7
c ---[1348]---> Adder-cost: 88   maxlim: 104   bits: 7/7
c ---[1346]---> Adder-cost: 94   maxlim: 58   bits: 6/6
c ---[1344]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1342]---> Adder-cost: 172   maxlim: 92   bits: 7/7
c ---[1340]---> Adder-cost: 126   maxlim: 68   bits: 7/7
c ---[1338]---> Adder-cost: 66   maxlim: 44   bits: 6/6
c ---[1336]---> Adder-cost: 54   maxlim: 47   bits: 6/6
c ---[1334]---> Adder-cost: 122   maxlim: 71   bits: 7/7
c ---[1332]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[1330]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[1328]---> Adder-cost: 26   maxlim: 22   bits: 5/5
c ---[1326]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[1324]---> Adder-cost: 122   maxlim: 65   bits: 7/7
c ---[1322]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[1320]---> Adder-cost: 270   maxlim: 137   bits: 8/8
c ---[1318]---> Adder-cost: 256   maxlim: 139   bits: 8/8
c ---[1316]---> Adder-cost: 82   maxlim: 52   bits: 6/6
c ---[1314]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[1312]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[1310]---> Adder-cost: 42   maxlim: 25   bits: 5/5
c ---[1308]---> Adder-cost: 60   maxlim: 34   bits: 6/6
c ---[1306]---> Adder-cost: 88   maxlim: 50   bits: 6/6
c ---[1304]---> Adder-cost: 72   maxlim: 48   bits: 6/6
c ---[1302]---> Adder-cost: 160   maxlim: 83   bits: 7/7
c ---[1300]---> Adder-cost: 228   maxlim: 119   bits: 7/7
c ---[1298]---> Adder-cost: 96   maxlim: 62   bits: 6/6
c ---[1296]---> Adder-cost: 110   maxlim: 69   bits: 7/7
c ---[1294]---> Adder-cost: 218   maxlim: 116   bits: 7/7
c ---[1292]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[1290]---> Adder-cost: 58   maxlim: 31   bits: 6/5
c ---[1288]---> Adder-cost: 134   maxlim: 90   bits: 7/7
c ---[1286]---> Adder-cost: 128   maxlim: 68   bits: 7/7
c ---[1284]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[1282]---> Adder-cost: 166   maxlim: 89   bits: 7/7
c ---[1280]---> Adder-cost: 142   maxlim: 78   bits: 7/7
c ---[1278]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1276]---> Adder-cost: 174   maxlim: 91   bits: 7/7
c ---[1274]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[1272]---> Adder-cost: 162   maxlim: 84   bits: 7/7
c ---[1270]---> Adder-cost: 132   maxlim: 74   bits: 7/7
c ---[1268]---> Adder-cost: 166   maxlim: 108   bits: 7/7
c ---[1266]---> Adder-cost: 230   maxlim: 122   bits: 7/7
c ---[1264]---> Adder-cost: 122   maxlim: 120   bits: 7/7
c ---[1262]---> Adder-cost: 142   maxlim: 82   bits: 7/7
c ---[1260]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[1258]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1254]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[1252]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1250]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[1248]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1246]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[1244]---> Adder-cost: 78   maxlim: 49   bits: 6/6
c ---[1242]---> Adder-cost: 62   maxlim: 35   bits: 6/6
c ---[1240]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1238]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[1236]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[1234]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[1232]---> Adder-cost: 92   maxlim: 53   bits: 6/6
c ---[1230]---> Adder-cost: 72   maxlim: 42   bits: 6/6
c ---[1228]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1226]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1224]---> Adder-cost: 10   maxlim: 7   bits: 4/3
c ---[1222]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[1220]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[1218]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[1216]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[1214]---> Adder-cost: 38   maxlim: 26   bits: 5/5
c ---[1212]---> Adder-cost: 54   maxlim: 34   bits: 6/6
c ---[1210]---> Adder-cost: 84   maxlim: 47   bits: 6/6
c ---[1208]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[1206]---> Adder-cost: 94   maxlim: 51   bits: 6/6
c ---[1204]---> Adder-cost: 74   maxlim: 47   bits: 6/6
c ---[1202]---> Adder-cost: 92   maxlim: 54   bits: 6/6
c ---[1200]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[1198]---> Adder-cost: 106   maxlim: 60   bits: 6/6
c ---[1196]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1194]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[1192]---> Adder-cost: 46   maxlim: 31   bits: 6/5
c ---[1190]---> Adder-cost: 268   maxlim: 137   bits: 8/8
c ---[1188]---> Adder-cost: 232   maxlim: 131   bits: 8/8
c ---[1186]---> Adder-cost: 232   maxlim: 122   bits: 7/7
c ---[1184]---> Adder-cost: 150   maxlim: 100   bits: 7/7
c ---[1182]---> Adder-cost: 274   maxlim: 148   bits: 8/8
c ---[1180]---> Adder-cost: 158   maxlim: 90   bits: 7/7
c ---[1178]---> Adder-cost: 102   maxlim: 59   bits: 6/6
c ---[1176]---> Adder-cost: 162   maxlim: 88   bits: 7/7
c ---[1174]---> Adder-cost: 248   maxlim: 128   bits: 8/8
c ---[1172]---> Adder-cost: 242   maxlim: 129   bits: 8/8
c ---[1170]---> Adder-cost: 114   maxlim: 64   bits: 7/7
c ---[1168]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[1166]---> Adder-cost: 46   maxlim: 43   bits: 6/6
c ---[1164]---> Adder-cost: 66   maxlim: 41   bits: 6/6
c ---[1162]---> Adder-cost: 68   maxlim: 40   bits: 6/6
c ---[1160]---> Adder-cost: 46   maxlim: 27   bits: 5/5
c ---[1156]---> Adder-cost: 58   maxlim: 37   bits: 6/6
c ---[1154]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1152]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1150]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[1148]---> Adder-cost: 10   maxlim: 13   bits: 4/4
c ---[1146]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[1144]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1142]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[1140]---> Adder-cost: 22   maxlim: 16   bits: 5/5
c ---[1138]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[1136]---> Adder-cost: 86   maxlim: 48   bits: 6/6
c ---[1134]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[1132]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[1130]---> Adder-cost: 266   maxlim: 137   bits: 8/8
c ---[1128]---> Adder-cost: 218   maxlim: 111   bits: 7/7
c ---[1126]---> Adder-cost: 182   maxlim: 101   bits: 7/7
c ---[1124]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[1122]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[1120]---> Adder-cost: 164   maxlim: 94   bits: 7/7
c ---[1118]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1116]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[1114]---> Adder-cost: 44   maxlim: 34   bits: 6/6
c ---[1112]---> Adder-cost: 110   maxlim: 65   bits: 7/7
c ---[1110]---> Adder-cost: 124   maxlim: 68   bits: 7/7
c ---[1108]---> Adder-cost: 92   maxlim: 62   bits: 6/6
c ---[1096]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[1094]---> Adder-cost: 86   maxlim: 48   bits: 6/6
c ---[1092]---> Adder-cost: 70   maxlim: 47   bits: 6/6
c ---[1090]---> Adder-cost: 110   maxlim: 66   bits: 7/7
c ---[1088]---> Adder-cost: 94   maxlim: 59   bits: 6/6
c ---[1086]---> Adder-cost: 190   maxlim: 101   bits: 7/7
c ---[1084]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[1082]---> Adder-cost: 84   maxlim: 101   bits: 7/7
c ---[1080]---> Adder-cost: 170   maxlim: 88   bits: 7/7
c ---[1078]---> Adder-cost: 42   maxlim: 23   bits: 5/5
c ---[1074]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[1072]---> Adder-cost: 210   maxlim: 110   bits: 7/7
c ---[1070]---> Adder-cost: 162   maxlim: 84   bits: 7/7
c ---[1068]---> Adder-cost: 122   maxlim: 77   bits: 7/7
c ---[1066]---> Adder-cost: 204   maxlim: 112   bits: 7/7
c ---[1064]---> Adder-cost: 18   maxlim: 14   bits: 4/4
c ---[1062]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1060]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[1058]---> Adder-cost: 116   maxlim: 65   bits: 7/7
c ---[1056]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[1054]---> Adder-cost: 230   maxlim: 126   bits: 7/7
c ---[1052]---> Adder-cost: 148   maxlim: 89   bits: 7/7
c ---[1048]---> Adder-cost: 84   maxlim: 49   bits: 6/6
c ---[1044]---> Adder-cost: 138   maxlim: 71   bits: 7/7
c ---[1042]---> Adder-cost: 92   maxlim: 57   bits: 6/6
c ---[1040]---> Adder-cost: 170   maxlim: 87   bits: 7/7
c ---[1038]---> Adder-cost: 202   maxlim: 111   bits: 7/7
c ---[1036]---> Adder-cost: 184   maxlim: 100   bits: 7/7
c ---[1034]---> Adder-cost: 146   maxlim: 97   bits: 7/7
c ---[1032]---> Adder-cost: 254   maxlim: 130   bits: 8/8
c ---[1030]---> Adder-cost: 198   maxlim: 135   bits: 8/8
c ---[1028]---> Adder-cost: 270   maxlim: 143   bits: 8/8
c ---[1026]---> Adder-cost: 188   maxlim: 103   bits: 7/7
c ---[1024]---> Adder-cost: 176   maxlim: 102   bits: 7/7
c ---[1022]---> Adder-cost: 192   maxlim: 112   bits: 7/7
c ---[1018]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[1014]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1012]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[1010]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1008]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1004]---> Adder-cost: 16   maxlim: 22   bits: 5/5
c ---[1002]---> Adder-cost: 64   maxlim: 36   bits: 6/6
c ---[1000]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[ 998]---> Adder-cost: 130   maxlim: 69   bits: 7/7
c ---[ 996]---> Adder-cost: 116   maxlim: 79   bits: 7/7
c ---[ 994]---> Adder-cost: 122   maxlim: 63   bits: 7/6
c ---[ 992]---> Adder-cost: 80   maxlim: 62   bits: 6/6
c ---[ 990]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[ 988]---> Adder-cost: 102   maxlim: 63   bits: 7/6
c ---[ 986]---> Adder-cost: 108   maxlim: 65   bits: 7/7
c ---[ 984]---> Adder-cost: 106   maxlim: 63   bits: 7/6
c ---[ 982]---> Adder-cost: 122   maxlim: 64   bits: 7/7
c ---[ 980]---> Adder-cost: 76   maxlim: 66   bits: 7/7
c ---[ 978]---> Adder-cost: 124   maxlim: 70   bits: 7/7
c ---[ 976]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 974]---> Adder-cost: 98   maxlim: 57   bits: 6/6
c ---[ 972]---> Adder-cost: 74   maxlim: 39   bits: 6/6
c ---[ 970]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 968]---> Adder-cost: 52   maxlim: 32   bits: 6/6
c ---[ 966]---> Adder-cost: 48   maxlim: 32   bits: 6/6
c ---[ 962]---> Adder-cost: 60   maxlim: 35   bits: 6/6
c ---[ 960]---> Adder-cost: 60   maxlim: 38   bits: 6/6
c ---[ 958]---> Adder-cost: 202   maxlim: 107   bits: 7/7
c ---[ 956]---> Adder-cost: 230   maxlim: 124   bits: 7/7
c ---[ 954]---> Adder-cost: 230   maxlim: 137   bits: 8/8
c ---[ 952]---> Adder-cost: 144   maxlim: 81   bits: 7/7
c ---[ 950]---> Adder-cost: 516   maxlim: 268   bits: 9/9
c ---[ 948]---> Adder-cost: 618   maxlim: 330   bits: 9/9
c ---[ 946]---> Adder-cost: 248   maxlim: 130   bits: 8/8
c ---[ 944]---> Adder-cost: 182   maxlim: 107   bits: 7/7
c ---[ 942]---> Adder-cost: 142   maxlim: 86   bits: 7/7
c ---[ 940]---> Adder-cost: 104   maxlim: 76   bits: 7/7
c ---[ 938]---> Adder-cost: 512   maxlim: 282   bits: 9/9
c ---[ 936]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 932]---> Adder-cost: 142   maxlim: 78   bits: 7/7
c ---[ 930]---> Adder-cost: 110   maxlim: 64   bits: 7/7
c ---[ 928]---> Adder-cost: 98   maxlim: 60   bits: 6/6
c ---[ 926]---> Adder-cost: 94   maxlim: 62   bits: 6/6
c ---[ 922]---> Adder-cost: 52   maxlim: 65   bits: 7/7
c ---[ 920]---> Adder-cost: 116   maxlim: 72   bits: 7/7
c ---[ 918]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[ 914]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 912]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 910]---> Adder-cost: 60   maxlim: 38   bits: 6/6
c ---[ 908]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 906]---> Adder-cost: 130   maxlim: 75   bits: 7/7
c ---[ 904]---> Adder-cost: 94   maxlim: 52   bits: 6/6
c ---[ 902]---> Adder-cost: 84   maxlim: 51   bits: 6/6
c ---[ 900]---> Adder-cost: 70   maxlim: 40   bits: 6/6
c ---[ 898]---> Adder-cost: 322   maxlim: 167   bits: 8/8
c ---[ 896]---> Adder-cost: 134   maxlim: 167   bits: 8/8
c ---[ 894]---> Adder-cost: 378   maxlim: 204   bits: 8/8
c ---[ 892]---> Adder-cost: 372   maxlim: 201   bits: 8/8
c ---[ 890]---> Adder-cost: 328   maxlim: 176   bits: 8/8
c ---[ 888]---> Adder-cost: 198   maxlim: 161   bits: 8/8
c ---[ 886]---> Adder-cost: 212   maxlim: 114   bits: 7/7
c ---[ 884]---> Adder-cost: 102   maxlim: 58   bits: 6/6
c ---[ 882]---> Adder-cost: 102   maxlim: 65   bits: 7/7
c ---[ 880]---> Adder-cost: 80   maxlim: 61   bits: 6/6
c ---[ 878]---> Adder-cost: 116   maxlim: 67   bits: 7/7
c ---[ 876]---> Adder-cost: 212   maxlim: 122   bits: 7/7
c ---[ 874]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[ 872]---> Adder-cost: 216   maxlim: 120   bits: 7/7
c ---[ 870]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 868]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 866]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[ 862]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[ 860]---> Adder-cost: 228   maxlim: 120   bits: 7/7
c ---[ 858]---> Adder-cost: 198   maxlim: 122   bits: 7/7
c ---[ 856]---> Adder-cost: 194   maxlim: 104   bits: 7/7
c ---[ 854]---> Adder-cost: 150   maxlim: 111   bits: 7/7
c ---[ 852]---> Adder-cost: 372   maxlim: 196   bits: 8/8
c ---[ 850]---> Adder-cost: 328   maxlim: 200   bits: 8/8
c ---[ 848]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 846]---> Adder-cost: 68   maxlim: 70   bits: 7/7
c ---[ 844]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 842]---> Adder-cost: 282   maxlim: 156   bits: 8/8
c ---[ 840]---> Adder-cost: 176   maxlim: 94   bits: 7/7
c ---[ 838]---> Adder-cost: 180   maxlim: 104   bits: 7/7
c ---[ 836]---> Adder-cost: 108   maxlim: 59   bits: 6/6
c ---[ 834]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[ 830]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[ 828]---> Adder-cost: 310   maxlim: 168   bits: 8/8
c ---[ 826]---> Adder-cost: 254   maxlim: 161   bits: 8/8
c ---[ 822]---> Adder-cost: 252   maxlim: 127   bits: 8/7
c ---[ 820]---> Adder-cost: 74   maxlim: 39   bits: 6/6
c ---[ 818]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[ 816]---> Adder-cost: 186   maxlim: 96   bits: 7/7
c ---[ 814]---> Adder-cost: 136   maxlim: 77   bits: 7/7
c ---[ 812]---> Adder-cost: 248   maxlim: 128   bits: 8/8
c ---[ 810]---> Adder-cost: 198   maxlim: 134   bits: 8/8
c ---[ 808]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 806]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[ 802]---> Adder-cost: 176   maxlim: 94   bits: 7/7
c ---[ 800]---> Adder-cost: 106   maxlim: 59   bits: 6/6
c ---[ 798]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[ 796]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 794]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[ 792]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 790]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 788]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 786]---> Adder-cost: 60   maxlim: 37   bits: 6/6
c ---[ 784]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[ 782]---> Adder-cost: 72   maxlim: 48   bits: 6/6
c ---[ 780]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[ 778]---> Adder-cost: 80   maxlim: 55   bits: 6/6
c ---[ 776]---> Adder-cost: 328   maxlim: 173   bits: 8/8
c ---[ 774]---> Adder-cost: 256   maxlim: 151   bits: 8/8
c ---[ 772]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 770]---> Adder-cost: 58   maxlim: 49   bits: 6/6
c ---[ 768]---> Adder-cost: 64   maxlim: 36   bits: 6/6
c ---[ 766]---> Adder-cost: 74   maxlim: 40   bits: 6/6
c ---[ 764]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[ 762]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 760]---> Adder-cost: 194   maxlim: 100   bits: 7/7
c ---[ 758]---> Adder-cost: 180   maxlim: 98   bits: 7/7
c ---[ 756]---> Adder-cost: 142   maxlim: 85   bits: 7/7
c ---[ 754]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 752]---> Adder-cost: 26   maxlim: 20   bits: 5/5
c ---[ 750]---> Adder-cost: 120   maxlim: 67   bits: 7/7
c ---[ 748]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 746]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[ 744]---> Adder-cost: 138   maxlim: 81   bits: 7/7
c ---[ 742]---> Adder-cost: 328   maxlim: 173   bits: 8/8
c ---[ 740]---> Adder-cost: 240   maxlim: 156   bits: 8/8
c ---[ 738]---> Adder-cost: 190   maxlim: 103   bits: 7/7
c ---[ 736]---> Adder-cost: 142   maxlim: 80   bits: 7/7
c ---[ 734]---> Adder-cost: 138   maxlim: 81   bits: 7/7
c ---[ 732]---> Adder-cost: 94   maxlim: 93   bits: 7/7
c ---[ 730]---> Adder-cost: 112   maxlim: 92   bits: 7/7
c ---[ 728]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 726]---> Adder-cost: 152   maxlim: 89   bits: 7/7
c ---[ 724]---> Adder-cost: 286   maxlim: 147   bits: 8/8
c ---[ 722]---> Adder-cost: 244   maxlim: 141   bits: 8/8
c ---[ 720]---> Adder-cost: 194   maxlim: 103   bits: 7/7
c ---[ 718]---> Adder-cost: 162   maxlim: 102   bits: 7/7
c ---[ 716]---> Adder-cost: 276   maxlim: 145   bits: 8/8
c ---[ 714]---> Adder-cost: 152   maxlim: 82   bits: 7/7
c ---[ 712]---> Adder-cost: 172   maxlim: 91   bits: 7/7
c ---[ 710]---> Adder-cost: 124   maxlim: 72   bits: 7/7
c ---[ 708]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 706]---> Adder-cost: 88   maxlim: 62   bits: 6/6
c ---[ 704]---> Adder-cost: 174   maxlim: 97   bits: 7/7
c ---[ 702]---> Adder-cost: 130   maxlim: 70   bits: 7/7
c ---[ 700]---> Adder-cost: 98   maxlim: 69   bits: 7/7
c ---[ 698]---> Adder-cost: 452   maxlim: 240   bits: 8/8
c ---[ 696]---> Adder-cost: 376   maxlim: 231   bits: 8/8
c ---[ 694]---> Adder-cost: 262   maxlim: 146   bits: 8/8
c ---[ 692]---> Adder-cost: 84   maxlim: 146   bits: 8/8
c ---[ 690]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 688]---> Adder-cost: 0   maxlim: 2   bits: 2/2
c ---[ 686]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 684]---> Adder-cost: 4   maxlim: 4   bits: 3/3
c ---[ 680]---> Adder-cost: 146   maxlim: 78   bits: 7/7
c ---[ 678]---> Adder-cost: 122   maxlim: 64   bits: 7/7
c ---[ 676]---> Adder-cost: 112   maxlim: 64   bits: 7/7
c ---[ 674]---> Adder-cost: 264   maxlim: 139   bits: 8/8
c ---[ 672]---> Adder-cost: 60   maxlim: 32   bits: 6/6
c ---[ 670]---> Adder-cost: 42   maxlim: 31   bits: 6/5
c ---[ 668]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 666]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 664]---> Adder-cost: 232   maxlim: 123   bits: 7/7
c ---[ 662]---> Adder-cost: 210   maxlim: 115   bits: 7/7
c ---[ 660]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 658]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 656]---> Adder-cost: 20   maxlim: 21   bits: 5/5
c ---[ 654]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 652]---> Adder-cost: 170   maxlim: 101   bits: 7/7
c ---[ 650]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 648]---> Adder-cost: 88   maxlim: 54   bits: 6/6
c ---[ 646]---> Adder-cost: 224   maxlim: 118   bits: 7/7
c ---[ 644]---> Adder-cost: 224   maxlim: 125   bits: 7/7
c ---[ 642]---> Adder-cost: 224   maxlim: 120   bits: 7/7
c ---[ 640]---> Adder-cost: 244   maxlim: 136   bits: 8/8
c ---[ 638]---> Adder-cost: 588   maxlim: 308   bits: 9/9
c ---[ 636]---> Adder-cost: 480   maxlim: 298   bits: 9/9
c ---[ 634]---> Adder-cost: 224   maxlim: 116   bits: 7/7
c ---[ 632]---> Adder-cost: 170   maxlim: 115   bits: 7/7
c ---[ 630]---> Adder-cost: 524   maxlim: 276   bits: 9/9
c ---[ 628]---> Adder-cost: 428   maxlim: 279   bits: 9/9
c ---[ 626]---> Adder-cost: 332   maxlim: 179   bits: 8/8
c ---[ 624]---> Adder-cost: 246   maxlim: 145   bits: 8/8
c ---[ 620]---> Adder-cost: 306   maxlim: 165   bits: 8/8
c ---[ 618]---> Adder-cost: 248   maxlim: 170   bits: 8/8
c ---[ 616]---> Adder-cost: 236   maxlim: 152   bits: 8/8
c ---[ 614]---> Adder-cost: 194   maxlim: 116   bits: 7/7
c ---[ 612]---> Adder-cost: 164   maxlim: 109   bits: 7/7
c ---[ 610]---> Adder-cost: 260   maxlim: 162   bits: 8/8
c ---[ 608]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[ 606]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 604]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 602]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 600]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 598]---> Adder-cost: 114   maxlim: 68   bits: 7/7
c ---[ 596]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[ 594]---> Adder-cost: 86   maxlim: 55   bits: 6/6
c ---[ 592]---> Adder-cost: 42   maxlim: 27   bits: 5/5
c ---[ 590]---> Adder-cost: 184   maxlim: 97   bits: 7/7
c ---[ 588]---> Adder-cost: 558   maxlim: 287   bits: 9/9
c ---[ 586]---> Adder-cost: 408   maxlim: 288   bits: 9/9
c ---[ 584]---> Adder-cost: 594   maxlim: 305   bits: 9/9
c ---[ 582]---> Adder-cost: 460   maxlim: 293   bits: 9/9
c ---[ 580]---> Adder-cost: 204   maxlim: 107   bits: 7/7
c ---[ 578]---> Adder-cost: 190   maxlim: 110   bits: 7/7
c ---[ 576]---> Adder-cost: 162   maxlim: 87   bits: 7/7
c ---[ 574]---> Adder-cost: 88   maxlim: 89   bits: 7/7
c ---[ 572]---> Adder-cost: 274   maxlim: 144   bits: 8/8
c ---[ 570]---> Adder-cost: 262   maxlim: 140   bits: 8/8
c ---[ 568]---> Adder-cost: 126   maxlim: 63   bits: 7/6
c ---[ 566]---> Adder-cost: 72   maxlim: 46   bits: 6/6
c ---[ 564]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[ 562]---> Adder-cost: 376   maxlim: 203   bits: 8/8
c ---[ 560]---> Adder-cost: 360   maxlim: 215   bits: 8/8
c ---[ 558]---> Adder-cost: 166   maxlim: 88   bits: 7/7
c ---[ 556]---> Adder-cost: 140   maxlim: 88   bits: 7/7
c ---[ 554]---> Adder-cost: 134   maxlim: 81   bits: 7/7
c ---[ 552]---> Adder-cost: 118   maxlim: 76   bits: 7/7
c ---[ 550]---> Adder-cost: 130   maxlim: 81   bits: 7/7
c ---[ 548]---> Adder-cost: 134   maxlim: 83   bits: 7/7
c ---[ 546]---> Adder-cost: 134   maxlim: 81   bits: 7/7
c ---[ 544]---> Adder-cost: 118   maxlim: 69   bits: 7/7
c ---[ 542]---> Adder-cost: 102   maxlim: 70   bits: 7/7
c ---[ 540]---> Adder-cost: 148   maxlim: 88   bits: 7/7
c ---[ 538]---> Adder-cost: 100   maxlim: 89   bits: 7/7
c ---[ 536]---> Adder-cost: 138   maxlim: 75   bits: 7/7
c ---[ 534]---> Adder-cost: 144   maxlim: 78   bits: 7/7
c ---[ 532]---> Adder-cost: 146   maxlim: 87   bits: 7/7
c ---[ 530]---> Adder-cost: 260   maxlim: 134   bits: 8/8
c ---[ 528]---> Adder-cost: 154   maxlim: 84   bits: 7/7
c ---[ 526]---> Adder-cost: 110   maxlim: 77   bits: 7/7
c ---[ 524]---> Adder-cost: 242   maxlim: 130   bits: 8/8
c ---[ 522]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 520]---> Adder-cost: 106   maxlim: 61   bits: 6/6
c ---[ 518]---> Adder-cost: 306   maxlim: 162   bits: 8/8
c ---[ 516]---> Adder-cost: 310   maxlim: 163   bits: 8/8
c ---[ 514]---> Adder-cost: 292   maxlim: 156   bits: 8/8
c ---[ 512]---> Adder-cost: 288   maxlim: 157   bits: 8/8
c ---[ 510]---> Adder-cost: 236   maxlim: 167   bits: 8/8
c ---[ 508]---> Adder-cost: 262   maxlim: 149   bits: 8/8
c ---[ 506]---> Adder-cost: 220   maxlim: 158   bits: 8/8
c ---[ 504]---> Adder-cost: 354   maxlim: 185   bits: 8/8
c ---[ 500]---> Adder-cost: 260   maxlim: 158   bits: 8/8
c ---[ 498]---> Adder-cost: 262   maxlim: 179   bits: 8/8
c ---[ 496]---> Adder-cost: 264   maxlim: 143   bits: 8/8
c ---[ 494]---> Adder-cost: 124   maxlim: 116   bits: 7/7
c ---[ 492]---> Adder-cost: 302   maxlim: 159   bits: 8/8
c ---[ 490]---> Adder-cost: 258   maxlim: 152   bits: 8/8
c ---[ 488]---> Adder-cost: 412   maxlim: 213   bits: 8/8
c ---[ 486]---> Adder-cost: 320   maxlim: 204   bits: 8/8
c ---[ 484]---> Adder-cost: 288   maxlim: 155   bits: 8/8
c ---[ 482]---> Adder-cost: 294   maxlim: 165   bits: 8/8
c ---[ 480]---> Adder-cost: 262   maxlim: 154   bits: 8/8
c ---[ 478]---> Adder-cost: 278   maxlim: 158   bits: 8/8
c ---[ 476]---> Adder-cost: 280   maxlim: 149   bits: 8/8
c ---[ 474]---> Adder-cost: 276   maxlim: 154   bits: 8/8
c ---[ 472]---> Adder-cost: 672   maxlim: 364   bits: 9/9
c ---[ 470]---> Adder-cost: 266   maxlim: 145   bits: 8/8
c ---[ 468]---> Adder-cost: 226   maxlim: 138   bits: 8/8
c ---[ 466]---> Adder-cost: 376   maxlim: 193   bits: 8/8
c ---[ 464]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 462]---> Adder-cost: 186   maxlim: 190   bits: 8/8
c ---[ 458]---> Adder-cost: 138   maxlim: 73   bits: 7/7
c ---[ 456]---> Adder-cost: 118   maxlim: 74   bits: 7/7
c ---[ 454]---> Adder-cost: 140   maxlim: 75   bits: 7/7
c ---[ 452]---> Adder-cost: 116   maxlim: 72   bits: 7/7
c ---[ 450]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[ 448]---> Adder-cost: 110   maxlim: 72   bits: 7/7
c ---[ 446]---> Adder-cost: 300   maxlim: 162   bits: 8/8
c ---[ 444]---> Adder-cost: 300   maxlim: 170   bits: 8/8
c ---[ 438]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 436]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 434]---> Adder-cost: 372   maxlim: 200   bits: 8/8
c ---[ 432]---> Adder-cost: 378   maxlim: 201   bits: 8/8
c ---[ 430]---> Adder-cost: 310   maxlim: 202   bits: 8/8
c ---[ 426]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 422]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 418]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 416]---> Adder-cost: 444   maxlim: 227   bits: 8/8
c ---[ 414]---> Adder-cost: 442   maxlim: 233   bits: 8/8
c ---[ 412]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[ 410]---> Adder-cost: 142   maxlim: 89   bits: 7/7
c ---[ 408]---> Adder-cost: 170   maxlim: 107   bits: 7/7
c ---[ 404]---> Adder-cost: 318   maxlim: 174   bits: 8/8
c ---[ 402]---> Adder-cost: 178   maxlim: 109   bits: 7/7
c ---[ 400]---> Adder-cost: 190   maxlim: 111   bits: 7/7
c ---[ 398]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[ 396]---> Adder-cost: 14   maxlim: 10   bits: 4/4
c ---[ 394]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 392]---> Adder-cost: 12   maxlim: 8   bits: 4/4
c ---[ 390]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 388]---> Adder-cost: 208   maxlim: 115   bits: 7/7
c ---[ 386]---> Adder-cost: 200   maxlim: 126   bits: 7/7
c ---[ 384]---> Adder-cost: 216   maxlim: 127   bits: 8/7
c ---[ 378]---> Adder-cost: 310   maxlim: 160   bits: 8/8
c ---[ 376]---> Adder-cost: 210   maxlim: 112   bits: 7/7
c ---[ 374]---> Adder-cost: 212   maxlim: 121   bits: 7/7
c ---[ 372]---> Adder-cost: 232   maxlim: 123   bits: 7/7
c ---[ 370]---> Adder-cost: 198   maxlim: 129   bits: 8/8
c ---[ 368]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 366]---> Adder-cost: 82   maxlim: 54   bits: 6/6
c ---[ 364]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[ 362]---> Adder-cost: 88   maxlim: 55   bits: 6/6
c ---[ 360]---> Adder-cost: 96   maxlim: 52   bits: 6/6
c ---[ 358]---> Adder-cost: 54   maxlim: 53   bits: 6/6
c ---[ 356]---> Adder-cost: 186   maxlim: 102   bits: 7/7
c ---[ 354]---> Adder-cost: 186   maxlim: 109   bits: 7/7
c ---[ 352]---> Adder-cost: 168   maxlim: 100   bits: 7/7
c ---[ 348]---> Adder-cost: 134   maxlim: 70   bits: 7/7
c ---[ 344]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 340]---> Adder-cost: 124   maxlim: 63   bits: 7/6
c ---[ 338]---> Adder-cost: 214   maxlim: 113   bits: 7/7
c ---[ 336]---> Adder-cost: 198   maxlim: 111   bits: 7/7
c ---[ 334]---> Adder-cost: 122   maxlim: 94   bits: 7/7
c ---[ 332]---> Adder-cost: 230   maxlim: 122   bits: 7/7
c ---[ 330]---> Adder-cost: 206   maxlim: 121   bits: 7/7
c ---[ 328]---> Adder-cost: 194   maxlim: 104   bits: 7/7
c ---[ 326]---> Adder-cost: 136   maxlim: 73   bits: 7/7
c ---[ 324]---> Adder-cost: 82   maxlim: 72   bits: 7/7
c ---[ 322]---> Adder-cost: 218   maxlim: 119   bits: 7/7
c ---[ 320]---> Adder-cost: 192   maxlim: 105   bits: 7/7
c ---[ 318]---> Adder-cost: 92   maxlim: 68   bits: 7/7
c ---[ 316]---> Adder-cost: 210   maxlim: 112   bits: 7/7
c ---[ 314]---> Adder-cost: 200   maxlim: 113   bits: 7/7
c ---[ 312]---> Adder-cost: 166   maxlim: 87   bits: 7/7
c ---[ 310]---> Adder-cost: 96   maxlim: 76   bits: 7/7
c ---[ 308]---> Adder-cost: 110   maxlim: 77   bits: 7/7
c ---[ 306]---> Adder-cost: 76   maxlim: 44   bits: 6/6
c ---[ 304]---> Adder-cost: 52   maxlim: 37   bits: 6/6
c ---[ 302]---> Adder-cost: 132   maxlim: 68   bits: 7/7
c ---[ 300]---> Adder-cost: 64   maxlim: 50   bits: 6/6
c ---[ 298]---> Adder-cost: 230   maxlim: 121   bits: 7/7
c ---[ 296]---> Adder-cost: 158   maxlim: 121   bits: 7/7
c ---[ 294]---> Adder-cost: 200   maxlim: 106   bits: 7/7
c ---[ 292]---> Adder-cost: 130   maxlim: 106   bits: 7/7
c ---[ 290]---> Adder-cost: 258   maxlim: 135   bits: 8/8
c ---[ 288]---> Adder-cost: 104   maxlim: 108   bits: 7/7
c ---[ 286]---> Adder-cost: 194   maxlim: 103   bits: 7/7
c ---[ 284]---> Adder-cost: 156   maxlim: 117   bits: 7/7
c ---[ 282]---> Adder-cost: 188   maxlim: 105   bits: 7/7
c ---[ 280]---> Adder-cost: 176   maxlim: 125   bits: 7/7
c ---[ 278]---> Adder-cost: 442   maxlim: 227   bits: 8/8
c ---[ 276]---> Adder-cost: 316   maxlim: 233   bits: 8/8
c ---[ 274]---> Adder-cost: 250   maxlim: 130   bits: 8/8
c ---[ 272]---> Adder-cost: 208   maxlim: 144   bits: 8/8
c ---[ 270]---> Adder-cost: 334   maxlim: 180   bits: 8/8
c ---[ 268]---> Adder-cost: 250   maxlim: 187   bits: 8/8
c ---[ 266]---> Adder-cost: 308   maxlim: 160   bits: 8/8
c ---[ 264]---> Adder-cost: 282   maxlim: 159   bits: 8/8
c ---[ 262]---> Adder-cost: 206   maxlim: 113   bits: 7/7
c ---[ 260]---> Adder-cost: 218   maxlim: 114   bits: 7/7
c ---[ 258]---> Adder-cost: 416   maxlim: 223   bits: 8/8
c ---[ 256]---> Adder-cost: 364   maxlim: 222   bits: 8/8
c ---[ 254]---> Adder-cost: 282   maxlim: 176   bits: 8/8
c ---[ 252]---> Adder-cost: 98   maxlim: 55   bits: 6/6
c ---[ 250]---> Adder-cost: 112   maxlim: 80   bits: 7/7
c ---[ 248]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[ 246]---> Adder-cost: 94   maxlim: 60   bits: 6/6
c ---[ 242]---> Adder-cost: 560   maxlim: 299   bits: 9/9
c ---[ 240]---> Adder-cost: 286   maxlim: 152   bits: 8/8
c ---[ 238]---> Adder-cost: 244   maxlim: 149   bits: 8/8
c ---[ 236]---> Adder-cost: 122   maxlim: 67   bits: 7/7
c ---[ 234]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[ 232]---> Adder-cost: 120   maxlim: 75   bits: 7/7
c ---[ 230]---> Adder-cost: 110   maxlim: 60   bits: 6/6
c ---[ 228]---> Adder-cost: 64   maxlim: 51   bits: 6/6
c ---[ 226]---> Adder-cost: 132   maxlim: 73   bits: 7/7
c ---[ 224]---> Adder-cost: 122   maxlim: 80   bits: 7/7
c ---[ 222]---> Adder-cost: 208   maxlim: 109   bits: 7/7
c ---[ 220]---> Adder-cost: 186   maxlim: 106   bits: 7/7
c ---[ 218]---> Adder-cost: 122   maxlim: 103   bits: 7/7
c ---[ 214]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[ 212]---> Adder-cost: 180   maxlim: 96   bits: 7/7
c ---[ 210]---> Adder-cost: 148   maxlim: 94   bits: 7/7
c ---[ 208]---> Adder-cost: 144   maxlim: 97   bits: 7/7
c ---[ 206]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[ 204]---> Adder-cost: 94   maxlim: 73   bits: 7/7
c ---[ 202]---> Adder-cost: 382   maxlim: 195   bits: 8/8
c ---[ 200]---> Adder-cost: 366   maxlim: 196   bits: 8/8
c ---[ 198]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[ 196]---> Adder-cost: 134   maxlim: 76   bits: 7/7
c ---[ 194]---> Adder-cost: 280   maxlim: 154   bits: 8/8
c ---[ 192]---> Adder-cost: 314   maxlim: 196   bits: 8/8
c ---[ 190]---> Adder-cost: 250   maxlim: 153   bits: 8/8
c ---[ 188]---> Adder-cost: 220   maxlim: 142   bits: 8/8
c ---[ 186]---> Adder-cost: 258   maxlim: 164   bits: 8/8
c ---[ 184]---> Adder-cost: 302   maxlim: 191   bits: 8/8
c ---[ 182]---> Adder-cost: 168   maxlim: 94   bits: 7/7
c ---[ 180]---> Adder-cost: 144   maxlim: 93   bits: 7/7
c ---[ 178]---> Adder-cost: 34   maxlim: 19   bits: 5/5
c ---[ 176]---> Adder-cost: 24   maxlim: 18   bits: 5/5
c ---[ 174]---> Adder-cost: 160   maxlim: 87   bits: 7/7
c ---[ 170]---> Adder-cost: 324   maxlim: 170   bits: 8/8
c ---[ 168]---> Adder-cost: 396   maxlim: 216   bits: 8/8
c ---[ 166]---> Adder-cost: 406   maxlim: 222   bits: 8/8
c ---[ 164]---> Adder-cost: 366   maxlim: 234   bits: 8/8
c ---[ 162]---> Adder-cost: 398   maxlim: 257   bits: 9/9
c ---[ 160]---> Adder-cost: 348   maxlim: 193   bits: 8/8
c ---[ 158]---> Adder-cost: 294   maxlim: 197   bits: 8/8
c ---[ 156]---> Adder-cost: 808   maxlim: 456   bits: 9/9
c ---[ 154]---> Adder-cost: 414   maxlim: 220   bits: 8/8
c ---[ 152]---> Adder-cost: 312   maxlim: 189   bits: 8/8
c ---[ 150]---> Adder-cost: 220   maxlim: 120   bits: 7/7
c ---[ 148]---> Adder-cost: 194   maxlim: 125   bits: 7/7
c ---[ 146]---> Adder-cost: 244   maxlim: 131   bits: 8/8
c ---[ 144]---> Adder-cost: 210   maxlim: 130   bits: 8/8
c ---[ 142]---> Adder-cost: 210   maxlim: 133   bits: 8/8
c ---[ 140]---> Adder-cost: 226   maxlim: 142   bits: 8/8
c ---[ 138]---> Adder-cost: 634   maxlim: 337   bits: 9/9
c ---[ 136]---> Adder-cost: 500   maxlim: 348   bits: 9/9
c ---[ 134]---> Adder-cost: 304   maxlim: 159   bits: 8/8
c ---[ 132]---> Adder-cost: 154   maxlim: 141   bits: 8/8
c ---[ 130]---> Adder-cost: 182   maxlim: 100   bits: 7/7
c ---[ 128]---> Adder-cost: 138   maxlim: 84   bits: 7/7
c ---[ 126]---> Adder-cost: 96   maxlim: 53   bits: 6/6
c ---[ 124]---> Adder-cost: 72   maxlim: 61   bits: 6/6
c ---[ 122]---> Adder-cost: 106   maxlim: 60   bits: 6/6
c ---[ 120]---> Adder-cost: 102   maxlim: 56   bits: 6/6
c ---[ 118]---> Adder-cost: 140   maxlim: 81   bits: 7/7
c ---[ 116]---> Adder-cost: 146   maxlim: 94   bits: 7/7
c ---[ 114]---> Adder-cost: 206   maxlim: 111   bits: 7/7
c ---[ 110]---> Adder-cost: 136   maxlim: 82   bits: 7/7
c ---[ 108]---> Adder-cost: 178   maxlim: 97   bits: 7/7
c ---[ 106]---> Adder-cost: 130   maxlim: 70   bits: 7/7
c ---[ 104]---> Adder-cost: 104   maxlim: 69   bits: 7/7
c ---[ 102]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 100]---> Adder-cost: 86   maxlim: 47   bits: 6/6
c ---[  98]---> Adder-cost: 36   maxlim: 26   bits: 5/5
c ---[  96]---> Adder-cost: 34   maxlim: 27   bits: 5/5
c ---[  94]---> Adder-cost: 50   maxlim: 31   bits: 6/5
c ---[  92]---> Adder-cost: 86   maxlim: 49   bits: 6/6
c ---[  90]---> Adder-cost: 408   maxlim: 216   bits: 8/8
c ---[  88]---> Adder-cost: 228   maxlim: 218   bits: 8/8
c ---[  86]---> Adder-cost: 498   maxlim: 285   bits: 9/9
c ---[  84]---> Adder-cost: 534   maxlim: 308   bits: 9/9
c ---[  82]---> Adder-cost: 328   maxlim: 174   bits: 8/8
c ---[  80]---> Adder-cost: 216   maxlim: 168   bits: 8/8
c ---[  78]---> Adder-cost: 512   maxlim: 263   bits: 9/9
c ---[  76]---> Adder-cost: 512   maxlim: 268   bits: 9/9
c ---[  74]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  72]---> Adder-cost: 44   maxlim: 27   bits: 5/5
c ---[  70]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  68]---> Adder-cost: 42   maxlim: 31   bits: 6/5
c ---[  66]---> Adder-cost: 46   maxlim: 28   bits: 5/5
c ---[  64]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[  62]---> Adder-cost: 66   maxlim: 42   bits: 6/6
c ---[  60]---> Adder-cost: 150   maxlim: 80   bits: 7/7
c ---[  58]---> Adder-cost: 80   maxlim: 77   bits: 7/7
c ---[  56]---> Adder-cost: 188   maxlim: 100   bits: 7/7
c ---[  54]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[  52]---> Adder-cost: 208   maxlim: 113   bits: 7/7
c ---[  50]---> Adder-cost: 174   maxlim: 117   bits: 7/7
c ---[  48]---> Adder-cost: 456   maxlim: 255   bits: 9/8
c ---[  46]---> Adder-cost: 296   maxlim: 161   bits: 8/8
c ---[  44]---> Adder-cost: 300   maxlim: 189   bits: 8/8
c ---[  42]---> Adder-cost: 338   maxlim: 219   bits: 8/8
c ---[  40]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[  38]---> Adder-cost: 142   maxlim: 94   bits: 7/7
c ---[  36]---> Adder-cost: 358   maxlim: 190   bits: 8/8
c ---[  34]---> Adder-cost: 280   maxlim: 208   bits: 8/8
c ---[  32]---> Adder-cost: 60   maxlim: 32   bits: 6/6
c ---[  30]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 30   bits: 5/5
c ---[  26]---> Adder-cost: 30   maxlim: 20   bits: 5/5
c ---[  24]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[  22]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[  20]---> Adder-cost: 34   maxlim: 19   bits: 5/5
c ---[  18]---> Adder-cost: 52   maxlim: 37   bits: 6/6
c ---[  16]---> Adder-cost: 134   maxlim: 73   bits: 7/7
c ---[  14]---> Adder-cost: 78   maxlim: 72   bits: 7/7
c ---[  12]---> Adder-cost: 128   maxlim: 68   bits: 7/7
c ---[  10]---> Adder-cost: 82   maxlim: 50   bits: 6/6
c ---[   8]---> Adder-cost: 72   maxlim: 56   bits: 6/6
c ---[   6]---> Adder-cost: 122   maxlim: 65   bits: 7/7
c ---[   4]---> Adder-cost: 56   maxlim: 58   bits: 6/6
c ---[   2]---> Adder-cost: 104   maxlim: 61   bits: 6/6
c ---[   0]---> Adder-cost: 70   maxlim: 43   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  765675  2724851 |  255225       0        0     nan |  0.000 % |
c |       100 |  765144  2723024 |  280747      42      162     3.9 |  8.564 % |
c |       250 |  764258  2719958 |  308822      85      321     3.8 |  8.686 % |
c |       476 |  762617  2714259 |  339704     128      496     3.9 |  8.909 % |
c |       813 |  760724  2707724 |  373674     267     1038     3.9 |  9.172 % |
c |      1319 |  757964  2698124 |  411042     479     1880     3.9 |  9.548 % |
c |      2078 |  753130  2681308 |  452146     723     2911     4.0 | 10.198 % |
c |      3217 |  747418  2661386 |  497361    1231     5275     4.3 | 10.966 % |
c |      4927 |  739659  2634389 |  547097    2054     9470     4.6 | 11.988 % |
c |      7489 |  731497  2606017 |  601807    3650    18443     5.1 | 13.075 % |
c |     11333 |  722132  2573000 |  661987    6393    34761     5.4 | 14.305 % |
c |     17099 |  707025  2519737 |  728186   10243    59810     5.8 | 16.262 % |
#### 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.91 0.95 0.92 2/54 25357
Raw data (stat): 25357 (runsolver) R 25356 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492070678 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14095 0 0 0 966 32 0 0 25 0 1 0 492070678 59625472 13740 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13740 603 41 0 14516 0
vsize: 58228
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14104 0 0 0 1965 32 0 0 25 0 1 0 492070678 59625472 13749 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13749 603 41 0 14516 0
vsize: 58228
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14105 0 0 0 2965 32 0 0 25 0 1 0 492070678 59625472 13750 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13750 603 41 0 14516 0
vsize: 58228
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14106 0 0 0 3965 32 0 0 25 0 1 0 492070678 59625472 13751 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13751 603 41 0 14516 0
vsize: 58228
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14106 0 0 0 4965 32 0 0 25 0 1 0 492070678 59625472 13751 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13751 603 41 0 14516 0
vsize: 58228
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14123 0 0 0 5965 32 0 0 25 0 1 0 492070678 59760640 13768 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14590 13768 603 41 0 14549 0
vsize: 58360
[startup+70.0007 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14150 0 0 0 6965 32 0 0 25 0 1 0 492070678 59895808 13795 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14623 13795 603 41 0 14582 0
vsize: 58492
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14179 0 0 0 7965 32 0 0 25 0 1 0 492070678 59895808 13824 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14623 13824 603 41 0 14582 0
vsize: 58492
[startup+90.0006 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14199 0 0 0 8965 32 0 0 25 0 1 0 492070678 60030976 13844 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14656 13844 603 41 0 14615 0
vsize: 58624
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14219 0 0 0 9965 33 0 0 25 0 1 0 492070678 60166144 13864 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14689 13864 603 41 0 14648 0
vsize: 58756
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14254 0 0 0 10965 33 0 0 25 0 1 0 492070678 60301312 13899 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14722 13899 603 41 0 14681 0
vsize: 58888
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14272 0 0 0 11965 33 0 0 25 0 1 0 492070678 60301312 13917 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14722 13917 603 41 0 14681 0
vsize: 58888
[startup+130 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14284 0 0 0 12965 33 0 0 25 0 1 0 492070678 60436480 13929 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14755 13929 603 41 0 14714 0
vsize: 59020
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14309 0 0 0 13965 33 0 0 25 0 1 0 492070678 60579840 13954 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14790 13954 603 41 0 14749 0
vsize: 59160
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14320 0 0 0 14965 33 0 0 25 0 1 0 492070678 60579840 13965 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14790 13965 603 41 0 14749 0
vsize: 59160
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14340 0 0 0 15966 33 0 0 25 0 1 0 492070678 60579840 13985 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14790 13985 603 41 0 14749 0
vsize: 59160
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14354 0 0 0 16966 33 0 0 25 0 1 0 492070678 60715008 13999 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14823 13999 603 41 0 14782 0
vsize: 59292
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14370 0 0 0 17966 33 0 0 25 0 1 0 492070678 60715008 14015 4294967295 134512640 134672761 3221224544 3221223716 134556609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14823 14015 603 41 0 14782 0
vsize: 59292
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14381 0 0 0 18966 33 0 0 25 0 1 0 492070678 60850176 14026 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14856 14026 603 41 0 14815 0
vsize: 59424
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14391 0 0 0 19966 33 0 0 25 0 1 0 492070678 60850176 14036 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14856 14036 603 41 0 14815 0
vsize: 59424
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14405 0 0 0 20966 33 0 0 25 0 1 0 492070678 60850176 14050 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14856 14050 603 41 0 14815 0
vsize: 59424
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14422 0 0 0 21966 34 0 0 25 0 1 0 492070678 60985344 14067 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14889 14067 603 41 0 14848 0
vsize: 59556
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14439 0 0 0 22967 34 0 0 25 0 1 0 492070678 60985344 14084 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14889 14084 603 41 0 14848 0
vsize: 59556
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25357
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14453 0 0 0 23967 34 0 0 25 0 1 0 492070678 61120512 14098 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14922 14098 603 41 0 14881 0
vsize: 59688
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25410
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14467 0 0 0 24964 36 0 0 25 0 1 0 492070678 61120512 14112 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14922 14112 603 41 0 14881 0
vsize: 59688
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25410
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14477 0 0 0 25964 36 0 0 25 0 1 0 492070678 61120512 14122 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14922 14122 603 41 0 14881 0
vsize: 59688
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25410
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14482 0 0 0 26964 36 0 0 25 0 1 0 492070678 61255680 14127 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14955 14127 603 41 0 14914 0
vsize: 59820
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25410
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14490 0 0 0 27964 36 0 0 25 0 1 0 492070678 61255680 14135 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14955 14135 603 41 0 14914 0
vsize: 59820
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25410
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14504 0 0 0 28964 36 0 0 25 0 1 0 492070678 61255680 14149 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14955 14149 603 41 0 14914 0
vsize: 59820
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25410
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14512 0 0 0 29965 36 0 0 25 0 1 0 492070678 61255680 14157 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14955 14157 603 41 0 14914 0
vsize: 59820
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14521 0 0 0 30965 36 0 0 25 0 1 0 492070678 61390848 14166 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14166 603 41 0 14947 0
vsize: 59952
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14527 0 0 0 31965 36 0 0 25 0 1 0 492070678 61390848 14172 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14172 603 41 0 14947 0
vsize: 59952
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14536 0 0 0 32965 36 0 0 25 0 1 0 492070678 61390848 14181 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14181 603 41 0 14947 0
vsize: 59952
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14543 0 0 0 33965 36 0 0 25 0 1 0 492070678 61390848 14188 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14188 603 41 0 14947 0
vsize: 59952
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14551 0 0 0 34965 36 0 0 25 0 1 0 492070678 61390848 14196 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14196 603 41 0 14947 0
vsize: 59952
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14554 0 0 0 35966 36 0 0 25 0 1 0 492070678 61526016 14199 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14199 603 41 0 14980 0
vsize: 60084
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14560 0 0 0 36966 36 0 0 25 0 1 0 492070678 61526016 14205 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14205 603 41 0 14980 0
vsize: 60084
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14566 0 0 0 37966 36 0 0 25 0 1 0 492070678 61526016 14211 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14211 603 41 0 14980 0
vsize: 60084
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14575 0 0 0 38966 36 0 0 25 0 1 0 492070678 61526016 14220 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14220 603 41 0 14980 0
vsize: 60084
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14579 0 0 0 39966 36 0 0 25 0 1 0 492070678 61526016 14224 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14224 603 41 0 14980 0
vsize: 60084
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14585 0 0 0 40966 36 0 0 25 0 1 0 492070678 61526016 14230 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14230 603 41 0 14980 0
vsize: 60084
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14593 0 0 0 41967 36 0 0 25 0 1 0 492070678 61526016 14238 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14238 603 41 0 14980 0
vsize: 60084
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14596 0 0 0 42967 36 0 0 25 0 1 0 492070678 61661184 14241 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14241 603 41 0 15013 0
vsize: 60216
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14597 0 0 0 43967 36 0 0 25 0 1 0 492070678 61661184 14242 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14242 603 41 0 15013 0
vsize: 60216
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14599 0 0 0 44967 36 0 0 25 0 1 0 492070678 61661184 14244 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14244 603 41 0 15013 0
vsize: 60216
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14601 0 0 0 45967 36 0 0 25 0 1 0 492070678 61661184 14246 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14246 603 41 0 15013 0
vsize: 60216
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14603 0 0 0 46967 36 0 0 25 0 1 0 492070678 61661184 14248 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14248 603 41 0 15013 0
vsize: 60216
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14604 0 0 0 47968 36 0 0 25 0 1 0 492070678 61661184 14249 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14249 603 41 0 15013 0
vsize: 60216
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14607 0 0 0 48968 36 0 0 25 0 1 0 492070678 61661184 14252 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14252 603 41 0 15013 0
vsize: 60216
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14608 0 0 0 49968 36 0 0 25 0 1 0 492070678 61661184 14253 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14253 603 41 0 15013 0
vsize: 60216
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14612 0 0 0 50968 36 0 0 25 0 1 0 492070678 61661184 14257 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14257 603 41 0 15013 0
vsize: 60216
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14615 0 0 0 51967 36 0 0 25 0 1 0 492070678 61661184 14260 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14260 603 41 0 15013 0
vsize: 60216
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14615 0 0 0 52968 36 0 0 25 0 1 0 492070678 61661184 14260 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14260 603 41 0 15013 0
vsize: 60216
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14617 0 0 0 53968 36 0 0 25 0 1 0 492070678 61661184 14262 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14262 603 41 0 15013 0
vsize: 60216
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14619 0 0 0 54968 37 0 0 25 0 1 0 492070678 61661184 14264 4294967295 134512640 134672761 3221224544 3221223744 134557959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14264 603 41 0 15013 0
vsize: 60216
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14621 0 0 0 55968 37 0 0 25 0 1 0 492070678 61661184 14266 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14266 603 41 0 15013 0
vsize: 60216
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14625 0 0 0 56968 37 0 0 25 0 1 0 492070678 61661184 14270 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14270 603 41 0 15013 0
vsize: 60216
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14628 0 0 0 57968 37 0 0 25 0 1 0 492070678 61661184 14273 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14273 603 41 0 15013 0
vsize: 60216
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14628 0 0 0 58969 37 0 0 25 0 1 0 492070678 61661184 14273 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14273 603 41 0 15013 0
vsize: 60216
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14629 0 0 0 59969 37 0 0 25 0 1 0 492070678 61661184 14274 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14274 603 41 0 15013 0
vsize: 60216
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25412
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14632 0 0 0 60969 37 0 0 25 0 1 0 492070678 61661184 14277 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14277 603 41 0 15013 0
vsize: 60216
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14633 0 0 0 61969 37 0 0 25 0 1 0 492070678 61661184 14278 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14278 603 41 0 15013 0
vsize: 60216
[startup+630.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14634 0 0 0 62969 37 0 0 25 0 1 0 492070678 61661184 14279 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14279 603 41 0 15013 0
vsize: 60216
[startup+640.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14635 0 0 0 63970 37 0 0 25 0 1 0 492070678 61661184 14280 4294967295 134512640 134672761 3221224544 3221223712 134564682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14280 603 41 0 15013 0
vsize: 60216
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14636 0 0 0 64970 37 0 0 25 0 1 0 492070678 61661184 14281 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14281 603 41 0 15013 0
vsize: 60216
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14638 0 0 0 65970 37 0 0 25 0 1 0 492070678 61661184 14283 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14283 603 41 0 15013 0
vsize: 60216
[startup+670.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14638 0 0 0 66970 37 0 0 25 0 1 0 492070678 61661184 14283 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14283 603 41 0 15013 0
vsize: 60216
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14639 0 0 0 67970 37 0 0 25 0 1 0 492070678 61661184 14284 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14284 603 41 0 15013 0
vsize: 60216
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14640 0 0 0 68969 37 0 0 25 0 1 0 492070678 61661184 14285 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14285 603 41 0 15013 0
vsize: 60216
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14642 0 0 0 69970 37 0 0 25 0 1 0 492070678 61661184 14287 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14287 603 41 0 15013 0
vsize: 60216
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14642 0 0 0 70970 37 0 0 25 0 1 0 492070678 61661184 14287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14287 603 41 0 15013 0
vsize: 60216
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14649 0 0 0 71970 37 0 0 25 0 1 0 492070678 61825024 14294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14294 603 41 0 15053 0
vsize: 60376
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14650 0 0 0 72970 37 0 0 25 0 1 0 492070678 61825024 14295 4294967295 134512640 134672761 3221224544 3221223760 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14295 603 41 0 15053 0
vsize: 60376
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14651 0 0 0 73970 37 0 0 25 0 1 0 492070678 61825024 14296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14651 0 0 0 74971 37 0 0 25 0 1 0 492070678 61825024 14296 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14651 0 0 0 75971 37 0 0 25 0 1 0 492070678 61825024 14296 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14651 0 0 0 76971 37 0 0 25 0 1 0 492070678 61825024 14296 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+780.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14651 0 0 0 77971 37 0 0 25 0 1 0 492070678 61825024 14296 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+790.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14652 0 0 0 78972 37 0 0 25 0 1 0 492070678 61825024 14297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14297 603 41 0 15053 0
vsize: 60376
[startup+800.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14652 0 0 0 79972 37 0 0 25 0 1 0 492070678 61825024 14297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14297 603 41 0 15053 0
vsize: 60376
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14653 0 0 0 80972 37 0 0 25 0 1 0 492070678 61825024 14298 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+820.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14653 0 0 0 81972 37 0 0 25 0 1 0 492070678 61825024 14298 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+830.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14653 0 0 0 82972 37 0 0 25 0 1 0 492070678 61825024 14298 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14653 0 0 0 83972 37 0 0 25 0 1 0 492070678 61825024 14298 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+850.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14653 0 0 0 84973 37 0 0 25 0 1 0 492070678 61825024 14298 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+860.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14654 0 0 0 85973 37 0 0 25 0 1 0 492070678 61825024 14299 4294967295 134512640 134672761 3221224544 3221223708 134564508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14299 603 41 0 15053 0
vsize: 60376
[startup+870.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14654 0 0 0 86973 37 0 0 25 0 1 0 492070678 61825024 14299 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14299 603 41 0 15053 0
vsize: 60376
[startup+880.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14654 0 0 0 87973 37 0 0 25 0 1 0 492070678 61825024 14299 4294967295 134512640 134672761 3221224544 3221223668 134566007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14299 603 41 0 15053 0
vsize: 60376
[startup+890.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14655 0 0 0 88973 37 0 0 25 0 1 0 492070678 61825024 14300 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14655 0 0 0 89973 37 0 0 25 0 1 0 492070678 61825024 14300 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14655 0 0 0 90973 37 0 0 25 0 1 0 492070678 61825024 14300 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14655 0 0 0 91973 37 0 0 25 0 1 0 492070678 61825024 14300 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+930.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14655 0 0 0 92974 37 0 0 25 0 1 0 492070678 61825024 14300 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14656 0 0 0 93974 37 0 0 25 0 1 0 492070678 61825024 14301 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14301 603 41 0 15053 0
vsize: 60376
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14656 0 0 0 94974 37 0 0 25 0 1 0 492070678 61825024 14301 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14301 603 41 0 15053 0
vsize: 60376
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14656 0 0 0 95974 37 0 0 25 0 1 0 492070678 61825024 14301 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14301 603 41 0 15053 0
vsize: 60376
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14658 0 0 0 96974 37 0 0 25 0 1 0 492070678 61825024 14303 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14303 603 41 0 15053 0
vsize: 60376
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14659 0 0 0 97975 37 0 0 25 0 1 0 492070678 61825024 14304 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14304 603 41 0 15053 0
vsize: 60376
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14659 0 0 0 98975 37 0 0 25 0 1 0 492070678 61825024 14304 4294967295 134512640 134672761 3221224544 3221223712 134564467 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14304 603 41 0 15053 0
vsize: 60376
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14659 0 0 0 99975 37 0 0 25 0 1 0 492070678 61825024 14304 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14304 603 41 0 15053 0
vsize: 60376
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14668 0 0 0 100975 37 0 0 25 0 1 0 492070678 61825024 14313 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14313 603 41 0 15053 0
vsize: 60376
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14668 0 0 0 101975 37 0 0 25 0 1 0 492070678 61825024 14313 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14313 603 41 0 15053 0
vsize: 60376
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14671 0 0 0 102976 37 0 0 25 0 1 0 492070678 61825024 14316 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14671 0 0 0 103976 37 0 0 25 0 1 0 492070678 61825024 14316 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14671 0 0 0 104976 37 0 0 25 0 1 0 492070678 61825024 14316 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14671 0 0 0 105976 37 0 0 25 0 1 0 492070678 61825024 14316 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14671 0 0 0 106976 37 0 0 25 0 1 0 492070678 61825024 14316 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14672 0 0 0 107977 37 0 0 25 0 1 0 492070678 61825024 14317 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14317 603 41 0 15053 0
vsize: 60376
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14672 0 0 0 108977 37 0 0 25 0 1 0 492070678 61825024 14317 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14317 603 41 0 15053 0
vsize: 60376
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14673 0 0 0 109977 37 0 0 25 0 1 0 492070678 61825024 14318 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14318 603 41 0 15053 0
vsize: 60376
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14673 0 0 0 110977 37 0 0 25 0 1 0 492070678 61825024 14318 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14318 603 41 0 15053 0
vsize: 60376
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14673 0 0 0 111977 37 0 0 25 0 1 0 492070678 61825024 14318 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14318 603 41 0 15053 0
vsize: 60376
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14674 0 0 0 112978 37 0 0 25 0 1 0 492070678 61825024 14319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14319 603 41 0 15053 0
vsize: 60376
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14674 0 0 0 113977 37 0 0 25 0 1 0 492070678 61825024 14319 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14319 603 41 0 15053 0
vsize: 60376
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14674 0 0 0 114977 37 0 0 25 0 1 0 492070678 61825024 14319 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14319 603 41 0 15053 0
vsize: 60376
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14675 0 0 0 115976 38 0 0 25 0 1 0 492070678 61825024 14320 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14320 603 41 0 15053 0
vsize: 60376
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14675 0 0 0 116975 38 0 0 25 0 1 0 492070678 61825024 14320 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14320 603 41 0 15053 0
vsize: 60376
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14677 0 0 0 117975 38 0 0 25 0 1 0 492070678 61825024 14322 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14322 603 41 0 15053 0
vsize: 60376
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14678 0 0 0 118976 38 0 0 25 0 1 0 492070678 61825024 14323 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14323 603 41 0 15053 0
vsize: 60376
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25414
Raw data (stat): 25357 (minisat+) R 25356 22932 22931 0 -1 0 14680 0 0 0 119976 38 0 0 25 0 1 0 492070678 61825024 14325 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14325 603 41 0 15053 0
vsize: 60376
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 25414
Raw data (stat): 25357 (minisat+) Z 25356 22932 22931 0 -1 12 14682 0 0 0 119976 41 0 0 25 0 1 0 492070678 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.04
CPU time (s): 1200.18
CPU user time (s): 1199.76
CPU system time (s): 0.412937
CPU usage (%): 100.011
Max. virtual memory (Kb): 60376
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####