Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-air04.opb
MD5SUMee388359e66788d310d5d5b34d6465c1
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 3896

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        852396 kB
Buffers:         35224 kB
Cached:         120264 kB
SwapCached:        708 kB
Active:          69060 kB
Inactive:        89016 kB
HighTotal:      131008 kB
HighFree:        41608 kB
LowTotal:       903652 kB
LowFree:        810788 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18540 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:47:53 (client local time) WITH STATUS 0 IN 1206.21 SECONDS
stats: 2901 7 1206.21 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:   67
c ---[1640]---> BDD-cost:  303
c ---[1638]---> BDD-cost:  119
c ---[1636]---> BDD-cost:  145
c ---[1634]---> BDD-cost:  165
c ---[1632]---> BDD-cost:  239
c ---[1630]---> BDD-cost:  223
c ---[1628]---> BDD-cost:   59
c ---[1626]---> BDD-cost:   35
c ---[1624]---> BDD-cost:   93
c ---[1622]---> BDD-cost:   45
c ---[1620]---> BDD-cost:  213
c ---[1618]---> BDD-cost:   73
c ---[1616]---> BDD-cost:   75
c ---[1614]---> BDD-cost:   63
c ---[1612]---> BDD-cost:   99
c ---[1608]---> BDD-cost:  187
c ---[1606]---> BDD-cost:   55
c ---[1604]---> BDD-cost:  107
c ---[1602]---> BDD-cost:   69
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   75
c ---[1596]---> BDD-cost:    3
c ---[1594]---> BDD-cost:  149
c ---[1592]---> BDD-cost:  137
c ---[1590]---> BDD-cost:  195
c ---[1588]---> BDD-cost:   93
c ---[1586]---> BDD-cost:  157
c ---[1584]---> BDD-cost:  233
c ---[1582]---> BDD-cost:  223
c ---[1580]---> BDD-cost:  225
c ---[1578]---> BDD-cost:  247
c ---[1576]---> BDD-cost:   75
c ---[1574]---> BDD-cost:  179
c ---[1572]---> BDD-cost:  225
c ---[1570]---> BDD-cost:  243
c ---[1568]---> BDD-cost:  199
c ---[1566]---> BDD-cost:   55
c ---[1564]---> BDD-cost:   57
c ---[1562]---> BDD-cost:   99
c ---[1560]---> BDD-cost:    9
c ---[1558]---> BDD-cost:    3
c ---[1556]---> BDD-cost:   23
c ---[1554]---> BDD-cost:   55
c ---[1552]---> BDD-cost:   51
c ---[1550]---> BDD-cost:   25
c ---[1548]---> BDD-cost:   23
c ---[1546]---> BDD-cost:   27
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:   37
c ---[1540]---> BDD-cost:   67
c ---[1538]---> BDD-cost:   67
c ---[1536]---> BDD-cost:  109
c ---[1534]---> BDD-cost:  211
c ---[1532]---> BDD-cost:   15
c ---[1530]---> BDD-cost:    0
c ---[1526]---> BDD-cost:   65
c ---[1524]---> BDD-cost:  117
c ---[1522]---> BDD-cost:   65
c ---[1520]---> BDD-cost:   65
c ---[1518]---> BDD-cost:   49
c ---[1516]---> BDD-cost:  439
c ---[1514]---> BDD-cost:  423
c ---[1512]---> BDD-cost:  287
c ---[1510]---> BDD-cost:   87
c ---[1508]---> BDD-cost:  217
c ---[1506]---> BDD-cost:  195
c ---[1504]---> BDD-cost:   63
c ---[1502]---> BDD-cost:   53
c ---[1500]---> BDD-cost:  359
c ---[1498]---> BDD-cost:  353
c ---[1494]---> BDD-cost:  169
c ---[1492]---> BDD-cost:  139
c ---[1490]---> BDD-cost:  159
c ---[1488]---> BDD-cost:   51
c ---[1486]---> BDD-cost:  223
c ---[1484]---> BDD-cost:  107
c ---[1482]---> BDD-cost:   75
c ---[1480]---> BDD-cost:  109
c ---[1478]---> BDD-cost:   93
c ---[1476]---> BDD-cost:   87
c ---[1474]---> BDD-cost:   87
c ---[1472]---> BDD-cost:    7
c ---[1468]---> BDD-cost:   73
c ---[1466]---> BDD-cost:    1
c ---[1464]---> BDD-cost:   71
c ---[1462]---> BDD-cost:  107
c ---[1460]---> BDD-cost:   77
c ---[1458]---> BDD-cost:    3
c ---[1456]---> BDD-cost:  107
c ---[1454]---> BDD-cost:  131
c ---[1452]---> BDD-cost:  135
c ---[1450]---> BDD-cost:   65
c ---[1448]---> BDD-cost:  165
c ---[1446]---> BDD-cost:  123
c ---[1444]---> BDD-cost:    1
c ---[1442]---> BDD-cost:    1
c ---[1440]---> BDD-cost:   87
c ---[1438]---> BDD-cost:  155
c ---[1436]---> BDD-cost:  167
c ---[1434]---> BDD-cost:  203
c ---[1432]---> BDD-cost:  231
c ---[1430]---> BDD-cost:  147
c ---[1428]---> BDD-cost:  135
c ---[1426]---> BDD-cost:   49
c ---[1424]---> BDD-cost:   31
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   23
c ---[1418]---> BDD-cost:   95
c ---[1416]---> BDD-cost:  325
c ---[1414]---> BDD-cost:  333
c ---[1412]---> BDD-cost:  173
c ---[1410]---> BDD-cost:  269
c ---[1408]---> BDD-cost:   31
c ---[1406]---> BDD-cost:  413
c ---[1404]---> BDD-cost:  313
c ---[1402]---> BDD-cost:  125
c ---[1400]---> BDD-cost:  113
c ---[1398]---> BDD-cost:   11
c ---[1396]---> BDD-cost:  247
c ---[1394]---> BDD-cost:   57
c ---[1392]---> BDD-cost:  237
c ---[1390]---> BDD-cost:  159
c ---[1388]---> BDD-cost:  117
c ---[1386]---> BDD-cost:   43
c ---[1384]---> BDD-cost:  143
c ---[1382]---> BDD-cost:   65
c ---[1380]---> BDD-cost:  123
c ---[1378]---> BDD-cost:   61
c ---[1376]---> BDD-cost:   39
c ---[1374]---> BDD-cost:  103
c ---[1372]---> BDD-cost:   85
c ---[1370]---> BDD-cost:   77
c ---[1368]---> BDD-cost:   57
c ---[1366]---> BDD-cost:  127
c ---[1364]---> BDD-cost:  157
c ---[1362]---> BDD-cost:  267
c ---[1360]---> BDD-cost:  223
c ---[1358]---> BDD-cost:  229
c ---[1356]---> BDD-cost:  257
c ---[1354]---> BDD-cost:   13
c ---[1352]---> BDD-cost:  241
c ---[1350]---> BDD-cost:  195
c ---[1348]---> BDD-cost:   49
c ---[1346]---> BDD-cost:  117
c ---[1344]---> BDD-cost:  197
c ---[1342]---> BDD-cost:  171
c ---[1340]---> BDD-cost:  287
c ---[1338]---> BDD-cost:   75
c ---[1336]---> BDD-cost:  215
c ---[1334]---> BDD-cost:  119
c ---[1332]---> BDD-cost:   57
c ---[1330]---> BDD-cost:  245
c ---[1328]---> BDD-cost:  257
c ---[1326]---> BDD-cost:  279
c ---[1324]---> BDD-cost:  227
c ---[1322]---> BDD-cost:  201
c ---[1320]---> BDD-cost:  143
c ---[1318]---> BDD-cost:  207
c ---[1316]---> BDD-cost:  131
c ---[1314]---> BDD-cost:  245
c ---[1312]---> BDD-cost:  115
c ---[1310]---> BDD-cost:  259
c ---[1308]---> BDD-cost:   91
c ---[1306]---> BDD-cost:   43
c ---[1304]---> BDD-cost:   39
c ---[1302]---> BDD-cost:   91
c ---[1300]---> BDD-cost:  179
c ---[1298]---> BDD-cost:   73
c ---[1296]---> BDD-cost:   29
c ---[1294]---> BDD-cost:  163
c ---[1292]---> BDD-cost:   81
c ---[1290]---> BDD-cost:   63
c ---[1288]---> BDD-cost:  189
c ---[1286]---> BDD-cost:  103
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  115
c ---[1280]---> BDD-cost:   19
c ---[1278]---> BDD-cost:   93
c ---[1276]---> BDD-cost:   99
c ---[1274]---> BDD-cost:   99
c ---[1272]---> BDD-cost:  103
c ---[1270]---> BDD-cost:   67
c ---[1268]---> BDD-cost:   23
c ---[1266]---> BDD-cost:  101
c ---[1264]---> BDD-cost:   85
c ---[1262]---> BDD-cost:   87
c ---[1260]---> BDD-cost:    7
c ---[1258]---> BDD-cost:   45
c ---[1256]---> BDD-cost:   43
c ---[1254]---> BDD-cost:   11
c ---[1252]---> BDD-cost:   59
c ---[1250]---> BDD-cost:  185
c ---[1248]---> BDD-cost:  249
c ---[1246]---> BDD-cost:  315
c ---[1244]---> BDD-cost:  137
c ---[1242]---> BDD-cost:  253
c ---[1240]---> BDD-cost:  161
c ---[1238]---> BDD-cost:  257
c ---[1236]---> BDD-cost:  167
c ---[1234]---> BDD-cost:  167
c ---[1232]---> BDD-cost:  141
c ---[1230]---> BDD-cost:   21
c ---[1228]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   95
c ---[1224]---> BDD-cost:  141
c ---[1222]---> BDD-cost:    0
c ---[1220]---> BDD-cost:  123
c ---[1218]---> BDD-cost:   83
c ---[1216]---> BDD-cost:   55
c ---[1214]---> BDD-cost:  183
c ---[1212]---> BDD-cost:  269
c ---[1210]---> BDD-cost:   63
c ---[1208]---> BDD-cost:   45
c ---[1206]---> BDD-cost:   39
c ---[1204]---> BDD-cost:   97
c ---[1202]---> BDD-cost:   51
c ---[1200]---> BDD-cost:   23
c ---[1198]---> BDD-cost:  101
c ---[1196]---> BDD-cost:   45
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   85
c ---[1190]---> BDD-cost:   35
c ---[1188]---> BDD-cost:   53
c ---[1186]---> BDD-cost:   21
c ---[1184]---> BDD-cost:  115
c ---[1182]---> BDD-cost:   99
c ---[1180]---> BDD-cost:   63
c ---[1178]---> BDD-cost:   77
c ---[1176]---> BDD-cost:   37
c ---[1174]---> BDD-cost:  139
c ---[1172]---> BDD-cost:  109
c ---[1170]---> BDD-cost:  407
c ---[1168]---> BDD-cost:  323
c ---[1166]---> BDD-cost:  109
c ---[1164]---> BDD-cost:   93
c ---[1162]---> BDD-cost:   51
c ---[1160]---> BDD-cost:   79
c ---[1158]---> BDD-cost:   75
c ---[1156]---> BDD-cost:  147
c ---[1154]---> BDD-cost:    0
c ---[1152]---> BDD-cost:  169
c ---[1150]---> BDD-cost:  209
c ---[1148]---> BDD-cost:   69
c ---[1146]---> BDD-cost:   51
c ---[1144]---> BDD-cost:   85
c ---[1140]---> BDD-cost:  103
c ---[1138]---> BDD-cost:  127
c ---[1136]---> BDD-cost:   77
c ---[1134]---> BDD-cost:   77
c ---[1132]---> BDD-cost:  181
c ---[1130]---> BDD-cost:  141
c ---[1128]---> BDD-cost:   89
c ---[1126]---> BDD-cost:   85
c ---[1124]---> BDD-cost:  119
c ---[1122]---> BDD-cost:   69
c ---[1120]---> BDD-cost:   57
c ---[1118]---> BDD-cost:   65
c ---[1116]---> BDD-cost:   47
c ---[1114]---> BDD-cost:   61
c ---[1112]---> BDD-cost:   31
c ---[1110]---> BDD-cost:  283
c ---[1106]---> BDD-cost:  183
c ---[1104]---> BDD-cost:  121
c ---[1102]---> BDD-cost:   89
c ---[1100]---> BDD-cost:  225
c ---[1098]---> BDD-cost:  267
c ---[1094]---> BDD-cost:  159
c ---[1092]---> BDD-cost:  209
c ---[1090]---> BDD-cost:   71
c ---[1088]---> BDD-cost:   99
c ---[1086]---> BDD-cost:  237
c ---[1084]---> BDD-cost:  129
c ---[1082]---> BDD-cost:  365
c ---[1080]---> BDD-cost:  369
c ---[1078]---> BDD-cost:  129
c ---[1076]---> BDD-cost:  101
c ---[1074]---> BDD-cost:  289
c ---[1072]---> BDD-cost:  279
c ---[1070]---> BDD-cost:  345
c ---[1068]---> BDD-cost:   81
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:   69
c ---[1062]---> BDD-cost:   83
c ---[1060]---> BDD-cost:   53
c ---[1058]---> BDD-cost:   67
c ---[1056]---> BDD-cost:   55
c ---[1054]---> BDD-cost:  145
c ---[1052]---> BDD-cost:  149
c ---[1050]---> BDD-cost:  105
c ---[1048]---> BDD-cost:   19
c ---[1046]---> BDD-cost:  105
c ---[1044]---> BDD-cost:  109
c ---[1042]---> BDD-cost:  101
c ---[1040]---> BDD-cost:  147
c ---[1038]---> BDD-cost:  231
c ---[1036]---> BDD-cost:  191
c ---[1034]---> BDD-cost:  157
c ---[1032]---> BDD-cost:  249
c ---[1030]---> BDD-cost:  385
c ---[1028]---> BDD-cost:   67
c ---[1026]---> BDD-cost:   71
c ---[1024]---> BDD-cost:   47
c ---[1022]---> BDD-cost:   75
c ---[1020]---> BDD-cost:  147
c ---[1018]---> BDD-cost:  139
c ---[1016]---> BDD-cost:  273
c ---[1014]---> BDD-cost:  213
c ---[1012]---> BDD-cost:  169
c ---[1010]---> BDD-cost:  239
c ---[1008]---> BDD-cost:  305
c ---[1006]---> BDD-cost:  109
c ---[1004]---> BDD-cost:  105
c ---[1002]---> BDD-cost:  147
c ---[1000]---> BDD-cost:  237
c ---[ 998]---> BDD-cost:  115
c ---[ 996]---> BDD-cost:  115
c ---[ 994]---> BDD-cost:   67
c ---[ 992]---> BDD-cost:  329
c ---[ 990]---> BDD-cost:  295
c ---[ 988]---> BDD-cost:   51
c ---[ 986]---> BDD-cost:   61
c ---[ 984]---> BDD-cost:  317
c ---[ 982]---> BDD-cost:   97
c ---[ 980]---> BDD-cost:   79
c ---[ 978]---> BDD-cost:   29
c ---[ 976]---> BDD-cost:  119
c ---[ 974]---> BDD-cost:   43
c ---[ 972]---> BDD-cost:   85
c ---[ 970]---> BDD-cost:   35
c ---[ 968]---> BDD-cost:   69
c ---[ 964]---> BDD-cost:   45
c ---[ 962]---> BDD-cost:   73
c ---[ 960]---> BDD-cost:   55
c ---[ 956]---> BDD-cost:   33
c ---[ 954]---> BDD-cost:  109
c ---[ 952]---> BDD-cost:   29
c ---[ 950]---> BDD-cost:  245
c ---[ 948]---> BDD-cost:  225
c ---[ 946]---> BDD-cost:  111
c ---[ 944]---> BDD-cost:  117
c ---[ 942]---> BDD-cost:  127
c ---[ 940]---> BDD-cost:  129
c ---[ 938]---> BDD-cost:  259
c ---[ 936]---> BDD-cost:  221
c ---[ 934]---> BDD-cost:  275
c ---[ 932]---> BDD-cost:   83
c ---[ 930]---> BDD-cost:  209
c ---[ 928]---> BDD-cost:  267
c ---[ 926]---> BDD-cost:  171
c ---[ 924]---> BDD-cost:   57
c ---[ 920]---> BDD-cost:  133
c ---[ 918]---> BDD-cost:  185
c ---[ 916]---> BDD-cost:  169
c ---[ 914]---> BDD-cost:  287
c ---[ 912]---> BDD-cost:   81
c ---[ 910]---> BDD-cost:   13
c ---[ 908]---> BDD-cost:  335
c ---[ 906]---> BDD-cost:  365
c ---[ 904]---> BDD-cost:  255
c ---[ 902]---> BDD-cost:  111
c ---[ 900]---> BDD-cost:   57
c ---[ 898]---> BDD-cost:  101
c ---[ 896]---> BDD-cost:  197
c ---[ 894]---> BDD-cost:  383
c ---[ 892]---> BDD-cost:  329
c ---[ 890]---> BDD-cost:  241
c ---[ 888]---> BDD-cost:  157
c ---[ 886]---> BDD-cost:  129
c ---[ 884]---> BDD-cost:   85
c ---[ 882]---> BDD-cost:   71
c ---[ 880]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   77
c ---[ 876]---> BDD-cost:   49
c ---[ 874]---> BDD-cost:  133
c ---[ 872]---> BDD-cost:  133
c ---[ 870]---> BDD-cost:  377
c ---[ 868]---> BDD-cost:  117
c ---[ 866]---> BDD-cost:  155
c ---[ 862]---> BDD-cost:  119
c ---[ 860]---> BDD-cost:  119
c ---[ 858]---> BDD-cost:  151
c ---[ 856]---> BDD-cost:  221
c ---[ 854]---> BDD-cost:  181
c ---[ 850]---> BDD-cost:   87
c ---[ 848]---> BDD-cost:  127
c ---[ 846]---> BDD-cost:  299
c ---[ 844]---> BDD-cost:  109
c ---[ 842]---> BDD-cost:  331
c ---[ 838]---> BDD-cost:   21
c ---[ 836]---> BDD-cost:  205
c ---[ 834]---> BDD-cost:  217
c ---[ 832]---> BDD-cost:  349
c ---[ 830]---> BDD-cost:  291
c ---[ 828]---> BDD-cost:  165
c ---[ 826]---> BDD-cost:  161
c ---[ 824]---> BDD-cost:   61
c ---[ 822]---> BDD-cost:   77
c ---[ 820]---> BDD-cost:   55
c ---[ 818]---> BDD-cost:  113
c ---[ 816]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:  189
c ---[ 812]---> BDD-cost:  157
c ---[ 810]---> BDD-cost:  149
c ---[ 808]---> BDD-cost:  139
c ---[ 806]---> BDD-cost:  165
c ---[ 804]---> BDD-cost:  181
c ---[ 802]---> BDD-cost:  253
c ---[ 800]---> BDD-cost:    0
c ---[ 798]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:  145
c ---[ 794]---> BDD-cost:  141
c ---[ 792]---> BDD-cost:  105
c ---[ 790]---> BDD-cost:   95
c ---[ 788]---> BDD-cost:   75
c ---[ 786]---> BDD-cost:  103
c ---[ 784]---> BDD-cost:  149
c ---[ 782]---> BDD-cost:  137
c ---[ 780]---> BDD-cost:   59
c ---[ 778]---> BDD-cost:  133
c ---[ 776]---> BDD-cost:    5
c ---[ 774]---> BDD-cost:   35
c ---[ 772]---> BDD-cost:    9
c ---[ 770]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   55
c ---[ 762]---> BDD-cost:  197
c ---[ 760]---> BDD-cost:  191
c ---[ 758]---> BDD-cost:  125
c ---[ 756]---> BDD-cost:    0
c ---[ 754]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  173
c ---[ 748]---> BDD-cost:   93
c ---[ 746]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:  321
c ---[ 742]---> BDD-cost:  195
c ---[ 740]---> BDD-cost:  163
c ---[ 734]---> BDD-cost:  151
c ---[ 732]---> BDD-cost:  115
c ---[ 730]---> BDD-cost:  253
c ---[ 728]---> BDD-cost:  381
c ---[ 726]---> BDD-cost:  345
c ---[ 724]---> BDD-cost:  185
c ---[ 720]---> BDD-cost:   83
c ---[ 718]---> BDD-cost:   69
c ---[ 716]---> BDD-cost:   51
c ---[ 714]---> BDD-cost:   47
c ---[ 712]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:  185
c ---[ 708]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  107
c ---[ 704]---> BDD-cost:  363
c ---[ 702]---> BDD-cost:  103
c ---[ 700]---> BDD-cost:  277
c ---[ 698]---> BDD-cost:  341
c ---[ 696]---> BDD-cost:  213
c ---[ 694]---> BDD-cost:  315
c ---[ 692]---> BDD-cost:  275
c ---[ 690]---> BDD-cost:  151
c ---[ 688]---> BDD-cost:  203
c ---[ 686]---> BDD-cost:  111
c ---[ 684]---> BDD-cost:  103
c ---[ 682]---> BDD-cost:   75
c ---[ 680]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   21
c ---[ 676]---> BDD-cost:   11
c ---[ 674]---> BDD-cost:   31
c ---[ 670]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:  149
c ---[ 666]---> BDD-cost:  167
c ---[ 664]---> BDD-cost:    0
c ---[ 662]---> BDD-cost:   97
c ---[ 660]---> BDD-cost:  149
c ---[ 658]---> BDD-cost:  395
c ---[ 656]---> BDD-cost:   25
c ---[ 654]---> BDD-cost:  389
c ---[ 652]---> BDD-cost:  251
c ---[ 650]---> BDD-cost:  375
c ---[ 648]---> BDD-cost:  343
c ---[ 646]---> BDD-cost:  267
c ---[ 644]---> BDD-cost:  135
c ---[ 642]---> BDD-cost:  135
c ---[ 640]---> BDD-cost:  263
c ---[ 638]---> BDD-cost:  259
c ---[ 636]---> BDD-cost:  245
c ---[ 634]---> BDD-cost:   45
c ---[ 632]---> BDD-cost:   41
c ---[ 630]---> BDD-cost:  127
c ---[ 628]---> BDD-cost:  117
c ---[ 626]---> BDD-cost:   53
c ---[ 624]---> BDD-cost:  149
c ---[ 622]---> BDD-cost:    9
c ---[ 620]---> BDD-cost:  103
c ---[ 618]---> BDD-cost:  215
c ---[ 616]---> BDD-cost:   89
c ---[ 614]---> BDD-cost:  177
c ---[ 612]---> BDD-cost:  343
c ---[ 610]---> BDD-cost:  237
c ---[ 608]---> BDD-cost:  177
c ---[ 606]---> BDD-cost:   85
c ---[ 604]---> BDD-cost:  267
c ---[ 602]---> BDD-cost:  225
c ---[ 600]---> BDD-cost:   85
c ---[ 598]---> BDD-cost:  109
c ---[ 596]---> BDD-cost:  105
c ---[ 594]---> BDD-cost:  113
c ---[ 592]---> BDD-cost:   55
c ---[ 590]---> BDD-cost:  117
c ---[ 588]---> BDD-cost:   83
c ---[ 586]---> BDD-cost:   79
c ---[ 584]---> BDD-cost:   81
c ---[ 582]---> BDD-cost:  263
c ---[ 580]---> BDD-cost:  179
c ---[ 578]---> BDD-cost:  143
c ---[ 576]---> BDD-cost:  281
c ---[ 574]---> BDD-cost:  389
c ---[ 572]---> BDD-cost:  333
c ---[ 570]---> BDD-cost:  357
c ---[ 568]---> BDD-cost:  345
c ---[ 566]---> BDD-cost:  263
c ---[ 564]---> BDD-cost:   89
c ---[ 562]---> BDD-cost:  285
c ---[ 558]---> BDD-cost:  419
c ---[ 556]---> BDD-cost:  135
c ---[ 554]---> BDD-cost:  357
c ---[ 552]---> BDD-cost:  473
c ---[ 550]---> BDD-cost:  455
c ---[ 548]---> BDD-cost:  405
c ---[ 546]---> BDD-cost:  241
c ---[ 544]---> BDD-cost:  211
c ---[ 542]---> BDD-cost:  313
c ---[ 540]---> BDD-cost:  371
c ---[ 538]---> BDD-cost:  389
c ---[ 536]---> BDD-cost:  223
c ---[ 534]---> BDD-cost:   71
c ---[ 532]---> BDD-cost:   63
c ---[ 530]---> BDD-cost:  221
c ---[ 528]---> BDD-cost:  147
c ---[ 526]---> BDD-cost:  131
c ---[ 524]---> BDD-cost:  185
c ---[ 522]---> BDD-cost:  141
c ---[ 520]---> BDD-cost:  249
c ---[ 518]---> BDD-cost:  261
c ---[ 516]---> BDD-cost:  311
c ---[ 514]---> BDD-cost:  261
c ---[ 512]---> BDD-cost:  387
c ---[ 510]---> BDD-cost:   51
c ---[ 508]---> BDD-cost:  247
c ---[ 506]---> BDD-cost:  295
c ---[ 504]---> BDD-cost:   31
c ---[ 502]---> BDD-cost:  355
c ---[ 500]---> BDD-cost:  135
c ---[ 498]---> BDD-cost:  443
c ---[ 496]---> BDD-cost:  653
c ---[ 494]---> BDD-cost:  703
c ---[ 492]---> BDD-cost:  517
c ---[ 490]---> BDD-cost:  441
c ---[ 488]---> BDD-cost:  159
c ---[ 486]---> BDD-cost:  411
c ---[ 484]---> BDD-cost:  289
c ---[ 482]---> BDD-cost:  277
c ---[ 480]---> BDD-cost:  239
c ---[ 478]---> BDD-cost:  201
c ---[ 476]---> BDD-cost:  309
c ---[ 474]---> BDD-cost:  287
c ---[ 472]---> BDD-cost:  177
c ---[ 470]---> BDD-cost:  143
c ---[ 468]---> BDD-cost:  131
c ---[ 466]---> BDD-cost:  155
c ---[ 464]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:  189
c ---[ 460]---> BDD-cost:  219
c ---[ 456]---> BDD-cost:  267
c ---[ 454]---> BDD-cost:  135
c ---[ 452]---> BDD-cost:   69
c ---[ 450]---> BDD-cost:   75
c ---[ 448]---> BDD-cost:   51
c ---[ 446]---> BDD-cost:  117
c ---[ 444]---> BDD-cost:  211
c ---[ 442]---> BDD-cost:  117
c ---[ 436]---> BDD-cost:  189
c ---[ 434]---> BDD-cost:   73
c ---[ 432]---> BDD-cost:   55
c ---[ 430]---> BDD-cost:   57
c ---[ 428]---> BDD-cost:   91
c ---[ 426]---> BDD-cost:  325
c ---[ 424]---> BDD-cost:  223
c ---[ 422]---> BDD-cost:   75
c ---[ 420]---> BDD-cost:   57
c ---[ 418]---> BDD-cost:   43
c ---[ 416]---> BDD-cost:  255
c ---[ 414]---> BDD-cost:  285
c ---[ 412]---> BDD-cost:  187
c ---[ 410]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   91
c ---[ 406]---> BDD-cost:  211
c ---[ 404]---> BDD-cost:  159
c ---[ 402]---> BDD-cost:   97
c ---[ 400]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   27
c ---[ 396]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  141
c ---[ 390]---> BDD-cost:  109
c ---[ 388]---> BDD-cost:  321
c ---[ 386]---> BDD-cost:  305
c ---[ 384]---> BDD-cost:  603
c ---[ 382]---> BDD-cost:  441
c ---[ 380]---> BDD-cost:  391
c ---[ 378]---> BDD-cost:   87
c ---[ 376]---> BDD-cost:  387
c ---[ 374]---> BDD-cost:  289
c ---[ 372]---> BDD-cost:  219
c ---[ 370]---> BDD-cost:  309
c ---[ 368]---> BDD-cost:  241
c ---[ 366]---> BDD-cost:  197
c ---[ 364]---> BDD-cost:  279
c ---[ 362]---> BDD-cost:  167
c ---[ 360]---> BDD-cost:  151
c ---[ 358]---> BDD-cost:   49
c ---[ 356]---> BDD-cost:   79
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:  107
c ---[ 350]---> BDD-cost:   55
c ---[ 346]---> BDD-cost:  177
c ---[ 344]---> BDD-cost:  223
c ---[ 342]---> BDD-cost:  119
c ---[ 340]---> BDD-cost:  137
c ---[ 338]---> BDD-cost:  105
c ---[ 336]---> BDD-cost:  183
c ---[ 334]---> BDD-cost:  109
c ---[ 332]---> BDD-cost:  179
c ---[ 330]---> BDD-cost:  285
c ---[ 328]---> BDD-cost:  191
c ---[ 326]---> BDD-cost:  177
c ---[ 324]---> BDD-cost:  145
c ---[ 320]---> BDD-cost:  153
c ---[ 318]---> BDD-cost:  121
c ---[ 316]---> BDD-cost:   95
c ---[ 314]---> BDD-cost:  111
c ---[ 312]---> BDD-cost:   35
c ---[ 310]---> BDD-cost:  115
c ---[ 308]---> BDD-cost:    0
c ---[ 306]---> BDD-cost:  281
c ---[ 304]---> BDD-cost:  265
c ---[ 302]---> BDD-cost:  167
c ---[ 300]---> BDD-cost:  151
c ---[ 298]---> BDD-cost:  167
c ---[ 296]---> BDD-cost:  137
c ---[ 292]---> BDD-cost:  375
c ---[ 290]---> BDD-cost:  287
c ---[ 288]---> BDD-cost:  247
c ---[ 286]---> BDD-cost:  249
c ---[ 284]---> BDD-cost:  131
c ---[ 282]---> BDD-cost:  187
c ---[ 280]---> BDD-cost:  135
c ---[ 278]---> BDD-cost:  129
c ---[ 276]---> BDD-cost:  317
c ---[ 274]---> BDD-cost:  365
c ---[ 272]---> BDD-cost:  235
c ---[ 270]---> BDD-cost:  249
c ---[ 268]---> BDD-cost:  283
c ---[ 266]---> BDD-cost:  105
c ---[ 264]---> BDD-cost:  233
c ---[ 262]---> BDD-cost:  259
c ---[ 260]---> BDD-cost:  287
c ---[ 258]---> BDD-cost:  175
c ---[ 256]---> BDD-cost:  233
c ---[ 254]---> BDD-cost:  167
c ---[ 252]---> BDD-cost:  159
c ---[ 250]---> BDD-cost:   47
c ---[ 246]---> BDD-cost:  135
c ---[ 244]---> BDD-cost:   59
c ---[ 242]---> BDD-cost:  147
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  203
c ---[ 236]---> BDD-cost:  275
c ---[ 234]---> BDD-cost:  263
c ---[ 232]---> BDD-cost:   31
c ---[ 230]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   31
c ---[ 226]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:  225
c ---[ 222]---> BDD-cost:   71
c ---[ 220]---> BDD-cost:   65
c ---[ 218]---> BDD-cost:  385
c ---[ 216]---> BDD-cost:  361
c ---[ 214]---> BDD-cost:   73
c ---[ 212]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:  131
c ---[ 206]---> BDD-cost:  145
c ---[ 204]---> BDD-cost:  121
c ---[ 202]---> BDD-cost:  117
c ---[ 200]---> BDD-cost:   61
c ---[ 198]---> BDD-cost:  111
c ---[ 196]---> BDD-cost:  123
c ---[ 194]---> BDD-cost:  125
c ---[ 192]---> BDD-cost:  243
c ---[ 190]---> BDD-cost:  143
c ---[ 188]---> BDD-cost:  149
c ---[ 186]---> BDD-cost:  103
c ---[ 184]---> BDD-cost:  155
c ---[ 182]---> BDD-cost:  247
c ---[ 180]---> BDD-cost:  143
c ---[ 178]---> BDD-cost:   89
c ---[ 176]---> BDD-cost:   91
c ---[ 174]---> BDD-cost:   81
c ---[ 172]---> BDD-cost:   79
c ---[ 170]---> BDD-cost:  117
c ---[ 168]---> BDD-cost:   89
c ---[ 166]---> BDD-cost:   61
c ---[ 164]---> BDD-cost:  127
c ---[ 162]---> BDD-cost:  135
c ---[ 160]---> BDD-cost:  161
c ---[ 158]---> BDD-cost:  141
c ---[ 156]---> BDD-cost:   91
c ---[ 154]---> BDD-cost:  437
c ---[ 152]---> BDD-cost:  309
c ---[ 150]---> BDD-cost:  173
c ---[ 148]---> BDD-cost:  441
c ---[ 146]---> BDD-cost:  489
c ---[ 144]---> BDD-cost:  299
c ---[ 142]---> BDD-cost:  455
c ---[ 140]---> BDD-cost:  333
c ---[ 138]---> BDD-cost:  421
c ---[ 136]---> BDD-cost:  375
c ---[ 134]---> BDD-cost:  143
c ---[ 132]---> BDD-cost:  433
c ---[ 130]---> BDD-cost:  405
c ---[ 128]---> BDD-cost:  333
c ---[ 126]---> BDD-cost:  673
c ---[ 124]---> BDD-cost:  685
c ---[ 122]---> BDD-cost:  385
c ---[ 120]---> BDD-cost:  267
c ---[ 118]---> BDD-cost:  345
c ---[ 116]---> BDD-cost:  365
c ---[ 114]---> BDD-cost:  391
c ---[ 112]---> BDD-cost:  111
c ---[ 110]---> BDD-cost:  313
c ---[ 108]---> BDD-cost:  275
c ---[ 106]---> BDD-cost:  257
c ---[ 104]---> BDD-cost:  203
c ---[ 102]---> BDD-cost:  311
c ---[ 100]---> BDD-cost:  227
c ---[  98]---> BDD-cost:  295
c ---[  96]---> BDD-cost:  233
c ---[  94]---> BDD-cost:  247
c ---[  92]---> BDD-cost:  237
c ---[  90]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   95
c ---[  86]---> BDD-cost:    0
c ---[  84]---> BDD-cost:  149
c ---[  80]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   85
c ---[  76]---> BDD-cost:  109
c ---[  74]---> BDD-cost:   43
c ---[  72]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   71
c ---[  68]---> BDD-cost:   67
c ---[  66]---> BDD-cost:  169
c ---[  64]---> BDD-cost:  151
c ---[  62]---> BDD-cost:  147
c ---[  60]---> BDD-cost:  177
c ---[  58]---> BDD-cost:  127
c ---[  56]---> BDD-cost:  131
c ---[  54]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  215
c ---[  50]---> BDD-cost:  181
c ---[  48]---> BDD-cost:  235
c ---[  46]---> BDD-cost:  163
c ---[  44]---> BDD-cost:  101
c ---[  42]---> BDD-cost:   57
c ---[  40]---> BDD-cost:   59
c ---[  38]---> BDD-cost:  139
c ---[  36]---> BDD-cost:   39
c ---[  34]---> BDD-cost:  151
c ---[  32]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   45
c ---[  28]---> BDD-cost:   45
c ---[  26]---> BDD-cost:   45
c ---[  24]---> BDD-cost:   65
c ---[  22]---> BDD-cost:   95
c ---[  20]---> BDD-cost:    0
c ---[  16]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   81
c ---[   2]---> BDD-cost:  223
c ---[   0]---> BDD-cost:  271
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       101 |  310358   807732 |  113797     101     4421    43.8 |  0.588 % |
c |       251 |  310340   807685 |  125176     248     8941    36.1 |  0.590 % |
c |       477 |  310255   807455 |  137694     461    13728    29.8 |  0.603 % |
c |       814 |  310255   807455 |  151464     798    37090    46.5 |  0.603 % |
c |      1320 |  309505   805553 |  166610    1266    60778    48.0 |  0.693 % |
c |      2079 |  309327   805067 |  183271    2007    94497    47.1 |  0.730 % |
c |      3219 |  308710   803466 |  201598    3121   175840    56.3 |  0.848 % |
c |      4927 |  308374   802597 |  221758    4783   334504    69.9 |  0.896 % |
c |      7489 |  307940   801458 |  243934    7200   539854    75.0 |  0.948 % |
c |     11334 |  307798   801098 |  268327   11017  1054203    95.7 |  0.963 % |
c |     17100 |  307510   800357 |  295160   16719  1913448   114.4 |  0.992 % |
c |     25749 |  307286   799785 |  324676   25320  3051328   120.5 |  1.011 % |
c |     38723 |  307204   799580 |  357144   38277  5578865   145.7 |  1.014 % |
c |     58184 |  306684   798243 |  392858   57603  9277788   161.1 |  1.076 % |
c |     87376 |  306512   797802 |  432144   86712 17039623   196.5 |  1.089 % |
c |    131165 |  306227   797059 |  475359  130316 29832985   228.9 |  1.132 % |

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/11107/stat): 11107 (minisat+_script) R 11106 11107 1333 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788444471 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/11107/statm): 174 3 169 147 0 27 0
[pid=11107] 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=11108
New process pid=11109
New process pid=11110
execve syscall for /bin/sed executable
One traced child (pid=11109) 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=11110) exited with status: 0
One traced child (pid=11108) exited with status: 0
New process pid=11111
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-air04.opb

[startup+10.0041 s]
Raw data (loadavg): 0.91 0.95 0.90 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 10912 0 0 0 901 49 0 0 25 0 1 0 1788444476 52420608 10523 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 12798 10523 145 145 0 12653 0
[pid=11111] vsize: 51192
Current children cumulated CPU time (s) 9.5
Current children cumulated vsize (Kb) 53316

[startup+20.0048 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 11038 0 0 0 1899 50 0 0 25 0 1 0 1788444476 52936704 10649 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 12924 10649 145 145 0 12779 0
[pid=11111] vsize: 51696
Current children cumulated CPU time (s) 19.49
Current children cumulated vsize (Kb) 53820

[startup+30.0064 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 11199 0 0 0 2895 52 0 0 25 0 1 0 1788444476 53612544 10810 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 13089 10810 145 145 0 12944 0
[pid=11111] vsize: 52356
Current children cumulated CPU time (s) 29.47
Current children cumulated vsize (Kb) 54480

[startup+40.0071 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 11377 0 0 0 3892 54 0 0 25 0 1 0 1788444476 54329344 10988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 13264 10988 145 145 0 13119 0
[pid=11111] vsize: 53056
Current children cumulated CPU time (s) 39.46
Current children cumulated vsize (Kb) 55180

[startup+50.0088 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 11553 0 0 0 4889 55 0 0 25 0 1 0 1788444476 55046144 11164 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 13439 11164 145 145 0 13294 0
[pid=11111] vsize: 53756
Current children cumulated CPU time (s) 49.44
Current children cumulated vsize (Kb) 55880

[startup+60.0094 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 11842 0 0 0 5884 57 0 0 25 0 1 0 1788444476 56254464 11453 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 13734 11453 145 145 0 13589 0
[pid=11111] vsize: 54936
Current children cumulated CPU time (s) 59.41
Current children cumulated vsize (Kb) 57060

[startup+70.01 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 12146 0 0 0 6877 60 0 0 25 0 1 0 1788444476 57487360 11757 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 14035 11757 145 145 0 13890 0
[pid=11111] vsize: 56140
Current children cumulated CPU time (s) 69.37
Current children cumulated vsize (Kb) 58264

[startup+80.0107 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 12464 0 0 0 7872 62 0 0 25 0 1 0 1788444476 58785792 12075 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 14352 12075 145 145 0 14207 0
[pid=11111] vsize: 57408
Current children cumulated CPU time (s) 79.34
Current children cumulated vsize (Kb) 59532

[startup+90.0114 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 12718 0 0 0 8868 64 0 0 25 0 1 0 1788444476 59817984 12329 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 14604 12329 145 145 0 14459 0
[pid=11111] vsize: 58416
Current children cumulated CPU time (s) 89.32
Current children cumulated vsize (Kb) 60540

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 13127 0 0 0 9862 67 0 0 25 0 1 0 1788444476 61526016 12738 4294967295 134512640 135094434 3221224432 3221223024 134551922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 15021 12738 145 145 0 14876 0
[pid=11111] vsize: 60084
Current children cumulated CPU time (s) 99.29
Current children cumulated vsize (Kb) 62208

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 13370 0 0 0 10857 69 0 0 25 0 1 0 1788444476 62513152 12981 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 15262 12981 145 145 0 15117 0
[pid=11111] vsize: 61048
Current children cumulated CPU time (s) 109.26
Current children cumulated vsize (Kb) 63172

[startup+120.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 13624 0 0 0 11853 71 0 0 19 0 1 0 1788444476 63545344 13235 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 15514 13235 145 145 0 15369 0
[pid=11111] vsize: 62056
Current children cumulated CPU time (s) 119.24
Current children cumulated vsize (Kb) 64180

[startup+130.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 13908 0 0 0 12849 72 0 0 25 0 1 0 1788444476 64700416 13519 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 15796 13519 145 145 0 15651 0
[pid=11111] vsize: 63184
Current children cumulated CPU time (s) 129.21
Current children cumulated vsize (Kb) 65308

[startup+140.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 14191 0 0 0 13844 75 0 0 25 0 1 0 1788444476 65785856 13802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 16061 13802 145 145 0 15916 0
[pid=11111] vsize: 64244
Current children cumulated CPU time (s) 139.19
Current children cumulated vsize (Kb) 66368

[startup+150.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 14485 0 0 0 14838 77 0 0 25 0 1 0 1788444476 66981888 14096 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 16353 14096 145 145 0 16208 0
[pid=11111] vsize: 65412
Current children cumulated CPU time (s) 149.15
Current children cumulated vsize (Kb) 67536

[startup+160.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 14839 0 0 0 15831 79 0 0 25 0 1 0 1788444476 68423680 14450 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 16705 14450 145 145 0 16560 0
[pid=11111] vsize: 66820
Current children cumulated CPU time (s) 159.1
Current children cumulated vsize (Kb) 68944

[startup+170.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 15165 0 0 0 16825 82 0 0 25 0 1 0 1788444476 69758976 14776 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 17031 14776 145 145 0 16886 0
[pid=11111] vsize: 68124
Current children cumulated CPU time (s) 169.07
Current children cumulated vsize (Kb) 70248

[startup+180.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 15463 0 0 0 17822 84 0 0 25 0 1 0 1788444476 70975488 15074 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 17328 15074 145 145 0 17183 0
[pid=11111] vsize: 69312
Current children cumulated CPU time (s) 179.06
Current children cumulated vsize (Kb) 71436

[startup+190.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 15819 0 0 0 18817 86 0 0 25 0 1 0 1788444476 72560640 15430 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 17715 15430 145 145 0 17570 0
[pid=11111] vsize: 70860
Current children cumulated CPU time (s) 189.03
Current children cumulated vsize (Kb) 72984

[startup+200.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 16154 0 0 0 19811 89 0 0 25 0 1 0 1788444476 73928704 15765 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 18049 15765 145 145 0 17904 0
[pid=11111] vsize: 72196
Current children cumulated CPU time (s) 199
Current children cumulated vsize (Kb) 74320

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 16561 0 0 0 20803 93 0 0 25 0 1 0 1788444476 75587584 16172 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 18454 16172 145 145 0 18309 0
[pid=11111] vsize: 73816
Current children cumulated CPU time (s) 208.96
Current children cumulated vsize (Kb) 75940

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 16809 0 0 0 21799 94 0 0 25 0 1 0 1788444476 76599296 16420 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 18701 16420 145 145 0 18556 0
[pid=11111] vsize: 74804
Current children cumulated CPU time (s) 218.93
Current children cumulated vsize (Kb) 76928

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 17095 0 0 0 22793 97 0 0 25 0 1 0 1788444476 77762560 16706 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 18985 16706 145 145 0 18840 0
[pid=11111] vsize: 75940
Current children cumulated CPU time (s) 228.9
Current children cumulated vsize (Kb) 78064

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 17321 0 0 0 23789 99 0 0 25 0 1 0 1788444476 78680064 16932 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 19209 16932 145 145 0 19064 0
[pid=11111] vsize: 76836
Current children cumulated CPU time (s) 238.88
Current children cumulated vsize (Kb) 78960

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) T 11107 11107 1333 0 -1 0 17582 0 0 0 24784 101 0 0 25 0 1 0 1788444476 79745024 17193 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11111/statm): 19469 17193 145 145 0 19324 0
[pid=11111] vsize: 77876
Current children cumulated CPU time (s) 248.85
Current children cumulated vsize (Kb) 80000

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 17898 0 0 0 25780 103 0 0 25 0 1 0 1788444476 81035264 17509 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 19784 17509 145 145 0 19639 0
[pid=11111] vsize: 79136
Current children cumulated CPU time (s) 258.83
Current children cumulated vsize (Kb) 81260

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 18292 0 0 0 26774 105 0 0 25 0 1 0 1788444476 82640896 17903 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 20176 17903 145 145 0 20031 0
[pid=11111] vsize: 80704
Current children cumulated CPU time (s) 268.79
Current children cumulated vsize (Kb) 82828

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 18573 0 0 0 27769 106 0 0 25 0 1 0 1788444476 83787776 18184 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 20456 18184 145 145 0 20311 0
[pid=11111] vsize: 81824
Current children cumulated CPU time (s) 278.75
Current children cumulated vsize (Kb) 83948

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 18858 0 0 0 28765 109 0 0 25 0 1 0 1788444476 84946944 18469 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 20739 18469 145 145 0 20594 0
[pid=11111] vsize: 82956
Current children cumulated CPU time (s) 288.74
Current children cumulated vsize (Kb) 85080

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 19087 0 0 0 29761 110 0 0 25 0 1 0 1788444476 85880832 18698 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 20967 18698 145 145 0 20822 0
[pid=11111] vsize: 83868
Current children cumulated CPU time (s) 298.71
Current children cumulated vsize (Kb) 85992

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 19457 0 0 0 30755 113 0 0 25 0 1 0 1788444476 87388160 19068 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 21335 19068 145 145 0 21190 0
[pid=11111] vsize: 85340
Current children cumulated CPU time (s) 308.68
Current children cumulated vsize (Kb) 87464

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 19785 0 0 0 31748 116 0 0 25 0 1 0 1788444476 88723456 19396 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 21661 19396 145 145 0 21516 0
[pid=11111] vsize: 86644
Current children cumulated CPU time (s) 318.64
Current children cumulated vsize (Kb) 88768

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 20132 0 0 0 32743 118 0 0 25 0 1 0 1788444476 90140672 19743 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 22007 19743 145 145 0 21862 0
[pid=11111] vsize: 88028
Current children cumulated CPU time (s) 328.61
Current children cumulated vsize (Kb) 90152

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 20526 0 0 0 33735 122 0 0 25 0 1 0 1788444476 91758592 20137 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 22402 20137 145 145 0 22257 0
[pid=11111] vsize: 89608
Current children cumulated CPU time (s) 338.57
Current children cumulated vsize (Kb) 91732

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 20855 0 0 0 34729 124 0 0 25 0 1 0 1788444476 93102080 20466 4294967295 134512640 135094434 3221224432 3221223104 134555576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 22730 20466 145 145 0 22585 0
[pid=11111] vsize: 90920
Current children cumulated CPU time (s) 348.53
Current children cumulated vsize (Kb) 93044

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 21098 0 0 0 35725 125 0 0 25 0 1 0 1788444476 94093312 20709 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 22972 20709 145 145 0 22827 0
[pid=11111] vsize: 91888
Current children cumulated CPU time (s) 358.5
Current children cumulated vsize (Kb) 94012

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 21366 0 0 0 36721 127 0 0 25 0 1 0 1788444476 95191040 20977 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 23240 20977 145 145 0 23095 0
[pid=11111] vsize: 92960
Current children cumulated CPU time (s) 368.48
Current children cumulated vsize (Kb) 95084

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 21795 0 0 0 37714 130 0 0 25 0 1 0 1788444476 96931840 21406 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 23665 21406 145 145 0 23520 0
[pid=11111] vsize: 94660
Current children cumulated CPU time (s) 378.44
Current children cumulated vsize (Kb) 96784

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 22145 0 0 0 38707 133 0 0 25 0 1 0 1788444476 98357248 21756 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 24013 21756 145 145 0 23868 0
[pid=11111] vsize: 96052
Current children cumulated CPU time (s) 388.4
Current children cumulated vsize (Kb) 98176

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 22483 0 0 0 39702 135 0 0 25 0 1 0 1788444476 99737600 22094 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 24350 22094 145 145 0 24205 0
[pid=11111] vsize: 97400
Current children cumulated CPU time (s) 398.37
Current children cumulated vsize (Kb) 99524

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 22779 0 0 0 40698 137 0 0 25 0 1 0 1788444476 101203968 22390 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 24708 22390 145 145 0 24563 0
[pid=11111] vsize: 98832
Current children cumulated CPU time (s) 408.35
Current children cumulated vsize (Kb) 100956

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 23092 0 0 0 41694 138 0 0 25 0 1 0 1788444476 102481920 22703 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 25020 22703 145 145 0 24875 0
[pid=11111] vsize: 100080
Current children cumulated CPU time (s) 418.32
Current children cumulated vsize (Kb) 102204

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 23502 0 0 0 42690 140 0 0 25 0 1 0 1788444476 104177664 23113 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 25434 23113 145 145 0 25289 0
[pid=11111] vsize: 101736
Current children cumulated CPU time (s) 428.3
Current children cumulated vsize (Kb) 103860

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 23945 0 0 0 43683 143 0 0 25 0 1 0 1788444476 105988096 23556 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 25876 23556 145 145 0 25731 0
[pid=11111] vsize: 103504
Current children cumulated CPU time (s) 438.26
Current children cumulated vsize (Kb) 105628

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 24205 0 0 0 44679 144 0 0 25 0 1 0 1788444476 107048960 23816 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 26135 23816 145 145 0 25990 0
[pid=11111] vsize: 104540
Current children cumulated CPU time (s) 448.23
Current children cumulated vsize (Kb) 106664

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 24401 0 0 0 45676 145 0 0 25 0 1 0 1788444476 107847680 24012 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 26330 24012 145 145 0 26185 0
[pid=11111] vsize: 105320
Current children cumulated CPU time (s) 458.21
Current children cumulated vsize (Kb) 107444

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 24770 0 0 0 46669 148 0 0 25 0 1 0 1788444476 109359104 24381 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 26699 24381 145 145 0 26554 0
[pid=11111] vsize: 106796
Current children cumulated CPU time (s) 468.17
Current children cumulated vsize (Kb) 108920

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 25139 0 0 0 47663 151 0 0 25 0 1 0 1788444476 110866432 24750 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 27067 24750 145 145 0 26922 0
[pid=11111] vsize: 108268
Current children cumulated CPU time (s) 478.14
Current children cumulated vsize (Kb) 110392

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 25527 0 0 0 48655 155 0 0 25 0 1 0 1788444476 112447488 25138 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 27453 25138 145 145 0 27308 0
[pid=11111] vsize: 109812
Current children cumulated CPU time (s) 488.1
Current children cumulated vsize (Kb) 111936

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 25902 0 0 0 49648 157 0 0 25 0 1 0 1788444476 113979392 25513 4294967295 134512640 135094434 3221224432 3221223024 134557283 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 27827 25514 145 145 0 27682 0
[pid=11111] vsize: 111308
Current children cumulated CPU time (s) 498.05
Current children cumulated vsize (Kb) 113432

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 26226 0 0 0 50642 160 0 0 25 0 1 0 1788444476 115294208 25837 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 28148 25837 145 145 0 28003 0
[pid=11111] vsize: 112592
Current children cumulated CPU time (s) 508.02
Current children cumulated vsize (Kb) 114716

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 26514 0 0 0 51638 162 0 0 25 0 1 0 1788444476 116469760 26125 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 28435 26125 145 145 0 28290 0
[pid=11111] vsize: 113740
Current children cumulated CPU time (s) 518
Current children cumulated vsize (Kb) 115864

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 26901 0 0 0 52631 165 0 0 25 0 1 0 1788444476 118046720 26512 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 28820 26512 145 145 0 28675 0
[pid=11111] vsize: 115280
Current children cumulated CPU time (s) 527.96
Current children cumulated vsize (Kb) 117404

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 27343 0 0 0 53624 167 0 0 25 0 1 0 1788444476 119857152 26954 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 29262 26954 145 145 0 29117 0
[pid=11111] vsize: 117048
Current children cumulated CPU time (s) 537.91
Current children cumulated vsize (Kb) 119172

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 27637 0 0 0 54618 170 0 0 25 0 1 0 1788444476 121053184 27248 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 29554 27248 145 145 0 29409 0
[pid=11111] vsize: 118216
Current children cumulated CPU time (s) 547.88
Current children cumulated vsize (Kb) 120340

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 28011 0 0 0 55613 172 0 0 25 0 1 0 1788444476 122580992 27622 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 29927 27622 145 145 0 29782 0
[pid=11111] vsize: 119708
Current children cumulated CPU time (s) 557.85
Current children cumulated vsize (Kb) 121832

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 28432 0 0 0 56607 176 0 0 25 0 1 0 1788444476 124301312 28043 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 30347 28043 145 145 0 30202 0
[pid=11111] vsize: 121388
Current children cumulated CPU time (s) 567.83
Current children cumulated vsize (Kb) 123512

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 28890 0 0 0 57601 179 0 0 25 0 1 0 1788444476 126177280 28501 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 30805 28501 145 145 0 30660 0
[pid=11111] vsize: 123220
Current children cumulated CPU time (s) 577.8
Current children cumulated vsize (Kb) 125344

[startup+590.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 29291 0 0 0 58594 183 0 0 25 0 1 0 1788444476 127823872 28902 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 31207 28902 145 145 0 31062 0
[pid=11111] vsize: 124828
Current children cumulated CPU time (s) 587.77
Current children cumulated vsize (Kb) 126952

[startup+600.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 29661 0 0 0 59586 185 0 0 25 0 1 0 1788444476 129335296 29272 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 31576 29272 145 145 0 31431 0
[pid=11111] vsize: 126304
Current children cumulated CPU time (s) 597.71
Current children cumulated vsize (Kb) 128428

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 29982 0 0 0 60580 189 0 0 25 0 1 0 1788444476 130650112 29593 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 31897 29593 145 145 0 31752 0
[pid=11111] vsize: 127588
Current children cumulated CPU time (s) 607.69
Current children cumulated vsize (Kb) 129712

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 30389 0 0 0 61575 191 0 0 25 0 1 0 1788444476 132288512 30000 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 32297 30000 145 145 0 32152 0
[pid=11111] vsize: 129188
Current children cumulated CPU time (s) 617.66
Current children cumulated vsize (Kb) 131312

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 30753 0 0 0 62571 193 0 0 25 0 1 0 1788444476 133840896 30364 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 32676 30364 145 145 0 32531 0
[pid=11111] vsize: 130704
Current children cumulated CPU time (s) 627.64
Current children cumulated vsize (Kb) 132828

[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 31136 0 0 0 63563 196 0 0 25 0 1 0 1788444476 135405568 30747 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 33058 30747 145 145 0 32913 0
[pid=11111] vsize: 132232
Current children cumulated CPU time (s) 637.59
Current children cumulated vsize (Kb) 134356

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 31579 0 0 0 64556 199 0 0 25 0 1 0 1788444476 137211904 31190 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 33499 31190 145 145 0 33354 0
[pid=11111] vsize: 133996
Current children cumulated CPU time (s) 647.55
Current children cumulated vsize (Kb) 136120

[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 31831 0 0 0 65551 201 0 0 25 0 1 0 1788444476 138240000 31442 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 33750 31442 145 145 0 33605 0
[pid=11111] vsize: 135000
Current children cumulated CPU time (s) 657.52
Current children cumulated vsize (Kb) 137124

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 32044 0 0 0 66547 203 0 0 25 0 1 0 1788444476 139108352 31655 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 33962 31655 145 145 0 33817 0
[pid=11111] vsize: 135848
Current children cumulated CPU time (s) 667.5
Current children cumulated vsize (Kb) 137972

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 32390 0 0 0 67541 206 0 0 25 0 1 0 1788444476 140529664 32001 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 34309 32001 145 145 0 34164 0
[pid=11111] vsize: 137236
Current children cumulated CPU time (s) 677.47
Current children cumulated vsize (Kb) 139360

[startup+690.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 32743 0 0 0 68533 209 0 0 25 0 1 0 1788444476 141979648 32354 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 34663 32354 145 145 0 34518 0
[pid=11111] vsize: 138652
Current children cumulated CPU time (s) 687.42
Current children cumulated vsize (Kb) 140776

[startup+700.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 33143 0 0 0 69526 212 0 0 25 0 1 0 1788444476 143613952 32754 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 35062 32754 145 145 0 34917 0
[pid=11111] vsize: 140248
Current children cumulated CPU time (s) 697.38
Current children cumulated vsize (Kb) 142372

[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 33486 0 0 0 70519 214 0 0 25 0 1 0 1788444476 145010688 33097 4294967295 134512640 135094434 3221224432 3221223080 134562037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 35403 33097 145 145 0 35258 0
[pid=11111] vsize: 141612
Current children cumulated CPU time (s) 707.33
Current children cumulated vsize (Kb) 143736

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 33863 0 0 0 71513 217 0 0 25 0 1 0 1788444476 146554880 33474 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 35780 33474 145 145 0 35635 0
[pid=11111] vsize: 143120
Current children cumulated CPU time (s) 717.3
Current children cumulated vsize (Kb) 145244

[startup+730.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 34157 0 0 0 72509 219 0 0 25 0 1 0 1788444476 147755008 33768 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 36073 33768 145 145 0 35928 0
[pid=11111] vsize: 144292
Current children cumulated CPU time (s) 727.28
Current children cumulated vsize (Kb) 146416

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 34527 0 0 0 73503 221 0 0 25 0 1 0 1788444476 149266432 34138 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 36442 34138 145 145 0 36297 0
[pid=11111] vsize: 145768
Current children cumulated CPU time (s) 737.24
Current children cumulated vsize (Kb) 147892

[startup+750.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 34804 0 0 0 74497 224 0 0 25 0 1 0 1788444476 150392832 34415 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 36717 34415 145 145 0 36572 0
[pid=11111] vsize: 146868
Current children cumulated CPU time (s) 747.21
Current children cumulated vsize (Kb) 148992

[startup+760.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 35150 0 0 0 75492 226 0 0 25 0 1 0 1788444476 151810048 34761 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 37063 34761 145 145 0 36918 0
[pid=11111] vsize: 148252
Current children cumulated CPU time (s) 757.18
Current children cumulated vsize (Kb) 150376

[startup+770.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 35574 0 0 0 76487 228 0 0 25 0 1 0 1788444476 153538560 35185 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 37485 35185 145 145 0 37340 0
[pid=11111] vsize: 149940
Current children cumulated CPU time (s) 767.15
Current children cumulated vsize (Kb) 152064

[startup+780.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 35851 0 0 0 77483 230 0 0 25 0 1 0 1788444476 154669056 35462 4294967295 134512640 135094434 3221224432 3221223024 134557256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 37761 35462 145 145 0 37616 0
[pid=11111] vsize: 151044
Current children cumulated CPU time (s) 777.13
Current children cumulated vsize (Kb) 153168

[startup+790.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 36192 0 0 0 78478 232 0 0 25 0 1 0 1788444476 156061696 35803 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 38101 35803 145 145 0 37956 0
[pid=11111] vsize: 152404
Current children cumulated CPU time (s) 787.1
Current children cumulated vsize (Kb) 154528

[startup+800.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 36427 0 0 0 79475 233 0 0 25 0 1 0 1788444476 157024256 36038 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 38336 36038 145 145 0 38191 0
[pid=11111] vsize: 153344
Current children cumulated CPU time (s) 797.08
Current children cumulated vsize (Kb) 155468

[startup+810.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 36753 0 0 0 80469 235 0 0 25 0 1 0 1788444476 158351360 36364 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 38660 36364 145 145 0 38515 0
[pid=11111] vsize: 154640
Current children cumulated CPU time (s) 807.04
Current children cumulated vsize (Kb) 156764

[startup+820.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 37028 0 0 0 81464 237 0 0 25 0 1 0 1788444476 159461376 36639 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 38931 36639 145 145 0 38786 0
[pid=11111] vsize: 155724
Current children cumulated CPU time (s) 817.01
Current children cumulated vsize (Kb) 157848

[startup+830.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 37318 0 0 0 82460 239 0 0 25 0 1 0 1788444476 160645120 36929 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 39220 36929 145 145 0 39075 0
[pid=11111] vsize: 156880
Current children cumulated CPU time (s) 826.99
Current children cumulated vsize (Kb) 159004

[startup+840.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 37575 0 0 0 83455 240 0 0 25 0 1 0 1788444476 161705984 37186 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 39479 37186 145 145 0 39334 0
[pid=11111] vsize: 157916
Current children cumulated CPU time (s) 836.95
Current children cumulated vsize (Kb) 160040

[startup+850.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 37769 0 0 0 84452 242 0 0 25 0 1 0 1788444476 162500608 37380 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 39673 37380 145 145 0 39528 0
[pid=11111] vsize: 158692
Current children cumulated CPU time (s) 846.94
Current children cumulated vsize (Kb) 160816

[startup+860.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 38029 0 0 0 85448 243 0 0 25 0 1 0 1788444476 163565568 37640 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 39933 37640 145 145 0 39788 0
[pid=11111] vsize: 159732
Current children cumulated CPU time (s) 856.91
Current children cumulated vsize (Kb) 161856

[startup+870.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 38323 0 0 0 86442 246 0 0 25 0 1 0 1788444476 164765696 37934 4294967295 134512640 135094434 3221224432 3221223056 134562131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 40226 37934 145 145 0 40081 0
[pid=11111] vsize: 160904
Current children cumulated CPU time (s) 866.88
Current children cumulated vsize (Kb) 163028

[startup+880.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 38646 0 0 0 87435 249 0 0 25 0 1 0 1788444476 166084608 38257 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 40548 38257 145 145 0 40403 0
[pid=11111] vsize: 162192
Current children cumulated CPU time (s) 876.84
Current children cumulated vsize (Kb) 164316

[startup+890.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 38963 0 0 0 88431 251 0 0 25 0 1 0 1788444476 167374848 38574 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 40863 38574 145 145 0 40718 0
[pid=11111] vsize: 163452
Current children cumulated CPU time (s) 886.82
Current children cumulated vsize (Kb) 165576

[startup+900.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 39204 0 0 0 89428 253 0 0 25 0 1 0 1788444476 168361984 38815 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 41104 38815 145 145 0 40959 0
[pid=11111] vsize: 164416
Current children cumulated CPU time (s) 896.81
Current children cumulated vsize (Kb) 166540

[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 39501 0 0 0 90423 255 0 0 25 0 1 0 1788444476 169582592 39112 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 41402 39112 145 145 0 41257 0
[pid=11111] vsize: 165608
Current children cumulated CPU time (s) 906.78
Current children cumulated vsize (Kb) 167732

[startup+920.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 39805 0 0 0 91419 256 0 0 25 0 1 0 1788444476 170827776 39416 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 41706 39416 145 145 0 41561 0
[pid=11111] vsize: 166824
Current children cumulated CPU time (s) 916.75
Current children cumulated vsize (Kb) 168948

[startup+930.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 40074 0 0 0 92415 258 0 0 25 0 1 0 1788444476 171929600 39685 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 41975 39685 145 145 0 41830 0
[pid=11111] vsize: 167900
Current children cumulated CPU time (s) 926.73
Current children cumulated vsize (Kb) 170024

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 40393 0 0 0 93411 260 0 0 25 0 1 0 1788444476 173223936 40004 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 42291 40004 145 145 0 42146 0
[pid=11111] vsize: 169164
Current children cumulated CPU time (s) 936.71
Current children cumulated vsize (Kb) 171288

[startup+950.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 40650 0 0 0 94406 261 0 0 25 0 1 0 1788444476 174272512 40261 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 42547 40261 145 145 0 42402 0
[pid=11111] vsize: 170188
Current children cumulated CPU time (s) 946.67
Current children cumulated vsize (Kb) 172312

[startup+960.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 40877 0 0 0 95403 263 0 0 25 0 1 0 1788444476 175198208 40488 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 42773 40488 145 145 0 42628 0
[pid=11111] vsize: 171092
Current children cumulated CPU time (s) 956.66
Current children cumulated vsize (Kb) 173216

[startup+970.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 41150 0 0 0 96399 264 0 0 25 0 1 0 1788444476 176312320 40761 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 43045 40761 145 145 0 42900 0
[pid=11111] vsize: 172180
Current children cumulated CPU time (s) 966.63
Current children cumulated vsize (Kb) 174304

[startup+980.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 41407 0 0 0 97394 266 0 0 25 0 1 0 1788444476 177360896 41018 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 43301 41018 145 145 0 43156 0
[pid=11111] vsize: 173204
Current children cumulated CPU time (s) 976.6
Current children cumulated vsize (Kb) 175328

[startup+990.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 41729 0 0 0 98389 269 0 0 25 0 1 0 1788444476 178675712 41340 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 43622 41340 145 145 0 43477 0
[pid=11111] vsize: 174488
Current children cumulated CPU time (s) 986.58
Current children cumulated vsize (Kb) 176612

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 42026 0 0 0 99384 271 0 0 25 0 1 0 1788444476 179888128 41637 4294967295 134512640 135094434 3221224432 3221223104 134556485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 43918 41637 145 145 0 43773 0
[pid=11111] vsize: 175672
Current children cumulated CPU time (s) 996.55
Current children cumulated vsize (Kb) 177796

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 42333 0 0 0 100380 272 0 0 25 0 1 0 1788444476 181149696 41944 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 44226 41944 145 145 0 44081 0
[pid=11111] vsize: 176904
Current children cumulated CPU time (s) 1006.52
Current children cumulated vsize (Kb) 179028

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 42610 0 0 0 101375 274 0 0 25 0 1 0 1788444476 182800384 42221 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 44629 42221 145 145 0 44484 0
[pid=11111] vsize: 178516
Current children cumulated CPU time (s) 1016.49
Current children cumulated vsize (Kb) 180640

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 42824 0 0 0 102372 275 0 0 25 0 1 0 1788444476 183672832 42435 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 44842 42435 145 145 0 44697 0
[pid=11111] vsize: 179368
Current children cumulated CPU time (s) 1026.47
Current children cumulated vsize (Kb) 181492

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 42988 0 0 0 103370 277 0 0 25 0 1 0 1788444476 184340480 42599 4294967295 134512640 135094434 3221224432 3221223104 134555305 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 45005 42599 145 145 0 44860 0
[pid=11111] vsize: 180020
Current children cumulated CPU time (s) 1036.47
Current children cumulated vsize (Kb) 182144

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 43284 0 0 0 104366 278 0 0 25 0 1 0 1788444476 185548800 42895 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 45300 42895 145 145 0 45155 0
[pid=11111] vsize: 181200
Current children cumulated CPU time (s) 1046.44
Current children cumulated vsize (Kb) 183324

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 43676 0 0 0 105361 280 0 0 25 0 1 0 1788444476 187150336 43287 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 45691 43287 145 145 0 45546 0
[pid=11111] vsize: 182764
Current children cumulated CPU time (s) 1056.41
Current children cumulated vsize (Kb) 184888

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 43962 0 0 0 106357 282 0 0 25 0 1 0 1788444476 188317696 43573 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 45976 43573 145 145 0 45831 0
[pid=11111] vsize: 183904
Current children cumulated CPU time (s) 1066.39
Current children cumulated vsize (Kb) 186028

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 44242 0 0 0 107351 285 0 0 25 0 1 0 1788444476 189460480 43853 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11111/statm): 46255 43853 145 145 0 46110 0
[pid=11111] vsize: 185020
Current children cumulated CPU time (s) 1076.36
Current children cumulated vsize (Kb) 187144

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 44525 0 0 0 108348 286 0 0 25 0 1 0 1788444476 190619648 44136 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 46538 44136 145 145 0 46393 0
[pid=11111] vsize: 186152
Current children cumulated CPU time (s) 1086.34
Current children cumulated vsize (Kb) 188276

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 44959 0 0 0 109344 287 0 0 25 0 1 0 1788444476 192393216 44570 4294967295 134512640 135094434 3221224432 3221223024 134557271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 46971 44570 145 145 0 46826 0
[pid=11111] vsize: 187884
Current children cumulated CPU time (s) 1096.31
Current children cumulated vsize (Kb) 190008

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 45341 0 0 0 110340 290 0 0 25 0 1 0 1788444476 193957888 44952 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 47353 44952 145 145 0 47208 0
[pid=11111] vsize: 189412
Current children cumulated CPU time (s) 1106.3
Current children cumulated vsize (Kb) 191536

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 45594 0 0 0 111337 291 0 0 25 0 1 0 1788444476 194977792 45205 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 47602 45205 145 145 0 47457 0
[pid=11111] vsize: 190408
Current children cumulated CPU time (s) 1116.28
Current children cumulated vsize (Kb) 192532

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 45851 0 0 0 112334 292 0 0 25 0 1 0 1788444476 196026368 45462 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 47858 45462 145 145 0 47713 0
[pid=11111] vsize: 191432
Current children cumulated CPU time (s) 1126.26
Current children cumulated vsize (Kb) 193556

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 46127 0 0 0 113329 294 0 0 25 0 1 0 1788444476 197152768 45738 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 48133 45738 145 145 0 47988 0
[pid=11111] vsize: 192532
Current children cumulated CPU time (s) 1136.23
Current children cumulated vsize (Kb) 194656

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 46539 0 0 0 114325 296 0 0 25 0 1 0 1788444476 198836224 46150 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 48544 46150 145 145 0 48399 0
[pid=11111] vsize: 194176
Current children cumulated CPU time (s) 1146.21
Current children cumulated vsize (Kb) 196300

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 46756 0 0 0 115322 297 0 0 25 0 1 0 1788444476 199720960 46367 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 48760 46367 145 145 0 48615 0
[pid=11111] vsize: 195040
Current children cumulated CPU time (s) 1156.19
Current children cumulated vsize (Kb) 197164

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 46954 0 0 0 116318 299 0 0 25 0 1 0 1788444476 200531968 46565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 48958 46565 145 145 0 48813 0
[pid=11111] vsize: 195832
Current children cumulated CPU time (s) 1166.17
Current children cumulated vsize (Kb) 197956

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 47217 0 0 0 117315 300 0 0 25 0 1 0 1788444476 201601024 46828 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 49219 46828 145 145 0 49074 0
[pid=11111] vsize: 196876
Current children cumulated CPU time (s) 1176.15
Current children cumulated vsize (Kb) 199000

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 47422 0 0 0 118313 302 0 0 25 0 1 0 1788444476 202465280 47033 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 49430 47033 145 145 0 49285 0
[pid=11111] vsize: 197720
Current children cumulated CPU time (s) 1186.15
Current children cumulated vsize (Kb) 199844

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 47743 0 0 0 119309 304 0 0 25 0 1 0 1788444476 203771904 47354 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 49749 47354 145 145 0 49604 0
[pid=11111] vsize: 198996
Current children cumulated CPU time (s) 1196.13
Current children cumulated vsize (Kb) 201120

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 47920 0 0 0 120307 305 0 0 25 0 1 0 1788444476 204509184 47531 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 49929 47531 145 145 0 49784 0
[pid=11111] vsize: 199716
Current children cumulated CPU time (s) 1206.12
Current children cumulated vsize (Kb) 201840



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11111
Raw data (/proc/11107/stat): 11107 (minisat+_script) S 11106 11107 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788444471 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11107/statm): 531 226 485 147 0 384 0
[pid=11107] vsize: 2124
Raw data (/proc/11111/stat): 11111 (minisat+_64-bit) R 11107 11107 1333 0 -1 0 47920 0 0 0 120307 305 0 0 25 0 1 0 1788444476 204509184 47531 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11111/statm): 49929 47531 145 145 0 49784 0
[pid=11111] vsize: 199716
Current children cumulated CPU time (s) 1206.12
Current children cumulated vsize (Kb) 201840

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1206.21
CPU user time (s): 1203.08
CPU system time (s): 3.13852
CPU usage (%): 99.6715
Max. virtual memory (cumulated for all children) (Kb): 201840

Verifier Data

ERROR: no interpretation found !