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/miplib2003/normalized-mps-v2-13-7-air04.opb
MD5SUM	ee388359e66788d310d5d5b34d6465c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63236
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	1176.04
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 18829

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-21 16:42:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17425 boxname=wulflinc9 idbench=1341 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ee388359e66788d310d5d5b34d6465c1  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 17425
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        489944 kB
Buffers:         27152 kB
Cached:         494884 kB
SwapCached:          0 kB
Active:         358168 kB
Inactive:       166652 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        489692 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14148 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:02:32 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 17425 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   67
c ---[1640]---> BDD-cost:  303
c ---[1638]---> BDD-cost:  119
c ---[1636]---> BDD-cost:  145
c ---[1634]---> BDD-cost:  165
c ---[1632]---> BDD-cost:  239
c ---[1630]---> BDD-cost:  223
c ---[1628]---> BDD-cost:   59
c ---[1626]---> BDD-cost:   35
c ---[1624]---> BDD-cost:   93
c ---[1622]---> BDD-cost:   45
c ---[1620]---> BDD-cost:  213
c ---[1618]---> BDD-cost:   73
c ---[1616]---> BDD-cost:   75
c ---[1614]---> BDD-cost:   63
c ---[1612]---> BDD-cost:   99
c ---[1608]---> BDD-cost:  187
c ---[1606]---> BDD-cost:   55
c ---[1604]---> BDD-cost:  107
c ---[1602]---> BDD-cost:   69
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   75
c ---[1596]---> BDD-cost:    3
c ---[1594]---> BDD-cost:  149
c ---[1592]---> BDD-cost:  137
c ---[1590]---> BDD-cost:  195
c ---[1588]---> BDD-cost:   93
c ---[1586]---> BDD-cost:  157
c ---[1584]---> BDD-cost:  233
c ---[1582]---> BDD-cost:  223
c ---[1580]---> BDD-cost:  225
c ---[1578]---> BDD-cost:  247
c ---[1576]---> BDD-cost:   75
c ---[1574]---> BDD-cost:  179
c ---[1572]---> BDD-cost:  225
c ---[1570]---> BDD-cost:  243
c ---[1568]---> BDD-cost:  199
c ---[1566]---> BDD-cost:   55
c ---[1564]---> BDD-cost:   57
c ---[1562]---> BDD-cost:   99
c ---[1560]---> BDD-cost:    9
c ---[1558]---> BDD-cost:    3
c ---[1556]---> BDD-cost:   23
c ---[1554]---> BDD-cost:   55
c ---[1552]---> BDD-cost:   51
c ---[1550]---> BDD-cost:   25
c ---[1548]---> BDD-cost:   23
c ---[1546]---> BDD-cost:   27
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:   37
c ---[1540]---> BDD-cost:   67
c ---[1538]---> BDD-cost:   67
c ---[1536]---> BDD-cost:  109
c ---[1534]---> BDD-cost:  211
c ---[1532]---> BDD-cost:   15
c ---[1530]---> BDD-cost:    0
c ---[1526]---> BDD-cost:   65
c ---[1524]---> BDD-cost:  117
c ---[1522]---> BDD-cost:   65
c ---[1520]---> BDD-cost:   65
c ---[1518]---> BDD-cost:   49
c ---[1516]---> BDD-cost:  439
c ---[1514]---> BDD-cost:  423
c ---[1512]---> BDD-cost:  287
c ---[1510]---> BDD-cost:   87
c ---[1508]---> BDD-cost:  217
c ---[1506]---> BDD-cost:  195
c ---[1504]---> BDD-cost:   63
c ---[1502]---> BDD-cost:   53
c ---[1500]---> BDD-cost:  359
c ---[1498]---> BDD-cost:  353
c ---[1494]---> BDD-cost:  169
c ---[1492]---> BDD-cost:  139
c ---[1490]---> BDD-cost:  159
c ---[1488]---> BDD-cost:   51
c ---[1486]---> BDD-cost:  223
c ---[1484]---> BDD-cost:  107
c ---[1482]---> BDD-cost:   75
c ---[1480]---> BDD-cost:  109
c ---[1478]---> BDD-cost:   93
c ---[1476]---> BDD-cost:   87
c ---[1474]---> BDD-cost:   87
c ---[1472]---> BDD-cost:    7
c ---[1468]---> BDD-cost:   73
c ---[1466]---> BDD-cost:    1
c ---[1464]---> BDD-cost:   71
c ---[1462]---> BDD-cost:  107
c ---[1460]---> BDD-cost:   77
c ---[1458]---> BDD-cost:    3
c ---[1456]---> BDD-cost:  107
c ---[1454]---> BDD-cost:  131
c ---[1452]---> BDD-cost:  135
c ---[1450]---> BDD-cost:   65
c ---[1448]---> BDD-cost:  165
c ---[1446]---> BDD-cost:  123
c ---[1444]---> BDD-cost:    1
c ---[1442]---> BDD-cost:    1
c ---[1440]---> BDD-cost:   87
c ---[1438]---> BDD-cost:  155
c ---[1436]---> BDD-cost:  167
c ---[1434]---> BDD-cost:  203
c ---[1432]---> BDD-cost:  231
c ---[1430]---> BDD-cost:  147
c ---[1428]---> BDD-cost:  135
c ---[1426]---> BDD-cost:   49
c ---[1424]---> BDD-cost:   31
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   23
c ---[1418]---> BDD-cost:   95
c ---[1416]---> BDD-cost:  325
c ---[1414]---> BDD-cost:  333
c ---[1412]---> BDD-cost:  173
c ---[1410]---> BDD-cost:  269
c ---[1408]---> BDD-cost:   31
c ---[1406]---> BDD-cost:  413
c ---[1404]---> BDD-cost:  313
c ---[1402]---> BDD-cost:  125
c ---[1400]---> BDD-cost:  113
c ---[1398]---> BDD-cost:   11
c ---[1396]---> BDD-cost:  247
c ---[1394]---> BDD-cost:   57
c ---[1392]---> BDD-cost:  237
c ---[1390]---> BDD-cost:  159
c ---[1388]---> BDD-cost:  117
c ---[1386]---> BDD-cost:   43
c ---[1384]---> BDD-cost:  143
c ---[1382]---> BDD-cost:   65
c ---[1380]---> BDD-cost:  123
c ---[1378]---> BDD-cost:   61
c ---[1376]---> BDD-cost:   39
c ---[1374]---> BDD-cost:  103
c ---[1372]---> BDD-cost:   85
c ---[1370]---> BDD-cost:   77
c ---[1368]---> BDD-cost:   57
c ---[1366]---> BDD-cost:  127
c ---[1364]---> BDD-cost:  157
c ---[1362]---> BDD-cost:  267
c ---[1360]---> BDD-cost:  223
c ---[1358]---> BDD-cost:  229
c ---[1356]---> BDD-cost:  257
c ---[1354]---> BDD-cost:   13
c ---[1352]---> BDD-cost:  241
c ---[1350]---> BDD-cost:  195
c ---[1348]---> BDD-cost:   49
c ---[1346]---> BDD-cost:  117
c ---[1344]---> BDD-cost:  197
c ---[1342]---> BDD-cost:  171
c ---[1340]---> BDD-cost:  287
c ---[1338]---> BDD-cost:   75
c ---[1336]---> BDD-cost:  215
c ---[1334]---> BDD-cost:  119
c ---[1332]---> BDD-cost:   57
c ---[1330]---> BDD-cost:  245
c ---[1328]---> BDD-cost:  257
c ---[1326]---> BDD-cost:  279
c ---[1324]---> BDD-cost:  227
c ---[1322]---> BDD-cost:  201
c ---[1320]---> BDD-cost:  143
c ---[1318]---> BDD-cost:  207
c ---[1316]---> BDD-cost:  131
c ---[1314]---> BDD-cost:  245
c ---[1312]---> BDD-cost:  115
c ---[1310]---> BDD-cost:  259
c ---[1308]---> BDD-cost:   91
c ---[1306]---> BDD-cost:   43
c ---[1304]---> BDD-cost:   39
c ---[1302]---> BDD-cost:   91
c ---[1300]---> BDD-cost:  179
c ---[1298]---> BDD-cost:   73
c ---[1296]---> BDD-cost:   29
c ---[1294]---> BDD-cost:  163
c ---[1292]---> BDD-cost:   81
c ---[1290]---> BDD-cost:   63
c ---[1288]---> BDD-cost:  189
c ---[1286]---> BDD-cost:  103
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  115
c ---[1280]---> BDD-cost:   19
c ---[1278]---> BDD-cost:   93
c ---[1276]---> BDD-cost:   99
c ---[1274]---> BDD-cost:   99
c ---[1272]---> BDD-cost:  103
c ---[1270]---> BDD-cost:   67
c ---[1268]---> BDD-cost:   23
c ---[1266]---> BDD-cost:  101
c ---[1264]---> BDD-cost:   85
c ---[1262]---> BDD-cost:   87
c ---[1260]---> BDD-cost:    7
c ---[1258]---> BDD-cost:   45
c ---[1256]---> BDD-cost:   43
c ---[1254]---> BDD-cost:   11
c ---[1252]---> BDD-cost:   59
c ---[1250]---> BDD-cost:  185
c ---[1248]---> BDD-cost:  249
c ---[1246]---> BDD-cost:  315
c ---[1244]---> BDD-cost:  137
c ---[1242]---> BDD-cost:  253
c ---[1240]---> BDD-cost:  161
c ---[1238]---> BDD-cost:  257
c ---[1236]---> BDD-cost:  167
c ---[1234]---> BDD-cost:  167
c ---[1232]---> BDD-cost:  141
c ---[1230]---> BDD-cost:   21
c ---[1228]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   95
c ---[1224]---> BDD-cost:  141
c ---[1222]---> BDD-cost:    0
c ---[1220]---> BDD-cost:  123
c ---[1218]---> BDD-cost:   83
c ---[1216]---> BDD-cost:   55
c ---[1214]---> BDD-cost:  183
c ---[1212]---> BDD-cost:  269
c ---[1210]---> BDD-cost:   63
c ---[1208]---> BDD-cost:   45
c ---[1206]---> BDD-cost:   39
c ---[1204]---> BDD-cost:   97
c ---[1202]---> BDD-cost:   51
c ---[1200]---> BDD-cost:   23
c ---[1198]---> BDD-cost:  101
c ---[1196]---> BDD-cost:   45
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   85
c ---[1190]---> BDD-cost:   35
c ---[1188]---> BDD-cost:   53
c ---[1186]---> BDD-cost:   21
c ---[1184]---> BDD-cost:  115
c ---[1182]---> BDD-cost:   99
c ---[1180]---> BDD-cost:   63
c ---[1178]---> BDD-cost:   77
c ---[1176]---> BDD-cost:   37
c ---[1174]---> BDD-cost:  139
c ---[1172]---> BDD-cost:  109
c ---[1170]---> BDD-cost:  407
c ---[1168]---> BDD-cost:  323
c ---[1166]---> BDD-cost:  109
c ---[1164]---> BDD-cost:   93
c ---[1162]---> BDD-cost:   51
c ---[1160]---> BDD-cost:   79
c ---[1158]---> BDD-cost:   75
c ---[1156]---> BDD-cost:  147
c ---[1154]---> BDD-cost:    0
c ---[1152]---> BDD-cost:  169
c ---[1150]---> BDD-cost:  209
c ---[1148]---> BDD-cost:   69
c ---[1146]---> BDD-cost:   51
c ---[1144]---> BDD-cost:   85
c ---[1140]---> BDD-cost:  103
c ---[1138]---> BDD-cost:  127
c ---[1136]---> BDD-cost:   77
c ---[1134]---> BDD-cost:   77
c ---[1132]---> BDD-cost:  181
c ---[1130]---> BDD-cost:  141
c ---[1128]---> BDD-cost:   89
c ---[1126]---> BDD-cost:   85
c ---[1124]---> BDD-cost:  119
c ---[1122]---> BDD-cost:   69
c ---[1120]---> BDD-cost:   57
c ---[1118]---> BDD-cost:   65
c ---[1116]---> BDD-cost:   47
c ---[1114]---> BDD-cost:   61
c ---[1112]---> BDD-cost:   31
c ---[1110]---> BDD-cost:  283
c ---[1106]---> BDD-cost:  183
c ---[1104]---> BDD-cost:  121
c ---[1102]---> BDD-cost:   89
c ---[1100]---> BDD-cost:  225
c ---[1098]---> BDD-cost:  267
c ---[1094]---> BDD-cost:  159
c ---[1092]---> BDD-cost:  209
c ---[1090]---> BDD-cost:   71
c ---[1088]---> BDD-cost:   99
c ---[1086]---> BDD-cost:  237
c ---[1084]---> BDD-cost:  129
c ---[1082]---> BDD-cost:  365
c ---[1080]---> BDD-cost:  369
c ---[1078]---> BDD-cost:  129
c ---[1076]---> BDD-cost:  101
c ---[1074]---> BDD-cost:  289
c ---[1072]---> BDD-cost:  279
c ---[1070]---> BDD-cost:  345
c ---[1068]---> BDD-cost:   81
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:   69
c ---[1062]---> BDD-cost:   83
c ---[1060]---> BDD-cost:   53
c ---[1058]---> BDD-cost:   67
c ---[1056]---> BDD-cost:   55
c ---[1054]---> BDD-cost:  145
c ---[1052]---> BDD-cost:  149
c ---[1050]---> BDD-cost:  105
c ---[1048]---> BDD-cost:   19
c ---[1046]---> BDD-cost:  105
c ---[1044]---> BDD-cost:  109
c ---[1042]---> BDD-cost:  101
c ---[1040]---> BDD-cost:  147
c ---[1038]---> BDD-cost:  231
c ---[1036]---> BDD-cost:  191
c ---[1034]---> BDD-cost:  157
c ---[1032]---> BDD-cost:  249
c ---[1030]---> BDD-cost:  385
c ---[1028]---> BDD-cost:   67
c ---[1026]---> BDD-cost:   71
c ---[1024]---> BDD-cost:   47
c ---[1022]---> BDD-cost:   75
c ---[1020]---> BDD-cost:  147
c ---[1018]---> BDD-cost:  139
c ---[1016]---> BDD-cost:  273
c ---[1014]---> BDD-cost:  213
c ---[1012]---> BDD-cost:  169
c ---[1010]---> BDD-cost:  239
c ---[1008]---> BDD-cost:  305
c ---[1006]---> BDD-cost:  109
c ---[1004]---> BDD-cost:  105
c ---[1002]---> BDD-cost:  147
c ---[1000]---> BDD-cost:  237
c ---[ 998]---> BDD-cost:  115
c ---[ 996]---> BDD-cost:  115
c ---[ 994]---> BDD-cost:   67
c ---[ 992]---> BDD-cost:  329
c ---[ 990]---> BDD-cost:  295
c ---[ 988]---> BDD-cost:   51
c ---[ 986]---> BDD-cost:   61
c ---[ 984]---> BDD-cost:  317
c ---[ 982]---> BDD-cost:   97
c ---[ 980]---> BDD-cost:   79
c ---[ 978]---> BDD-cost:   29
c ---[ 976]---> BDD-cost:  119
c ---[ 974]---> BDD-cost:   43
c ---[ 972]---> BDD-cost:   85
c ---[ 970]---> BDD-cost:   35
c ---[ 968]---> BDD-cost:   69
c ---[ 964]---> BDD-cost:   45
c ---[ 962]---> BDD-cost:   73
c ---[ 960]---> BDD-cost:   55
c ---[ 956]---> BDD-cost:   33
c ---[ 954]---> BDD-cost:  109
c ---[ 952]---> BDD-cost:   29
c ---[ 950]---> BDD-cost:  245
c ---[ 948]---> BDD-cost:  225
c ---[ 946]---> BDD-cost:  111
c ---[ 944]---> BDD-cost:  117
c ---[ 942]---> BDD-cost:  127
c ---[ 940]---> BDD-cost:  129
c ---[ 938]---> BDD-cost:  259
c ---[ 936]---> BDD-cost:  221
c ---[ 934]---> BDD-cost:  275
c ---[ 932]---> BDD-cost:   83
c ---[ 930]---> BDD-cost:  209
c ---[ 928]---> BDD-cost:  267
c ---[ 926]---> BDD-cost:  171
c ---[ 924]---> BDD-cost:   57
c ---[ 920]---> BDD-cost:  133
c ---[ 918]---> BDD-cost:  185
c ---[ 916]---> BDD-cost:  169
c ---[ 914]---> BDD-cost:  287
c ---[ 912]---> BDD-cost:   81
c ---[ 910]---> BDD-cost:   13
c ---[ 908]---> BDD-cost:  335
c ---[ 906]---> BDD-cost:  365
c ---[ 904]---> BDD-cost:  255
c ---[ 902]---> BDD-cost:  111
c ---[ 900]---> BDD-cost:   57
c ---[ 898]---> BDD-cost:  101
c ---[ 896]---> BDD-cost:  197
c ---[ 894]---> BDD-cost:  383
c ---[ 892]---> BDD-cost:  329
c ---[ 890]---> BDD-cost:  241
c ---[ 888]---> BDD-cost:  157
c ---[ 886]---> BDD-cost:  129
c ---[ 884]---> BDD-cost:   85
c ---[ 882]---> BDD-cost:   71
c ---[ 880]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   77
c ---[ 876]---> BDD-cost:   49
c ---[ 874]---> BDD-cost:  133
c ---[ 872]---> BDD-cost:  133
c ---[ 870]---> BDD-cost:  377
c ---[ 868]---> BDD-cost:  117
c ---[ 866]---> BDD-cost:  155
c ---[ 862]---> BDD-cost:  119
c ---[ 860]---> BDD-cost:  119
c ---[ 858]---> BDD-cost:  151
c ---[ 856]---> BDD-cost:  221
c ---[ 854]---> BDD-cost:  181
c ---[ 850]---> BDD-cost:   87
c ---[ 848]---> BDD-cost:  127
c ---[ 846]---> BDD-cost:  299
c ---[ 844]---> BDD-cost:  109
c ---[ 842]---> BDD-cost:  331
c ---[ 838]---> BDD-cost:   21
c ---[ 836]---> BDD-cost:  205
c ---[ 834]---> BDD-cost:  217
c ---[ 832]---> BDD-cost:  349
c ---[ 830]---> BDD-cost:  291
c ---[ 828]---> BDD-cost:  165
c ---[ 826]---> BDD-cost:  161
c ---[ 824]---> BDD-cost:   61
c ---[ 822]---> BDD-cost:   77
c ---[ 820]---> BDD-cost:   55
c ---[ 818]---> BDD-cost:  113
c ---[ 816]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:  189
c ---[ 812]---> BDD-cost:  157
c ---[ 810]---> BDD-cost:  149
c ---[ 808]---> BDD-cost:  139
c ---[ 806]---> BDD-cost:  165
c ---[ 804]---> BDD-cost:  181
c ---[ 802]---> BDD-cost:  253
c ---[ 800]---> BDD-cost:    0
c ---[ 798]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:  145
c ---[ 794]---> BDD-cost:  141
c ---[ 792]---> BDD-cost:  105
c ---[ 790]---> BDD-cost:   95
c ---[ 788]---> BDD-cost:   75
c ---[ 786]---> BDD-cost:  103
c ---[ 784]---> BDD-cost:  149
c ---[ 782]---> BDD-cost:  137
c ---[ 780]---> BDD-cost:   59
c ---[ 778]---> BDD-cost:  133
c ---[ 776]---> BDD-cost:    5
c ---[ 774]---> BDD-cost:   35
c ---[ 772]---> BDD-cost:    9
c ---[ 770]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   55
c ---[ 762]---> BDD-cost:  197
c ---[ 760]---> BDD-cost:  191
c ---[ 758]---> BDD-cost:  125
c ---[ 756]---> BDD-cost:    0
c ---[ 754]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  173
c ---[ 748]---> BDD-cost:   93
c ---[ 746]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:  321
c ---[ 742]---> BDD-cost:  195
c ---[ 740]---> BDD-cost:  163
c ---[ 734]---> BDD-cost:  151
c ---[ 732]---> BDD-cost:  115
c ---[ 730]---> BDD-cost:  253
c ---[ 728]---> BDD-cost:  381
c ---[ 726]---> BDD-cost:  345
c ---[ 724]---> BDD-cost:  185
c ---[ 720]---> BDD-cost:   83
c ---[ 718]---> BDD-cost:   69
c ---[ 716]---> BDD-cost:   51
c ---[ 714]---> BDD-cost:   47
c ---[ 712]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:  185
c ---[ 708]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  107
c ---[ 704]---> BDD-cost:  363
c ---[ 702]---> BDD-cost:  103
c ---[ 700]---> BDD-cost:  277
c ---[ 698]---> BDD-cost:  341
c ---[ 696]---> BDD-cost:  213
c ---[ 694]---> BDD-cost:  315
c ---[ 692]---> BDD-cost:  275
c ---[ 690]---> BDD-cost:  151
c ---[ 688]---> BDD-cost:  203
c ---[ 686]---> BDD-cost:  111
c ---[ 684]---> BDD-cost:  103
c ---[ 682]---> BDD-cost:   75
c ---[ 680]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   21
c ---[ 676]---> BDD-cost:   11
c ---[ 674]---> BDD-cost:   31
c ---[ 670]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:  149
c ---[ 666]---> BDD-cost:  167
c ---[ 664]---> BDD-cost:    0
c ---[ 662]---> BDD-cost:   97
c ---[ 660]---> BDD-cost:  149
c ---[ 658]---> BDD-cost:  395
c ---[ 656]---> BDD-cost:   25
c ---[ 654]---> BDD-cost:  389
c ---[ 652]---> BDD-cost:  251
c ---[ 650]---> BDD-cost:  375
c ---[ 648]---> BDD-cost:  343
c ---[ 646]---> BDD-cost:  267
c ---[ 644]---> BDD-cost:  135
c ---[ 642]---> BDD-cost:  135
c ---[ 640]---> BDD-cost:  263
c ---[ 638]---> BDD-cost:  259
c ---[ 636]---> BDD-cost:  245
c ---[ 634]---> BDD-cost:   45
c ---[ 632]---> BDD-cost:   41
c ---[ 630]---> BDD-cost:  127
c ---[ 628]---> BDD-cost:  117
c ---[ 626]---> BDD-cost:   53
c ---[ 624]---> BDD-cost:  149
c ---[ 622]---> BDD-cost:    9
c ---[ 620]---> BDD-cost:  103
c ---[ 618]---> BDD-cost:  215
c ---[ 616]---> BDD-cost:   89
c ---[ 614]---> BDD-cost:  177
c ---[ 612]---> BDD-cost:  343
c ---[ 610]---> BDD-cost:  237
c ---[ 608]---> BDD-cost:  177
c ---[ 606]---> BDD-cost:   85
c ---[ 604]---> BDD-cost:  267
c ---[ 602]---> BDD-cost:  225
c ---[ 600]---> BDD-cost:   85
c ---[ 598]---> BDD-cost:  109
c ---[ 596]---> BDD-cost:  105
c ---[ 594]---> BDD-cost:  113
c ---[ 592]---> BDD-cost:   55
c ---[ 590]---> BDD-cost:  117
c ---[ 588]---> BDD-cost:   83
c ---[ 586]---> BDD-cost:   79
c ---[ 584]---> BDD-cost:   81
c ---[ 582]---> BDD-cost:  263
c ---[ 580]---> BDD-cost:  179
c ---[ 578]---> BDD-cost:  143
c ---[ 576]---> BDD-cost:  281
c ---[ 574]---> BDD-cost:  389
c ---[ 572]---> BDD-cost:  333
c ---[ 570]---> BDD-cost:  357
c ---[ 568]---> BDD-cost:  345
c ---[ 566]---> BDD-cost:  263
c ---[ 564]---> BDD-cost:   89
c ---[ 562]---> BDD-cost:  285
c ---[ 558]---> BDD-cost:  419
c ---[ 556]---> BDD-cost:  135
c ---[ 554]---> BDD-cost:  357
c ---[ 552]---> BDD-cost:  473
c ---[ 550]---> BDD-cost:  455
c ---[ 548]---> BDD-cost:  405
c ---[ 546]---> BDD-cost:  241
c ---[ 544]---> BDD-cost:  211
c ---[ 542]---> BDD-cost:  313
c ---[ 540]---> BDD-cost:  371
c ---[ 538]---> BDD-cost:  389
c ---[ 536]---> BDD-cost:  223
c ---[ 534]---> BDD-cost:   71
c ---[ 532]---> BDD-cost:   63
c ---[ 530]---> BDD-cost:  221
c ---[ 528]---> BDD-cost:  147
c ---[ 526]---> BDD-cost:  131
c ---[ 524]---> BDD-cost:  185
c ---[ 522]---> BDD-cost:  141
c ---[ 520]---> BDD-cost:  249
c ---[ 518]---> BDD-cost:  261
c ---[ 516]---> BDD-cost:  311
c ---[ 514]---> BDD-cost:  261
c ---[ 512]---> BDD-cost:  387
c ---[ 510]---> BDD-cost:   51
c ---[ 508]---> BDD-cost:  247
c ---[ 506]---> BDD-cost:  295
c ---[ 504]---> BDD-cost:   31
c ---[ 502]---> BDD-cost:  355
c ---[ 500]---> BDD-cost:  135
c ---[ 498]---> BDD-cost:  443
c ---[ 496]---> BDD-cost:  653
c ---[ 494]---> BDD-cost:  703
c ---[ 492]---> BDD-cost:  517
c ---[ 490]---> BDD-cost:  441
c ---[ 488]---> BDD-cost:  159
c ---[ 486]---> BDD-cost:  411
c ---[ 484]---> BDD-cost:  289
c ---[ 482]---> BDD-cost:  277
c ---[ 480]---> BDD-cost:  239
c ---[ 478]---> BDD-cost:  201
c ---[ 476]---> BDD-cost:  309
c ---[ 474]---> BDD-cost:  287
c ---[ 472]---> BDD-cost:  177
c ---[ 470]---> BDD-cost:  143
c ---[ 468]---> BDD-cost:  131
c ---[ 466]---> BDD-cost:  155
c ---[ 464]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:  189
c ---[ 460]---> BDD-cost:  219
c ---[ 456]---> BDD-cost:  267
c ---[ 454]---> BDD-cost:  135
c ---[ 452]---> BDD-cost:   69
c ---[ 450]---> BDD-cost:   75
c ---[ 448]---> BDD-cost:   51
c ---[ 446]---> BDD-cost:  117
c ---[ 444]---> BDD-cost:  211
c ---[ 442]---> BDD-cost:  117
c ---[ 436]---> BDD-cost:  189
c ---[ 434]---> BDD-cost:   73
c ---[ 432]---> BDD-cost:   55
c ---[ 430]---> BDD-cost:   57
c ---[ 428]---> BDD-cost:   91
c ---[ 426]---> BDD-cost:  325
c ---[ 424]---> BDD-cost:  223
c ---[ 422]---> BDD-cost:   75
c ---[ 420]---> BDD-cost:   57
c ---[ 418]---> BDD-cost:   43
c ---[ 416]---> BDD-cost:  255
c ---[ 414]---> BDD-cost:  285
c ---[ 412]---> BDD-cost:  187
c ---[ 410]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   91
c ---[ 406]---> BDD-cost:  211
c ---[ 404]---> BDD-cost:  159
c ---[ 402]---> BDD-cost:   97
c ---[ 400]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   27
c ---[ 396]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  141
c ---[ 390]---> BDD-cost:  109
c ---[ 388]---> BDD-cost:  321
c ---[ 386]---> BDD-cost:  305
c ---[ 384]---> BDD-cost:  603
c ---[ 382]---> BDD-cost:  441
c ---[ 380]---> BDD-cost:  391
c ---[ 378]---> BDD-cost:   87
c ---[ 376]---> BDD-cost:  387
c ---[ 374]---> BDD-cost:  289
c ---[ 372]---> BDD-cost:  219
c ---[ 370]---> BDD-cost:  309
c ---[ 368]---> BDD-cost:  241
c ---[ 366]---> BDD-cost:  197
c ---[ 364]---> BDD-cost:  279
c ---[ 362]---> BDD-cost:  167
c ---[ 360]---> BDD-cost:  151
c ---[ 358]---> BDD-cost:   49
c ---[ 356]---> BDD-cost:   79
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:  107
c ---[ 350]---> BDD-cost:   55
c ---[ 346]---> BDD-cost:  177
c ---[ 344]---> BDD-cost:  223
c ---[ 342]---> BDD-cost:  119
c ---[ 340]---> BDD-cost:  137
c ---[ 338]---> BDD-cost:  105
c ---[ 336]---> BDD-cost:  183
c ---[ 334]---> BDD-cost:  109
c ---[ 332]---> BDD-cost:  179
c ---[ 330]---> BDD-cost:  285
c ---[ 328]---> BDD-cost:  191
c ---[ 326]---> BDD-cost:  177
c ---[ 324]---> BDD-cost:  145
c ---[ 320]---> BDD-cost:  153
c ---[ 318]---> BDD-cost:  121
c ---[ 316]---> BDD-cost:   95
c ---[ 314]---> BDD-cost:  111
c ---[ 312]---> BDD-cost:   35
c ---[ 310]---> BDD-cost:  115
c ---[ 308]---> BDD-cost:    0
c ---[ 306]---> BDD-cost:  281
c ---[ 304]---> BDD-cost:  265
c ---[ 302]---> BDD-cost:  167
c ---[ 300]---> BDD-cost:  151
c ---[ 298]---> BDD-cost:  167
c ---[ 296]---> BDD-cost:  137
c ---[ 292]---> BDD-cost:  375
c ---[ 290]---> BDD-cost:  287
c ---[ 288]---> BDD-cost:  247
c ---[ 286]---> BDD-cost:  249
c ---[ 284]---> BDD-cost:  131
c ---[ 282]---> BDD-cost:  187
c ---[ 280]---> BDD-cost:  135
c ---[ 278]---> BDD-cost:  129
c ---[ 276]---> BDD-cost:  317
c ---[ 274]---> BDD-cost:  365
c ---[ 272]---> BDD-cost:  235
c ---[ 270]---> BDD-cost:  249
c ---[ 268]---> BDD-cost:  283
c ---[ 266]---> BDD-cost:  105
c ---[ 264]---> BDD-cost:  233
c ---[ 262]---> BDD-cost:  259
c ---[ 260]---> BDD-cost:  287
c ---[ 258]---> BDD-cost:  175
c ---[ 256]---> BDD-cost:  233
c ---[ 254]---> BDD-cost:  167
c ---[ 252]---> BDD-cost:  159
c ---[ 250]---> BDD-cost:   47
c ---[ 246]---> BDD-cost:  135
c ---[ 244]---> BDD-cost:   59
c ---[ 242]---> BDD-cost:  147
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  203
c ---[ 236]---> BDD-cost:  275
c ---[ 234]---> BDD-cost:  263
c ---[ 232]---> BDD-cost:   31
c ---[ 230]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   31
c ---[ 226]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:  225
c ---[ 222]---> BDD-cost:   71
c ---[ 220]---> BDD-cost:   65
c ---[ 218]---> BDD-cost:  385
c ---[ 216]---> BDD-cost:  361
c ---[ 214]---> BDD-cost:   73
c ---[ 212]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:  131
c ---[ 206]---> BDD-cost:  145
c ---[ 204]---> BDD-cost:  121
c ---[ 202]---> BDD-cost:  117
c ---[ 200]---> BDD-cost:   61
c ---[ 198]---> BDD-cost:  111
c ---[ 196]---> BDD-cost:  123
c ---[ 194]---> BDD-cost:  125
c ---[ 192]---> BDD-cost:  243
c ---[ 190]---> BDD-cost:  143
c ---[ 188]---> BDD-cost:  149
c ---[ 186]---> BDD-cost:  103
c ---[ 184]---> BDD-cost:  155
c ---[ 182]---> BDD-cost:  247
c ---[ 180]---> BDD-cost:  143
c ---[ 178]---> BDD-cost:   89
c ---[ 176]---> BDD-cost:   91
c ---[ 174]---> BDD-cost:   81
c ---[ 172]---> BDD-cost:   79
c ---[ 170]---> BDD-cost:  117
c ---[ 168]---> BDD-cost:   89
c ---[ 166]---> BDD-cost:   61
c ---[ 164]---> BDD-cost:  127
c ---[ 162]---> BDD-cost:  135
c ---[ 160]---> BDD-cost:  161
c ---[ 158]---> BDD-cost:  141
c ---[ 156]---> BDD-cost:   91
c ---[ 154]---> BDD-cost:  437
c ---[ 152]---> BDD-cost:  309
c ---[ 150]---> BDD-cost:  173
c ---[ 148]---> BDD-cost:  441
c ---[ 146]---> BDD-cost:  489
c ---[ 144]---> BDD-cost:  299
c ---[ 142]---> BDD-cost:  455
c ---[ 140]---> BDD-cost:  333
c ---[ 138]---> BDD-cost:  421
c ---[ 136]---> BDD-cost:  375
c ---[ 134]---> BDD-cost:  143
c ---[ 132]---> BDD-cost:  433
c ---[ 130]---> BDD-cost:  405
c ---[ 128]---> BDD-cost:  333
c ---[ 126]---> BDD-cost:  673
c ---[ 124]---> BDD-cost:  685
c ---[ 122]---> BDD-cost:  385
c ---[ 120]---> BDD-cost:  267
c ---[ 118]---> BDD-cost:  345
c ---[ 116]---> BDD-cost:  365
c ---[ 114]---> BDD-cost:  391
c ---[ 112]---> BDD-cost:  111
c ---[ 110]---> BDD-cost:  313
c ---[ 108]---> BDD-cost:  275
c ---[ 106]---> BDD-cost:  257
c ---[ 104]---> BDD-cost:  203
c ---[ 102]---> BDD-cost:  311
c ---[ 100]---> BDD-cost:  227
c ---[  98]---> BDD-cost:  295
c ---[  96]---> BDD-cost:  233
c ---[  94]---> BDD-cost:  247
c ---[  92]---> BDD-cost:  237
c ---[  90]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   95
c ---[  86]---> BDD-cost:    0
c ---[  84]---> BDD-cost:  149
c ---[  80]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   85
c ---[  76]---> BDD-cost:  109
c ---[  74]---> BDD-cost:   43
c ---[  72]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   71
c ---[  68]---> BDD-cost:   67
c ---[  66]---> BDD-cost:  169
c ---[  64]---> BDD-cost:  151
c ---[  62]---> BDD-cost:  147
c ---[  60]---> BDD-cost:  177
c ---[  58]---> BDD-cost:  127
c ---[  56]---> BDD-cost:  131
c ---[  54]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  215
c ---[  50]---> BDD-cost:  181
c ---[  48]---> BDD-cost:  235
c ---[  46]---> BDD-cost:  163
c ---[  44]---> BDD-cost:  101
c ---[  42]---> BDD-cost:   57
c ---[  40]---> BDD-cost:   59
c ---[  38]---> BDD-cost:  139
c ---[  36]---> BDD-cost:   39
c ---[  34]---> BDD-cost:  151
c ---[  32]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   45
c ---[  28]---> BDD-cost:   45
c ---[  26]---> BDD-cost:   45
c ---[  24]---> BDD-cost:   65
c ---[  22]---> BDD-cost:   95
c ---[  20]---> BDD-cost:    0
c ---[  16]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   81
c ---[   2]---> BDD-cost:  223
c ---[   0]---> BDD-cost:  271
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       101 |  310358   807732 |  113797     101     4421    43.8 |  0.588 % |
c |       251 |  310340   807685 |  125176     248     8941    36.1 |  0.590 % |
c |       477 |  310255   807455 |  137694     461    13728    29.8 |  0.603 % |
c |       814 |  310255   807455 |  151464     798    37090    46.5 |  0.603 % |
c |      1320 |  309505   805553 |  166610    1266    60778    48.0 |  0.693 % |
c |      2079 |  309327   805067 |  183271    2007    94497    47.1 |  0.730 % |
c |      3219 |  308710   803466 |  201598    3121   175840    56.3 |  0.848 % |
c |      4927 |  308374   802597 |  221758    4783   334504    69.9 |  0.896 % |
c |      7489 |  307940   801458 |  243934    7200   539854    75.0 |  0.948 % |
c |     11334 |  307798   801098 |  268327   11017  1054203    95.7 |  0.963 % |
c |     17100 |  307510   800357 |  295160   16719  1913448   114.4 |  0.992 % |
c |     25749 |  307286   799785 |  324676   25320  3051328   120.5 |  1.011 % |
c |     38723 |  307204   799580 |  357144   38277  5578865   145.7 |  1.014 % |
c |     58184 |  306684   798243 |  392858   57603  9277788   161.1 |  1.076 % |
c |     87376 |  306512   797802 |  432144   86712 17039623   196.5 |  1.089 % |
c |    131165 |  306227   797059 |  475359  130316 29832985   228.9 |  1.132 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.93 2/54 20873
Raw data (stat): 20873 (runsolver) R 20872 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488384324 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.99973 s]
Raw data (loadavg): 0.88 0.94 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 11041 0 0 0 970 28 0 0 25 0 1 0 488384324 54317056 10671 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13261 10671 603 41 0 13220 0
vsize: 53044
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 11183 0 0 0 1970 29 0 0 25 0 1 0 488384324 54857728 10813 4294967295 134512640 134672761 3221224624 3221223820 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13393 10813 603 41 0 13352 0
vsize: 53572
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.94 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 11356 0 0 0 2969 29 0 0 25 0 1 0 488384324 55672832 10986 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13592 10986 603 41 0 13551 0
vsize: 54368
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.94 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 11535 0 0 0 3968 30 0 0 25 0 1 0 488384324 56344576 11165 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13756 11165 603 41 0 13715 0
vsize: 55024
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 11713 0 0 0 4968 30 0 0 25 0 1 0 488384324 57061376 11343 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13931 11343 603 41 0 13890 0
vsize: 55724
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 12037 0 0 0 5966 32 0 0 25 0 1 0 488384324 58404864 11667 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14259 11667 603 41 0 14218 0
vsize: 57036
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 12311 0 0 0 6966 33 0 0 25 0 1 0 488384324 59486208 11941 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14523 11941 603 41 0 14482 0
vsize: 58092
[startup+80.0032 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 12671 0 0 0 7965 34 0 0 25 0 1 0 488384324 60968960 12301 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14885 12301 603 41 0 14844 0
vsize: 59540
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 13018 0 0 0 8964 35 0 0 25 0 1 0 488384324 62427136 12648 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15241 12648 603 41 0 15200 0
vsize: 60964
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 13329 0 0 0 9963 36 0 0 25 0 1 0 488384324 63778816 12959 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15571 12959 603 41 0 15530 0
vsize: 62284
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 13571 0 0 0 10963 36 0 0 25 0 1 0 488384324 64720896 13201 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15801 13201 603 41 0 15760 0
vsize: 63204
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 13853 0 0 0 11962 37 0 0 25 0 1 0 488384324 65794048 13483 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16063 13483 603 41 0 16022 0
vsize: 64252
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 14135 0 0 0 12961 38 0 0 25 0 1 0 488384324 67006464 13765 4294967295 134512640 134672761 3221224624 3221223808 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16359 13765 603 41 0 16318 0
vsize: 65436
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 14488 0 0 0 13961 39 0 0 25 0 1 0 488384324 68354048 14118 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16688 14118 603 41 0 16647 0
vsize: 66752
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 14725 0 0 0 14960 40 0 0 25 0 1 0 488384324 69292032 14355 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16917 14355 603 41 0 16876 0
vsize: 67668
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 15107 0 0 0 15958 41 0 0 25 0 1 0 488384324 70905856 14737 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17311 14737 603 41 0 17270 0
vsize: 69244
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 15446 0 0 0 16958 42 0 0 25 0 1 0 488384324 72257536 15076 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17641 15076 603 41 0 17600 0
vsize: 70564
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 15751 0 0 0 17957 42 0 0 25 0 1 0 488384324 73469952 15381 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17937 15381 603 41 0 17896 0
vsize: 71748
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 16157 0 0 0 18957 43 0 0 25 0 1 0 488384324 75354112 15787 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18397 15787 603 41 0 18356 0
vsize: 73588
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 16542 0 0 0 19956 44 0 0 25 0 1 0 488384324 76828672 16172 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18757 16172 603 41 0 18716 0
vsize: 75028
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 16837 0 0 0 20955 45 0 0 25 0 1 0 488384324 78036992 16467 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19052 16467 603 41 0 19011 0
vsize: 76208
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 17143 0 0 0 21955 46 0 0 25 0 1 0 488384324 79384576 16773 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19381 16773 603 41 0 19340 0
vsize: 77524
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 17357 0 0 0 22955 46 0 0 25 0 1 0 488384324 80191488 16987 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19578 16987 603 41 0 19537 0
vsize: 78312
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 17644 0 0 0 23954 47 0 0 25 0 1 0 488384324 81399808 17274 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19873 17274 603 41 0 19832 0
vsize: 79492
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 17921 0 0 0 24954 47 0 0 25 0 1 0 488384324 82481152 17551 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20137 17551 603 41 0 20096 0
vsize: 80548
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 18337 0 0 0 25953 48 0 0 25 0 1 0 488384324 84234240 17967 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20565 17967 603 41 0 20524 0
vsize: 82260
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 18621 0 0 0 26952 49 0 0 25 0 1 0 488384324 85315584 18251 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20829 18251 603 41 0 20788 0
vsize: 83316
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 18905 0 0 0 27952 50 0 0 25 0 1 0 488384324 86523904 18535 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21124 18535 603 41 0 21083 0
vsize: 84496
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 19155 0 0 0 28951 51 0 0 25 0 1 0 488384324 87597056 18785 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21386 18785 603 41 0 21345 0
vsize: 85544
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 19521 0 0 0 29950 52 0 0 25 0 1 0 488384324 89083904 19151 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21749 19151 603 41 0 21708 0
vsize: 86996
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 19873 0 0 0 30949 53 0 0 25 0 1 0 488384324 90423296 19503 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 19503 603 41 0 22035 0
vsize: 88304
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 20196 0 0 0 31949 54 0 0 25 0 1 0 488384324 91762688 19826 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22403 19826 603 41 0 22362 0
vsize: 89612
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 20605 0 0 0 32948 55 0 0 25 0 1 0 488384324 93503488 20235 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22828 20235 603 41 0 22787 0
vsize: 91312
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 20953 0 0 0 33946 57 0 0 25 0 1 0 488384324 94851072 20583 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23157 20583 603 41 0 23116 0
vsize: 92628
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 21207 0 0 0 34945 58 0 0 25 0 1 0 488384324 95928320 20837 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23420 20837 603 41 0 23379 0
vsize: 93680
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 21468 0 0 0 35945 58 0 0 25 0 1 0 488384324 97005568 21098 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23683 21098 603 41 0 23642 0
vsize: 94732
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 21911 0 0 0 36944 60 0 0 25 0 1 0 488384324 98754560 21541 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24110 21541 603 41 0 24069 0
vsize: 96440
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 22268 0 0 0 37943 61 0 0 25 0 1 0 488384324 100237312 21898 4294967295 134512640 134672761 3221224624 3221223760 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24472 21898 603 41 0 24431 0
vsize: 97888
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 22624 0 0 0 38941 62 0 0 25 0 1 0 488384324 101707776 22254 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24831 22254 603 41 0 24790 0
vsize: 99324
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 22916 0 0 0 39940 64 0 0 25 0 1 0 488384324 103182336 22546 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25191 22546 603 41 0 25150 0
vsize: 100764
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 23237 0 0 0 40939 65 0 0 25 0 1 0 488384324 104394752 22867 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25487 22867 603 41 0 25446 0
vsize: 101948
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 23662 0 0 0 41938 66 0 0 25 0 1 0 488384324 106156032 23292 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25917 23292 603 41 0 25876 0
vsize: 103668
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 24081 0 0 0 42937 67 0 0 25 0 1 0 488384324 107896832 23711 4294967295 134512640 134672761 3221224624 3221223808 134558903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26342 23711 603 41 0 26301 0
vsize: 105368
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 24334 0 0 0 43937 68 0 0 25 0 1 0 488384324 108965888 23964 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26603 23964 603 41 0 26562 0
vsize: 106412
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 24570 0 0 0 44936 69 0 0 25 0 1 0 488384324 109907968 24200 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26833 24200 603 41 0 26792 0
vsize: 107332
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 24961 0 0 0 45936 70 0 0 25 0 1 0 488384324 111521792 24591 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27227 24591 603 41 0 27186 0
vsize: 108908
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 25311 0 0 0 46934 71 0 0 25 0 1 0 488384324 112873472 24941 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27557 24941 603 41 0 27516 0
vsize: 110228
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 25711 0 0 0 47933 72 0 0 25 0 1 0 488384324 114614272 25341 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27982 25342 603 41 0 27941 0
vsize: 111928
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 26113 0 0 0 48932 74 0 0 25 0 1 0 488384324 116224000 25743 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28375 25743 603 41 0 28334 0
vsize: 113500
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 26412 0 0 0 49932 74 0 0 25 0 1 0 488384324 117432320 26042 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28670 26042 603 41 0 28629 0
vsize: 114680
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 26722 0 0 0 50931 75 0 0 25 0 1 0 488384324 118632448 26352 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28963 26352 603 41 0 28922 0
vsize: 115852
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 27162 0 0 0 51930 76 0 0 25 0 1 0 488384324 120512512 26792 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29422 26792 603 41 0 29381 0
vsize: 117688
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 27539 0 0 0 52929 77 0 0 25 0 1 0 488384324 121991168 27169 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29783 27169 603 41 0 29742 0
vsize: 119132
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 27860 0 0 0 53928 78 0 0 25 0 1 0 488384324 123334656 27490 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30111 27490 603 41 0 30070 0
vsize: 120444
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 28292 0 0 0 54927 80 0 0 25 0 1 0 488384324 125112320 27922 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30545 27922 603 41 0 30504 0
vsize: 122180
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 28755 0 0 0 55926 81 0 0 25 0 1 0 488384324 127021056 28385 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31011 28385 603 41 0 30970 0
vsize: 124044
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 29181 0 0 0 56925 82 0 0 25 0 1 0 488384324 128741376 28811 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31431 28811 603 41 0 31390 0
vsize: 125724
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 29598 0 0 0 57924 83 0 0 25 0 1 0 488384324 130486272 29228 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31857 29228 603 41 0 31816 0
vsize: 127428
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 29930 0 0 0 58923 85 0 0 25 0 1 0 488384324 131837952 29560 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32187 29560 603 41 0 32146 0
vsize: 128748
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 30301 0 0 0 59922 85 0 0 25 0 1 0 488384324 133337088 29931 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32553 29931 603 41 0 32512 0
vsize: 130212
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 30757 0 0 0 60922 86 0 0 25 0 1 0 488384324 135229440 30387 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33015 30387 603 41 0 32974 0
vsize: 132060
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 31127 0 0 0 61921 86 0 0 25 0 1 0 488384324 136704000 30757 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33375 30757 603 41 0 33334 0
vsize: 133500
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 31517 0 0 0 62920 88 0 0 25 0 1 0 488384324 138313728 31147 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33768 31147 603 41 0 33727 0
vsize: 135072
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 31886 0 0 0 63920 88 0 0 25 0 1 0 488384324 139776000 31516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34125 31516 603 41 0 34084 0
vsize: 136500
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 32101 0 0 0 64919 89 0 0 25 0 1 0 488384324 140718080 31731 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34355 31731 603 41 0 34314 0
vsize: 137420
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 32429 0 0 0 65919 90 0 0 25 0 1 0 488384324 142069760 32059 4294967295 134512640 134672761 3221224624 3221223808 134558771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34685 32059 603 41 0 34644 0
vsize: 138740
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 32769 0 0 0 66918 91 0 0 25 0 1 0 488384324 143400960 32399 4294967295 134512640 134672761 3221224624 3221223808 134558632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35010 32399 603 41 0 34969 0
vsize: 140040
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 33180 0 0 0 67917 92 0 0 25 0 1 0 488384324 145141760 32810 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35435 32810 603 41 0 35394 0
vsize: 141740
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 33536 0 0 0 68916 93 0 0 25 0 1 0 488384324 146620416 33166 4294967295 134512640 134672761 3221224624 3221223788 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35796 33166 603 41 0 35755 0
vsize: 143184
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 33921 0 0 0 69915 94 0 0 25 0 1 0 488384324 148099072 33551 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36157 33551 603 41 0 36116 0
vsize: 144628
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 34249 0 0 0 70915 95 0 0 25 0 1 0 488384324 149450752 33879 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36487 33879 603 41 0 36446 0
vsize: 145948
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 34591 0 0 0 71914 96 0 0 25 0 1 0 488384324 150937600 34221 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36850 34221 603 41 0 36809 0
vsize: 147400
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 34916 0 0 0 72913 97 0 0 25 0 1 0 488384324 152289280 34546 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37180 34546 603 41 0 37139 0
vsize: 148720
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 35215 0 0 0 73913 97 0 0 25 0 1 0 488384324 153497600 34845 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37475 34845 603 41 0 37434 0
vsize: 149900
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 35649 0 0 0 74912 99 0 0 25 0 1 0 488384324 155230208 35279 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37898 35279 603 41 0 37857 0
vsize: 151592
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 35948 0 0 0 75911 99 0 0 25 0 1 0 488384324 156438528 35578 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38193 35578 603 41 0 38152 0
vsize: 152772
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 36288 0 0 0 76910 100 0 0 25 0 1 0 488384324 157786112 35918 4294967295 134512640 134672761 3221224624 3221223808 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38522 35919 603 41 0 38481 0
vsize: 154088
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 36541 0 0 0 77910 101 0 0 25 0 1 0 488384324 158859264 36171 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 36171 603 41 0 38743 0
vsize: 155136
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 36862 0 0 0 78909 102 0 0 25 0 1 0 488384324 160194560 36492 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39110 36492 603 41 0 39069 0
vsize: 156440
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 37143 0 0 0 79908 103 0 0 25 0 1 0 488384324 161263616 36773 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39371 36773 603 41 0 39330 0
vsize: 157484
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 37440 0 0 0 80907 104 0 0 25 0 1 0 488384324 162471936 37070 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39666 37070 603 41 0 39625 0
vsize: 158664
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 37695 0 0 0 81907 105 0 0 25 0 1 0 488384324 163553280 37325 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39930 37325 603 41 0 39889 0
vsize: 159720
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 37894 0 0 0 82907 105 0 0 25 0 1 0 488384324 164364288 37524 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40128 37524 603 41 0 40087 0
vsize: 160512
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 38160 0 0 0 83907 105 0 0 25 0 1 0 488384324 165445632 37790 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40392 37790 603 41 0 40351 0
vsize: 161568
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 38455 0 0 0 84906 106 0 0 25 0 1 0 488384324 166662144 38085 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40689 38085 603 41 0 40648 0
vsize: 162756
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 38790 0 0 0 85906 107 0 0 25 0 1 0 488384324 168009728 38420 4294967295 134512640 134672761 3221224624 3221223792 134559131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41018 38420 603 41 0 40977 0
vsize: 164072
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 39122 0 0 0 86905 108 0 0 25 0 1 0 488384324 169349120 38752 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41345 38752 603 41 0 41304 0
vsize: 165380
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 39355 0 0 0 87904 109 0 0 25 0 1 0 488384324 170299392 38985 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41577 38985 603 41 0 41536 0
vsize: 166308
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 39671 0 0 0 88904 110 0 0 25 0 1 0 488384324 171634688 39301 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41903 39301 603 41 0 41862 0
vsize: 167612
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 39953 0 0 0 89903 110 0 0 25 0 1 0 488384324 172851200 39583 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42200 39583 603 41 0 42159 0
vsize: 168800
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 40246 0 0 0 90903 111 0 0 25 0 1 0 488384324 174063616 39876 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42496 39876 603 41 0 42455 0
vsize: 169984
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 40563 0 0 0 91902 112 0 0 25 0 1 0 488384324 175280128 40193 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42793 40193 603 41 0 42752 0
vsize: 171172
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 40827 0 0 0 92901 113 0 0 25 0 1 0 488384324 176357376 40457 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43056 40457 603 41 0 43015 0
vsize: 172224
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 41038 0 0 0 93900 115 0 0 25 0 1 0 488384324 177168384 40668 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43254 40668 603 41 0 43213 0
vsize: 173016
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 41323 0 0 0 94899 116 0 0 25 0 1 0 488384324 178380800 40953 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43550 40953 603 41 0 43509 0
vsize: 174200
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 41605 0 0 0 95899 116 0 0 25 0 1 0 488384324 179597312 41235 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43847 41235 603 41 0 43806 0
vsize: 175388
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 41908 0 0 0 96898 117 0 0 25 0 1 0 488384324 180789248 41538 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44138 41538 603 41 0 44097 0
vsize: 176552
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 42252 0 0 0 97897 118 0 0 25 0 1 0 488384324 182128640 41882 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44465 41882 603 41 0 44424 0
vsize: 177860
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 42543 0 0 0 98897 118 0 0 25 0 1 0 488384324 183848960 42173 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44885 42173 603 41 0 44844 0
vsize: 179540
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 42832 0 0 0 99896 119 0 0 25 0 1 0 488384324 185053184 42462 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45179 42462 603 41 0 45138 0
vsize: 180716
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 42981 0 0 0 100896 119 0 0 25 0 1 0 488384324 185724928 42611 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45343 42611 603 41 0 45302 0
vsize: 181372
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 43195 0 0 0 101895 120 0 0 25 0 1 0 488384324 186527744 42825 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45539 42825 603 41 0 45498 0
vsize: 182156
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 43516 0 0 0 102895 121 0 0 25 0 1 0 488384324 187883520 43146 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45870 43146 603 41 0 45829 0
vsize: 183480
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 43898 0 0 0 103895 122 0 0 25 0 1 0 488384324 189497344 43528 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46264 43528 603 41 0 46223 0
vsize: 185056
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20873
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 44196 0 0 0 104894 122 0 0 25 0 1 0 488384324 190701568 43826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46558 43826 603 41 0 46517 0
vsize: 186232
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 44466 0 0 0 105892 125 0 0 25 0 1 0 488384324 191778816 44096 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46821 44096 603 41 0 46780 0
vsize: 187284
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 44793 0 0 0 106890 126 0 0 25 0 1 0 488384324 193122304 44423 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47149 44423 603 41 0 47108 0
vsize: 188596
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 45304 0 0 0 107889 128 0 0 25 0 1 0 488384324 195162112 44934 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47647 44934 603 41 0 47606 0
vsize: 190588
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 45631 0 0 0 108889 128 0 0 25 0 1 0 488384324 196509696 45261 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47976 45261 603 41 0 47935 0
vsize: 191904
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 45840 0 0 0 109888 129 0 0 25 0 1 0 488384324 197312512 45470 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48172 45470 603 41 0 48131 0
vsize: 192688
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 46073 0 0 0 110888 130 0 0 25 0 1 0 488384324 198246400 45703 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48400 45703 603 41 0 48359 0
vsize: 193600
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 46423 0 0 0 111887 131 0 0 25 0 1 0 488384324 199712768 46053 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48758 46053 603 41 0 48717 0
vsize: 195032
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20926
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 46814 0 0 0 112885 132 0 0 25 0 1 0 488384324 201322496 46444 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49151 46444 603 41 0 49110 0
vsize: 196604
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20928
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 46970 0 0 0 113885 132 0 0 25 0 1 0 488384324 201986048 46600 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49313 46600 603 41 0 49272 0
vsize: 197252
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20928
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 47200 0 0 0 114885 133 0 0 25 0 1 0 488384324 202932224 46830 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49544 46830 603 41 0 49503 0
vsize: 198176
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20928
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 47456 0 0 0 115884 134 0 0 25 0 1 0 488384324 204001280 47086 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49805 47086 603 41 0 49764 0
vsize: 199220
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20928
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 47713 0 0 0 116884 134 0 0 25 0 1 0 488384324 205082624 47343 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50069 47343 603 41 0 50028 0
vsize: 200276
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20928
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 47985 0 0 0 117884 135 0 0 25 0 1 0 488384324 206151680 47615 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50330 47615 603 41 0 50289 0
vsize: 201320
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20928
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 48130 0 0 0 118884 135 0 0 25 0 1 0 488384324 206692352 47760 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50462 47760 603 41 0 50421 0
vsize: 201848
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20928
Raw data (stat): 20873 (minisat+) R 20872 30854 30853 0 -1 0 48425 0 0 0 119884 135 0 0 25 0 1 0 488384324 207896576 48055 4294967295 134512640 134672761 3221224624 3221223728 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50756 48055 603 41 0 50715 0
vsize: 203024
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 20928
Raw data (stat): 20873 (minisat+) Z 20872 30854 30853 0 -1 12 48427 0 0 0 119884 144 0 0 25 0 1 0 488384324 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.13
CPU time (s): 1200.29
CPU user time (s): 1198.85
CPU system time (s): 1.44478
CPU usage (%): 100.013
Max. virtual memory (Kb): 203024
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####