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/miplib3/normalized-mps-v2-20-10-air04.opb
MD5SUM	26490113618ae9605b5ebe6370b5910b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.116981
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 21456

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        585656 kB
Buffers:         33996 kB
Cached:         390412 kB
SwapCached:        524 kB
Active:         188420 kB
Inactive:       237936 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        585404 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16928 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:10:34 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 13179 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1642]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[1640]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[1638]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[1636]---> Adder-cost: 10   maxlim: 11   bits: 4/4
c ---[1634]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1632]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1628]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1626]---> Adder-cost: 56   maxlim: 34   bits: 6/6
c ---[1624]---> Adder-cost: 208   maxlim: 107   bits: 7/7
c ---[1622]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1620]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[1618]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1616]---> Adder-cost: 42   maxlim: 32   bits: 6/6
c ---[1614]---> Adder-cost: 144   maxlim: 120   bits: 7/7
c ---[1612]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1610]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1606]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1604]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[1602]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[1600]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1598]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[1596]---> Adder-cost: 256   maxlim: 130   bits: 8/8
c ---[1594]---> Adder-cost: 188   maxlim: 97   bits: 7/7
c ---[1592]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1588]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1586]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1582]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[1580]---> Adder-cost: 138   maxlim: 118   bits: 7/7
c ---[1578]---> Adder-cost: 276   maxlim: 142   bits: 8/8
c ---[1576]---> Adder-cost: 92   maxlim: 50   bits: 6/6
c ---[1574]---> Adder-cost: 48   maxlim: 48   bits: 6/6
c ---[1572]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1570]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[1568]---> Adder-cost: 226   maxlim: 119   bits: 7/7
c ---[1566]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[1564]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1562]---> Adder-cost: 114   maxlim: 77   bits: 7/7
c ---[1560]---> Adder-cost: 50   maxlim: 77   bits: 7/7
c ---[1558]---> Adder-cost: 156   maxlim: 79   bits: 7/7
c ---[1556]---> Adder-cost: 110   maxlim: 89   bits: 7/7
c ---[1554]---> Adder-cost: 100   maxlim: 72   bits: 7/7
c ---[1550]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[1548]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[1546]---> Adder-cost: 96   maxlim: 52   bits: 6/6
c ---[1544]---> Adder-cost: 106   maxlim: 59   bits: 6/6
c ---[1542]---> Adder-cost: 178   maxlim: 94   bits: 7/7
c ---[1540]---> Adder-cost: 172   maxlim: 104   bits: 7/7
c ---[1538]---> Adder-cost: 166   maxlim: 87   bits: 7/7
c ---[1536]---> Adder-cost: 126   maxlim: 68   bits: 7/7
c ---[1534]---> Adder-cost: 72   maxlim: 63   bits: 7/6
c ---[1532]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[1530]---> Adder-cost: 140   maxlim: 72   bits: 7/7
c ---[1528]---> Adder-cost: 110   maxlim: 68   bits: 7/7
c ---[1526]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[1524]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[1522]---> Adder-cost: 148   maxlim: 80   bits: 7/7
c ---[1520]---> Adder-cost: 142   maxlim: 78   bits: 7/7
c ---[1518]---> Adder-cost: 178   maxlim: 108   bits: 7/7
c ---[1516]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[1514]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1512]---> Adder-cost: 78   maxlim: 44   bits: 6/6
c ---[1510]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[1508]---> Adder-cost: 106   maxlim: 57   bits: 6/6
c ---[1506]---> Adder-cost: 122   maxlim: 64   bits: 7/7
c ---[1504]---> Adder-cost: 240   maxlim: 125   bits: 7/7
c ---[1502]---> Adder-cost: 186   maxlim: 129   bits: 8/8
c ---[1500]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[1498]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[1496]---> Adder-cost: 68   maxlim: 41   bits: 6/6
c ---[1494]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[1492]---> Adder-cost: 86   maxlim: 49   bits: 6/6
c ---[1490]---> Adder-cost: 136   maxlim: 73   bits: 7/7
c ---[1488]---> Adder-cost: 94   maxlim: 67   bits: 7/7
c ---[1486]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1484]---> Adder-cost: 164   maxlim: 85   bits: 7/7
c ---[1482]---> Adder-cost: 142   maxlim: 96   bits: 7/7
c ---[1480]---> Adder-cost: 148   maxlim: 77   bits: 7/7
c ---[1478]---> Adder-cost: 92   maxlim: 67   bits: 7/7
c ---[1476]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1474]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[1472]---> Adder-cost: 44   maxlim: 25   bits: 5/5
c ---[1470]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1468]---> Adder-cost: 98   maxlim: 55   bits: 6/6
c ---[1464]---> Adder-cost: 48   maxlim: 30   bits: 5/5
c ---[1460]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1458]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[1456]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[1452]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1450]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[1448]---> Adder-cost: 268   maxlim: 143   bits: 8/8
c ---[1446]---> Adder-cost: 246   maxlim: 152   bits: 8/8
c ---[1444]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[1442]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[1440]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[1438]---> Adder-cost: 232   maxlim: 120   bits: 7/7
c ---[1436]---> Adder-cost: 168   maxlim: 113   bits: 7/7
c ---[1434]---> Adder-cost: 46   maxlim: 30   bits: 5/5
c ---[1432]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1430]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1428]---> Adder-cost: 62   maxlim: 41   bits: 6/6
c ---[1426]---> Adder-cost: 66   maxlim: 37   bits: 6/6
c ---[1424]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1422]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[1420]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1416]---> Adder-cost: 174   maxlim: 94   bits: 7/7
c ---[1414]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[1412]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1410]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[1408]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1406]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1404]---> Adder-cost: 142   maxlim: 75   bits: 7/7
c ---[1402]---> Adder-cost: 98   maxlim: 69   bits: 7/7
c ---[1400]---> Adder-cost: 190   maxlim: 98   bits: 7/7
c ---[1398]---> Adder-cost: 108   maxlim: 83   bits: 7/7
c ---[1396]---> Adder-cost: 152   maxlim: 79   bits: 7/7
c ---[1394]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[1392]---> Adder-cost: 200   maxlim: 120   bits: 7/7
c ---[1390]---> Adder-cost: 208   maxlim: 113   bits: 7/7
c ---[1388]---> Adder-cost: 232   maxlim: 124   bits: 7/7
c ---[1386]---> Adder-cost: 156   maxlim: 93   bits: 7/7
c ---[1384]---> Adder-cost: 220   maxlim: 113   bits: 7/7
c ---[1382]---> Adder-cost: 228   maxlim: 123   bits: 7/7
c ---[1380]---> Adder-cost: 162   maxlim: 114   bits: 7/7
c ---[1378]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[1376]---> Adder-cost: 50   maxlim: 34   bits: 6/6
c ---[1374]---> Adder-cost: 84   maxlim: 50   bits: 6/6
c ---[1372]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1370]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1368]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1366]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[1364]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[1362]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[1360]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[1358]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1356]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1354]---> Adder-cost: 62   maxlim: 34   bits: 6/6
c ---[1352]---> Adder-cost: 74   maxlim: 47   bits: 6/6
c ---[1350]---> Adder-cost: 108   maxlim: 63   bits: 7/6
c ---[1346]---> Adder-cost: 202   maxlim: 106   bits: 7/7
c ---[1342]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1340]---> Adder-cost: 108   maxlim: 59   bits: 6/6
c ---[1338]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1336]---> Adder-cost: 62   maxlim: 35   bits: 6/6
c ---[1334]---> Adder-cost: 50   maxlim: 38   bits: 6/6
c ---[1332]---> Adder-cost: 430   maxlim: 220   bits: 8/8
c ---[1330]---> Adder-cost: 422   maxlim: 215   bits: 8/8
c ---[1328]---> Adder-cost: 284   maxlim: 145   bits: 8/8
c ---[1326]---> Adder-cost: 218   maxlim: 129   bits: 8/8
c ---[1324]---> Adder-cost: 188   maxlim: 98   bits: 7/7
c ---[1322]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1320]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[1318]---> Adder-cost: 350   maxlim: 180   bits: 8/8
c ---[1316]---> Adder-cost: 322   maxlim: 195   bits: 8/8
c ---[1312]---> Adder-cost: 152   maxlim: 85   bits: 7/7
c ---[1310]---> Adder-cost: 146   maxlim: 86   bits: 7/7
c ---[1308]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[1306]---> Adder-cost: 218   maxlim: 113   bits: 7/7
c ---[1304]---> Adder-cost: 156   maxlim: 114   bits: 7/7
c ---[1302]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[1300]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[1298]---> Adder-cost: 114   maxlim: 68   bits: 7/7
c ---[1296]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[1294]---> Adder-cost: 58   maxlim: 46   bits: 6/6
c ---[1292]---> Adder-cost: 54   maxlim: 47   bits: 6/6
c ---[1288]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1286]---> Adder-cost: 70   maxlim: 44   bits: 6/6
c ---[1284]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1282]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1280]---> Adder-cost: 38   maxlim: 35   bits: 6/6
c ---[1278]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1276]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[1274]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1272]---> Adder-cost: 104   maxlim: 71   bits: 7/7
c ---[1270]---> Adder-cost: 146   maxlim: 84   bits: 7/7
c ---[1268]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[1266]---> Adder-cost: 56   maxlim: 61   bits: 6/6
c ---[1264]---> Adder-cost: 78   maxlim: 44   bits: 6/6
c ---[1262]---> Adder-cost: 144   maxlim: 78   bits: 7/7
c ---[1260]---> Adder-cost: 158   maxlim: 86   bits: 7/7
c ---[1258]---> Adder-cost: 192   maxlim: 106   bits: 7/7
c ---[1256]---> Adder-cost: 222   maxlim: 117   bits: 7/7
c ---[1254]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[1252]---> Adder-cost: 128   maxlim: 70   bits: 7/7
c ---[1250]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[1248]---> Adder-cost: 50   maxlim: 31   bits: 6/5
c ---[1246]---> Adder-cost: 88   maxlim: 50   bits: 6/6
c ---[1244]---> Adder-cost: 316   maxlim: 163   bits: 8/8
c ---[1242]---> Adder-cost: 324   maxlim: 168   bits: 8/8
c ---[1240]---> Adder-cost: 204   maxlim: 156   bits: 8/8
c ---[1238]---> Adder-cost: 260   maxlim: 136   bits: 8/8
c ---[1236]---> Adder-cost: 142   maxlim: 135   bits: 8/8
c ---[1234]---> Adder-cost: 404   maxlim: 207   bits: 8/8
c ---[1232]---> Adder-cost: 342   maxlim: 202   bits: 8/8
c ---[1230]---> Adder-cost: 120   maxlim: 65   bits: 7/7
c ---[1228]---> Adder-cost: 98   maxlim: 61   bits: 6/6
c ---[1226]---> Adder-cost: 220   maxlim: 127   bits: 8/7
c ---[1224]---> Adder-cost: 48   maxlim: 29   bits: 5/5
c ---[1222]---> Adder-cost: 212   maxlim: 119   bits: 7/7
c ---[1220]---> Adder-cost: 158   maxlim: 98   bits: 7/7
c ---[1218]---> Adder-cost: 104   maxlim: 61   bits: 6/6
c ---[1216]---> Adder-cost: 70   maxlim: 73   bits: 7/7
c ---[1214]---> Adder-cost: 136   maxlim: 72   bits: 7/7
c ---[1212]---> Adder-cost: 98   maxlim: 68   bits: 7/7
c ---[1210]---> Adder-cost: 108   maxlim: 62   bits: 6/6
c ---[1208]---> Adder-cost: 82   maxlim: 57   bits: 6/6
c ---[1206]---> Adder-cost: 96   maxlim: 53   bits: 6/6
c ---[1204]---> Adder-cost: 76   maxlim: 53   bits: 6/6
c ---[1202]---> Adder-cost: 62   maxlim: 41   bits: 6/6
c ---[1200]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1198]---> Adder-cost: 130   maxlim: 69   bits: 7/7
c ---[1196]---> Adder-cost: 168   maxlim: 106   bits: 7/7
c ---[1194]---> Adder-cost: 254   maxlim: 134   bits: 8/8
c ---[1192]---> Adder-cost: 210   maxlim: 115   bits: 7/7
c ---[1190]---> Adder-cost: 216   maxlim: 116   bits: 7/7
c ---[1188]---> Adder-cost: 216   maxlim: 129   bits: 8/8
c ---[1186]---> Adder-cost: 224   maxlim: 121   bits: 7/7
c ---[1184]---> Adder-cost: 202   maxlim: 115   bits: 7/7
c ---[1182]---> Adder-cost: 46   maxlim: 35   bits: 6/6
c ---[1180]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[1178]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[1176]---> Adder-cost: 178   maxlim: 120   bits: 7/7
c ---[1174]---> Adder-cost: 260   maxlim: 144   bits: 8/8
c ---[1172]---> Adder-cost: 134   maxlim: 97   bits: 7/7
c ---[1170]---> Adder-cost: 204   maxlim: 108   bits: 7/7
c ---[1168]---> Adder-cost: 138   maxlim: 104   bits: 7/7
c ---[1166]---> Adder-cost: 234   maxlim: 123   bits: 7/7
c ---[1164]---> Adder-cost: 192   maxlim: 130   bits: 8/8
c ---[1162]---> Adder-cost: 258   maxlim: 145   bits: 8/8
c ---[1160]---> Adder-cost: 210   maxlim: 120   bits: 7/7
c ---[1158]---> Adder-cost: 186   maxlim: 102   bits: 7/7
c ---[1156]---> Adder-cost: 138   maxlim: 72   bits: 7/7
c ---[1154]---> Adder-cost: 194   maxlim: 110   bits: 7/7
c ---[1152]---> Adder-cost: 126   maxlim: 66   bits: 7/7
c ---[1150]---> Adder-cost: 230   maxlim: 124   bits: 7/7
c ---[1148]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[1146]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[1144]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[1142]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[1140]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1138]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[1136]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1134]---> Adder-cost: 40   maxlim: 29   bits: 5/5
c ---[1132]---> Adder-cost: 174   maxlim: 95   bits: 7/7
c ---[1130]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1128]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[1126]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[1124]---> Adder-cost: 102   maxlim: 57   bits: 6/6
c ---[1122]---> Adder-cost: 98   maxlim: 58   bits: 6/6
c ---[1120]---> Adder-cost: 48   maxlim: 42   bits: 6/6
c ---[1118]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1116]---> Adder-cost: 90   maxlim: 53   bits: 6/6
c ---[1114]---> Adder-cost: 96   maxlim: 51   bits: 6/6
c ---[1112]---> Adder-cost: 90   maxlim: 52   bits: 6/6
c ---[1110]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[1108]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1106]---> Adder-cost: 88   maxlim: 47   bits: 6/6
c ---[1104]---> Adder-cost: 74   maxlim: 46   bits: 6/6
c ---[1102]---> Adder-cost: 42   maxlim: 45   bits: 6/6
c ---[1100]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1098]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1096]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[1094]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[1092]---> Adder-cost: 178   maxlim: 93   bits: 7/7
c ---[1090]---> Adder-cost: 234   maxlim: 127   bits: 8/7
c ---[1088]---> Adder-cost: 300   maxlim: 158   bits: 8/8
c ---[1086]---> Adder-cost: 236   maxlim: 130   bits: 8/8
c ---[1084]---> Adder-cost: 140   maxlim: 89   bits: 7/7
c ---[1082]---> Adder-cost: 256   maxlim: 132   bits: 8/8
c ---[1080]---> Adder-cost: 162   maxlim: 84   bits: 7/7
c ---[1078]---> Adder-cost: 148   maxlim: 84   bits: 7/7
c ---[1076]---> Adder-cost: 142   maxlim: 77   bits: 7/7
c ---[1074]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1072]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[1070]---> Adder-cost: 90   maxlim: 49   bits: 6/6
c ---[1068]---> Adder-cost: 140   maxlim: 71   bits: 7/7
c ---[1066]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[1064]---> Adder-cost: 118   maxlim: 84   bits: 7/7
c ---[1062]---> Adder-cost: 108   maxlim: 92   bits: 7/7
c ---[1060]---> Adder-cost: 166   maxlim: 93   bits: 7/7
c ---[1058]---> Adder-cost: 246   maxlim: 137   bits: 8/8
c ---[1056]---> Adder-cost: 60   maxlim: 33   bits: 6/6
c ---[1054]---> Adder-cost: 42   maxlim: 25   bits: 5/5
c ---[1052]---> Adder-cost: 30   maxlim: 24   bits: 5/5
c ---[1050]---> Adder-cost: 94   maxlim: 51   bits: 6/6
c ---[1048]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1046]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1044]---> Adder-cost: 28   maxlim: 24   bits: 5/5
c ---[1042]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[1040]---> Adder-cost: 46   maxlim: 38   bits: 6/6
c ---[1038]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1036]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[1034]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[1032]---> Adder-cost: 92   maxlim: 50   bits: 6/6
c ---[1030]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1028]---> Adder-cost: 76   maxlim: 55   bits: 6/6
c ---[1026]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[1024]---> Adder-cost: 138   maxlim: 87   bits: 7/7
c ---[1022]---> Adder-cost: 368   maxlim: 206   bits: 8/8
c ---[1020]---> Adder-cost: 292   maxlim: 186   bits: 8/8
c ---[1018]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[1016]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1014]---> Adder-cost: 68   maxlim: 45   bits: 6/6
c ---[1012]---> Adder-cost: 68   maxlim: 40   bits: 6/6
c ---[1010]---> Adder-cost: 74   maxlim: 42   bits: 6/6
c ---[1008]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[1006]---> Adder-cost: 118   maxlim: 85   bits: 7/7
c ---[1004]---> Adder-cost: 196   maxlim: 105   bits: 7/7
c ---[1002]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1000]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 998]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[ 994]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[ 992]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 990]---> Adder-cost: 68   maxlim: 49   bits: 6/6
c ---[ 988]---> Adder-cost: 84   maxlim: 50   bits: 6/6
c ---[ 986]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 984]---> Adder-cost: 112   maxlim: 69   bits: 7/7
c ---[ 982]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[ 980]---> Adder-cost: 106   maxlim: 60   bits: 6/6
c ---[ 978]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 976]---> Adder-cost: 76   maxlim: 47   bits: 6/6
c ---[ 974]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 972]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 970]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 968]---> Adder-cost: 50   maxlim: 38   bits: 6/6
c ---[ 964]---> Adder-cost: 174   maxlim: 92   bits: 7/7
c ---[ 962]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 960]---> Adder-cost: 90   maxlim: 49   bits: 6/6
c ---[ 958]---> Adder-cost: 214   maxlim: 113   bits: 7/7
c ---[ 956]---> Adder-cost: 254   maxlim: 141   bits: 8/8
c ---[ 952]---> Adder-cost: 150   maxlim: 80   bits: 7/7
c ---[ 950]---> Adder-cost: 200   maxlim: 105   bits: 7/7
c ---[ 948]---> Adder-cost: 140   maxlim: 109   bits: 7/7
c ---[ 946]---> Adder-cost: 222   maxlim: 119   bits: 7/7
c ---[ 944]---> Adder-cost: 114   maxlim: 96   bits: 7/7
c ---[ 942]---> Adder-cost: 358   maxlim: 185   bits: 8/8
c ---[ 940]---> Adder-cost: 318   maxlim: 185   bits: 8/8
c ---[ 938]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[ 936]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[ 934]---> Adder-cost: 276   maxlim: 145   bits: 8/8
c ---[ 932]---> Adder-cost: 244   maxlim: 140   bits: 8/8
c ---[ 930]---> Adder-cost: 328   maxlim: 174   bits: 8/8
c ---[ 928]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 926]---> Adder-cost: 78   maxlim: 49   bits: 6/6
c ---[ 924]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 922]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[ 920]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 918]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[ 916]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[ 914]---> Adder-cost: 142   maxlim: 75   bits: 7/7
c ---[ 912]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[ 910]---> Adder-cost: 56   maxlim: 54   bits: 6/6
c ---[ 908]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[ 906]---> Adder-cost: 98   maxlim: 57   bits: 6/6
c ---[ 904]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 902]---> Adder-cost: 224   maxlim: 117   bits: 7/7
c ---[ 900]---> Adder-cost: 184   maxlim: 98   bits: 7/7
c ---[ 898]---> Adder-cost: 150   maxlim: 88   bits: 7/7
c ---[ 896]---> Adder-cost: 214   maxlim: 125   bits: 7/7
c ---[ 894]---> Adder-cost: 380   maxlim: 194   bits: 8/8
c ---[ 892]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 890]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 888]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 886]---> Adder-cost: 132   maxlim: 74   bits: 7/7
c ---[ 884]---> Adder-cost: 132   maxlim: 75   bits: 7/7
c ---[ 882]---> Adder-cost: 258   maxlim: 138   bits: 8/8
c ---[ 880]---> Adder-cost: 198   maxlim: 109   bits: 7/7
c ---[ 878]---> Adder-cost: 156   maxlim: 90   bits: 7/7
c ---[ 876]---> Adder-cost: 214   maxlim: 120   bits: 7/7
c ---[ 874]---> Adder-cost: 282   maxlim: 154   bits: 8/8
c ---[ 872]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 870]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 868]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[ 866]---> Adder-cost: 100   maxlim: 58   bits: 6/6
c ---[ 864]---> Adder-cost: 92   maxlim: 58   bits: 6/6
c ---[ 862]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[ 860]---> Adder-cost: 322   maxlim: 165   bits: 8/8
c ---[ 858]---> Adder-cost: 282   maxlim: 155   bits: 8/8
c ---[ 856]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 854]---> Adder-cost: 76   maxlim: 47   bits: 6/6
c ---[ 852]---> Adder-cost: 272   maxlim: 159   bits: 8/8
c ---[ 850]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[ 848]---> Adder-cost: 68   maxlim: 41   bits: 6/6
c ---[ 846]---> Adder-cost: 64   maxlim: 43   bits: 6/6
c ---[ 844]---> Adder-cost: 80   maxlim: 44   bits: 6/6
c ---[ 842]---> Adder-cost: 58   maxlim: 45   bits: 6/6
c ---[ 840]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 836]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 834]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[ 832]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[ 828]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 826]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[ 824]---> Adder-cost: 236   maxlim: 123   bits: 7/7
c ---[ 822]---> Adder-cost: 196   maxlim: 113   bits: 7/7
c ---[ 820]---> Adder-cost: 104   maxlim: 56   bits: 6/6
c ---[ 818]---> Adder-cost: 108   maxlim: 64   bits: 7/7
c ---[ 816]---> Adder-cost: 122   maxlim: 69   bits: 7/7
c ---[ 814]---> Adder-cost: 124   maxlim: 70   bits: 7/7
c ---[ 812]---> Adder-cost: 240   maxlim: 130   bits: 8/8
c ---[ 810]---> Adder-cost: 238   maxlim: 131   bits: 8/8
c ---[ 808]---> Adder-cost: 254   maxlim: 138   bits: 8/8
c ---[ 806]---> Adder-cost: 170   maxlim: 141   bits: 8/8
c ---[ 804]---> Adder-cost: 254   maxlim: 134   bits: 8/8
c ---[ 802]---> Adder-cost: 158   maxlim: 86   bits: 7/7
c ---[ 800]---> Adder-cost: 80   maxlim: 55   bits: 6/6
c ---[ 796]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 794]---> Adder-cost: 160   maxlim: 93   bits: 7/7
c ---[ 792]---> Adder-cost: 104   maxlim: 93   bits: 7/7
c ---[ 790]---> Adder-cost: 272   maxlim: 146   bits: 8/8
c ---[ 788]---> Adder-cost: 182   maxlim: 151   bits: 8/8
c ---[ 786]---> Adder-cost: 316   maxlim: 168   bits: 8/8
c ---[ 784]---> Adder-cost: 350   maxlim: 197   bits: 8/8
c ---[ 782]---> Adder-cost: 232   maxlim: 128   bits: 8/8
c ---[ 780]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[ 778]---> Adder-cost: 64   maxlim: 45   bits: 6/6
c ---[ 776]---> Adder-cost: 86   maxlim: 52   bits: 6/6
c ---[ 774]---> Adder-cost: 172   maxlim: 101   bits: 7/7
c ---[ 772]---> Adder-cost: 354   maxlim: 194   bits: 8/8
c ---[ 770]---> Adder-cost: 316   maxlim: 165   bits: 8/8
c ---[ 768]---> Adder-cost: 224   maxlim: 161   bits: 8/8
c ---[ 766]---> Adder-cost: 126   maxlim: 65   bits: 7/7
c ---[ 764]---> Adder-cost: 86   maxlim: 50   bits: 6/6
c ---[ 762]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 760]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[ 758]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[ 756]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 754]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 752]---> Adder-cost: 126   maxlim: 72   bits: 7/7
c ---[ 750]---> Adder-cost: 356   maxlim: 189   bits: 8/8
c ---[ 748]---> Adder-cost: 168   maxlim: 177   bits: 8/8
c ---[ 744]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 742]---> Adder-cost: 98   maxlim: 61   bits: 6/6
c ---[ 740]---> Adder-cost: 132   maxlim: 76   bits: 7/7
c ---[ 738]---> Adder-cost: 208   maxlim: 111   bits: 7/7
c ---[ 736]---> Adder-cost: 156   maxlim: 91   bits: 7/7
c ---[ 732]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 730]---> Adder-cost: 128   maxlim: 74   bits: 7/7
c ---[ 728]---> Adder-cost: 272   maxlim: 150   bits: 8/8
c ---[ 726]---> Adder-cost: 304   maxlim: 166   bits: 8/8
c ---[ 722]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 720]---> Adder-cost: 200   maxlim: 103   bits: 7/7
c ---[ 718]---> Adder-cost: 236   maxlim: 131   bits: 8/8
c ---[ 716]---> Adder-cost: 340   maxlim: 175   bits: 8/8
c ---[ 714]---> Adder-cost: 272   maxlim: 177   bits: 8/8
c ---[ 712]---> Adder-cost: 156   maxlim: 83   bits: 7/7
c ---[ 710]---> Adder-cost: 138   maxlim: 86   bits: 7/7
c ---[ 708]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[ 706]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[ 704]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[ 702]---> Adder-cost: 58   maxlim: 54   bits: 6/6
c ---[ 700]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[ 698]---> Adder-cost: 150   maxlim: 80   bits: 7/7
c ---[ 696]---> Adder-cost: 136   maxlim: 75   bits: 7/7
c ---[ 694]---> Adder-cost: 136   maxlim: 76   bits: 7/7
c ---[ 692]---> Adder-cost: 152   maxlim: 83   bits: 7/7
c ---[ 690]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 688]---> Adder-cost: 242   maxlim: 127   bits: 8/7
c ---[ 686]---> Adder-cost: 142   maxlim: 129   bits: 8/8
c ---[ 684]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 682]---> Adder-cost: 138   maxlim: 71   bits: 7/7
c ---[ 680]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[ 678]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 676]---> Adder-cost: 68   maxlim: 38   bits: 6/6
c ---[ 674]---> Adder-cost: 90   maxlim: 56   bits: 6/6
c ---[ 672]---> Adder-cost: 144   maxlim: 76   bits: 7/7
c ---[ 670]---> Adder-cost: 128   maxlim: 69   bits: 7/7
c ---[ 668]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[ 666]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 664]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 662]---> Adder-cost: 18   maxlim: 18   bits: 5/5
c ---[ 660]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 658]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 654]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[ 652]---> Adder-cost: 186   maxlim: 99   bits: 7/7
c ---[ 650]---> Adder-cost: 78   maxlim: 99   bits: 7/7
c ---[ 648]---> Adder-cost: 120   maxlim: 63   bits: 7/6
c ---[ 646]---> Adder-cost: 156   maxlim: 89   bits: 7/7
c ---[ 642]---> Adder-cost: 90   maxlim: 48   bits: 6/6
c ---[ 640]---> Adder-cost: 60   maxlim: 47   bits: 6/6
c ---[ 638]---> Adder-cost: 292   maxlim: 161   bits: 8/8
c ---[ 636]---> Adder-cost: 196   maxlim: 158   bits: 8/8
c ---[ 634]---> Adder-cost: 144   maxlim: 84   bits: 7/7
c ---[ 628]---> Adder-cost: 116   maxlim: 78   bits: 7/7
c ---[ 626]---> Adder-cost: 234   maxlim: 127   bits: 8/7
c ---[ 624]---> Adder-cost: 332   maxlim: 196   bits: 8/8
c ---[ 622]---> Adder-cost: 324   maxlim: 174   bits: 8/8
c ---[ 620]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 616]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 614]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[ 612]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 610]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 608]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[ 606]---> Adder-cost: 76   maxlim: 43   bits: 6/6
c ---[ 604]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 602]---> Adder-cost: 318   maxlim: 182   bits: 8/8
c ---[ 600]---> Adder-cost: 216   maxlim: 187   bits: 8/8
c ---[ 598]---> Adder-cost: 280   maxlim: 177   bits: 8/8
c ---[ 596]---> Adder-cost: 338   maxlim: 175   bits: 8/8
c ---[ 594]---> Adder-cost: 232   maxlim: 160   bits: 8/8
c ---[ 592]---> Adder-cost: 282   maxlim: 160   bits: 8/8
c ---[ 590]---> Adder-cost: 230   maxlim: 175   bits: 8/8
c ---[ 588]---> Adder-cost: 134   maxlim: 77   bits: 7/7
c ---[ 586]---> Adder-cost: 94   maxlim: 57   bits: 6/6
c ---[ 584]---> Adder-cost: 88   maxlim: 56   bits: 6/6
c ---[ 582]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[ 580]---> Adder-cost: 34   maxlim: 25   bits: 5/5
c ---[ 578]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 576]---> Adder-cost: 12   maxlim: 14   bits: 4/4
c ---[ 574]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 570]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 566]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 564]---> Adder-cost: 122   maxlim: 74   bits: 7/7
c ---[ 562]---> Adder-cost: 144   maxlim: 81   bits: 7/7
c ---[ 560]---> Adder-cost: 374   maxlim: 198   bits: 8/8
c ---[ 558]---> Adder-cost: 214   maxlim: 199   bits: 8/8
c ---[ 556]---> Adder-cost: 376   maxlim: 197   bits: 8/8
c ---[ 554]---> Adder-cost: 286   maxlim: 177   bits: 8/8
c ---[ 552]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 550]---> Adder-cost: 322   maxlim: 197   bits: 8/8
c ---[ 548]---> Adder-cost: 256   maxlim: 134   bits: 8/8
c ---[ 546]---> Adder-cost: 190   maxlim: 130   bits: 8/8
c ---[ 544]---> Adder-cost: 226   maxlim: 133   bits: 8/8
c ---[ 542]---> Adder-cost: 252   maxlim: 132   bits: 8/8
c ---[ 540]---> Adder-cost: 210   maxlim: 136   bits: 8/8
c ---[ 538]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 536]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 534]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 532]---> Adder-cost: 104   maxlim: 59   bits: 6/6
c ---[ 530]---> Adder-cost: 56   maxlim: 36   bits: 6/6
c ---[ 528]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[ 526]---> Adder-cost: 106   maxlim: 91   bits: 7/7
c ---[ 524]---> Adder-cost: 196   maxlim: 108   bits: 7/7
c ---[ 522]---> Adder-cost: 138   maxlim: 110   bits: 7/7
c ---[ 520]---> Adder-cost: 178   maxlim: 103   bits: 7/7
c ---[ 518]---> Adder-cost: 316   maxlim: 173   bits: 8/8
c ---[ 516]---> Adder-cost: 242   maxlim: 138   bits: 8/8
c ---[ 514]---> Adder-cost: 162   maxlim: 89   bits: 7/7
c ---[ 512]---> Adder-cost: 116   maxlim: 76   bits: 7/7
c ---[ 510]---> Adder-cost: 248   maxlim: 134   bits: 8/8
c ---[ 508]---> Adder-cost: 224   maxlim: 144   bits: 8/8
c ---[ 506]---> Adder-cost: 104   maxlim: 55   bits: 6/6
c ---[ 504]---> Adder-cost: 112   maxlim: 64   bits: 7/7
c ---[ 502]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 500]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[ 498]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 496]---> Adder-cost: 94   maxlim: 60   bits: 6/6
c ---[ 494]---> Adder-cost: 64   maxlim: 50   bits: 6/6
c ---[ 492]---> Adder-cost: 74   maxlim: 54   bits: 6/6
c ---[ 490]---> Adder-cost: 248   maxlim: 132   bits: 8/8
c ---[ 488]---> Adder-cost: 148   maxlim: 126   bits: 7/7
c ---[ 486]---> Adder-cost: 250   maxlim: 143   bits: 8/8
c ---[ 484]---> Adder-cost: 352   maxlim: 195   bits: 8/8
c ---[ 482]---> Adder-cost: 274   maxlim: 170   bits: 8/8
c ---[ 480]---> Adder-cost: 296   maxlim: 179   bits: 8/8
c ---[ 478]---> Adder-cost: 290   maxlim: 178   bits: 8/8
c ---[ 476]---> Adder-cost: 238   maxlim: 133   bits: 8/8
c ---[ 474]---> Adder-cost: 166   maxlim: 128   bits: 8/8
c ---[ 472]---> Adder-cost: 264   maxlim: 148   bits: 8/8
c ---[ 468]---> Adder-cost: 398   maxlim: 210   bits: 8/8
c ---[ 466]---> Adder-cost: 366   maxlim: 221   bits: 8/8
c ---[ 464]---> Adder-cost: 400   maxlim: 237   bits: 8/8
c ---[ 462]---> Adder-cost: 416   maxlim: 239   bits: 8/8
c ---[ 460]---> Adder-cost: 338   maxlim: 204   bits: 8/8
c ---[ 458]---> Adder-cost: 214   maxlim: 121   bits: 7/7
c ---[ 456]---> Adder-cost: 190   maxlim: 108   bits: 7/7
c ---[ 454]---> Adder-cost: 276   maxlim: 157   bits: 8/8
c ---[ 452]---> Adder-cost: 330   maxlim: 187   bits: 8/8
c ---[ 450]---> Adder-cost: 362   maxlim: 196   bits: 8/8
c ---[ 448]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 446]---> Adder-cost: 184   maxlim: 121   bits: 7/7
c ---[ 444]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[ 442]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 440]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 438]---> Adder-cost: 112   maxlim: 76   bits: 7/7
c ---[ 436]---> Adder-cost: 250   maxlim: 130   bits: 8/8
c ---[ 434]---> Adder-cost: 262   maxlim: 137   bits: 8/8
c ---[ 432]---> Adder-cost: 304   maxlim: 156   bits: 8/8
c ---[ 430]---> Adder-cost: 284   maxlim: 173   bits: 8/8
c ---[ 428]---> Adder-cost: 368   maxlim: 194   bits: 8/8
c ---[ 426]---> Adder-cost: 284   maxlim: 194   bits: 8/8
c ---[ 424]---> Adder-cost: 278   maxlim: 148   bits: 8/8
c ---[ 422]---> Adder-cost: 116   maxlim: 139   bits: 8/8
c ---[ 420]---> Adder-cost: 342   maxlim: 178   bits: 8/8
c ---[ 418]---> Adder-cost: 208   maxlim: 184   bits: 8/8
c ---[ 416]---> Adder-cost: 420   maxlim: 222   bits: 8/8
c ---[ 414]---> Adder-cost: 586   maxlim: 327   bits: 9/9
c ---[ 412]---> Adder-cost: 658   maxlim: 353   bits: 9/9
c ---[ 410]---> Adder-cost: 462   maxlim: 346   bits: 9/9
c ---[ 408]---> Adder-cost: 394   maxlim: 221   bits: 8/8
c ---[ 406]---> Adder-cost: 364   maxlim: 224   bits: 8/8
c ---[ 404]---> Adder-cost: 260   maxlim: 145   bits: 8/8
c ---[ 402]---> Adder-cost: 256   maxlim: 140   bits: 8/8
c ---[ 400]---> Adder-cost: 222   maxlim: 121   bits: 7/7
c ---[ 398]---> Adder-cost: 118   maxlim: 130   bits: 8/8
c ---[ 396]---> Adder-cost: 296   maxlim: 155   bits: 8/8
c ---[ 394]---> Adder-cost: 280   maxlim: 144   bits: 8/8
c ---[ 392]---> Adder-cost: 156   maxlim: 89   bits: 7/7
c ---[ 390]---> Adder-cost: 138   maxlim: 78   bits: 7/7
c ---[ 388]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 386]---> Adder-cost: 70   maxlim: 62   bits: 6/6
c ---[ 384]---> Adder-cost: 180   maxlim: 95   bits: 7/7
c ---[ 382]---> Adder-cost: 204   maxlim: 112   bits: 7/7
c ---[ 378]---> Adder-cost: 254   maxlim: 134   bits: 8/8
c ---[ 376]---> Adder-cost: 124   maxlim: 68   bits: 7/7
c ---[ 374]---> Adder-cost: 80   maxlim: 54   bits: 6/6
c ---[ 372]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 370]---> Adder-cost: 52   maxlim: 38   bits: 6/6
c ---[ 368]---> Adder-cost: 112   maxlim: 61   bits: 6/6
c ---[ 366]---> Adder-cost: 80   maxlim: 61   bits: 6/6
c ---[ 360]---> Adder-cost: 184   maxlim: 95   bits: 7/7
c ---[ 358]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 356]---> Adder-cost: 64   maxlim: 41   bits: 6/6
c ---[ 354]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 352]---> Adder-cost: 86   maxlim: 50   bits: 6/6
c ---[ 350]---> Adder-cost: 306   maxlim: 164   bits: 8/8
c ---[ 348]---> Adder-cost: 210   maxlim: 147   bits: 8/8
c ---[ 346]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 344]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 342]---> Adder-cost: 252   maxlim: 128   bits: 8/8
c ---[ 340]---> Adder-cost: 260   maxlim: 143   bits: 8/8
c ---[ 338]---> Adder-cost: 176   maxlim: 96   bits: 7/7
c ---[ 336]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 334]---> Adder-cost: 76   maxlim: 46   bits: 6/6
c ---[ 332]---> Adder-cost: 186   maxlim: 106   bits: 7/7
c ---[ 330]---> Adder-cost: 140   maxlim: 80   bits: 7/7
c ---[ 328]---> Adder-cost: 102   maxlim: 69   bits: 7/7
c ---[ 326]---> Adder-cost: 50   maxlim: 45   bits: 6/6
c ---[ 324]---> Adder-cost: 98   maxlim: 58   bits: 6/6
c ---[ 322]---> Adder-cost: 128   maxlim: 74   bits: 7/7
c ---[ 318]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 316]---> Adder-cost: 312   maxlim: 161   bits: 8/8
c ---[ 314]---> Adder-cost: 228   maxlim: 172   bits: 8/8
c ---[ 312]---> Adder-cost: 584   maxlim: 302   bits: 9/9
c ---[ 310]---> Adder-cost: 434   maxlim: 302   bits: 9/9
c ---[ 308]---> Adder-cost: 348   maxlim: 196   bits: 8/8
c ---[ 306]---> Adder-cost: 312   maxlim: 200   bits: 8/8
c ---[ 304]---> Adder-cost: 278   maxlim: 145   bits: 8/8
c ---[ 302]---> Adder-cost: 230   maxlim: 139   bits: 8/8
c ---[ 300]---> Adder-cost: 284   maxlim: 155   bits: 8/8
c ---[ 298]---> Adder-cost: 208   maxlim: 122   bits: 7/7
c ---[ 296]---> Adder-cost: 198   maxlim: 124   bits: 7/7
c ---[ 294]---> Adder-cost: 234   maxlim: 143   bits: 8/8
c ---[ 292]---> Adder-cost: 148   maxlim: 84   bits: 7/7
c ---[ 290]---> Adder-cost: 120   maxlim: 96   bits: 7/7
c ---[ 288]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 286]---> Adder-cost: 40   maxlim: 23   bits: 5/5
c ---[ 284]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 282]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[ 278]---> Adder-cost: 170   maxlim: 89   bits: 7/7
c ---[ 276]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 274]---> Adder-cost: 146   maxlim: 109   bits: 7/7
c ---[ 272]---> Adder-cost: 118   maxlim: 69   bits: 7/7
c ---[ 270]---> Adder-cost: 88   maxlim: 56   bits: 6/6
c ---[ 268]---> Adder-cost: 172   maxlim: 92   bits: 7/7
c ---[ 266]---> Adder-cost: 188   maxlim: 103   bits: 7/7
c ---[ 264]---> Adder-cost: 260   maxlim: 143   bits: 8/8
c ---[ 262]---> Adder-cost: 190   maxlim: 131   bits: 8/8
c ---[ 260]---> Adder-cost: 162   maxlim: 89   bits: 7/7
c ---[ 258]---> Adder-cost: 168   maxlim: 106   bits: 7/7
c ---[ 254]---> Adder-cost: 144   maxlim: 79   bits: 7/7
c ---[ 252]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 250]---> Adder-cost: 90   maxlim: 54   bits: 6/6
c ---[ 246]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[ 244]---> Adder-cost: 266   maxlim: 141   bits: 8/8
c ---[ 242]---> Adder-cost: 246   maxlim: 134   bits: 8/8
c ---[ 240]---> Adder-cost: 152   maxlim: 86   bits: 7/7
c ---[ 238]---> Adder-cost: 154   maxlim: 88   bits: 7/7
c ---[ 236]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[ 234]---> Adder-cost: 146   maxlim: 84   bits: 7/7
c ---[ 230]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 228]---> Adder-cost: 262   maxlim: 144   bits: 8/8
c ---[ 226]---> Adder-cost: 238   maxlim: 139   bits: 8/8
c ---[ 224]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 222]---> Adder-cost: 180   maxlim: 98   bits: 7/7
c ---[ 220]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[ 218]---> Adder-cost: 114   maxlim: 65   bits: 7/7
c ---[ 216]---> Adder-cost: 310   maxlim: 159   bits: 8/8
c ---[ 214]---> Adder-cost: 342   maxlim: 207   bits: 8/8
c ---[ 212]---> Adder-cost: 222   maxlim: 118   bits: 7/7
c ---[ 210]---> Adder-cost: 220   maxlim: 136   bits: 8/8
c ---[ 208]---> Adder-cost: 256   maxlim: 142   bits: 8/8
c ---[ 206]---> Adder-cost: 236   maxlim: 137   bits: 8/8
c ---[ 204]---> Adder-cost: 260   maxlim: 150   bits: 8/8
c ---[ 202]---> Adder-cost: 268   maxlim: 144   bits: 8/8
c ---[ 200]---> Adder-cost: 178   maxlim: 101   bits: 7/7
c ---[ 198]---> Adder-cost: 218   maxlim: 117   bits: 7/7
c ---[ 196]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[ 194]---> Adder-cost: 138   maxlim: 81   bits: 7/7
c ---[ 192]---> Adder-cost: 92   maxlim: 74   bits: 7/7
c ---[ 188]---> Adder-cost: 132   maxlim: 68   bits: 7/7
c ---[ 186]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[ 184]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 182]---> Adder-cost: 170   maxlim: 109   bits: 7/7
c ---[ 180]---> Adder-cost: 266   maxlim: 138   bits: 8/8
c ---[ 178]---> Adder-cost: 214   maxlim: 134   bits: 8/8
c ---[ 176]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 174]---> Adder-cost: 14   maxlim: 14   bits: 4/4
c ---[ 172]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 170]---> Adder-cost: 26   maxlim: 20   bits: 5/5
c ---[ 168]---> Adder-cost: 212   maxlim: 114   bits: 7/7
c ---[ 166]---> Adder-cost: 142   maxlim: 122   bits: 7/7
c ---[ 164]---> Adder-cost: 352   maxlim: 193   bits: 8/8
c ---[ 162]---> Adder-cost: 276   maxlim: 193   bits: 8/8
c ---[ 160]---> Adder-cost: 66   maxlim: 37   bits: 6/6
c ---[ 158]---> Adder-cost: 78   maxlim: 46   bits: 6/6
c ---[ 154]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 152]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 150]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 148]---> Adder-cost: 104   maxlim: 59   bits: 6/6
c ---[ 146]---> Adder-cost: 94   maxlim: 56   bits: 6/6
c ---[ 144]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[ 142]---> Adder-cost: 112   maxlim: 68   bits: 7/7
c ---[ 140]---> Adder-cost: 224   maxlim: 122   bits: 7/7
c ---[ 138]---> Adder-cost: 182   maxlim: 121   bits: 7/7
c ---[ 136]---> Adder-cost: 138   maxlim: 75   bits: 7/7
c ---[ 134]---> Adder-cost: 100   maxlim: 58   bits: 6/6
c ---[ 132]---> Adder-cost: 132   maxlim: 87   bits: 7/7
c ---[ 130]---> Adder-cost: 224   maxlim: 126   bits: 7/7
c ---[ 128]---> Adder-cost: 120   maxlim: 105   bits: 7/7
c ---[ 126]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[ 124]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 122]---> Adder-cost: 72   maxlim: 50   bits: 6/6
c ---[ 120]---> Adder-cost: 112   maxlim: 63   bits: 7/6
c ---[ 118]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[ 116]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[ 114]---> Adder-cost: 124   maxlim: 64   bits: 7/7
c ---[ 112]---> Adder-cost: 104   maxlim: 68   bits: 7/7
c ---[ 110]---> Adder-cost: 146   maxlim: 81   bits: 7/7
c ---[ 108]---> Adder-cost: 138   maxlim: 82   bits: 7/7
c ---[ 106]---> Adder-cost: 386   maxlim: 219   bits: 8/8
c ---[ 104]---> Adder-cost: 302   maxlim: 171   bits: 8/8
c ---[ 102]---> Adder-cost: 212   maxlim: 172   bits: 8/8
c ---[ 100]---> Adder-cost: 378   maxlim: 247   bits: 8/8
c ---[  98]---> Adder-cost: 456   maxlim: 245   bits: 8/8
c ---[  96]---> Adder-cost: 376   maxlim: 247   bits: 8/8
c ---[  94]---> Adder-cost: 412   maxlim: 229   bits: 8/8
c ---[  92]---> Adder-cost: 366   maxlim: 234   bits: 8/8
c ---[  90]---> Adder-cost: 400   maxlim: 211   bits: 8/8
c ---[  88]---> Adder-cost: 324   maxlim: 210   bits: 8/8
c ---[  86]---> Adder-cost: 400   maxlim: 217   bits: 8/8
c ---[  84]---> Adder-cost: 338   maxlim: 204   bits: 8/8
c ---[  82]---> Adder-cost: 316   maxlim: 207   bits: 8/8
c ---[  80]---> Adder-cost: 632   maxlim: 337   bits: 9/9
c ---[  78]---> Adder-cost: 612   maxlim: 367   bits: 9/9
c ---[  76]---> Adder-cost: 364   maxlim: 194   bits: 8/8
c ---[  74]---> Adder-cost: 258   maxlim: 152   bits: 8/8
c ---[  72]---> Adder-cost: 308   maxlim: 174   bits: 8/8
c ---[  70]---> Adder-cost: 334   maxlim: 185   bits: 8/8
c ---[  68]---> Adder-cost: 290   maxlim: 203   bits: 8/8
c ---[  66]---> Adder-cost: 280   maxlim: 157   bits: 8/8
c ---[  64]---> Adder-cost: 242   maxlim: 151   bits: 8/8
c ---[  62]---> Adder-cost: 234   maxlim: 129   bits: 8/8
c ---[  60]---> Adder-cost: 222   maxlim: 127   bits: 8/7
c ---[  58]---> Adder-cost: 290   maxlim: 160   bits: 8/8
c ---[  56]---> Adder-cost: 192   maxlim: 169   bits: 8/8
c ---[  54]---> Adder-cost: 252   maxlim: 174   bits: 8/8
c ---[  52]---> Adder-cost: 216   maxlim: 122   bits: 7/7
c ---[  50]---> Adder-cost: 204   maxlim: 124   bits: 7/7
c ---[  46]---> Adder-cost: 228   maxlim: 120   bits: 7/7
c ---[  44]---> Adder-cost: 140   maxlim: 75   bits: 7/7
c ---[  40]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[  38]---> Adder-cost: 110   maxlim: 74   bits: 7/7
c ---[  36]---> Adder-cost: 94   maxlim: 55   bits: 6/6
c ---[  34]---> Adder-cost: 68   maxlim: 50   bits: 6/6
c ---[  32]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[  30]---> Adder-cost: 74   maxlim: 40   bits: 6/6
c ---[  28]---> Adder-cost: 68   maxlim: 43   bits: 6/6
c ---[  26]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[  24]---> Adder-cost: 134   maxlim: 76   bits: 7/7
c ---[  22]---> Adder-cost: 158   maxlim: 89   bits: 7/7
c ---[  20]---> Adder-cost: 140   maxlim: 88   bits: 7/7
c ---[  18]---> Adder-cost: 120   maxlim: 75   bits: 7/7
c ---[  16]---> Adder-cost: 140   maxlim: 79   bits: 7/7
c ---[  14]---> Adder-cost: 196   maxlim: 108   bits: 7/7
c ---[  12]---> Adder-cost: 162   maxlim: 108   bits: 7/7
c ---[  10]---> Adder-cost: 208   maxlim: 118   bits: 7/7
c ---[   8]---> Adder-cost: 146   maxlim: 83   bits: 7/7
c ---[   6]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   4]---> Adder-cost: 54   maxlim: 36   bits: 6/6
c ---[   2]---> Adder-cost: 134   maxlim: 71   bits: 7/7
c ---[   0]---> Adder-cost: 86   maxlim: 70   bits: 7/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  794675  2828045 |  264891       0        0     nan |  0.000 % |
c |       101 |  793926  2825448 |  291380      27       94     3.5 |  8.594 % |
c |       251 |  793081  2822517 |  320518      82      291     3.5 |  8.699 % |
c |       477 |  791736  2817804 |  352569     158      582     3.7 |  8.882 % |
c |       816 |  789367  2809549 |  387826     245      891     3.6 |  9.182 % |
c |      1324 |  786208  2798570 |  426609     419     1684     4.0 |  9.592 % |
c |      2083 |  781691  2782963 |  469270     702     2852     4.1 | 10.182 % |
c |      3222 |  777251  2767505 |  516197    1379     6473     4.7 | 10.756 % |
c |      4931 |  769972  2742122 |  567817    2281    10886     4.8 | 11.696 % |
c |      7494 |  762191  2714907 |  624599    3936    20767     5.3 | 12.687 % |
c |     11342 |  752725  2681775 |  687059    6675    36966     5.5 | 13.899 % |
c |     17108 |  737586  2628156 |  755764   10422    60973     5.9 | 15.796 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.93 2/54 20444
Raw data (stat): 20444 (runsolver) R 20443 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549170837 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99999 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14588 0 0 0 964 34 0 0 25 0 1 0 549170837 71577600 14230 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14230 603 41 0 17434 0
vsize: 69900
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14598 0 0 0 1964 34 0 0 25 0 1 0 549170837 71577600 14240 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14240 603 41 0 17434 0
vsize: 69900
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14600 0 0 0 2964 34 0 0 25 0 1 0 549170837 71577600 14242 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14242 603 41 0 17434 0
vsize: 69900
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14600 0 0 0 3963 35 0 0 25 0 1 0 549170837 71577600 14242 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14242 603 41 0 17434 0
vsize: 69900
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14601 0 0 0 4963 35 0 0 25 0 1 0 549170837 71577600 14243 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14243 603 41 0 17434 0
vsize: 69900
[startup+60.0017 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14616 0 0 0 5963 35 0 0 25 0 1 0 549170837 71712768 14258 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17508 14258 603 41 0 17467 0
vsize: 70032
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14631 0 0 0 6963 35 0 0 25 0 1 0 549170837 71712768 14273 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17508 14273 603 41 0 17467 0
vsize: 70032
[startup+80.002 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14658 0 0 0 7963 35 0 0 25 0 1 0 549170837 71847936 14300 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 14300 603 41 0 17500 0
vsize: 70164
[startup+90.0017 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14677 0 0 0 8964 36 0 0 25 0 1 0 549170837 71983104 14319 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 14319 603 41 0 17533 0
vsize: 70296
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14692 0 0 0 9964 36 0 0 25 0 1 0 549170837 71983104 14334 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 14334 603 41 0 17533 0
vsize: 70296
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14720 0 0 0 10963 36 0 0 25 0 1 0 549170837 72118272 14362 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17607 14362 603 41 0 17566 0
vsize: 70428
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14739 0 0 0 11963 36 0 0 25 0 1 0 549170837 72253440 14381 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17640 14381 603 41 0 17599 0
vsize: 70560
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14768 0 0 0 12964 36 0 0 25 0 1 0 549170837 72253440 14410 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17640 14410 603 41 0 17599 0
vsize: 70560
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14783 0 0 0 13964 36 0 0 25 0 1 0 549170837 72388608 14425 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17673 14425 603 41 0 17632 0
vsize: 70692
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14802 0 0 0 14964 36 0 0 25 0 1 0 549170837 72388608 14444 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17673 14444 603 41 0 17632 0
vsize: 70692
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14817 0 0 0 15964 36 0 0 25 0 1 0 549170837 72523776 14459 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17706 14459 603 41 0 17665 0
vsize: 70824
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14846 0 0 0 16964 37 0 0 25 0 1 0 549170837 72708096 14488 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17751 14488 603 41 0 17710 0
vsize: 71004
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14860 0 0 0 17964 37 0 0 25 0 1 0 549170837 72708096 14502 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17751 14502 603 41 0 17710 0
vsize: 71004
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14873 0 0 0 18964 37 0 0 25 0 1 0 549170837 72708096 14515 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17751 14515 603 41 0 17710 0
vsize: 71004
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14880 0 0 0 19964 37 0 0 25 0 1 0 549170837 72843264 14522 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17784 14522 603 41 0 17743 0
vsize: 71136
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14897 0 0 0 20964 37 0 0 25 0 1 0 549170837 72843264 14539 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17784 14539 603 41 0 17743 0
vsize: 71136
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14915 0 0 0 21964 37 0 0 25 0 1 0 549170837 72978432 14557 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17817 14557 603 41 0 17776 0
vsize: 71268
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14931 0 0 0 22964 37 0 0 25 0 1 0 549170837 72978432 14573 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17817 14573 603 41 0 17776 0
vsize: 71268
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14950 0 0 0 23964 37 0 0 25 0 1 0 549170837 73113600 14592 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17850 14592 603 41 0 17809 0
vsize: 71400
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14965 0 0 0 24964 38 0 0 25 0 1 0 549170837 73113600 14607 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17850 14607 603 41 0 17809 0
vsize: 71400
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14978 0 0 0 25964 38 0 0 25 0 1 0 549170837 73113600 14620 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17850 14620 603 41 0 17809 0
vsize: 71400
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14985 0 0 0 26964 38 0 0 25 0 1 0 549170837 73248768 14627 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17883 14627 603 41 0 17842 0
vsize: 71532
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 14998 0 0 0 27964 38 0 0 25 0 1 0 549170837 73248768 14640 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17883 14640 603 41 0 17842 0
vsize: 71532
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15014 0 0 0 28964 38 0 0 25 0 1 0 549170837 73248768 14656 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17883 14656 603 41 0 17842 0
vsize: 71532
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15022 0 0 0 29964 38 0 0 25 0 1 0 549170837 73383936 14664 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17916 14664 603 41 0 17875 0
vsize: 71664
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15031 0 0 0 30964 38 0 0 25 0 1 0 549170837 73383936 14673 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17916 14673 603 41 0 17875 0
vsize: 71664
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15042 0 0 0 31965 38 0 0 25 0 1 0 549170837 73383936 14684 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17916 14684 603 41 0 17875 0
vsize: 71664
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15049 0 0 0 32965 38 0 0 25 0 1 0 549170837 73383936 14691 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17916 14691 603 41 0 17875 0
vsize: 71664
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15054 0 0 0 33965 38 0 0 25 0 1 0 549170837 73519104 14696 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17949 14696 603 41 0 17908 0
vsize: 71796
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15057 0 0 0 34965 38 0 0 25 0 1 0 549170837 73519104 14699 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17949 14699 603 41 0 17908 0
vsize: 71796
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15065 0 0 0 35965 38 0 0 25 0 1 0 549170837 73519104 14707 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17949 14707 603 41 0 17908 0
vsize: 71796
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15076 0 0 0 36965 38 0 0 25 0 1 0 549170837 73519104 14718 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17949 14718 603 41 0 17908 0
vsize: 71796
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15083 0 0 0 37965 38 0 0 25 0 1 0 549170837 73519104 14725 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17949 14725 603 41 0 17908 0
vsize: 71796
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15089 0 0 0 38966 38 0 0 25 0 1 0 549170837 73654272 14731 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14731 603 41 0 17941 0
vsize: 71928
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15090 0 0 0 39966 38 0 0 25 0 1 0 549170837 73654272 14732 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14732 603 41 0 17941 0
vsize: 71928
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15094 0 0 0 40966 38 0 0 25 0 1 0 549170837 73654272 14736 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14736 603 41 0 17941 0
vsize: 71928
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15101 0 0 0 41966 38 0 0 25 0 1 0 549170837 73654272 14743 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14743 603 41 0 17941 0
vsize: 71928
[startup+430.002 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15106 0 0 0 42966 38 0 0 25 0 1 0 549170837 73654272 14748 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14748 603 41 0 17941 0
vsize: 71928
[startup+440.002 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15111 0 0 0 43966 38 0 0 25 0 1 0 549170837 73654272 14753 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14753 603 41 0 17941 0
vsize: 71928
[startup+450.003 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15116 0 0 0 44967 39 0 0 25 0 1 0 549170837 73654272 14758 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14758 603 41 0 17941 0
vsize: 71928
[startup+460.003 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15120 0 0 0 45967 39 0 0 25 0 1 0 549170837 73654272 14762 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14762 603 41 0 17941 0
vsize: 71928
[startup+470.004 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15124 0 0 0 46967 39 0 0 25 0 1 0 549170837 73654272 14766 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14766 603 41 0 17941 0
vsize: 71928
[startup+480.004 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15124 0 0 0 47967 39 0 0 25 0 1 0 549170837 73654272 14766 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 14766 603 41 0 17941 0
vsize: 71928
[startup+490.003 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15126 0 0 0 48967 39 0 0 25 0 1 0 549170837 73789440 14768 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14768 603 41 0 17974 0
vsize: 72060
[startup+500.003 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15127 0 0 0 49968 39 0 0 25 0 1 0 549170837 73789440 14769 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14769 603 41 0 17974 0
vsize: 72060
[startup+510.003 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15129 0 0 0 50968 39 0 0 25 0 1 0 549170837 73789440 14771 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14771 603 41 0 17974 0
vsize: 72060
[startup+520.003 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15131 0 0 0 51967 39 0 0 25 0 1 0 549170837 73789440 14773 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14773 603 41 0 17974 0
vsize: 72060
[startup+530.004 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15132 0 0 0 52968 39 0 0 25 0 1 0 549170837 73789440 14774 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14774 603 41 0 17974 0
vsize: 72060
[startup+540.004 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15133 0 0 0 53968 39 0 0 25 0 1 0 549170837 73789440 14775 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14775 603 41 0 17974 0
vsize: 72060
[startup+550.004 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15134 0 0 0 54968 39 0 0 25 0 1 0 549170837 73789440 14776 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14776 603 41 0 17974 0
vsize: 72060
[startup+560.004 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15137 0 0 0 55968 39 0 0 25 0 1 0 549170837 73789440 14779 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14779 603 41 0 17974 0
vsize: 72060
[startup+570.005 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20444
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15139 0 0 0 56968 39 0 0 25 0 1 0 549170837 73789440 14781 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14781 603 41 0 17974 0
vsize: 72060
[startup+580.005 s]
Raw data (loadavg): 1.08 1.00 0.94 2/54 20497
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15140 0 0 0 57968 39 0 0 25 0 1 0 549170837 73789440 14782 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14782 603 41 0 17974 0
vsize: 72060
[startup+590.004 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 20497
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15143 0 0 0 58968 40 0 0 25 0 1 0 549170837 73789440 14785 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14785 603 41 0 17974 0
vsize: 72060
[startup+600.006 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 20497
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15144 0 0 0 59968 40 0 0 25 0 1 0 549170837 73789440 14786 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14786 603 41 0 17974 0
vsize: 72060
[startup+610.006 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 20497
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15146 0 0 0 60967 41 0 0 25 0 1 0 549170837 73789440 14788 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14788 603 41 0 17974 0
vsize: 72060
[startup+620.007 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 20497
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15147 0 0 0 61967 41 0 0 25 0 1 0 549170837 73789440 14789 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14789 603 41 0 17974 0
vsize: 72060
[startup+630.007 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 20497
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15147 0 0 0 62967 42 0 0 25 0 1 0 549170837 73789440 14789 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14789 603 41 0 17974 0
vsize: 72060
[startup+640.007 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 20497
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15148 0 0 0 63966 42 0 0 25 0 1 0 549170837 73789440 14790 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14790 603 41 0 17974 0
vsize: 72060
[startup+650.007 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15149 0 0 0 64966 43 0 0 25 0 1 0 549170837 73789440 14791 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14791 603 41 0 17974 0
vsize: 72060
[startup+660.008 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15150 0 0 0 65966 43 0 0 25 0 1 0 549170837 73789440 14792 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14792 603 41 0 17974 0
vsize: 72060
[startup+670.008 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15150 0 0 0 66966 43 0 0 25 0 1 0 549170837 73789440 14792 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14792 603 41 0 17974 0
vsize: 72060
[startup+680.008 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15151 0 0 0 67966 43 0 0 25 0 1 0 549170837 73789440 14793 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14793 603 41 0 17974 0
vsize: 72060
[startup+690.008 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15153 0 0 0 68966 44 0 0 25 0 1 0 549170837 73789440 14795 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14795 603 41 0 17974 0
vsize: 72060
[startup+700.008 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15159 0 0 0 69966 44 0 0 25 0 1 0 549170837 73789440 14801 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14801 603 41 0 17974 0
vsize: 72060
[startup+710.008 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15160 0 0 0 70966 44 0 0 25 0 1 0 549170837 73789440 14802 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+720.009 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15160 0 0 0 71966 44 0 0 25 0 1 0 549170837 73789440 14802 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+730.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15160 0 0 0 72966 45 0 0 25 0 1 0 549170837 73789440 14802 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14802 603 41 0 17974 0
vsize: 72060
[startup+740.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15161 0 0 0 73965 45 0 0 25 0 1 0 549170837 73789440 14803 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14803 603 41 0 17974 0
vsize: 72060
[startup+750.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15163 0 0 0 74965 45 0 0 25 0 1 0 549170837 73789440 14805 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14805 603 41 0 17974 0
vsize: 72060
[startup+760.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15164 0 0 0 75965 46 0 0 25 0 1 0 549170837 73789440 14806 4294967295 134512640 134672761 3221224544 3221223712 134565029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14806 603 41 0 17974 0
vsize: 72060
[startup+770.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15166 0 0 0 76964 47 0 0 25 0 1 0 549170837 73789440 14808 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14808 603 41 0 17974 0
vsize: 72060
[startup+780.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15166 0 0 0 77964 47 0 0 25 0 1 0 549170837 73789440 14808 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14808 603 41 0 17974 0
vsize: 72060
[startup+790.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15168 0 0 0 78964 47 0 0 25 0 1 0 549170837 73789440 14810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14810 603 41 0 17974 0
vsize: 72060
[startup+800.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15170 0 0 0 79963 48 0 0 25 0 1 0 549170837 73789440 14812 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14812 603 41 0 17974 0
vsize: 72060
[startup+810.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15173 0 0 0 80963 49 0 0 25 0 1 0 549170837 73789440 14815 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 14815 603 41 0 17974 0
vsize: 72060
[startup+820.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15175 0 0 0 81963 49 0 0 25 0 1 0 549170837 73924608 14817 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14817 603 41 0 18007 0
vsize: 72192
[startup+830.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15175 0 0 0 82962 50 0 0 25 0 1 0 549170837 73924608 14817 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14817 603 41 0 18007 0
vsize: 72192
[startup+840.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15176 0 0 0 83963 50 0 0 25 0 1 0 549170837 73924608 14818 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14818 603 41 0 18007 0
vsize: 72192
[startup+850.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15176 0 0 0 84962 50 0 0 25 0 1 0 549170837 73924608 14818 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14818 603 41 0 18007 0
vsize: 72192
[startup+860.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15177 0 0 0 85962 51 0 0 25 0 1 0 549170837 73924608 14819 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14819 603 41 0 18007 0
vsize: 72192
[startup+870.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15178 0 0 0 86962 51 0 0 25 0 1 0 549170837 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+880.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15178 0 0 0 87962 52 0 0 25 0 1 0 549170837 73924608 14820 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+890.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15178 0 0 0 88962 52 0 0 25 0 1 0 549170837 73924608 14820 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+900.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15178 0 0 0 89962 52 0 0 25 0 1 0 549170837 73924608 14820 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14820 603 41 0 18007 0
vsize: 72192
[startup+910.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15179 0 0 0 90962 53 0 0 25 0 1 0 549170837 73924608 14821 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14821 603 41 0 18007 0
vsize: 72192
[startup+920.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15180 0 0 0 91963 53 0 0 25 0 1 0 549170837 73924608 14822 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+930.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20499
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15180 0 0 0 92963 53 0 0 25 0 1 0 549170837 73924608 14822 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+940.052 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15180 0 0 0 93965 53 0 0 25 0 1 0 549170837 73924608 14822 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14822 603 41 0 18007 0
vsize: 72192
[startup+950.065 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15181 0 0 0 94966 53 0 0 25 0 1 0 549170837 73924608 14823 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+960.065 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15181 0 0 0 95967 53 0 0 25 0 1 0 549170837 73924608 14823 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+970.066 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15181 0 0 0 96967 53 0 0 25 0 1 0 549170837 73924608 14823 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+980.067 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15181 0 0 0 97967 53 0 0 25 0 1 0 549170837 73924608 14823 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+990.066 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15181 0 0 0 98967 53 0 0 25 0 1 0 549170837 73924608 14823 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15181 0 0 0 99967 53 0 0 25 0 1 0 549170837 73924608 14823 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14823 603 41 0 18007 0
vsize: 72192
[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15190 0 0 0 100967 53 0 0 25 0 1 0 549170837 73924608 14832 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14832 603 41 0 18007 0
vsize: 72192
[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15191 0 0 0 101968 53 0 0 25 0 1 0 549170837 73924608 14833 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14833 603 41 0 18007 0
vsize: 72192
[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15191 0 0 0 102968 53 0 0 25 0 1 0 549170837 73924608 14833 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14833 603 41 0 18007 0
vsize: 72192
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15192 0 0 0 103968 54 0 0 25 0 1 0 549170837 73924608 14834 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15192 0 0 0 104968 54 0 0 25 0 1 0 549170837 73924608 14834 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15192 0 0 0 105969 54 0 0 25 0 1 0 549170837 73924608 14834 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14834 603 41 0 18007 0
vsize: 72192
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15193 0 0 0 106969 54 0 0 25 0 1 0 549170837 73924608 14835 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14835 603 41 0 18007 0
vsize: 72192
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15194 0 0 0 107969 54 0 0 25 0 1 0 549170837 73924608 14836 4294967295 134512640 134672761 3221224544 3221223668 134566095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14836 603 41 0 18007 0
vsize: 72192
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15195 0 0 0 108969 54 0 0 25 0 1 0 549170837 73924608 14837 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14837 603 41 0 18007 0
vsize: 72192
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15196 0 0 0 109969 54 0 0 25 0 1 0 549170837 73924608 14838 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14838 603 41 0 18007 0
vsize: 72192
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15197 0 0 0 110970 54 0 0 25 0 1 0 549170837 73924608 14839 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14839 603 41 0 18007 0
vsize: 72192
[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15199 0 0 0 111970 54 0 0 25 0 1 0 549170837 73924608 14841 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14841 603 41 0 18007 0
vsize: 72192
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15200 0 0 0 112970 54 0 0 25 0 1 0 549170837 73924608 14842 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15200 0 0 0 113970 54 0 0 25 0 1 0 549170837 73924608 14842 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15200 0 0 0 114970 54 0 0 25 0 1 0 549170837 73924608 14842 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14842 603 41 0 18007 0
vsize: 72192
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15201 0 0 0 115970 54 0 0 25 0 1 0 549170837 73924608 14843 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14843 603 41 0 18007 0
vsize: 72192
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15202 0 0 0 116970 54 0 0 25 0 1 0 549170837 73924608 14844 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 14844 603 41 0 18007 0
vsize: 72192
[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15203 0 0 0 117970 54 0 0 25 0 1 0 549170837 73924608 14845 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14845 603 41 0 18007 0
vsize: 72192
[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15204 0 0 0 118971 54 0 0 25 0 1 0 549170837 73924608 14846 4294967295 134512640 134672761 3221224544 3221223792 134562135 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14846 603 41 0 18007 0
vsize: 72192
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20501
Raw data (stat): 20444 (minisat+) R 20443 28546 28545 0 -1 0 15204 0 0 0 119971 54 0 0 25 0 1 0 549170837 73924608 14846 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 14846 603 41 0 18007 0
vsize: 72192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 20501
Raw data (stat): 20444 (minisat+) Z 20443 28546 28545 0 -1 12 15206 0 0 0 119971 57 0 0 25 0 1 0 549170837 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.11
CPU time (s): 1200.29
CPU user time (s): 1199.71
CPU system time (s): 0.572912
CPU usage (%): 100.014
Max. virtual memory (Kb): 72192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####