Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-air04.opb
MD5SUM26490113618ae9605b5ebe6370b5910b
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 8904
Biggest coefficient in the objective function 2258
Number of bits for the biggest coefficient in the objective function 12
Sum of the numbers in the objective function 5135151
Number of bits of the sum of numbers in the objective function 23
Biggest number in a constraint 2258
Number of bits of the biggest number in a constraint 12
Biggest sum of numbers in a constraint 5135151
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables8904
Total number of constraints9727
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)9727
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint368

Trace number 4500

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        871528 kB
Buffers:         36028 kB
Cached:          99308 kB
SwapCached:        732 kB
Active:          65740 kB
Inactive:        72192 kB
HighTotal:      131008 kB
HighFree:        30100 kB
LowTotal:       903652 kB
LowFree:        841428 kB
SwapTotal:     2097136 kB
SwapFree:      2095856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19520 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:05:24 (client local time) WITH STATUS 0 IN 1206.01 SECONDS
stats: 2958 7 1206.01 0

Solver Data

c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       100 |  310358   807732 |  113797     100     2792    27.9 |  0.588 % |
c |       250 |  310331   807657 |  125176     249    12761    51.2 |  0.592 % |
c |       475 |  310198   807286 |  137694     459    35376    77.1 |  0.620 % |
c |       812 |  310052   806901 |  151464     787    48598    61.8 |  0.642 % |
c |      1319 |  309884   806468 |  166610    1289    73251    56.8 |  0.667 % |
c |      2078 |  309785   806192 |  183271    2043   141139    69.1 |  0.692 % |
c |      3217 |  309724   806017 |  201598    3171   279873    88.3 |  0.705 % |
c |      4927 |  309614   805741 |  221758    4872   562380   115.4 |  0.716 % |
c |      7490 |  309614   805741 |  243934    7435  1259451   169.4 |  0.716 % |
c |     11334 |  309475   805377 |  268327   11239  1793736   159.6 |  0.732 % |
c |     17101 |  309226   804713 |  295160   16957  2478519   146.2 |  0.776 % |
c |     25752 |  307768   801003 |  324676   25505  3930547   154.1 |  0.987 % |
c |     38728 |  307515   800363 |  357144   38421  6348349   165.2 |  1.003 % |
c |     58191 |  307356   799958 |  392858   57785 10148314   175.6 |  1.017 % |
c |     87385 |  306886   798753 |  432144   86840 17512694   201.7 |  1.062 % |
c |    131176 |  306715   798313 |  475359  130557 31984227   245.0 |  1.079 % |

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/26510/stat): 26510 (minisat+_script) R 26509 26510 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793566986 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26510/statm): 174 3 169 147 0 27 0
[pid=26510] 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=26511
New process pid=26512
New process pid=26513
execve syscall for /bin/sed executable
One traced child (pid=26512) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=26513) exited with status: 0
One traced child (pid=26511) exited with status: 0
New process pid=26514
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-air04.opb

[startup+10.0043 s]
Raw data (loadavg): 0.87 0.94 0.69 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 10937 0 2 0 888 44 0 0 25 0 1 0 1793566992 52551680 10549 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26514/statm): 12830 10549 145 145 0 12685 0
[pid=26514] vsize: 51320
Current children cumulated CPU time (s) 9.33
Current children cumulated vsize (Kb) 53444

[startup+20.0051 s]
Raw data (loadavg): 0.89 0.94 0.69 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 11185 0 2 0 1883 46 0 0 25 0 1 0 1793566992 53530624 10797 4294967295 134512640 135094434 3221224432 3221223024 134556902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 13069 10797 145 145 0 12924 0
[pid=26514] vsize: 52276
Current children cumulated CPU time (s) 19.3
Current children cumulated vsize (Kb) 54400

[startup+30.0059 s]
Raw data (loadavg): 0.90 0.94 0.69 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 11528 0 2 0 2877 48 0 0 25 0 1 0 1793566992 54943744 11140 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26514/statm): 13414 11140 145 145 0 13269 0
[pid=26514] vsize: 53656
Current children cumulated CPU time (s) 29.26
Current children cumulated vsize (Kb) 55780

[startup+40.0067 s]
Raw data (loadavg): 0.92 0.94 0.70 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 12131 0 2 0 3867 53 0 0 25 0 1 0 1793566992 57405440 11743 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 14015 11743 145 145 0 13870 0
[pid=26514] vsize: 56060
Current children cumulated CPU time (s) 39.21
Current children cumulated vsize (Kb) 58184

[startup+50.0084 s]
Raw data (loadavg): 0.93 0.94 0.70 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 12615 0 2 0 4858 56 0 0 25 0 1 0 1793566992 59412480 12227 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 14505 12227 145 145 0 14360 0
[pid=26514] vsize: 58020
Current children cumulated CPU time (s) 49.15
Current children cumulated vsize (Kb) 60144

[startup+60.0092 s]
Raw data (loadavg): 0.94 0.95 0.70 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 12865 0 2 0 5854 57 0 0 25 0 1 0 1793566992 60428288 12477 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 14753 12477 145 145 0 14608 0
[pid=26514] vsize: 59012
Current children cumulated CPU time (s) 59.12
Current children cumulated vsize (Kb) 61136

[startup+70.01 s]
Raw data (loadavg): 0.95 0.95 0.71 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 13115 0 2 0 6850 59 0 0 25 0 1 0 1793566992 61444096 12727 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 15001 12727 145 145 0 14856 0
[pid=26514] vsize: 60004
Current children cumulated CPU time (s) 69.1
Current children cumulated vsize (Kb) 62128

[startup+80.0108 s]
Raw data (loadavg): 0.96 0.95 0.71 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 13399 0 2 0 7844 62 0 0 25 0 1 0 1793566992 62599168 13011 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 15283 13011 145 145 0 15138 0
[pid=26514] vsize: 61132
Current children cumulated CPU time (s) 79.07
Current children cumulated vsize (Kb) 63256

[startup+90.0106 s]
Raw data (loadavg): 0.96 0.95 0.71 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 13646 0 2 0 8840 64 0 0 25 0 1 0 1793566992 63668224 13258 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 15544 13258 145 145 0 15399 0
[pid=26514] vsize: 62176
Current children cumulated CPU time (s) 89.05
Current children cumulated vsize (Kb) 64300

[startup+100.011 s]
Raw data (loadavg): 0.97 0.95 0.71 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 13993 0 2 0 9834 66 0 0 25 0 1 0 1793566992 65081344 13605 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 15889 13605 145 145 0 15744 0
[pid=26514] vsize: 63556
Current children cumulated CPU time (s) 99.01
Current children cumulated vsize (Kb) 65680

[startup+110.012 s]
Raw data (loadavg): 0.97 0.95 0.72 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 14366 0 2 0 10828 68 0 0 25 0 1 0 1793566992 66600960 13978 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 16260 13978 145 145 0 16115 0
[pid=26514] vsize: 65040
Current children cumulated CPU time (s) 108.97
Current children cumulated vsize (Kb) 67164

[startup+120.015 s]
Raw data (loadavg): 0.98 0.95 0.72 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 14810 0 2 0 11820 71 0 0 25 0 1 0 1793566992 68411392 14422 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 16702 14422 145 145 0 16557 0
[pid=26514] vsize: 66808
Current children cumulated CPU time (s) 118.92
Current children cumulated vsize (Kb) 68932

[startup+130.016 s]
Raw data (loadavg): 0.98 0.95 0.72 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 15052 0 2 0 12816 73 0 0 25 0 1 0 1793566992 69394432 14664 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 16942 14664 145 145 0 16797 0
[pid=26514] vsize: 67768
Current children cumulated CPU time (s) 128.9
Current children cumulated vsize (Kb) 69892

[startup+140.017 s]
Raw data (loadavg): 0.98 0.95 0.73 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 15329 0 2 0 13811 75 0 0 25 0 1 0 1793566992 70524928 14941 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 17218 14941 145 145 0 17073 0
[pid=26514] vsize: 68872
Current children cumulated CPU time (s) 138.87
Current children cumulated vsize (Kb) 70996

[startup+150.018 s]
Raw data (loadavg): 0.98 0.95 0.73 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 15659 0 2 0 14805 77 0 0 25 0 1 0 1793566992 71868416 15271 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 17546 15271 145 145 0 17401 0
[pid=26514] vsize: 70184
Current children cumulated CPU time (s) 148.83
Current children cumulated vsize (Kb) 72308

[startup+160.019 s]
Raw data (loadavg): 0.99 0.95 0.73 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 16062 0 2 0 15798 80 0 0 25 0 1 0 1793566992 73510912 15674 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 17947 15674 145 145 0 17802 0
[pid=26514] vsize: 71788
Current children cumulated CPU time (s) 158.79
Current children cumulated vsize (Kb) 73912

[startup+170.019 s]
Raw data (loadavg): 0.99 0.96 0.73 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 16307 0 2 0 16794 83 0 0 25 0 1 0 1793566992 74493952 15919 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 18187 15919 145 145 0 18042 0
[pid=26514] vsize: 72748
Current children cumulated CPU time (s) 168.78
Current children cumulated vsize (Kb) 74872

[startup+180.02 s]
Raw data (loadavg): 0.99 0.96 0.73 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 16706 0 2 0 17788 85 0 0 25 0 1 0 1793566992 76255232 16318 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 18617 16318 145 145 0 18472 0
[pid=26514] vsize: 74468
Current children cumulated CPU time (s) 178.74
Current children cumulated vsize (Kb) 76592

[startup+190.02 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 16932 0 2 0 18784 86 0 0 25 0 1 0 1793566992 77172736 16544 4294967295 134512640 135094434 3221224432 3221223104 134556327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 18841 16544 145 145 0 18696 0
[pid=26514] vsize: 75364
Current children cumulated CPU time (s) 188.71
Current children cumulated vsize (Kb) 77488

[startup+200.021 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 17294 0 2 0 19779 88 0 0 25 0 1 0 1793566992 78651392 16906 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 19202 16906 145 145 0 19057 0
[pid=26514] vsize: 76808
Current children cumulated CPU time (s) 198.68
Current children cumulated vsize (Kb) 78932

[startup+210.022 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 17713 0 2 0 20771 92 0 0 25 0 1 0 1793566992 80359424 17325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 19619 17325 145 145 0 19474 0
[pid=26514] vsize: 78476
Current children cumulated CPU time (s) 208.64
Current children cumulated vsize (Kb) 80600

[startup+220.023 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 17968 0 2 0 21767 94 0 0 25 0 1 0 1793566992 81383424 17580 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 19869 17580 145 145 0 19724 0
[pid=26514] vsize: 79476
Current children cumulated CPU time (s) 218.62
Current children cumulated vsize (Kb) 81600

[startup+230.024 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 18179 0 2 0 22764 95 0 0 25 0 1 0 1793566992 82227200 17791 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 20075 17791 145 145 0 19930 0
[pid=26514] vsize: 80300
Current children cumulated CPU time (s) 228.6
Current children cumulated vsize (Kb) 82424

[startup+240.024 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 18520 0 2 0 23758 98 0 0 25 0 1 0 1793566992 83615744 18132 4294967295 134512640 135094434 3221224432 3221223056 134557728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 20414 18132 145 145 0 20269 0
[pid=26514] vsize: 81656
Current children cumulated CPU time (s) 238.57
Current children cumulated vsize (Kb) 83780

[startup+250.025 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 18832 0 2 0 24753 99 0 0 25 0 1 0 1793566992 84881408 18444 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 20723 18444 145 145 0 20578 0
[pid=26514] vsize: 82892
Current children cumulated CPU time (s) 248.53
Current children cumulated vsize (Kb) 85016

[startup+260.026 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) T 26510 26510 9854 0 -1 0 19242 0 2 0 25747 102 0 0 25 0 1 0 1793566992 86560768 18854 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434789 0 0 17 1 0 0
Raw data (/proc/26514/statm): 21133 18854 145 145 0 20988 0
[pid=26514] vsize: 84532
Current children cumulated CPU time (s) 258.5
Current children cumulated vsize (Kb) 86656

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 19646 0 2 0 26740 105 0 0 25 0 1 0 1793566992 88207360 19258 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 21535 19258 145 145 0 21390 0
[pid=26514] vsize: 86140
Current children cumulated CPU time (s) 268.46
Current children cumulated vsize (Kb) 88264

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 19882 0 2 0 27736 106 0 0 25 0 1 0 1793566992 89169920 19494 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 21770 19494 145 145 0 21625 0
[pid=26514] vsize: 87080
Current children cumulated CPU time (s) 278.43
Current children cumulated vsize (Kb) 89204

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 20093 0 2 0 28733 108 0 0 25 0 1 0 1793566992 90030080 19705 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 21980 19705 145 145 0 21835 0
[pid=26514] vsize: 87920
Current children cumulated CPU time (s) 288.42
Current children cumulated vsize (Kb) 90044

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 20381 0 2 0 29729 110 0 0 25 0 1 0 1793566992 91205632 19993 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 22267 19993 145 145 0 22122 0
[pid=26514] vsize: 89068
Current children cumulated CPU time (s) 298.4
Current children cumulated vsize (Kb) 91192

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 20710 0 2 0 30722 112 0 0 25 0 1 0 1793566992 92549120 20322 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 22595 20322 145 145 0 22450 0
[pid=26514] vsize: 90380
Current children cumulated CPU time (s) 308.35
Current children cumulated vsize (Kb) 92504

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 21069 0 2 0 31717 115 0 0 25 0 1 0 1793566992 94011392 20681 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 22952 20681 145 145 0 22807 0
[pid=26514] vsize: 91808
Current children cumulated CPU time (s) 318.33
Current children cumulated vsize (Kb) 93932

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 21314 0 2 0 32714 116 0 0 25 0 1 0 1793566992 95023104 20926 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 23199 20926 145 145 0 23054 0
[pid=26514] vsize: 92796
Current children cumulated CPU time (s) 328.31
Current children cumulated vsize (Kb) 94920

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 21574 0 2 0 33709 118 0 0 25 0 1 0 1793566992 96083968 21186 4294967295 134512640 135094434 3221224432 3221223136 134555129 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 23458 21186 145 145 0 23313 0
[pid=26514] vsize: 93832
Current children cumulated CPU time (s) 338.28
Current children cumulated vsize (Kb) 95956

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 21858 0 2 0 34705 120 0 0 25 0 1 0 1793566992 97239040 21470 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 23740 21470 145 145 0 23595 0
[pid=26514] vsize: 94960
Current children cumulated CPU time (s) 348.26
Current children cumulated vsize (Kb) 97084

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 22128 0 2 0 35699 122 0 0 25 0 1 0 1793566992 98336768 21740 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 24008 21740 145 145 0 23863 0
[pid=26514] vsize: 96032
Current children cumulated CPU time (s) 358.22
Current children cumulated vsize (Kb) 98156

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 22570 0 2 0 36693 126 0 0 25 0 1 0 1793566992 100143104 22182 4294967295 134512640 135094434 3221224432 3221223056 134557694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 24449 22182 145 145 0 24304 0
[pid=26514] vsize: 97796
Current children cumulated CPU time (s) 368.2
Current children cumulated vsize (Kb) 99920

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 23139 0 2 0 37687 128 0 0 25 0 1 0 1793566992 102469632 22751 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 25017 22751 145 145 0 24872 0
[pid=26514] vsize: 100068
Current children cumulated CPU time (s) 378.16
Current children cumulated vsize (Kb) 102192

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 23409 0 2 0 38683 130 0 0 25 0 1 0 1793566992 103571456 23021 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 25286 23021 145 145 0 25141 0
[pid=26514] vsize: 101144
Current children cumulated CPU time (s) 388.14
Current children cumulated vsize (Kb) 103268

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 23652 0 2 0 39678 132 0 0 25 0 1 0 1793566992 104562688 23264 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 25528 23264 145 145 0 25383 0
[pid=26514] vsize: 102112
Current children cumulated CPU time (s) 398.11
Current children cumulated vsize (Kb) 104236

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 24010 0 2 0 40674 133 0 0 25 0 1 0 1793566992 105992192 23622 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 25877 23622 145 145 0 25732 0
[pid=26514] vsize: 103508
Current children cumulated CPU time (s) 408.08
Current children cumulated vsize (Kb) 105632

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 24294 0 2 0 41670 135 0 0 25 0 1 0 1793566992 107413504 23906 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 26224 23906 145 145 0 26079 0
[pid=26514] vsize: 104896
Current children cumulated CPU time (s) 418.06
Current children cumulated vsize (Kb) 107020

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 24761 0 2 0 42662 138 0 0 25 0 1 0 1793566992 109322240 24373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 26690 24373 145 145 0 26545 0
[pid=26514] vsize: 106760
Current children cumulated CPU time (s) 428.01
Current children cumulated vsize (Kb) 108884

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 25093 0 2 0 43656 140 0 0 25 0 1 0 1793566992 110678016 24705 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 27021 24705 145 145 0 26876 0
[pid=26514] vsize: 108084
Current children cumulated CPU time (s) 437.97
Current children cumulated vsize (Kb) 110208

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 25377 0 2 0 44652 142 0 0 25 0 1 0 1793566992 111837184 24989 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 27304 24989 145 145 0 27159 0
[pid=26514] vsize: 109216
Current children cumulated CPU time (s) 447.95
Current children cumulated vsize (Kb) 111340

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 25710 0 2 0 45647 143 0 0 25 0 1 0 1793566992 113201152 25322 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 27637 25322 145 145 0 27492 0
[pid=26514] vsize: 110548
Current children cumulated CPU time (s) 457.91
Current children cumulated vsize (Kb) 112672

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 25904 0 2 0 46643 145 0 0 25 0 1 0 1793566992 113991680 25516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 27830 25516 145 145 0 27685 0
[pid=26514] vsize: 111320
Current children cumulated CPU time (s) 467.89
Current children cumulated vsize (Kb) 113444

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 26162 0 2 0 47639 147 0 0 25 0 1 0 1793566992 115044352 25774 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 28087 25774 145 145 0 27942 0
[pid=26514] vsize: 112348
Current children cumulated CPU time (s) 477.87
Current children cumulated vsize (Kb) 114472

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 26480 0 2 0 48635 149 0 0 25 0 1 0 1793566992 116342784 26092 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 28404 26092 145 145 0 28259 0
[pid=26514] vsize: 113616
Current children cumulated CPU time (s) 487.85
Current children cumulated vsize (Kb) 115740

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 26782 0 2 0 49631 151 0 0 25 0 1 0 1793566992 117575680 26394 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 28705 26394 145 145 0 28560 0
[pid=26514] vsize: 114820
Current children cumulated CPU time (s) 497.83
Current children cumulated vsize (Kb) 116944

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 27035 0 2 0 50627 152 0 0 25 0 1 0 1793566992 118607872 26647 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 28957 26647 145 145 0 28812 0
[pid=26514] vsize: 115828
Current children cumulated CPU time (s) 507.8
Current children cumulated vsize (Kb) 117952

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 27376 0 2 0 51621 155 0 0 25 0 1 0 1793566992 120000512 26988 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 29297 26988 145 145 0 29152 0
[pid=26514] vsize: 117188
Current children cumulated CPU time (s) 517.77
Current children cumulated vsize (Kb) 119312

[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 27719 0 2 0 52615 157 0 0 25 0 1 0 1793566992 121397248 27331 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 29638 27331 145 145 0 29493 0
[pid=26514] vsize: 118552
Current children cumulated CPU time (s) 527.73
Current children cumulated vsize (Kb) 120676

[startup+540.048 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 27993 0 2 0 53611 159 0 0 25 0 1 0 1793566992 122515456 27605 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 29911 27605 145 145 0 29766 0
[pid=26514] vsize: 119644
Current children cumulated CPU time (s) 537.71
Current children cumulated vsize (Kb) 121768

[startup+550.049 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 28319 0 2 0 54606 161 0 0 25 0 1 0 1793566992 123846656 27931 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 30236 27931 145 145 0 30091 0
[pid=26514] vsize: 120944
Current children cumulated CPU time (s) 547.68
Current children cumulated vsize (Kb) 123068

[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 28557 0 2 0 55602 162 0 0 25 0 1 0 1793566992 124817408 28169 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 30473 28169 145 145 0 30328 0
[pid=26514] vsize: 121892
Current children cumulated CPU time (s) 557.65
Current children cumulated vsize (Kb) 124016

[startup+570.05 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 28841 0 2 0 56597 164 0 0 25 0 1 0 1793566992 125976576 28453 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 30756 28453 145 145 0 30611 0
[pid=26514] vsize: 123024
Current children cumulated CPU time (s) 567.62
Current children cumulated vsize (Kb) 125148

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 29097 0 2 0 57593 166 0 0 25 0 1 0 1793566992 127021056 28709 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 31011 28709 145 145 0 30866 0
[pid=26514] vsize: 124044
Current children cumulated CPU time (s) 577.6
Current children cumulated vsize (Kb) 126168

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 29370 0 2 0 58589 168 0 0 25 0 1 0 1793566992 128135168 28982 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 31283 28982 145 145 0 31138 0
[pid=26514] vsize: 125132
Current children cumulated CPU time (s) 587.58
Current children cumulated vsize (Kb) 127256

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 29717 0 2 0 59581 172 0 0 25 0 1 0 1793566992 129552384 29329 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26514/statm): 31629 29329 145 145 0 31484 0
[pid=26514] vsize: 126516
Current children cumulated CPU time (s) 597.54
Current children cumulated vsize (Kb) 128640

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 29984 0 2 0 60576 174 0 0 25 0 1 0 1793566992 130637824 29596 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26514/statm): 31894 29596 145 145 0 31749 0
[pid=26514] vsize: 127576
Current children cumulated CPU time (s) 607.51
Current children cumulated vsize (Kb) 129700

[startup+620.055 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 30374 0 2 0 61569 176 0 0 25 0 1 0 1793566992 132227072 29986 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26514/statm): 32282 29986 145 145 0 32137 0
[pid=26514] vsize: 129128
Current children cumulated CPU time (s) 617.46
Current children cumulated vsize (Kb) 131252

[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 30718 0 2 0 62562 179 0 0 25 0 1 0 1793566992 133632000 30330 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 32625 30330 145 145 0 32480 0
[pid=26514] vsize: 130500
Current children cumulated CPU time (s) 627.42
Current children cumulated vsize (Kb) 132624

[startup+640.058 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 31055 0 2 0 63557 181 0 0 25 0 1 0 1793566992 135008256 30667 4294967295 134512640 135094434 3221224432 3221223088 134558292 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 32961 30667 145 145 0 32816 0
[pid=26514] vsize: 131844
Current children cumulated CPU time (s) 637.39
Current children cumulated vsize (Kb) 133968

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 31406 0 2 0 64550 183 0 0 25 0 1 0 1793566992 136445952 31018 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 33312 31018 145 145 0 33167 0
[pid=26514] vsize: 133248
Current children cumulated CPU time (s) 647.34
Current children cumulated vsize (Kb) 135372

[startup+660.059 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 31739 0 2 0 65545 186 0 0 25 0 1 0 1793566992 137809920 31351 4294967295 134512640 135094434 3221224432 3221223104 134555602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 33645 31351 145 145 0 33500 0
[pid=26514] vsize: 134580
Current children cumulated CPU time (s) 657.32
Current children cumulated vsize (Kb) 136704

[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 31941 0 2 0 66542 188 0 0 25 0 1 0 1793566992 138637312 31553 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 33847 31553 145 145 0 33702 0
[pid=26514] vsize: 135388
Current children cumulated CPU time (s) 667.31
Current children cumulated vsize (Kb) 137512

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 32262 0 2 0 67538 190 0 0 25 0 1 0 1793566992 139948032 31874 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 34167 31874 145 145 0 34022 0
[pid=26514] vsize: 136668
Current children cumulated CPU time (s) 677.29
Current children cumulated vsize (Kb) 138792

[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 32594 0 2 0 68534 192 0 0 25 0 1 0 1793566992 141316096 32206 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 34501 32206 145 145 0 34356 0
[pid=26514] vsize: 138004
Current children cumulated CPU time (s) 687.27
Current children cumulated vsize (Kb) 140128

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 32866 0 2 0 69530 193 0 0 25 0 1 0 1793566992 142426112 32478 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 34772 32478 145 145 0 34627 0
[pid=26514] vsize: 139088
Current children cumulated CPU time (s) 697.24
Current children cumulated vsize (Kb) 141212

[startup+710.064 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 33071 0 2 0 70525 196 0 0 25 0 1 0 1793566992 143269888 32683 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 34978 32683 145 145 0 34833 0
[pid=26514] vsize: 139912
Current children cumulated CPU time (s) 707.22
Current children cumulated vsize (Kb) 142036

[startup+720.065 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 33340 0 2 0 71521 198 0 0 25 0 1 0 1793566992 144367616 32952 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 35246 32952 145 145 0 35101 0
[pid=26514] vsize: 140984
Current children cumulated CPU time (s) 717.2
Current children cumulated vsize (Kb) 143108

[startup+730.066 s]
Raw data (loadavg): 0.99 0.97 0.83 1/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) T 26510 26510 9854 0 -1 0 33630 0 2 0 72516 199 0 0 25 0 1 0 1793566992 145551360 33242 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26514/statm): 35535 33242 145 145 0 35390 0
[pid=26514] vsize: 142140
Current children cumulated CPU time (s) 727.16
Current children cumulated vsize (Kb) 144264

[startup+740.069 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 33940 0 2 0 73513 200 0 0 25 0 1 0 1793566992 146812928 33552 4294967295 134512640 135094434 3221224432 3221223024 134556866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 35843 33552 145 145 0 35698 0
[pid=26514] vsize: 143372
Current children cumulated CPU time (s) 737.14
Current children cumulated vsize (Kb) 145496

[startup+750.071 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 34239 0 2 0 74509 202 0 0 25 0 1 0 1793566992 148037632 33851 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 36142 33851 145 145 0 35997 0
[pid=26514] vsize: 144568
Current children cumulated CPU time (s) 747.12
Current children cumulated vsize (Kb) 146692

[startup+760.071 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 34541 0 2 0 75504 204 0 0 25 0 1 0 1793566992 149270528 34153 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 36443 34153 145 145 0 36298 0
[pid=26514] vsize: 145772
Current children cumulated CPU time (s) 757.09
Current children cumulated vsize (Kb) 147896

[startup+770.071 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 34869 0 2 0 76499 206 0 0 19 0 1 0 1793566992 150609920 34481 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 36770 34481 145 145 0 36625 0
[pid=26514] vsize: 147080
Current children cumulated CPU time (s) 767.06
Current children cumulated vsize (Kb) 149204

[startup+780.072 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 35158 0 2 0 77495 209 0 0 25 0 1 0 1793566992 151789568 34770 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 37058 34770 145 145 0 36913 0
[pid=26514] vsize: 148232
Current children cumulated CPU time (s) 777.05
Current children cumulated vsize (Kb) 150356

[startup+790.073 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 35423 0 2 0 78491 210 0 0 25 0 1 0 1793566992 152866816 35035 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 37321 35035 145 145 0 37176 0
[pid=26514] vsize: 149284
Current children cumulated CPU time (s) 787.02
Current children cumulated vsize (Kb) 151408

[startup+800.074 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 35795 0 2 0 79486 212 0 0 25 0 1 0 1793566992 154382336 35407 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 37691 35407 145 145 0 37546 0
[pid=26514] vsize: 150764
Current children cumulated CPU time (s) 796.99
Current children cumulated vsize (Kb) 152888

[startup+810.075 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 36085 0 2 0 80481 214 0 0 25 0 1 0 1793566992 155566080 35697 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 37980 35697 145 145 0 37835 0
[pid=26514] vsize: 151920
Current children cumulated CPU time (s) 806.96
Current children cumulated vsize (Kb) 154044

[startup+820.076 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 36358 0 2 0 81477 216 0 0 25 0 1 0 1793566992 156680192 35970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 38252 35970 145 145 0 38107 0
[pid=26514] vsize: 153008
Current children cumulated CPU time (s) 816.94
Current children cumulated vsize (Kb) 155132

[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 36623 0 2 0 82472 218 0 0 25 0 1 0 1793566992 157761536 36235 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 38516 36235 145 145 0 38371 0
[pid=26514] vsize: 154064
Current children cumulated CPU time (s) 826.91
Current children cumulated vsize (Kb) 156188

[startup+840.078 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 36900 0 2 0 83467 220 0 0 25 0 1 0 1793566992 158900224 36512 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 38794 36512 145 145 0 38649 0
[pid=26514] vsize: 155176
Current children cumulated CPU time (s) 836.88
Current children cumulated vsize (Kb) 157300

[startup+850.079 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 37354 0 2 0 84461 222 0 0 25 0 1 0 1793566992 160755712 36966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 39247 36966 145 145 0 39102 0
[pid=26514] vsize: 156988
Current children cumulated CPU time (s) 846.84
Current children cumulated vsize (Kb) 159112

[startup+860.08 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 37758 0 2 0 85458 224 0 0 25 0 1 0 1793566992 162406400 37370 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 39650 37370 145 145 0 39505 0
[pid=26514] vsize: 158600
Current children cumulated CPU time (s) 856.83
Current children cumulated vsize (Kb) 160724

[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.84 1/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) T 26510 26510 9854 0 -1 0 38144 0 2 0 86453 227 0 0 25 0 1 0 1793566992 163987456 37756 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26514/statm): 40036 37756 145 145 0 39891 0
[pid=26514] vsize: 160144
Current children cumulated CPU time (s) 866.81
Current children cumulated vsize (Kb) 162268

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 38442 0 2 0 87450 228 0 0 25 0 1 0 1793566992 165208064 38054 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 40334 38054 145 145 0 40189 0
[pid=26514] vsize: 161336
Current children cumulated CPU time (s) 876.79
Current children cumulated vsize (Kb) 163460

[startup+890.084 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 38712 0 2 0 88445 230 0 0 25 0 1 0 1793566992 166301696 38324 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 40601 38324 145 145 0 40456 0
[pid=26514] vsize: 162404
Current children cumulated CPU time (s) 886.76
Current children cumulated vsize (Kb) 164528

[startup+900.085 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 39042 0 2 0 89440 233 0 0 25 0 1 0 1793566992 167645184 38654 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 40929 38654 145 145 0 40784 0
[pid=26514] vsize: 163716
Current children cumulated CPU time (s) 896.74
Current children cumulated vsize (Kb) 165840

[startup+910.086 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 39296 0 2 0 90436 234 0 0 25 0 1 0 1793566992 168677376 38908 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 41181 38908 145 145 0 41036 0
[pid=26514] vsize: 164724
Current children cumulated CPU time (s) 906.71
Current children cumulated vsize (Kb) 166848

[startup+920.087 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 39688 0 2 0 91431 237 0 0 25 0 1 0 1793566992 170278912 39300 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 41572 39300 145 145 0 41427 0
[pid=26514] vsize: 166288
Current children cumulated CPU time (s) 916.69
Current children cumulated vsize (Kb) 168412

[startup+930.088 s]
Raw data (loadavg): 0.99 0.97 0.85 1/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) T 26510 26510 9854 0 -1 0 40091 0 2 0 92424 239 0 0 25 0 1 0 1793566992 171925504 39703 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26514/statm): 41974 39703 145 145 0 41829 0
[pid=26514] vsize: 167896
Current children cumulated CPU time (s) 926.64
Current children cumulated vsize (Kb) 170020

[startup+940.088 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) T 26510 26510 9854 0 -1 0 40498 0 2 0 93419 242 0 0 25 0 1 0 1793566992 173592576 40110 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26514/statm): 42381 40110 145 145 0 42236 0
[pid=26514] vsize: 169524
Current children cumulated CPU time (s) 936.62
Current children cumulated vsize (Kb) 171648

[startup+950.09 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 40881 0 2 0 94415 244 0 0 25 0 1 0 1793566992 175157248 40493 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 42763 40493 145 145 0 42618 0
[pid=26514] vsize: 171052
Current children cumulated CPU time (s) 946.6
Current children cumulated vsize (Kb) 173176

[startup+960.091 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 41313 0 2 0 95410 246 0 0 25 0 1 0 1793566992 176926720 40925 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 43195 40925 145 145 0 43050 0
[pid=26514] vsize: 172780
Current children cumulated CPU time (s) 956.57
Current children cumulated vsize (Kb) 174904

[startup+970.092 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 41709 0 2 0 96406 248 0 0 25 0 1 0 1793566992 178548736 41321 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 43591 41321 145 145 0 43446 0
[pid=26514] vsize: 174364
Current children cumulated CPU time (s) 966.55
Current children cumulated vsize (Kb) 176488

[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 42113 0 2 0 97402 250 0 0 25 0 1 0 1793566992 180195328 41725 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 43993 41725 145 145 0 43848 0
[pid=26514] vsize: 175972
Current children cumulated CPU time (s) 976.53
Current children cumulated vsize (Kb) 178096

[startup+990.093 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 42398 0 2 0 98400 251 0 0 25 0 1 0 1793566992 181358592 42010 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 44277 42010 145 145 0 44132 0
[pid=26514] vsize: 177108
Current children cumulated CPU time (s) 986.52
Current children cumulated vsize (Kb) 179232

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 42632 0 2 0 99396 253 0 0 25 0 1 0 1793566992 182312960 42244 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 44510 42244 145 145 0 44365 0
[pid=26514] vsize: 178040
Current children cumulated CPU time (s) 996.5
Current children cumulated vsize (Kb) 180164

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 42942 0 2 0 100390 255 0 0 25 0 1 0 1793566992 183578624 42554 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 44819 42554 145 145 0 44674 0
[pid=26514] vsize: 179276
Current children cumulated CPU time (s) 1006.46
Current children cumulated vsize (Kb) 181400

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 43263 0 2 0 101386 257 0 0 25 0 1 0 1793566992 184889344 42875 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26514/statm): 45139 42875 145 145 0 44994 0
[pid=26514] vsize: 180556
Current children cumulated CPU time (s) 1016.44
Current children cumulated vsize (Kb) 182680

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 43608 0 2 0 102380 259 0 0 25 0 1 0 1793566992 186298368 43220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 45483 43220 145 145 0 45338 0
[pid=26514] vsize: 181932
Current children cumulated CPU time (s) 1026.4
Current children cumulated vsize (Kb) 184056

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 43946 0 2 0 103375 262 0 0 25 0 1 0 1793566992 187678720 43558 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 45820 43558 145 145 0 45675 0
[pid=26514] vsize: 183280
Current children cumulated CPU time (s) 1036.38
Current children cumulated vsize (Kb) 185404

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 44335 0 2 0 104370 265 0 0 25 0 1 0 1793566992 189272064 43947 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26514/statm): 46209 43947 145 145 0 46064 0
[pid=26514] vsize: 184836
Current children cumulated CPU time (s) 1046.36
Current children cumulated vsize (Kb) 186960

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 44591 0 2 0 105366 266 0 0 25 0 1 0 1793566992 190853120 44203 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 46595 44203 145 145 0 46450 0
[pid=26514] vsize: 186380
Current children cumulated CPU time (s) 1056.33
Current children cumulated vsize (Kb) 188504

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 44871 0 2 0 106360 269 0 0 25 0 1 0 1793566992 192000000 44483 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 46875 44483 145 145 0 46730 0
[pid=26514] vsize: 187500
Current children cumulated CPU time (s) 1066.3
Current children cumulated vsize (Kb) 189624

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 45133 0 2 0 107356 270 0 0 25 0 1 0 1793566992 193069056 44745 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 47136 44745 145 145 0 46991 0
[pid=26514] vsize: 188544
Current children cumulated CPU time (s) 1076.27
Current children cumulated vsize (Kb) 190668

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 45414 0 2 0 108352 271 0 0 25 0 1 0 1793566992 194220032 45026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 47417 45026 145 145 0 47272 0
[pid=26514] vsize: 189668
Current children cumulated CPU time (s) 1086.24
Current children cumulated vsize (Kb) 191792

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 45695 0 2 0 109348 274 0 0 25 0 1 0 1793566992 195366912 45307 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 47697 45307 145 145 0 47552 0
[pid=26514] vsize: 190788
Current children cumulated CPU time (s) 1096.23
Current children cumulated vsize (Kb) 192912

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 46029 0 2 0 110343 276 0 0 25 0 1 0 1793566992 196726784 45641 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 48029 45641 145 145 0 47884 0
[pid=26514] vsize: 192116
Current children cumulated CPU time (s) 1106.2
Current children cumulated vsize (Kb) 194240

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 46379 0 2 0 111336 278 0 0 25 0 1 0 1793566992 198156288 45991 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 48378 45991 145 145 0 48233 0
[pid=26514] vsize: 193512
Current children cumulated CPU time (s) 1116.15
Current children cumulated vsize (Kb) 195636

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 46700 0 2 0 112332 280 0 0 25 0 1 0 1793566992 199467008 46312 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 48698 46312 145 145 0 48553 0
[pid=26514] vsize: 194792
Current children cumulated CPU time (s) 1126.13
Current children cumulated vsize (Kb) 196916

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 46980 0 2 0 113328 281 0 0 25 0 1 0 1793566992 200601600 46592 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 48975 46592 145 145 0 48830 0
[pid=26514] vsize: 195900
Current children cumulated CPU time (s) 1136.1
Current children cumulated vsize (Kb) 198024

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 47198 0 2 0 114324 283 0 0 25 0 1 0 1793566992 201490432 46810 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 49192 46810 145 145 0 49047 0
[pid=26514] vsize: 196768
Current children cumulated CPU time (s) 1146.08
Current children cumulated vsize (Kb) 198892

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 47459 0 2 0 115321 284 0 0 25 0 1 0 1793566992 202555392 47071 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 49452 47071 145 145 0 49307 0
[pid=26514] vsize: 197808
Current children cumulated CPU time (s) 1156.06
Current children cumulated vsize (Kb) 199932

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 47782 0 2 0 116316 286 0 0 25 0 1 0 1793566992 203886592 47394 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 49777 47394 145 145 0 49632 0
[pid=26514] vsize: 199108
Current children cumulated CPU time (s) 1166.03
Current children cumulated vsize (Kb) 201232

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 48136 0 2 0 117311 289 0 0 25 0 1 0 1793566992 205324288 47748 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 50128 47748 145 145 0 49983 0
[pid=26514] vsize: 200512
Current children cumulated CPU time (s) 1176.01
Current children cumulated vsize (Kb) 202636

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 48454 0 2 0 118307 290 0 0 25 0 1 0 1793566992 206626816 48066 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 50446 48066 145 145 0 50301 0
[pid=26514] vsize: 201784
Current children cumulated CPU time (s) 1185.98
Current children cumulated vsize (Kb) 203908

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 48731 0 2 0 119302 292 0 0 25 0 1 0 1793566992 207753216 48343 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 50721 48343 145 145 0 50576 0
[pid=26514] vsize: 202884
Current children cumulated CPU time (s) 1195.95
Current children cumulated vsize (Kb) 205008

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 49041 0 2 0 120298 293 0 0 25 0 1 0 1793566992 209018880 48653 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 51030 48653 145 145 0 50885 0
[pid=26514] vsize: 204120
Current children cumulated CPU time (s) 1205.92
Current children cumulated vsize (Kb) 206244



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26514
Raw data (/proc/26510/stat): 26510 (minisat+_script) S 26509 26510 9854 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793566986 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26510/statm): 531 226 485 147 0 384 0
[pid=26510] vsize: 2124
Raw data (/proc/26514/stat): 26514 (minisat+_64-bit) R 26510 26510 9854 0 -1 0 49041 0 2 0 120298 293 0 0 25 0 1 0 1793566992 209018880 48653 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26514/statm): 51030 48653 145 145 0 50885 0
[pid=26514] vsize: 204120
Current children cumulated CPU time (s) 1205.92
Current children cumulated vsize (Kb) 206244

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

Child status: 0
Real time (s): 1210.21
CPU time (s): 1206.01
CPU user time (s): 1202.99
CPU system time (s): 3.02554
CPU usage (%): 99.6534
Max. virtual memory (cumulated for all children) (Kb): 206244

Verifier Data

ERROR: no interpretation found !