PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        793288 kB
Buffers:         37220 kB
Cached:         166088 kB
SwapCached:         12 kB
Active:          71792 kB
Inactive:       134400 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        793036 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            29400 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:50:52 (client local time) WITH STATUS 10 IN 1200.38 SECONDS
stats: 5185 7 1200.38 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================
c   -- Clauses(.)/Splits(s): ..................................................
c ---[1640]---> BDD-cost:    3
c ---[1638]---> BDD-cost:    5
c ---[1636]---> BDD-cost:    9
c ---[1634]---> BDD-cost:   11
c ---[1632]---> BDD-cost:   11
c ---[1630]---> BDD-cost:   13
c ---[1628]---> BDD-cost:   17
c ---[1626]---> BDD-cost:   21
c ---[1624]---> BDD-cost:   21
c ---[1621]---> BDD-cost:   23
c ---[1618]---> BDD-cost:   23
c ---[1616]---> BDD-cost:   23
c ---[1614]---> BDD-cost:   23
c ---[1612]---> BDD-cost:   23
c ---[1610]---> BDD-cost:   23
c ---[1606]---> BDD-cost:   25
c ---[1604]---> BDD-cost:   23
c ---[1603]---> BDD-cost:   25
c ---[1601]---> BDD-cost:   27
c ---[1599]---> BDD-cost:   15
c ---[1597]---> BDD-cost:   11
c ---[1592]---> BDD-cost:   29
c ---[1590]---> BDD-cost:   31
c ---[1588]---> BDD-cost:   31
c ---[1586]---> BDD-cost:   10
c ---[1584]---> BDD-cost:   15
c ---[1582]---> BDD-cost:   10
c ---[1580]---> BDD-cost:   19
c ---[1578]---> BDD-cost:   31
c ---[1576]---> BDD-cost:    0
c ---[1574]---> BDD-cost:   35
c ---[1572]---> BDD-cost:    9
c ---[1570]---> BDD-cost:   35
c ---[1568]---> BDD-cost:   37
c ---[1566]---> BDD-cost:   37
c ---[1564]---> BDD-cost:   37
c ---[1562]---> BDD-cost:   37
c ---[1560]---> BDD-cost:   39
c ---[1558]---> BDD-cost:   27
c ---[1556]---> BDD-cost:   39
c ---[1554]---> BDD-cost:    0
c ---[1552]---> BDD-cost:   39
c ---[1550]---> BDD-cost:   43
c ---[1548]---> BDD-cost:   45
c ---[1546]---> BDD-cost:   45
c ---[1544]---> BDD-cost:   11
c ---[1541]---> BDD-cost:   45
c ---[1539]---> BDD-cost:   23
c ---[1537]---> BDD-cost:   45
c ---[1536]---> BDD-cost:   45
c ---[1534]---> BDD-cost:   47
c ---[1532]---> BDD-cost:   47
c ---[1530]---> BDD-cost:   47
c ---[1528]---> BDD-cost:   17
c ---[1526]---> BDD-cost:   47
c ---[1524]---> BDD-cost:   45
c ---[1522]---> BDD-cost:   49
c ---[1520]---> BDD-cost:   47
c ---[1518]---> BDD-cost:   49
c ---[1514]---> BDD-cost:   49
c ---[1512]---> BDD-cost:   45
c ---[1510]---> BDD-cost:   35
c ---[1508]---> BDD-cost:   41
c ---[1503]---> BDD-cost:   51
c ---[1501]---> BDD-cost:   51
c ---[1499]---> BDD-cost:   51
c ---[1497]---> BDD-cost:   51
c ---[1495]---> BDD-cost:   45
c ---[1493]---> BDD-cost:   49
c ---[1491]---> BDD-cost:   51
c ---[1490]---> BDD-cost:   47
c ---[1488]---> BDD-cost:   53
c ---[1485]---> BDD-cost:   55
c ---[1483]---> BDD-cost:   53
c ---[1481]---> BDD-cost:   49
c ---[1479]---> BDD-cost:   29
c ---[1478]---> BDD-cost:   55
c ---[1476]---> BDD-cost:   55
c ---[1474]---> BDD-cost:   21
c ---[1472]---> BDD-cost:   55
c ---[1470]---> BDD-cost:   41
c ---[1467]---> BDD-cost:   57
c ---[1465]---> BDD-cost:   57
c ---[1463]---> BDD-cost:   57
c ---[1461]---> BDD-cost:   57
c ---[1459]---> BDD-cost:   55
c ---[1457]---> BDD-cost:   57
c ---[1455]---> BDD-cost:   57
c ---[1453]---> BDD-cost:   57
c ---[1452]---> BDD-cost:   57
c ---[1448]---> BDD-cost:   59
c ---[1446]---> BDD-cost:   19
c ---[1442]---> BDD-cost:   55
c ---[1440]---> BDD-cost:   59
c ---[1438]---> BDD-cost:   57
c ---[1436]---> BDD-cost:   59
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   61
c ---[1430]---> BDD-cost:   57
c ---[1428]---> BDD-cost:   61
c ---[1427]---> BDD-cost:   55
c ---[1425]---> BDD-cost:   61
c ---[1422]---> BDD-cost:   15
c ---[1420]---> BDD-cost:   59
c ---[1418]---> BDD-cost:   63
c ---[1416]---> BDD-cost:   53
c ---[1414]---> BDD-cost:   33
c ---[1412]---> BDD-cost:   65
c ---[1410]---> BDD-cost:   53
c ---[1408]---> BDD-cost:   61
c ---[1406]---> BDD-cost:   65
c ---[1402]---> BDD-cost:   65
c ---[1400]---> BDD-cost:   61
c ---[1398]---> BDD-cost:   65
c ---[1396]---> BDD-cost:   47
c ---[1394]---> BDD-cost:   67
c ---[1392]---> BDD-cost:   67
c ---[1390]---> BDD-cost:   67
c ---[1388]---> BDD-cost:   57
c ---[1386]---> BDD-cost:   49
c ---[1384]---> BDD-cost:   59
c ---[1382]---> BDD-cost:   69
c ---[1380]---> BDD-cost:   53
c ---[1378]---> BDD-cost:   65
c ---[1376]---> BDD-cost:   65
c ---[1374]---> BDD-cost:   67
c ---[1372]---> BDD-cost:   69
c ---[1370]---> BDD-cost:   63
c ---[1368]---> BDD-cost:   71
c ---[1366]---> BDD-cost:   71
c ---[1364]---> BDD-cost:   39
c ---[1362]---> BDD-cost:   71
c ---[1360]---> BDD-cost:   71
c ---[1358]---> BDD-cost:   71
c ---[1356]---> BDD-cost:   71
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   59
c ---[1350]---> BDD-cost:   71
c ---[1348]---> BDD-cost:   73
c ---[1346]---> BDD-cost:   71
c ---[1344]---> BDD-cost:   73
c ---[1343]---> BDD-cost:   45
c ---[1339]---> BDD-cost:   73
c ---[1337]---> BDD-cost:   71
c ---[1334]---> BDD-cost:   31
c ---[1332]---> BDD-cost:   49
c ---[1330]---> BDD-cost:   75
c ---[1327]---> BDD-cost:   75
c ---[1325]---> BDD-cost:   73
c ---[1324]---> BDD-cost:   75
c ---[1323]---> BDD-cost:   53
c ---[1320]---> BDD-cost:   75
c ---[1318]---> BDD-cost:   77
c ---[1316]---> BDD-cost:   63
c ---[1314]---> BDD-cost:    0
c ---[1312]---> BDD-cost:   53
c ---[1310]---> BDD-cost:   77
c ---[1308]---> BDD-cost:   73
c ---[1306]---> BDD-cost:   79
c ---[1304]---> BDD-cost:   79
c ---[1302]---> BDD-cost:   79
c ---[1300]---> BDD-cost:   55
c ---[1298]---> BDD-cost:   51
c ---[1296]---> BDD-cost:   77
c ---[1294]---> BDD-cost:   13
c ---[1292]---> BDD-cost:   81
c ---[1290]---> BDD-cost:   55
c ---[1288]---> BDD-cost:   81
c ---[1286]---> BDD-cost:   75
c ---[1284]---> BDD-cost:   79
c ---[1283]---> BDD-cost:   81
c ---[1278]---> BDD-cost:   81
c ---[1277]---> BDD-cost:   81
c ---[1276]---> BDD-cost:   77
c ---[1272]---> BDD-cost:   81
c ---[1270]---> BDD-cost:   77
c ---[1268]---> BDD-cost:   61
c ---[1265]---> BDD-cost:   75
c ---[1263]---> BDD-cost:   83
c ---[1262]---> BDD-cost:   77
c ---[1261]---> BDD-cost:   83
c ---[1258]---> BDD-cost:   83
c ---[1256]---> BDD-cost:    0
c ---[1254]---> BDD-cost:   83
c ---[1252]---> BDD-cost:   67
c ---[1250]---> BDD-cost:   81
c ---[1248]---> BDD-cost:   43
c ---[1246]---> BDD-cost:   85
c ---[1244]---> BDD-cost:   85
c ---[1242]---> BDD-cost:   47
c ---[1240]---> BDD-cost:   71
c ---[1238]---> BDD-cost:   83
c ---[1236]---> BDD-cost:   87
c ---[1234]---> BDD-cost:   87
c ---[1232]---> BDD-cost:   35
c ---[1230]---> BDD-cost:   79
c ---[1228]---> BDD-cost:   89
c ---[1226]---> BDD-cost:   89
c ---[1224]---> BDD-cost:   89
c ---[1222]---> BDD-cost:   89
c ---[1220]---> BDD-cost:   77
c ---[1218]---> BDD-cost:    9
c ---[1216]---> BDD-cost:   91
c ---[1214]---> BDD-cost:   91
c ---[1212]---> BDD-cost:   77
c ---[1210]---> BDD-cost:   89
c ---[1208]---> BDD-cost:   91
c ---[1206]---> BDD-cost:   87
c ---[1205]---> BDD-cost:   93
c ---[1203]---> BDD-cost:   91
c ---[1201]---> BDD-cost:    7
c ---[1199]---> BDD-cost:   93
c ---[1197]---> BDD-cost:   61
c ---[1195]---> BDD-cost:   57
c ---[1193]---> BDD-cost:   55
c ---[1191]---> BDD-cost:   67
c ---[1189]---> BDD-cost:   89
c ---[1186]---> BDD-cost:   59
c ---[1184]---> BDD-cost:   95
c ---[1182]---> BDD-cost:   93
c ---[1178]---> BDD-cost:   31
c ---[1176]---> BDD-cost:   97
c ---[1174]---> BDD-cost:   95
c ---[1172]---> BDD-cost:   97
c ---[1170]---> BDD-cost:   91
c ---[1168]---> BDD-cost:   69
c ---[1166]---> BDD-cost:   95
c ---[1164]---> BDD-cost:   91
c ---[1162]---> BDD-cost:   77
c ---[1160]---> BDD-cost:    5
c ---[1158]---> BDD-cost:   91
c ---[1156]---> BDD-cost:   99
c ---[1154]---> BDD-cost:   79
c ---[1152]---> BDD-cost:   91
c ---[1150]---> BDD-cost:   99
c ---[1148]---> BDD-cost:   95
c ---[1146]---> BDD-cost:   99
c ---[1144]---> BDD-cost:   97
c ---[1142]---> BDD-cost:  101
c ---[1140]---> BDD-cost:   99
c ---[1138]---> BDD-cost:   87
c ---[1136]---> BDD-cost:  101
c ---[1132]---> BDD-cost:  103
c ---[1130]---> BDD-cost:  103
c ---[1128]---> BDD-cost:  101
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  103
c ---[1122]---> BDD-cost:   95
c ---[1120]---> BDD-cost:   99
c ---[1118]---> BDD-cost:  105
c ---[1116]---> BDD-cost:   85
c ---[1114]---> BDD-cost:  105
c ---[1112]---> BDD-cost:   97
c ---[1110]---> BDD-cost:  105
c ---[1108]---> BDD-cost:  105
c ---[1105]---> BDD-cost:  107
c ---[1104]---> BDD-cost:   81
c ---[1101]---> BDD-cost:  105
c ---[1099]---> BDD-cost:  105
c ---[1097]---> BDD-cost:   19
c ---[1095]---> BDD-cost:  107
c ---[1093]---> BDD-cost:  107
c ---[1090]---> BDD-cost:  107
c ---[1089]---> BDD-cost:  105
c ---[1088]---> BDD-cost:    0
c ---[1085]---> BDD-cost:  103
c ---[1083]---> BDD-cost:  109
c ---[1081]---> BDD-cost:   95
c ---[1079]---> BDD-cost:  109
c ---[1075]---> BDD-cost:  109
c ---[1074]---> BDD-cost:  109
c ---[1071]---> BDD-cost:   77
c ---[1069]---> BDD-cost:  109
c ---[1067]---> BDD-cost:  109
c ---[1065]---> BDD-cost:  105
c ---[1064]---> BDD-cost:   53
c ---[1063]---> BDD-cost:  107
c ---[1060]---> BDD-cost:  111
c ---[1058]---> BDD-cost:  103
c ---[1056]---> BDD-cost:  111
c ---[1054]---> BDD-cost:  111
c ---[1050]---> BDD-cost:  111
c ---[1048]---> BDD-cost:  103
c ---[1046]---> BDD-cost:   79
c ---[1045]---> BDD-cost:  111
c ---[1043]---> BDD-cost:  101
c ---[1041]---> BDD-cost:  113
c ---[1039]---> BDD-cost:  109
c ---[1036]---> BDD-cost:  111
c ---[1034]---> BDD-cost:  105
c ---[1032]---> BDD-cost:  111
c ---[1029]---> BDD-cost:  115
c ---[1027]---> BDD-cost:  103
c ---[1026]---> BDD-cost:  115
c ---[1024]---> BDD-cost:  115
c ---[1022]---> BDD-cost:  101
c ---[1016]---> BDD-cost:  115
c ---[1014]---> BDD-cost:  115
c ---[1013]---> BDD-cost:   83
c ---[1011]---> BDD-cost:   31
c ---[1010]---> BDD-cost:   51
c ---[1008]---> BDD-cost:  117
c ---[1006]---> BDD-cost:   97
c ---[1004]---> BDD-cost:  117
c ---[1002]---> BDD-cost:   99
c ---[1000]---> BDD-cost:  117
c ---[ 998]---> BDD-cost:  117
c ---[ 996]---> BDD-cost:  119
c ---[ 994]---> BDD-cost:   83
c ---[ 992]---> BDD-cost:  119
c ---[ 990]---> BDD-cost:  117
c ---[ 988]---> BDD-cost:  117
c ---[ 986]---> BDD-cost:  117
c ---[ 984]---> BDD-cost:  121
c ---[ 982]---> BDD-cost:  121
c ---[ 980]---> BDD-cost:  113
c ---[ 978]---> BDD-cost:  119
c ---[ 976]---> BDD-cost:  121
c ---[ 974]---> BDD-cost:  109
c ---[ 972]---> BDD-cost:   71
c ---[ 970]---> BDD-cost:    3
c ---[ 969]---> BDD-cost:  123
c ---[ 967]---> BDD-cost:  123
c ---[ 965]---> BDD-cost:  123
c ---[ 962]---> BDD-cost:  123
c ---[ 959]---> BDD-cost:  109
c ---[ 957]---> BDD-cost:  117
c ---[ 956]---> BDD-cost:  123
c ---[ 954]---> BDD-cost:  107
c ---[ 952]---> BDD-cost:  125
c ---[ 950]---> BDD-cost:  127
c ---[ 948]---> BDD-cost:  105
c ---[ 946]---> BDD-cost:  127
c ---[ 944]---> BDD-cost:  127
c ---[ 942]---> BDD-cost:    0
c ---[ 940]---> BDD-cost:  115
c ---[ 938]---> BDD-cost:  117
c ---[ 936]---> BDD-cost:  129
c ---[ 934]---> BDD-cost:  121
c ---[ 932]---> BDD-cost:  115
c ---[ 930]---> BDD-cost:  129
c ---[ 928]---> BDD-cost:  131
c ---[ 926]---> BDD-cost:   43
c ---[ 925]---> BDD-cost:  131
c ---[ 923]---> BDD-cost:  131
c ---[ 920]---> BDD-cost:    0
c ---[ 918]---> BDD-cost:  133
c ---[ 916]---> BDD-cost:  131
c ---[ 914]---> BDD-cost:  133
c ---[ 910]---> BDD-cost:  133
c ---[ 908]---> BDD-cost:  133
c ---[ 906]---> BDD-cost:   17
c ---[ 904]---> BDD-cost:  135
c ---[ 902]---> BDD-cost:  125
c ---[ 900]---> BDD-cost:   93
c ---[ 898]---> BDD-cost:   97
c ---[ 896]---> BDD-cost:  135
c ---[ 893]---> BDD-cost:  135
c ---[ 892]---> BDD-cost:  135
c ---[ 890]---> BDD-cost:  131
c ---[ 888]---> BDD-cost:    0
c ---[ 886]---> BDD-cost:  135
c ---[ 884]---> BDD-cost:  135
c ---[ 881]---> BDD-cost:  137
c ---[ 879]---> BDD-cost:  137
c ---[ 878]---> BDD-cost:    0
c ---[ 876]---> BDD-cost:  137
c ---[ 874]---> BDD-cost:  135
c ---[ 872]---> BDD-cost:  127
c ---[ 870]---> BDD-cost:  131
c ---[ 869]---> BDD-cost:  127
c ---[ 867]---> BDD-cost:   75
c ---[ 865]---> BDD-cost:  133
c ---[ 862]---> BDD-cost:  139
c ---[ 860]---> BDD-cost:  101
c ---[ 858]---> BDD-cost:  137
c ---[ 856]---> BDD-cost:  125
c ---[ 854]---> BDD-cost:  129
c ---[ 852]---> BDD-cost:  139
c ---[ 850]---> BDD-cost:  141
c ---[ 848]---> BDD-cost:   65
c ---[ 846]---> BDD-cost:   41
c ---[ 844]---> BDD-cost:  143
c ---[ 842]---> BDD-cost:  133
c ---[ 840]---> BDD-cost:  143
c ---[ 838]---> BDD-cost:  109
c ---[ 836]---> BDD-cost:   73
c ---[ 834]---> BDD-cost:   97
c ---[ 832]---> BDD-cost:  145
c ---[ 830]---> BDD-cost:  145
c ---[ 828]---> BDD-cost:   43
c ---[ 826]---> BDD-cost:  139
c ---[ 824]---> BDD-cost:  123
c ---[ 822]---> BDD-cost:  147
c ---[ 820]---> BDD-cost:  147
c ---[ 818]---> BDD-cost:  145
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  147
c ---[ 812]---> BDD-cost:  147
c ---[ 810]---> BDD-cost:  131
c ---[ 808]---> BDD-cost:  145
c ---[ 806]---> BDD-cost:  147
c ---[ 804]---> BDD-cost:  147
c ---[ 802]---> BDD-cost:  141
c ---[ 800]---> BDD-cost:  147
c ---[ 798]---> BDD-cost:  139
c ---[ 796]---> BDD-cost:   87
c ---[ 794]---> BDD-cost:  149
c ---[ 792]---> BDD-cost:  149
c ---[ 790]---> BDD-cost:  147
c ---[ 788]---> BDD-cost:  149
c ---[ 786]---> BDD-cost:  149
c ---[ 784]---> BDD-cost:  137
c ---[ 780]---> BDD-cost:   99
c ---[ 778]---> BDD-cost:  149
c ---[ 776]---> BDD-cost:  149
c ---[ 774]---> BDD-cost:  139
c ---[ 772]---> BDD-cost:  151
c ---[ 770]---> BDD-cost:  151
c ---[ 768]---> BDD-cost:  149
c ---[ 766]---> BDD-cost:  151
c ---[ 764]---> BDD-cost:  147
c ---[ 762]---> BDD-cost:   83
c ---[ 760]---> BDD-cost:  151
c ---[ 758]---> BDD-cost:   13
c ---[ 756]---> BDD-cost:  153
c ---[ 754]---> BDD-cost:   87
c ---[ 750]---> BDD-cost:  155
c ---[ 748]---> BDD-cost:  151
c ---[ 746]---> BDD-cost:  155
c ---[ 744]---> BDD-cost:  155
c ---[ 742]---> BDD-cost:    0
c ---[ 740]---> BDD-cost:  157
c ---[ 738]---> BDD-cost:  147
c ---[ 735]---> BDD-cost:  157
c ---[ 733]---> BDD-cost:  157
c ---[ 730]---> BDD-cost:  159
c ---[ 728]---> BDD-cost:  119
c ---[ 724]---> BDD-cost:  159
c ---[ 722]---> BDD-cost:  159
c ---[ 720]---> BDD-cost:  149
c ---[ 718]---> BDD-cost:   61
c ---[ 716]---> BDD-cost:  161
c ---[ 714]---> BDD-cost:  141
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  165
c ---[ 708]---> BDD-cost:  165
c ---[ 706]---> BDD-cost:  165
c ---[ 703]---> BDD-cost:  167
c ---[ 701]---> BDD-cost:  167
c ---[ 699]---> BDD-cost:   83
c ---[ 697]---> BDD-cost:  167
c ---[ 695]---> BDD-cost:  165
c ---[ 693]---> BDD-cost:  165
c ---[ 692]---> BDD-cost:  155
c ---[ 690]---> BDD-cost:  163
c ---[ 688]---> BDD-cost:  165
c ---[ 686]---> BDD-cost:  161
c ---[ 684]---> BDD-cost:  139
c ---[ 682]---> BDD-cost:  167
c ---[ 680]---> BDD-cost:  169
c ---[ 678]---> BDD-cost:    0
c ---[ 676]---> BDD-cost:  169
c ---[ 674]---> BDD-cost:  139
c ---[ 672]---> BDD-cost:  161
c ---[ 670]---> BDD-cost:  167
c ---[ 668]---> BDD-cost:  119
c ---[ 666]---> BDD-cost:  155
c ---[ 664]---> BDD-cost:  169
c ---[ 662]---> BDD-cost:  109
c ---[ 660]---> BDD-cost:  151
c ---[ 658]---> BDD-cost:  157
c ---[ 656]---> BDD-cost:  173
c ---[ 654]---> BDD-cost:  155
c ---[ 652]---> BDD-cost:  165
c ---[ 650]---> BDD-cost:  111
c ---[ 648]---> BDD-cost:  129
c ---[ 646]---> BDD-cost:  173
c ---[ 644]---> BDD-cost:  177
c ---[ 642]---> BDD-cost:  177
c ---[ 640]---> BDD-cost:    0
c ---[ 638]---> BDD-cost:  173
c ---[ 636]---> BDD-cost:  177
c ---[ 634]---> BDD-cost:  103
c ---[ 632]---> BDD-cost:  167
c ---[ 630]---> BDD-cost:  161
c ---[ 628]---> BDD-cost:  179
c ---[ 626]---> BDD-cost:  181
c ---[ 624]---> BDD-cost:  165
c ---[ 622]---> BDD-cost:  183
c ---[ 618]---> BDD-cost:  183
c ---[ 616]---> BDD-cost:   55
c ---[ 613]---> BDD-cost:  185
c ---[ 611]---> BDD-cost:  185
c ---[ 609]---> BDD-cost:  185
c ---[ 607]---> BDD-cost:  183
c ---[ 606]---> BDD-cost:  169
c ---[ 602]---> BDD-cost:  187
c ---[ 600]---> BDD-cost:  187
c ---[ 598]---> BDD-cost:  177
c ---[ 596]---> BDD-cost:  185
c ---[ 594]---> BDD-cost:  187
c ---[ 592]---> BDD-cost:  189
c ---[ 591]---> BDD-cost:  189
c ---[ 589]---> BDD-cost:    0
c ---[ 587]---> BDD-cost:  163
c ---[ 584]---> BDD-cost:    0
c ---[ 582]---> BDD-cost:  191
c ---[ 580]---> BDD-cost:  151
c ---[ 578]---> BDD-cost:  101
c ---[ 576]---> BDD-cost:  191
c ---[ 574]---> BDD-cost:  193
c ---[ 572]---> BDD-cost:  193
c ---[ 570]---> BDD-cost:  191
c ---[ 568]---> BDD-cost:  187
c ---[ 566]---> BDD-cost:  123
c ---[ 564]---> BDD-cost:  177
c ---[ 562]---> BDD-cost:  195
c ---[ 560]---> BDD-cost:  197
c ---[ 558]---> BDD-cost:  197
c ---[ 556]---> BDD-cost:  191
c ---[ 554]---> BDD-cost:  201
c ---[ 552]---> BDD-cost:  201
c ---[ 550]---> BDD-cost:  201
c ---[ 548]---> BDD-cost:  179
c ---[ 546]---> BDD-cost:  205
c ---[ 544]---> BDD-cost:  205
c ---[ 542]---> BDD-cost:  201
c ---[ 540]---> BDD-cost:  207
c ---[ 538]---> BDD-cost:  205
c ---[ 536]---> BDD-cost:  209
c ---[ 534]---> BDD-cost:  209
c ---[ 532]---> BDD-cost:  145
c ---[ 530]---> BDD-cost:  157
c ---[ 526]---> BDD-cost:  211
c ---[ 524]---> BDD-cost:  203
c ---[ 522]---> BDD-cost:  211
c ---[ 520]---> BDD-cost:  211
c ---[ 518]---> BDD-cost:  215
c ---[ 516]---> BDD-cost:  181
c ---[ 514]---> BDD-cost:  211
c ---[ 512]---> BDD-cost:  187
c ---[ 510]---> BDD-cost:  127
c ---[ 508]---> BDD-cost:  215
c ---[ 506]---> BDD-cost:  203
c ---[ 504]---> BDD-cost:   71
c ---[ 502]---> BDD-cost:  207
c ---[ 500]---> BDD-cost:  217
c ---[ 498]---> BDD-cost:   89
c ---[ 496]---> BDD-cost:  207
c ---[ 494]---> BDD-cost:  221
c ---[ 492]---> BDD-cost:  223
c ---[ 490]---> BDD-cost:  125
c ---[ 488]---> BDD-cost:  219
c ---[ 486]---> BDD-cost:  225
c ---[ 484]---> BDD-cost:  225
c ---[ 482]---> BDD-cost:  223
c ---[ 480]---> BDD-cost:  225
c ---[ 478]---> BDD-cost:  225
c ---[ 476]---> BDD-cost:  225
c ---[ 475]---> BDD-cost:  225
c ---[ 473]---> BDD-cost:  225
c ---[ 470]---> BDD-cost:  107
c ---[ 468]---> BDD-cost:  229
c ---[ 466]---> BDD-cost:  229
c ---[ 464]---> BDD-cost:  229
c ---[ 462]---> BDD-cost:  233
c ---[ 460]---> BDD-cost:  229
c ---[ 457]---> BDD-cost:  233
c ---[ 455]---> BDD-cost:  231
c ---[ 454]---> BDD-cost:  233
c ---[ 452]---> BDD-cost:  235
c ---[ 450]---> BDD-cost:  231
c ---[ 448]---> BDD-cost:  233
c ---[ 446]---> BDD-cost:  237
c ---[ 444]---> BDD-cost:  175
c ---[ 442]---> BDD-cost:  201
c ---[ 440]---> BDD-cost:  223
c ---[ 438]---> BDD-cost:  239
c ---[ 436]---> BDD-cost:   87
c ---[ 434]---> BDD-cost:  171
c ---[ 432]---> BDD-cost:  237
c ---[ 430]---> BDD-cost:  239
c ---[ 426]---> BDD-cost:  239
c ---[ 424]---> BDD-cost:  207
c ---[ 422]---> BDD-cost:  241
c ---[ 420]---> BDD-cost:  237
c ---[ 418]---> BDD-cost:  241
c ---[ 416]---> BDD-cost:  221
c ---[ 414]---> BDD-cost:  243
c ---[ 412]---> BDD-cost:  243
c ---[ 410]---> BDD-cost:   65
c ---[ 408]---> BDD-cost:  145
c ---[ 406]---> BDD-cost:  217
c ---[ 404]---> BDD-cost:  233
c ---[ 402]---> BDD-cost:  245
c ---[ 400]---> BDD-cost:  241
c ---[ 398]---> BDD-cost:  247
c ---[ 396]---> BDD-cost:  197
c ---[ 394]---> BDD-cost:  245
c ---[ 392]---> BDD-cost:  247
c ---[ 390]---> BDD-cost:  249
c ---[ 388]---> BDD-cost:  185
c ---[ 386]---> BDD-cost:  251
c ---[ 384]---> BDD-cost:  253
c ---[ 382]---> BDD-cost:  251
c ---[ 380]---> BDD-cost:  249
c ---[ 378]---> BDD-cost:  251
c ---[ 376]---> BDD-cost:  249
c ---[ 374]---> BDD-cost:  255
c ---[ 372]---> BDD-cost:  255
c ---[ 370]---> BDD-cost:  255
c ---[ 368]---> BDD-cost:  105
c ---[ 366]---> BDD-cost:   43
c ---[ 364]---> BDD-cost:  257
c ---[ 362]---> BDD-cost:  207
c ---[ 360]---> BDD-cost:  257
c ---[ 358]---> BDD-cost:  249
c ---[ 356]---> BDD-cost:  243
c ---[ 354]---> BDD-cost:  259
c ---[ 353]---> BDD-cost:  205
c ---[ 351]---> BDD-cost:  259
c ---[ 349]---> BDD-cost:  201
c ---[ 347]---> BDD-cost:  257
c ---[ 344]---> BDD-cost:  221
c ---[ 342]---> BDD-cost:  217
c ---[ 340]---> BDD-cost:  261
c ---[ 338]---> BDD-cost:  259
c ---[ 336]---> BDD-cost:  257
c ---[ 334]---> BDD-cost:  191
c ---[ 332]---> BDD-cost:   99
c ---[ 330]---> BDD-cost:  263
c ---[ 328]---> BDD-cost:  267
c ---[ 326]---> BDD-cost:  267
c ---[ 324]---> BDD-cost:  265
c ---[ 322]---> BDD-cost:  261
c ---[ 320]---> BDD-cost:  267
c ---[ 318]---> BDD-cost:  267
c ---[ 316]---> BDD-cost:    0
c ---[ 314]---> BDD-cost:  143
c ---[ 312]---> BDD-cost:  267
c ---[ 310]---> BDD-cost:  245
c ---[ 308]---> BDD-cost:  249
c ---[ 306]---> BDD-cost:   33
c ---[ 304]---> BDD-cost:  273
c ---[ 302]---> BDD-cost:  269
c ---[ 300]---> BDD-cost:  261
c ---[ 298]---> BDD-cost:  275
c ---[ 296]---> BDD-cost:  271
c ---[ 294]---> BDD-cost:  271
c ---[ 292]---> BDD-cost:  273
c ---[ 290]---> BDD-cost:  277
c ---[ 288]---> BDD-cost:  277
c ---[ 286]---> BDD-cost:  277
c ---[ 284]---> BDD-cost:  277
c ---[ 282]---> BDD-cost:  279
c ---[ 280]---> BDD-cost:  277
c ---[ 278]---> BDD-cost:  209
c ---[ 276]---> BDD-cost:  267
c ---[ 274]---> BDD-cost:  283
c ---[ 272]---> BDD-cost:  243
c ---[ 270]---> BDD-cost:  281
c ---[ 268]---> BDD-cost:  281
c ---[ 266]---> BDD-cost:  275
c ---[ 264]---> BDD-cost:  215
c ---[ 262]---> BDD-cost:  283
c ---[ 260]---> BDD-cost:  169
c ---[ 258]---> BDD-cost:  225
c ---[ 256]---> BDD-cost:  287
c ---[ 254]---> BDD-cost:  259
c ---[ 252]---> BDD-cost:  261
c ---[ 250]---> BDD-cost:  279
c ---[ 248]---> BDD-cost:  289
c ---[ 246]---> BDD-cost:  249
c ---[ 244]---> BDD-cost:  231
c ---[ 242]---> BDD-cost:  287
c ---[ 240]---> BDD-cost:  287
c ---[ 238]---> BDD-cost:  291
c ---[ 236]---> BDD-cost:  293
c ---[ 234]---> BDD-cost:   49
c ---[ 232]---> BDD-cost:  299
c ---[ 230]---> BDD-cost:  259
c ---[ 228]---> BDD-cost:  291
c ---[ 226]---> BDD-cost:   81
c ---[ 224]---> BDD-cost:  289
c ---[ 222]---> BDD-cost:  303
c ---[ 220]---> BDD-cost:  305
c ---[ 219]---> BDD-cost:  309
c ---[ 217]---> BDD-cost:  303
c ---[ 214]---> BDD-cost:  309
c ---[ 212]---> BDD-cost:  311
c ---[ 210]---> BDD-cost:  309
c ---[ 208]---> BDD-cost:  313
c ---[ 206]---> BDD-cost:  287
c ---[ 204]---> BDD-cost:  311
c ---[ 202]---> BDD-cost:  309
c ---[ 200]---> BDD-cost:  315
c ---[ 198]---> BDD-cost:  317
c ---[ 195]---> BDD-cost:  319
c ---[ 194]---> BDD-cost:  315
c ---[ 192]---> BDD-cost:  311
c ---[ 190]---> BDD-cost:  321
c ---[ 187]---> BDD-cost:  201
c ---[ 186]---> BDD-cost:  321
c ---[ 184]---> BDD-cost:  319
c ---[ 182]---> BDD-cost:  257
c ---[ 180]---> BDD-cost:  249
c ---[ 178]---> BDD-cost:  315
c ---[ 176]---> BDD-cost:  329
c ---[ 174]---> BDD-cost:  197
c ---[ 172]---> BDD-cost:  331
c ---[ 170]---> BDD-cost:  227
c ---[ 168]---> BDD-cost:  339
c ---[ 166]---> BDD-cost:  341
c ---[ 164]---> BDD-cost:  305
c ---[ 162]---> BDD-cost:  173
c ---[ 160]---> BDD-cost:  261
c ---[ 158]---> BDD-cost:  307
c ---[ 156]---> BDD-cost:  345
c ---[ 154]---> BDD-cost:  345
c ---[ 152]---> BDD-cost:  295
c ---[ 150]---> BDD-cost:  345
c ---[ 148]---> BDD-cost:  275
c ---[ 146]---> BDD-cost:  243
c ---[ 144]---> BDD-cost:  349
c ---[ 142]---> BDD-cost:  345
c ---[ 140]---> BDD-cost:  345
c ---[ 138]---> BDD-cost:  353
c ---[ 136]---> BDD-cost:  291
c ---[ 134]---> BDD-cost:  355
c ---[ 132]---> BDD-cost:  345
c ---[ 130]---> BDD-cost:  347
c ---[ 128]---> BDD-cost:  359
c ---[ 126]---> BDD-cost:  287
c ---[ 124]---> BDD-cost:  135
c ---[ 122]---> BDD-cost:  369
c ---[ 120]---> BDD-cost:  365
c ---[ 118]---> BDD-cost:  365
c ---[ 116]---> BDD-cost:  367
c ---[ 114]---> BDD-cost:  371
c ---[ 112]---> BDD-cost:  103
c ---[ 110]---> BDD-cost:  375
c ---[ 108]---> BDD-cost:  375
c ---[ 106]---> BDD-cost:    0
c ---[ 104]---> BDD-cost:  141
c ---[ 102]---> BDD-cost:  385
c ---[ 100]---> BDD-cost:  361
c ---[  97]---> BDD-cost:  385
c ---[  95]---> BDD-cost:  383
c ---[  94]---> BDD-cost:  351
c ---[  92]---> BDD-cost:  387
c ---[  90]---> BDD-cost:  247
c ---[  88]---> BDD-cost:  383
c ---[  86]---> BDD-cost:  353
c ---[  84]---> BDD-cost:  381
c ---[  82]---> BDD-cost:  389
c ---[  80]---> BDD-cost:  391
c ---[  78]---> BDD-cost:  343
c ---[  76]---> BDD-cost:  365
c ---[  74]---> BDD-cost:  291
c ---[  72]---> BDD-cost:  391
c ---[  70]---> BDD-cost:   25
c ---[  68]---> BDD-cost:  387
c ---[  66]---> BDD-cost:  403
c ---[  64]---> BDD-cost:  391
c ---[  62]---> BDD-cost:  405
c ---[  60]---> BDD-cost:  407
c ---[  58]---> BDD-cost:  363
c ---[  56]---> BDD-cost:  323
c ---[  54]---> BDD-cost:  333
c ---[  52]---> BDD-cost:  365
c ---[  48]---> BDD-cost:  419
c ---[  46]---> BDD-cost:  419
c ---[  44]---> BDD-cost:  377
c ---[  42]---> BDD-cost:  427
c ---[  40]---> BDD-cost:  431
c ---[  38]---> BDD-cost:  405
c ---[  36]---> BDD-cost:  433
c ---[  34]---> BDD-cost:  441
c ---[  32]---> BDD-cost:  357
c ---[  30]---> BDD-cost:  443
c ---[  28]---> BDD-cost:  411
c ---[  26]---> BDD-cost:  457
c ---[  24]---> BDD-cost:  333
c ---[  22]---> BDD-cost:  471
c ---[  20]---> BDD-cost:  455
c ---[  18]---> BDD-cost:  487
c ---[  16]---> BDD-cost:  441
c ---[  14]---> BDD-cost:  299
c ---[  12]---> BDD-cost:  603
c ---[  10]---> BDD-cost:  441
c ---[   8]---> BDD-cost:  653
c ---[   6]---> BDD-cost:  673
c ---[   4]---> BDD-cost:  689
c ---[   2]---> BDD-cost:  531
c ---[   0]---> BDD-cost:  685
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  310077   809974 |   93023       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/132106          
c   -- var.elim.:  2000/132106          
c   -- var.elim.:  3000/132106          
c   -- var.elim.:  4000/132106          
c   -- var.elim.:  5000/132106          
c   -- var.elim.:  6000/132106          
c   -- var.elim.:  7000/132106          
c   -- var.elim.:  8000/132106          
c   -- var.elim.:  9000/132106          
c   -- var.elim.:  10000/132106          
c   -- var.elim.:  11000/132106          
c   -- var.elim.:  12000/132106          
c   -- var.elim.:  13000/132106          
c   -- var.elim.:  14000/132106          
c   -- var.elim.:  15000/132106          
c   -- var.elim.:  16000/132106          
c   -- var.elim.:  17000/132106          
c   -- var.elim.:  18000/132106          
c   -- var.elim.:  19000/132106          
c   -- var.elim.:  20000/132106          
c   -- var.elim.:  21000/132106          
c   -- var.elim.:  22000/132106          
c   -- var.elim.:  23000/132106          
c   -- var.elim.:  24000/132106          
c   -- var.elim.:  25000/132106          
c   -- var.elim.:  26000/132106          
c   -- var.elim.:  27000/132106          
c   -- var.elim.:  28000/132106          
c   -- var.elim.:  29000/132106          
c   -- var.elim.:  30000/132106          
c   -- var.elim.:  31000/132106          
c   -- var.elim.:  32000/132106          
c   -- var.elim.:  33000/132106          
c   -- var.elim.:  34000/132106          
c   -- var.elim.:  35000/132106          
c   -- var.elim.:  36000/132106          
c   -- var.elim.:  37000/132106          
c   -- var.elim.:  38000/132106          
c   -- var.elim.:  39000/132106          
c   -- var.elim.:  40000/132106          
c   -- var.elim.:  41000/132106          
c   -- var.elim.:  42000/132106          
c   -- var.elim.:  43000/132106          
c   -- var.elim.:  44000/132106          
c   -- var.elim.:  45000/132106          
c   -- var.elim.:  46000/132106          
c   -- var.elim.:  47000/132106          
c   -- var.elim.:  48000/132106          
c   -- var.elim.:  49000/132106          
c   -- var.elim.:  50000/132106          
c   -- var.elim.:  51000/132106          
c   -- var.elim.:  52000/132106          
c   -- var.elim.:  53000/132106          
c   -- var.elim.:  54000/132106          
c   -- var.elim.:  55000/132106          
c   -- var.elim.:  56000/132106          
c   -- var.elim.:  57000/132106          
c   -- var.elim.:  58000/132106          
c   -- var.elim.:  59000/132106          
c   -- var.elim.:  60000/132106          
c   -- var.elim.:  61000/132106          
c   -- var.elim.:  62000/132106          
c   -- var.elim.:  63000/132106          
c   -- var.elim.:  64000/132106          
c   -- var.elim.:  65000/132106          
c   -- var.elim.:  66000/132106          
c   -- var.elim.:  67000/132106          
c   -- var.elim.:  68000/132106          
c   -- var.elim.:  69000/132106          
c   -- var.elim.:  70000/132106          
c   -- var.elim.:  71000/132106          
c   -- var.elim.:  72000/132106          
c   -- var.elim.:  73000/132106          
c   -- var.elim.:  74000/132106          
c   -- var.elim.:  75000/132106          
c   -- var.elim.:  76000/132106          
c   -- var.elim.:  77000/132106          
c   -- var.elim.:  78000/132106          
c   -- var.elim.:  79000/132106          
c   -- var.elim.:  80000/132106          
c   -- var.elim.:  81000/132106          
c   -- var.elim.:  82000/132106          
c   -- var.elim.:  83000/132106          
c   -- var.elim.:  84000/132106          
c   -- var.elim.:  85000/132106          
c   -- var.elim.:  86000/132106          
c   -- var.elim.:  87000/132106          
c   -- var.elim.:  88000/132106          
c   -- var.elim.:  89000/132106          
c   -- var.elim.:  90000/132106          
c   -- var.elim.:  91000/132106          
c   -- var.elim.:  92000/132106          
c   -- var.elim.:  93000/132106          
c   -- var.elim.:  94000/132106          
c   -- var.elim.:  95000/132106          
c   -- var.elim.:  96000/132106          
c   -- var.elim.:  97000/132106          
c   -- var.elim.:  98000/132106          
c   -- var.elim.:  99000/132106          
c   -- var.elim.:  100000/132106          
c   -- var.elim.:  101000/132106          
c   -- var.elim.:  102000/132106          
c   -- var.elim.:  103000/132106          
c   -- var.elim.:  104000/132106          
c   -- var.elim.:  105000/132106          
c   -- var.elim.:  106000/132106          
c   -- var.elim.:  107000/132106          
c   -- var.elim.:  108000/132106          
c   -- var.elim.:  109000/132106          
c   -- var.elim.:  110000/132106          
c   -- var.elim.:  111000/132106          
c   -- var.elim.:  112000/132106          
c   -- var.elim.:  113000/132106          
c   -- var.elim.:  114000/132106          
c   -- var.elim.:  115000/132106          
c   -- var.elim.:  116000/132106          
c   -- var.elim.:  117000/132106          
c   -- var.elim.:  118000/132106          
c   -- var.elim.:  119000/132106          
c   -- var.elim.:  120000/132106          
c   -- var.elim.:  121000/132106          
c   -- var.elim.:  122000/132106          
c   -- var.elim.:  123000/132106          
c   -- var.elim.:  124000/132106          
c   -- var.elim.:  125000/132106          
c   -- var.elim.:  126000/132106          
c   -- var.elim.:  127000/132106          
c   -- var.elim.:  128000/132106          
c   -- var.elim.:  129000/132106          
c   -- var.elim.:  130000/132106          
c   -- var.elim.:  131000/132106          
c   -- var.elim.:  132000/132106          
c   -- var.elim.:  132106/132106          
c   -- var.elim.:  1000/5844          
c   -- var.elim.:  2000/5844          
c   -- var.elim.:  3000/5844          
c   -- var.elim.:  4000/5844          
c   -- var.elim.:  5000/5844          
c   -- var.elim.:  5844/5844          
c   -- subsuming                       
c   -- var.elim.:  1000/3926          
c   -- var.elim.:  2000/3926          
c   -- var.elim.:  3000/3926          
c   -- var.elim.:  3926/3926          
c   -- var.elim.:  1000/4057          
c   -- var.elim.:  2000/4057          
c   -- var.elim.:  3000/4057          
c   -- var.elim.:  4000/4057          
c   -- var.elim.:  4057/4057          
c   -- subsuming                       
c   -- var.elim.:  1000/3533          
c   -- var.elim.:  2000/3533          
c   -- var.elim.:  3000/3533          
c   -- var.elim.:  3533/3533          
c   -- var.elim.:  952/952          
c   -- subsuming                       
c   -- var.elim.:  814/814          
c   -- var.elim.:  5/5          
c |         0 |  305953   793877 |      --       0       --      -- |     --   | -4118/-13739
c |         0 |  305953   793877 |  122381       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 8.01978 s)
c ==============================================================================
c [1mFound solution: 35205[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 73418   maxlim: 5099946   bits: 23/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        53 |  819796  2629102 |  245938      53      553    10.4 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/82277          
c   -- var.elim.:  2000/82277          
c   -- var.elim.:  3000/82277          
c   -- var.elim.:  4000/82277          
c   -- var.elim.:  5000/82277          
c   -- var.elim.:  6000/82277          
c   -- var.elim.:  7000/82277          
c   -- var.elim.:  8000/82277          
c   -- var.elim.:  9000/82277          
c   -- var.elim.:  10000/82277          
c   -- var.elim.:  11000/82277          
c   -- var.elim.:  12000/82277          
c   -- var.elim.:  13000/82277          
c   -- var.elim.:  14000/82277          
c   -- var.elim.:  15000/82277          
c   -- var.elim.:  16000/82277          
c   -- var.elim.:  17000/82277          
c   -- var.elim.:  18000/82277          
c   -- var.elim.:  19000/82277          
c   -- var.elim.:  20000/82277          
c   -- var.elim.:  21000/82277          
c   -- var.elim.:  22000/82277          
c   -- var.elim.:  23000/82277          
c   -- var.elim.:  24000/82277          
c   -- var.elim.:  25000/82277          
c   -- var.elim.:  26000/82277          
c   -- var.elim.:  27000/82277          
c   -- var.elim.:  28000/82277          
c   -- var.elim.:  29000/82277          
c   -- var.elim.:  30000/82277          
c   -- var.elim.:  31000/82277          
c   -- var.elim.:  32000/82277          
c   -- var.elim.:  33000/82277          
c   -- var.elim.:  34000/82277          
c   -- var.elim.:  35000/82277          
c   -- var.elim.:  36000/82277          
c   -- var.elim.:  37000/82277          
c   -- var.elim.:  38000/82277          
c   -- var.elim.:  39000/82277          
c   -- var.elim.:  40000/82277          
c   -- var.elim.:  41000/82277          
c   -- var.elim.:  42000/82277          
c   -- var.elim.:  43000/82277          
c   -- var.elim.:  44000/82277          
c   -- var.elim.:  45000/82277          
c   -- var.elim.:  46000/82277          
c   -- var.elim.:  47000/82277          
c   -- var.elim.:  48000/82277          
c   -- var.elim.:  49000/82277          
c   -- var.elim.:  50000/82277          
c   -- var.elim.:  51000/82277          
c   -- var.elim.:  52000/82277          
c   -- var.elim.:  53000/82277          
c   -- var.elim.:  54000/82277          
c   -- var.elim.:  55000/82277          
c   -- var.elim.:  56000/82277          
c   -- var.elim.:  57000/82277          
c   -- var.elim.:  58000/82277          
c   -- var.elim.:  59000/82277          
c   -- var.elim.:  60000/82277          
c   -- var.elim.:  61000/82277          
c   -- var.elim.:  62000/82277          
c   -- var.elim.:  63000/82277          
c   -- var.elim.:  64000/82277          
c   -- var.elim.:  65000/82277          
c   -- var.elim.:  66000/82277          
c   -- var.elim.:  67000/82277          
c   -- var.elim.:  68000/82277          
c   -- var.elim.:  69000/82277          
c   -- var.elim.:  70000/82277          
c   -- var.elim.:  71000/82277          
c   -- var.elim.:  72000/82277          
c   -- var.elim.:  73000/82277          
c   -- var.elim.:  74000/82277          
c   -- var.elim.:  75000/82277          
c   -- var.elim.:  76000/82277          
c   -- var.elim.:  77000/82277          
c   -- var.elim.:  78000/82277          
c   -- var.elim.:  79000/82277          
c   -- var.elim.:  80000/82277          
c   -- var.elim.:  81000/82277          
c   -- var.elim.:  82000/82277          
c   -- var.elim.:  82277/82277          
c   -- var.elim.:  44/44          
c |        53 |  819359  2627292 |      --      53       --      -- |     --   | -405/-1623
c |        53 |  819359  2627292 |  327743      53      553    10.4 |  0.000 % |
c |       153 |  819359  2627292 |  360517     153     1955    12.8 |  0.413 % |
c |       305 |  819359  2627292 |  396569     305     9342    30.6 |  0.413 % |
c |       530 |  819359  2627292 |  436226     530    11979    22.6 |  0.413 % |
c |       868 |  819359  2627292 |  479849     868   105366   121.4 |  0.413 % |
c |      1374 |  819172  2626650 |  527713    1372   107761    78.5 |  0.426 % |
c |      2133 |  819064  2626240 |  580408    2108   124484    59.1 |  0.433 % |
c |      3273 |  819064  2626240 |  638449    3248   421590   129.8 |  0.433 % |
c |      4983 |  819033  2626123 |  702267    4954   527134   106.4 |  0.435 % |
c |      7546 |  819026  2626106 |  772488    7513  1122815   149.4 |  0.435 % |
c |     11390 |  818932  2625783 |  849639   11356  1895840   166.9 |  0.442 % |
c |     17156 |  818929  2625769 |  934600   17121  2906529   169.8 |  0.442 % |
c |     25805 |  818929  2625769 | 1028060   25770  6396371   248.2 |  0.442 % |
c |     38779 |  818745  2625074 | 1130611   38692  8656825   223.7 |  0.457 % |
c ==============================================================================
c (current CPU-time: 716.517 s)
c ==============================================================================
c [1mFound solution: 33402[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5101749   bits: 23/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     49346 |  818469  2624139 |  245540   49205 10512189   213.6 |  0.457 % |
c   -- subsuming                       
c   -- var.elim.:  303/303          
c   -- var.elim.:  23/23          
c |     49346 |  818293  2623111 |      --   49205       --      -- |     --   | -176/-1022
c |     49346 |  818293  2623111 |  327317   49181 10512116   213.7 |  0.457 % |
c |     49446 |  818293  2623111 |  360048   49281 10513660   213.3 |  0.491 % |
c |     49596 |  818293  2623111 |  396053   49431 10515739   212.7 |  0.491 % |
c |     49821 |  818293  2623111 |  435659   49656 10523665   211.9 |  0.491 % |
c |     50158 |  818293  2623111 |  479225   49993 10538052   210.8 |  0.491 % |
c |     50664 |  818293  2623111 |  527147   50499 10546817   208.9 |  0.491 % |
c |     51423 |  818293  2623111 |  579862   51258 10573915   206.3 |  0.491 % |
c |     52563 |  818293  2623111 |  637848   52398 10605644   202.4 |  0.491 % |
c |     54271 |  818293  2623111 |  701633   54106 10692719   197.6 |  0.491 % |
c |     56833 |  818293  2623111 |  771796   56668 10743802   189.6 |  0.491 % |
c |     60679 |  818293  2623111 |  848976   60514 11177104   184.7 |  0.491 % |
c |     66445 |  818293  2623111 |  933874   66280 11526433   173.9 |  0.491 % |
c |     75094 |  818293  2623111 | 1027261   74929 12065180   161.0 |  0.491 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 x102 -x103 -x104 -x105 -x106 -x107 x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 -x2002 -x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 -x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 -x2039 -x2040 -x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 -x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 -x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 -x2126 -x2127 -x2128 -x2129 -x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 -x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 -x2147 -x2148 -x2149 -x2150 -x2151 -x2152 -x2153 x2154 -x2155 -x2156 -x2157 -x2158 -x2159 -x2160 -x2161 -x2162 -x2163 -x2164 -x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 -x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 -x2180 -x2181 -x2182 -x2183 -x2184 -x2185 -x2186 -x2187 -x2188 -x2189 -x2190 -x2191 -x2192 -x2193 -x2194 -x2195 -x2196 -x2197 -x2198 -x2199 -x2200 -x2201 -x2202 -x2203 -x2204 -x2205 -x2206 -x2207 -x2208 -x2209 -x2210 -x2211 -x2212 -x2213 -x2214 -x2215 -x2216 -x2217 -x2218 -x2219 -x2220 -x2221 -x2222 -x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 -x2233 -x2234 -x2235 -x2236 -x2237 -x2238 -x2239 -x2240 -x2241 -x2242 -x2243 -x2244 -x2245 -x2246 -x2247 -x2248 -x2249 -x2250 -x2251 -x2252 -x2253 -x2254 -x2255 -x2256 -x2257 -x2258 -x2259 -x2260 -x2261 -x2262 -x2263 -x2264 -x2265 -x2266 -x2267 x2268 -x2269 -x2270 -x2271 -x2272 -x2273 -x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 -x2281 -x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 -x2293 -x2294 -x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 -x2303 -x2304 -x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 -x2316 -x2317 -x2318 -x2319 -x2320 -x2321 -x2322 -x2323 -x2324 -x2325 -x2326 -x2327 -x2328 -x2329 -x2330 -x2331 -x2332 -x2333 -x2334 -x2335 -x2336 -x2337 -x2338 -x2339 -x2340 -x2341 -x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 -x2349 -x2350 -x2351 -x2352 -x2353 -x2354 -x2355 -x2356 -x2357 -x2358 -x2359 -x2360 -x2361 -x2362 -x2363 -x2364 -x2365 -x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 -x2373 -x2374 -x2375 -x2376 -x2377 -x2378 -x2379 -x2380 -x2381 -x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 -x2392 -x2393 -x2394 -x2395 -x2396 -x2397 x2398 -x2399 -x2400 -x2401 -x2402 -x2403 -x2404 -x2405 -x2406 -x2407 -x2408 -x2409 -x2410 -x2411 -x2412 -x2413 -x2414 -x2415 -x2416 -x2417 -x2418 -x2419 -x2420 -x2421 -x2422 -x2423 -x2424 -x2425 -x2426 -x2427 -x2428 -x2429 -x2430 -x2431 -x2432 -x2433 -x2434 -x2435 -x2436 -x2437 -x2438 -x2439 -x2440 -x2441 -x2442 -x2443 -x2444 -x2445 -x2446 -x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 -x2457 -x2458 -x2459 -x2460 -x2461 -x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 -x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 -x2483 -x2484 -x2485 -x2486 -x2487 -x2488 -x2489 -x2490 -x2491 -x2492 -x2493 -x2494 -x2495 -x2496 -x2497 -x2498 -x2499 -x2500 -x2501 -x2502 -x2503 -x2504 -x2505 -x2506 -x2507 -x2508 -x2509 -x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 -x2519 -x2520 -x2521 -x2522 -x2523 x2524 -x2525 -x2526 -x2527 -x2528 -x2529 -x2530 -x2531 -x2532 -x2533 -x2534 -x2535 -x2536 -x2537 -x2538 -x2539 -x2540 -x2541 -x2542 -x2543 -x2544 -x2545 -x2546 -x2547 -x2548 -x2549 -x2550 -x2551 -x2552 -x2553 -x2554 -x2555 -x2556 -x2557 -x2558 -x2559 -x2560 -x2561 -x2562 -x2563 -x2564 -x2565 -x2566 -x2567 -x2568 -x2569 -x2570 -x2571 -x2572 -x2573 -x2574 -x2575 -x2576 -x2577 -x2578 -x2579 -x2580 -x2581 -x2582 -x2583 -x2584 -x2585 -x2586 -x2587 -x2588 -x2589 -x2590 -x2591 -x2592 -x2593 -x2594 -x2595 -x2596 -x2597 -x2598 -x2599 x2600 -x2601 -x2602 -x2603 -x2604 -x2605 -x2606 -x2607 -x2608 -x2609 -x2610 -x2611 -x2612 -x2613 -x2614 -x2615 -x2616 -x2617 -x2618 -x2619 -x2620 -x2621 -x2622 -x2623 -x2624 -x2625 -x2626 -x2627 -x2628 -x2629 -x2630 -x2631 -x2632 -x2633 -x2634 -x2635 -x2636 -x2637 -x2638 x2639 -x2640 -x2641 -x2642 -x2643 -x2644 -x2645 -x2646 -x2647 -x2648 -x2649 -x2650 -x2651 -x2652 -x2653 -x2654 -x2655 -x2656 -x2657 -x2658 -x2659 -x2660 -x2661 -x2662 -x2663 -x2664 -x2665 -x2666 -x2667 -x2668 -x2669 -x2670 -x2671 -x2672 -x2673 -x2674 -x2675 -x2676 -x2677 -x2678 -x2679 -x2680 -x2681 -x2682 -x2683 -x2684 -x2685 -x2686 -x2687 -x2688 -x2689 -x2690 -x2691 -x2692 -x2693 -x2694 -x2695 -x2696 -x2697 -x2698 -x2699 -x2700 -x2701 -x2702 -x2703 -x2704 -x2705 -x2706 -x2707 -x2708 -x2709 -x2710 -x2711 -x2712 -x2713 -x2714 -x2715 -x2716 -x2717 -x2718 -x2719 -x2720 -x2721 -x2722 -x2723 -x2724 -x2725 -x2726 -x2727 -x2728 -x2729 -x2730 -x2731 -x2732 -x2733 -x2734 -x2735 -x2736 -x2737 -x2738 -x2739 -x2740 -x2741 -x2742 -x2743 -x2744 -x2745 -x2746 -x2747 -x2748 -x2749 -x2750 -x2751 -x2752 -x2753 -x2754 -x2755 -x2756 -x2757 -x2758 -x2759 -x2760 -x2761 -x2762 -x2763 -x2764 -x2765 -x2766 -x2767 -x2768 -x2769 -x2770 -x2771 -x2772 -x2773 -x2774 -x2775 -x2776 -x2777 -x2778 -x2779 -x2780 -x2781 -x2782 -x2783 -x2784 -x2785 -x2786 -x2787 -x2788 -x2789 -x2790 -x2791 -x2792 -x2793 -x2794 -x2795 -x2796 -x2797 -x2798 -x2799 -x2800 -x2801 -x2802 -x2803 -x2804 -x2805 -x2806 -x2807 -x2808 -x2809 -x2810 -x2811 -x2812 -x2813 -x2814 -x2815 -x2816 -x2817 -x2818 -x2819 -x2820 -x2821 -x2822 -x2823 -x2824 -x2825 -x2826 -x2827 -x2828 -x2829 -x2830 -x2831 -x2832 -x2833 -x2834 -x2835 -x2836 -x2837 -x2838 -x2839 -x2840 -x2841 -x2842 -x2843 -x2844 -x2845 -x2846 -x2847 -x2848 -x2849 -x2850 -x2851 -x2852 -x2853 -x2854 -x2855 -x2856 -x2857 -x2858 -x2859 -x2860 -x2861 -x2862 -x2863 -x2864 -x2865 -x2866 -x2867 -x2868 -x2869 -x2870 -x2871 -x2872 -x2873 -x2874 -x2875 -x2876 -x2877 -x2878 -x2879 -x2880 -x2881 -x2882 -x2883 -x2884 -x2885 -x2886 -x2887 -x2888 -x2889 -x2890 -x2891 -x2892 -x2893 -x2894 -x2895 -x2896 -x2897 -x2898 -x2899 -x2900 -x2901 -x2902 -x2903 -x2904 -x2905 -x2906 -x2907 -x2908 -x2909 -x2910 -x2911 -x2912 -x2913 -x2914 -x2915 -x2916 -x2917 -x2918 -x2919 -x2920 -x2921 -x2922 -x2923 -x2924 -x2925 -x2926 -x2927 -x2928 -x2929 -x2930 -x2931 -x2932 -x2933 -x2934 -x2935 -x2936 -x2937 -x2938 -x2939 -x2940 -x2941 -x2942 -x2943 -x2944 -x2945 -x2946 -x2947 -x2948 -x2949 -x2950 -x2951 -x2952 -x2953 -x2954 -x2955 -x2956 -x2957 -x2958 -x2959 -x2960 -x2961 -x2962 -x2963 -x2964 -x2965 -x2966 -x2967 -x2968 -x2969 -x2970 -x2971 -x2972 -x2973 -x2974 -x2975 -x2976 -x2977 -x2978 -x2979 -x2980 -x2981 -x2982 -x2983 -x2984 -x2985 -x2986 -x2987 -x2988 -x2989 -x2990 -x2991 -x2992 -x2993 -x2994 -x2995 -x2996 -x2997 -x2998 -x2999 -x3000 -x3001 -x3002 -x3003 -x3004 -x3005 -x3006 -x3007 -x3008 -x3009 -x3010 -x3011 -x3012 -x3013 -x3014 -x3015 -x3016 -x3017 -x3018 -x3019 -x3020 -x3021 -x3022 -x3023 -x3024 -x3025 -x3026 -x3027 -x3028 -x3029 -x3030 -x3031 -x3032 -x3033 -x3034 -x3035 -x3036 -x3037 -x3038 -x3039 -x3040 -x3041 -x3042 -x3043 -x3044 -x3045 -x3046 -x3047 -x3048 -x3049 -x3050 -x3051 -x3052 -x3053 -x3054 -x3055 -x3056 -x3057 -x3058 -x3059 -x3060 -x3061 -x3062 -x3063 -x3064 -x3065 -x3066 -x3067 -x3068 -x3069 -x3070 -x3071 -x3072 -x3073 -x3074 -x3075 -x3076 -x3077 -x3078 -x3079 -x3080 -x3081 -x3082 -x3083 -x3084 -x3085 -x3086 -x3087 -x3088 -x3089 -x3090 -x3091 -x3092 -x3093 -x3094 -x3095 -x3096 -x3097 -x3098 -x3099 -x3100 -x3101 -x3102 -x3103 -x3104 -x3105 -x3106 -x3107 -x3108 -x3109 -x3110 -x3111 -x3112 -x3113 -x3114 -x3115 -x3116 -x3117 -x3118 -x3119 -x3120 -x3121 -x3122 -x3123 -x3124 -x3125 -x3126 -x3127 -x3128 -x3129 -x3130 -x3131 -x3132 -x3133 -x3134 -x3135 -x3136 -x3137 -x3138 -x3139 -x3140 -x3141 -x3142 -x3143 -x3144 -x3145 -x3146 -x3147 -x3148 -x3149 -x3150 -x3151 -x3152 -x3153 -x3154 -x3155 -x3156 -x3157 -x3158 -x3159 -x3160 -x3161 -x3162 x3163 -x3164 -x3165 -x3166 -x3167 -x3168 -x3169 -x3170 -x3171 -x3172 -x3173 -x3174 -x3175 -x3176 -x3177 -x3178 -x3179 -x3180 -x3181 -x3182 -x3183 -x3184 -x3185 -x3186 -x3187 -x3188 -x3189 -x3190 -x3191 -x3192 -x3193 -x3194 -x3195 -x3196 -x3197 -x3198 -x3199 -x3200 -x3201 -x3202 -x3203 -x3204 -x3205 -x3206 -x3207 -x3208 -x3209 -x3210 -x3211 -x3212 -x3213 -x3214 -x3215 -x3216 -x3217 -x3218 -x3219 -x3220 -x3221 -x3222 x3223 -x3224 -x3225 -x3226 -x3227 -x3228 -x3229 -x3230 -x3231 -x3232 -x3233 -x3234 -x3235 -x3236 -x3237 -x3238 -x3239 -x3240 -x3241 -x3242 -x3243 -x3244 -x3245 -x3246 -x3247 -x3248 -x3249 -x3250 -x3251 -x3252 -x3253 -x3254 -x3255 -x3256 -x3257 -x3258 -x3259 -x3260 -x3261 -x3262 -x3263 -x3264 -x3265 -x3266 -x3267 -x3268 -x3269 -x3270 -x3271 -x3272 -x3273 -x3274 -x3275 -x3276 -x3277 -x3278 -x3279 -x3280 -x3281 -x3282 -x3283 -x3284 -x3285 -x3286 -x3287 -x3288 -x3289 -x3290 -x3291 -x3292 -x3293 -x3294 -x3295 -x3296 -x3297 -x3298 -x3299 -x3300 -x3301 -x3302 -x3303 -x3304 -x3305 -x3306 -x3307 -x3308 -x3309 -x3310 -x3311 -x3312 -x3313 -x3314 -x3315 -x3316 -x3317 -x3318 -x3319 -x3320 -x3321 -x3322 -x3323 -x3324 -x3325 -x3326 -x3327 -x3328 -x3329 -x3330 -x3331 -x3332 -x3333 -x3334 -x3335 -x3336 -x3337 -x3338 -x3339 -x3340 -x3341 -x3342 -x3343 -x3344 -x3345 -x3346 -x3347 -x3348 -x3349 -x3350 -x3351 -x3352 -x3353 -x3354 -x3355 -x3356 -x3357 -x3358 -x3359 -x3360 -x3361 -x3362 -x3363 -x3364 -x3365 -x3366 -x3367 -x3368 -x3369 -x3370 -x3371 -x3372 -x3373 -x3374 -x3375 -x3376 -x3377 -x3378 -x3379 -x3380 -x3381 -x3382 -x3383 -x3384 -x3385 -x3386 -x3387 -x3388 -x3389 -x3390 -x3391 -x3392 -x3393 -x3394 -x3395 -x3396 -x3397 -x3398 -x3399 -x3400 -x3401 -x3402 -x3403 -x3404 -x3405 -x3406 -x3407 -x3408 -x3409 -x3410 -x3411 -x3412 -x3413 -x3414 -x3415 x3416 -x3417 -x3418 -x3419 -x3420 -x3421 -x3422 -x3423 x3424 -x3425 -x3426 -x3427 -x3428 -x3429 -x3430 -x3431 -x3432 -x3433 -x3434 -x3435 -x3436 -x3437 -x3438 -x3439 -x3440 -x3441 -x3442 -x3443 -x3444 -x3445 -x3446 -x3447 -x3448 -x3449 -x3450 -x3451 -x3452 -x3453 -x3454 -x3455 -x3456 -x3457 -x3458 -x3459 -x3460 -x3461 -x3462 -x3463 -x3464 -x3465 -x3466 -x3467 -x3468 -x3469 -x3470 -x3471 -x3472 -x3473 -x3474 -x3475 -x3476 -x3477 -x3478 -x3479 -x3480 -x3481 -x3482 -x3483 -x3484 -x3485 -x3486 -x3487 -x3488 -x3489 -x3490 -x3491 -x3492 -x3493 -x3494 -x3495 -x3496 -x3497 -x3498 -x3499 -x3500 -x3501 -x3502 -x3503 -x3504 -x3505 -x3506 -x3507 -x3508 -x3509 -x3510 -x3511 -x3512 -x3513 -x3514 -x3515 -x3516 -x3517 -x3518 -x3519 -x3520 -x3521 -x3522 -x3523 -x3524 -x3525 -x3526 -x3527 -x3528 -x3529 -x3530 -x3531 -x3532 -x3533 -x3534 -x3535 -x3536 -x3537 -x3538 -x3539 -x3540 -x3541 -x3542 -x3543 -x3544 -x3545 -x3546 -x3547 -x3548 -x3549 -x3550 -x3551 -x3552 -x3553 -x3554 -x3555 -x3556 -x3557 -x3558 -x3559 -x3560 -x3561 -x3562 -x3563 -x3564 -x3565 -x3566 -x3567 -x3568 -x3569 -x3570 -x3571 -x3572 -x3573 -x3574 -x3575 -x3576 -x3577 -x3578 -x3579 -x3580 -x3581 -x3582 -x3583 -x3584 -x3585 -x3586 -x3587 -x3588 -x3589 -x3590 -x3591 -x3592 -x3593 -x3594 -x3595 -x3596 -x3597 -x3598 -x3599 x3600 -x3601 -x3602 -x3603 -x3604 -x3605 -x3606 -x3607 -x3608 -x3609 -x3610 -x3611 -x3612 -x3613 -x3614 -x3615 -x3616 -x3617 -x3618 -x3619 -x3620 -x3621 -x3622 -x3623 -x3624 -x3625 -x3626 -x3627 -x3628 -x3629 -x3630 -x3631 -x3632 -x3633 -x3634 -x3635 -x3636 -x3637 -x3638 -x3639 -x3640 -x3641 -x3642 -x3643 -x3644 -x3645 -x3646 -x3647 -x3648 -x3649 -x3650 -x3651 -x3652 -x3653 -x3654 -x3655 -x3656 -x3657 -x3658 -x3659 -x3660 -x3661 -x3662 -x3663 -x3664 -x3665 -x3666 -x3667 -x3668 -x3669 -x3670 -x3671 -x3672 -x3673 -x3674 -x3675 -x3676 -x3677 -x3678 -x3679 -x3680 -x3681 -x3682 -x3683 -x3684 -x3685 -x3686 -x3687 -x3688 -x3689 -x3690 -x3691 -x3692 -x3693 -x3694 -x3695 -x3696 -x3697 -x3698 -x3699 -x3700 -x3701 -x3702 -x3703 -x3704 -x3705 -x3706 -x3707 -x3708 -x3709 -x3710 -x3711 -x3712 -x3713 -x3714 -x3715 -x3716 -x3717 -x3718 -x3719 -x3720 -x3721 -x3722 -x3723 -x3724 -x3725 -x3726 -x3727 -x3728 -x3729 -x3730 -x3731 -x3732 -x3733 -x3734 -x3735 -x3736 -x3737 -x3738 -x3739 -x3740 -x3741 -x3742 -x3743 -x3744 -x3745 -x3746 -x3747 -x3748 -x3749 -x3750 -x3751 -x3752 -x3753 -x3754 -x3755 -x3756 -x3757 -x3758 -x3759 -x3760 -x3761 -x3762 -x3763 -x3764 -x3765 -x3766 -x3767 -x3768 -x3769 -x3770 -x3771 -x3772 -x3773 -x3774 -x3775 -x3776 -x3777 -x3778 -x3779 -x3780 -x3781 -x3782 -x3783 -x3784 -x3785 -x3786 -x3787 -x3788 -x3789 -x3790 -x3791 -x3792 -x3793 -x3794 -x3795 -x3796 -x3797 -x3798 -x3799 -x3800 -x3801 -x3802 -x3803 -x3804 -x3805 -x3806 -x3807 -x3808 -x3809 -x3810 -x3811 -x3812 -x3813 -x3814 -x3815 -x3816 -x3817 -x3818 -x3819 -x3820 -x3821 -x3822 -x3823 -x3824 -x3825 -x3826 -x3827 -x3828 -x3829 -x3830 -x3831 -x3832 -x3833 -x3834 -x3835 -x3836 -x3837 -x3838 -x3839 -x3840 -x3841 -x3842 -x3843 -x3844 -x3845 -x3846 -x3847 -x3848 -x3849 -x3850 -x3851 -x3852 -x3853 -x3854 -x3855 -x3856 -x3857 -x3858 -x3859 -x3860 -x3861 -x3862 -x3863 -x3864 -x3865 -x3866 -x3867 -x3868 -x3869 -x3870 -x3871 -x3872 -x3873 -x3874 -x3875 -x3876 -x3877 -x3878 -x3879 -x3880 -x3881 -x3882 -x3883 -x3884 -x3885 -x3886 -x3887 -x3888 -x3889 -x3890 -x3891 -x3892 -x3893 -x3894 -x3895 -x3896 -x3897 -x3898 -x3899 -x3900 -x3901 -x3902 -x3903 -x3904 -x3905 -x3906 -x3907 -x3908 -x3909 -x3910 -x3911 -x3912 -x3913 -x3914 -x3915 -x3916 -x3917 -x3918 -x3919 -x3920 -x3921 -x3922 -x3923 -x3924 -x3925 -x3926 -x3927 -x3928 -x3929 -x3930 -x3931 -x3932 -x3933 -x3934 -x3935 -x3936 -x3937 -x3938 -x3939 -x3940 -x3941 -x3942 -x3943 -x3944 -x3945 -x3946 -x3947 -x3948 -x3949 -x3950 -x3951 -x3952 -x3953 -x3954 -x3955 -x3956 -x3957 -x3958 -x3959 -x3960 -x3961 -x3962 -x3963 -x3964 -x3965 -x3966 -x3967 -x3968 -x3969 -x3970 -x3971 -x3972 -x3973 -x3974 -x3975 -x3976 -x3977 -x3978 -x3979 -x3980 -x3981 -x3982 -x3983 -x3984 -x3985 -x3986 -x3987 -x3988 -x3989 -x3990 -x3991 -x3992 -x3993 -x3994 -x3995 -x3996 -x3997 -x3998 -x3999 -x4000 -x4001 -x4002 -x4003 -x4004 -x4005 -x4006 -x4007 -x4008 -x4009 -x4010 -x4011 -x4012 -x4013 -x4014 -x4015 -x4016 -x4017 -x4018 -x4019 -x4020 -x4021 -x4022 -x4023 -x4024 -x4025 -x4026 -x4027 -x4028 -x4029 -x4030 -x4031 -x4032 -x4033 -x4034 -x4035 -x4036 -x4037 -x4038 -x4039 -x4040 -x4041 -x4042 -x4043 -x4044 -x4045 -x4046 -x4047 -x4048 -x4049 -x4050 -x4051 -x4052 -x4053 -x4054 -x4055 -x4056 -x4057 -x4058 -x4059 -x4060 -x4061 -x4062 -x4063 -x4064 -x4065 -x4066 -x4067 -x4068 -x4069 -x4070 -x4071 -x4072 -x4073 -x4074 -x4075 -x4076 -x4077 -x4078 -x4079 -x4080 -x4081 -x4082 -x4083 -x4084 -x4085 -x4086 -x4087 -x4088 -x4089 -x4090 -x4091 -x4092 -x4093 -x4094 -x4095 -x4096 -x4097 -x4098 -x4099 -x4100 -x4101 -x4102 -x4103 -x4104 -x4105 -x4106 -x4107 -x4108 -x4109 -x4110 -x4111 -x4112 -x4113 -x4114 -x4115 -x4116 -x4117 -x4118 -x4119 -x4120 -x4121 -x4122 -x4123 x4124 -x4125 -x4126 -x4127 -x4128 -x4129 -x4130 -x4131 -x4132 -x4133 -x4134 -x4135 -x4136 -x4137 -x4138 -x4139 -x4140 -x4141 -x4142 -x4143 -x4144 -x4145 -x4146 -x4147 -x4148 -x4149 -x4150 -x4151 -x4152 -x4153 -x4154 -x4155 -x4156 -x4157 -x4158 -x4159 -x4160 -x4161 -x4162 -x4163 -x4164 -x4165 -x4166 -x4167 -x4168 -x4169 -x4170 -x4171 -x4172 -x4173 -x4174 -x4175 -x4176 -x4177 -x4178 -x4179 -x4180 -x4181 -x4182 -x4183 -x4184 -x4185 -x4186 -x4187 -x4188 -x4189 -x4190 -x4191 -x4192 -x4193 -x4194 -x4195 -x4196 -x4197 -x4198 -x4199 -x4200 -x4201 -x4202 -x4203 -x4204 -x4205 -x4206 -x4207 -x4208 -x4209 -x4210 -x4211 -x4212 -x4213 -x4214 -x4215 -x4216 -x4217 -x4218 -x4219 -x4220 -x4221 -x4222 -x4223 -x4224 -x4225 -x4226 -x4227 -x4228 -x4229 -x4230 -x4231 -x4232 -x4233 -x4234 -x4235 -x4236 -x4237 -x4238 -x4239 -x4240 -x4241 -x4242 -x4243 -x4244 -x4245 -x4246 -x4247 -x4248 -x4249 -x4250 -x4251 -x4252 -x4253 -x4254 -x4255 -x4256 -x4257 -x4258 -x4259 -x4260 -x4261 -x4262 -x4263 -x4264 -x4265 -x4266 -x4267 -x4268 -x4269 -x4270 -x4271 -x4272 -x4273 -x4274 -x4275 -x4276 -x4277 -x4278 -x4279 -x4280 -x4281 -x4282 -x4283 -x4284 -x4285 -x4286 -x4287 -x4288 -x4289 -x4290 -x4291 -x4292 -x4293 -x4294 -x4295 -x4296 -x4297 -x4298 -x4299 -x4300 -x4301 -x4302 -x4303 -x4304 -x4305 -x4306 -x4307 -x4308 -x4309 -x4310 -x4311 -x4312 -x4313 -x4314 -x4315 -x4316 -x4317 -x4318 -x4319 -x4320 -x4321 -x4322 -x4323 -x4324 -x4325 -x4326 -x4327 -x4328 x4329 -x4330 -x4331 -x4332 -x4333 -x4334 -x4335 -x4336 -x4337 -x4338 -x4339 -x4340 -x4341 -x4342 -x4343 -x4344 -x4345 -x4346 -x4347 -x4348 -x4349 -x4350 -x4351 -x4352 -x4353 -x4354 -x4355 -x4356 -x4357 -x4358 -x4359 -x4360 -x4361 -x4362 -x4363 -x4364 -x4365 -x4366 -x4367 -x4368 -x4369 -x4370 -x4371 -x4372 -x4373 -x4374 -x4375 -x4376 -x4377 -x4378 -x4379 -x4380 -x4381 -x4382 -x4383 -x4384 -x4385 -x4386 -x4387 -x4388 -x4389 -x4390 -x4391 -x4392 -x4393 -x4394 -x4395 -x4396 -x4397 -x4398 -x4399 -x4400 -x4401 -x4402 -x4403 -x4404 -x4405 -x4406 -x4407 -x4408 -x4409 -x4410 -x4411 -x4412 -x4413 -x4414 -x4415 -x4416 -x4417 -x4418 -x4419 -x4420 -x4421 -x4422 -x4423 -x4424 -x4425 -x4426 -x4427 -x4428 -x4429 -x4430 -x4431 -x4432 -x4433 -x4434 -x4435 -x4436 -x4437 -x4438 -x4439 -x4440 -x4441 -x4442 -x4443 -x4444 -x4445 -x4446 -x4447 -x4448 -x4449 x4450 -x4451 -x4452 -x4453 -x4454 -x4455 -x4456 -x4457 -x4458 -x4459 -x4460 -x4461 -x4462 -x4463 -x4464 -x4465 -x4466 -x4467 -x4468 -x4469 -x4470 -x4471 -x4472 -x4473 -x4474 -x4475 -x4476 -x4477 -x4478 -x4479 -x4480 -x4481 -x4482 -x4483 -x4484 -x4485 -x4486 -x4487 -x4488 -x4489 -x4490 x4491 -x4492 -x4493 -x4494 -x4495 -x4496 -x4497 -x4498 -x4499 -x4500 -x4501 -x4502 -x4503 -x4504 -x4505 -x4506 -x4507 -x4508 -x4509 -x4510 -x4511 -x4512 -x4513 -x4514 -x4515 -x4516 -x4517 -x4518 -x4519 -x4520 -x4521 -x4522 -x4523 -x4524 -x4525 -x4526 -x4527 -x4528 -x4529 -x4530 -x4531 -x4532 -x4533 -x4534 -x4535 -x4536 -x4537 -x4538 -x4539 -x4540 -x4541 -x4542 -x4543 -x4544 -x4545 -x4546 -x4547 -x4548 -x4549 -x4550 -x4551 -x4552 -x4553 -x4554 -x4555 -x4556 -x4557 -x4558 -x4559 -x4560 -x4561 -x4562 -x4563 -x4564 -x4565 -x4566 -x4567 -x4568 -x4569 -x4570 -x4571 -x4572 -x4573 -x4574 -x4575 -x4576 -x4577 -x4578 -x4579 -x4580 -x4581 -x4582 -x4583 -x4584 -x4585 -x4586 -x4587 -x4588 -x4589 -x4590 -x4591 -x4592 -x4593 -x4594 -x4595 -x4596 -x4597 -x4598 -x4599 -x4600 -x4601 -x4602 -x4603 -x4604 -x4605 -x4606 -x4607 -x4608 -x4609 -x4610 -x4611 -x4612 -x4613 -x4614 -x4615 -x4616 -x4617 -x4618 -x4619 -x4620 -x4621 -x4622 -x4623 -x4624 -x4625 -x4626 -x4627 -x4628 -x4629 -x4630 -x4631 -x4632 -x4633 -x4634 -x4635 -x4636 -x4637 -x4638 -x4639 -x4640 -x4641 -x4642 -x4643 -x4644 -x4645 -x4646 -x4647 -x4648 -x4649 -x4650 -x4651 -x4652 -x4653 -x4654 -x4655 -x4656 -x4657 -x4658 -x4659 -x4660 -x4661 -x4662 -x4663 -x4664 -x4665 -x4666 -x4667 -x4668 -x4669 -x4670 -x4671 -x4672 -x4673 -x4674 -x4675 -x4676 -x4677 -x4678 -x4679 -x4680 -x4681 -x4682 -x4683 -x4684 -x4685 -x4686 -x4687 -x4688 -x4689 -x4690 -x4691 -x4692 -x4693 -x4694 -x4695 -x4696 -x4697 -x4698 -x4699 -x4700 -x4701 -x4702 -x4703 -x4704 -x4705 -x4706 -x4707 -x4708 -x4709 -x4710 -x4711 -x4712 -x4713 -x4714 -x4715 -x4716 -x4717 -x4718 -x4719 -x4720 -x4721 -x4722 -x4723 -x4724 -x4725 -x4726 -x4727 -x4728 -x4729 -x4730 -x4731 -x4732 -x4733 -x4734 -x4735 -x4736 -x4737 -x4738 -x4739 -x4740 -x4741 -x4742 -x4743 -x4744 -x4745 -x4746 -x4747 -x4748 -x4749 -x4750 -x4751 -x4752 -x4753 -x4754 -x4755 -x4756 -x4757 -x4758 -x4759 -x4760 -x4761 -x4762 -x4763 -x4764 -x4765 -x4766 -x4767 -x4768 -x4769 -x4770 -x4771 -x4772 -x4773 -x4774 -x4775 -x4776 -x4777 -x4778 -x4779 -x4780 -x4781 -x4782 -x4783 -x4784 -x4785 -x4786 -x4787 -x4788 -x4789 -x4790 -x4791 -x4792 -x4793 -x4794 -x4795 -x4796 -x4797 -x4798 -x4799 -x4800 -x4801 -x4802 -x4803 -x4804 -x4805 -x4806 -x4807 -x4808 -x4809 -x4810 -x4811 -x4812 -x4813 -x4814 -x4815 -x4816 -x4817 -x4818 -x4819 -x4820 -x4821 -x4822 -x4823 -x4824 -x4825 -x4826 -x4827 -x4828 -x4829 -x4830 -x4831 -x4832 -x4833 -x4834 -x4835 -x4836 -x4837 -x4838 -x4839 -x4840 -x4841 -x4842 -x4843 -x4844 -x4845 -x4846 -x4847 -x4848 -x4849 -x4850 -x4851 -x4852 -x4853 -x4854 -x4855 -x4856 -x4857 -x4858 -x4859 -x4860 -x4861 -x4862 -x4863 -x4864 -x4865 -x4866 -x4867 -x4868 -x4869 -x4870 -x4871 -x4872 -x4873 -x4874 -x4875 -x4876 -x4877 -x4878 -x4879 -x4880 -x4881 -x4882 -x4883 -x4884 -x4885 -x4886 -x4887 -x4888 -x4889 -x4890 -x4891 -x4892 -x4893 -x4894 -x4895 -x4896 -x4897 -x4898 -x4899 -x4900 -x4901 -x4902 -x4903 -x4904 -x4905 -x4906 -x4907 -x4908 -x4909 -x4910 -x4911 -x4912 -x4913 -x4914 -x4915 -x4916 -x4917 -x4918 -x4919 -x4920 -x4921 -x4922 -x4923 -x4924 -x4925 -x4926 -x4927 -x4928 -x4929 -x4930 -x4931 -x4932 -x4933 -x4934 -x4935 -x4936 -x4937 -x4938 -x4939 -x4940 -x4941 -x4942 -x4943 -x4944 -x4945 -x4946 -x4947 -x4948 -x4949 -x4950 -x4951 -x4952 -x4953 -x4954 -x4955 -x4956 -x4957 -x4958 -x4959 -x4960 -x4961 -x4962 -x4963 -x4964 -x4965 -x4966 -x4967 -x4968 -x4969 -x4970 -x4971 -x4972 -x4973 -x4974 -x4975 -x4976 -x4977 -x4978 -x4979 -x4980 -x4981 -x4982 -x4983 -x4984 -x4985 -x4986 -x4987 -x4988 -x4989 -x4990 -x4991 -x4992 -x4993 -x4994 -x4995 -x4996 -x4997 -x4998 -x4999 -x5000 -x5001 -x5002 -x5003 -x5004 -x5005 -x5006 -x5007 -x5008 -x5009 -x5010 -x5011 -x5012 -x5013 -x5014 -x5015 -x5016 -x5017 -x5018 -x5019 -x5020 -x5021 -x5022 -x5023 -x5024 -x5025 -x5026 -x5027 -x5028 -x5029 -x5030 -x5031 -x5032 -x5033 -x5034 -x5035 -x5036 -x5037 -x5038 -x5039 -x5040 -x5041 -x5042 -x5043 -x5044 -x5045 -x5046 -x5047 -x5048 -x5049 -x5050 -x5051 -x5052 -x5053 -x5054 -x5055 -x5056 -x5057 -x5058 -x5059 -x5060 -x5061 -x5062 -x5063 -x5064 -x5065 -x5066 -x5067 -x5068 -x5069 -x5070 -x5071 -x5072 -x5073 -x5074 -x5075 -x5076 -x5077 -x5078 -x5079 -x5080 -x5081 -x5082 -x5083 -x5084 -x5085 -x5086 -x5087 -x5088 -x5089 -x5090 -x5091 -x5092 -x5093 -x5094 -x5095 -x5096 -x5097 -x5098 -x5099 -x5100 -x5101 -x5102 -x5103 -x5104 -x5105 -x5106 -x5107 -x5108 -x5109 -x5110 -x5111 -x5112 -x5113 -x5114 -x5115 -x5116 -x5117 -x5118 -x5119 -x5120 -x5121 -x5122 -x5123 -x5124 -x5125 -x5126 -x5127 -x5128 -x5129 -x5130 -x5131 -x5132 -x5133 -x5134 -x5135 -x5136 -x5137 -x5138 -x5139 -x5140 -x5141 -x5142 -x5143 -x5144 -x5145 -x5146 -x5147 -x5148 -x5149 -x5150 -x5151 -x5152 -x5153 -x5154 -x5155 -x5156 -x5157 -x5158 -x5159 -x5160 -x5161 -x5162 -x5163 -x5164 -x5165 -x5166 -x5167 -x5168 -x5169 -x5170 -x5171 -x5172 -x5173 -x5174 -x5175 -x5176 -x5177 -x5178 -x5179 -x5180 -x5181 -x5182 -x5183 -x5184 -x5185 -x5186 -x5187 -x5188 -x5189 -x5190 -x5191 -x5192 -x5193 -x5194 -x5195 -x5196 -x5197 -x5198 -x5199 -x5200 -x5201 -x5202 -x5203 -x5204 -x5205 -x5206 -x5207 -x5208 -x5209 -x5210 -x5211 -x5212 -x5213 -x5214 -x5215 -x5216 -x5217 -x5218 -x5219 -x5220 -x5221 -x5222 -x5223 -x5224 -x5225 -x5226 -x5227 -x5228 -x5229 -x5230 -x5231 -x5232 -x5233 -x5234 -x5235 -x5236 -x5237 -x5238 -x5239 -x5240 -x5241 -x5242 -x5243 -x5244 -x5245 -x5246 -x5247 -x5248 -x5249 -x5250 -x5251 -x5252 -x5253 -x5254 -x5255 -x5256 -x5257 -x5258 -x5259 -x5260 -x5261 -x5262 -x5263 -x5264 -x5265 -x5266 -x5267 -x5268 -x5269 -x5270 -x5271 -x5272 -x5273 -x5274 -x5275 -x5276 -x5277 -x5278 -x5279 -x5280 -x5281 -x5282 -x5283 -x5284 -x5285 -x5286 -x5287 -x5288 -x5289 -x5290 -x5291 -x5292 -x5293 -x5294 -x5295 -x5296 -x5297 -x5298 -x5299 -x5300 -x5301 -x5302 -x5303 -x5304 -x5305 -x5306 -x5307 -x5308 -x5309 -x5310 -x5311 -x5312 -x5313 -x5314 -x5315 -x5316 -x5317 -x5318 -x5319 -x5320 -x5321 -x5322 -x5323 -x5324 -x5325 -x5326 -x5327 -x5328 -x5329 -x5330 -x5331 -x5332 -x5333 -x5334 -x5335 -x5336 -x5337 -x5338 -x5339 -x5340 -x5341 -x5342 -x5343 -x5344 -x5345 -x5346 x5347 -x5348 -x5349 -x5350 -x5351 -x5352 -x5353 -x5354 -x5355 -x5356 -x5357 -x5358 -x5359 -x5360 -x5361 -x5362 -x5363 -x5364 -x5365 -x5366 -x5367 -x5368 -x5369 -x5370 -x5371 -x5372 -x5373 -x5374 -x5375 -x5376 -x5377 -x5378 -x5379 -x5380 -x5381 -x5382 -x5383 -x5384 -x5385 -x5386 -x5387 -x5388 -x5389 -x5390 -x5391 -x5392 -x5393 -x5394 -x5395 -x5396 -x5397 -x5398 -x5399 -x5400 -x5401 -x5402 -x5403 -x5404 -x5405 -x5406 -x5407 -x5408 -x5409 -x5410 -x5411 -x5412 -x5413 -x5414 -x5415 -x5416 -x5417 -x5418 -x5419 -x5420 -x5421 -x5422 -x5423 -x5424 -x5425 -x5426 -x5427 -x5428 -x5429 -x5430 -x5431 -x5432 -x5433 -x5434 -x5435 -x5436 -x5437 -x5438 -x5439 -x5440 -x5441 -x5442 -x5443 -x5444 -x5445 -x5446 -x5447 -x5448 -x5449 -x5450 -x5451 -x5452 -x5453 -x5454 -x5455 -x5456 -x5457 -x5458 -x5459 -x5460 -x5461 -x5462 -x5463 -x5464 -x5465 -x5466 -x5467 -x5468 -x5469 -x5470 -x5471 -x5472 -x5473 -x5474 -x5475 -x5476 -x5477 -x5478 -x5479 -x5480 -x5481 -x5482 -x5483 -x5484 -x5485 -x5486 -x5487 -x5488 -x5489 -x5490 -x5491 -x5492 -x5493 -x5494 -x5495 -x5496 -x5497 -x5498 -x5499 -x5500 -x5501 -x5502 -x5503 -x5504 -x5505 -x5506 -x5507 -x5508 -x5509 -x5510 -x5511 -x5512 x5513 -x5514 -x5515 -x5516 -x5517 -x5518 -x5519 -x5520 -x5521 -x5522 -x5523 -x5524 -x5525 -x5526 -x5527 -x5528 -x5529 -x5530 -x5531 -x5532 -x5533 -x5534 -x5535 -x5536 -x5537 -x5538 -x5539 -x5540 -x5541 -x5542 -x5543 -x5544 -x5545 -x5546 -x5547 -x5548 -x5549 -x5550 -x5551 -x5552 -x5553 -x5554 -x5555 -x5556 -x5557 -x5558 -x5559 -x5560 -x5561 -x5562 -x5563 -x5564 -x5565 -x5566 -x5567 -x5568 -x5569 -x5570 -x5571 -x5572 -x5573 -x5574 -x5575 -x5576 -x5577 -x5578 -x5579 -x5580 -x5581 -x5582 -x5583 -x5584 -x5585 -x5586 -x5587 -x5588 -x5589 -x5590 -x5591 -x5592 -x5593 -x5594 -x5595 -x5596 -x5597 -x5598 -x5599 -x5600 -x5601 -x5602 -x5603 -x5604 -x5605 -x5606 -x5607 -x5608 -x5609 -x5610 -x5611 -x5612 -x5613 -x5614 -x5615 -x5616 -x5617 -x5618 -x5619 -x5620 -x5621 -x5622 -x5623 -x5624 -x5625 -x5626 -x5627 -x5628 -x5629 -x5630 -x5631 -x5632 -x5633 -x5634 -x5635 -x5636 -x5637 -x5638 -x5639 -x5640 -x5641 -x5642 -x5643 -x5644 -x5645 -x5646 -x5647 -x5648 -x5649 -x5650 -x5651 -x5652 -x5653 -x5654 -x5655 -x5656 -x5657 -x5658 -x5659 -x5660 -x5661 -x5662 -x5663 -x5664 -x5665 -x5666 -x5667 -x5668 -x5669 -x5670 -x5671 -x5672 -x5673 -x5674 -x5675 -x5676 -x5677 -x5678 -x5679 -x5680 -x5681 -x5682 -x5683 -x5684 -x5685 -x5686 x5687 -x5688 -x5689 -x5690 -x5691 -x5692 -x5693 -x5694 -x5695 -x5696 -x5697 -x5698 -x5699 -x5700 -x5701 -x5702 x5703 -x5704 -x5705 -x5706 -x5707 -x5708 -x5709 -x5710 -x5711 -x5712 -x5713 -x5714 -x5715 -x5716 -x5717 -x5718 -x5719 -x5720 -x5721 -x5722 -x5723 -x5724 -x5725 -x5726 -x5727 -x5728 -x5729 -x5730 -x5731 -x5732 -x5733 -x5734 -x5735 -x5736 -x5737 -x5738 -x5739 -x5740 -x5741 -x5742 -x5743 -x5744 -x5745 -x5746 -x5747 -x5748 -x5749 -x5750 -x5751 -x5752 -x5753 -x5754 -x5755 -x5756 -x5757 -x5758 -x5759 -x5760 -x5761 -x5762 -x5763 -x5764 -x5765 -x5766 -x5767 -x5768 -x5769 -x5770 -x5771 -x5772 -x5773 -x5774 -x5775 -x5776 -x5777 -x5778 -x5779 -x5780 -x5781 -x5782 -x5783 -x5784 -x5785 -x5786 -x5787 -x5788 -x5789 -x5790 -x5791 -x5792 -x5793 -x5794 -x5795 -x5796 -x5797 -x5798 -x5799 -x5800 -x5801 -x5802 -x5803 -x5804 -x5805 -x5806 -x5807 -x5808 -x5809 -x5810 -x5811 -x5812 -x5813 -x5814 -x5815 -x5816 -x5817 -x5818 -x5819 -x5820 -x5821 -x5822 -x5823 -x5824 -x5825 -x5826 -x5827 -x5828 -x5829 -x5830 -x5831 -x5832 -x5833 -x5834 -x5835 -x5836 -x5837 -x5838 -x5839 -x5840 -x5841 -x5842 -x5843 -x5844 -x5845 -x5846 -x5847 -x5848 -x5849 -x5850 -x5851 -x5852 -x5853 -x5854 -x5855 -x5856 -x5857 -x5858 -x5859 -x5860 -x5861 -x5862 -x5863 -x5864 -x5865 -x5866 -x5867 -x5868 -x5869 -x5870 -x5871 -x5872 -x5873 -x5874 -x5875 -x5876 -x5877 -x5878 -x5879 -x5880 -x5881 -x5882 -x5883 -x5884 -x5885 -x5886 -x5887 -x5888 -x5889 -x5890 -x5891 -x5892 -x5893 -x5894 -x5895 -x5896 -x5897 -x5898 -x5899 -x5900 -x5901 -x5902 -x5903 -x5904 -x5905 -x5906 -x5907 -x5908 -x5909 -x5910 -x5911 -x5912 -x5913 -x5914 -x5915 -x5916 -x5917 -x5918 -x5919 -x5920 -x5921 -x5922 -x5923 -x5924 -x5925 -x5926 -x5927 -x5928 -x5929 -x5930 -x5931 -x5932 -x5933 -x5934 -x5935 -x5936 -x5937 -x5938 -x5939 -x5940 -x5941 -x5942 -x5943 -x5944 -x5945 -x5946 -x5947 -x5948 -x5949 -x5950 -x5951 -x5952 -x5953 -x5954 -x5955 -x5956 -x5957 -x5958 -x5959 -x5960 -x5961 -x5962 -x5963 -x5964 -x5965 -x5966 -x5967 -x5968 -x5969 -x5970 -x5971 -x5972 -x5973 -x5974 -x5975 -x5976 -x5977 -x5978 -x5979 -x5980 -x5981 -x5982 -x5983 -x5984 -x5985 -x5986 -x5987 -x5988 -x5989 -x5990 -x5991 -x5992 -x5993 -x5994 -x5995 -x5996 -x5997 -x5998 -x5999 -x6000 -x6001 -x6002 -x6003 -x6004 -x6005 -x6006 -x6007 -x6008 -x6009 -x6010 -x6011 -x6012 -x6013 -x6014 -x6015 -x6016 -x6017 -x6018 -x6019 -x6020 -x6021 -x6022 -x6023 -x6024 -x6025 -x6026 -x6027 -x6028 -x6029 -x6030 -x6031 -x6032 -x6033 -x6034 -x6035 -x6036 -x6037 -x6038 -x6039 -x6040 -x6041 -x6042 -x6043 -x6044 -x6045 -x6046 -x6047 -x6048 -x6049 -x6050 -x6051 -x6052 -x6053 -x6054 -x6055 -x6056 -x6057 -x6058 -x6059 -x6060 -x6061 -x6062 -x6063 -x6064 -x6065 -x6066 -x6067 -x6068 -x6069 -x6070 -x6071 -x6072 -x6073 -x6074 -x6075 -x6076 -x6077 -x6078 -x6079 -x6080 -x6081 -x6082 -x6083 -x6084 -x6085 -x6086 -x6087 -x6088 -x6089 -x6090 -x6091 -x6092 -x6093 -x6094 -x6095 -x6096 -x6097 -x6098 -x6099 -x6100 -x6101 -x6102 -x6103 -x6104 -x6105 -x6106 -x6107 -x6108 -x6109 -x6110 -x6111 -x6112 -x6113 -x6114 -x6115 -x6116 -x6117 -x6118 -x6119 -x6120 -x6121 -x6122 -x6123 -x6124 -x6125 -x6126 -x6127 -x6128 -x6129 -x6130 -x6131 -x6132 -x6133 -x6134 -x6135 -x6136 -x6137 -x6138 -x6139 -x6140 -x6141 -x6142 -x6143 -x6144 -x6145 -x6146 -x6147 -x6148 -x6149 -x6150 -x6151 -x6152 -x6153 -x6154 -x6155 -x6156 -x6157 -x6158 -x6159 -x6160 -x6161 -x6162 -x6163 -x6164 -x6165 -x6166 -x6167 -x6168 -x6169 -x6170 -x6171 x6172 -x6173 -x6174 -x6175 -x6176 -x6177 -x6178 -x6179 -x6180 -x6181 -x6182 -x6183 -x6184 -x6185 -x6186 -x6187 -x6188 -x6189 -x6190 -x6191 -x6192 -x6193 -x6194 -x6195 -x6196 -x6197 -x6198 -x6199 -x6200 -x6201 -x6202 -x6203 -x6204 -x6205 -x6206 -x6207 -x6208 -x6209 -x6210 -x6211 -x6212 -x6213 -x6214 -x6215 -x6216 -x6217 -x6218 -x6219 -x6220 -x6221 -x6222 -x6223 -x6224 -x6225 -x6226 -x6227 -x6228 -x6229 -x6230 -x6231 -x6232 -x6233 -x6234 -x6235 -x6236 -x6237 -x6238 -x6239 -x6240 -x6241 -x6242 -x6243 -x6244 -x6245 -x6246 -x6247 -x6248 -x6249 -x6250 -x6251 -x6252 -x6253 -x6254 -x6255 -x6256 -x6257 -x6258 -x6259 -x6260 -x6261 -x6262 -x6263 -x6264 -x6265 -x6266 -x6267 -x6268 -x6269 -x6270 -x6271 -x6272 -x6273 -x6274 -x6275 -x6276 -x6277 -x6278 -x6279 -x6280 -x6281 -x6282 -x6283 x6284 -x6285 -x6286 -x6287 -x6288 -x6289 -x6290 -x6291 -x6292 -x6293 -x6294 -x6295 -x6296 -x6297 -x6298 -x6299 -x6300 -x6301 -x6302 -x6303 -x6304 -x6305 -x6306 -x6307 -x6308 -x6309 -x6310 -x6311 -x6312 -x6313 -x6314 -x6315 -x6316 -x6317 -x6318 -x6319 -x6320 -x6321 -x6322 -x6323 -x6324 -x6325 -x6326 -x6327 -x6328 -x6329 -x6330 -x6331 -x6332 -x6333 -x6334 -x6335 -x6336 -x6337 -x6338 -x6339 -x6340 -x6341 -x6342 -x6343 -x6344 -x6345 -x6346 -x6347 -x6348 -x6349 -x6350 -x6351 -x6352 -x6353 -x6354 -x6355 -x6356 -x6357 -x6358 -x6359 -x6360 -x6361 -x6362 -x6363 -x6364 -x6365 -x6366 -x6367 -x6368 -x6369 -x6370 -x6371 -x6372 -x6373 -x6374 -x6375 -x6376 x6377 -x6378 -x6379 -x6380 -x6381 -x6382 -x6383 -x6384 -x6385 -x6386 -x6387 -x6388 -x6389 -x6390 -x6391 -x6392 -x6393 -x6394 -x6395 -x6396 -x6397 -x6398 -x6399 -x6400 -x6401 -x6402 -x6403 -x6404 -x6405 -x6406 -x6407 -x6408 -x6409 -x6410 -x6411 -x6412 -x6413 -x6414 -x6415 -x6416 -x6417 -x6418 -x6419 -x6420 -x6421 -x6422 -x6423 -x6424 -x6425 -x6426 -x6427 -x6428 -x6429 -x6430 -x6431 -x6432 -x6433 -x6434 -x6435 -x6436 -x6437 -x6438 -x6439 -x6440 -x6441 -x6442 -x6443 -x6444 -x6445 -x6446 -x6447 -x6448 -x6449 -x6450 -x6451 -x6452 -x6453 -x6454 -x6455 x6456 -x6457 -x6458 -x6459 -x6460 -x6461 -x6462 -x6463 -x6464 -x6465 -x6466 -x6467 -x6468 -x6469 -x6470 -x6471 -x6472 -x6473 -x6474 -x6475 -x6476 -x6477 x6478 -x6479 -x6480 -x6481 -x6482 -x6483 -x6484 -x6485 -x6486 -x6487 -x6488 -x6489 -x6490 -x6491 -x6492 -x6493 -x6494 -x6495 -x6496 -x6497 -x6498 -x6499 -x6500 -x6501 -x6502 -x6503 -x6504 -x6505 -x6506 -x6507 -x6508 -x6509 -x6510 -x6511 -x6512 x6513 -x6514 -x6515 -x6516 -x6517 -x6518 -x6519 -x6520 -x6521 -x6522 -x6523 -x6524 -x6525 -x6526 -x6527 -x6528 -x6529 -x6530 -x6531 -x6532 -x6533 -x6534 -x6535 -x6536 -x6537 -x6538 -x6539 -x6540 -x6541 -x6542 -x6543 -x6544 -x6545 -x6546 -x6547 -x6548 -x6549 -x6550 -x6551 -x6552 -x6553 -x6554 -x6555 -x6556 -x6557 -x6558 -x6559 -x6560 -x6561 -x6562 -x6563 -x6564 -x6565 -x6566 -x6567 -x6568 -x6569 x6570 -x6571 -x6572 -x6573 -x6574 -x6575 -x6576 -x6577 -x6578 -x6579 -x6580 -x6581 -x6582 -x6583 -x6584 -x6585 -x6586 -x6587 -x6588 -x6589 -x6590 -x6591 -x6592 -x6593 -x6594 -x6595 -x6596 -x6597 -x6598 -x6599 -x6600 -x6601 -x6602 -x6603 -x6604 -x6605 -x6606 -x6607 -x6608 -x6609 -x6610 -x6611 -x6612 -x6613 -x6614 -x6615 -x6616 -x6617 -x6618 -x6619 -x6620 -x6621 -x6622 -x6623 -x6624 -x6625 -x6626 -x6627 -x6628 -x6629 -x6630 -x6631 -x6632 -x6633 -x6634 -x6635 -x6636 -x6637 -x6638 -x6639 -x6640 -x6641 -x6642 -x6643 -x6644 -x6645 -x6646 -x6647 -x6648 -x6649 -x6650 -x6651 -x6652 -x6653 -x6654 -x6655 -x6656 -x6657 -x6658 -x6659 -x6660 -x6661 -x6662 -x6663 -x6664 -x6665 -x6666 -x6667 -x6668 -x6669 -x6670 -x6671 -x6672 -x6673 -x6674 -x6675 -x6676 -x6677 -x6678 -x6679 -x6680 -x6681 -x6682 -x6683 -x6684 -x6685 -x6686 -x6687 -x6688 -x6689 -x6690 -x6691 -x6692 -x6693 -x6694 -x6695 -x6696 -x6697 -x6698 -x6699 -x6700 -x6701 -x6702 -x6703 -x6704 -x6705 -x6706 -x6707 -x6708 -x6709 -x6710 -x6711 -x6712 -x6713 -x6714 -x6715 -x6716 -x6717 -x6718 -x6719 -x6720 -x6721 -x6722 -x6723 -x6724 -x6725 -x6726 -x6727 -x6728 -x6729 -x6730 -x6731 -x6732 -x6733 -x6734 -x6735 -x6736 -x6737 -x6738 -x6739 -x6740 -x6741 -x6742 -x6743 -x6744 -x6745 -x6746 -x6747 -x6748 -x6749 -x6750 -x6751 -x6752 -x6753 -x6754 -x6755 -x6756 -x6757 -x6758 -x6759 -x6760 -x6761 -x6762 -x6763 -x6764 -x6765 -x6766 -x6767 -x6768 -x6769 -x6770 -x6771 -x6772 -x6773 -x6774 -x6775 -x6776 -x6777 -x6778 -x6779 -x6780 -x6781 -x6782 -x6783 -x6784 -x6785 -x6786 -x6787 -x6788 -x6789 -x6790 -x6791 -x6792 -x6793 -x6794 -x6795 -x6796 -x6797 -x6798 -x6799 -x6800 -x6801 -x6802 -x6803 -x6804 -x6805 -x6806 -x6807 -x6808 -x6809 -x6810 -x6811 -x6812 -x6813 -x6814 -x6815 -x6816 -x6817 -x6818 -x6819 -x6820 -x6821 -x6822 -x6823 -x6824 -x6825 -x6826 -x6827 -x6828 -x6829 -x6830 -x6831 -x6832 -x6833 -x6834 -x6835 -x6836 -x6837 -x6838 -x6839 -x6840 -x6841 -x6842 -x6843 -x6844 -x6845 -x6846 -x6847 -x6848 -x6849 -x6850 -x6851 -x6852 -x6853 -x6854 -x6855 -x6856 -x6857 -x6858 -x6859 -x6860 -x6861 -x6862 x6863 -x6864 -x6865 -x6866 -x6867 -x6868 -x6869 -x6870 -x6871 -x6872 -x6873 -x6874 -x6875 -x6876 -x6877 -x6878 -x6879 -x6880 -x6881 -x6882 -x6883 -x6884 -x6885 -x6886 -x6887 -x6888 -x6889 -x6890 -x6891 -x6892 -x6893 -x6894 -x6895 -x6896 -x6897 -x6898 -x6899 -x6900 -x6901 -x6902 -x6903 -x6904 x6905 -x6906 -x6907 -x6908 -x6909 -x6910 -x6911 -x6912 -x6913 -x6914 -x6915 -x6916 -x6917 -x6918 -x6919 -x6920 -x6921 -x6922 -x6923 -x6924 -x6925 -x6926 -x6927 -x6928 -x6929 -x6930 -x6931 -x6932 -x6933 -x6934 -x6935 -x6936 -x6937 -x6938 -x6939 -x6940 -x6941 -x6942 -x6943 -x6944 -x6945 -x6946 -x6947 -x6948 -x6949 -x6950 -x6951 -x6952 -x6953 -x6954 -x6955 -x6956 -x6957 -x6958 -x6959 -x6960 -x6961 -x6962 -x6963 -x6964 -x6965 -x6966 -x6967 -x6968 -x6969 -x6970 -x6971 -x6972 -x6973 -x6974 -x6975 -x6976 -x6977 -x6978 -x6979 -x6980 -x6981 -x6982 -x6983 -x6984 -x6985 -x6986 x6987 -x6988 -x6989 -x6990 -x6991 -x6992 -x6993 -x6994 -x6995 -x6996 -x6997 -x6998 -x6999 -x7000 -x7001 -x7002 -x7003 -x7004 -x7005 -x7006 -x7007 -x7008 -x7009 -x7010 -x7011 -x7012 -x7013 -x7014 -x7015 -x7016 -x7017 -x7018 -x7019 -x7020 -x7021 -x7022 -x7023 -x7024 -x7025 -x7026 -x7027 -x7028 -x7029 -x7030 -x7031 -x7032 -x7033 -x7034 -x7035 -x7036 -x7037 -x7038 -x7039 -x7040 -x7041 -x7042 -x7043 -x7044 -x7045 -x7046 -x7047 -x7048 -x7049 -x7050 -x7051 -x7052 -x7053 -x7054 -x7055 -x7056 -x7057 -x7058 -x7059 -x7060 -x7061 -x7062 -x7063 -x7064 -x7065 -x7066 -x7067 -x7068 -x7069 -x7070 -x7071 -x7072 -x7073 -x7074 -x7075 -x7076 -x7077 -x7078 -x7079 -x7080 -x7081 -x7082 -x7083 -x7084 -x7085 -x7086 -x7087 -x7088 -x7089 -x7090 -x7091 -x7092 -x7093 -x7094 -x7095 -x7096 -x7097 -x7098 -x7099 -x7100 -x7101 -x7102 -x7103 -x7104 -x7105 -x7106 -x7107 -x7108 -x7109 -x7110 -x7111 -x7112 -x7113 -x7114 -x7115 -x7116 -x7117 -x7118 -x7119 -x7120 -x7121 -x7122 -x7123 -x7124 -x7125 -x7126 -x7127 -x7128 -x7129 -x7130 -x7131 -x7132 -x7133 -x7134 -x7135 x7136 -x7137 -x7138 -x7139 -x7140 -x7141 -x7142 -x7143 -x7144 -x7145 -x7146 -x7147 -x7148 -x7149 -x7150 -x7151 -x7152 -x7153 -x7154 -x7155 -x7156 -x7157 -x7158 -x7159 x7160 -x7161 -x7162 -x7163 -x7164 -x7165 -x7166 -x7167 -x7168 -x7169 -x7170 -x7171 -x7172 -x7173 -x7174 -x7175 -x7176 -x7177 -x7178 -x7179 -x7180 -x7181 -x7182 -x7183 -x7184 -x7185 -x7186 -x7187 -x7188 -x7189 -x7190 -x7191 -x7192 -x7193 -x7194 -x7195 -x7196 -x7197 -x7198 -x7199 -x7200 -x7201 -x7202 -x7203 -x7204 -x7205 -x7206 -x7207 -x7208 -x7209 -x7210 -x7211 -x7212 -x7213 -x7214 -x7215 -x7216 -x7217 -x7218 -x7219 -x7220 -x7221 -x7222 -x7223 -x7224 -x7225 -x7226 -x7227 -x7228 -x7229 -x7230 -x7231 -x7232 -x7233 -x7234 -x7235 -x7236 -x7237 -x7238 -x7239 -x7240 -x7241 -x7242 -x7243 -x7244 -x7245 -x7246 -x7247 -x7248 -x7249 -x7250 -x7251 -x7252 -x7253 -x7254 -x7255 -x7256 -x7257 -x7258 -x7259 -x7260 -x7261 -x7262 -x7263 -x7264 -x7265 -x7266 -x7267 -x7268 -x7269 -x7270 -x7271 -x7272 -x7273 -x7274 -x7275 -x7276 -x7277 -x7278 -x7279 -x7280 -x7281 -x7282 -x7283 -x7284 -x7285 -x7286 -x7287 -x7288 -x7289 -x7290 -x7291 -x7292 -x7293 -x7294 -x7295 -x7296 -x7297 -x7298 -x7299 -x7300 -x7301 -x7302 -x7303 -x7304 -x7305 -x7306 -x7307 -x7308 -x7309 -x7310 -x7311 -x7312 -x7313 -x7314 -x7315 -x7316 -x7317 -x7318 -x7319 -x7320 -x7321 -x7322 -x7323 -x7324 -x7325 -x7326 -x7327 -x7328 -x7329 -x7330 -x7331 -x7332 -x7333 -x7334 -x7335 -x7336 -x7337 -x7338 -x7339 -x7340 -x7341 -x7342 -x7343 -x7344 -x7345 -x7346 -x7347 -x7348 -x7349 -x7350 -x7351 -x7352 -x7353 -x7354 -x7355 -x7356 -x7357 -x7358 -x7359 -x7360 -x7361 -x7362 -x7363 -x7364 -x7365 -x7366 -x7367 -x7368 -x7369 -x7370 -x7371 -x7372 -x7373 -x7374 -x7375 -x7376 -x7377 -x7378 -x7379 -x7380 -x7381 -x7382 -x7383 -x7384 -x7385 -x7386 -x7387 -x7388 -x7389 -x7390 -x7391 -x7392 -x7393 -x7394 -x7395 -x7396 -x7397 -x7398 -x7399 -x7400 -x7401 -x7402 -x7403 -x7404 -x7405 -x7406 -x7407 -x7408 -x7409 -x7410 -x7411 x7412 -x7413 -x7414 -x7415 -x7416 -x7417 -x7418 -x7419 -x7420 -x7421 -x7422 -x7423 -x7424 -x7425 -x7426 -x7427 -x7428 -x7429 -x7430 -x7431 -x7432 -x7433 -x7434 -x7435 -x7436 -x7437 -x7438 -x7439 -x7440 -x7441 -x7442 -x7443 -x7444 -x7445 -x7446 -x7447 -x7448 -x7449 -x7450 -x7451 -x7452 -x7453 -x7454 -x7455 -x7456 -x7457 -x7458 -x7459 -x7460 -x7461 -x7462 -x7463 -x7464 -x7465 -x7466 -x7467 -x7468 -x7469 -x7470 -x7471 -x7472 -x7473 -x7474 -x7475 -x7476 -x7477 -x7478 -x7479 -x7480 -x7481 -x7482 -x7483 -x7484 -x7485 -x7486 -x7487 -x7488 -x7489 -x7490 -x7491 -x7492 -x7493 -x7494 -x7495 -x7496 -x7497 -x7498 -x7499 -x7500 -x7501 -x7502 -x7503 -x7504 -x7505 -x7506 -x7507 -x7508 -x7509 -x7510 -x7511 -x7512 -x7513 -x7514 -x7515 -x7516 -x7517 -x7518 -x7519 -x7520 -x7521 -x7522 -x7523 -x7524 -x7525 -x7526 -x7527 -x7528 -x7529 -x7530 -x7531 -x7532 -x7533 -x7534 -x7535 -x7536 -x7537 -x7538 -x7539 -x7540 -x7541 -x7542 -x7543 -x7544 -x7545 -x7546 -x7547 -x7548 -x7549 -x7550 -x7551 -x7552 -x7553 -x7554 -x7555 -x7556 -x7557 -x7558 -x7559 -x7560 -x7561 -x7562 -x7563 -x7564 -x7565 -x7566 -x7567 -x7568 -x7569 x7570 -x7571 -x7572 -x7573 -x7574 -x7575 -x7576 -x7577 -x7578 -x7579 -x7580 -x7581 -x7582 -x7583 -x7584 -x7585 -x7586 -x7587 -x7588 -x7589 -x7590 -x7591 -x7592 -x7593 -x7594 -x7595 -x7596 -x7597 -x7598 -x7599 -x7600 -x7601 -x7602 -x7603 -x7604 -x7605 -x7606 -x7607 -x7608 -x7609 -x7610 -x7611 -x7612 -x7613 -x7614 -x7615 -x7616 -x7617 -x7618 -x7619 -x7620 -x7621 -x7622 -x7623 -x7624 -x7625 -x7626 -x7627 -x7628 -x7629 -x7630 -x7631 -x7632 -x7633 -x7634 -x7635 -x7636 -x7637 -x7638 -x7639 -x7640 -x7641 -x7642 -x7643 -x7644 -x7645 -x7646 -x7647 -x7648 -x7649 -x7650 -x7651 -x7652 -x7653 -x7654 -x7655 -x7656 -x7657 -x7658 -x7659 -x7660 -x7661 -x7662 -x7663 -x7664 -x7665 -x7666 -x7667 -x7668 -x7669 -x7670 -x7671 -x7672 -x7673 -x7674 -x7675 -x7676 -x7677 -x7678 -x7679 -x7680 -x7681 -x7682 -x7683 -x7684 -x7685 -x7686 -x7687 -x7688 -x7689 -x7690 -x7691 -x7692 -x7693 -x7694 -x7695 -x7696 -x7697 -x7698 -x7699 -x7700 -x7701 -x7702 -x7703 -x7704 -x7705 -x7706 -x7707 -x7708 -x7709 -x7710 -x7711 -x7712 -x7713 -x7714 -x7715 -x7716 -x7717 -x7718 -x7719 -x7720 x7721 -x7722 -x7723 -x7724 -x7725 -x7726 -x7727 -x7728 -x7729 -x7730 -x7731 -x7732 -x7733 -x7734 -x7735 -x7736 -x7737 -x7738 -x7739 -x7740 -x7741 -x7742 -x7743 -x7744 -x7745 -x7746 -x7747 -x7748 -x7749 -x7750 -x7751 -x7752 -x7753 -x7754 -x7755 -x7756 -x7757 -x7758 -x7759 -x7760 -x7761 -x7762 -x7763 -x7764 -x7765 -x7766 -x7767 -x7768 -x7769 -x7770 -x7771 -x7772 -x7773 -x7774 -x7775 -x7776 -x7777 -x7778 -x7779 -x7780 -x7781 -x7782 -x7783 -x7784 -x7785 -x7786 -x7787 -x7788 -x7789 -x7790 -x7791 -x7792 -x7793 -x7794 -x7795 -x7796 -x7797 -x7798 -x7799 -x7800 -x7801 -x7802 -x7803 -x7804 -x7805 -x7806 -x7807 -x7808 -x7809 -x7810 -x7811 -x7812 -x7813 -x7814 -x7815 -x7816 -x7817 -x7818 -x7819 -x7820 -x7821 -x7822 -x7823 -x7824 -x7825 -x7826 -x7827 -x7828 -x7829 -x7830 -x7831 -x7832 -x7833 -x7834 -x7835 -x7836 -x7837 -x7838 -x7839 -x7840 -x7841 -x7842 -x7843 -x7844 -x7845 -x7846 -x7847 -x7848 -x7849 -x7850 -x7851 -x7852 -x7853 -x7854 -x7855 -x7856 -x7857 -x7858 -x7859 -x7860 -x7861 -x7862 -x7863 -x7864 -x7865 -x7866 -x7867 -x7868 -x7869 -x7870 -x7871 -x7872 -x7873 -x7874 -x7875 -x7876 -x7877 -x7878 -x7879 -x7880 -x7881 -x7882 -x7883 -x7884 -x7885 -x7886 -x7887 -x7888 -x7889 -x7890 -x7891 -x7892 -x7893 -x7894 -x7895 -x7896 -x7897 -x7898 -x7899 -x7900 -x7901 -x7902 -x7903 -x7904 -x7905 -x7906 -x7907 -x7908 -x7909 -x7910 -x7911 -x7912 -x7913 -x7914 -x7915 -x7916 -x7917 -x7918 -x7919 -x7920 -x7921 -x7922 -x7923 -x7924 -x7925 -x7926 -x7927 -x7928 -x7929 -x7930 -x7931 -x7932 -x7933 -x7934 -x7935 -x7936 -x7937 -x7938 -x7939 -x7940 -x7941 -x7942 -x7943 -x7944 -x7945 -x7946 -x7947 -x7948 -x7949 -x7950 -x7951 -x7952 -x7953 -x7954 -x7955 -x7956 -x7957 -x7958 -x7959 -x7960 -x7961 -x7962 -x7963 -x7964 -x7965 -x7966 -x7967 -x7968 -x7969 -x7970 -x7971 -x7972 -x7973 -x7974 -x7975 -x7976 -x7977 -x7978 -x7979 -x7980 -x7981 -x7982 -x7983 -x7984 -x7985 -x7986 -x7987 -x7988 -x7989 -x7990 -x7991 -x7992 -x7993 -x7994 -x7995 -x7996 -x7997 -x7998 -x7999 -x8000 -x8001 -x8002 -x8003 -x8004 -x8005 -x8006 -x8007 -x8008 -x8009 -x8010 -x8011 -x8012 -x8013 -x8014 -x8015 -x8016 -x8017 -x8018 -x8019 -x8020 -x8021 -x8022 -x8023 -x8024 -x8025 -x8026 -x8027 -x8028 -x8029 -x8030 -x8031 -x8032 -x8033 -x8034 -x8035 -x8036 -x8037 -x8038 -x8039 -x8040 -x8041 -x8042 -x8043 x8044 -x8045 -x8046 -x8047 -x8048 -x8049 -x8050 -x8051 -x8052 -x8053 -x8054 -x8055 -x8056 -x8057 -x8058 -x8059 -x8060 -x8061 -x8062 -x8063 -x8064 -x8065 -x8066 -x8067 -x8068 -x8069 -x8070 -x8071 -x8072 -x8073 -x8074 -x8075 -x8076 -x8077 -x8078 -x8079 -x8080 -x8081 -x8082 -x8083 -x8084 -x8085 -x8086 -x8087 -x8088 -x8089 -x8090 -x8091 -x8092 -x8093 -x8094 -x8095 -x8096 -x8097 -x8098 -x8099 -x8100 -x8101 -x8102 -x8103 -x8104 -x8105 -x8106 -x8107 -x8108 -x8109 -x8110 -x8111 -x8112 -x8113 -x8114 -x8115 -x8116 -x8117 -x8118 -x8119 -x8120 -x8121 -x8122 -x8123 -x8124 -x8125 -x8126 -x8127 -x8128 -x8129 -x8130 -x8131 -x8132 -x8133 -x8134 -x8135 -x8136 -x8137 -x8138 -x8139 -x8140 -x8141 -x8142 -x8143 -x8144 -x8145 -x8146 -x8147 -x8148 -x8149 -x8150 -x8151 x8152 -x8153 -x8154 -x8155 -x8156 -x8157 -x8158 -x8159 -x8160 -x8161 -x8162 -x8163 -x8164 -x8165 -x8166 -x8167 -x8168 -x8169 -x8170 -x8171 -x8172 -x8173 -x8174 -x8175 -x8176 -x8177 -x8178 -x8179 -x8180 -x8181 -x8182 -x8183 -x8184 -x8185 -x8186 -x8187 -x8188 -x8189 -x8190 -x8191 -x8192 -x8193 -x8194 -x8195 x8196 -x8197 -x8198 -x8199 -x8200 -x8201 -x8202 -x8203 -x8204 -x8205 x8206 -x8207 -x8208 -x8209 -x8210 -x8211 -x8212 -x8213 -x8214 -x8215 -x8216 -x8217 -x8218 -x8219 -x8220 -x8221 -x8222 -x8223 -x8224 -x8225 -x8226 x8227 -x8228 -x8229 -x8230 -x8231 -x8232 -x8233 -x8234 -x8235 -x8236 -x8237 -x8238 -x8239 -x8240 -x8241 x8242 -x8243 -x8244 -x8245 -x8246 -x8247 -x8248 -x8249 -x8250 -x8251 -x8252 -x8253 -x8254 -x8255 -x8256 -x8257 -x8258 -x8259 -x8260 -x8261 -x8262 -x8263 -x8264 -x8265 -x8266 -x8267 -x8268 -x8269 -x8270 -x8271 -x8272 -x8273 -x8274 -x8275 -x8276 -x8277 -x8278 -x8279 -x8280 -x8281 -x8282 -x8283 -x8284 -x8285 -x8286 -x8287 -x8288 -x8289 -x8290 -x8291 -x8292 -x8293 -x8294 -x8295 -x8296 -x8297 -x8298 x8299 -x8300 -x8301 -x8302 -x8303 -x8304 -x8305 -x8306 -x8307 -x8308 -x8309 -x8310 -x8311 -x8312 -x8313 -x8314 -x8315 -x8316 -x8317 -x8318 -x8319 -x8320 -x8321 -x8322 -x8323 -x8324 -x8325 -x8326 -x8327 -x8328 -x8329 -x8330 -x8331 -x8332 -x8333 -x8334 -x8335 -x8336 -x8337 -x8338 -x8339 -x8340 -x8341 -x8342 -x8343 -x8344 -x8345 -x8346 -x8347 -x8348 -x8349 -x8350 -x8351 -x8352 -x8353 -x8354 -x8355 -x8356 -x8357 -x8358 -x8359 -x8360 -x8361 -x8362 -x8363 -x8364 -x8365 -x8366 -x8367 -x8368 -x8369 -x8370 -x8371 -x8372 -x8373 -x8374 -x8375 -x8376 x8377 -x8378 -x8379 -x8380 -x8381 -x8382 -x8383 -x8384 -x8385 -x8386 -x8387 -x8388 -x8389 -x8390 -x8391 -x8392 -x8393 -x8394 -x8395 -x8396 -x8397 -x8398 -x8399 -x8400 -x8401 -x8402 -x8403 -x8404 -x8405 -x8406 -x8407 -x8408 -x8409 -x8410 -x8411 x8412 -x8413 -x8414 -x8415 -x8416 -x8417 -x8418 -x8419 -x8420 -x8421 -x8422 -x8423 -x8424 -x8425 -x8#### 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.92 0.98 0.91 2/54 6248
Raw data (stat): 6248 (runsolver) R 6247 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487844834 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+10.0006 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 28727 0 0 0 928 70 0 0 25 0 1 0 487844834 106606592 21394 4294967295 134512640 134672761 3221224576 3220462272 134523717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26027 21394 603 41 0 25986 0
vsize: 104108
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 56627 0 0 0 1867 130 0 0 25 0 1 0 487844834 217231360 43691 4294967295 134512640 134672761 3221224576 3221222564 134544430 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53035 43691 603 41 0 52994 0
vsize: 212140
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 84864 0 0 0 2801 197 0 0 25 0 1 0 487844834 296468480 66637 4294967295 134512640 134672761 3221224576 3221223120 134621517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72380 66637 603 41 0 72339 0
vsize: 289520
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 86650 0 0 0 3796 202 0 0 25 0 1 0 487844834 299765760 67299 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73185 67299 603 41 0 73144 0
vsize: 292740
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 86762 0 0 0 4796 202 0 0 25 0 1 0 487844834 300281856 67411 4294967295 134512640 134672761 3221224576 3221223712 134614503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73311 67411 603 41 0 73270 0
vsize: 293244
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 86776 0 0 0 5796 202 0 0 25 0 1 0 487844834 300281856 67425 4294967295 134512640 134672761 3221224576 3221223700 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73311 67425 603 41 0 73270 0
vsize: 293244
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 86876 0 0 0 6796 202 0 0 25 0 1 0 487844834 300683264 67525 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73409 67525 603 41 0 73368 0
vsize: 293636
[startup+80.002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 87101 0 0 0 7796 203 0 0 25 0 1 0 487844834 301608960 67750 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73635 67750 603 41 0 73594 0
vsize: 294540
[startup+90.002 s]
Raw data (loadavg): 1.05 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 87216 0 0 0 8796 203 0 0 25 0 1 0 487844834 301993984 67865 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73729 67865 603 41 0 73688 0
vsize: 294916
[startup+100.003 s]
Raw data (loadavg): 1.04 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 87240 0 0 0 9796 203 0 0 25 0 1 0 487844834 302125056 67889 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73761 67889 603 41 0 73720 0
vsize: 295044
[startup+110.003 s]
Raw data (loadavg): 1.03 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 87613 0 0 0 10795 205 0 0 25 0 1 0 487844834 303579136 68262 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74116 68262 603 41 0 74075 0
vsize: 296464
[startup+120.003 s]
Raw data (loadavg): 1.03 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 87662 0 0 0 11795 205 0 0 25 0 1 0 487844834 303710208 68311 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74148 68311 603 41 0 74107 0
vsize: 296592
[startup+130.004 s]
Raw data (loadavg): 1.02 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 87877 0 0 0 12794 206 0 0 25 0 1 0 487844834 304631808 68526 4294967295 134512640 134672761 3221224576 3221223728 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74373 68526 603 41 0 74332 0
vsize: 297492
[startup+140.005 s]
Raw data (loadavg): 1.02 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 88061 0 0 0 13794 206 0 0 25 0 1 0 487844834 305426432 68710 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74567 68710 603 41 0 74526 0
vsize: 298268
[startup+150.006 s]
Raw data (loadavg): 1.02 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 88094 0 0 0 14794 206 0 0 25 0 1 0 487844834 305561600 68743 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74600 68743 603 41 0 74559 0
vsize: 298400
[startup+160.005 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 88675 0 0 0 15793 208 0 0 25 0 1 0 487844834 307949568 69324 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75183 69324 603 41 0 75142 0
vsize: 300732
[startup+170.005 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89146 0 0 0 16792 209 0 0 25 0 1 0 487844834 309870592 69795 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75652 69795 603 41 0 75611 0
vsize: 302608
[startup+180.005 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89598 0 0 0 17791 210 0 0 25 0 1 0 487844834 311709696 70247 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76101 70247 603 41 0 76060 0
vsize: 304404
[startup+190.005 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89632 0 0 0 18791 210 0 0 25 0 1 0 487844834 311840768 70281 4294967295 134512640 134672761 3221224576 3221223700 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76133 70281 603 41 0 76092 0
vsize: 304532
[startup+200.005 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89657 0 0 0 19791 210 0 0 25 0 1 0 487844834 311975936 70306 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76166 70306 603 41 0 76125 0
vsize: 304664
[startup+210.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89678 0 0 0 20791 210 0 0 25 0 1 0 487844834 311975936 70327 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76166 70327 603 41 0 76125 0
vsize: 304664
[startup+220.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89696 0 0 0 21791 210 0 0 25 0 1 0 487844834 312107008 70345 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76198 70345 603 41 0 76157 0
vsize: 304792
[startup+230.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89703 0 0 0 22791 210 0 0 25 0 1 0 487844834 312107008 70352 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76198 70352 603 41 0 76157 0
vsize: 304792
[startup+240.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89728 0 0 0 23792 210 0 0 25 0 1 0 487844834 312344576 70377 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76256 70377 603 41 0 76215 0
vsize: 305024
[startup+250.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89729 0 0 0 24792 210 0 0 25 0 1 0 487844834 312344576 70378 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76256 70378 603 41 0 76215 0
vsize: 305024
[startup+260.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89756 0 0 0 25792 210 0 0 25 0 1 0 487844834 312344576 70405 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76256 70405 603 41 0 76215 0
vsize: 305024
[startup+270.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 89913 0 0 0 26792 211 0 0 25 0 1 0 487844834 312999936 70562 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76416 70562 603 41 0 76375 0
vsize: 305664
[startup+280.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 90513 0 0 0 27791 212 0 0 25 0 1 0 487844834 315514880 71162 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77030 71162 603 41 0 76989 0
vsize: 308120
[startup+290.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 91603 0 0 0 28788 215 0 0 25 0 1 0 487844834 319864832 72252 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78092 72252 603 41 0 78051 0
vsize: 312368
[startup+300.009 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 92241 0 0 0 29787 216 0 0 25 0 1 0 487844834 322498560 72890 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78735 72890 603 41 0 78694 0
vsize: 314940
[startup+310.009 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93054 0 0 0 30784 219 0 0 25 0 1 0 487844834 325914624 73703 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79569 73703 603 41 0 79528 0
vsize: 318276
[startup+320.009 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93302 0 0 0 31784 219 0 0 25 0 1 0 487844834 326836224 73951 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79794 73951 603 41 0 79753 0
vsize: 319176
[startup+330.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93534 0 0 0 32784 220 0 0 25 0 1 0 487844834 327860224 74183 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80044 74183 603 41 0 80003 0
vsize: 320176
[startup+340.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93607 0 0 0 33784 220 0 0 25 0 1 0 487844834 328134656 74256 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80111 74256 603 41 0 80070 0
vsize: 320444
[startup+350.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93680 0 0 0 34784 220 0 0 25 0 1 0 487844834 328417280 74329 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80180 74329 603 41 0 80139 0
vsize: 320720
[startup+360.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93700 0 0 0 35783 220 0 0 25 0 1 0 487844834 328548352 74349 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80212 74349 603 41 0 80171 0
vsize: 320848
[startup+370.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93722 0 0 0 36783 221 0 0 25 0 1 0 487844834 328548352 74371 4294967295 134512640 134672761 3221224576 3221223760 134616001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80212 74371 603 41 0 80171 0
vsize: 320848
[startup+380.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93751 0 0 0 37783 221 0 0 25 0 1 0 487844834 328683520 74400 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80245 74400 603 41 0 80204 0
vsize: 320980
[startup+390.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93772 0 0 0 38783 221 0 0 25 0 1 0 487844834 328818688 74421 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80278 74421 603 41 0 80237 0
vsize: 321112
[startup+400.011 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93805 0 0 0 39783 221 0 0 25 0 1 0 487844834 328945664 74454 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80309 74454 603 41 0 80268 0
vsize: 321236
[startup+410.012 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93851 0 0 0 40783 221 0 0 25 0 1 0 487844834 329076736 74500 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80341 74500 603 41 0 80300 0
vsize: 321364
[startup+420.012 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93869 0 0 0 41783 221 0 0 25 0 1 0 487844834 329211904 74518 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80374 74518 603 41 0 80333 0
vsize: 321496
[startup+430.012 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93927 0 0 0 42783 222 0 0 25 0 1 0 487844834 329351168 74576 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80408 74576 603 41 0 80367 0
vsize: 321632
[startup+440.012 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 93965 0 0 0 43784 222 0 0 25 0 1 0 487844834 329621504 74614 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80474 74614 603 41 0 80433 0
vsize: 321896
[startup+450.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94007 0 0 0 44784 222 0 0 25 0 1 0 487844834 329752576 74656 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80506 74656 603 41 0 80465 0
vsize: 322024
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94114 0 0 0 45783 222 0 0 25 0 1 0 487844834 330149888 74763 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80603 74763 603 41 0 80562 0
vsize: 322412
[startup+470.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94331 0 0 0 46783 223 0 0 25 0 1 0 487844834 331194368 74980 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80858 74980 603 41 0 80817 0
vsize: 323432
[startup+480.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94425 0 0 0 47783 223 0 0 25 0 1 0 487844834 331595776 75074 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80956 75074 603 41 0 80915 0
vsize: 323824
[startup+490.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94499 0 0 0 48783 223 0 0 25 0 1 0 487844834 331857920 75148 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81020 75148 603 41 0 80979 0
vsize: 324080
[startup+500.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94749 0 0 0 49783 224 0 0 25 0 1 0 487844834 332877824 75398 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81269 75398 603 41 0 81228 0
vsize: 325076
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94882 0 0 0 50782 224 0 0 25 0 1 0 487844834 333418496 75531 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81401 75531 603 41 0 81360 0
vsize: 325604
[startup+520.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 94971 0 0 0 51782 225 0 0 25 0 1 0 487844834 333824000 75620 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81500 75620 603 41 0 81459 0
vsize: 326000
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95024 0 0 0 52782 225 0 0 25 0 1 0 487844834 333955072 75673 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81532 75673 603 41 0 81491 0
vsize: 326128
[startup+540.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95088 0 0 0 53782 225 0 0 25 0 1 0 487844834 334225408 75737 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81598 75737 603 41 0 81557 0
vsize: 326392
[startup+550.016 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95191 0 0 0 54782 225 0 0 25 0 1 0 487844834 334749696 75840 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81726 75840 603 41 0 81685 0
vsize: 326904
[startup+560.016 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95354 0 0 0 55782 226 0 0 25 0 1 0 487844834 335413248 76003 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81888 76003 603 41 0 81847 0
vsize: 327552
[startup+570.016 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95674 0 0 0 56782 226 0 0 25 0 1 0 487844834 336728064 76323 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82209 76323 603 41 0 82168 0
vsize: 328836
[startup+580.017 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95691 0 0 0 57782 226 0 0 25 0 1 0 487844834 336728064 76340 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82209 76340 603 41 0 82168 0
vsize: 328836
[startup+590.017 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95710 0 0 0 58782 226 0 0 25 0 1 0 487844834 336863232 76359 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82242 76359 603 41 0 82201 0
vsize: 328968
[startup+600.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95724 0 0 0 59782 226 0 0 25 0 1 0 487844834 336863232 76373 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82242 76373 603 41 0 82201 0
vsize: 328968
[startup+610.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95773 0 0 0 60783 226 0 0 25 0 1 0 487844834 337133568 76422 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82308 76422 603 41 0 82267 0
vsize: 329232
[startup+620.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 95823 0 0 0 61783 226 0 0 25 0 1 0 487844834 337264640 76472 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82340 76472 603 41 0 82299 0
vsize: 329360
[startup+630.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96340 0 0 0 62782 227 0 0 25 0 1 0 487844834 339423232 76989 4294967295 134512640 134672761 3221224576 3221223760 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82867 76989 603 41 0 82826 0
vsize: 331468
[startup+640.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96370 0 0 0 63782 227 0 0 25 0 1 0 487844834 339558400 77019 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82900 77019 603 41 0 82859 0
vsize: 331600
[startup+650.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96435 0 0 0 64782 227 0 0 25 0 1 0 487844834 339832832 77084 4294967295 134512640 134672761 3221224576 3221223728 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82967 77084 603 41 0 82926 0
vsize: 331868
[startup+660.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96449 0 0 0 65783 227 0 0 25 0 1 0 487844834 339832832 77098 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82967 77098 603 41 0 82926 0
vsize: 331868
[startup+670.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96476 0 0 0 66783 227 0 0 25 0 1 0 487844834 339963904 77125 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82999 77125 603 41 0 82958 0
vsize: 331996
[startup+680.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96492 0 0 0 67783 227 0 0 25 0 1 0 487844834 339963904 77141 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82999 77141 603 41 0 82958 0
vsize: 331996
[startup+690.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96514 0 0 0 68783 227 0 0 25 0 1 0 487844834 340099072 77163 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83032 77163 603 41 0 82991 0
vsize: 332128
[startup+700.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96547 0 0 0 69783 227 0 0 25 0 1 0 487844834 340230144 77196 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83064 77196 603 41 0 83023 0
vsize: 332256
[startup+710.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 96586 0 0 0 70783 227 0 0 25 0 1 0 487844834 340365312 77235 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83097 77235 603 41 0 83056 0
vsize: 332388
[startup+720.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 104009 0 0 0 71762 249 0 0 25 0 1 0 487844834 346804224 78788 4294967295 134512640 134672761 3221224576 3220802624 134594037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84669 78788 603 41 0 84628 0
vsize: 338676
[startup+730.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 109141 0 0 0 72748 263 0 0 25 0 1 0 487844834 348459008 79246 4294967295 134512640 134672761 3221224576 3221223760 134593685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85073 79246 603 41 0 85032 0
vsize: 340292
[startup+740.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110895 0 0 0 73743 267 0 0 25 0 1 0 487844834 348172288 79279 4294967295 134512640 134672761 3221224576 3221223700 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79279 603 41 0 84962 0
vsize: 340012
[startup+750.022 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110896 0 0 0 74744 267 0 0 25 0 1 0 487844834 348172288 79280 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79280 603 41 0 84962 0
vsize: 340012
[startup+760.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110896 0 0 0 75744 267 0 0 25 0 1 0 487844834 348172288 79280 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79280 603 41 0 84962 0
vsize: 340012
[startup+770.022 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110897 0 0 0 76744 267 0 0 25 0 1 0 487844834 348172288 79281 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79281 603 41 0 84962 0
vsize: 340012
[startup+780.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110897 0 0 0 77744 267 0 0 25 0 1 0 487844834 348172288 79281 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79281 603 41 0 84962 0
vsize: 340012
[startup+790.022 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110898 0 0 0 78744 267 0 0 25 0 1 0 487844834 348172288 79282 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79282 603 41 0 84962 0
vsize: 340012
[startup+800.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110898 0 0 0 79745 267 0 0 25 0 1 0 487844834 348172288 79282 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79282 603 41 0 84962 0
vsize: 340012
[startup+810.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110899 0 0 0 80745 267 0 0 25 0 1 0 487844834 348172288 79283 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79283 603 41 0 84962 0
vsize: 340012
[startup+820.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110906 0 0 0 81745 267 0 0 25 0 1 0 487844834 348172288 79290 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79290 603 41 0 84962 0
vsize: 340012
[startup+830.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110908 0 0 0 82745 267 0 0 25 0 1 0 487844834 348172288 79292 4294967295 134512640 134672761 3221224576 3221223776 134610652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79292 603 41 0 84962 0
vsize: 340012
[startup+840.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110915 0 0 0 83745 267 0 0 25 0 1 0 487844834 348172288 79299 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79299 603 41 0 84962 0
vsize: 340012
[startup+850.024 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110921 0 0 0 84746 267 0 0 25 0 1 0 487844834 348172288 79305 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79305 603 41 0 84962 0
vsize: 340012
[startup+860.023 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110923 0 0 0 85746 267 0 0 25 0 1 0 487844834 348172288 79307 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79307 603 41 0 84962 0
vsize: 340012
[startup+870.024 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110930 0 0 0 86746 267 0 0 25 0 1 0 487844834 348172288 79314 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79314 603 41 0 84962 0
vsize: 340012
[startup+880.024 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 110941 0 0 0 87746 267 0 0 25 0 1 0 487844834 348172288 79325 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85003 79325 603 41 0 84962 0
vsize: 340012
[startup+890.024 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111021 0 0 0 88746 268 0 0 25 0 1 0 487844834 348295168 79405 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85033 79405 603 41 0 84992 0
vsize: 340132
[startup+900.025 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111035 0 0 0 89746 268 0 0 25 0 1 0 487844834 348295168 79419 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85033 79419 603 41 0 84992 0
vsize: 340132
[startup+910.025 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111083 0 0 0 90746 268 0 0 25 0 1 0 487844834 348426240 79467 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85065 79467 603 41 0 85024 0
vsize: 340260
[startup+920.025 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111216 0 0 0 91746 268 0 0 25 0 1 0 487844834 349089792 79600 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85227 79600 603 41 0 85186 0
vsize: 340908
[startup+930.025 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111354 0 0 0 92746 269 0 0 25 0 1 0 487844834 349614080 79738 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85355 79738 603 41 0 85314 0
vsize: 341420
[startup+940.026 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111378 0 0 0 93746 269 0 0 25 0 1 0 487844834 349749248 79762 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85388 79762 603 41 0 85347 0
vsize: 341552
[startup+950.026 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111492 0 0 0 94745 269 0 0 25 0 1 0 487844834 350142464 79876 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85484 79876 603 41 0 85443 0
vsize: 341936
[startup+960.027 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111587 0 0 0 95745 270 0 0 25 0 1 0 487844834 350539776 79971 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85581 79971 603 41 0 85540 0
vsize: 342324
[startup+970.027 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111650 0 0 0 96745 270 0 0 25 0 1 0 487844834 350801920 80034 4294967295 134512640 134672761 3221224576 3221223728 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85645 80034 603 41 0 85604 0
vsize: 342580
[startup+980.027 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111707 0 0 0 97745 270 0 0 25 0 1 0 487844834 351068160 80091 4294967295 134512640 134672761 3221224576 3221223712 134614524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85710 80091 603 41 0 85669 0
vsize: 342840
[startup+990.027 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111731 0 0 0 98745 270 0 0 25 0 1 0 487844834 351330304 80115 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85774 80115 603 41 0 85733 0
vsize: 343096
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111773 0 0 0 99745 270 0 0 25 0 1 0 487844834 351592448 80157 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85838 80157 603 41 0 85797 0
vsize: 343352
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111788 0 0 0 100745 271 0 0 25 0 1 0 487844834 351592448 80172 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85838 80172 603 41 0 85797 0
vsize: 343352
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111826 0 0 0 101745 271 0 0 25 0 1 0 487844834 351727616 80210 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85871 80210 603 41 0 85830 0
vsize: 343484
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111858 0 0 0 102745 271 0 0 25 0 1 0 487844834 351862784 80242 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85904 80242 603 41 0 85863 0
vsize: 343616
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 111901 0 0 0 103745 271 0 0 25 0 1 0 487844834 352129024 80285 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85969 80285 603 41 0 85928 0
vsize: 343876
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112014 0 0 0 104745 271 0 0 25 0 1 0 487844834 352522240 80398 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86065 80398 603 41 0 86024 0
vsize: 344260
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112031 0 0 0 105746 271 0 0 25 0 1 0 487844834 352657408 80415 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86098 80415 603 41 0 86057 0
vsize: 344392
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112090 0 0 0 106746 271 0 0 25 0 1 0 487844834 352788480 80474 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86130 80474 603 41 0 86089 0
vsize: 344520
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112113 0 0 0 107746 272 0 0 25 0 1 0 487844834 352919552 80497 4294967295 134512640 134672761 3221224576 3221223700 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86162 80497 603 41 0 86121 0
vsize: 344648
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112140 0 0 0 108746 272 0 0 25 0 1 0 487844834 353054720 80524 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86195 80524 603 41 0 86154 0
vsize: 344780
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112163 0 0 0 109746 272 0 0 25 0 1 0 487844834 353185792 80547 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86227 80547 603 41 0 86186 0
vsize: 344908
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112179 0 0 0 110746 272 0 0 25 0 1 0 487844834 353185792 80563 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86227 80563 603 41 0 86186 0
vsize: 344908
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112204 0 0 0 111746 272 0 0 25 0 1 0 487844834 353320960 80588 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86260 80588 603 41 0 86219 0
vsize: 345040
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112271 0 0 0 112746 272 0 0 25 0 1 0 487844834 353583104 80655 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86324 80655 603 41 0 86283 0
vsize: 345296
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112293 0 0 0 113746 272 0 0 25 0 1 0 487844834 353718272 80677 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86357 80677 603 41 0 86316 0
vsize: 345428
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112315 0 0 0 114746 272 0 0 25 0 1 0 487844834 353718272 80699 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86357 80699 603 41 0 86316 0
vsize: 345428
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112411 0 0 0 115746 273 0 0 25 0 1 0 487844834 354123776 80795 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86456 80795 603 41 0 86415 0
vsize: 345824
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112445 0 0 0 116746 273 0 0 25 0 1 0 487844834 354254848 80829 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86488 80829 603 41 0 86447 0
vsize: 345952
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112467 0 0 0 117746 273 0 0 25 0 1 0 487844834 354390016 80851 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86521 80851 603 41 0 86480 0
vsize: 346084
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112482 0 0 0 118746 273 0 0 25 0 1 0 487844834 354390016 80866 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86521 80866 603 41 0 86480 0
vsize: 346084
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 6248
Raw data (stat): 6248 (minisat+) R 6247 27222 27221 0 -1 0 112538 0 0 0 119746 273 0 0 25 0 1 0 487844834 354648064 80922 4294967295 134512640 134672761 3221224576 3221223712 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86584 80922 603 41 0 86543 0
vsize: 346336
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 1.00 1.00 0.91 1/54 6248
Raw data (stat): 6248 (minisat+) Z 6247 27222 27221 0 -1 12 112539 0 0 0 119748 289 0 0 25 0 1 0 487844834 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.21
CPU time (s): 1200.38
CPU user time (s): 1197.48
CPU system time (s): 2.89356
CPU usage (%): 100.014
Max. virtual memory (Kb): 346336
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####