Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-air04.opb
MD5SUMeb0734273e24196dd14c6f237b52fa81
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 2683

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907684 kB
Buffers:         33616 kB
Cached:          63716 kB
SwapCached:        792 kB
Active:          31864 kB
Inactive:        68164 kB
HighTotal:      131008 kB
HighFree:        66192 kB
LowTotal:       903652 kB
LowFree:        841492 kB
SwapTotal:     2097892 kB
SwapFree:      2096664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            21224 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 21:01:11 (client local time) WITH STATUS 0 IN 1206.12 SECONDS
stats: 2841 7 1206.12 0

Solver Data

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

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/24826/stat): 24826 (minisat+_script) R 24825 24826 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844201494 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24826/statm): 174 3 169 147 0 27 0
[pid=24826] 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=24827
New process pid=24828
New process pid=24829
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=24828) exited with status: 0
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=24829) exited with status: 0
One traced child (pid=24827) exited with status: 0
New process pid=24830
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-air04.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.95 0.98 4/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 10940 0 0 0 895 51 0 0 25 0 1 0 1844201499 52555776 10550 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 12831 10550 145 145 0 12686 0
[pid=24830] vsize: 51324
Current children cumulated CPU time (s) 9.48
Current children cumulated vsize (Kb) 53448

[startup+20.006 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 11186 0 0 0 1889 53 0 0 25 0 1 0 1844201499 53526528 10796 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 13068 10796 145 145 0 12923 0
[pid=24830] vsize: 52272
Current children cumulated CPU time (s) 19.44
Current children cumulated vsize (Kb) 54396

[startup+30.0078 s]
Raw data (loadavg): 0.95 0.96 0.98 1/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) T 24826 24826 19818 0 -1 0 11524 0 0 0 2882 56 0 0 25 0 1 0 1844201499 54919168 11134 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24830/statm): 13408 11134 145 145 0 13263 0
[pid=24830] vsize: 53632
Current children cumulated CPU time (s) 29.4
Current children cumulated vsize (Kb) 55756

[startup+40.0086 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 12112 0 0 0 3871 61 0 0 25 0 1 0 1844201499 57319424 11722 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 13994 11722 145 145 0 13849 0
[pid=24830] vsize: 55976
Current children cumulated CPU time (s) 39.34
Current children cumulated vsize (Kb) 58100

[startup+50.0094 s]
Raw data (loadavg): 0.96 0.96 0.98 1/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) T 24826 24826 19818 0 -1 0 12603 0 0 0 4861 65 0 0 25 0 1 0 1844201499 59355136 12213 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24830/statm): 14491 12213 145 145 0 14346 0
[pid=24830] vsize: 57964
Current children cumulated CPU time (s) 49.28
Current children cumulated vsize (Kb) 60088

[startup+60.0101 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 12856 0 0 0 5856 68 0 0 25 0 1 0 1844201499 60383232 12466 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 14742 12466 145 145 0 14597 0
[pid=24830] vsize: 58968
Current children cumulated CPU time (s) 59.26
Current children cumulated vsize (Kb) 61092

[startup+70.0109 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 13099 0 0 0 6852 69 0 0 25 0 1 0 1844201499 61370368 12709 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 14983 12709 145 145 0 14838 0
[pid=24830] vsize: 59932
Current children cumulated CPU time (s) 69.23
Current children cumulated vsize (Kb) 62056

[startup+80.0117 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 13388 0 0 0 7847 73 0 0 25 0 1 0 1844201499 62545920 12998 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 15270 12998 145 145 0 15125 0
[pid=24830] vsize: 61080
Current children cumulated CPU time (s) 79.22
Current children cumulated vsize (Kb) 63204

[startup+90.0125 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 13636 0 0 0 8843 75 0 0 25 0 1 0 1844201499 63619072 13246 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 15532 13246 145 145 0 15387 0
[pid=24830] vsize: 62128
Current children cumulated CPU time (s) 89.2
Current children cumulated vsize (Kb) 64252

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 13991 0 0 0 9837 78 0 0 25 0 1 0 1844201499 65064960 13601 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 15885 13601 145 145 0 15740 0
[pid=24830] vsize: 63540
Current children cumulated CPU time (s) 99.17
Current children cumulated vsize (Kb) 65664

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 14340 0 0 0 10832 81 0 0 25 0 1 0 1844201499 66486272 13950 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 16232 13950 145 145 0 16087 0
[pid=24830] vsize: 64928
Current children cumulated CPU time (s) 109.15
Current children cumulated vsize (Kb) 67052

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 14795 0 0 0 11824 84 0 0 25 0 1 0 1844201499 68341760 14405 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 16685 14405 145 145 0 16540 0
[pid=24830] vsize: 66740
Current children cumulated CPU time (s) 119.1
Current children cumulated vsize (Kb) 68864

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 15042 0 0 0 12819 87 0 0 25 0 1 0 1844201499 69345280 14652 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 16930 14652 145 145 0 16785 0
[pid=24830] vsize: 67720
Current children cumulated CPU time (s) 129.08
Current children cumulated vsize (Kb) 69844

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 15316 0 0 0 13814 89 0 0 25 0 1 0 1844201499 70463488 14926 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 17203 14926 145 145 0 17058 0
[pid=24830] vsize: 68812
Current children cumulated CPU time (s) 139.05
Current children cumulated vsize (Kb) 70936

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 15622 0 0 0 14807 92 0 0 25 0 1 0 1844201499 71708672 15232 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 17507 15232 145 145 0 17362 0
[pid=24830] vsize: 70028
Current children cumulated CPU time (s) 149.01
Current children cumulated vsize (Kb) 72152

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 16046 0 0 0 15800 95 0 0 25 0 1 0 1844201499 73437184 15656 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 17929 15656 145 145 0 17784 0
[pid=24830] vsize: 71716
Current children cumulated CPU time (s) 158.97
Current children cumulated vsize (Kb) 73840

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 16291 0 0 0 16796 97 0 0 25 0 1 0 1844201499 74420224 15901 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 18169 15901 145 145 0 18024 0
[pid=24830] vsize: 72676
Current children cumulated CPU time (s) 168.95
Current children cumulated vsize (Kb) 74800

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 16682 0 0 0 17790 99 0 0 25 0 1 0 1844201499 76148736 16292 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 18591 16292 145 145 0 18446 0
[pid=24830] vsize: 74364
Current children cumulated CPU time (s) 178.91
Current children cumulated vsize (Kb) 76488

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 16898 0 0 0 18786 101 0 0 25 0 1 0 1844201499 77029376 16508 4294967295 134512640 135094434 3221224432 3221223092 134553454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 18806 16508 145 145 0 18661 0
[pid=24830] vsize: 75224
Current children cumulated CPU time (s) 188.89
Current children cumulated vsize (Kb) 77348

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 17257 0 0 0 19779 104 0 0 25 0 1 0 1844201499 78491648 16867 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 19163 16867 145 145 0 19018 0
[pid=24830] vsize: 76652
Current children cumulated CPU time (s) 198.85
Current children cumulated vsize (Kb) 78776

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 17671 0 0 0 20771 107 0 0 25 0 1 0 1844201499 80179200 17281 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 19575 17281 145 145 0 19430 0
[pid=24830] vsize: 78300
Current children cumulated CPU time (s) 208.8
Current children cumulated vsize (Kb) 80424

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 17943 0 0 0 21767 108 0 0 25 0 1 0 1844201499 81276928 17553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 19843 17553 145 145 0 19698 0
[pid=24830] vsize: 79372
Current children cumulated CPU time (s) 218.77
Current children cumulated vsize (Kb) 81496

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 18155 0 0 0 22764 110 0 0 25 0 1 0 1844201499 82145280 17765 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 20055 17765 145 145 0 19910 0
[pid=24830] vsize: 80220
Current children cumulated CPU time (s) 228.76
Current children cumulated vsize (Kb) 82344

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 18475 0 0 0 23758 113 0 0 25 0 1 0 1844201499 83427328 18085 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 20368 18085 145 145 0 20223 0
[pid=24830] vsize: 81472
Current children cumulated CPU time (s) 238.73
Current children cumulated vsize (Kb) 83596

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 18794 0 0 0 24754 114 0 0 25 0 1 0 1844201499 84717568 18404 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 20683 18404 145 145 0 20538 0
[pid=24830] vsize: 82732
Current children cumulated CPU time (s) 248.7
Current children cumulated vsize (Kb) 84856

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 19185 0 0 0 25748 118 0 0 25 0 1 0 1844201499 86319104 18795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 21074 18795 145 145 0 20929 0
[pid=24830] vsize: 84296
Current children cumulated CPU time (s) 258.68
Current children cumulated vsize (Kb) 86420

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 19622 0 0 0 26740 121 0 0 25 0 1 0 1844201499 88100864 19232 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 21509 19232 145 145 0 21364 0
[pid=24830] vsize: 86036
Current children cumulated CPU time (s) 268.63
Current children cumulated vsize (Kb) 88160

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 19847 0 0 0 27736 123 0 0 25 0 1 0 1844201499 89018368 19457 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 21733 19457 145 145 0 21588 0
[pid=24830] vsize: 86932
Current children cumulated CPU time (s) 278.61
Current children cumulated vsize (Kb) 89056

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 20050 0 0 0 28732 125 0 0 25 0 1 0 1844201499 89845760 19660 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 21935 19660 145 145 0 21790 0
[pid=24830] vsize: 87740
Current children cumulated CPU time (s) 288.59
Current children cumulated vsize (Kb) 89864

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 20345 0 0 0 29728 127 0 0 25 0 1 0 1844201499 91054080 19955 4294967295 134512640 135094434 3221224432 3221223024 134557391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 22230 19955 145 145 0 22085 0
[pid=24830] vsize: 88920
Current children cumulated CPU time (s) 298.57
Current children cumulated vsize (Kb) 91044

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 20655 0 0 0 30722 129 0 0 25 0 1 0 1844201499 92315648 20265 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 22538 20265 145 145 0 22393 0
[pid=24830] vsize: 90152
Current children cumulated CPU time (s) 308.53
Current children cumulated vsize (Kb) 92276

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 21023 0 0 0 31717 131 0 0 25 0 1 0 1844201499 93818880 20633 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 22905 20633 145 145 0 22760 0
[pid=24830] vsize: 91620
Current children cumulated CPU time (s) 318.5
Current children cumulated vsize (Kb) 93744

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 21276 0 0 0 32713 133 0 0 25 0 1 0 1844201499 94859264 20886 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 23159 20886 145 145 0 23014 0
[pid=24830] vsize: 92636
Current children cumulated CPU time (s) 328.48
Current children cumulated vsize (Kb) 94760

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 21520 0 0 0 33709 135 0 0 25 0 1 0 1844201499 95854592 21130 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 23402 21130 145 145 0 23257 0
[pid=24830] vsize: 93608
Current children cumulated CPU time (s) 338.46
Current children cumulated vsize (Kb) 95732

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 21825 0 0 0 34703 137 0 0 25 0 1 0 1844201499 97099776 21435 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 23706 21435 145 145 0 23561 0
[pid=24830] vsize: 94824
Current children cumulated CPU time (s) 348.42
Current children cumulated vsize (Kb) 96948

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 22089 0 0 0 35698 140 0 0 25 0 1 0 1844201499 98172928 21699 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 23968 21699 145 145 0 23823 0
[pid=24830] vsize: 95872
Current children cumulated CPU time (s) 358.4
Current children cumulated vsize (Kb) 97996

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 22456 0 0 0 36693 142 0 0 25 0 1 0 1844201499 99667968 22066 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 24333 22066 145 145 0 24188 0
[pid=24830] vsize: 97332
Current children cumulated CPU time (s) 368.37
Current children cumulated vsize (Kb) 99456

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 23094 0 0 0 37685 145 0 0 25 0 1 0 1844201499 102285312 22704 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 24972 22704 145 145 0 24827 0
[pid=24830] vsize: 99888
Current children cumulated CPU time (s) 378.32
Current children cumulated vsize (Kb) 102012

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 23374 0 0 0 38681 146 0 0 25 0 1 0 1844201499 103419904 22984 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 25249 22984 145 145 0 25104 0
[pid=24830] vsize: 100996
Current children cumulated CPU time (s) 388.29
Current children cumulated vsize (Kb) 103120

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 23594 0 0 0 39677 148 0 0 25 0 1 0 1844201499 104316928 23204 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 25468 23204 145 145 0 25323 0
[pid=24830] vsize: 101872
Current children cumulated CPU time (s) 398.27
Current children cumulated vsize (Kb) 103996

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 23929 0 0 0 40670 151 0 0 25 0 1 0 1844201499 105652224 23539 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 25794 23539 145 145 0 25649 0
[pid=24830] vsize: 103176
Current children cumulated CPU time (s) 408.23
Current children cumulated vsize (Kb) 105300

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 24250 0 0 0 41665 153 0 0 25 0 1 0 1844201499 107225088 23860 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 26178 23860 145 145 0 26033 0
[pid=24830] vsize: 104712
Current children cumulated CPU time (s) 418.2
Current children cumulated vsize (Kb) 106836

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 24692 0 0 0 42657 156 0 0 25 0 1 0 1844201499 109031424 24302 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 26619 24302 145 145 0 26474 0
[pid=24830] vsize: 106476
Current children cumulated CPU time (s) 428.15
Current children cumulated vsize (Kb) 108600

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 25035 0 0 0 43652 159 0 0 25 0 1 0 1844201499 110432256 24645 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 26961 24645 145 145 0 26816 0
[pid=24830] vsize: 107844
Current children cumulated CPU time (s) 438.13
Current children cumulated vsize (Kb) 109968

[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 25369 0 0 0 44648 160 0 0 25 0 1 0 1844201499 111796224 24979 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 27294 24979 145 145 0 27149 0
[pid=24830] vsize: 109176
Current children cumulated CPU time (s) 448.1
Current children cumulated vsize (Kb) 111300

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 25655 0 0 0 45642 163 0 0 25 0 1 0 1844201499 112963584 25265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 27579 25265 145 145 0 27434 0
[pid=24830] vsize: 110316
Current children cumulated CPU time (s) 458.07
Current children cumulated vsize (Kb) 112440

[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 25869 0 0 0 46639 164 0 0 25 0 1 0 1844201499 113840128 25479 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 27793 25479 145 145 0 27648 0
[pid=24830] vsize: 111172
Current children cumulated CPU time (s) 468.05
Current children cumulated vsize (Kb) 113296

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 26112 0 0 0 47635 166 0 0 25 0 1 0 1844201499 114831360 25722 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 28035 25722 145 145 0 27890 0
[pid=24830] vsize: 112140
Current children cumulated CPU time (s) 478.03
Current children cumulated vsize (Kb) 114264

[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 26411 0 0 0 48630 167 0 0 25 0 1 0 1844201499 116051968 26021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 28333 26021 145 145 0 28188 0
[pid=24830] vsize: 113332
Current children cumulated CPU time (s) 487.99
Current children cumulated vsize (Kb) 115456

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 26763 0 0 0 49625 169 0 0 25 0 1 0 1844201499 117489664 26373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 28684 26373 145 145 0 28539 0
[pid=24830] vsize: 114736
Current children cumulated CPU time (s) 497.96
Current children cumulated vsize (Kb) 116860

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 26992 0 0 0 50621 170 0 0 25 0 1 0 1844201499 118423552 26602 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 28912 26602 145 145 0 28767 0
[pid=24830] vsize: 115648
Current children cumulated CPU time (s) 507.93
Current children cumulated vsize (Kb) 117772

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 27326 0 0 0 51615 173 0 0 25 0 1 0 1844201499 119787520 26936 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 29245 26936 145 145 0 29100 0
[pid=24830] vsize: 116980
Current children cumulated CPU time (s) 517.9
Current children cumulated vsize (Kb) 119104

[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 27649 0 0 0 52610 174 0 0 25 0 1 0 1844201499 121102336 27259 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 29566 27259 145 145 0 29421 0
[pid=24830] vsize: 118264
Current children cumulated CPU time (s) 527.86
Current children cumulated vsize (Kb) 120388

[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 27918 0 0 0 53606 177 0 0 25 0 1 0 1844201499 122200064 27528 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 29834 27528 145 145 0 29689 0
[pid=24830] vsize: 119336
Current children cumulated CPU time (s) 537.85
Current children cumulated vsize (Kb) 121460

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 28243 0 0 0 54602 178 0 0 25 0 1 0 1844201499 123527168 27853 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 30158 27853 145 145 0 30013 0
[pid=24830] vsize: 120632
Current children cumulated CPU time (s) 547.82
Current children cumulated vsize (Kb) 122756

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 28466 0 0 0 55598 180 0 0 25 0 1 0 1844201499 124436480 28076 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 30380 28076 145 145 0 30235 0
[pid=24830] vsize: 121520
Current children cumulated CPU time (s) 557.8
Current children cumulated vsize (Kb) 123644

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 28782 0 0 0 56593 182 0 0 25 0 1 0 1844201499 125730816 28392 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 30696 28392 145 145 0 30551 0
[pid=24830] vsize: 122784
Current children cumulated CPU time (s) 567.77
Current children cumulated vsize (Kb) 124908

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 29053 0 0 0 57587 185 0 0 25 0 1 0 1844201499 126832640 28663 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 30965 28663 145 145 0 30820 0
[pid=24830] vsize: 123860
Current children cumulated CPU time (s) 577.74
Current children cumulated vsize (Kb) 125984

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 29301 0 0 0 58585 186 0 0 25 0 1 0 1844201499 127844352 28911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 31212 28911 145 145 0 31067 0
[pid=24830] vsize: 124848
Current children cumulated CPU time (s) 587.73
Current children cumulated vsize (Kb) 126972

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 29622 0 0 0 59579 188 0 0 25 0 1 0 1844201499 129155072 29232 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 31532 29232 145 145 0 31387 0
[pid=24830] vsize: 126128
Current children cumulated CPU time (s) 597.69
Current children cumulated vsize (Kb) 128252

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 29931 0 0 0 60573 190 0 0 25 0 1 0 1844201499 130416640 29541 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 31840 29541 145 145 0 31695 0
[pid=24830] vsize: 127360
Current children cumulated CPU time (s) 607.65
Current children cumulated vsize (Kb) 129484

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 30276 0 0 0 61567 193 0 0 25 0 1 0 1844201499 131825664 29886 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 32184 29886 145 145 0 32039 0
[pid=24830] vsize: 128736
Current children cumulated CPU time (s) 617.62
Current children cumulated vsize (Kb) 130860

[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 30670 0 0 0 62559 195 0 0 25 0 1 0 1844201499 133427200 30280 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 32575 30280 145 145 0 32430 0
[pid=24830] vsize: 130300
Current children cumulated CPU time (s) 627.56
Current children cumulated vsize (Kb) 132424

[startup+640.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 31005 0 0 0 63554 198 0 0 25 0 1 0 1844201499 134795264 30615 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 32909 30615 145 145 0 32764 0
[pid=24830] vsize: 131636
Current children cumulated CPU time (s) 637.54
Current children cumulated vsize (Kb) 133760

[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 31314 0 0 0 64548 200 0 0 25 0 1 0 1844201499 136060928 30924 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 33218 30924 145 145 0 33073 0
[pid=24830] vsize: 132872
Current children cumulated CPU time (s) 647.5
Current children cumulated vsize (Kb) 134996

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 31713 0 0 0 65541 203 0 0 25 0 1 0 1844201499 137699328 31323 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 33618 31323 145 145 0 33473 0
[pid=24830] vsize: 134472
Current children cumulated CPU time (s) 657.46
Current children cumulated vsize (Kb) 136596

[startup+670.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 31889 0 0 0 66538 205 0 0 25 0 1 0 1844201499 138416128 31499 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 33793 31499 145 145 0 33648 0
[pid=24830] vsize: 135172
Current children cumulated CPU time (s) 667.45
Current children cumulated vsize (Kb) 137296

[startup+680.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 32188 0 0 0 67532 207 0 0 25 0 1 0 1844201499 139636736 31798 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 34091 31798 145 145 0 33946 0
[pid=24830] vsize: 136364
Current children cumulated CPU time (s) 677.41
Current children cumulated vsize (Kb) 138488

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 32529 0 0 0 68529 209 0 0 25 0 1 0 1844201499 141041664 32139 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 34434 32139 145 145 0 34289 0
[pid=24830] vsize: 137736
Current children cumulated CPU time (s) 687.4
Current children cumulated vsize (Kb) 139860

[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 32795 0 0 0 69525 210 0 0 25 0 1 0 1844201499 142127104 32405 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 34699 32405 145 145 0 34554 0
[pid=24830] vsize: 138796
Current children cumulated CPU time (s) 697.37
Current children cumulated vsize (Kb) 140920

[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 33006 0 0 0 70522 212 0 0 25 0 1 0 1844201499 142987264 32616 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 34909 32616 145 145 0 34764 0
[pid=24830] vsize: 139636
Current children cumulated CPU time (s) 707.36
Current children cumulated vsize (Kb) 141760

[startup+720.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 33274 0 0 0 71518 214 0 0 25 0 1 0 1844201499 144089088 32884 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 35178 32884 145 145 0 35033 0
[pid=24830] vsize: 140712
Current children cumulated CPU time (s) 717.34
Current children cumulated vsize (Kb) 142836

[startup+730.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 33569 0 0 0 72514 215 0 0 25 0 1 0 1844201499 145293312 33179 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 35472 33179 145 145 0 35327 0
[pid=24830] vsize: 141888
Current children cumulated CPU time (s) 727.31
Current children cumulated vsize (Kb) 144012

[startup+740.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 33864 0 0 0 73511 217 0 0 25 0 1 0 1844201499 146493440 33474 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 35765 33474 145 145 0 35620 0
[pid=24830] vsize: 143060
Current children cumulated CPU time (s) 737.3
Current children cumulated vsize (Kb) 145184

[startup+750.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 34177 0 0 0 74507 218 0 0 25 0 1 0 1844201499 147771392 33787 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 36077 33787 145 145 0 35932 0
[pid=24830] vsize: 144308
Current children cumulated CPU time (s) 747.27
Current children cumulated vsize (Kb) 146432

[startup+760.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 34461 0 0 0 75503 221 0 0 25 0 1 0 1844201499 148934656 34071 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 36361 34071 145 145 0 36216 0
[pid=24830] vsize: 145444
Current children cumulated CPU time (s) 757.26
Current children cumulated vsize (Kb) 147568

[startup+770.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 34782 0 0 0 76499 223 0 0 25 0 1 0 1844201499 150245376 34392 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 36681 34392 145 145 0 36536 0
[pid=24830] vsize: 146724
Current children cumulated CPU time (s) 767.24
Current children cumulated vsize (Kb) 148848

[startup+780.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 35104 0 0 0 77493 226 0 0 25 0 1 0 1844201499 151560192 34714 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 37002 34714 145 145 0 36857 0
[pid=24830] vsize: 148008
Current children cumulated CPU time (s) 777.21
Current children cumulated vsize (Kb) 150132

[startup+790.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 35342 0 0 0 78489 228 0 0 25 0 1 0 1844201499 152522752 34952 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 37237 34952 145 145 0 37092 0
[pid=24830] vsize: 148948
Current children cumulated CPU time (s) 787.19
Current children cumulated vsize (Kb) 151072

[startup+800.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 35701 0 0 0 79483 231 0 0 25 0 1 0 1844201499 153989120 35311 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 37595 35311 145 145 0 37450 0
[pid=24830] vsize: 150380
Current children cumulated CPU time (s) 797.16
Current children cumulated vsize (Kb) 152504

[startup+810.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 36043 0 0 0 80476 234 0 0 25 0 1 0 1844201499 155385856 35653 4294967295 134512640 135094434 3221224432 3221223024 134556918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 37936 35653 145 145 0 37791 0
[pid=24830] vsize: 151744
Current children cumulated CPU time (s) 807.12
Current children cumulated vsize (Kb) 153868

[startup+820.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 36293 0 0 0 81471 236 0 0 25 0 1 0 1844201499 156405760 35903 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 38185 35903 145 145 0 38040 0
[pid=24830] vsize: 152740
Current children cumulated CPU time (s) 817.09
Current children cumulated vsize (Kb) 154864

[startup+830.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 36567 0 0 0 82467 237 0 0 25 0 1 0 1844201499 157523968 36177 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 38458 36177 145 145 0 38313 0
[pid=24830] vsize: 153832
Current children cumulated CPU time (s) 827.06
Current children cumulated vsize (Kb) 155956

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 36829 0 0 0 83463 238 0 0 25 0 1 0 1844201499 158601216 36439 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 38721 36439 145 145 0 38576 0
[pid=24830] vsize: 154884
Current children cumulated CPU time (s) 837.03
Current children cumulated vsize (Kb) 157008

[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 37240 0 0 0 84459 240 0 0 25 0 1 0 1844201499 160280576 36850 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 39131 36850 145 145 0 38986 0
[pid=24830] vsize: 156524
Current children cumulated CPU time (s) 847.01
Current children cumulated vsize (Kb) 158648

[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 37668 0 0 0 85455 242 0 0 25 0 1 0 1844201499 162029568 37278 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 39558 37278 145 145 0 39413 0
[pid=24830] vsize: 158232
Current children cumulated CPU time (s) 856.99
Current children cumulated vsize (Kb) 160356

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 38055 0 0 0 86450 244 0 0 25 0 1 0 1844201499 163614720 37665 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 39945 37665 145 145 0 39800 0
[pid=24830] vsize: 159780
Current children cumulated CPU time (s) 866.96
Current children cumulated vsize (Kb) 161904

[startup+880.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 38357 0 0 0 87446 246 0 0 25 0 1 0 1844201499 164847616 37967 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 40246 37967 145 145 0 40101 0
[pid=24830] vsize: 160984
Current children cumulated CPU time (s) 876.94
Current children cumulated vsize (Kb) 163108

[startup+890.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 38651 0 0 0 88441 247 0 0 25 0 1 0 1844201499 166043648 38261 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 40538 38261 145 145 0 40393 0
[pid=24830] vsize: 162152
Current children cumulated CPU time (s) 886.9
Current children cumulated vsize (Kb) 164276

[startup+900.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 38956 0 0 0 89437 249 0 0 25 0 1 0 1844201499 167284736 38566 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 40841 38566 145 145 0 40696 0
[pid=24830] vsize: 163364
Current children cumulated CPU time (s) 896.88
Current children cumulated vsize (Kb) 165488

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 39218 0 0 0 90432 251 0 0 25 0 1 0 1844201499 168353792 38828 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 41102 38828 145 145 0 40957 0
[pid=24830] vsize: 164408
Current children cumulated CPU time (s) 906.85
Current children cumulated vsize (Kb) 166532

[startup+920.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 39581 0 0 0 91425 253 0 0 25 0 1 0 1844201499 169836544 39191 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 41464 39191 145 145 0 41319 0
[pid=24830] vsize: 165856
Current children cumulated CPU time (s) 916.8
Current children cumulated vsize (Kb) 167980

[startup+930.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 39975 0 0 0 92418 257 0 0 25 0 1 0 1844201499 171446272 39585 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 41857 39585 145 145 0 41712 0
[pid=24830] vsize: 167428
Current children cumulated CPU time (s) 926.77
Current children cumulated vsize (Kb) 169552

[startup+940.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 40384 0 0 0 93413 259 0 0 25 0 1 0 1844201499 173117440 39994 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 42265 39994 145 145 0 42120 0
[pid=24830] vsize: 169060
Current children cumulated CPU time (s) 936.74
Current children cumulated vsize (Kb) 171184

[startup+950.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 40768 0 0 0 94409 261 0 0 25 0 1 0 1844201499 174690304 40378 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 42649 40378 145 145 0 42504 0
[pid=24830] vsize: 170596
Current children cumulated CPU time (s) 946.72
Current children cumulated vsize (Kb) 172720

[startup+960.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 41214 0 0 0 95403 264 0 0 25 0 1 0 1844201499 176513024 40824 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 43094 40824 145 145 0 42949 0
[pid=24830] vsize: 172376
Current children cumulated CPU time (s) 956.69
Current children cumulated vsize (Kb) 174500

[startup+970.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) T 24826 24826 19818 0 -1 0 41599 0 0 0 96399 265 0 0 25 0 1 0 1844201499 178085888 41209 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24830/statm): 43478 41209 145 145 0 43333 0
[pid=24830] vsize: 173912
Current children cumulated CPU time (s) 966.66
Current children cumulated vsize (Kb) 176036

[startup+980.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 42011 0 0 0 97396 266 0 0 25 0 1 0 1844201499 179773440 41621 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 43890 41621 145 145 0 43745 0
[pid=24830] vsize: 175560
Current children cumulated CPU time (s) 976.64
Current children cumulated vsize (Kb) 177684

[startup+990.078 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 42343 0 0 0 98392 268 0 0 25 0 1 0 1844201499 181125120 41953 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 44220 41953 145 145 0 44075 0
[pid=24830] vsize: 176880
Current children cumulated CPU time (s) 986.62
Current children cumulated vsize (Kb) 179004

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 42554 0 0 0 99387 271 0 0 25 0 1 0 1844201499 181989376 42164 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 44431 42164 145 145 0 44286 0
[pid=24830] vsize: 177724
Current children cumulated CPU time (s) 996.6
Current children cumulated vsize (Kb) 179848

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 42850 0 0 0 100382 273 0 0 25 0 1 0 1844201499 183193600 42460 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 44725 42460 145 145 0 44580 0
[pid=24830] vsize: 178900
Current children cumulated CPU time (s) 1006.57
Current children cumulated vsize (Kb) 181024

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 43183 0 0 0 101378 275 0 0 25 0 1 0 1844201499 184557568 42793 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 45058 42793 145 145 0 44913 0
[pid=24830] vsize: 180232
Current children cumulated CPU time (s) 1016.55
Current children cumulated vsize (Kb) 182356

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 43482 0 0 0 102374 277 0 0 25 0 1 0 1844201499 185778176 43092 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 45356 43092 145 145 0 45211 0
[pid=24830] vsize: 181424
Current children cumulated CPU time (s) 1026.53
Current children cumulated vsize (Kb) 183548

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 43849 0 0 0 103370 279 0 0 25 0 1 0 1844201499 187277312 43459 4294967295 134512640 135094434 3221224432 3221223024 134556906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 45722 43459 145 145 0 45577 0
[pid=24830] vsize: 182888
Current children cumulated CPU time (s) 1036.51
Current children cumulated vsize (Kb) 185012

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 44270 0 0 0 104365 281 0 0 25 0 1 0 1844201499 189001728 43880 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 46143 43880 145 145 0 45998 0
[pid=24830] vsize: 184572
Current children cumulated CPU time (s) 1046.48
Current children cumulated vsize (Kb) 186696

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 44505 0 0 0 105361 283 0 0 25 0 1 0 1844201499 190496768 44115 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 46508 44115 145 145 0 46363 0
[pid=24830] vsize: 186032
Current children cumulated CPU time (s) 1056.46
Current children cumulated vsize (Kb) 188156

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 44773 0 0 0 106356 285 0 0 25 0 1 0 1844201499 191590400 44383 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 46775 44383 145 145 0 46630 0
[pid=24830] vsize: 187100
Current children cumulated CPU time (s) 1066.43
Current children cumulated vsize (Kb) 189224

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 45066 0 0 0 107353 287 0 0 25 0 1 0 1844201499 192790528 44676 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 47068 44676 145 145 0 46923 0
[pid=24830] vsize: 188272
Current children cumulated CPU time (s) 1076.42
Current children cumulated vsize (Kb) 190396

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 45333 0 0 0 108349 288 0 0 25 0 1 0 1844201499 193880064 44943 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 47334 44943 145 145 0 47189 0
[pid=24830] vsize: 189336
Current children cumulated CPU time (s) 1086.39
Current children cumulated vsize (Kb) 191460

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) T 24826 24826 19818 0 -1 0 45587 0 0 0 109345 290 0 0 25 0 1 0 1844201499 194916352 45197 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24830/statm): 47587 45197 145 145 0 47442 0
[pid=24830] vsize: 190348
Current children cumulated CPU time (s) 1096.37
Current children cumulated vsize (Kb) 192472

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 45936 0 0 0 110339 292 0 0 25 0 1 0 1844201499 196337664 45546 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 47934 45546 145 145 0 47789 0
[pid=24830] vsize: 191736
Current children cumulated CPU time (s) 1106.33
Current children cumulated vsize (Kb) 193860

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 46280 0 0 0 111332 295 0 0 25 0 1 0 1844201499 197742592 45890 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24830/statm): 48277 45890 145 145 0 48132 0
[pid=24830] vsize: 193108
Current children cumulated CPU time (s) 1116.29
Current children cumulated vsize (Kb) 195232

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 46597 0 0 0 112325 297 0 0 25 0 1 0 1844201499 199036928 46207 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 48593 46207 145 145 0 48448 0
[pid=24830] vsize: 194372
Current children cumulated CPU time (s) 1126.24
Current children cumulated vsize (Kb) 196496

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 46934 0 0 0 113320 299 0 0 25 0 1 0 1844201499 200409088 46544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 48928 46544 145 145 0 48783 0
[pid=24830] vsize: 195712
Current children cumulated CPU time (s) 1136.21
Current children cumulated vsize (Kb) 197836

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 47155 0 0 0 114317 301 0 0 25 0 1 0 1844201499 201306112 46765 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 49147 46765 145 145 0 49002 0
[pid=24830] vsize: 196588
Current children cumulated CPU time (s) 1146.2
Current children cumulated vsize (Kb) 198712

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 47383 0 0 0 115314 302 0 0 25 0 1 0 1844201499 202235904 46993 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 49374 46993 145 145 0 49229 0
[pid=24830] vsize: 197496
Current children cumulated CPU time (s) 1156.18
Current children cumulated vsize (Kb) 199620

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 47683 0 0 0 116308 305 0 0 25 0 1 0 1844201499 203464704 47293 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 49674 47293 145 145 0 49529 0
[pid=24830] vsize: 198696
Current children cumulated CPU time (s) 1166.15
Current children cumulated vsize (Kb) 200820

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 48032 0 0 0 117303 308 0 0 25 0 1 0 1844201499 204902400 47642 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 50025 47642 145 145 0 49880 0
[pid=24830] vsize: 200100
Current children cumulated CPU time (s) 1176.13
Current children cumulated vsize (Kb) 202224

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 48389 0 0 0 118298 310 0 0 25 0 1 0 1844201499 206352384 47999 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 50379 47999 145 145 0 50234 0
[pid=24830] vsize: 201516
Current children cumulated CPU time (s) 1186.1
Current children cumulated vsize (Kb) 203640

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 48624 0 0 0 119294 311 0 0 25 0 1 0 1844201499 207306752 48234 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 50612 48234 145 145 0 50467 0
[pid=24830] vsize: 202448
Current children cumulated CPU time (s) 1196.07
Current children cumulated vsize (Kb) 204572

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 48952 0 0 0 120289 313 0 0 25 0 1 0 1844201499 208646144 48562 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 50939 48562 145 145 0 50794 0
[pid=24830] vsize: 203756
Current children cumulated CPU time (s) 1206.04
Current children cumulated vsize (Kb) 205880



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 24830
Raw data (/proc/24826/stat): 24826 (minisat+_script) S 24825 24826 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844201494 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24826/statm): 531 226 485 147 0 384 0
[pid=24826] vsize: 2124
Raw data (/proc/24830/stat): 24830 (minisat+_64-bit) R 24826 24826 19818 0 -1 0 48952 0 0 0 120289 313 0 0 25 0 1 0 1844201499 208646144 48562 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24830/statm): 50939 48562 145 145 0 50794 0
[pid=24830] vsize: 203756
Current children cumulated CPU time (s) 1206.04
Current children cumulated vsize (Kb) 205880

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1206.12
CPU user time (s): 1202.89
CPU system time (s): 3.22951
CPU usage (%): 99.6642
Max. virtual memory (cumulated for all children) (Kb): 205880

Verifier Data

ERROR: no interpretation found !