PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-air06.opb
MD5SUM	f85d0079133f298b06c25764b03ff228
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50233
Optimality of the best value was proved	NO
Number of terms in the objective function	8627
Biggest coefficient in the objective function	1859
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	4587852
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	1859
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	4587852
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.81
Number of variables	8627
Total number of constraints	9452
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9452
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	461
Trace number 19292

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890104 kB
Buffers:         24132 kB
Cached:          94100 kB
SwapCached:       4304 kB
Active:          39212 kB
Inactive:        84736 kB
HighTotal:      131008 kB
HighFree:        39536 kB
LowTotal:       903652 kB
LowFree:        850568 kB
SwapTotal:     2097892 kB
SwapFree:      2092680 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14920 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:05:24 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 16671 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1628 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1626]---> BDD-cost:  103
c ---[1622]---> BDD-cost:   43
c ---[1618]---> BDD-cost:   59
c ---[1616]---> BDD-cost:   33
c ---[1614]---> BDD-cost:  109
c ---[1612]---> BDD-cost:  113
c ---[1610]---> BDD-cost:   79
c ---[1608]---> BDD-cost:    3
c ---[1604]---> BDD-cost:   41
c ---[1602]---> BDD-cost:   51
c ---[1600]---> BDD-cost:  147
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:   23
c ---[1594]---> BDD-cost:  135
c ---[1592]---> BDD-cost:   81
c ---[1590]---> BDD-cost:   41
c ---[1588]---> BDD-cost:   27
c ---[1586]---> BDD-cost:   25
c ---[1584]---> BDD-cost:    8
c ---[1582]---> BDD-cost:   71
c ---[1580]---> BDD-cost:  137
c ---[1578]---> BDD-cost:   25
c ---[1576]---> BDD-cost:   13
c ---[1574]---> BDD-cost:   27
c ---[1572]---> BDD-cost:    9
c ---[1570]---> BDD-cost:  131
c ---[1566]---> BDD-cost:   47
c ---[1564]---> BDD-cost:   41
c ---[1562]---> BDD-cost:   27
c ---[1560]---> BDD-cost:   35
c ---[1558]---> BDD-cost:  133
c ---[1556]---> BDD-cost:  303
c ---[1554]---> BDD-cost:  231
c ---[1552]---> BDD-cost:  175
c ---[1550]---> BDD-cost:  131
c ---[1548]---> BDD-cost:   89
c ---[1546]---> BDD-cost:   53
c ---[1544]---> BDD-cost:   65
c ---[1542]---> BDD-cost:  141
c ---[1540]---> BDD-cost:  129
c ---[1538]---> BDD-cost:   21
c ---[1536]---> BDD-cost:   13
c ---[1534]---> BDD-cost:   83
c ---[1532]---> BDD-cost:   63
c ---[1530]---> BDD-cost:    7
c ---[1528]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   41
c ---[1522]---> BDD-cost:   93
c ---[1520]---> BDD-cost:   55
c ---[1518]---> BDD-cost:   27
c ---[1516]---> BDD-cost:  253
c ---[1514]---> BDD-cost:  189
c ---[1512]---> BDD-cost:  131
c ---[1510]---> BDD-cost:  143
c ---[1508]---> BDD-cost:   55
c ---[1506]---> BDD-cost:  105
c ---[1504]---> BDD-cost:  357
c ---[1502]---> BDD-cost:  355
c ---[1500]---> BDD-cost:  361
c ---[1498]---> BDD-cost:  257
c ---[1496]---> BDD-cost:  263
c ---[1494]---> BDD-cost:  271
c ---[1492]---> BDD-cost:   91
c ---[1488]---> BDD-cost:   15
c ---[1486]---> BDD-cost:    7
c ---[1484]---> BDD-cost:   37
c ---[1478]---> BDD-cost:    1
c ---[1476]---> BDD-cost:   14
c ---[1474]---> BDD-cost:    7
c ---[1472]---> BDD-cost:    1
c ---[1470]---> BDD-cost:    1
c ---[1468]---> BDD-cost:    5
c ---[1466]---> BDD-cost:  103
c ---[1464]---> BDD-cost:  203
c ---[1462]---> BDD-cost:   91
c ---[1460]---> BDD-cost:   49
c ---[1458]---> BDD-cost:    7
c ---[1456]---> BDD-cost:   77
c ---[1452]---> BDD-cost:   55
c ---[1450]---> BDD-cost:   19
c ---[1448]---> BDD-cost:   95
c ---[1446]---> BDD-cost:  101
c ---[1444]---> BDD-cost:  115
c ---[1442]---> BDD-cost:   67
c ---[1440]---> BDD-cost:   33
c ---[1438]---> BDD-cost:   29
c ---[1436]---> BDD-cost:   91
c ---[1434]---> BDD-cost:   25
c ---[1428]---> BDD-cost:   11
c ---[1426]---> BDD-cost:   15
c ---[1424]---> BDD-cost:   29
c ---[1422]---> BDD-cost:  127
c ---[1420]---> BDD-cost:  195
c ---[1418]---> BDD-cost:  143
c ---[1416]---> BDD-cost:  111
c ---[1414]---> BDD-cost:  169
c ---[1412]---> BDD-cost:  169
c ---[1410]---> BDD-cost:  171
c ---[1408]---> BDD-cost:  135
c ---[1406]---> BDD-cost:   43
c ---[1404]---> BDD-cost:  257
c ---[1402]---> BDD-cost:  261
c ---[1400]---> BDD-cost:  167
c ---[1398]---> BDD-cost:  125
c ---[1396]---> BDD-cost:  125
c ---[1394]---> BDD-cost:   39
c ---[1392]---> BDD-cost:   37
c ---[1390]---> BDD-cost:   43
c ---[1386]---> BDD-cost:   29
c ---[1384]---> BDD-cost:   33
c ---[1382]---> BDD-cost:  107
c ---[1380]---> BDD-cost:   57
c ---[1378]---> BDD-cost:  169
c ---[1376]---> BDD-cost:   79
c ---[1374]---> BDD-cost:   81
c ---[1372]---> BDD-cost:  219
c ---[1370]---> BDD-cost:  229
c ---[1368]---> BDD-cost:  111
c ---[1366]---> BDD-cost:    5
c ---[1364]---> BDD-cost:   89
c ---[1362]---> BDD-cost:  389
c ---[1360]---> BDD-cost:  335
c ---[1358]---> BDD-cost:  191
c ---[1356]---> BDD-cost:  121
c ---[1354]---> BDD-cost:  137
c ---[1352]---> BDD-cost:   83
c ---[1350]---> BDD-cost:  199
c ---[1348]---> BDD-cost:   15
c ---[1346]---> BDD-cost:  109
c ---[1344]---> BDD-cost:   55
c ---[1342]---> BDD-cost:  181
c ---[1340]---> BDD-cost:  133
c ---[1338]---> BDD-cost:   81
c ---[1336]---> BDD-cost:   33
c ---[1334]---> BDD-cost:  131
c ---[1332]---> BDD-cost:   75
c ---[1330]---> BDD-cost:   49
c ---[1328]---> BDD-cost:   17
c ---[1326]---> BDD-cost:   97
c ---[1324]---> BDD-cost:  129
c ---[1322]---> BDD-cost:   69
c ---[1320]---> BDD-cost:  273
c ---[1318]---> BDD-cost:  261
c ---[1316]---> BDD-cost:   89
c ---[1314]---> BDD-cost:  119
c ---[1312]---> BDD-cost:   53
c ---[1310]---> BDD-cost:   43
c ---[1308]---> BDD-cost:   61
c ---[1306]---> BDD-cost:   99
c ---[1304]---> BDD-cost:   81
c ---[1302]---> BDD-cost:  165
c ---[1300]---> BDD-cost:  231
c ---[1298]---> BDD-cost:  121
c ---[1296]---> BDD-cost:  135
c ---[1294]---> BDD-cost:  227
c ---[1292]---> BDD-cost:   35
c ---[1290]---> BDD-cost:   55
c ---[1288]---> BDD-cost:  143
c ---[1286]---> BDD-cost:  135
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  177
c ---[1280]---> BDD-cost:  151
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  179
c ---[1274]---> BDD-cost:   61
c ---[1272]---> BDD-cost:  167
c ---[1270]---> BDD-cost:  145
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:  243
c ---[1264]---> BDD-cost:   15
c ---[1262]---> BDD-cost:  137
c ---[1260]---> BDD-cost:   85
c ---[1258]---> BDD-cost:   37
c ---[1254]---> BDD-cost:   43
c ---[1252]---> BDD-cost:   19
c ---[1250]---> BDD-cost:   23
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   91
c ---[1244]---> BDD-cost:   95
c ---[1242]---> BDD-cost:   61
c ---[1240]---> BDD-cost:   79
c ---[1238]---> BDD-cost:   89
c ---[1236]---> BDD-cost:  105
c ---[1234]---> BDD-cost:   97
c ---[1232]---> BDD-cost:  105
c ---[1230]---> BDD-cost:   81
c ---[1228]---> BDD-cost:   19
c ---[1226]---> BDD-cost:   13
c ---[1224]---> BDD-cost:    3
c ---[1222]---> BDD-cost:   21
c ---[1220]---> BDD-cost:   65
c ---[1218]---> BDD-cost:   35
c ---[1216]---> BDD-cost:   69
c ---[1214]---> BDD-cost:   45
c ---[1212]---> BDD-cost:   59
c ---[1210]---> BDD-cost:   89
c ---[1208]---> BDD-cost:   65
c ---[1206]---> BDD-cost:  101
c ---[1204]---> BDD-cost:   87
c ---[1202]---> BDD-cost:   95
c ---[1200]---> BDD-cost:   69
c ---[1198]---> BDD-cost:  119
c ---[1196]---> BDD-cost:   53
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   27
c ---[1190]---> BDD-cost:  273
c ---[1188]---> BDD-cost:  231
c ---[1186]---> BDD-cost:  243
c ---[1184]---> BDD-cost:  121
c ---[1182]---> BDD-cost:  295
c ---[1180]---> BDD-cost:  175
c ---[1178]---> BDD-cost:  115
c ---[1176]---> BDD-cost:  175
c ---[1174]---> BDD-cost:  249
c ---[1172]---> BDD-cost:  233
c ---[1170]---> BDD-cost:  123
c ---[1168]---> BDD-cost:   81
c ---[1166]---> BDD-cost:    5
c ---[1164]---> BDD-cost:   75
c ---[1162]---> BDD-cost:   71
c ---[1160]---> BDD-cost:   39
c ---[1156]---> BDD-cost:   65
c ---[1154]---> BDD-cost:   51
c ---[1152]---> BDD-cost:   21
c ---[1150]---> BDD-cost:   15
c ---[1148]---> BDD-cost:    3
c ---[1146]---> BDD-cost:   21
c ---[1144]---> BDD-cost:   17
c ---[1142]---> BDD-cost:   33
c ---[1140]---> BDD-cost:   11
c ---[1138]---> BDD-cost:   29
c ---[1136]---> BDD-cost:   95
c ---[1134]---> BDD-cost:   79
c ---[1132]---> BDD-cost:   37
c ---[1130]---> BDD-cost:  273
c ---[1128]---> BDD-cost:  221
c ---[1126]---> BDD-cost:  189
c ---[1124]---> BDD-cost:   81
c ---[1122]---> BDD-cost:   35
c ---[1120]---> BDD-cost:  185
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   59
c ---[1114]---> BDD-cost:   59
c ---[1112]---> BDD-cost:  125
c ---[1110]---> BDD-cost:  135
c ---[1108]---> BDD-cost:  117
c ---[1096]---> BDD-cost:   73
c ---[1094]---> BDD-cost:   95
c ---[1092]---> BDD-cost:   53
c ---[1090]---> BDD-cost:  117
c ---[1088]---> BDD-cost:  117
c ---[1086]---> BDD-cost:  199
c ---[1084]---> BDD-cost:  189
c ---[1082]---> BDD-cost:   25
c ---[1080]---> BDD-cost:  173
c ---[1078]---> BDD-cost:   45
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:  219
c ---[1070]---> BDD-cost:  167
c ---[1068]---> BDD-cost:  121
c ---[1066]---> BDD-cost:  203
c ---[1064]---> BDD-cost:   27
c ---[1062]---> BDD-cost:   17
c ---[1060]---> BDD-cost:   87
c ---[1058]---> BDD-cost:  111
c ---[1056]---> BDD-cost:  169
c ---[1054]---> BDD-cost:  251
c ---[1052]---> BDD-cost:  155
c ---[1048]---> BDD-cost:   93
c ---[1044]---> BDD-cost:  141
c ---[1042]---> BDD-cost:  103
c ---[1040]---> BDD-cost:  173
c ---[1038]---> BDD-cost:  221
c ---[1036]---> BDD-cost:  199
c ---[1034]---> BDD-cost:  185
c ---[1032]---> BDD-cost:  259
c ---[1030]---> BDD-cost:  129
c ---[1028]---> BDD-cost:  283
c ---[1026]---> BDD-cost:  187
c ---[1024]---> BDD-cost:  187
c ---[1022]---> BDD-cost:  173
c ---[1018]---> BDD-cost:   55
c ---[1014]---> BDD-cost:   37
c ---[1012]---> BDD-cost:   59
c ---[1010]---> BDD-cost:   57
c ---[1008]---> BDD-cost:   49
c ---[1004]---> BDD-cost:    1
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   91
c ---[ 998]---> BDD-cost:  137
c ---[ 996]---> BDD-cost:   77
c ---[ 994]---> BDD-cost:  125
c ---[ 992]---> BDD-cost:   49
c ---[ 990]---> BDD-cost:  103
c ---[ 988]---> BDD-cost:  119
c ---[ 986]---> BDD-cost:   81
c ---[ 984]---> BDD-cost:  121
c ---[ 982]---> BDD-cost:  127
c ---[ 980]---> BDD-cost:   25
c ---[ 978]---> BDD-cost:  139
c ---[ 976]---> BDD-cost:   73
c ---[ 974]---> BDD-cost:  113
c ---[ 972]---> BDD-cost:   77
c ---[ 970]---> BDD-cost:   69
c ---[ 968]---> BDD-cost:   53
c ---[ 966]---> BDD-cost:   33
c ---[ 962]---> BDD-cost:   65
c ---[ 960]---> BDD-cost:   65
c ---[ 958]---> BDD-cost:  213
c ---[ 956]---> BDD-cost:  247
c ---[ 954]---> BDD-cost:  273
c ---[ 952]---> BDD-cost:  145
c ---[ 950]---> BDD-cost:  535
c ---[ 948]---> BDD-cost:  659
c ---[ 946]---> BDD-cost:  259
c ---[ 944]---> BDD-cost:  213
c ---[ 942]---> BDD-cost:  157
c ---[ 940]---> BDD-cost:   65
c ---[ 938]---> BDD-cost:  561
c ---[ 936]---> BDD-cost:  117
c ---[ 932]---> BDD-cost:  153
c ---[ 930]---> BDD-cost:  113
c ---[ 928]---> BDD-cost:  119
c ---[ 926]---> BDD-cost:   99
c ---[ 922]---> BDD-cost:    6
c ---[ 920]---> BDD-cost:  113
c ---[ 918]---> BDD-cost:   75
c ---[ 914]---> BDD-cost:   17
c ---[ 912]---> BDD-cost:  149
c ---[ 910]---> BDD-cost:   63
c ---[ 908]---> BDD-cost:   41
c ---[ 906]---> BDD-cost:  135
c ---[ 904]---> BDD-cost:   99
c ---[ 902]---> BDD-cost:   99
c ---[ 900]---> BDD-cost:   65
c ---[ 898]---> BDD-cost:  333
c ---[ 896]---> BDD-cost:   93
c ---[ 894]---> BDD-cost:  407
c ---[ 892]---> BDD-cost:  393
c ---[ 890]---> BDD-cost:  349
c ---[ 888]---> BDD-cost:  189
c ---[ 886]---> BDD-cost:  225
c ---[ 884]---> BDD-cost:  115
c ---[ 882]---> BDD-cost:  117
c ---[ 880]---> BDD-cost:   57
c ---[ 878]---> BDD-cost:  109
c ---[ 876]---> BDD-cost:  219
c ---[ 874]---> BDD-cost:  139
c ---[ 872]---> BDD-cost:  239
c ---[ 870]---> BDD-cost:   65
c ---[ 868]---> BDD-cost:   39
c ---[ 866]---> BDD-cost:   59
c ---[ 862]---> BDD-cost:    9
c ---[ 860]---> BDD-cost:  239
c ---[ 858]---> BDD-cost:  165
c ---[ 856]---> BDD-cost:  207
c ---[ 854]---> BDD-cost:  219
c ---[ 852]---> BDD-cost:  391
c ---[ 850]---> BDD-cost:  315
c ---[ 848]---> BDD-cost:  147
c ---[ 846]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:  187
c ---[ 842]---> BDD-cost:  311
c ---[ 840]---> BDD-cost:  187
c ---[ 838]---> BDD-cost:  195
c ---[ 836]---> BDD-cost:  117
c ---[ 834]---> BDD-cost:  111
c ---[ 830]---> BDD-cost:   91
c ---[ 828]---> BDD-cost:  333
c ---[ 826]---> BDD-cost:  207
c ---[ 822]---> BDD-cost:  253
c ---[ 820]---> BDD-cost:   77
c ---[ 818]---> BDD-cost:   77
c ---[ 816]---> BDD-cost:  191
c ---[ 814]---> BDD-cost:  153
c ---[ 812]---> BDD-cost:  255
c ---[ 810]---> BDD-cost:  189
c ---[ 808]---> BDD-cost:   17
c ---[ 806]---> BDD-cost:   39
c ---[ 802]---> BDD-cost:  187
c ---[ 800]---> BDD-cost:  117
c ---[ 798]---> BDD-cost:   49
c ---[ 796]---> BDD-cost:   37
c ---[ 794]---> BDD-cost:   61
c ---[ 792]---> BDD-cost:   33
c ---[ 790]---> BDD-cost:    0
c ---[ 788]---> BDD-cost:   83
c ---[ 786]---> BDD-cost:   73
c ---[ 784]---> BDD-cost:   91
c ---[ 782]---> BDD-cost:   55
c ---[ 780]---> BDD-cost:  105
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  345
c ---[ 774]---> BDD-cost:  295
c ---[ 772]---> BDD-cost:  101
c ---[ 770]---> BDD-cost:   21
c ---[ 768]---> BDD-cost:   71
c ---[ 766]---> BDD-cost:   77
c ---[ 764]---> BDD-cost:   61
c ---[ 762]---> BDD-cost:   53
c ---[ 760]---> BDD-cost:  199
c ---[ 758]---> BDD-cost:  195
c ---[ 756]---> BDD-cost:  155
c ---[ 754]---> BDD-cost:   29
c ---[ 752]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:  133
c ---[ 748]---> BDD-cost:   65
c ---[ 746]---> BDD-cost:   57
c ---[ 744]---> BDD-cost:  157
c ---[ 742]---> BDD-cost:  345
c ---[ 740]---> BDD-cost:  201
c ---[ 738]---> BDD-cost:  205
c ---[ 736]---> BDD-cost:  151
c ---[ 734]---> BDD-cost:  135
c ---[ 732]---> BDD-cost:   73
c ---[ 730]---> BDD-cost:  161
c ---[ 728]---> BDD-cost:  181
c ---[ 726]---> BDD-cost:  177
c ---[ 724]---> BDD-cost:  293
c ---[ 722]---> BDD-cost:  279
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  145
c ---[ 716]---> BDD-cost:  289
c ---[ 714]---> BDD-cost:  163
c ---[ 712]---> BDD-cost:  181
c ---[ 710]---> BDD-cost:  141
c ---[ 708]---> BDD-cost:  115
c ---[ 706]---> BDD-cost:  123
c ---[ 704]---> BDD-cost:  189
c ---[ 702]---> BDD-cost:  139
c ---[ 700]---> BDD-cost:   63
c ---[ 698]---> BDD-cost:  473
c ---[ 696]---> BDD-cost:  429
c ---[ 694]---> BDD-cost:  285
c ---[ 692]---> BDD-cost:    9
c ---[ 690]---> BDD-cost:    5
c ---[ 688]---> BDD-cost:    0
c ---[ 686]---> BDD-cost:    3
c ---[ 684]---> BDD-cost:    4
c ---[ 680]---> BDD-cost:  155
c ---[ 678]---> BDD-cost:  127
c ---[ 676]---> BDD-cost:  109
c ---[ 674]---> BDD-cost:  273
c ---[ 672]---> BDD-cost:   63
c ---[ 670]---> BDD-cost:   45
c ---[ 668]---> BDD-cost:   23
c ---[ 666]---> BDD-cost:   29
c ---[ 664]---> BDD-cost:  245
c ---[ 662]---> BDD-cost:  227
c ---[ 660]---> BDD-cost:   49
c ---[ 658]---> BDD-cost:    9
c ---[ 656]---> BDD-cost:    0
c ---[ 654]---> BDD-cost:  149
c ---[ 652]---> BDD-cost:  183
c ---[ 650]---> BDD-cost:  119
c ---[ 648]---> BDD-cost:  107
c ---[ 646]---> BDD-cost:  235
c ---[ 644]---> BDD-cost:  227
c ---[ 642]---> BDD-cost:  239
c ---[ 640]---> BDD-cost:  269
c ---[ 638]---> BDD-cost:  615
c ---[ 636]---> BDD-cost:  441
c ---[ 634]---> BDD-cost:  231
c ---[ 632]---> BDD-cost:  123
c ---[ 630]---> BDD-cost:  547
c ---[ 628]---> BDD-cost:  543
c ---[ 626]---> BDD-cost:  357
c ---[ 624]---> BDD-cost:  237
c ---[ 620]---> BDD-cost:  327
c ---[ 618]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:  287
c ---[ 614]---> BDD-cost:  205
c ---[ 612]---> BDD-cost:  177
c ---[ 610]---> BDD-cost:  313
c ---[ 608]---> BDD-cost:   57
c ---[ 606]---> BDD-cost:   61
c ---[ 604]---> BDD-cost:   45
c ---[ 602]---> BDD-cost:   35
c ---[ 600]---> BDD-cost:  133
c ---[ 598]---> BDD-cost:  107
c ---[ 596]---> BDD-cost:   91
c ---[ 594]---> BDD-cost:   93
c ---[ 592]---> BDD-cost:   35
c ---[ 590]---> BDD-cost:  187
c ---[ 588]---> BDD-cost:  573
c ---[ 586]---> BDD-cost:  305
c ---[ 584]---> BDD-cost:  607
c ---[ 582]---> BDD-cost:  443
c ---[ 580]---> BDD-cost:  213
c ---[ 578]---> BDD-cost:  213
c ---[ 576]---> BDD-cost:  167
c ---[ 574]---> BDD-cost:    4
c ---[ 572]---> BDD-cost:  283
c ---[ 570]---> BDD-cost:  277
c ---[ 568]---> BDD-cost:  125
c ---[ 566]---> BDD-cost:   85
c ---[ 564]---> BDD-cost:   81
c ---[ 562]---> BDD-cost:  403
c ---[ 560]---> BDD-cost:  391
c ---[ 558]---> BDD-cost:  175
c ---[ 556]---> BDD-cost:  159
c ---[ 554]---> BDD-cost:  155
c ---[ 552]---> BDD-cost:  101
c ---[ 550]---> BDD-cost:  155
c ---[ 548]---> BDD-cost:  165
c ---[ 546]---> BDD-cost:  153
c ---[ 544]---> BDD-cost:  135
c ---[ 542]---> BDD-cost:   81
c ---[ 540]---> BDD-cost:  167
c ---[ 538]---> BDD-cost:   27
c ---[ 536]---> BDD-cost:  147
c ---[ 534]---> BDD-cost:  155
c ---[ 532]---> BDD-cost:  173
c ---[ 530]---> BDD-cost:  267
c ---[ 528]---> BDD-cost:  157
c ---[ 526]---> BDD-cost:   91
c ---[ 524]---> BDD-cost:  259
c ---[ 522]---> BDD-cost:  117
c ---[ 520]---> BDD-cost:  121
c ---[ 518]---> BDD-cost:  323
c ---[ 516]---> BDD-cost:  325
c ---[ 514]---> BDD-cost:  311
c ---[ 512]---> BDD-cost:  313
c ---[ 510]---> BDD-cost:  247
c ---[ 508]---> BDD-cost:  297
c ---[ 506]---> BDD-cost:  211
c ---[ 504]---> BDD-cost:  369
c ---[ 500]---> BDD-cost:  305
c ---[ 498]---> BDD-cost:  341
c ---[ 496]---> BDD-cost:  285
c ---[ 494]---> BDD-cost:   77
c ---[ 492]---> BDD-cost:  317
c ---[ 490]---> BDD-cost:  275
c ---[ 488]---> BDD-cost:  423
c ---[ 486]---> BDD-cost:  403
c ---[ 484]---> BDD-cost:  307
c ---[ 482]---> BDD-cost:  327
c ---[ 480]---> BDD-cost:  307
c ---[ 478]---> BDD-cost:  315
c ---[ 476]---> BDD-cost:  297
c ---[ 474]---> BDD-cost:  273
c ---[ 472]---> BDD-cost:  701
c ---[ 470]---> BDD-cost:  289
c ---[ 468]---> BDD-cost:  245
c ---[ 466]---> BDD-cost:  385
c ---[ 464]---> BDD-cost:  363
c ---[ 462]---> BDD-cost:   27
c ---[ 458]---> BDD-cost:  145
c ---[ 456]---> BDD-cost:  147
c ---[ 454]---> BDD-cost:  149
c ---[ 452]---> BDD-cost:  125
c ---[ 450]---> BDD-cost:  147
c ---[ 448]---> BDD-cost:  111
c ---[ 446]---> BDD-cost:  319
c ---[ 444]---> BDD-cost:  309
c ---[ 438]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:    7
c ---[ 434]---> BDD-cost:  399
c ---[ 432]---> BDD-cost:  401
c ---[ 430]---> BDD-cost:  371
c ---[ 426]---> BDD-cost:   65
c ---[ 422]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:   15
c ---[ 416]---> BDD-cost:  453
c ---[ 414]---> BDD-cost:  457
c ---[ 412]---> BDD-cost:  197
c ---[ 410]---> BDD-cost:  123
c ---[ 408]---> BDD-cost:  165
c ---[ 404]---> BDD-cost:  335
c ---[ 402]---> BDD-cost:  169
c ---[ 400]---> BDD-cost:  209
c ---[ 398]---> BDD-cost:   61
c ---[ 396]---> BDD-cost:   17
c ---[ 394]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:   41
c ---[ 388]---> BDD-cost:  229
c ---[ 386]---> BDD-cost:  231
c ---[ 384]---> BDD-cost:  223
c ---[ 378]---> BDD-cost:  319
c ---[ 376]---> BDD-cost:  223
c ---[ 374]---> BDD-cost:  241
c ---[ 372]---> BDD-cost:  245
c ---[ 370]---> BDD-cost:  229
c ---[ 368]---> BDD-cost:  109
c ---[ 366]---> BDD-cost:   73
c ---[ 364]---> BDD-cost:   85
c ---[ 362]---> BDD-cost:   99
c ---[ 360]---> BDD-cost:  103
c ---[ 358]---> BDD-cost:    5
c ---[ 356]---> BDD-cost:  201
c ---[ 354]---> BDD-cost:  215
c ---[ 352]---> BDD-cost:  197
c ---[ 348]---> BDD-cost:  139
c ---[ 344]---> BDD-cost:   83
c ---[ 340]---> BDD-cost:  125
c ---[ 338]---> BDD-cost:  225
c ---[ 336]---> BDD-cost:  181
c ---[ 334]---> BDD-cost:  151
c ---[ 332]---> BDD-cost:  243
c ---[ 330]---> BDD-cost:  179
c ---[ 328]---> BDD-cost:  207
c ---[ 326]---> BDD-cost:  145
c ---[ 324]---> BDD-cost:   21
c ---[ 322]---> BDD-cost:  235
c ---[ 320]---> BDD-cost:  209
c ---[ 318]---> BDD-cost:   55
c ---[ 316]---> BDD-cost:  223
c ---[ 314]---> BDD-cost:  193
c ---[ 312]---> BDD-cost:  173
c ---[ 310]---> BDD-cost:   63
c ---[ 308]---> BDD-cost:   87
c ---[ 306]---> BDD-cost:   87
c ---[ 304]---> BDD-cost:   33
c ---[ 302]---> BDD-cost:  135
c ---[ 300]---> BDD-cost:   75
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  233
c ---[ 294]---> BDD-cost:  211
c ---[ 292]---> BDD-cost:  119
c ---[ 290]---> BDD-cost:  269
c ---[ 288]---> BDD-cost:   51
c ---[ 286]---> BDD-cost:  205
c ---[ 284]---> BDD-cost:  233
c ---[ 282]---> BDD-cost:  207
c ---[ 280]---> BDD-cost:  243
c ---[ 278]---> BDD-cost:  453
c ---[ 276]---> BDD-cost:  465
c ---[ 274]---> BDD-cost:  259
c ---[ 272]---> BDD-cost:  227
c ---[ 270]---> BDD-cost:  359
c ---[ 268]---> BDD-cost:  209
c ---[ 266]---> BDD-cost:  319
c ---[ 264]---> BDD-cost:  287
c ---[ 262]---> BDD-cost:  225
c ---[ 260]---> BDD-cost:  227
c ---[ 258]---> BDD-cost:  445
c ---[ 256]---> BDD-cost:  339
c ---[ 254]---> BDD-cost:  343
c ---[ 252]---> BDD-cost:  105
c ---[ 250]---> BDD-cost:   73
c ---[ 248]---> BDD-cost:   89
c ---[ 246]---> BDD-cost:  109
c ---[ 242]---> BDD-cost:  597
c ---[ 240]---> BDD-cost:  303
c ---[ 238]---> BDD-cost:  253
c ---[ 236]---> BDD-cost:  133
c ---[ 234]---> BDD-cost:  119
c ---[ 232]---> BDD-cost:   99
c ---[ 230]---> BDD-cost:  119
c ---[ 228]---> BDD-cost:   67
c ---[ 226]---> BDD-cost:  145
c ---[ 224]---> BDD-cost:  135
c ---[ 222]---> BDD-cost:  217
c ---[ 220]---> BDD-cost:  211
c ---[ 218]---> BDD-cost:  141
c ---[ 214]---> BDD-cost:  167
c ---[ 212]---> BDD-cost:  191
c ---[ 210]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  175
c ---[ 206]---> BDD-cost:  147
c ---[ 204]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:  389
c ---[ 200]---> BDD-cost:  349
c ---[ 198]---> BDD-cost:  151
c ---[ 196]---> BDD-cost:  151
c ---[ 194]---> BDD-cost:  307
c ---[ 192]---> BDD-cost:  355
c ---[ 190]---> BDD-cost:  269
c ---[ 188]---> BDD-cost:  267
c ---[ 186]---> BDD-cost:  327
c ---[ 184]---> BDD-cost:  347
c ---[ 182]---> BDD-cost:  187
c ---[ 180]---> BDD-cost:  117
c ---[ 178]---> BDD-cost:   37
c ---[ 176]---> BDD-cost:   17
c ---[ 174]---> BDD-cost:  171
c ---[ 170]---> BDD-cost:  339
c ---[ 168]---> BDD-cost:  429
c ---[ 166]---> BDD-cost:  443
c ---[ 164]---> BDD-cost:  419
c ---[ 162]---> BDD-cost:  465
c ---[ 160]---> BDD-cost:  379
c ---[ 158]---> BDD-cost:  307
c ---[ 156]---> BDD-cost:  907
c ---[ 154]---> BDD-cost:  439
c ---[ 152]---> BDD-cost:  303
c ---[ 150]---> BDD-cost:  239
c ---[ 148]---> BDD-cost:  219
c ---[ 146]---> BDD-cost:  261
c ---[ 144]---> BDD-cost:  247
c ---[ 142]---> BDD-cost:  265
c ---[ 140]---> BDD-cost:  273
c ---[ 138]---> BDD-cost:  673
c ---[ 136]---> BDD-cost:  433
c ---[ 134]---> BDD-cost:  317
c ---[ 132]---> BDD-cost:  187
c ---[ 130]---> BDD-cost:  199
c ---[ 128]---> BDD-cost:  155
c ---[ 126]---> BDD-cost:  105
c ---[ 124]---> BDD-cost:   31
c ---[ 122]---> BDD-cost:  117
c ---[ 120]---> BDD-cost:  107
c ---[ 118]---> BDD-cost:  141
c ---[ 116]---> BDD-cost:  165
c ---[ 114]---> BDD-cost:  221
c ---[ 110]---> BDD-cost:  163
c ---[ 108]---> BDD-cost:  179
c ---[ 106]---> BDD-cost:  139
c ---[ 104]---> BDD-cost:   83
c ---[ 102]---> BDD-cost:   67
c ---[ 100]---> BDD-cost:   87
c ---[  98]---> BDD-cost:   31
c ---[  96]---> BDD-cost:   23
c ---[  94]---> BDD-cost:   31
c ---[  92]---> BDD-cost:   91
c ---[  90]---> BDD-cost:  431
c ---[  88]---> BDD-cost:  203
c ---[  86]---> BDD-cost:  565
c ---[  84]---> BDD-cost:  611
c ---[  82]---> BDD-cost:  347
c ---[  80]---> BDD-cost:  175
c ---[  78]---> BDD-cost:  525
c ---[  76]---> BDD-cost:  505
c ---[  74]---> BDD-cost:   57
c ---[  72]---> BDD-cost:   45
c ---[  70]---> BDD-cost:   57
c ---[  68]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   55
c ---[  64]---> BDD-cost:   57
c ---[  62]---> BDD-cost:   57
c ---[  60]---> BDD-cost:  159
c ---[  58]---> BDD-cost:   71
c ---[  56]---> BDD-cost:  199
c ---[  54]---> BDD-cost:  191
c ---[  52]---> BDD-cost:  225
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:  509
c ---[  46]---> BDD-cost:  321
c ---[  44]---> BDD-cost:  333
c ---[  42]---> BDD-cost:  407
c ---[  40]---> BDD-cost:  191
c ---[  38]---> BDD-cost:  135
c ---[  36]---> BDD-cost:  379
c ---[  34]---> BDD-cost:  365
c ---[  32]---> BDD-cost:   63
c ---[  30]---> BDD-cost:   31
c ---[  28]---> BDD-cost:   33
c ---[  26]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   31
c ---[  18]---> BDD-cost:   47
c ---[  16]---> BDD-cost:  139
c ---[  14]---> BDD-cost:    9
c ---[  12]---> BDD-cost:  135
c ---[  10]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   53
c ---[   6]---> BDD-cost:  129
c ---[   4]---> BDD-cost:    7
c ---[   2]---> BDD-cost:  119
c ---[   0]---> BDD-cost:   85
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  297923   775365 |   99307       0        0     nan |  0.000 % |
c |       101 |  297806   775070 |  109237     100     2794    27.9 |  0.656 % |
c |       251 |  297804   775064 |  120161     248    14520    58.5 |  0.657 % |
c |       476 |  297507   774267 |  132177     467    22948    49.1 |  0.710 % |
c |       813 |  297152   773365 |  145395     797    35416    44.4 |  0.754 % |
c |      1319 |  296676   772113 |  159934    1277    64842    50.8 |  0.837 % |
c |      2078 |  296505   771647 |  175928    2025   118379    58.5 |  0.874 % |
c |      3217 |  296041   770425 |  193521    3109   207452    66.7 |  0.949 % |
c |      4927 |  295699   769540 |  212873    4779   350269    73.3 |  0.998 % |
c |      7492 |  295396   768750 |  234160    7275   566032    77.8 |  1.037 % |
c |     11337 |  294904   767451 |  257576   10971   954090    87.0 |  1.105 % |
c |     17103 |  294446   766278 |  283334   16577  1527497    92.1 |  1.145 % |
c |     25754 |  293444   763687 |  311667   24858  2532372   101.9 |  1.262 % |
c |     38729 |  292783   762005 |  342834   37493  4503970   120.1 |  1.316 % |
c |     58190 |  291850   759627 |  377118   56625  8594924   151.8 |  1.423 % |
c |     87385 |  291219   758027 |  414829   85473 17541788   205.2 |  1.468 % |
#### 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.86 0.97 0.92 2/54 4192
Raw data (stat): 4192 (runsolver) R 4191 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547339881 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99979 s]
Raw data (loadavg): 0.88 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 10673 0 0 0 970 28 0 0 25 0 1 0 547339881 45465600 10318 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11100 10318 603 41 0 11059 0
vsize: 44400
[startup+20.0006 s]
Raw data (loadavg): 0.90 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 10824 0 0 0 1969 29 0 0 25 0 1 0 547339881 46137344 10469 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11264 10469 603 41 0 11223 0
vsize: 45056
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 10996 0 0 0 2969 30 0 0 25 0 1 0 547339881 46833664 10641 4294967295 134512640 134672761 3221224624 3221223808 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11434 10641 603 41 0 11393 0
vsize: 45736
[startup+40.0016 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 11145 0 0 0 3968 31 0 0 25 0 1 0 547339881 47374336 10790 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11566 10790 603 41 0 11525 0
vsize: 46264
[startup+50.0018 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 11323 0 0 0 4967 31 0 0 25 0 1 0 547339881 48189440 10968 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11765 10968 603 41 0 11724 0
vsize: 47060
[startup+60.0017 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 11511 0 0 0 5966 33 0 0 25 0 1 0 547339881 48861184 11156 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11929 11156 603 41 0 11888 0
vsize: 47716
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 11701 0 0 0 6966 33 0 0 25 0 1 0 547339881 49672192 11346 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12127 11346 603 41 0 12086 0
vsize: 48508
[startup+80.0032 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 11897 0 0 0 7965 34 0 0 25 0 1 0 547339881 50483200 11542 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12325 11542 603 41 0 12284 0
vsize: 49300
[startup+90.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 12064 0 0 0 8964 35 0 0 25 0 1 0 547339881 51159040 11709 4294967295 134512640 134672761 3221224624 3221223808 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12490 11709 603 41 0 12449 0
vsize: 49960
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 12256 0 0 0 9963 36 0 0 25 0 1 0 547339881 51834880 11901 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12655 11901 603 41 0 12614 0
vsize: 50620
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 12387 0 0 0 10963 37 0 0 25 0 1 0 547339881 52527104 12032 4294967295 134512640 134672761 3221224624 3221223840 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12824 12032 603 41 0 12783 0
vsize: 51296
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 12593 0 0 0 11962 37 0 0 25 0 1 0 547339881 53338112 12238 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13022 12238 603 41 0 12981 0
vsize: 52088
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 12733 0 0 0 12962 38 0 0 25 0 1 0 547339881 53878784 12378 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13154 12378 603 41 0 13113 0
vsize: 52616
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 12926 0 0 0 13961 39 0 0 25 0 1 0 547339881 54689792 12571 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13352 12571 603 41 0 13311 0
vsize: 53408
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 13089 0 0 0 14961 39 0 0 25 0 1 0 547339881 55361536 12734 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13516 12734 603 41 0 13475 0
vsize: 54064
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 13305 0 0 0 15960 40 0 0 25 0 1 0 547339881 56172544 12950 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12950 603 41 0 13673 0
vsize: 54856
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 13542 0 0 0 16960 41 0 0 25 0 1 0 547339881 57114624 13187 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13944 13187 603 41 0 13903 0
vsize: 55776
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 13806 0 0 0 17958 42 0 0 25 0 1 0 547339881 58191872 13451 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14207 13451 603 41 0 14166 0
vsize: 56828
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 13975 0 0 0 18958 43 0 0 25 0 1 0 547339881 58998784 13620 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14404 13620 603 41 0 14363 0
vsize: 57616
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 14185 0 0 0 19957 44 0 0 25 0 1 0 547339881 59809792 13830 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14602 13830 603 41 0 14561 0
vsize: 58408
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 14415 0 0 0 20956 44 0 0 25 0 1 0 547339881 60751872 14060 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14832 14060 603 41 0 14791 0
vsize: 59328
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 14625 0 0 0 21956 45 0 0 25 0 1 0 547339881 61558784 14270 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15029 14270 603 41 0 14988 0
vsize: 60116
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 14779 0 0 0 22955 46 0 0 25 0 1 0 547339881 62361600 14424 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14424 603 41 0 15184 0
vsize: 60900
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 14999 0 0 0 23954 47 0 0 25 0 1 0 547339881 63176704 14644 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14644 603 41 0 15383 0
vsize: 61696
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 15302 0 0 0 24953 48 0 0 25 0 1 0 547339881 64516096 14947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15751 14947 603 41 0 15710 0
vsize: 63004
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 15555 0 0 0 25952 49 0 0 25 0 1 0 547339881 65458176 15200 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15981 15200 603 41 0 15940 0
vsize: 63924
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 15736 0 0 0 26952 50 0 0 25 0 1 0 547339881 66273280 15381 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16180 15381 603 41 0 16139 0
vsize: 64720
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 15971 0 0 0 27951 51 0 0 25 0 1 0 547339881 67215360 15616 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16410 15616 603 41 0 16369 0
vsize: 65640
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 16141 0 0 0 28950 51 0 0 25 0 1 0 547339881 67891200 15786 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16575 15786 603 41 0 16534 0
vsize: 66300
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 16396 0 0 0 29949 53 0 0 25 0 1 0 547339881 68964352 16041 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16837 16041 603 41 0 16796 0
vsize: 67348
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 16616 0 0 0 30949 53 0 0 25 0 1 0 547339881 69779456 16261 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17036 16261 603 41 0 16995 0
vsize: 68144
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 16923 0 0 0 31948 54 0 0 25 0 1 0 547339881 71131136 16568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17366 16568 603 41 0 17325 0
vsize: 69464
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 17157 0 0 0 32948 55 0 0 25 0 1 0 547339881 72069120 16802 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17595 16802 603 41 0 17554 0
vsize: 70380
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 17430 0 0 0 33947 55 0 0 25 0 1 0 547339881 73142272 17075 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17857 17075 603 41 0 17816 0
vsize: 71428
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 17668 0 0 0 34946 56 0 0 25 0 1 0 547339881 74096640 17313 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18090 17313 603 41 0 18049 0
vsize: 72360
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 17902 0 0 0 35946 57 0 0 25 0 1 0 547339881 75046912 17547 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18322 17547 603 41 0 18281 0
vsize: 73288
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 18114 0 0 0 36945 58 0 0 25 0 1 0 547339881 75984896 17759 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18551 17759 603 41 0 18510 0
vsize: 74204
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 18339 0 0 0 37944 59 0 0 25 0 1 0 547339881 76787712 17984 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18747 17984 603 41 0 18706 0
vsize: 74988
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 18725 0 0 0 38943 60 0 0 25 0 1 0 547339881 78405632 18370 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18370 603 41 0 19101 0
vsize: 76568
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 18981 0 0 0 39942 61 0 0 25 0 1 0 547339881 79491072 18626 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19407 18626 603 41 0 19366 0
vsize: 77628
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 19219 0 0 0 40941 62 0 0 25 0 1 0 547339881 80433152 18864 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19637 18864 603 41 0 19596 0
vsize: 78548
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 19425 0 0 0 41941 63 0 0 25 0 1 0 547339881 81244160 19070 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19835 19070 603 41 0 19794 0
vsize: 79340
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 19638 0 0 0 42940 64 0 0 25 0 1 0 547339881 82182144 19283 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20064 19283 603 41 0 20023 0
vsize: 80256
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 19887 0 0 0 43940 65 0 0 25 0 1 0 547339881 83128320 19532 4294967295 134512640 134672761 3221224624 3221223808 134557999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20295 19532 603 41 0 20254 0
vsize: 81180
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 20240 0 0 0 44938 66 0 0 25 0 1 0 547339881 84619264 19885 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20659 19885 603 41 0 20618 0
vsize: 82636
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 20534 0 0 0 45937 68 0 0 25 0 1 0 547339881 85831680 20179 4294967295 134512640 134672761 3221224624 3221223760 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20955 20179 603 41 0 20914 0
vsize: 83820
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 20776 0 0 0 46936 69 0 0 25 0 1 0 547339881 86777856 20421 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21186 20421 603 41 0 21145 0
vsize: 84744
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 21008 0 0 0 47935 70 0 0 25 0 1 0 547339881 87719936 20653 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21416 20653 603 41 0 21375 0
vsize: 85664
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 21241 0 0 0 48934 71 0 0 25 0 1 0 547339881 88657920 20886 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21645 20886 603 41 0 21604 0
vsize: 86580
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 21461 0 0 0 49933 72 0 0 25 0 1 0 547339881 89591808 21106 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21873 21106 603 41 0 21832 0
vsize: 87492
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 21733 0 0 0 50932 73 0 0 25 0 1 0 547339881 90669056 21378 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22136 21378 603 41 0 22095 0
vsize: 88544
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 21948 0 0 0 51932 74 0 0 25 0 1 0 547339881 91615232 21593 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22367 21593 603 41 0 22326 0
vsize: 89468
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 22178 0 0 0 52931 75 0 0 25 0 1 0 547339881 92565504 21823 4294967295 134512640 134672761 3221224624 3221223728 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22599 21823 603 41 0 22558 0
vsize: 90396
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 22386 0 0 0 53929 76 0 0 25 0 1 0 547339881 93634560 22031 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22860 22031 603 41 0 22819 0
vsize: 91440
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 22600 0 0 0 54928 77 0 0 25 0 1 0 547339881 94437376 22245 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23056 22245 603 41 0 23015 0
vsize: 92224
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 22886 0 0 0 55927 78 0 0 25 0 1 0 547339881 95653888 22531 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23353 22531 603 41 0 23312 0
vsize: 93412
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 23194 0 0 0 56926 79 0 0 25 0 1 0 547339881 96866304 22839 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23649 22839 603 41 0 23608 0
vsize: 94596
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 23385 0 0 0 57925 80 0 0 25 0 1 0 547339881 97677312 23030 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23847 23030 603 41 0 23806 0
vsize: 95388
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 23647 0 0 0 58924 82 0 0 25 0 1 0 547339881 98762752 23292 4294967295 134512640 134672761 3221224624 3221223824 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24112 23292 603 41 0 24071 0
vsize: 96448
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 23976 0 0 0 59923 83 0 0 25 0 1 0 547339881 100114432 23621 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24442 23621 603 41 0 24401 0
vsize: 97768
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 24251 0 0 0 60922 84 0 0 25 0 1 0 547339881 101310464 23896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24734 23896 603 41 0 24693 0
vsize: 98936
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 24545 0 0 0 61921 85 0 0 25 0 1 0 547339881 102526976 24190 4294967295 134512640 134672761 3221224624 3221223728 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25031 24190 603 41 0 24990 0
vsize: 100124
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 24876 0 0 0 62920 86 0 0 25 0 1 0 547339881 103743488 24521 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25328 24521 603 41 0 25287 0
vsize: 101312
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 25235 0 0 0 63919 88 0 0 25 0 1 0 547339881 105238528 24880 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25693 24880 603 41 0 25652 0
vsize: 102772
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 25605 0 0 0 64918 89 0 0 25 0 1 0 547339881 106721280 25250 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26055 25250 603 41 0 26014 0
vsize: 104220
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 25908 0 0 0 65917 89 0 0 25 0 1 0 547339881 108072960 25553 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26385 25553 603 41 0 26344 0
vsize: 105540
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 26218 0 0 0 66917 90 0 0 25 0 1 0 547339881 109268992 25863 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26677 25863 603 41 0 26636 0
vsize: 106708
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 26539 0 0 0 67916 91 0 0 25 0 1 0 547339881 110600192 26184 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27002 26184 603 41 0 26961 0
vsize: 108008
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 26882 0 0 0 68915 92 0 0 25 0 1 0 547339881 111955968 26527 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27333 26527 603 41 0 27292 0
vsize: 109332
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 27158 0 0 0 69915 92 0 0 25 0 1 0 547339881 113168384 26803 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27629 26803 603 41 0 27588 0
vsize: 110516
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 27489 0 0 0 70914 93 0 0 25 0 1 0 547339881 114515968 27134 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27958 27134 603 41 0 27917 0
vsize: 111832
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 27682 0 0 0 71914 94 0 0 25 0 1 0 547339881 115195904 27327 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28124 27327 603 41 0 28083 0
vsize: 112496
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 27993 0 0 0 72913 95 0 0 25 0 1 0 547339881 116518912 27638 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28447 27638 603 41 0 28406 0
vsize: 113788
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 28344 0 0 0 73912 96 0 0 25 0 1 0 547339881 118026240 27989 4294967295 134512640 134672761 3221224624 3221223728 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28815 27989 603 41 0 28774 0
vsize: 115260
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 28585 0 0 0 74911 97 0 0 25 0 1 0 547339881 118951936 28230 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29041 28230 603 41 0 29000 0
vsize: 116164
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 28894 0 0 0 75911 98 0 0 25 0 1 0 547339881 120172544 28539 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29339 28539 603 41 0 29298 0
vsize: 117356
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 29124 0 0 0 76910 98 0 0 25 0 1 0 547339881 121114624 28769 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29569 28769 603 41 0 29528 0
vsize: 118276
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 29388 0 0 0 77909 99 0 0 25 0 1 0 547339881 122195968 29033 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29833 29033 603 41 0 29792 0
vsize: 119332
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 29709 0 0 0 78909 100 0 0 25 0 1 0 547339881 123531264 29354 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30159 29354 603 41 0 30118 0
vsize: 120636
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 29999 0 0 0 79908 101 0 0 25 0 1 0 547339881 124751872 29644 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30457 29644 603 41 0 30416 0
vsize: 121828
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 30443 0 0 0 80908 101 0 0 25 0 1 0 547339881 126509056 30088 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30886 30088 603 41 0 30845 0
vsize: 123544
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 30711 0 0 0 81907 102 0 0 25 0 1 0 547339881 127602688 30356 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31153 30356 603 41 0 31112 0
vsize: 124612
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 30952 0 0 0 82906 104 0 0 25 0 1 0 547339881 128544768 30597 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31383 30597 603 41 0 31342 0
vsize: 125532
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 31170 0 0 0 83905 104 0 0 25 0 1 0 547339881 129482752 30815 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31612 30815 603 41 0 31571 0
vsize: 126448
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 31493 0 0 0 84905 105 0 0 25 0 1 0 547339881 130842624 31138 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31944 31138 603 41 0 31903 0
vsize: 127776
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 31881 0 0 0 85904 106 0 0 25 0 1 0 547339881 132411392 31526 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32327 31526 603 41 0 32286 0
vsize: 129308
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 32136 0 0 0 86903 107 0 0 25 0 1 0 547339881 133361664 31781 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32559 31781 603 41 0 32518 0
vsize: 130236
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4192
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 32433 0 0 0 87903 108 0 0 25 0 1 0 547339881 134680576 32078 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32881 32078 603 41 0 32840 0
vsize: 131524
[startup+890.022 s]
Raw data (loadavg): 1.14 1.00 0.93 2/54 4245
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 32673 0 0 0 88894 116 0 0 25 0 1 0 547339881 135622656 32318 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33111 32318 603 41 0 33070 0
vsize: 132444
[startup+900.024 s]
Raw data (loadavg): 1.12 1.00 0.93 2/54 4245
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 33030 0 0 0 89893 117 0 0 25 0 1 0 547339881 137117696 32675 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33476 32675 603 41 0 33435 0
vsize: 133904
[startup+910.023 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 4245
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 33229 0 0 0 90893 118 0 0 25 0 1 0 547339881 137928704 32874 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33674 32874 603 41 0 33633 0
vsize: 134696
[startup+920.023 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 4245
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 33445 0 0 0 91892 118 0 0 25 0 1 0 547339881 138727424 33090 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33869 33090 603 41 0 33828 0
vsize: 135476
[startup+930.024 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 4245
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 33709 0 0 0 92892 119 0 0 25 0 1 0 547339881 139812864 33354 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34134 33354 603 41 0 34093 0
vsize: 136536
[startup+940.024 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 4245
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 34100 0 0 0 93891 120 0 0 25 0 1 0 547339881 141414400 33745 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34525 33745 603 41 0 34484 0
vsize: 138100
[startup+950.024 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 4245
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 34385 0 0 0 94891 120 0 0 25 0 1 0 547339881 142618624 34030 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34819 34030 603 41 0 34778 0
vsize: 139276
[startup+960.024 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 34744 0 0 0 95890 121 0 0 25 0 1 0 547339881 144113664 34389 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35184 34389 603 41 0 35143 0
vsize: 140736
[startup+970.025 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 35180 0 0 0 96889 122 0 0 25 0 1 0 547339881 145879040 34825 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35615 34825 603 41 0 35574 0
vsize: 142460
[startup+980.024 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 35469 0 0 0 97888 123 0 0 25 0 1 0 547339881 146972672 35114 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35882 35114 603 41 0 35841 0
vsize: 143528
[startup+990.024 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 35699 0 0 0 98888 123 0 0 25 0 1 0 547339881 148033536 35344 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36141 35344 603 41 0 36100 0
vsize: 144564
[startup+1000.02 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 35949 0 0 0 99888 124 0 0 25 0 1 0 547339881 148979712 35594 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36372 35594 603 41 0 36331 0
vsize: 145488
[startup+1010.02 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 36068 0 0 0 100888 125 0 0 25 0 1 0 547339881 149516288 35713 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36503 35713 603 41 0 36462 0
vsize: 146012
[startup+1020.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 36281 0 0 0 101887 125 0 0 25 0 1 0 547339881 150319104 35926 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36699 35926 603 41 0 36658 0
vsize: 146796
[startup+1030.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 36560 0 0 0 102887 126 0 0 25 0 1 0 547339881 151531520 36205 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36995 36205 603 41 0 36954 0
vsize: 147980
[startup+1040.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 36922 0 0 0 103886 126 0 0 25 0 1 0 547339881 152879104 36567 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37324 36567 603 41 0 37283 0
vsize: 149296
[startup+1050.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 37063 0 0 0 104886 127 0 0 25 0 1 0 547339881 153550848 36708 4294967295 134512640 134672761 3221224624 3221223824 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37488 36708 603 41 0 37447 0
vsize: 149952
[startup+1060.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 37345 0 0 0 105886 128 0 0 25 0 1 0 547339881 154636288 36990 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37753 36990 603 41 0 37712 0
vsize: 151012
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 37601 0 0 0 106885 128 0 0 25 0 1 0 547339881 155709440 37246 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38015 37246 603 41 0 37974 0
vsize: 152060
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 37897 0 0 0 107884 129 0 0 25 0 1 0 547339881 156901376 37542 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38306 37542 603 41 0 38265 0
vsize: 153224
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 38144 0 0 0 108884 130 0 0 25 0 1 0 547339881 157843456 37789 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38536 37789 603 41 0 38495 0
vsize: 154144
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 38377 0 0 0 109883 131 0 0 25 0 1 0 547339881 158916608 38022 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38798 38022 603 41 0 38757 0
vsize: 155192
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 38694 0 0 0 110882 132 0 0 25 0 1 0 547339881 160108544 38339 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39089 38339 603 41 0 39048 0
vsize: 156356
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 39027 0 0 0 111882 132 0 0 25 0 1 0 547339881 161476608 38672 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39423 38672 603 41 0 39382 0
vsize: 157692
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 39387 0 0 0 112881 133 0 0 25 0 1 0 547339881 162959360 39032 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39785 39032 603 41 0 39744 0
vsize: 159140
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 39764 0 0 0 113880 134 0 0 25 0 1 0 547339881 164532224 39409 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40169 39409 603 41 0 40128 0
vsize: 160676
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 40091 0 0 0 114880 134 0 0 25 0 1 0 547339881 165933056 39736 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40511 39736 603 41 0 40470 0
vsize: 162044
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 40306 0 0 0 115879 136 0 0 25 0 1 0 547339881 166875136 39951 4294967295 134512640 134672761 3221224624 3221223760 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40741 39951 603 41 0 40700 0
vsize: 162964
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 40516 0 0 0 116878 137 0 0 25 0 1 0 547339881 167677952 40161 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40937 40161 603 41 0 40896 0
vsize: 163748
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 40822 0 0 0 117878 137 0 0 25 0 1 0 547339881 168882176 40467 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41231 40467 603 41 0 41190 0
vsize: 164924
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 41002 0 0 0 118877 138 0 0 25 0 1 0 547339881 169697280 40647 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41430 40647 603 41 0 41389 0
vsize: 165720
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4247
Raw data (stat): 4192 (minisat+) R 4191 27222 27221 0 -1 0 41182 0 0 0 119877 139 0 0 25 0 1 0 547339881 170364928 40827 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41593 40827 603 41 0 41552 0
vsize: 166372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 4247
Raw data (stat): 4192 (minisat+) Z 4191 27222 27221 0 -1 12 41184 0 0 0 119877 146 0 0 25 0 1 0 547339881 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.24
CPU user time (s): 1198.77
CPU system time (s): 1.46578
CPU usage (%): 100.012
Max. virtual memory (Kb): 166372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####