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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-air06.opb
MD5SUMf85d0079133f298b06c25764b03ff228
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 70057
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 numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.67
Number of variables8627
Total number of constraints9452
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)9452
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint461

Trace number 2685

Launcher Data

LAUNCH ON wulflinc8 THE 2005-09-18 20:41:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2843 boxname=wulflinc8 idbench=499 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f85d0079133f298b06c25764b03ff228  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-air06.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-air06.opb
IDLAUNCH: 2843
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        913964 kB
Buffers:         34992 kB
Cached:          60708 kB
SwapCached:        792 kB
Active:          69848 kB
Inactive:        28468 kB
HighTotal:      131008 kB
HighFree:        66472 kB
LowTotal:       903652 kB
LowFree:        847492 kB
SwapTotal:     2097136 kB
SwapFree:      2095876 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5752 kB
Slab:            16556 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 21:01:23 (client local time) WITH STATUS 0 IN 1207.04 SECONDS
stats: 2843 7 1207.04 0

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 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/7878/stat): 7878 (minisat+_script) R 7877 7878 27660 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1772420436 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7878/statm): 174 3 169 147 0 27 0
[pid=7878] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=7879
New process pid=7880
New process pid=7881
execve syscall for /bin/sed executable
One traced child (pid=7880) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=7881) exited with status: 0
One traced child (pid=7879) exited with status: 0
New process pid=7882
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-air06.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.96 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 10543 0 0 0 906 44 0 0 25 0 1 0 1772420441 43544576 10155 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 10631 10155 145 145 0 10486 0
[pid=7882] vsize: 42524
Current children cumulated CPU time (s) 9.52
Current children cumulated vsize (Kb) 44648

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 10696 0 0 0 1903 45 0 0 25 0 1 0 1772420441 44130304 10308 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 10774 10308 145 145 0 10629 0
[pid=7882] vsize: 43096
Current children cumulated CPU time (s) 19.5
Current children cumulated vsize (Kb) 45220

[startup+30.0072 s]
Raw data (loadavg): 0.95 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 10880 0 0 0 2899 47 0 0 25 0 1 0 1772420441 44892160 10492 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 10960 10492 145 145 0 10815 0
[pid=7882] vsize: 43840
Current children cumulated CPU time (s) 29.48
Current children cumulated vsize (Kb) 45964

[startup+40.008 s]
Raw data (loadavg): 0.95 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 11032 0 0 0 3896 49 0 0 25 0 1 0 1772420441 45506560 10644 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 11110 10644 145 145 0 10965 0
[pid=7882] vsize: 44440
Current children cumulated CPU time (s) 39.47
Current children cumulated vsize (Kb) 46564

[startup+50.0087 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 11191 0 0 0 4893 50 0 0 25 0 1 0 1772420441 46157824 10803 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 11269 10803 145 145 0 11124 0
[pid=7882] vsize: 45076
Current children cumulated CPU time (s) 49.45
Current children cumulated vsize (Kb) 47200

[startup+60.0095 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 11390 0 0 0 5889 52 0 0 25 0 1 0 1772420441 46997504 11002 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 11474 11002 145 145 0 11329 0
[pid=7882] vsize: 45896
Current children cumulated CPU time (s) 59.43
Current children cumulated vsize (Kb) 48020

[startup+70.0103 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 11579 0 0 0 6885 54 0 0 25 0 1 0 1772420441 47693824 11191 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 11644 11191 145 145 0 11499 0
[pid=7882] vsize: 46576
Current children cumulated CPU time (s) 69.41
Current children cumulated vsize (Kb) 48700

[startup+80.0111 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 11750 0 0 0 7882 55 0 0 25 0 1 0 1772420441 48390144 11362 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 11814 11362 145 145 0 11669 0
[pid=7882] vsize: 47256
Current children cumulated CPU time (s) 79.39
Current children cumulated vsize (Kb) 49380

[startup+90.0119 s]
Raw data (loadavg): 0.98 0.97 0.96 1/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) T 7878 7878 27660 0 -1 0 11940 0 0 0 8877 57 0 0 25 0 1 0 1772420441 49164288 11552 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7882/statm): 12003 11552 145 145 0 11858 0
[pid=7882] vsize: 48012
Current children cumulated CPU time (s) 89.36
Current children cumulated vsize (Kb) 50136

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 12117 0 0 0 9874 58 0 0 25 0 1 0 1772420441 49881088 11729 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 12178 11729 145 145 0 12033 0
[pid=7882] vsize: 48712
Current children cumulated CPU time (s) 99.34
Current children cumulated vsize (Kb) 50836

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 12268 0 0 0 10872 59 0 0 25 0 1 0 1772420441 50556928 11880 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 12343 11880 145 145 0 12198 0
[pid=7882] vsize: 49372
Current children cumulated CPU time (s) 109.33
Current children cumulated vsize (Kb) 51496

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 12429 0 0 0 11869 61 0 0 25 0 1 0 1772420441 51212288 12041 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 12503 12041 145 145 0 12358 0
[pid=7882] vsize: 50012
Current children cumulated CPU time (s) 119.32
Current children cumulated vsize (Kb) 52136

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 12607 0 0 0 12866 62 0 0 25 0 1 0 1772420441 51937280 12219 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 12680 12219 145 145 0 12535 0
[pid=7882] vsize: 50720
Current children cumulated CPU time (s) 129.3
Current children cumulated vsize (Kb) 52844

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 12774 0 0 0 13863 63 0 0 25 0 1 0 1772420441 52613120 12386 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 12845 12386 145 145 0 12700 0
[pid=7882] vsize: 51380
Current children cumulated CPU time (s) 139.28
Current children cumulated vsize (Kb) 53504

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 12947 0 0 0 14860 64 0 0 25 0 1 0 1772420441 53317632 12559 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 13017 12559 145 145 0 12872 0
[pid=7882] vsize: 52068
Current children cumulated CPU time (s) 149.26
Current children cumulated vsize (Kb) 54192

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 13149 0 0 0 15857 65 0 0 25 0 1 0 1772420441 54140928 12761 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 13218 12761 145 145 0 13073 0
[pid=7882] vsize: 52872
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 54996

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 13366 0 0 0 16853 68 0 0 25 0 1 0 1772420441 55021568 12978 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 13433 12978 145 145 0 13288 0
[pid=7882] vsize: 53732
Current children cumulated CPU time (s) 169.23
Current children cumulated vsize (Kb) 55856

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 13668 0 0 0 17847 71 0 0 25 0 1 0 1772420441 56254464 13280 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 13734 13280 145 145 0 13589 0
[pid=7882] vsize: 54936
Current children cumulated CPU time (s) 179.2
Current children cumulated vsize (Kb) 57060

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 13845 0 0 0 18844 73 0 0 25 0 1 0 1772420441 56975360 13457 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 13910 13457 145 145 0 13765 0
[pid=7882] vsize: 55640
Current children cumulated CPU time (s) 189.19
Current children cumulated vsize (Kb) 57764

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 14020 0 0 0 19841 73 0 0 25 0 1 0 1772420441 57683968 13632 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 14083 13632 145 145 0 13938 0
[pid=7882] vsize: 56332
Current children cumulated CPU time (s) 199.16
Current children cumulated vsize (Kb) 58456

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 14260 0 0 0 20837 75 0 0 25 0 1 0 1772420441 58662912 13872 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 14322 13872 145 145 0 14177 0
[pid=7882] vsize: 57288
Current children cumulated CPU time (s) 209.14
Current children cumulated vsize (Kb) 59412

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 14445 0 0 0 21834 77 0 0 25 0 1 0 1772420441 59416576 14057 4294967295 134512640 135094434 3221224432 3221223024 134556937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 14506 14057 145 145 0 14361 0
[pid=7882] vsize: 58024
Current children cumulated CPU time (s) 219.13
Current children cumulated vsize (Kb) 60148

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 14647 0 0 0 22830 79 0 0 25 0 1 0 1772420441 60370944 14259 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 14739 14259 145 145 0 14594 0
[pid=7882] vsize: 58956
Current children cumulated CPU time (s) 229.11
Current children cumulated vsize (Kb) 61080

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 14810 0 0 0 23827 80 0 0 25 0 1 0 1772420441 61034496 14422 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 14901 14422 145 145 0 14756 0
[pid=7882] vsize: 59604
Current children cumulated CPU time (s) 239.09
Current children cumulated vsize (Kb) 61728

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 15067 0 0 0 24822 83 0 0 25 0 1 0 1772420441 62078976 14679 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 15156 14679 145 145 0 15011 0
[pid=7882] vsize: 60624
Current children cumulated CPU time (s) 249.07
Current children cumulated vsize (Kb) 62748

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 15406 0 0 0 25817 86 0 0 25 0 1 0 1772420441 63471616 15018 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 15496 15018 145 145 0 15351 0
[pid=7882] vsize: 61984
Current children cumulated CPU time (s) 259.05
Current children cumulated vsize (Kb) 64108

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 15572 0 0 0 26814 87 0 0 25 0 1 0 1772420441 64147456 15184 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 15661 15184 145 145 0 15516 0
[pid=7882] vsize: 62644
Current children cumulated CPU time (s) 269.03
Current children cumulated vsize (Kb) 64768

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 15805 0 0 0 27810 89 0 0 25 0 1 0 1772420441 65089536 15417 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 15891 15417 145 145 0 15746 0
[pid=7882] vsize: 63564
Current children cumulated CPU time (s) 279.01
Current children cumulated vsize (Kb) 65688

[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 15981 0 0 0 28807 90 0 0 25 0 1 0 1772420441 65806336 15593 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 16066 15593 145 145 0 15921 0
[pid=7882] vsize: 64264
Current children cumulated CPU time (s) 288.99
Current children cumulated vsize (Kb) 66388

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 16210 0 0 0 29802 92 0 0 25 0 1 0 1772420441 66740224 15822 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 16294 15822 145 145 0 16149 0
[pid=7882] vsize: 65176
Current children cumulated CPU time (s) 298.96
Current children cumulated vsize (Kb) 67300

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 16431 0 0 0 30799 93 0 0 25 0 1 0 1772420441 67641344 16043 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 16514 16043 145 145 0 16369 0
[pid=7882] vsize: 66056
Current children cumulated CPU time (s) 308.94
Current children cumulated vsize (Kb) 68180

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 16727 0 0 0 31794 96 0 0 25 0 1 0 1772420441 68849664 16339 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 16809 16339 145 145 0 16664 0
[pid=7882] vsize: 67236
Current children cumulated CPU time (s) 318.92
Current children cumulated vsize (Kb) 69360

[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 16984 0 0 0 32789 98 0 0 25 0 1 0 1772420441 69898240 16596 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 17065 16596 145 145 0 16920 0
[pid=7882] vsize: 68260
Current children cumulated CPU time (s) 328.89
Current children cumulated vsize (Kb) 70384

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 17250 0 0 0 33783 100 0 0 25 0 1 0 1772420441 70983680 16862 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 17330 16862 145 145 0 17185 0
[pid=7882] vsize: 69320
Current children cumulated CPU time (s) 338.85
Current children cumulated vsize (Kb) 71444

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 17484 0 0 0 34780 102 0 0 25 0 1 0 1772420441 71938048 17096 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 17563 17096 145 145 0 17418 0
[pid=7882] vsize: 70252
Current children cumulated CPU time (s) 348.84
Current children cumulated vsize (Kb) 72376

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 17749 0 0 0 35774 104 0 0 25 0 1 0 1772420441 73015296 17361 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 17826 17361 145 145 0 17681 0
[pid=7882] vsize: 71304
Current children cumulated CPU time (s) 358.8
Current children cumulated vsize (Kb) 73428

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 17949 0 0 0 36770 105 0 0 25 0 1 0 1772420441 73830400 17561 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 18025 17561 145 145 0 17880 0
[pid=7882] vsize: 72100
Current children cumulated CPU time (s) 368.77
Current children cumulated vsize (Kb) 74224

[startup+380.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 18139 0 0 0 37767 107 0 0 25 0 1 0 1772420441 74604544 17751 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 18214 17751 145 145 0 18069 0
[pid=7882] vsize: 72856
Current children cumulated CPU time (s) 378.76
Current children cumulated vsize (Kb) 74980

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 18490 0 0 0 38762 110 0 0 25 0 1 0 1772420441 76038144 18102 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 18564 18102 145 145 0 18419 0
[pid=7882] vsize: 74256
Current children cumulated CPU time (s) 388.74
Current children cumulated vsize (Kb) 76380

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 18791 0 0 0 39756 113 0 0 25 0 1 0 1772420441 77266944 18403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 18864 18403 145 145 0 18719 0
[pid=7882] vsize: 75456
Current children cumulated CPU time (s) 398.71
Current children cumulated vsize (Kb) 77580

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 19041 0 0 0 40751 115 0 0 25 0 1 0 1772420441 78286848 18653 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 19113 18653 145 145 0 18968 0
[pid=7882] vsize: 76452
Current children cumulated CPU time (s) 408.68
Current children cumulated vsize (Kb) 78576

[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 19256 0 0 0 41747 117 0 0 25 0 1 0 1772420441 79167488 18868 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 19328 18868 145 145 0 19183 0
[pid=7882] vsize: 77312
Current children cumulated CPU time (s) 418.66
Current children cumulated vsize (Kb) 79436

[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 19471 0 0 0 42743 119 0 0 25 0 1 0 1772420441 80039936 19083 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 19541 19083 145 145 0 19396 0
[pid=7882] vsize: 78164
Current children cumulated CPU time (s) 428.64
Current children cumulated vsize (Kb) 80288

[startup+440.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 19692 0 0 0 43739 121 0 0 25 0 1 0 1772420441 80945152 19304 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 19762 19304 145 145 0 19617 0
[pid=7882] vsize: 79048
Current children cumulated CPU time (s) 438.62
Current children cumulated vsize (Kb) 81172

[startup+450.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 20003 0 0 0 44733 124 0 0 25 0 1 0 1772420441 82214912 19615 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 20072 19615 145 145 0 19927 0
[pid=7882] vsize: 80288
Current children cumulated CPU time (s) 448.59
Current children cumulated vsize (Kb) 82412

[startup+460.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 20311 0 0 0 45728 128 0 0 25 0 1 0 1772420441 83472384 19923 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 20379 19923 145 145 0 20234 0
[pid=7882] vsize: 81516
Current children cumulated CPU time (s) 458.58
Current children cumulated vsize (Kb) 83640

[startup+470.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 20577 0 0 0 46724 129 0 0 25 0 1 0 1772420441 84557824 20189 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 20644 20189 145 145 0 20499 0
[pid=7882] vsize: 82576
Current children cumulated CPU time (s) 468.55
Current children cumulated vsize (Kb) 84700

[startup+480.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 20814 0 0 0 47720 131 0 0 25 0 1 0 1772420441 85524480 20426 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 20880 20426 145 145 0 20735 0
[pid=7882] vsize: 83520
Current children cumulated CPU time (s) 478.53
Current children cumulated vsize (Kb) 85644

[startup+490.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 21042 0 0 0 48716 133 0 0 25 0 1 0 1772420441 86454272 20654 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 21107 20654 145 145 0 20962 0
[pid=7882] vsize: 84428
Current children cumulated CPU time (s) 488.51
Current children cumulated vsize (Kb) 86552

[startup+500.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 21287 0 0 0 49711 135 0 0 25 0 1 0 1772420441 87453696 20899 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 21351 20899 145 145 0 21206 0
[pid=7882] vsize: 85404
Current children cumulated CPU time (s) 498.48
Current children cumulated vsize (Kb) 87528

[startup+510.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) T 7878 7878 27660 0 -1 0 21524 0 0 0 50705 137 0 0 25 0 1 0 1772420441 88420352 21136 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7882/statm): 21587 21136 145 145 0 21442 0
[pid=7882] vsize: 86348
Current children cumulated CPU time (s) 508.44
Current children cumulated vsize (Kb) 88472

[startup+520.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 21793 0 0 0 51701 139 0 0 25 0 1 0 1772420441 89518080 21405 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 21855 21405 145 145 0 21710 0
[pid=7882] vsize: 87420
Current children cumulated CPU time (s) 518.42
Current children cumulated vsize (Kb) 89544

[startup+530.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 21948 0 0 0 52698 140 0 0 25 0 1 0 1772420441 90148864 21560 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 22009 21560 145 145 0 21864 0
[pid=7882] vsize: 88036
Current children cumulated CPU time (s) 528.4
Current children cumulated vsize (Kb) 90160

[startup+540.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 22208 0 0 0 53694 141 0 0 25 0 1 0 1772420441 91471872 21820 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 22332 21820 145 145 0 22187 0
[pid=7882] vsize: 89328
Current children cumulated CPU time (s) 538.37
Current children cumulated vsize (Kb) 91452

[startup+550.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 22387 0 0 0 54691 143 0 0 25 0 1 0 1772420441 92205056 21999 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 22511 21999 145 145 0 22366 0
[pid=7882] vsize: 90044
Current children cumulated CPU time (s) 548.36
Current children cumulated vsize (Kb) 92168

[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 22635 0 0 0 55687 144 0 0 25 0 1 0 1772420441 93212672 22247 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 22757 22247 145 145 0 22612 0
[pid=7882] vsize: 91028
Current children cumulated CPU time (s) 558.33
Current children cumulated vsize (Kb) 93152

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 22944 0 0 0 56682 146 0 0 25 0 1 0 1772420441 94478336 22556 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 23066 22556 145 145 0 22921 0
[pid=7882] vsize: 92264
Current children cumulated CPU time (s) 568.3
Current children cumulated vsize (Kb) 94388

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 23213 0 0 0 57678 148 0 0 25 0 1 0 1772420441 95576064 22825 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 23334 22825 145 145 0 23189 0
[pid=7882] vsize: 93336
Current children cumulated CPU time (s) 578.28
Current children cumulated vsize (Kb) 95460

[startup+590.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 23432 0 0 0 58676 149 0 0 25 0 1 0 1772420441 96468992 23044 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 23552 23044 145 145 0 23407 0
[pid=7882] vsize: 94208
Current children cumulated CPU time (s) 588.27
Current children cumulated vsize (Kb) 96332

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 23742 0 0 0 59672 151 0 0 25 0 1 0 1772420441 97734656 23354 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 23861 23354 145 145 0 23716 0
[pid=7882] vsize: 95444
Current children cumulated CPU time (s) 598.25
Current children cumulated vsize (Kb) 97568

[startup+610.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 24004 0 0 0 60668 152 0 0 25 0 1 0 1772420441 98828288 23616 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 24128 23616 145 145 0 23983 0
[pid=7882] vsize: 96512
Current children cumulated CPU time (s) 608.22
Current children cumulated vsize (Kb) 98636

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 24285 0 0 0 61664 154 0 0 25 0 1 0 1772420441 99975168 23897 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 24408 23897 145 145 0 24263 0
[pid=7882] vsize: 97632
Current children cumulated CPU time (s) 618.2
Current children cumulated vsize (Kb) 99756

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 24603 0 0 0 62659 156 0 0 25 0 1 0 1772420441 101253120 24215 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 24720 24215 145 145 0 24575 0
[pid=7882] vsize: 98880
Current children cumulated CPU time (s) 628.17
Current children cumulated vsize (Kb) 101004

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 24929 0 0 0 63654 158 0 0 25 0 1 0 1772420441 102584320 24541 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 25045 24541 145 145 0 24900 0
[pid=7882] vsize: 100180
Current children cumulated CPU time (s) 638.14
Current children cumulated vsize (Kb) 102304

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 25280 0 0 0 64650 159 0 0 25 0 1 0 1772420441 104017920 24892 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 25395 24892 145 145 0 25250 0
[pid=7882] vsize: 101580
Current children cumulated CPU time (s) 648.11
Current children cumulated vsize (Kb) 103704

[startup+660.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 25625 0 0 0 65646 161 0 0 25 0 1 0 1772420441 105426944 25237 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 25739 25237 145 145 0 25594 0
[pid=7882] vsize: 102956
Current children cumulated CPU time (s) 658.09
Current children cumulated vsize (Kb) 105080

[startup+670.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 25969 0 0 0 66641 163 0 0 25 0 1 0 1772420441 106831872 25581 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 26082 25581 145 145 0 25937 0
[pid=7882] vsize: 104328
Current children cumulated CPU time (s) 668.06
Current children cumulated vsize (Kb) 106452

[startup+680.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 26263 0 0 0 67636 165 0 0 25 0 1 0 1772420441 108036096 25875 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 26376 25875 145 145 0 26231 0
[pid=7882] vsize: 105504
Current children cumulated CPU time (s) 678.03
Current children cumulated vsize (Kb) 107628

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 26569 0 0 0 68632 167 0 0 25 0 1 0 1772420441 109285376 26181 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 26681 26181 145 145 0 26536 0
[pid=7882] vsize: 106724
Current children cumulated CPU time (s) 688.01
Current children cumulated vsize (Kb) 108848

[startup+700.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 26880 0 0 0 69629 168 0 0 25 0 1 0 1772420441 110555136 26492 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 26991 26492 145 145 0 26846 0
[pid=7882] vsize: 107964
Current children cumulated CPU time (s) 697.99
Current children cumulated vsize (Kb) 110088

[startup+710.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 27202 0 0 0 70624 170 0 0 25 0 1 0 1772420441 111869952 26814 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 27312 26814 145 145 0 27167 0
[pid=7882] vsize: 109248
Current children cumulated CPU time (s) 707.96
Current children cumulated vsize (Kb) 111372

[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 27430 0 0 0 71620 172 0 0 25 0 1 0 1772420441 112799744 27042 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 27539 27042 145 145 0 27394 0
[pid=7882] vsize: 110156
Current children cumulated CPU time (s) 717.94
Current children cumulated vsize (Kb) 112280

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 27646 0 0 0 72617 173 0 0 25 0 1 0 1772420441 113684480 27258 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 27755 27258 145 145 0 27610 0
[pid=7882] vsize: 111020
Current children cumulated CPU time (s) 727.92
Current children cumulated vsize (Kb) 113144

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 27970 0 0 0 73611 176 0 0 25 0 1 0 1772420441 115007488 27582 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 28078 27582 145 145 0 27933 0
[pid=7882] vsize: 112312
Current children cumulated CPU time (s) 737.89
Current children cumulated vsize (Kb) 114436

[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 28285 0 0 0 74608 178 0 0 25 0 1 0 1772420441 116293632 27897 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 28392 27897 145 145 0 28247 0
[pid=7882] vsize: 113568
Current children cumulated CPU time (s) 747.88
Current children cumulated vsize (Kb) 115692

[startup+760.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 28544 0 0 0 75604 180 0 0 25 0 1 0 1772420441 117354496 28156 4294967295 134512640 135094434 3221224432 3221223024 134557191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 28651 28156 145 145 0 28506 0
[pid=7882] vsize: 114604
Current children cumulated CPU time (s) 757.86
Current children cumulated vsize (Kb) 116728

[startup+770.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 28849 0 0 0 76599 182 0 0 25 0 1 0 1772420441 118599680 28461 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 28955 28461 145 145 0 28810 0
[pid=7882] vsize: 115820
Current children cumulated CPU time (s) 767.83
Current children cumulated vsize (Kb) 117944

[startup+780.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 29076 0 0 0 77596 183 0 0 25 0 1 0 1772420441 119525376 28688 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 29181 28688 145 145 0 29036 0
[pid=7882] vsize: 116724
Current children cumulated CPU time (s) 777.81
Current children cumulated vsize (Kb) 118848

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 29322 0 0 0 78592 185 0 0 25 0 1 0 1772420441 120528896 28934 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 29426 28934 145 145 0 29281 0
[pid=7882] vsize: 117704
Current children cumulated CPU time (s) 787.79
Current children cumulated vsize (Kb) 119828

[startup+800.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 29624 0 0 0 79587 187 0 0 25 0 1 0 1772420441 121761792 29236 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 29727 29236 145 145 0 29582 0
[pid=7882] vsize: 118908
Current children cumulated CPU time (s) 797.76
Current children cumulated vsize (Kb) 121032

[startup+810.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 29930 0 0 0 80584 188 0 0 25 0 1 0 1772420441 123011072 29542 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 30032 29542 145 145 0 29887 0
[pid=7882] vsize: 120128
Current children cumulated CPU time (s) 807.74
Current children cumulated vsize (Kb) 122252

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 30374 0 0 0 81579 190 0 0 25 0 1 0 1772420441 124817408 29986 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 30473 29986 145 145 0 30328 0
[pid=7882] vsize: 121892
Current children cumulated CPU time (s) 817.71
Current children cumulated vsize (Kb) 124016

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 30616 0 0 0 82577 191 0 0 25 0 1 0 1772420441 125800448 30228 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 30713 30228 145 145 0 30568 0
[pid=7882] vsize: 122852
Current children cumulated CPU time (s) 827.7
Current children cumulated vsize (Kb) 124976

[startup+840.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 30856 0 0 0 83575 192 0 0 25 0 1 0 1772420441 126763008 30468 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 30948 30468 145 145 0 30803 0
[pid=7882] vsize: 123792
Current children cumulated CPU time (s) 837.69
Current children cumulated vsize (Kb) 125916

[startup+850.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 31076 0 0 0 84571 193 0 0 25 0 1 0 1772420441 127664128 30688 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 31168 30688 145 145 0 31023 0
[pid=7882] vsize: 124672
Current children cumulated CPU time (s) 847.66
Current children cumulated vsize (Kb) 126796

[startup+860.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 31390 0 0 0 85567 195 0 0 25 0 1 0 1772420441 128950272 31002 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 31482 31002 145 145 0 31337 0
[pid=7882] vsize: 125928
Current children cumulated CPU time (s) 857.64
Current children cumulated vsize (Kb) 128052

[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 31768 0 0 0 86563 197 0 0 25 0 1 0 1772420441 130490368 31380 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 31858 31380 145 145 0 31713 0
[pid=7882] vsize: 127432
Current children cumulated CPU time (s) 867.62
Current children cumulated vsize (Kb) 129556

[startup+880.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 32012 0 0 0 87559 198 0 0 25 0 1 0 1772420441 131485696 31624 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 32101 31624 145 145 0 31956 0
[pid=7882] vsize: 128404
Current children cumulated CPU time (s) 877.59
Current children cumulated vsize (Kb) 130528

[startup+890.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 32308 0 0 0 88556 200 0 0 25 0 1 0 1772420441 132698112 31920 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 32397 31920 145 145 0 32252 0
[pid=7882] vsize: 129588
Current children cumulated CPU time (s) 887.58
Current children cumulated vsize (Kb) 131712

[startup+900.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 32541 0 0 0 89553 200 0 0 25 0 1 0 1772420441 133652480 32153 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 32630 32153 145 145 0 32485 0
[pid=7882] vsize: 130520
Current children cumulated CPU time (s) 897.55
Current children cumulated vsize (Kb) 132644

[startup+910.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 32899 0 0 0 90550 202 0 0 25 0 1 0 1772420441 135114752 32511 4294967295 134512640 135094434 3221224432 3221223024 134557283 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 32987 32511 145 145 0 32842 0
[pid=7882] vsize: 131948
Current children cumulated CPU time (s) 907.54
Current children cumulated vsize (Kb) 134072

[startup+920.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 33095 0 0 0 91547 203 0 0 25 0 1 0 1772420441 135913472 32707 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 33182 32707 145 145 0 33037 0
[pid=7882] vsize: 132728
Current children cumulated CPU time (s) 917.52
Current children cumulated vsize (Kb) 134852

[startup+930.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 33317 0 0 0 92546 204 0 0 25 0 1 0 1772420441 136822784 32929 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 33404 32929 145 145 0 33259 0
[pid=7882] vsize: 133616
Current children cumulated CPU time (s) 927.52
Current children cumulated vsize (Kb) 135740

[startup+940.086 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 33549 0 0 0 93541 206 0 0 25 0 1 0 1772420441 137768960 33161 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 33635 33161 145 145 0 33490 0
[pid=7882] vsize: 134540
Current children cumulated CPU time (s) 937.49
Current children cumulated vsize (Kb) 136664

[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 33909 0 0 0 94536 208 0 0 25 0 1 0 1772420441 139231232 33521 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 33992 33521 145 145 0 33847 0
[pid=7882] vsize: 135968
Current children cumulated CPU time (s) 947.46
Current children cumulated vsize (Kb) 138092

[startup+960.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 34232 0 0 0 95531 211 0 0 25 0 1 0 1772420441 140550144 33844 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 34314 33844 145 145 0 34169 0
[pid=7882] vsize: 137256
Current children cumulated CPU time (s) 957.44
Current children cumulated vsize (Kb) 139380

[startup+970.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 34566 0 0 0 96527 213 0 0 25 0 1 0 1772420441 141905920 34178 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 34645 34178 145 145 0 34500 0
[pid=7882] vsize: 138580
Current children cumulated CPU time (s) 967.42
Current children cumulated vsize (Kb) 140704

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 34991 0 0 0 97522 216 0 0 25 0 1 0 1772420441 143646720 34603 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 35070 34603 145 145 0 34925 0
[pid=7882] vsize: 140280
Current children cumulated CPU time (s) 977.4
Current children cumulated vsize (Kb) 142404

[startup+990.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 35312 0 0 0 98517 218 0 0 25 0 1 0 1772420441 144957440 34924 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 35390 34924 145 145 0 35245 0
[pid=7882] vsize: 141560
Current children cumulated CPU time (s) 987.37
Current children cumulated vsize (Kb) 143684

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 35542 0 0 0 99511 221 0 0 25 0 1 0 1772420441 145895424 35154 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 35619 35154 145 145 0 35474 0
[pid=7882] vsize: 142476
Current children cumulated CPU time (s) 997.34
Current children cumulated vsize (Kb) 144600

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 35774 0 0 0 100506 224 0 0 25 0 1 0 1772420441 146845696 35386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7882/statm): 35851 35386 145 145 0 35706 0
[pid=7882] vsize: 143404
Current children cumulated CPU time (s) 1007.32
Current children cumulated vsize (Kb) 145528

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 35927 0 0 0 101503 226 0 0 25 0 1 0 1772420441 147472384 35539 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 36004 35539 145 145 0 35859 0
[pid=7882] vsize: 144016
Current children cumulated CPU time (s) 1017.31
Current children cumulated vsize (Kb) 146140

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 36132 0 0 0 102501 227 0 0 25 0 1 0 1772420441 148307968 35744 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 36208 35744 145 145 0 36063 0
[pid=7882] vsize: 144832
Current children cumulated CPU time (s) 1027.3
Current children cumulated vsize (Kb) 146956

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 36345 0 0 0 103498 228 0 0 25 0 1 0 1772420441 149176320 35957 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 36420 35957 145 145 0 36275 0
[pid=7882] vsize: 145680
Current children cumulated CPU time (s) 1037.28
Current children cumulated vsize (Kb) 147804

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 36678 0 0 0 104494 230 0 0 25 0 1 0 1772420441 150540288 36290 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 36753 36290 145 145 0 36608 0
[pid=7882] vsize: 147012
Current children cumulated CPU time (s) 1047.26
Current children cumulated vsize (Kb) 149136

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 36942 0 0 0 105490 232 0 0 25 0 1 0 1772420441 151568384 36554 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 37004 36554 145 145 0 36859 0
[pid=7882] vsize: 148016
Current children cumulated CPU time (s) 1057.24
Current children cumulated vsize (Kb) 150140

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 37154 0 0 0 106487 233 0 0 25 0 1 0 1772420441 152432640 36766 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 37215 36766 145 145 0 37070 0
[pid=7882] vsize: 148860
Current children cumulated CPU time (s) 1067.22
Current children cumulated vsize (Kb) 150984

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 37392 0 0 0 107483 236 0 0 25 0 1 0 1772420441 153407488 37004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 37453 37004 145 145 0 37308 0
[pid=7882] vsize: 149812
Current children cumulated CPU time (s) 1077.21
Current children cumulated vsize (Kb) 151936

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 37675 0 0 0 108479 238 0 0 25 0 1 0 1772420441 154562560 37287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 37735 37287 145 145 0 37590 0
[pid=7882] vsize: 150940
Current children cumulated CPU time (s) 1087.19
Current children cumulated vsize (Kb) 153064

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 37947 0 0 0 109475 240 0 0 25 0 1 0 1772420441 155672576 37559 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 38006 37559 145 145 0 37861 0
[pid=7882] vsize: 152024
Current children cumulated CPU time (s) 1097.17
Current children cumulated vsize (Kb) 154148

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 38172 0 0 0 110472 242 0 0 25 0 1 0 1772420441 156594176 37784 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 38231 37784 145 145 0 38086 0
[pid=7882] vsize: 152924
Current children cumulated CPU time (s) 1107.16
Current children cumulated vsize (Kb) 155048

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 38408 0 0 0 111468 244 0 0 25 0 1 0 1772420441 157560832 38020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 38467 38020 145 145 0 38322 0
[pid=7882] vsize: 153868
Current children cumulated CPU time (s) 1117.14
Current children cumulated vsize (Kb) 155992

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 38760 0 0 0 112465 245 0 0 25 0 1 0 1772420441 158998528 38372 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 38818 38372 145 145 0 38673 0
[pid=7882] vsize: 155272
Current children cumulated CPU time (s) 1127.12
Current children cumulated vsize (Kb) 157396

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 39052 0 0 0 113461 247 0 0 25 0 1 0 1772420441 160194560 38664 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 39110 38664 145 145 0 38965 0
[pid=7882] vsize: 156440
Current children cumulated CPU time (s) 1137.1
Current children cumulated vsize (Kb) 158564

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 39445 0 0 0 114457 249 0 0 25 0 1 0 1772420441 161800192 39057 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 39502 39057 145 145 0 39357 0
[pid=7882] vsize: 158008
Current children cumulated CPU time (s) 1147.08
Current children cumulated vsize (Kb) 160132

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 39807 0 0 0 115454 250 0 0 25 0 1 0 1772420441 163344384 39419 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 39879 39419 145 145 0 39734 0
[pid=7882] vsize: 159516
Current children cumulated CPU time (s) 1157.06
Current children cumulated vsize (Kb) 161640

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 40036 0 0 0 116450 253 0 0 25 0 1 0 1772420441 164274176 39648 4294967295 134512640 135094434 3221224432 3221223024 134557018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 40106 39648 145 145 0 39961 0
[pid=7882] vsize: 160424
Current children cumulated CPU time (s) 1167.05
Current children cumulated vsize (Kb) 162548

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 40307 0 0 0 117446 254 0 0 25 0 1 0 1772420441 165380096 39919 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 40376 39919 145 145 0 40231 0
[pid=7882] vsize: 161504
Current children cumulated CPU time (s) 1177.02
Current children cumulated vsize (Kb) 163628

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 40525 0 0 0 118443 256 0 0 25 0 1 0 1772420441 166268928 40137 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 40593 40137 145 145 0 40448 0
[pid=7882] vsize: 162372
Current children cumulated CPU time (s) 1187.01
Current children cumulated vsize (Kb) 164496

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 40811 0 0 0 119440 257 0 0 25 0 1 0 1772420441 167440384 40423 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 40879 40423 145 145 0 40734 0
[pid=7882] vsize: 163516
Current children cumulated CPU time (s) 1196.99
Current children cumulated vsize (Kb) 165640

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 40928 0 0 0 120437 258 0 0 25 0 1 0 1772420441 167915520 40540 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 40995 40540 145 145 0 40850 0
[pid=7882] vsize: 163980
Current children cumulated CPU time (s) 1206.97
Current children cumulated vsize (Kb) 166104



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 7882
Raw data (/proc/7878/stat): 7878 (minisat+_script) S 7877 7878 27660 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1772420436 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7878/statm): 531 226 485 147 0 384 0
[pid=7878] vsize: 2124
Raw data (/proc/7882/stat): 7882 (minisat+_64-bit) R 7878 7878 27660 0 -1 0 40928 0 0 0 120437 258 0 0 25 0 1 0 1772420441 167915520 40540 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7882/statm): 40995 40540 145 145 0 40850 0
[pid=7882] vsize: 163980
Current children cumulated CPU time (s) 1206.97
Current children cumulated vsize (Kb) 166104

Sending SIGTERM to -7878
Sleeping 2 seconds
One traced child (pid=7878) ended because it received signal 15 (SIGTERM)
One traced child (pid=7882) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.19
CPU time (s): 1207.04
CPU user time (s): 1204.38
CPU system time (s): 2.66359
CPU usage (%): 99.74
Max. virtual memory (cumulated for all children) (Kb): 166104

Verifier Data

ERROR: no interpretation found !