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 7133

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-14 21:30:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5179 boxname=wulflinc26 idbench=399 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  80cb01878488e5fe06c52c88c5a85bdd  /oldhome/oroussel/tmp/wulflinc26/normalized-air04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc26/normalized-air04.opb
IDLAUNCH: 5179
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        795524 kB
Buffers:         36464 kB
Cached:         162000 kB
SwapCached:       2476 kB
Active:          72696 kB
Inactive:       131084 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        795272 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29748 kB
Committed_AS:    63612 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:50:12 (client local time) WITH STATUS 10 IN 1200.33 SECONDS
stats: 5179 7 1200.33 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310073   809962 |  103357       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 38448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 73418   maxlim: 5096703   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        48 |  823835  2644804 |  274611      48      590    12.3 |  0.000 % |
c |       148 |  823835  2644804 |  302072     148     2027    13.7 |  0.386 % |
c |       299 |  823835  2644804 |  332279     299     8366    28.0 |  0.386 % |
c |       524 |  823835  2644804 |  365507     524    11937    22.8 |  0.386 % |
c ==============================================================================
c [1mFound solution: 37913[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5097238   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       618 |  823885  2645062 |  274628     618    14579    23.6 |  0.386 % |
c |       718 |  823885  2645062 |  302090     718    15509    21.6 |  0.388 % |
c |       870 |  823885  2645062 |  332299     870    18539    21.3 |  0.388 % |
c |      1095 |  823885  2645062 |  365529    1095    84538    77.2 |  0.388 % |
c |      1432 |  823854  2644957 |  402082    1428    88570    62.0 |  0.391 % |
c |      1938 |  823845  2644928 |  442291    1933   153814    79.6 |  0.392 % |
c |      2697 |  823845  2644928 |  486520    2692   241645    89.8 |  0.392 % |
c |      3836 |  823607  2644098 |  535172    3771   306203    81.2 |  0.411 % |
c |      5544 |  823068  2642219 |  588689    5357   421967    78.8 |  0.455 % |
c ==============================================================================
c [1mFound solution: 37389[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5097762   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6327 |  823081  2642321 |  274360    6140   621671   101.2 |  0.455 % |
c |      6427 |  823072  2642290 |  301796    6239   622158    99.7 |  0.458 % |
c |      6577 |  823063  2642261 |  331975    6388   622850    97.5 |  0.459 % |
c |      6802 |  823043  2642189 |  365173    6611   625583    94.6 |  0.461 % |
c |      7139 |  822987  2641993 |  401690    6888   610606    88.6 |  0.466 % |
c |      7645 |  822922  2641766 |  441859    7385   627323    84.9 |  0.472 % |
c |      8404 |  822906  2641714 |  486045    8142   645480    79.3 |  0.473 % |
c |      9544 |  822897  2641685 |  534650    9281   862409    92.9 |  0.474 % |
c |     11252 |  822891  2641665 |  588115   10986  1023661    93.2 |  0.475 % |
c |     13814 |  822845  2641515 |  646926   13542  1404455   103.7 |  0.479 % |
c |     17658 |  822829  2641463 |  711619   17384  1519778    87.4 |  0.480 % |
c |     23425 |  822820  2641434 |  782781   23150  2507373   108.3 |  0.481 % |
c |     32074 |  822802  2641376 |  861059   31797  3125154    98.3 |  0.483 % |
c |     45048 |  822802  2641376 |  947165   44771  8578381   191.6 |  0.483 % |
c |     64509 |  822786  2641324 | 1041881   64229 16722979   260.4 |  0.484 % |
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 -x83#### 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.95 0.90 2/54 5337
Raw data (stat): 5337 (runsolver) R 5336 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487848348 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99949 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 23727 0 0 0 942 56 0 0 25 0 1 0 487848348 95633408 19673 4294967295 134512640 134672761 3221224640 3221222656 134523700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23348 19673 603 41 0 23307 0
vsize: 93392
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 59342 0 0 0 1856 142 0 0 25 0 1 0 487848348 211980288 46060 4294967295 134512640 134672761 3221224640 3221223904 134596859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51753 46060 603 41 0 51712 0
vsize: 207012
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 66312 0 0 0 2838 159 0 0 25 0 1 0 487848348 236429312 53012 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57722 53012 603 41 0 57681 0
vsize: 230888
[startup+40.0005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70232 0 0 0 3829 169 0 0 25 0 1 0 487848348 239992832 53897 4294967295 134512640 134672761 3221224640 3221223824 134593685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58592 53897 603 41 0 58551 0
vsize: 234368
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70281 0 0 0 4829 169 0 0 25 0 1 0 487848348 239706112 53928 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53928 603 41 0 58481 0
vsize: 234088
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70281 0 0 0 5828 169 0 0 25 0 1 0 487848348 239706112 53928 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53928 603 41 0 58481 0
vsize: 234088
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70285 0 0 0 6829 169 0 0 25 0 1 0 487848348 239706112 53932 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53932 603 41 0 58481 0
vsize: 234088
[startup+80.0012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70294 0 0 0 7829 169 0 0 25 0 1 0 487848348 239706112 53941 4294967295 134512640 134672761 3221224640 3221223764 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53941 603 41 0 58481 0
vsize: 234088
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70314 0 0 0 8829 169 0 0 25 0 1 0 487848348 239706112 53961 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53961 603 41 0 58481 0
vsize: 234088
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70330 0 0 0 9829 169 0 0 25 0 1 0 487848348 239706112 53977 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53977 603 41 0 58481 0
vsize: 234088
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70335 0 0 0 10829 169 0 0 25 0 1 0 487848348 239706112 53982 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53982 603 41 0 58481 0
vsize: 234088
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70351 0 0 0 11829 169 0 0 25 0 1 0 487848348 239706112 53998 4294967295 134512640 134672761 3221224640 3221223840 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58522 53998 603 41 0 58481 0
vsize: 234088
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 70423 0 0 0 12829 169 0 0 25 0 1 0 487848348 239841280 54070 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58555 54070 603 41 0 58514 0
vsize: 234220
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 72519 0 0 0 13823 175 0 0 25 0 1 0 487848348 241532928 54393 4294967295 134512640 134672761 3221224640 3221222576 134523032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58968 54393 603 41 0 58927 0
vsize: 235872
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 72920 0 0 0 14822 176 0 0 25 0 1 0 487848348 240672768 54283 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58758 54283 603 41 0 58717 0
vsize: 235032
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 72920 0 0 0 15822 176 0 0 25 0 1 0 487848348 240672768 54283 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58758 54283 603 41 0 58717 0
vsize: 235032
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 72920 0 0 0 16823 176 0 0 25 0 1 0 487848348 240672768 54283 4294967295 134512640 134672761 3221224640 3221223808 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58758 54283 603 41 0 58717 0
vsize: 235032
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 72920 0 0 0 17823 176 0 0 25 0 1 0 487848348 240672768 54283 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58758 54283 603 41 0 58717 0
vsize: 235032
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 72972 0 0 0 18823 176 0 0 25 0 1 0 487848348 241000448 54335 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58838 54335 603 41 0 58797 0
vsize: 235352
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73152 0 0 0 19823 176 0 0 25 0 1 0 487848348 241672192 54515 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59002 54515 603 41 0 58961 0
vsize: 236008
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73333 0 0 0 20822 177 0 0 25 0 1 0 487848348 242483200 54696 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59200 54696 603 41 0 59159 0
vsize: 236800
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73484 0 0 0 21822 178 0 0 25 0 1 0 487848348 243023872 54847 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59332 54847 603 41 0 59291 0
vsize: 237328
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73627 0 0 0 22821 178 0 0 25 0 1 0 487848348 243699712 54990 4294967295 134512640 134672761 3221224640 3221223784 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59497 54990 603 41 0 59456 0
vsize: 237988
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73694 0 0 0 23821 178 0 0 25 0 1 0 487848348 243970048 55057 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59563 55057 603 41 0 59522 0
vsize: 238252
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73708 0 0 0 24822 178 0 0 25 0 1 0 487848348 243970048 55071 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59563 55071 603 41 0 59522 0
vsize: 238252
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73721 0 0 0 25822 178 0 0 25 0 1 0 487848348 243970048 55084 4294967295 134512640 134672761 3221224640 3221223832 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59563 55084 603 41 0 59522 0
vsize: 238252
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73745 0 0 0 26822 178 0 0 25 0 1 0 487848348 244105216 55108 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59596 55108 603 41 0 59555 0
vsize: 238384
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73761 0 0 0 27822 179 0 0 25 0 1 0 487848348 244240384 55124 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59629 55124 603 41 0 59588 0
vsize: 238516
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73773 0 0 0 28822 179 0 0 25 0 1 0 487848348 244240384 55136 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59629 55136 603 41 0 59588 0
vsize: 238516
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73784 0 0 0 29822 179 0 0 25 0 1 0 487848348 244240384 55147 4294967295 134512640 134672761 3221224640 3221223744 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59629 55147 603 41 0 59588 0
vsize: 238516
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73796 0 0 0 30822 179 0 0 25 0 1 0 487848348 244375552 55159 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59662 55159 603 41 0 59621 0
vsize: 238648
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73826 0 0 0 31822 179 0 0 25 0 1 0 487848348 244576256 55189 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59711 55189 603 41 0 59670 0
vsize: 238844
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73868 0 0 0 32823 179 0 0 25 0 1 0 487848348 244711424 55231 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59744 55231 603 41 0 59703 0
vsize: 238976
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73887 0 0 0 33823 179 0 0 25 0 1 0 487848348 244711424 55250 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59744 55250 603 41 0 59703 0
vsize: 238976
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73910 0 0 0 34823 179 0 0 25 0 1 0 487848348 244846592 55273 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59777 55273 603 41 0 59736 0
vsize: 239108
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73933 0 0 0 35823 179 0 0 25 0 1 0 487848348 244981760 55296 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59810 55296 603 41 0 59769 0
vsize: 239240
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 73954 0 0 0 36823 179 0 0 25 0 1 0 487848348 244981760 55317 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59810 55317 603 41 0 59769 0
vsize: 239240
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 74344 0 0 0 37822 180 0 0 25 0 1 0 487848348 246607872 55707 4294967295 134512640 134672761 3221224640 3221223744 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60207 55707 603 41 0 60166 0
vsize: 240828
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 74861 0 0 0 38821 181 0 0 25 0 1 0 487848348 248782848 56224 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60738 56224 603 41 0 60697 0
vsize: 242952
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 74922 0 0 0 39821 182 0 0 25 0 1 0 487848348 248918016 56285 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60771 56285 603 41 0 60730 0
vsize: 243084
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 74945 0 0 0 40821 182 0 0 25 0 1 0 487848348 249053184 56308 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60804 56308 603 41 0 60763 0
vsize: 243216
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 74974 0 0 0 41821 182 0 0 25 0 1 0 487848348 249188352 56337 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60837 56337 603 41 0 60796 0
vsize: 243348
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75011 0 0 0 42821 182 0 0 25 0 1 0 487848348 249319424 56374 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60869 56374 603 41 0 60828 0
vsize: 243476
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75054 0 0 0 43821 182 0 0 25 0 1 0 487848348 249454592 56417 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60902 56417 603 41 0 60861 0
vsize: 243608
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75146 0 0 0 44821 183 0 0 25 0 1 0 487848348 249864192 56509 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61002 56509 603 41 0 60961 0
vsize: 244008
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75177 0 0 0 45821 183 0 0 25 0 1 0 487848348 249999360 56540 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61035 56540 603 41 0 60994 0
vsize: 244140
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75229 0 0 0 46821 183 0 0 25 0 1 0 487848348 250269696 56592 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61101 56592 603 41 0 61060 0
vsize: 244404
[startup+480 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75251 0 0 0 47821 183 0 0 25 0 1 0 487848348 250269696 56614 4294967295 134512640 134672761 3221224640 3221223808 134564711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61101 56614 603 41 0 61060 0
vsize: 244404
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75335 0 0 0 48821 183 0 0 25 0 1 0 487848348 250675200 56698 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61200 56698 603 41 0 61159 0
vsize: 244800
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75351 0 0 0 49821 184 0 0 25 0 1 0 487848348 250675200 56714 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61200 56714 603 41 0 61159 0
vsize: 244800
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75367 0 0 0 50821 184 0 0 25 0 1 0 487848348 250810368 56730 4294967295 134512640 134672761 3221224640 3221223764 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61233 56730 603 41 0 61192 0
vsize: 244932
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75388 0 0 0 51821 184 0 0 25 0 1 0 487848348 250810368 56751 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61233 56751 603 41 0 61192 0
vsize: 244932
[startup+530 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75415 0 0 0 52821 184 0 0 25 0 1 0 487848348 250945536 56778 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61266 56778 603 41 0 61225 0
vsize: 245064
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75451 0 0 0 53821 184 0 0 25 0 1 0 487848348 251080704 56814 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61299 56814 603 41 0 61258 0
vsize: 245196
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75558 0 0 0 54821 184 0 0 25 0 1 0 487848348 251518976 56921 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61406 56921 603 41 0 61365 0
vsize: 245624
[startup+560 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75580 0 0 0 55821 184 0 0 25 0 1 0 487848348 251654144 56943 4294967295 134512640 134672761 3221224640 3221223776 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61439 56943 603 41 0 61398 0
vsize: 245756
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 75773 0 0 0 56820 185 0 0 25 0 1 0 487848348 252465152 57136 4294967295 134512640 134672761 3221224640 3221223744 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61637 57136 603 41 0 61596 0
vsize: 246548
[startup+580 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 76275 0 0 0 57818 186 0 0 25 0 1 0 487848348 254603264 57638 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62159 57638 603 41 0 62118 0
vsize: 248636
[startup+590.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 76722 0 0 0 58817 188 0 0 25 0 1 0 487848348 256425984 58085 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62604 58085 603 41 0 62563 0
vsize: 250416
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 77120 0 0 0 59817 188 0 0 25 0 1 0 487848348 258072576 58483 4294967295 134512640 134672761 3221224640 3221223744 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63006 58483 603 41 0 62965 0
vsize: 252024
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 77622 0 0 0 60816 190 0 0 25 0 1 0 487848348 260132864 58985 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63509 58985 603 41 0 63468 0
vsize: 254036
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 78102 0 0 0 61814 191 0 0 25 0 1 0 487848348 262037504 59465 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63974 59465 603 41 0 63933 0
vsize: 255896
[startup+630.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 78605 0 0 0 62814 192 0 0 25 0 1 0 487848348 264216576 59968 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64506 59968 603 41 0 64465 0
vsize: 258024
[startup+640.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 79119 0 0 0 63812 194 0 0 25 0 1 0 487848348 266244096 60482 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65001 60482 603 41 0 64960 0
vsize: 260004
[startup+650.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 79615 0 0 0 64811 195 0 0 25 0 1 0 487848348 268308480 60978 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65505 60978 603 41 0 65464 0
vsize: 262020
[startup+660.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 80110 0 0 0 65810 196 0 0 25 0 1 0 487848348 270368768 61473 4294967295 134512640 134672761 3221224640 3221223744 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66008 61473 603 41 0 65967 0
vsize: 264032
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 80604 0 0 0 66809 197 0 0 25 0 1 0 487848348 272281600 61967 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66475 61967 603 41 0 66434 0
vsize: 265900
[startup+680.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81053 0 0 0 67809 198 0 0 25 0 1 0 487848348 274194432 62416 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66942 62416 603 41 0 66901 0
vsize: 267768
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81084 0 0 0 68809 198 0 0 25 0 1 0 487848348 274329600 62447 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66975 62447 603 41 0 66934 0
vsize: 267900
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81151 0 0 0 69809 198 0 0 25 0 1 0 487848348 274599936 62514 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67041 62514 603 41 0 67000 0
vsize: 268164
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81437 0 0 0 70808 199 0 0 25 0 1 0 487848348 275689472 62800 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67307 62800 603 41 0 67266 0
vsize: 269228
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81509 0 0 0 71808 199 0 0 25 0 1 0 487848348 275959808 62872 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67373 62872 603 41 0 67332 0
vsize: 269492
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81535 0 0 0 72808 199 0 0 25 0 1 0 487848348 276094976 62898 4294967295 134512640 134672761 3221224640 3221223792 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67406 62898 603 41 0 67365 0
vsize: 269624
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81567 0 0 0 73808 199 0 0 25 0 1 0 487848348 276230144 62930 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67439 62930 603 41 0 67398 0
vsize: 269756
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81658 0 0 0 74808 199 0 0 25 0 1 0 487848348 276635648 63021 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67538 63021 603 41 0 67497 0
vsize: 270152
[startup+760.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81702 0 0 0 75808 200 0 0 25 0 1 0 487848348 276770816 63065 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67571 63065 603 41 0 67530 0
vsize: 270284
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81766 0 0 0 76809 200 0 0 25 0 1 0 487848348 277037056 63129 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67636 63129 603 41 0 67595 0
vsize: 270544
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81788 0 0 0 77809 200 0 0 25 0 1 0 487848348 277172224 63151 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67669 63151 603 41 0 67628 0
vsize: 270676
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81830 0 0 0 78809 200 0 0 25 0 1 0 487848348 277307392 63193 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67702 63193 603 41 0 67661 0
vsize: 270808
[startup+800.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81858 0 0 0 79809 200 0 0 25 0 1 0 487848348 277442560 63221 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67735 63221 603 41 0 67694 0
vsize: 270940
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81894 0 0 0 80809 200 0 0 25 0 1 0 487848348 277577728 63257 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67768 63257 603 41 0 67727 0
vsize: 271072
[startup+820.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81922 0 0 0 81809 200 0 0 25 0 1 0 487848348 277712896 63285 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67801 63285 603 41 0 67760 0
vsize: 271204
[startup+830.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 81938 0 0 0 82809 201 0 0 25 0 1 0 487848348 277712896 63301 4294967295 134512640 134672761 3221224640 3221223828 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67801 63301 603 41 0 67760 0
vsize: 271204
[startup+840.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 82060 0 0 0 83809 201 0 0 25 0 1 0 487848348 278253568 63423 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67933 63423 603 41 0 67892 0
vsize: 271732
[startup+850.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 82272 0 0 0 84808 202 0 0 25 0 1 0 487848348 279068672 63635 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68132 63635 603 41 0 68091 0
vsize: 272528
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 82750 0 0 0 85807 203 0 0 25 0 1 0 487848348 281001984 64113 4294967295 134512640 134672761 3221224640 3221223744 134559859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68604 64113 603 41 0 68563 0
vsize: 274416
[startup+870.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 83211 0 0 0 86805 205 0 0 25 0 1 0 487848348 282918912 64574 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69072 64574 603 41 0 69031 0
vsize: 276288
[startup+880.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 83705 0 0 0 87804 206 0 0 25 0 1 0 487848348 284991488 65068 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69578 65068 603 41 0 69537 0
vsize: 278312
[startup+890.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 84191 0 0 0 88804 207 0 0 25 0 1 0 487848348 286949376 65554 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70056 65554 603 41 0 70015 0
vsize: 280224
[startup+900.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 84649 0 0 0 89803 208 0 0 25 0 1 0 487848348 288845824 66012 4294967295 134512640 134672761 3221224640 3221223744 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70519 66012 603 41 0 70478 0
vsize: 282076
[startup+910.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 85113 0 0 0 90801 210 0 0 25 0 1 0 487848348 290750464 66476 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70984 66476 603 41 0 70943 0
vsize: 283936
[startup+920.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 85594 0 0 0 91801 210 0 0 25 0 1 0 487848348 292691968 66957 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71458 66957 603 41 0 71417 0
vsize: 285832
[startup+930.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 86096 0 0 0 92800 211 0 0 25 0 1 0 487848348 294707200 67459 4294967295 134512640 134672761 3221224640 3221223744 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71950 67459 603 41 0 71909 0
vsize: 287800
[startup+940.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 86601 0 0 0 93800 212 0 0 25 0 1 0 487848348 296853504 67964 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72474 67964 603 41 0 72433 0
vsize: 289896
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 87109 0 0 0 94799 213 0 0 25 0 1 0 487848348 298913792 68472 4294967295 134512640 134672761 3221224640 3221223744 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72977 68472 603 41 0 72936 0
vsize: 291908
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 87610 0 0 0 95798 214 0 0 25 0 1 0 487848348 301002752 68973 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73487 68973 603 41 0 73446 0
vsize: 293948
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 88100 0 0 0 96797 215 0 0 25 0 1 0 487848348 303022080 69463 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73980 69463 603 41 0 73939 0
vsize: 295920
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 88585 0 0 0 97796 216 0 0 25 0 1 0 487848348 304918528 69948 4294967295 134512640 134672761 3221224640 3221223744 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74443 69948 603 41 0 74402 0
vsize: 297772
[startup+990.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89036 0 0 0 98796 217 0 0 25 0 1 0 487848348 306835456 70399 4294967295 134512640 134672761 3221224640 3221223744 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74911 70399 603 41 0 74870 0
vsize: 299644
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89236 0 0 0 99795 217 0 0 25 0 1 0 487848348 307654656 70599 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75111 70599 603 41 0 75070 0
vsize: 300444
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89256 0 0 0 100795 217 0 0 25 0 1 0 487848348 307654656 70619 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75111 70619 603 41 0 75070 0
vsize: 300444
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89285 0 0 0 101796 217 0 0 25 0 1 0 487848348 308043776 70648 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75206 70648 603 41 0 75165 0
vsize: 300824
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89312 0 0 0 102796 217 0 0 25 0 1 0 487848348 308178944 70675 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75239 70675 603 41 0 75198 0
vsize: 300956
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89333 0 0 0 103796 217 0 0 25 0 1 0 487848348 308314112 70696 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75272 70696 603 41 0 75231 0
vsize: 301088
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89393 0 0 0 104796 218 0 0 25 0 1 0 487848348 308432896 70756 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75301 70756 603 41 0 75260 0
vsize: 301204
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89413 0 0 0 105796 218 0 0 25 0 1 0 487848348 308568064 70776 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75334 70776 603 41 0 75293 0
vsize: 301336
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89453 0 0 0 106796 218 0 0 25 0 1 0 487848348 308703232 70816 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75367 70816 603 41 0 75326 0
vsize: 301468
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89478 0 0 0 107795 219 0 0 25 0 1 0 487848348 308838400 70841 4294967295 134512640 134672761 3221224640 3221223764 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75400 70841 603 41 0 75359 0
vsize: 301600
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89514 0 0 0 108796 219 0 0 25 0 1 0 487848348 308973568 70877 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75433 70877 603 41 0 75392 0
vsize: 301732
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89629 0 0 0 109795 219 0 0 25 0 1 0 487848348 309510144 70992 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75564 70992 603 41 0 75523 0
vsize: 302256
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89766 0 0 0 110795 220 0 0 25 0 1 0 487848348 310075392 71129 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75702 71129 603 41 0 75661 0
vsize: 302808
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89812 0 0 0 111795 220 0 0 25 0 1 0 487848348 310210560 71175 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75735 71175 603 41 0 75694 0
vsize: 302940
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89844 0 0 0 112795 220 0 0 25 0 1 0 487848348 310345728 71207 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75768 71207 603 41 0 75727 0
vsize: 303072
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89901 0 0 0 113795 220 0 0 25 0 1 0 487848348 310616064 71264 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75834 71264 603 41 0 75793 0
vsize: 303336
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 89991 0 0 0 114795 220 0 0 25 0 1 0 487848348 310890496 71354 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75901 71354 603 41 0 75860 0
vsize: 303604
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 90384 0 0 0 115794 221 0 0 25 0 1 0 487848348 312532992 71747 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76302 71747 603 41 0 76261 0
vsize: 305208
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 90847 0 0 0 116794 222 0 0 25 0 1 0 487848348 314458112 72210 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76772 72210 603 41 0 76731 0
vsize: 307088
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 91292 0 0 0 117793 223 0 0 25 0 1 0 487848348 316219392 72655 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77202 72655 603 41 0 77161 0
vsize: 308808
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 91535 0 0 0 118793 224 0 0 25 0 1 0 487848348 317173760 72898 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77435 72898 603 41 0 77394 0
vsize: 309740
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5337
Raw data (stat): 5337 (minisat+) R 5336 22612 22611 0 -1 0 91747 0 0 0 119792 224 0 0 25 0 1 0 487848348 318136320 73110 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77670 73110 603 41 0 77629 0
vsize: 310680
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 5337
Raw data (stat): 5337 (minisat+) Z 5336 22612 22611 0 -1 12 91750 0 0 0 119794 238 0 0 25 0 1 0 487848348 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.17
CPU time (s): 1200.33
CPU user time (s): 1197.94
CPU system time (s): 2.38564
CPU usage (%): 100.013
Max. virtual memory (Kb): 310680
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####