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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.06
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 6075

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        873880 kB
Buffers:         37076 kB
Cached:          91992 kB
SwapCached:        676 kB
Active:          27124 kB
Inactive:       104404 kB
HighTotal:      131008 kB
HighFree:        39788 kB
LowTotal:       903652 kB
LowFree:        834092 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            23612 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:27:13 (client local time) WITH STATUS 0 IN 1207.2 SECONDS
stats: 3227 7 1207.2 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/4701/stat): 4701 (minisat+_script) R 4700 4701 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855159068 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/4701/statm): 174 3 169 147 0 27 0
[pid=4701] 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=4702
New process pid=4703
New process pid=4704
One traced child (pid=4703) exited with status: 0
execve syscall for /bin/sed executable
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=4704) exited with status: 0
One traced child (pid=4702) exited with status: 0
New process pid=4705
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-air06.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 10543 0 0 0 906 43 0 0 25 0 1 0 1855159073 43544576 10155 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 10631 10155 145 145 0 10486 0
[pid=4705] vsize: 42524
Current children cumulated CPU time (s) 9.49
Current children cumulated vsize (Kb) 44648

[startup+20.005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 10696 0 0 0 1903 45 0 0 25 0 1 0 1855159073 44130304 10308 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 10774 10308 145 145 0 10629 0
[pid=4705] vsize: 43096
Current children cumulated CPU time (s) 19.48
Current children cumulated vsize (Kb) 45220

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 10879 0 0 0 2900 47 0 0 25 0 1 0 1855159073 44888064 10491 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 10959 10491 145 145 0 10814 0
[pid=4705] vsize: 43836
Current children cumulated CPU time (s) 29.47
Current children cumulated vsize (Kb) 45960

[startup+40.0075 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 11030 0 0 0 3896 49 0 0 25 0 1 0 1855159073 45498368 10642 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 11108 10642 145 145 0 10963 0
[pid=4705] vsize: 44432
Current children cumulated CPU time (s) 39.45
Current children cumulated vsize (Kb) 46556

[startup+50.0093 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 11189 0 0 0 4893 51 0 0 25 0 1 0 1855159073 46149632 10801 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 11267 10801 145 145 0 11122 0
[pid=4705] vsize: 45068
Current children cumulated CPU time (s) 49.44
Current children cumulated vsize (Kb) 47192

[startup+60.0101 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 11386 0 0 0 5889 53 0 0 25 0 1 0 1855159073 46981120 10998 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 11470 10998 145 145 0 11325 0
[pid=4705] vsize: 45880
Current children cumulated CPU time (s) 59.42
Current children cumulated vsize (Kb) 48004

[startup+70.0119 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 11579 0 0 0 6885 55 0 0 25 0 1 0 1855159073 47693824 11191 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 11644 11191 145 145 0 11499 0
[pid=4705] vsize: 46576
Current children cumulated CPU time (s) 69.4
Current children cumulated vsize (Kb) 48700

[startup+80.0127 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 11749 0 0 0 7881 56 0 0 25 0 1 0 1855159073 48386048 11361 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 11813 11361 145 145 0 11668 0
[pid=4705] vsize: 47252
Current children cumulated CPU time (s) 79.37
Current children cumulated vsize (Kb) 49376

[startup+90.0135 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 11939 0 0 0 8878 58 0 0 25 0 1 0 1855159073 49156096 11551 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 12001 11551 145 145 0 11856 0
[pid=4705] vsize: 48004
Current children cumulated CPU time (s) 89.36
Current children cumulated vsize (Kb) 50128

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 12111 0 0 0 9875 59 0 0 25 0 1 0 1855159073 49856512 11723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 12172 11723 145 145 0 12027 0
[pid=4705] vsize: 48688
Current children cumulated CPU time (s) 99.34
Current children cumulated vsize (Kb) 50812

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 12268 0 0 0 10871 61 0 0 25 0 1 0 1855159073 50556928 11880 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 12343 11880 145 145 0 12198 0
[pid=4705] vsize: 49372
Current children cumulated CPU time (s) 109.32
Current children cumulated vsize (Kb) 51496

[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 12429 0 0 0 11868 63 0 0 25 0 1 0 1855159073 51212288 12041 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 12503 12041 145 145 0 12358 0
[pid=4705] vsize: 50012
Current children cumulated CPU time (s) 119.31
Current children cumulated vsize (Kb) 52136

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 12608 0 0 0 12864 64 0 0 25 0 1 0 1855159073 51941376 12220 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 12681 12220 145 145 0 12536 0
[pid=4705] vsize: 50724
Current children cumulated CPU time (s) 129.28
Current children cumulated vsize (Kb) 52848

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 12781 0 0 0 13861 66 0 0 25 0 1 0 1855159073 52641792 12393 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 12852 12393 145 145 0 12707 0
[pid=4705] vsize: 51408
Current children cumulated CPU time (s) 139.27
Current children cumulated vsize (Kb) 53532

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 12957 0 0 0 14858 67 0 0 25 0 1 0 1855159073 53358592 12569 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 13027 12569 145 145 0 12882 0
[pid=4705] vsize: 52108
Current children cumulated CPU time (s) 149.25
Current children cumulated vsize (Kb) 54232

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 13162 0 0 0 15855 69 0 0 25 0 1 0 1855159073 54194176 12774 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 13231 12774 145 145 0 13086 0
[pid=4705] vsize: 52924
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 55048

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 13390 0 0 0 16851 71 0 0 25 0 1 0 1855159073 55119872 13002 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 13457 13002 145 145 0 13312 0
[pid=4705] vsize: 53828
Current children cumulated CPU time (s) 169.22
Current children cumulated vsize (Kb) 55952

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 13669 0 0 0 17847 73 0 0 25 0 1 0 1855159073 56258560 13281 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 13735 13281 145 145 0 13590 0
[pid=4705] vsize: 54940
Current children cumulated CPU time (s) 179.2
Current children cumulated vsize (Kb) 57064

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 13854 0 0 0 18843 75 0 0 25 0 1 0 1855159073 57012224 13466 4294967295 134512640 135094434 3221224432 3221223108 134553524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 13919 13466 145 145 0 13774 0
[pid=4705] vsize: 55676
Current children cumulated CPU time (s) 189.18
Current children cumulated vsize (Kb) 57800

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 14045 0 0 0 19841 76 0 0 25 0 1 0 1855159073 57786368 13657 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 14108 13657 145 145 0 13963 0
[pid=4705] vsize: 56432
Current children cumulated CPU time (s) 199.17
Current children cumulated vsize (Kb) 58556

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 14286 0 0 0 20837 78 0 0 25 0 1 0 1855159073 58769408 13898 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 14348 13898 145 145 0 14203 0
[pid=4705] vsize: 57392
Current children cumulated CPU time (s) 209.15
Current children cumulated vsize (Kb) 59516

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 14469 0 0 0 21834 79 0 0 25 0 1 0 1855159073 59514880 14081 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 14530 14081 145 145 0 14385 0
[pid=4705] vsize: 58120
Current children cumulated CPU time (s) 219.13
Current children cumulated vsize (Kb) 60244

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 14654 0 0 0 22830 80 0 0 25 0 1 0 1855159073 60399616 14266 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 14746 14266 145 145 0 14601 0
[pid=4705] vsize: 58984
Current children cumulated CPU time (s) 229.1
Current children cumulated vsize (Kb) 61108

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 14864 0 0 0 23827 81 0 0 25 0 1 0 1855159073 61251584 14476 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 14954 14476 145 145 0 14809 0
[pid=4705] vsize: 59816
Current children cumulated CPU time (s) 239.08
Current children cumulated vsize (Kb) 61940

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 15123 0 0 0 24823 83 0 0 25 0 1 0 1855159073 62316544 14735 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 15214 14735 145 145 0 15069 0
[pid=4705] vsize: 60856
Current children cumulated CPU time (s) 249.06
Current children cumulated vsize (Kb) 62980

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 15448 0 0 0 25818 85 0 0 25 0 1 0 1855159073 63643648 15060 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 15538 15060 145 145 0 15393 0
[pid=4705] vsize: 62152
Current children cumulated CPU time (s) 259.03
Current children cumulated vsize (Kb) 64276

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 15594 0 0 0 26814 87 0 0 25 0 1 0 1855159073 64237568 15206 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 15683 15206 145 145 0 15538 0
[pid=4705] vsize: 62732
Current children cumulated CPU time (s) 269.01
Current children cumulated vsize (Kb) 64856

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 15841 0 0 0 27808 90 0 0 25 0 1 0 1855159073 65236992 15453 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 15927 15453 145 145 0 15782 0
[pid=4705] vsize: 63708
Current children cumulated CPU time (s) 278.98
Current children cumulated vsize (Kb) 65832

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 16008 0 0 0 28805 91 0 0 25 0 1 0 1855159073 65916928 15620 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 16093 15620 145 145 0 15948 0
[pid=4705] vsize: 64372
Current children cumulated CPU time (s) 288.96
Current children cumulated vsize (Kb) 66496

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 16263 0 0 0 29801 94 0 0 25 0 1 0 1855159073 66957312 15875 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 16347 15875 145 145 0 16202 0
[pid=4705] vsize: 65388
Current children cumulated CPU time (s) 298.95
Current children cumulated vsize (Kb) 67512

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 16478 0 0 0 30797 95 0 0 25 0 1 0 1855159073 67833856 16090 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 16561 16090 145 145 0 16416 0
[pid=4705] vsize: 66244
Current children cumulated CPU time (s) 308.92
Current children cumulated vsize (Kb) 68368

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 16769 0 0 0 31793 97 0 0 25 0 1 0 1855159073 69021696 16381 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 16851 16381 145 145 0 16706 0
[pid=4705] vsize: 67404
Current children cumulated CPU time (s) 318.9
Current children cumulated vsize (Kb) 69528

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 17020 0 0 0 32788 99 0 0 25 0 1 0 1855159073 70041600 16632 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 17100 16632 145 145 0 16955 0
[pid=4705] vsize: 68400
Current children cumulated CPU time (s) 328.87
Current children cumulated vsize (Kb) 70524

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 17287 0 0 0 33785 101 0 0 25 0 1 0 1855159073 71131136 16899 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 17366 16899 145 145 0 17221 0
[pid=4705] vsize: 69464
Current children cumulated CPU time (s) 338.86
Current children cumulated vsize (Kb) 71588

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 17535 0 0 0 34780 102 0 0 25 0 1 0 1855159073 72142848 17147 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 17613 17147 145 145 0 17468 0
[pid=4705] vsize: 70452
Current children cumulated CPU time (s) 348.82
Current children cumulated vsize (Kb) 72576

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 17768 0 0 0 35776 103 0 0 25 0 1 0 1855159073 73093120 17380 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 17845 17380 145 145 0 17700 0
[pid=4705] vsize: 71380
Current children cumulated CPU time (s) 358.79
Current children cumulated vsize (Kb) 73504

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 17978 0 0 0 36772 106 0 0 25 0 1 0 1855159073 73949184 17590 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 18054 17590 145 145 0 17909 0
[pid=4705] vsize: 72216
Current children cumulated CPU time (s) 368.78
Current children cumulated vsize (Kb) 74340

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 18196 0 0 0 37767 108 0 0 25 0 1 0 1855159073 74838016 17808 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 18271 17808 145 145 0 18126 0
[pid=4705] vsize: 73084
Current children cumulated CPU time (s) 378.75
Current children cumulated vsize (Kb) 75208

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 18548 0 0 0 38763 110 0 0 25 0 1 0 1855159073 76275712 18160 4294967295 134512640 135094434 3221224432 3221223104 134555846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 18622 18160 145 145 0 18477 0
[pid=4705] vsize: 74488
Current children cumulated CPU time (s) 388.73
Current children cumulated vsize (Kb) 76612

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 18813 0 0 0 39759 112 0 0 25 0 1 0 1855159073 77357056 18425 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 18886 18425 145 145 0 18741 0
[pid=4705] vsize: 75544
Current children cumulated CPU time (s) 398.71
Current children cumulated vsize (Kb) 77668

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 19083 0 0 0 40754 114 0 0 25 0 1 0 1855159073 78458880 18695 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 19155 18695 145 145 0 19010 0
[pid=4705] vsize: 76620
Current children cumulated CPU time (s) 408.68
Current children cumulated vsize (Kb) 78744

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 19285 0 0 0 41751 115 0 0 25 0 1 0 1855159073 79282176 18897 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 19356 18897 145 145 0 19211 0
[pid=4705] vsize: 77424
Current children cumulated CPU time (s) 418.66
Current children cumulated vsize (Kb) 79548

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 19486 0 0 0 42748 117 0 0 25 0 1 0 1855159073 80101376 19098 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 19556 19098 145 145 0 19411 0
[pid=4705] vsize: 78224
Current children cumulated CPU time (s) 428.65
Current children cumulated vsize (Kb) 80348

[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 19746 0 0 0 43745 118 0 0 25 0 1 0 1855159073 81162240 19358 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 19815 19358 145 145 0 19670 0
[pid=4705] vsize: 79260
Current children cumulated CPU time (s) 438.63
Current children cumulated vsize (Kb) 81384

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 20075 0 0 0 44739 119 0 0 25 0 1 0 1855159073 82505728 19687 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 20143 19687 145 145 0 19998 0
[pid=4705] vsize: 80572
Current children cumulated CPU time (s) 448.58
Current children cumulated vsize (Kb) 82696

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 20381 0 0 0 45735 121 0 0 25 0 1 0 1855159073 83763200 19993 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 20450 19993 145 145 0 20305 0
[pid=4705] vsize: 81800
Current children cumulated CPU time (s) 458.56
Current children cumulated vsize (Kb) 83924

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 20623 0 0 0 46731 122 0 0 25 0 1 0 1855159073 84746240 20235 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 20690 20235 145 145 0 20545 0
[pid=4705] vsize: 82760
Current children cumulated CPU time (s) 468.53
Current children cumulated vsize (Kb) 84884

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 20860 0 0 0 47728 123 0 0 25 0 1 0 1855159073 85712896 20472 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 20926 20472 145 145 0 20781 0
[pid=4705] vsize: 83704
Current children cumulated CPU time (s) 478.51
Current children cumulated vsize (Kb) 85828

[startup+490.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 21091 0 0 0 48725 125 0 0 18 0 1 0 1855159073 86654976 20703 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 21156 20703 145 145 0 21011 0
[pid=4705] vsize: 84624
Current children cumulated CPU time (s) 488.5
Current children cumulated vsize (Kb) 86748

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 21330 0 0 0 49721 127 0 0 25 0 1 0 1855159073 87629824 20942 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 21394 20942 145 145 0 21249 0
[pid=4705] vsize: 85576
Current children cumulated CPU time (s) 498.48
Current children cumulated vsize (Kb) 87700

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 21585 0 0 0 50717 129 0 0 25 0 1 0 1855159073 88670208 21197 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 21648 21197 145 145 0 21503 0
[pid=4705] vsize: 86592
Current children cumulated CPU time (s) 508.46
Current children cumulated vsize (Kb) 88716

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 21823 0 0 0 51713 130 0 0 25 0 1 0 1855159073 89640960 21435 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 21885 21435 145 145 0 21740 0
[pid=4705] vsize: 87540
Current children cumulated CPU time (s) 518.43
Current children cumulated vsize (Kb) 89664

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) T 4701 4701 19818 0 -1 0 22030 0 0 0 52710 132 0 0 25 0 1 0 1855159073 90484736 21642 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4705/statm): 22091 21642 145 145 0 21946 0
[pid=4705] vsize: 88364
Current children cumulated CPU time (s) 528.42
Current children cumulated vsize (Kb) 90488

[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 22243 0 0 0 53706 133 0 0 25 0 1 0 1855159073 91615232 21855 4294967295 134512640 135094434 3221224432 3221223104 134556478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 22367 21855 145 145 0 22222 0
[pid=4705] vsize: 89468
Current children cumulated CPU time (s) 538.39
Current children cumulated vsize (Kb) 91592

[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 22459 0 0 0 54703 135 0 0 25 0 1 0 1855159073 92495872 22071 4294967295 134512640 135094434 3221224432 3221223044 134563154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 22582 22071 145 145 0 22437 0
[pid=4705] vsize: 90328
Current children cumulated CPU time (s) 548.38
Current children cumulated vsize (Kb) 92452

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 22725 0 0 0 55699 136 0 0 25 0 1 0 1855159073 93581312 22337 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 22847 22337 145 145 0 22702 0
[pid=4705] vsize: 91388
Current children cumulated CPU time (s) 558.35
Current children cumulated vsize (Kb) 93512

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 23024 0 0 0 56695 138 0 0 25 0 1 0 1855159073 94801920 22636 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 23145 22636 145 145 0 23000 0
[pid=4705] vsize: 92580
Current children cumulated CPU time (s) 568.33
Current children cumulated vsize (Kb) 94704

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 23263 0 0 0 57691 139 0 0 25 0 1 0 1855159073 95776768 22875 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 23383 22875 145 145 0 23238 0
[pid=4705] vsize: 93532
Current children cumulated CPU time (s) 578.3
Current children cumulated vsize (Kb) 95656

[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 23516 0 0 0 58688 140 0 0 25 0 1 0 1855159073 96813056 23128 4294967295 134512640 135094434 3221224432 3221223104 134555940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 23636 23128 145 145 0 23491 0
[pid=4705] vsize: 94544
Current children cumulated CPU time (s) 588.28
Current children cumulated vsize (Kb) 96668

[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 23828 0 0 0 59684 142 0 0 25 0 1 0 1855159073 98086912 23440 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 23947 23440 145 145 0 23802 0
[pid=4705] vsize: 95788
Current children cumulated CPU time (s) 598.26
Current children cumulated vsize (Kb) 97912

[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 24108 0 0 0 60679 143 0 0 25 0 1 0 1855159073 99254272 23720 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 24232 23720 145 145 0 24087 0
[pid=4705] vsize: 96928
Current children cumulated CPU time (s) 608.22
Current children cumulated vsize (Kb) 99052

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 24382 0 0 0 61675 146 0 0 25 0 1 0 1855159073 100372480 23994 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 24505 23994 145 145 0 24360 0
[pid=4705] vsize: 98020
Current children cumulated CPU time (s) 618.21
Current children cumulated vsize (Kb) 100144

[startup+630.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 24719 0 0 0 62670 148 0 0 25 0 1 0 1855159073 101724160 24331 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 24835 24331 145 145 0 24690 0
[pid=4705] vsize: 99340
Current children cumulated CPU time (s) 628.18
Current children cumulated vsize (Kb) 101464

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 25101 0 0 0 63665 150 0 0 25 0 1 0 1855159073 103284736 24713 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 25216 24713 145 145 0 25071 0
[pid=4705] vsize: 100864
Current children cumulated CPU time (s) 638.15
Current children cumulated vsize (Kb) 102988

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 25446 0 0 0 64661 152 0 0 25 0 1 0 1855159073 104697856 25058 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 25561 25058 145 145 0 25416 0
[pid=4705] vsize: 102244
Current children cumulated CPU time (s) 648.13
Current children cumulated vsize (Kb) 104368

[startup+660.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 25752 0 0 0 65658 154 0 0 25 0 1 0 1855159073 105947136 25364 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 25866 25364 145 145 0 25721 0
[pid=4705] vsize: 103464
Current children cumulated CPU time (s) 658.12
Current children cumulated vsize (Kb) 105588

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 26061 0 0 0 66655 155 0 0 25 0 1 0 1855159073 107208704 25673 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 26174 25673 145 145 0 26029 0
[pid=4705] vsize: 104696
Current children cumulated CPU time (s) 668.1
Current children cumulated vsize (Kb) 106820

[startup+680.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 26384 0 0 0 67650 158 0 0 25 0 1 0 1855159073 108527616 25996 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 26496 25996 145 145 0 26351 0
[pid=4705] vsize: 105984
Current children cumulated CPU time (s) 678.08
Current children cumulated vsize (Kb) 108108

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 26740 0 0 0 68647 159 0 0 25 0 1 0 1855159073 109981696 26352 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 26851 26352 145 145 0 26706 0
[pid=4705] vsize: 107404
Current children cumulated CPU time (s) 688.06
Current children cumulated vsize (Kb) 109528

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 26984 0 0 0 69644 161 0 0 25 0 1 0 1855159073 110981120 26596 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 27095 26596 145 145 0 26950 0
[pid=4705] vsize: 108380
Current children cumulated CPU time (s) 698.05
Current children cumulated vsize (Kb) 110504

[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 27331 0 0 0 70640 162 0 0 25 0 1 0 1855159073 112398336 26943 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 27441 26943 145 145 0 27296 0
[pid=4705] vsize: 109764
Current children cumulated CPU time (s) 708.02
Current children cumulated vsize (Kb) 111888

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 27522 0 0 0 71637 163 0 0 25 0 1 0 1855159073 113176576 27134 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 27631 27134 145 145 0 27486 0
[pid=4705] vsize: 110524
Current children cumulated CPU time (s) 718
Current children cumulated vsize (Kb) 112648

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 27841 0 0 0 72632 166 0 0 25 0 1 0 1855159073 114479104 27453 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 27949 27453 145 145 0 27804 0
[pid=4705] vsize: 111796
Current children cumulated CPU time (s) 727.98
Current children cumulated vsize (Kb) 113920

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 28163 0 0 0 73629 168 0 0 25 0 1 0 1855159073 115798016 27775 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 28271 27775 145 145 0 28126 0
[pid=4705] vsize: 113084
Current children cumulated CPU time (s) 737.97
Current children cumulated vsize (Kb) 115208

[startup+750.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 28408 0 0 0 74625 170 0 0 25 0 1 0 1855159073 116797440 28020 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 28515 28020 145 145 0 28370 0
[pid=4705] vsize: 114060
Current children cumulated CPU time (s) 747.95
Current children cumulated vsize (Kb) 116184

[startup+760.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 28725 0 0 0 75620 172 0 0 25 0 1 0 1855159073 118091776 28337 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 28831 28337 145 145 0 28686 0
[pid=4705] vsize: 115324
Current children cumulated CPU time (s) 757.92
Current children cumulated vsize (Kb) 117448

[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 28974 0 0 0 76618 173 0 0 25 0 1 0 1855159073 119107584 28586 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 29079 28586 145 145 0 28934 0
[pid=4705] vsize: 116316
Current children cumulated CPU time (s) 767.91
Current children cumulated vsize (Kb) 118440

[startup+780.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 29212 0 0 0 77614 175 0 0 25 0 1 0 1855159073 120078336 28824 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 29316 28824 145 145 0 29171 0
[pid=4705] vsize: 117264
Current children cumulated CPU time (s) 777.89
Current children cumulated vsize (Kb) 119388

[startup+790.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 29512 0 0 0 78610 176 0 0 25 0 1 0 1855159073 121307136 29124 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 29616 29124 145 145 0 29471 0
[pid=4705] vsize: 118464
Current children cumulated CPU time (s) 787.86
Current children cumulated vsize (Kb) 120588

[startup+800.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 29774 0 0 0 79607 177 0 0 25 0 1 0 1855159073 122376192 29386 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 29877 29386 145 145 0 29732 0
[pid=4705] vsize: 119508
Current children cumulated CPU time (s) 797.84
Current children cumulated vsize (Kb) 121632

[startup+810.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 30208 0 0 0 80603 179 0 0 25 0 1 0 1855159073 124137472 29820 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4705/statm): 30307 29820 145 145 0 30162 0
[pid=4705] vsize: 121228
Current children cumulated CPU time (s) 807.82
Current children cumulated vsize (Kb) 123352

[startup+820.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 30533 0 0 0 81599 181 0 0 25 0 1 0 1855159073 125464576 30145 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 30631 30145 145 145 0 30486 0
[pid=4705] vsize: 122524
Current children cumulated CPU time (s) 817.8
Current children cumulated vsize (Kb) 124648

[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 30762 0 0 0 82596 182 0 0 25 0 1 0 1855159073 126398464 30374 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 30859 30374 145 145 0 30714 0
[pid=4705] vsize: 123436
Current children cumulated CPU time (s) 827.78
Current children cumulated vsize (Kb) 125560

[startup+840.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 30993 0 0 0 83592 184 0 0 25 0 1 0 1855159073 127324160 30605 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 31085 30605 145 145 0 30940 0
[pid=4705] vsize: 124340
Current children cumulated CPU time (s) 837.76
Current children cumulated vsize (Kb) 126464

[startup+850.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 31269 0 0 0 84589 186 0 0 25 0 1 0 1855159073 128450560 30881 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 31360 30881 145 145 0 31215 0
[pid=4705] vsize: 125440
Current children cumulated CPU time (s) 847.75
Current children cumulated vsize (Kb) 127564

[startup+860.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 31652 0 0 0 85584 188 0 0 25 0 1 0 1855159073 130019328 31264 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 31743 31264 145 145 0 31598 0
[pid=4705] vsize: 126972
Current children cumulated CPU time (s) 857.72
Current children cumulated vsize (Kb) 129096

[startup+870.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 31925 0 0 0 86581 190 0 0 25 0 1 0 1855159073 131133440 31537 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 32015 31537 145 145 0 31870 0
[pid=4705] vsize: 128060
Current children cumulated CPU time (s) 867.71
Current children cumulated vsize (Kb) 130184

[startup+880.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 32221 0 0 0 87578 192 0 0 25 0 1 0 1855159073 132341760 31833 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 32310 31833 145 145 0 32165 0
[pid=4705] vsize: 129240
Current children cumulated CPU time (s) 877.7
Current children cumulated vsize (Kb) 131364

[startup+890.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 32452 0 0 0 88574 193 0 0 25 0 1 0 1855159073 133287936 32064 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 32541 32064 145 145 0 32396 0
[pid=4705] vsize: 130164
Current children cumulated CPU time (s) 887.67
Current children cumulated vsize (Kb) 132288

[startup+900.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 32799 0 0 0 89569 195 0 0 25 0 1 0 1855159073 134705152 32411 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 32887 32411 145 145 0 32742 0
[pid=4705] vsize: 131548
Current children cumulated CPU time (s) 897.64
Current children cumulated vsize (Kb) 133672

[startup+910.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 33024 0 0 0 90567 196 0 0 25 0 1 0 1855159073 135626752 32636 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 33112 32636 145 145 0 32967 0
[pid=4705] vsize: 132448
Current children cumulated CPU time (s) 907.63
Current children cumulated vsize (Kb) 134572

[startup+920.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 33293 0 0 0 91563 197 0 0 25 0 1 0 1855159073 136724480 32905 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 33380 32905 145 145 0 33235 0
[pid=4705] vsize: 133520
Current children cumulated CPU time (s) 917.6
Current children cumulated vsize (Kb) 135644

[startup+930.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 33483 0 0 0 92561 198 0 0 25 0 1 0 1855159073 137498624 33095 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 33569 33095 145 145 0 33424 0
[pid=4705] vsize: 134276
Current children cumulated CPU time (s) 927.59
Current children cumulated vsize (Kb) 136400

[startup+940.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 33810 0 0 0 93557 200 0 0 25 0 1 0 1855159073 138825728 33422 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 33893 33422 145 145 0 33748 0
[pid=4705] vsize: 135572
Current children cumulated CPU time (s) 937.57
Current children cumulated vsize (Kb) 137696

[startup+950.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 34179 0 0 0 94551 203 0 0 25 0 1 0 1855159073 140333056 33791 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 34261 33791 145 145 0 34116 0
[pid=4705] vsize: 137044
Current children cumulated CPU time (s) 947.54
Current children cumulated vsize (Kb) 139168

[startup+960.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 34452 0 0 0 95548 205 0 0 25 0 1 0 1855159073 141447168 34064 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 34533 34064 145 145 0 34388 0
[pid=4705] vsize: 138132
Current children cumulated CPU time (s) 957.53
Current children cumulated vsize (Kb) 140256

[startup+970.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 34884 0 0 0 96543 207 0 0 25 0 1 0 1855159073 143208448 34496 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 34963 34496 145 145 0 34818 0
[pid=4705] vsize: 139852
Current children cumulated CPU time (s) 967.5
Current children cumulated vsize (Kb) 141976

[startup+980.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 35244 0 0 0 97539 209 0 0 25 0 1 0 1855159073 144678912 34856 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 35322 34856 145 145 0 35177 0
[pid=4705] vsize: 141288
Current children cumulated CPU time (s) 977.48
Current children cumulated vsize (Kb) 143412

[startup+990.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 35459 0 0 0 98535 211 0 0 25 0 1 0 1855159073 145555456 35071 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 35536 35071 145 145 0 35391 0
[pid=4705] vsize: 142144
Current children cumulated CPU time (s) 987.46
Current children cumulated vsize (Kb) 144268

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 35716 0 0 0 99532 213 0 0 25 0 1 0 1855159073 146608128 35328 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 35793 35328 145 145 0 35648 0
[pid=4705] vsize: 143172
Current children cumulated CPU time (s) 997.45
Current children cumulated vsize (Kb) 145296

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 35886 0 0 0 100530 214 0 0 25 0 1 0 1855159073 147304448 35498 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 35963 35498 145 145 0 35818 0
[pid=4705] vsize: 143852
Current children cumulated CPU time (s) 1007.44
Current children cumulated vsize (Kb) 145976

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 36093 0 0 0 101527 215 0 0 25 0 1 0 1855159073 148148224 35705 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 36169 35705 145 145 0 36024 0
[pid=4705] vsize: 144676
Current children cumulated CPU time (s) 1017.42
Current children cumulated vsize (Kb) 146800

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 36305 0 0 0 102524 216 0 0 25 0 1 0 1855159073 149012480 35917 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 36380 35917 145 145 0 36235 0
[pid=4705] vsize: 145520
Current children cumulated CPU time (s) 1027.4
Current children cumulated vsize (Kb) 147644

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 36626 0 0 0 103520 219 0 0 25 0 1 0 1855159073 150327296 36238 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 36701 36238 145 145 0 36556 0
[pid=4705] vsize: 146804
Current children cumulated CPU time (s) 1037.39
Current children cumulated vsize (Kb) 148928

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 36938 0 0 0 104515 220 0 0 25 0 1 0 1855159073 151552000 36550 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 37000 36550 145 145 0 36855 0
[pid=4705] vsize: 148000
Current children cumulated CPU time (s) 1047.35
Current children cumulated vsize (Kb) 150124

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 37117 0 0 0 105513 222 0 0 25 0 1 0 1855159073 152285184 36729 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 37179 36729 145 145 0 37034 0
[pid=4705] vsize: 148716
Current children cumulated CPU time (s) 1057.35
Current children cumulated vsize (Kb) 150840

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 37358 0 0 0 106510 223 0 0 25 0 1 0 1855159073 153268224 36970 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 37419 36970 145 145 0 37274 0
[pid=4705] vsize: 149676
Current children cumulated CPU time (s) 1067.33
Current children cumulated vsize (Kb) 151800

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 37637 0 0 0 107506 226 0 0 25 0 1 0 1855159073 154406912 37249 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 37697 37249 145 145 0 37552 0
[pid=4705] vsize: 150788
Current children cumulated CPU time (s) 1077.32
Current children cumulated vsize (Kb) 152912

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 37898 0 0 0 108503 227 0 0 25 0 1 0 1855159073 155471872 37510 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 37957 37510 145 145 0 37812 0
[pid=4705] vsize: 151828
Current children cumulated CPU time (s) 1087.3
Current children cumulated vsize (Kb) 153952

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 38152 0 0 0 109500 228 0 0 25 0 1 0 1855159073 156512256 37764 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 38211 37764 145 145 0 38066 0
[pid=4705] vsize: 152844
Current children cumulated CPU time (s) 1097.28
Current children cumulated vsize (Kb) 154968

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 38386 0 0 0 110497 230 0 0 25 0 1 0 1855159073 157470720 37998 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 38445 37998 145 145 0 38300 0
[pid=4705] vsize: 153780
Current children cumulated CPU time (s) 1107.27
Current children cumulated vsize (Kb) 155904

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 38738 0 0 0 111493 232 0 0 25 0 1 0 1855159073 158908416 38350 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 38796 38350 145 145 0 38651 0
[pid=4705] vsize: 155184
Current children cumulated CPU time (s) 1117.25
Current children cumulated vsize (Kb) 157308

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 39033 0 0 0 112490 234 0 0 25 0 1 0 1855159073 160116736 38645 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 39091 38645 145 145 0 38946 0
[pid=4705] vsize: 156364
Current children cumulated CPU time (s) 1127.24
Current children cumulated vsize (Kb) 158488

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 39424 0 0 0 113487 235 0 0 25 0 1 0 1855159073 161714176 39036 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 39481 39036 145 145 0 39336 0
[pid=4705] vsize: 157924
Current children cumulated CPU time (s) 1137.22
Current children cumulated vsize (Kb) 160048

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 39794 0 0 0 114484 237 0 0 25 0 1 0 1855159073 163287040 39406 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 39865 39406 145 145 0 39720 0
[pid=4705] vsize: 159460
Current children cumulated CPU time (s) 1147.21
Current children cumulated vsize (Kb) 161584

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 40035 0 0 0 115482 238 0 0 25 0 1 0 1855159073 164270080 39647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 40105 39647 145 145 0 39960 0
[pid=4705] vsize: 160420
Current children cumulated CPU time (s) 1157.2
Current children cumulated vsize (Kb) 162544

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 40305 0 0 0 116478 240 0 0 25 0 1 0 1855159073 165371904 39917 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 40374 39917 145 145 0 40229 0
[pid=4705] vsize: 161496
Current children cumulated CPU time (s) 1167.18
Current children cumulated vsize (Kb) 163620

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 40533 0 0 0 117475 241 0 0 25 0 1 0 1855159073 166309888 40145 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 40603 40145 145 145 0 40458 0
[pid=4705] vsize: 162412
Current children cumulated CPU time (s) 1177.16
Current children cumulated vsize (Kb) 164536

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 40816 0 0 0 118472 242 0 0 25 0 1 0 1855159073 167460864 40428 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 40884 40428 145 145 0 40739 0
[pid=4705] vsize: 163536
Current children cumulated CPU time (s) 1187.14
Current children cumulated vsize (Kb) 165660

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 40929 0 0 0 119471 243 0 0 25 0 1 0 1855159073 167919616 40541 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 40996 40541 145 145 0 40851 0
[pid=4705] vsize: 163984
Current children cumulated CPU time (s) 1197.14
Current children cumulated vsize (Kb) 166108

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 41200 0 0 0 120466 246 0 0 25 0 1 0 1855159073 169029632 40812 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 41267 40812 145 145 0 41122 0
[pid=4705] vsize: 165068
Current children cumulated CPU time (s) 1207.12
Current children cumulated vsize (Kb) 167192



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4705
Raw data (/proc/4701/stat): 4701 (minisat+_script) S 4700 4701 19818 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855159068 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4701/statm): 531 226 485 147 0 384 0
[pid=4701] vsize: 2124
Raw data (/proc/4705/stat): 4705 (minisat+_64-bit) R 4701 4701 19818 0 -1 0 41200 0 0 0 120466 246 0 0 25 0 1 0 1855159073 169029632 40812 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4705/statm): 41267 40812 145 145 0 41122 0
[pid=4705] vsize: 165068
Current children cumulated CPU time (s) 1207.12
Current children cumulated vsize (Kb) 167192

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1207.2
CPU user time (s): 1204.67
CPU system time (s): 2.53661
CPU usage (%): 99.7534
Max. virtual memory (cumulated for all children) (Kb): 167192

Verifier Data

ERROR: no interpretation found !