Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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 6235

Launcher Data

LAUNCH ON wulflinc12 THE 2005-09-20 04:42:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3399 boxname=wulflinc12 idbench=1055 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  26490113618ae9605b5ebe6370b5910b  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 3399
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        901196 kB
Buffers:         33384 kB
Cached:          69280 kB
SwapCached:        492 kB
Active:          52500 kB
Inactive:        52712 kB
HighTotal:      131008 kB
HighFree:        59528 kB
LowTotal:       903652 kB
LowFree:        841668 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5892 kB
Slab:            22436 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:02:24 (client local time) WITH STATUS 0 IN 1206.2 SECONDS
stats: 3399 7 1206.2 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/12083/stat): 12083 (minisat+_script) R 12082 12083 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797501237 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12083/statm): 174 3 169 147 0 27 0
[pid=12083] 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=12084
New process pid=12085
New process pid=12086
execve syscall for /bin/sed executable
One traced child (pid=12085) 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=12086) exited with status: 0
One traced child (pid=12084) exited with status: 0
New process pid=12087
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-air04.opb

[startup+10.0037 s]
Raw data (loadavg): 1.03 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 10940 0 0 0 906 44 0 0 25 0 1 0 1797501242 52555776 10550 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 12831 10550 145 145 0 12686 0
[pid=12087] vsize: 51324
Current children cumulated CPU time (s) 9.5
Current children cumulated vsize (Kb) 53448

[startup+20.0046 s]
Raw data (loadavg): 1.03 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 11189 0 0 0 1900 47 0 0 25 0 1 0 1797501242 53538816 10799 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 13071 10799 145 145 0 12926 0
[pid=12087] vsize: 52284
Current children cumulated CPU time (s) 19.47
Current children cumulated vsize (Kb) 54408

[startup+30.0054 s]
Raw data (loadavg): 1.02 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 11534 0 0 0 2893 50 0 0 25 0 1 0 1797501242 54960128 11144 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 13418 11144 145 145 0 13273 0
[pid=12087] vsize: 53672
Current children cumulated CPU time (s) 29.43
Current children cumulated vsize (Kb) 55796

[startup+40.0063 s]
Raw data (loadavg): 1.02 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 12146 0 0 0 3880 57 0 0 25 0 1 0 1797501242 57458688 11756 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 14028 11756 145 145 0 13883 0
[pid=12087] vsize: 56112
Current children cumulated CPU time (s) 39.37
Current children cumulated vsize (Kb) 58236

[startup+50.0071 s]
Raw data (loadavg): 1.02 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 12619 0 0 0 4871 60 0 0 25 0 1 0 1797501242 59420672 12229 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 14507 12229 145 145 0 14362 0
[pid=12087] vsize: 58028
Current children cumulated CPU time (s) 49.31
Current children cumulated vsize (Kb) 60152

[startup+60.0079 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 12875 0 0 0 5866 63 0 0 25 0 1 0 1797501242 60461056 12485 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 14761 12485 145 145 0 14616 0
[pid=12087] vsize: 59044
Current children cumulated CPU time (s) 59.29
Current children cumulated vsize (Kb) 61168

[startup+70.0088 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 13118 0 0 0 6862 65 0 0 25 0 1 0 1797501242 61448192 12728 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 15002 12728 145 145 0 14857 0
[pid=12087] vsize: 60008
Current children cumulated CPU time (s) 69.27
Current children cumulated vsize (Kb) 62132

[startup+80.0096 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 13401 0 0 0 7856 68 0 0 25 0 1 0 1797501242 62599168 13011 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 15283 13011 145 145 0 15138 0
[pid=12087] vsize: 61132
Current children cumulated CPU time (s) 79.24
Current children cumulated vsize (Kb) 63256

[startup+90.0104 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 13646 0 0 0 8852 70 0 0 25 0 1 0 1797501242 63660032 13256 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 15542 13256 145 145 0 15397 0
[pid=12087] vsize: 62168
Current children cumulated CPU time (s) 89.22
Current children cumulated vsize (Kb) 64292

[startup+100.011 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 13992 0 0 0 9846 72 0 0 25 0 1 0 1797501242 65069056 13602 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 15886 13602 145 145 0 15741 0
[pid=12087] vsize: 63544
Current children cumulated CPU time (s) 99.18
Current children cumulated vsize (Kb) 65668

[startup+110.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 14350 0 0 0 10840 74 0 0 25 0 1 0 1797501242 66527232 13960 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 16242 13960 145 145 0 16097 0
[pid=12087] vsize: 64968
Current children cumulated CPU time (s) 109.14
Current children cumulated vsize (Kb) 67092

[startup+120.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 14797 0 0 0 11832 78 0 0 25 0 1 0 1797501242 68349952 14407 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 16687 14407 145 145 0 16542 0
[pid=12087] vsize: 66748
Current children cumulated CPU time (s) 119.1
Current children cumulated vsize (Kb) 68872

[startup+130.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 15042 0 0 0 12827 80 0 0 25 0 1 0 1797501242 69345280 14652 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 16930 14652 145 145 0 16785 0
[pid=12087] vsize: 67720
Current children cumulated CPU time (s) 129.07
Current children cumulated vsize (Kb) 69844

[startup+140.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 15314 0 0 0 13821 83 0 0 25 0 1 0 1797501242 70455296 14924 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 17201 14924 145 145 0 17056 0
[pid=12087] vsize: 68804
Current children cumulated CPU time (s) 139.04
Current children cumulated vsize (Kb) 70928

[startup+150.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 15615 0 0 0 14816 85 0 0 25 0 1 0 1797501242 71680000 15225 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 17500 15225 145 145 0 17355 0
[pid=12087] vsize: 70000
Current children cumulated CPU time (s) 149.01
Current children cumulated vsize (Kb) 72124

[startup+160.016 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 16037 0 0 0 15808 88 0 0 25 0 1 0 1797501242 73404416 15647 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 17921 15647 145 145 0 17776 0
[pid=12087] vsize: 71684
Current children cumulated CPU time (s) 158.96
Current children cumulated vsize (Kb) 73808

[startup+170.017 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 16288 0 0 0 16803 90 0 0 25 0 1 0 1797501242 74407936 15898 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 18166 15898 145 145 0 18021 0
[pid=12087] vsize: 72664
Current children cumulated CPU time (s) 168.93
Current children cumulated vsize (Kb) 74788

[startup+180.018 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 16674 0 0 0 17797 93 0 0 25 0 1 0 1797501242 76115968 16284 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 18583 16284 145 145 0 18438 0
[pid=12087] vsize: 74332
Current children cumulated CPU time (s) 178.9
Current children cumulated vsize (Kb) 76456

[startup+190.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 16877 0 0 0 18794 94 0 0 25 0 1 0 1797501242 76943360 16487 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 18785 16487 145 145 0 18640 0
[pid=12087] vsize: 75140
Current children cumulated CPU time (s) 188.88
Current children cumulated vsize (Kb) 77264

[startup+200.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 17230 0 0 0 19788 97 0 0 25 0 1 0 1797501242 78381056 16840 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 19136 16840 145 145 0 18991 0
[pid=12087] vsize: 76544
Current children cumulated CPU time (s) 198.85
Current children cumulated vsize (Kb) 78668

[startup+210.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 17633 0 0 0 20781 99 0 0 25 0 1 0 1797501242 80023552 17243 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 19537 17243 145 145 0 19392 0
[pid=12087] vsize: 78148
Current children cumulated CPU time (s) 208.8
Current children cumulated vsize (Kb) 80272

[startup+220.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 17923 0 0 0 21776 101 0 0 25 0 1 0 1797501242 81195008 17533 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 19823 17533 145 145 0 19678 0
[pid=12087] vsize: 79292
Current children cumulated CPU time (s) 218.77
Current children cumulated vsize (Kb) 81416

[startup+230.021 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 18141 0 0 0 22771 103 0 0 25 0 1 0 1797501242 82087936 17751 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 20041 17751 145 145 0 19896 0
[pid=12087] vsize: 80164
Current children cumulated CPU time (s) 228.74
Current children cumulated vsize (Kb) 82288

[startup+240.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 18408 0 0 0 23766 106 0 0 25 0 1 0 1797501242 83152896 18018 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 20301 18018 145 145 0 20156 0
[pid=12087] vsize: 81204
Current children cumulated CPU time (s) 238.72
Current children cumulated vsize (Kb) 83328

[startup+250.023 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 18778 0 0 0 24760 109 0 0 25 0 1 0 1797501242 84652032 18388 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 20667 18388 145 145 0 20522 0
[pid=12087] vsize: 82668
Current children cumulated CPU time (s) 248.69
Current children cumulated vsize (Kb) 84792

[startup+260.024 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 19122 0 0 0 25754 112 0 0 25 0 1 0 1797501242 86061056 18732 4294967295 134512640 135094434 3221224432 3221223024 134556765 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 21011 18732 145 145 0 20866 0
[pid=12087] vsize: 84044
Current children cumulated CPU time (s) 258.66
Current children cumulated vsize (Kb) 86168

[startup+270.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 19560 0 0 0 26747 115 0 0 25 0 1 0 1797501242 87851008 19170 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 21448 19170 145 145 0 21303 0
[pid=12087] vsize: 85792
Current children cumulated CPU time (s) 268.62
Current children cumulated vsize (Kb) 87916

[startup+280.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 19839 0 0 0 27742 117 0 0 25 0 1 0 1797501242 88985600 19449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 21725 19449 145 145 0 21580 0
[pid=12087] vsize: 86900
Current children cumulated CPU time (s) 278.59
Current children cumulated vsize (Kb) 89024

[startup+290.026 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 19999 0 0 0 28738 118 0 0 25 0 1 0 1797501242 89636864 19609 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 21884 19609 145 145 0 21739 0
[pid=12087] vsize: 87536
Current children cumulated CPU time (s) 288.56
Current children cumulated vsize (Kb) 89660

[startup+300.026 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 20283 0 0 0 29735 119 0 0 25 0 1 0 1797501242 90800128 19893 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 22168 19893 145 145 0 22023 0
[pid=12087] vsize: 88672
Current children cumulated CPU time (s) 298.54
Current children cumulated vsize (Kb) 90796

[startup+310.027 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) T 12083 12083 8263 0 -1 0 20574 0 0 0 30729 121 0 0 25 0 1 0 1797501242 91983872 20184 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12087/statm): 22457 20184 145 145 0 22312 0
[pid=12087] vsize: 89828
Current children cumulated CPU time (s) 308.5
Current children cumulated vsize (Kb) 91952

[startup+320.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 20937 0 0 0 31724 123 0 0 25 0 1 0 1797501242 93466624 20547 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 22819 20547 145 145 0 22674 0
[pid=12087] vsize: 91276
Current children cumulated CPU time (s) 318.47
Current children cumulated vsize (Kb) 93400

[startup+330.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 21211 0 0 0 32720 125 0 0 25 0 1 0 1797501242 94593024 20821 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 23094 20821 145 145 0 22949 0
[pid=12087] vsize: 92376
Current children cumulated CPU time (s) 328.45
Current children cumulated vsize (Kb) 94500

[startup+340.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 21453 0 0 0 33716 127 0 0 25 0 1 0 1797501242 95580160 21063 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 23335 21063 145 145 0 23190 0
[pid=12087] vsize: 93340
Current children cumulated CPU time (s) 338.43
Current children cumulated vsize (Kb) 95464

[startup+350.029 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 21779 0 0 0 34710 129 0 0 25 0 1 0 1797501242 96911360 21389 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 23660 21389 145 145 0 23515 0
[pid=12087] vsize: 94640
Current children cumulated CPU time (s) 348.39
Current children cumulated vsize (Kb) 96764

[startup+360.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 22043 0 0 0 35704 131 0 0 25 0 1 0 1797501242 97984512 21653 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 23922 21653 145 145 0 23777 0
[pid=12087] vsize: 95688
Current children cumulated CPU time (s) 358.35
Current children cumulated vsize (Kb) 97812

[startup+370.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 22310 0 0 0 36700 133 0 0 25 0 1 0 1797501242 99074048 21920 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 24188 21920 145 145 0 24043 0
[pid=12087] vsize: 96752
Current children cumulated CPU time (s) 368.33
Current children cumulated vsize (Kb) 98876

[startup+380.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 22919 0 0 0 37692 137 0 0 25 0 1 0 1797501242 101568512 22529 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 24797 22529 145 145 0 24652 0
[pid=12087] vsize: 99188
Current children cumulated CPU time (s) 378.29
Current children cumulated vsize (Kb) 101312

[startup+390.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 23297 0 0 0 38686 140 0 0 25 0 1 0 1797501242 103108608 22907 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 25173 22907 145 145 0 25028 0
[pid=12087] vsize: 100692
Current children cumulated CPU time (s) 388.26
Current children cumulated vsize (Kb) 102816

[startup+400.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 23523 0 0 0 39682 141 0 0 25 0 1 0 1797501242 104030208 23133 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 25398 23133 145 145 0 25253 0
[pid=12087] vsize: 101592
Current children cumulated CPU time (s) 398.23
Current children cumulated vsize (Kb) 103716

[startup+410.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 23823 0 0 0 40677 143 0 0 25 0 1 0 1797501242 105222144 23433 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 25689 23433 145 145 0 25544 0
[pid=12087] vsize: 102756
Current children cumulated CPU time (s) 408.2
Current children cumulated vsize (Kb) 104880

[startup+420.036 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 24142 0 0 0 41671 146 0 0 25 0 1 0 1797501242 106782720 23752 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 26070 23752 145 145 0 25925 0
[pid=12087] vsize: 104280
Current children cumulated CPU time (s) 418.17
Current children cumulated vsize (Kb) 106404

[startup+430.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 24517 0 0 0 42666 147 0 0 25 0 1 0 1797501242 108314624 24127 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 26444 24127 145 145 0 26299 0
[pid=12087] vsize: 105776
Current children cumulated CPU time (s) 428.13
Current children cumulated vsize (Kb) 107900

[startup+440.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 24922 0 0 0 43660 150 0 0 25 0 1 0 1797501242 109969408 24532 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 26848 24532 145 145 0 26703 0
[pid=12087] vsize: 107392
Current children cumulated CPU time (s) 438.1
Current children cumulated vsize (Kb) 109516

[startup+450.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 25260 0 0 0 44655 152 0 0 25 0 1 0 1797501242 111353856 24870 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 27186 24870 145 145 0 27041 0
[pid=12087] vsize: 108744
Current children cumulated CPU time (s) 448.07
Current children cumulated vsize (Kb) 110868

[startup+460.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 25502 0 0 0 45651 154 0 0 25 0 1 0 1797501242 112340992 25112 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 27427 25112 145 145 0 27282 0
[pid=12087] vsize: 109708
Current children cumulated CPU time (s) 458.05
Current children cumulated vsize (Kb) 111832

[startup+470.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 25776 0 0 0 46646 156 0 0 25 0 1 0 1797501242 113463296 25386 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 27701 25386 145 145 0 27556 0
[pid=12087] vsize: 110804
Current children cumulated CPU time (s) 468.02
Current children cumulated vsize (Kb) 112928

[startup+480.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 25993 0 0 0 47643 158 0 0 25 0 1 0 1797501242 114348032 25603 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 27917 25603 145 145 0 27772 0
[pid=12087] vsize: 111668
Current children cumulated CPU time (s) 478.01
Current children cumulated vsize (Kb) 113792

[startup+490.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 26299 0 0 0 48637 161 0 0 25 0 1 0 1797501242 115593216 25909 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 28221 25909 145 145 0 28076 0
[pid=12087] vsize: 112884
Current children cumulated CPU time (s) 487.98
Current children cumulated vsize (Kb) 115008

[startup+500.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 26637 0 0 0 49632 163 0 0 25 0 1 0 1797501242 116973568 26247 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 28558 26247 145 145 0 28413 0
[pid=12087] vsize: 114232
Current children cumulated CPU time (s) 497.95
Current children cumulated vsize (Kb) 116356

[startup+510.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 26898 0 0 0 50628 164 0 0 25 0 1 0 1797501242 118042624 26508 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 28819 26508 145 145 0 28674 0
[pid=12087] vsize: 115276
Current children cumulated CPU time (s) 507.92
Current children cumulated vsize (Kb) 117400

[startup+520.043 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 27126 0 0 0 51625 165 0 0 25 0 1 0 1797501242 118968320 26736 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 29045 26736 145 145 0 28900 0
[pid=12087] vsize: 116180
Current children cumulated CPU time (s) 517.9
Current children cumulated vsize (Kb) 118304

[startup+530.043 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 27499 0 0 0 52619 169 0 0 25 0 1 0 1797501242 120496128 27109 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 29418 27109 145 145 0 29273 0
[pid=12087] vsize: 117672
Current children cumulated CPU time (s) 527.88
Current children cumulated vsize (Kb) 119796

[startup+540.044 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 27777 0 0 0 53615 170 0 0 25 0 1 0 1797501242 121622528 27387 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 29693 27387 145 145 0 29548 0
[pid=12087] vsize: 118772
Current children cumulated CPU time (s) 537.85
Current children cumulated vsize (Kb) 120896

[startup+550.045 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 28068 0 0 0 54610 172 0 0 25 0 1 0 1797501242 122810368 27678 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 29983 27678 145 145 0 29838 0
[pid=12087] vsize: 119932
Current children cumulated CPU time (s) 547.82
Current children cumulated vsize (Kb) 122056

[startup+560.046 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 28329 0 0 0 55606 173 0 0 25 0 1 0 1797501242 123875328 27939 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 30243 27939 145 145 0 30098 0
[pid=12087] vsize: 120972
Current children cumulated CPU time (s) 557.79
Current children cumulated vsize (Kb) 123096

[startup+570.047 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) T 12083 12083 8263 0 -1 0 28616 0 0 0 56602 175 0 0 25 0 1 0 1797501242 125050880 28226 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12087/statm): 30530 28226 145 145 0 30385 0
[pid=12087] vsize: 122120
Current children cumulated CPU time (s) 567.77
Current children cumulated vsize (Kb) 124244

[startup+580.048 s]
Raw data (loadavg): 1.00 0.99 0.95 1/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) T 12083 12083 8263 0 -1 0 28895 0 0 0 57598 177 0 0 25 0 1 0 1797501242 126189568 28505 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12087/statm): 30808 28505 145 145 0 30663 0
[pid=12087] vsize: 123232
Current children cumulated CPU time (s) 577.75
Current children cumulated vsize (Kb) 125356

[startup+590.048 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 29185 0 0 0 58594 178 0 0 25 0 1 0 1797501242 127373312 28795 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 31097 28795 145 145 0 30952 0
[pid=12087] vsize: 124388
Current children cumulated CPU time (s) 587.72
Current children cumulated vsize (Kb) 126512

[startup+600.048 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 29431 0 0 0 59590 180 0 0 25 0 1 0 1797501242 128376832 29041 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 31342 29041 145 145 0 31197 0
[pid=12087] vsize: 125368
Current children cumulated CPU time (s) 597.7
Current children cumulated vsize (Kb) 127492

[startup+610.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 29777 0 0 0 60584 182 0 0 25 0 1 0 1797501242 129785856 29387 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 31686 29387 145 145 0 31541 0
[pid=12087] vsize: 126744
Current children cumulated CPU time (s) 607.66
Current children cumulated vsize (Kb) 128868

[startup+620.051 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 30043 0 0 0 61580 184 0 0 25 0 1 0 1797501242 130871296 29653 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 31951 29653 145 145 0 31806 0
[pid=12087] vsize: 127804
Current children cumulated CPU time (s) 617.64
Current children cumulated vsize (Kb) 129928

[startup+630.052 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 30445 0 0 0 62574 186 0 0 25 0 1 0 1797501242 132509696 30055 4294967295 134512640 135094434 3221224432 3221223088 134557823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 32351 30055 145 145 0 32206 0
[pid=12087] vsize: 129404
Current children cumulated CPU time (s) 627.6
Current children cumulated vsize (Kb) 131528

[startup+640.053 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 30782 0 0 0 63569 189 0 0 25 0 1 0 1797501242 133885952 30392 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 32687 30392 145 145 0 32542 0
[pid=12087] vsize: 130748
Current children cumulated CPU time (s) 637.58
Current children cumulated vsize (Kb) 132872

[startup+650.053 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 31111 0 0 0 64565 191 0 0 25 0 1 0 1797501242 135229440 30721 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 33015 30721 145 145 0 32870 0
[pid=12087] vsize: 132060
Current children cumulated CPU time (s) 647.56
Current children cumulated vsize (Kb) 134184

[startup+660.054 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 31486 0 0 0 65558 193 0 0 25 0 1 0 1797501242 136761344 31096 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 33389 31096 145 145 0 33244 0
[pid=12087] vsize: 133556
Current children cumulated CPU time (s) 657.51
Current children cumulated vsize (Kb) 135680

[startup+670.055 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 31790 0 0 0 66552 195 0 0 25 0 1 0 1797501242 138010624 31400 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 33694 31400 145 145 0 33549 0
[pid=12087] vsize: 134776
Current children cumulated CPU time (s) 667.47
Current children cumulated vsize (Kb) 136900

[startup+680.055 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 32007 0 0 0 67549 197 0 0 25 0 1 0 1797501242 138895360 31617 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 33910 31617 145 145 0 33765 0
[pid=12087] vsize: 135640
Current children cumulated CPU time (s) 677.46
Current children cumulated vsize (Kb) 137764

[startup+690.056 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 32327 0 0 0 68545 198 0 0 25 0 1 0 1797501242 140230656 31937 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 34236 31937 145 145 0 34091 0
[pid=12087] vsize: 136944
Current children cumulated CPU time (s) 687.43
Current children cumulated vsize (Kb) 139068

[startup+700.057 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 32632 0 0 0 69542 200 0 0 25 0 1 0 1797501242 141463552 32242 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 34537 32242 145 145 0 34392 0
[pid=12087] vsize: 138148
Current children cumulated CPU time (s) 697.42
Current children cumulated vsize (Kb) 140272

[startup+710.058 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 32890 0 0 0 70537 202 0 0 25 0 1 0 1797501242 142516224 32500 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 34794 32500 145 145 0 34649 0
[pid=12087] vsize: 139176
Current children cumulated CPU time (s) 707.39
Current children cumulated vsize (Kb) 141300

[startup+720.059 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 33108 0 0 0 71532 204 0 0 25 0 1 0 1797501242 143413248 32718 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 35013 32718 145 145 0 34868 0
[pid=12087] vsize: 140052
Current children cumulated CPU time (s) 717.36
Current children cumulated vsize (Kb) 142176

[startup+730.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 33369 0 0 0 72526 207 0 0 25 0 1 0 1797501242 144478208 32979 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 35273 32979 145 145 0 35128 0
[pid=12087] vsize: 141092
Current children cumulated CPU time (s) 727.33
Current children cumulated vsize (Kb) 143216

[startup+740.061 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 33661 0 0 0 73522 209 0 0 25 0 1 0 1797501242 145666048 33271 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 35563 33271 145 145 0 35418 0
[pid=12087] vsize: 142252
Current children cumulated CPU time (s) 737.31
Current children cumulated vsize (Kb) 144376

[startup+750.062 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 33971 0 0 0 74517 211 0 0 25 0 1 0 1797501242 146931712 33581 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 35872 33581 145 145 0 35727 0
[pid=12087] vsize: 143488
Current children cumulated CPU time (s) 747.28
Current children cumulated vsize (Kb) 145612

[startup+760.064 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 34277 0 0 0 75512 214 0 0 25 0 1 0 1797501242 148185088 33887 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 36178 33887 145 145 0 36033 0
[pid=12087] vsize: 144712
Current children cumulated CPU time (s) 757.26
Current children cumulated vsize (Kb) 146836

[startup+770.065 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 34554 0 0 0 76507 216 0 0 25 0 1 0 1797501242 149315584 34164 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 36454 34164 145 145 0 36309 0
[pid=12087] vsize: 145816
Current children cumulated CPU time (s) 767.23
Current children cumulated vsize (Kb) 147940

[startup+780.064 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 34915 0 0 0 77503 218 0 0 25 0 1 0 1797501242 150790144 34525 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 36814 34525 145 145 0 36669 0
[pid=12087] vsize: 147256
Current children cumulated CPU time (s) 777.21
Current children cumulated vsize (Kb) 149380

[startup+790.065 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 35185 0 0 0 78498 220 0 0 25 0 1 0 1797501242 151891968 34795 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 37083 34795 145 145 0 36938 0
[pid=12087] vsize: 148332
Current children cumulated CPU time (s) 787.18
Current children cumulated vsize (Kb) 150456

[startup+800.066 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 35448 0 0 0 79493 222 0 0 25 0 1 0 1797501242 152961024 35058 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 37344 35058 145 145 0 37199 0
[pid=12087] vsize: 149376
Current children cumulated CPU time (s) 797.15
Current children cumulated vsize (Kb) 151500

[startup+810.067 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 35825 0 0 0 80486 224 0 0 25 0 1 0 1797501242 154497024 35435 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 37719 35435 145 145 0 37574 0
[pid=12087] vsize: 150876
Current children cumulated CPU time (s) 807.1
Current children cumulated vsize (Kb) 153000

[startup+820.068 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 36087 0 0 0 81482 226 0 0 25 0 1 0 1797501242 155566080 35697 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 37980 35697 145 145 0 37835 0
[pid=12087] vsize: 151920
Current children cumulated CPU time (s) 817.08
Current children cumulated vsize (Kb) 154044

[startup+830.069 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 36368 0 0 0 82477 227 0 0 25 0 1 0 1797501242 156712960 35978 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 38260 35978 145 145 0 38115 0
[pid=12087] vsize: 153040
Current children cumulated CPU time (s) 827.04
Current children cumulated vsize (Kb) 155164

[startup+840.069 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 36630 0 0 0 83474 228 0 0 25 0 1 0 1797501242 157782016 36240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 38521 36240 145 145 0 38376 0
[pid=12087] vsize: 154084
Current children cumulated CPU time (s) 837.02
Current children cumulated vsize (Kb) 156208

[startup+850.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 36902 0 0 0 84471 230 0 0 25 0 1 0 1797501242 158900224 36512 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 38794 36512 145 145 0 38649 0
[pid=12087] vsize: 155176
Current children cumulated CPU time (s) 847.01
Current children cumulated vsize (Kb) 157300

[startup+860.071 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 37349 0 0 0 85465 233 0 0 25 0 1 0 1797501242 160727040 36959 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 39240 36959 145 145 0 39095 0
[pid=12087] vsize: 156960
Current children cumulated CPU time (s) 856.98
Current children cumulated vsize (Kb) 159084

[startup+870.072 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 37750 0 0 0 86460 235 0 0 25 0 1 0 1797501242 162365440 37360 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 39640 37360 145 145 0 39495 0
[pid=12087] vsize: 158560
Current children cumulated CPU time (s) 866.95
Current children cumulated vsize (Kb) 160684

[startup+880.073 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 38127 0 0 0 87454 238 0 0 25 0 1 0 1797501242 163905536 37737 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 40016 37737 145 145 0 39871 0
[pid=12087] vsize: 160064
Current children cumulated CPU time (s) 876.92
Current children cumulated vsize (Kb) 162188

[startup+890.074 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 38428 0 0 0 88450 239 0 0 25 0 1 0 1797501242 165138432 38038 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 40317 38038 145 145 0 40172 0
[pid=12087] vsize: 161268
Current children cumulated CPU time (s) 886.89
Current children cumulated vsize (Kb) 163392

[startup+900.074 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 38701 0 0 0 89445 241 0 0 25 0 1 0 1797501242 166248448 38311 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 40588 38311 145 145 0 40443 0
[pid=12087] vsize: 162352
Current children cumulated CPU time (s) 896.86
Current children cumulated vsize (Kb) 164476

[startup+910.076 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 39017 0 0 0 90440 242 0 0 25 0 1 0 1797501242 167534592 38627 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 40902 38627 145 145 0 40757 0
[pid=12087] vsize: 163608
Current children cumulated CPU time (s) 906.82
Current children cumulated vsize (Kb) 165732

[startup+920.077 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 39268 0 0 0 91437 244 0 0 25 0 1 0 1797501242 168554496 38878 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 41151 38878 145 145 0 41006 0
[pid=12087] vsize: 164604
Current children cumulated CPU time (s) 916.81
Current children cumulated vsize (Kb) 166728

[startup+930.077 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 39654 0 0 0 92432 246 0 0 25 0 1 0 1797501242 170131456 39264 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 41536 39264 145 145 0 41391 0
[pid=12087] vsize: 166144
Current children cumulated CPU time (s) 926.78
Current children cumulated vsize (Kb) 168268

[startup+940.078 s]
Raw data (loadavg): 1.00 0.99 0.95 1/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) T 12083 12083 8263 0 -1 0 40045 0 0 0 93425 249 0 0 25 0 1 0 1797501242 171737088 39655 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12087/statm): 41928 39655 145 145 0 41783 0
[pid=12087] vsize: 167712
Current children cumulated CPU time (s) 936.74
Current children cumulated vsize (Kb) 169836

[startup+950.079 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 40444 0 0 0 94421 251 0 0 25 0 1 0 1797501242 173363200 40054 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 42325 40054 145 145 0 42180 0
[pid=12087] vsize: 169300
Current children cumulated CPU time (s) 946.72
Current children cumulated vsize (Kb) 171424

[startup+960.08 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 40824 0 0 0 95418 253 0 0 25 0 1 0 1797501242 174915584 40434 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 42704 40434 145 145 0 42559 0
[pid=12087] vsize: 170816
Current children cumulated CPU time (s) 956.71
Current children cumulated vsize (Kb) 172940

[startup+970.083 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 41256 0 0 0 96413 255 0 0 25 0 1 0 1797501242 176685056 40866 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 43136 40866 145 145 0 42991 0
[pid=12087] vsize: 172544
Current children cumulated CPU time (s) 966.68
Current children cumulated vsize (Kb) 174668

[startup+980.083 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 41649 0 0 0 97409 256 0 0 25 0 1 0 1797501242 178294784 41259 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 43529 41259 145 145 0 43384 0
[pid=12087] vsize: 174116
Current children cumulated CPU time (s) 976.65
Current children cumulated vsize (Kb) 176240

[startup+990.084 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 42047 0 0 0 98406 258 0 0 25 0 1 0 1797501242 179920896 41657 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 43926 41657 145 145 0 43781 0
[pid=12087] vsize: 175704
Current children cumulated CPU time (s) 986.64
Current children cumulated vsize (Kb) 177828

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 42344 0 0 0 99403 259 0 0 25 0 1 0 1797501242 181129216 41954 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 44221 41954 145 145 0 44076 0
[pid=12087] vsize: 176884
Current children cumulated CPU time (s) 996.62
Current children cumulated vsize (Kb) 179008

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 42571 0 0 0 100400 261 0 0 25 0 1 0 1797501242 182059008 42181 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 44448 42181 145 145 0 44303 0
[pid=12087] vsize: 177792
Current children cumulated CPU time (s) 1006.61
Current children cumulated vsize (Kb) 179916

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 42875 0 0 0 101394 263 0 0 25 0 1 0 1797501242 183296000 42485 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 44750 42485 145 145 0 44605 0
[pid=12087] vsize: 179000
Current children cumulated CPU time (s) 1016.57
Current children cumulated vsize (Kb) 181124

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 43204 0 0 0 102389 266 0 0 25 0 1 0 1797501242 184639488 42814 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 45078 42814 145 145 0 44933 0
[pid=12087] vsize: 180312
Current children cumulated CPU time (s) 1026.55
Current children cumulated vsize (Kb) 182436

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 43529 0 0 0 103384 268 0 0 25 0 1 0 1797501242 185970688 43139 4294967295 134512640 135094434 3221224432 3221223024 134556918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 45403 43139 145 145 0 45258 0
[pid=12087] vsize: 181612
Current children cumulated CPU time (s) 1036.52
Current children cumulated vsize (Kb) 183736

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 43882 0 0 0 104378 271 0 0 25 0 1 0 1797501242 187412480 43492 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 45755 43492 145 145 0 45610 0
[pid=12087] vsize: 183020
Current children cumulated CPU time (s) 1046.49
Current children cumulated vsize (Kb) 185144

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 44281 0 0 0 105375 273 0 0 25 0 1 0 1797501242 189042688 43891 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 46153 43891 145 145 0 46008 0
[pid=12087] vsize: 184612
Current children cumulated CPU time (s) 1056.48
Current children cumulated vsize (Kb) 186736

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 44547 0 0 0 106370 275 0 0 25 0 1 0 1797501242 190672896 44157 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 46551 44157 145 145 0 46406 0
[pid=12087] vsize: 186204
Current children cumulated CPU time (s) 1066.45
Current children cumulated vsize (Kb) 188328

[startup+1080.1 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 44818 0 0 0 107365 278 0 0 25 0 1 0 1797501242 191774720 44428 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 46820 44428 145 145 0 46675 0
[pid=12087] vsize: 187280
Current children cumulated CPU time (s) 1076.43
Current children cumulated vsize (Kb) 189404

[startup+1090.1 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 45085 0 0 0 108361 280 0 0 25 0 1 0 1797501242 192868352 44695 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 47087 44695 145 145 0 46942 0
[pid=12087] vsize: 188348
Current children cumulated CPU time (s) 1086.41
Current children cumulated vsize (Kb) 190472

[startup+1100.1 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 45368 0 0 0 109356 283 0 0 25 0 1 0 1797501242 194023424 44978 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 47369 44978 145 145 0 47224 0
[pid=12087] vsize: 189476
Current children cumulated CPU time (s) 1096.39
Current children cumulated vsize (Kb) 191600

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.95 1/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) T 12083 12083 8263 0 -1 0 45626 0 0 0 110353 284 0 0 25 0 1 0 1797501242 195076096 45236 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12087/statm): 47626 45236 145 145 0 47481 0
[pid=12087] vsize: 190504
Current children cumulated CPU time (s) 1106.37
Current children cumulated vsize (Kb) 192628

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 45963 0 0 0 111346 287 0 0 25 0 1 0 1797501242 196448256 45573 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 47961 45573 145 145 0 47816 0
[pid=12087] vsize: 191844
Current children cumulated CPU time (s) 1116.33
Current children cumulated vsize (Kb) 193968

[startup+1130.1 s]
Raw data (loadavg): 1.08 1.00 0.95 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 46298 0 0 0 112340 290 0 0 25 0 1 0 1797501242 197816320 45908 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 48295 45908 145 145 0 48150 0
[pid=12087] vsize: 193180
Current children cumulated CPU time (s) 1126.3
Current children cumulated vsize (Kb) 195304

[startup+1140.1 s]
Raw data (loadavg): 1.14 1.02 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 46618 0 0 0 113334 292 0 0 25 0 1 0 1797501242 199122944 46228 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 48614 46228 145 145 0 48469 0
[pid=12087] vsize: 194456
Current children cumulated CPU time (s) 1136.26
Current children cumulated vsize (Kb) 196580

[startup+1150.1 s]
Raw data (loadavg): 1.12 1.02 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 46952 0 0 0 114329 295 0 0 25 0 1 0 1797501242 200482816 46562 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 48946 46562 145 145 0 48801 0
[pid=12087] vsize: 195784
Current children cumulated CPU time (s) 1146.24
Current children cumulated vsize (Kb) 197908

[startup+1160.1 s]
Raw data (loadavg): 1.10 1.02 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 47155 0 0 0 115326 296 0 0 25 0 1 0 1797501242 201306112 46765 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 49147 46765 145 145 0 49002 0
[pid=12087] vsize: 196588
Current children cumulated CPU time (s) 1156.22
Current children cumulated vsize (Kb) 198712

[startup+1170.1 s]
Raw data (loadavg): 1.08 1.02 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 47394 0 0 0 116323 297 0 0 25 0 1 0 1797501242 202280960 47004 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 49385 47004 145 145 0 49240 0
[pid=12087] vsize: 197540
Current children cumulated CPU time (s) 1166.2
Current children cumulated vsize (Kb) 199664

[startup+1180.1 s]
Raw data (loadavg): 1.07 1.02 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 47692 0 0 0 117318 299 0 0 25 0 1 0 1797501242 203501568 47302 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 49683 47302 145 145 0 49538 0
[pid=12087] vsize: 198732
Current children cumulated CPU time (s) 1176.17
Current children cumulated vsize (Kb) 200856

[startup+1190.1 s]
Raw data (loadavg): 1.06 1.01 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 48035 0 0 0 118313 302 0 0 25 0 1 0 1797501242 204910592 47645 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 50027 47645 145 145 0 49882 0
[pid=12087] vsize: 200108
Current children cumulated CPU time (s) 1186.15
Current children cumulated vsize (Kb) 202232

[startup+1200.11 s]
Raw data (loadavg): 1.05 1.01 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 48391 0 0 0 119307 305 0 0 25 0 1 0 1797501242 206360576 48001 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12087/statm): 50381 48001 145 145 0 50236 0
[pid=12087] vsize: 201524
Current children cumulated CPU time (s) 1196.12
Current children cumulated vsize (Kb) 203648

[startup+1210.11 s]
Raw data (loadavg): 1.04 1.01 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 48623 0 0 0 120303 307 0 0 25 0 1 0 1797501242 207302656 48233 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 50611 48233 145 145 0 50466 0
[pid=12087] vsize: 202444
Current children cumulated CPU time (s) 1206.1
Current children cumulated vsize (Kb) 204568



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.04 1.01 0.96 2/57 12087
Raw data (/proc/12083/stat): 12083 (minisat+_script) S 12082 12083 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797501237 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12083/statm): 531 226 485 147 0 384 0
[pid=12083] vsize: 2124
Raw data (/proc/12087/stat): 12087 (minisat+_64-bit) R 12083 12083 8263 0 -1 0 48623 0 0 0 120303 307 0 0 25 0 1 0 1797501242 207302656 48233 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12087/statm): 50611 48233 145 145 0 50466 0
[pid=12087] vsize: 202444
Current children cumulated CPU time (s) 1206.1
Current children cumulated vsize (Kb) 204568

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1206.2
CPU user time (s): 1203.03
CPU system time (s): 3.16152
CPU usage (%): 99.669
Max. virtual memory (cumulated for all children) (Kb): 204568

Verifier Data

ERROR: no interpretation found !