Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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 6071

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        915800 kB
Buffers:          3164 kB
Cached:          90784 kB
SwapCached:        708 kB
Active:          25168 kB
Inactive:        71436 kB
HighTotal:      131008 kB
HighFree:        35924 kB
LowTotal:       903652 kB
LowFree:        879876 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5756 kB
Slab:            16536 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:23:37 (client local time) WITH STATUS 0 IN 1206.09 SECONDS
stats: 3225 7 1206.09 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/24795/stat): 24795 (minisat+_script) R 24794 24795 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796925697 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24795/statm): 174 3 169 147 0 27 0
[pid=24795] 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=24796
New process pid=24797
New process pid=24798
execve syscall for /bin/sed executable
One traced child (pid=24797) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=24798) exited with status: 0
One traced child (pid=24796) exited with status: 0
New process pid=24799
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-air04.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 10940 0 0 0 900 49 0 0 25 0 1 0 1796925702 52555776 10550 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 12831 10550 145 145 0 12686 0
[pid=24799] vsize: 51324
Current children cumulated CPU time (s) 9.51
Current children cumulated vsize (Kb) 53448

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 11188 0 0 0 1895 51 0 0 25 0 1 0 1796925702 53534720 10798 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 13070 10798 145 145 0 12925 0
[pid=24799] vsize: 52280
Current children cumulated CPU time (s) 19.48
Current children cumulated vsize (Kb) 54404

[startup+30.006 s]
Raw data (loadavg): 0.95 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 11527 0 0 0 2890 53 0 0 25 0 1 0 1796925702 54931456 11137 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 13411 11137 145 145 0 13266 0
[pid=24799] vsize: 53644
Current children cumulated CPU time (s) 29.45
Current children cumulated vsize (Kb) 55768

[startup+40.0067 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 12123 0 0 0 3878 58 0 0 25 0 1 0 1796925702 57364480 11733 4294967295 134512640 135094434 3221224448 3221223084 134562042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 14005 11733 145 145 0 13860 0
[pid=24799] vsize: 56020
Current children cumulated CPU time (s) 39.38
Current children cumulated vsize (Kb) 58144

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 12609 0 0 0 4869 62 0 0 25 0 1 0 1796925702 59379712 12219 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 14497 12219 145 145 0 14352 0
[pid=24799] vsize: 57988
Current children cumulated CPU time (s) 49.33
Current children cumulated vsize (Kb) 60112

[startup+60.0082 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 12856 0 0 0 5865 64 0 0 25 0 1 0 1796925702 60383232 12466 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 14742 12466 145 145 0 14597 0
[pid=24799] vsize: 58968
Current children cumulated CPU time (s) 59.31
Current children cumulated vsize (Kb) 61092

[startup+70.0089 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 13094 0 0 0 6861 66 0 0 25 0 1 0 1796925702 61349888 12704 4294967295 134512640 135094434 3221224448 3221223120 134556468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 14978 12704 145 145 0 14833 0
[pid=24799] vsize: 59912
Current children cumulated CPU time (s) 69.29
Current children cumulated vsize (Kb) 62036

[startup+80.0107 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) T 24795 24795 824 0 -1 0 13379 0 0 0 7855 68 0 0 25 0 1 0 1796925702 62509056 12989 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24799/statm): 15261 12989 145 145 0 15116 0
[pid=24799] vsize: 61044
Current children cumulated CPU time (s) 79.25
Current children cumulated vsize (Kb) 63168

[startup+90.0114 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 13633 0 0 0 8850 70 0 0 25 0 1 0 1796925702 63606784 13243 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 15529 13243 145 145 0 15384 0
[pid=24799] vsize: 62116
Current children cumulated CPU time (s) 89.22
Current children cumulated vsize (Kb) 64240

[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 13986 0 0 0 9844 72 0 0 25 0 1 0 1796925702 65044480 13596 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 15880 13596 145 145 0 15735 0
[pid=24799] vsize: 63520
Current children cumulated CPU time (s) 99.18
Current children cumulated vsize (Kb) 65644

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 14312 0 0 0 10838 74 0 0 25 0 1 0 1796925702 66371584 13922 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 16204 13922 145 145 0 16059 0
[pid=24799] vsize: 64816
Current children cumulated CPU time (s) 109.14
Current children cumulated vsize (Kb) 66940

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 14780 0 0 0 11830 78 0 0 25 0 1 0 1796925702 68280320 14390 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 16670 14390 145 145 0 16525 0
[pid=24799] vsize: 66680
Current children cumulated CPU time (s) 119.1
Current children cumulated vsize (Kb) 68804

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 15017 0 0 0 12825 81 0 0 25 0 1 0 1796925702 69246976 14627 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 16906 14627 145 145 0 16761 0
[pid=24799] vsize: 67624
Current children cumulated CPU time (s) 129.08
Current children cumulated vsize (Kb) 69748

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 15291 0 0 0 13819 83 0 0 25 0 1 0 1796925702 70361088 14901 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 17178 14901 145 145 0 17033 0
[pid=24799] vsize: 68712
Current children cumulated CPU time (s) 139.04
Current children cumulated vsize (Kb) 70836

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 15592 0 0 0 14812 86 0 0 25 0 1 0 1796925702 71585792 15202 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 17477 15202 145 145 0 17332 0
[pid=24799] vsize: 69908
Current children cumulated CPU time (s) 149
Current children cumulated vsize (Kb) 72032

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 16023 0 0 0 15803 90 0 0 25 0 1 0 1796925702 73347072 15633 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 17907 15633 145 145 0 17762 0
[pid=24799] vsize: 71628
Current children cumulated CPU time (s) 158.95
Current children cumulated vsize (Kb) 73752

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 16282 0 0 0 16799 92 0 0 25 0 1 0 1796925702 74383360 15892 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 18160 15892 145 145 0 18015 0
[pid=24799] vsize: 72640
Current children cumulated CPU time (s) 168.93
Current children cumulated vsize (Kb) 74764

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 16671 0 0 0 17792 94 0 0 25 0 1 0 1796925702 76103680 16281 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 18580 16281 145 145 0 18435 0
[pid=24799] vsize: 74320
Current children cumulated CPU time (s) 178.88
Current children cumulated vsize (Kb) 76444

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 16871 0 0 0 18789 96 0 0 25 0 1 0 1796925702 76918784 16481 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 18779 16481 145 145 0 18634 0
[pid=24799] vsize: 75116
Current children cumulated CPU time (s) 188.87
Current children cumulated vsize (Kb) 77240

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 17230 0 0 0 19783 98 0 0 25 0 1 0 1796925702 78381056 16840 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 19136 16840 145 145 0 18991 0
[pid=24799] vsize: 76544
Current children cumulated CPU time (s) 198.83
Current children cumulated vsize (Kb) 78668

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 17620 0 0 0 20775 101 0 0 25 0 1 0 1796925702 79970304 17230 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 19524 17230 145 145 0 19379 0
[pid=24799] vsize: 78096
Current children cumulated CPU time (s) 208.78
Current children cumulated vsize (Kb) 80220

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 17919 0 0 0 21770 104 0 0 25 0 1 0 1796925702 81178624 17529 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 19819 17529 145 145 0 19674 0
[pid=24799] vsize: 79276
Current children cumulated CPU time (s) 218.76
Current children cumulated vsize (Kb) 81400

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 18139 0 0 0 22765 106 0 0 25 0 1 0 1796925702 82079744 17749 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 20039 17749 145 145 0 19894 0
[pid=24799] vsize: 80156
Current children cumulated CPU time (s) 228.73
Current children cumulated vsize (Kb) 82280

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 18395 0 0 0 23761 107 0 0 25 0 1 0 1796925702 83099648 18005 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 20288 18005 145 145 0 20143 0
[pid=24799] vsize: 81152
Current children cumulated CPU time (s) 238.7
Current children cumulated vsize (Kb) 83276

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 18771 0 0 0 24755 109 0 0 25 0 1 0 1796925702 84623360 18381 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 20660 18381 145 145 0 20515 0
[pid=24799] vsize: 82640
Current children cumulated CPU time (s) 248.66
Current children cumulated vsize (Kb) 84764

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 19117 0 0 0 25749 112 0 0 25 0 1 0 1796925702 86040576 18727 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 21006 18727 145 145 0 20861 0
[pid=24799] vsize: 84024
Current children cumulated CPU time (s) 258.63
Current children cumulated vsize (Kb) 86148

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 19556 0 0 0 26741 116 0 0 25 0 1 0 1796925702 87834624 19166 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 21444 19166 145 145 0 21299 0
[pid=24799] vsize: 85776
Current children cumulated CPU time (s) 268.59
Current children cumulated vsize (Kb) 87900

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 19839 0 0 0 27738 117 0 0 25 0 1 0 1796925702 88985600 19449 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 21725 19449 145 145 0 21580 0
[pid=24799] vsize: 86900
Current children cumulated CPU time (s) 278.57
Current children cumulated vsize (Kb) 89024

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 19998 0 0 0 28734 118 0 0 25 0 1 0 1796925702 89632768 19608 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 21883 19608 145 145 0 21738 0
[pid=24799] vsize: 87532
Current children cumulated CPU time (s) 288.54
Current children cumulated vsize (Kb) 89656

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 20283 0 0 0 29730 121 0 0 25 0 1 0 1796925702 90800128 19893 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 22168 19893 145 145 0 22023 0
[pid=24799] vsize: 88672
Current children cumulated CPU time (s) 298.53
Current children cumulated vsize (Kb) 90796

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 20576 0 0 0 30725 122 0 0 25 0 1 0 1796925702 91992064 20186 4294967295 134512640 135094434 3221224448 3221223040 134556928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 22459 20186 145 145 0 22314 0
[pid=24799] vsize: 89836
Current children cumulated CPU time (s) 308.49
Current children cumulated vsize (Kb) 91960

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 20938 0 0 0 31719 125 0 0 25 0 1 0 1796925702 93470720 20548 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 22820 20548 145 145 0 22675 0
[pid=24799] vsize: 91280
Current children cumulated CPU time (s) 318.46
Current children cumulated vsize (Kb) 93404

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 21212 0 0 0 32713 128 0 0 25 0 1 0 1796925702 94597120 20822 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 23095 20822 145 145 0 22950 0
[pid=24799] vsize: 92380
Current children cumulated CPU time (s) 328.43
Current children cumulated vsize (Kb) 94504

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 21458 0 0 0 33709 129 0 0 25 0 1 0 1796925702 95600640 21068 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 23340 21068 145 145 0 23195 0
[pid=24799] vsize: 93360
Current children cumulated CPU time (s) 338.4
Current children cumulated vsize (Kb) 95484

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 21780 0 0 0 34703 132 0 0 25 0 1 0 1796925702 96915456 21390 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 23661 21390 145 145 0 23516 0
[pid=24799] vsize: 94644
Current children cumulated CPU time (s) 348.37
Current children cumulated vsize (Kb) 96768

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 22047 0 0 0 35698 133 0 0 25 0 1 0 1796925702 98000896 21657 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 23926 21657 145 145 0 23781 0
[pid=24799] vsize: 95704
Current children cumulated CPU time (s) 358.33
Current children cumulated vsize (Kb) 97828

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 22319 0 0 0 36693 135 0 0 25 0 1 0 1796925702 99110912 21929 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 24197 21929 145 145 0 24052 0
[pid=24799] vsize: 96788
Current children cumulated CPU time (s) 368.3
Current children cumulated vsize (Kb) 98912

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 22932 0 0 0 37685 139 0 0 25 0 1 0 1796925702 101617664 22542 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 24809 22542 145 145 0 24664 0
[pid=24799] vsize: 99236
Current children cumulated CPU time (s) 378.26
Current children cumulated vsize (Kb) 101360

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 23305 0 0 0 38680 142 0 0 25 0 1 0 1796925702 103141376 22915 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 25181 22915 145 145 0 25036 0
[pid=24799] vsize: 100724
Current children cumulated CPU time (s) 388.24
Current children cumulated vsize (Kb) 102848

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 23538 0 0 0 39675 143 0 0 25 0 1 0 1796925702 104091648 23148 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 25413 23148 145 145 0 25268 0
[pid=24799] vsize: 101652
Current children cumulated CPU time (s) 398.2
Current children cumulated vsize (Kb) 103776

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 23840 0 0 0 40668 146 0 0 25 0 1 0 1796925702 105287680 23450 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 25705 23450 145 145 0 25560 0
[pid=24799] vsize: 102820
Current children cumulated CPU time (s) 408.16
Current children cumulated vsize (Kb) 104944

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 24161 0 0 0 41662 149 0 0 25 0 1 0 1796925702 106860544 23771 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 26089 23771 145 145 0 25944 0
[pid=24799] vsize: 104356
Current children cumulated CPU time (s) 418.13
Current children cumulated vsize (Kb) 106480

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 24568 0 0 0 42656 152 0 0 25 0 1 0 1796925702 108523520 24178 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 26495 24178 145 145 0 26350 0
[pid=24799] vsize: 105980
Current children cumulated CPU time (s) 428.1
Current children cumulated vsize (Kb) 108104

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 24980 0 0 0 43649 155 0 0 25 0 1 0 1796925702 110206976 24590 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 26906 24590 145 145 0 26761 0
[pid=24799] vsize: 107624
Current children cumulated CPU time (s) 438.06
Current children cumulated vsize (Kb) 109748

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 25302 0 0 0 44642 158 0 0 25 0 1 0 1796925702 111525888 24912 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 27228 24912 145 145 0 27083 0
[pid=24799] vsize: 108912
Current children cumulated CPU time (s) 448.02
Current children cumulated vsize (Kb) 111036

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 25567 0 0 0 45637 161 0 0 25 0 1 0 1796925702 112607232 25177 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 27492 25177 145 145 0 27347 0
[pid=24799] vsize: 109968
Current children cumulated CPU time (s) 458
Current children cumulated vsize (Kb) 112092

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 25811 0 0 0 46633 163 0 0 25 0 1 0 1796925702 113606656 25421 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 27736 25421 145 145 0 27591 0
[pid=24799] vsize: 110944
Current children cumulated CPU time (s) 467.98
Current children cumulated vsize (Kb) 113068

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 26039 0 0 0 47628 165 0 0 25 0 1 0 1796925702 114532352 25649 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 27962 25649 145 145 0 27817 0
[pid=24799] vsize: 111848
Current children cumulated CPU time (s) 477.95
Current children cumulated vsize (Kb) 113972

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 26353 0 0 0 48622 168 0 0 25 0 1 0 1796925702 115814400 25963 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 28275 25963 145 145 0 28130 0
[pid=24799] vsize: 113100
Current children cumulated CPU time (s) 487.92
Current children cumulated vsize (Kb) 115224

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 26693 0 0 0 49616 172 0 0 25 0 1 0 1796925702 117202944 26303 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 28614 26303 145 145 0 28469 0
[pid=24799] vsize: 114456
Current children cumulated CPU time (s) 497.9
Current children cumulated vsize (Kb) 116580

[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 26943 0 0 0 50612 174 0 0 25 0 1 0 1796925702 118226944 26553 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 28864 26553 145 145 0 28719 0
[pid=24799] vsize: 115456
Current children cumulated CPU time (s) 507.88
Current children cumulated vsize (Kb) 117580

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 27218 0 0 0 51608 176 0 0 25 0 1 0 1796925702 119349248 26828 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 29138 26828 145 145 0 28993 0
[pid=24799] vsize: 116552
Current children cumulated CPU time (s) 517.86
Current children cumulated vsize (Kb) 118676

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 27577 0 0 0 52602 179 0 0 25 0 1 0 1796925702 120807424 27187 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 29494 27187 145 145 0 29349 0
[pid=24799] vsize: 117976
Current children cumulated CPU time (s) 527.83
Current children cumulated vsize (Kb) 120100

[startup+540.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 27836 0 0 0 53598 180 0 0 25 0 1 0 1796925702 121864192 27446 4294967295 134512640 135094434 3221224448 3221223040 134556870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 29752 27446 145 145 0 29607 0
[pid=24799] vsize: 119008
Current children cumulated CPU time (s) 537.8
Current children cumulated vsize (Kb) 121132

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 28165 0 0 0 54592 183 0 0 25 0 1 0 1796925702 123207680 27775 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 30080 27775 145 145 0 29935 0
[pid=24799] vsize: 120320
Current children cumulated CPU time (s) 547.77
Current children cumulated vsize (Kb) 122444

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 28377 0 0 0 55589 185 0 0 25 0 1 0 1796925702 124071936 27987 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 30291 27987 145 145 0 30146 0
[pid=24799] vsize: 121164
Current children cumulated CPU time (s) 557.76
Current children cumulated vsize (Kb) 123288

[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 28675 0 0 0 56584 187 0 0 25 0 1 0 1796925702 125292544 28285 4294967295 134512640 135094434 3221224448 3221223120 134555602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 30589 28285 145 145 0 30444 0
[pid=24799] vsize: 122356
Current children cumulated CPU time (s) 567.73
Current children cumulated vsize (Kb) 124480

[startup+580.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 28976 0 0 0 57578 190 0 0 25 0 1 0 1796925702 126521344 28586 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 30889 28586 145 145 0 30744 0
[pid=24799] vsize: 123556
Current children cumulated CPU time (s) 577.7
Current children cumulated vsize (Kb) 125680

[startup+590.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 29252 0 0 0 58574 193 0 0 25 0 1 0 1796925702 127643648 28862 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 31163 28862 145 145 0 31018 0
[pid=24799] vsize: 124652
Current children cumulated CPU time (s) 587.69
Current children cumulated vsize (Kb) 126776

[startup+600.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 29546 0 0 0 59568 196 0 0 25 0 1 0 1796925702 128843776 29156 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 31456 29156 145 145 0 31311 0
[pid=24799] vsize: 125824
Current children cumulated CPU time (s) 597.66
Current children cumulated vsize (Kb) 127948

[startup+610.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 29870 0 0 0 60562 198 0 0 25 0 1 0 1796925702 130166784 29480 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 31779 29480 145 145 0 31634 0
[pid=24799] vsize: 127116
Current children cumulated CPU time (s) 607.62
Current children cumulated vsize (Kb) 129240

[startup+620.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 30192 0 0 0 61556 201 0 0 25 0 1 0 1796925702 131481600 29802 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 32100 29802 145 145 0 31955 0
[pid=24799] vsize: 128400
Current children cumulated CPU time (s) 617.59
Current children cumulated vsize (Kb) 130524

[startup+630.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 30577 0 0 0 62549 204 0 0 25 0 1 0 1796925702 133050368 30187 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 32483 30187 145 145 0 32338 0
[pid=24799] vsize: 129932
Current children cumulated CPU time (s) 627.55
Current children cumulated vsize (Kb) 132056

[startup+640.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 30905 0 0 0 63543 207 0 0 25 0 1 0 1796925702 134389760 30515 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 32810 30515 145 145 0 32665 0
[pid=24799] vsize: 131240
Current children cumulated CPU time (s) 637.52
Current children cumulated vsize (Kb) 133364

[startup+650.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 31229 0 0 0 64537 210 0 0 25 0 1 0 1796925702 135712768 30839 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 33133 30839 145 145 0 32988 0
[pid=24799] vsize: 132532
Current children cumulated CPU time (s) 647.49
Current children cumulated vsize (Kb) 134656

[startup+660.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 31633 0 0 0 65529 214 0 0 25 0 1 0 1796925702 137371648 31243 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 33538 31243 145 145 0 33393 0
[pid=24799] vsize: 134152
Current children cumulated CPU time (s) 657.45
Current children cumulated vsize (Kb) 136276

[startup+670.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 31846 0 0 0 66525 216 0 0 25 0 1 0 1796925702 138240000 31456 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 33750 31456 145 145 0 33605 0
[pid=24799] vsize: 135000
Current children cumulated CPU time (s) 667.43
Current children cumulated vsize (Kb) 137124

[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 32122 0 0 0 67521 217 0 0 25 0 1 0 1796925702 139366400 31732 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 34025 31732 145 145 0 33880 0
[pid=24799] vsize: 136100
Current children cumulated CPU time (s) 677.4
Current children cumulated vsize (Kb) 138224

[startup+690.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 32462 0 0 0 68517 219 0 0 25 0 1 0 1796925702 140767232 32072 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 34367 32072 145 145 0 34222 0
[pid=24799] vsize: 137468
Current children cumulated CPU time (s) 687.38
Current children cumulated vsize (Kb) 139592

[startup+700.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 32732 0 0 0 69513 221 0 0 25 0 1 0 1796925702 141869056 32342 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 34636 32342 145 145 0 34491 0
[pid=24799] vsize: 138544
Current children cumulated CPU time (s) 697.36
Current children cumulated vsize (Kb) 140668

[startup+710.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 32939 0 0 0 70510 222 0 0 25 0 1 0 1796925702 142712832 32549 4294967295 134512640 135094434 3221224448 3221223088 134562066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 34842 32549 145 145 0 34697 0
[pid=24799] vsize: 139368
Current children cumulated CPU time (s) 707.34
Current children cumulated vsize (Kb) 141492

[startup+720.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 33195 0 0 0 71506 224 0 0 25 0 1 0 1796925702 143765504 32805 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 35099 32805 145 145 0 34954 0
[pid=24799] vsize: 140396
Current children cumulated CPU time (s) 717.32
Current children cumulated vsize (Kb) 142520

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 33496 0 0 0 72501 227 0 0 25 0 1 0 1796925702 144994304 33106 4294967295 134512640 135094434 3221224448 3221223060 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 35399 33106 145 145 0 35254 0
[pid=24799] vsize: 141596
Current children cumulated CPU time (s) 727.3
Current children cumulated vsize (Kb) 143720

[startup+740.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 33773 0 0 0 73498 228 0 0 25 0 1 0 1796925702 146124800 33383 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 35675 33383 145 145 0 35530 0
[pid=24799] vsize: 142700
Current children cumulated CPU time (s) 737.28
Current children cumulated vsize (Kb) 144824

[startup+750.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 34086 0 0 0 74494 230 0 0 25 0 1 0 1796925702 147402752 33696 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 35987 33696 145 145 0 35842 0
[pid=24799] vsize: 143948
Current children cumulated CPU time (s) 747.26
Current children cumulated vsize (Kb) 146072

[startup+760.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 34385 0 0 0 75488 232 0 0 25 0 1 0 1796925702 148623360 33995 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24799/statm): 36285 33995 145 145 0 36140 0
[pid=24799] vsize: 145140
Current children cumulated CPU time (s) 757.22
Current children cumulated vsize (Kb) 147264

[startup+770.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 34668 0 0 0 76482 235 0 0 25 0 1 0 1796925702 149782528 34278 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 36568 34278 145 145 0 36423 0
[pid=24799] vsize: 146272
Current children cumulated CPU time (s) 767.19
Current children cumulated vsize (Kb) 148396

[startup+780.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 35025 0 0 0 77475 238 0 0 25 0 1 0 1796925702 151236608 34635 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 36923 34635 145 145 0 36778 0
[pid=24799] vsize: 147692
Current children cumulated CPU time (s) 777.15
Current children cumulated vsize (Kb) 149816

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 35254 0 0 0 78472 239 0 0 25 0 1 0 1796925702 152170496 34864 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 37151 34864 145 145 0 37006 0
[pid=24799] vsize: 148604
Current children cumulated CPU time (s) 787.13
Current children cumulated vsize (Kb) 150728

[startup+800.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 35582 0 0 0 79466 242 0 0 25 0 1 0 1796925702 153501696 35192 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 37476 35192 145 145 0 37331 0
[pid=24799] vsize: 149904
Current children cumulated CPU time (s) 797.1
Current children cumulated vsize (Kb) 152028

[startup+810.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 35970 0 0 0 80457 245 0 0 25 0 1 0 1796925702 155086848 35580 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 37863 35580 145 145 0 37718 0
[pid=24799] vsize: 151452
Current children cumulated CPU time (s) 807.04
Current children cumulated vsize (Kb) 153576

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 36193 0 0 0 81454 247 0 0 25 0 1 0 1796925702 155996160 35803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 38085 35803 145 145 0 37940 0
[pid=24799] vsize: 152340
Current children cumulated CPU time (s) 817.03
Current children cumulated vsize (Kb) 154464

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 36473 0 0 0 82450 249 0 0 25 0 1 0 1796925702 157147136 36083 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 38366 36083 145 145 0 38221 0
[pid=24799] vsize: 153464
Current children cumulated CPU time (s) 827.01
Current children cumulated vsize (Kb) 155588

[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 36747 0 0 0 83446 251 0 0 25 0 1 0 1796925702 158265344 36357 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 38639 36357 145 145 0 38494 0
[pid=24799] vsize: 154556
Current children cumulated CPU time (s) 836.99
Current children cumulated vsize (Kb) 156680

[startup+850.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 37071 0 0 0 84441 253 0 0 25 0 1 0 1796925702 159592448 36681 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 38963 36681 145 145 0 38818 0
[pid=24799] vsize: 155852
Current children cumulated CPU time (s) 846.96
Current children cumulated vsize (Kb) 157976

[startup+860.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 37541 0 0 0 85435 255 0 0 25 0 1 0 1796925702 161513472 37151 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 39432 37151 145 145 0 39287 0
[pid=24799] vsize: 157728
Current children cumulated CPU time (s) 856.92
Current children cumulated vsize (Kb) 159852

[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 37917 0 0 0 86429 258 0 0 25 0 1 0 1796925702 163053568 37527 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 39808 37527 145 145 0 39663 0
[pid=24799] vsize: 159232
Current children cumulated CPU time (s) 866.89
Current children cumulated vsize (Kb) 161356

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 38253 0 0 0 87425 261 0 0 25 0 1 0 1796925702 164421632 37863 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 40142 37863 145 145 0 39997 0
[pid=24799] vsize: 160568
Current children cumulated CPU time (s) 876.88
Current children cumulated vsize (Kb) 162692

[startup+890.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 38531 0 0 0 88419 263 0 0 25 0 1 0 1796925702 165556224 38141 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 40419 38141 145 145 0 40274 0
[pid=24799] vsize: 161676
Current children cumulated CPU time (s) 886.84
Current children cumulated vsize (Kb) 163800

[startup+900.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 38809 0 0 0 89415 265 0 0 25 0 1 0 1796925702 166686720 38419 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 40695 38419 145 145 0 40550 0
[pid=24799] vsize: 162780
Current children cumulated CPU time (s) 896.82
Current children cumulated vsize (Kb) 164904

[startup+910.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 39094 0 0 0 90409 267 0 0 25 0 1 0 1796925702 167845888 38704 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 40978 38704 145 145 0 40833 0
[pid=24799] vsize: 163912
Current children cumulated CPU time (s) 906.78
Current children cumulated vsize (Kb) 166036

[startup+920.086 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) T 24795 24795 824 0 -1 0 39396 0 0 0 91405 269 0 0 25 0 1 0 1796925702 169078784 39006 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24799/statm): 41279 39006 145 145 0 41134 0
[pid=24799] vsize: 165116
Current children cumulated CPU time (s) 916.76
Current children cumulated vsize (Kb) 167240

[startup+930.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 39791 0 0 0 92400 271 0 0 25 0 1 0 1796925702 170692608 39401 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 41673 39401 145 145 0 41528 0
[pid=24799] vsize: 166692
Current children cumulated CPU time (s) 926.73
Current children cumulated vsize (Kb) 168816

[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 40196 0 0 0 93396 272 0 0 25 0 1 0 1796925702 172355584 39806 4294967295 134512640 135094434 3221224448 3221223040 134557514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 42079 39806 145 145 0 41934 0
[pid=24799] vsize: 168316
Current children cumulated CPU time (s) 936.7
Current children cumulated vsize (Kb) 170440

[startup+950.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 40607 0 0 0 94391 274 0 0 25 0 1 0 1796925702 174034944 40217 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 42489 40217 145 145 0 42344 0
[pid=24799] vsize: 169956
Current children cumulated CPU time (s) 946.67
Current children cumulated vsize (Kb) 172080

[startup+960.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 40977 0 0 0 95385 277 0 0 25 0 1 0 1796925702 175542272 40587 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 42857 40587 145 145 0 42712 0
[pid=24799] vsize: 171428
Current children cumulated CPU time (s) 956.64
Current children cumulated vsize (Kb) 173552

[startup+970.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 41414 0 0 0 96379 279 0 0 25 0 1 0 1796925702 177332224 41024 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 43294 41024 145 145 0 43149 0
[pid=24799] vsize: 173176
Current children cumulated CPU time (s) 966.6
Current children cumulated vsize (Kb) 175300

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 41802 0 0 0 97375 281 0 0 25 0 1 0 1796925702 178917376 41412 4294967295 134512640 135094434 3221224448 3221223040 134556823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 43681 41412 145 145 0 43536 0
[pid=24799] vsize: 174724
Current children cumulated CPU time (s) 976.58
Current children cumulated vsize (Kb) 176848

[startup+990.092 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 42200 0 0 0 98371 283 0 0 25 0 1 0 1796925702 180551680 41810 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 44080 41810 145 145 0 43935 0
[pid=24799] vsize: 176320
Current children cumulated CPU time (s) 986.56
Current children cumulated vsize (Kb) 178444

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 42468 0 0 0 99367 285 0 0 25 0 1 0 1796925702 181637120 42078 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 44345 42078 145 145 0 44200 0
[pid=24799] vsize: 177380
Current children cumulated CPU time (s) 996.54
Current children cumulated vsize (Kb) 179504

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 42678 0 0 0 100363 286 0 0 25 0 1 0 1796925702 182493184 42288 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 44554 42288 145 145 0 44409 0
[pid=24799] vsize: 178216
Current children cumulated CPU time (s) 1006.51
Current children cumulated vsize (Kb) 180340

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 42996 0 0 0 101358 288 0 0 25 0 1 0 1796925702 183791616 42606 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 44871 42606 145 145 0 44726 0
[pid=24799] vsize: 179484
Current children cumulated CPU time (s) 1016.48
Current children cumulated vsize (Kb) 181608

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 43317 0 0 0 102354 290 0 0 25 0 1 0 1796925702 185102336 42927 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 45191 42927 145 145 0 45046 0
[pid=24799] vsize: 180764
Current children cumulated CPU time (s) 1026.46
Current children cumulated vsize (Kb) 182888

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 43674 0 0 0 103349 293 0 0 25 0 1 0 1796925702 186560512 43284 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 45547 43284 145 145 0 45402 0
[pid=24799] vsize: 182188
Current children cumulated CPU time (s) 1036.44
Current children cumulated vsize (Kb) 184312

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 44003 0 0 0 104343 295 0 0 25 0 1 0 1796925702 187904000 43613 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 45875 43613 145 145 0 45730 0
[pid=24799] vsize: 183500
Current children cumulated CPU time (s) 1046.4
Current children cumulated vsize (Kb) 185624

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 44366 0 0 0 105339 298 0 0 25 0 1 0 1796925702 189390848 43976 4294967295 134512640 135094434 3221224448 3221223040 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 46238 43976 145 145 0 46093 0
[pid=24799] vsize: 184952
Current children cumulated CPU time (s) 1056.39
Current children cumulated vsize (Kb) 187076

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 44629 0 0 0 106335 299 0 0 25 0 1 0 1796925702 191000576 44239 4294967295 134512640 135094434 3221224448 3221223040 134556990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 46631 44239 145 145 0 46486 0
[pid=24799] vsize: 186524
Current children cumulated CPU time (s) 1066.36
Current children cumulated vsize (Kb) 188648

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 44907 0 0 0 107331 300 0 0 25 0 1 0 1796925702 192139264 44517 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 46909 44517 145 145 0 46764 0
[pid=24799] vsize: 187636
Current children cumulated CPU time (s) 1076.33
Current children cumulated vsize (Kb) 189760

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 45170 0 0 0 108327 302 0 0 25 0 1 0 1796925702 193212416 44780 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 47171 44780 145 145 0 47026 0
[pid=24799] vsize: 188684
Current children cumulated CPU time (s) 1086.31
Current children cumulated vsize (Kb) 190808

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 45443 0 0 0 109324 303 0 0 25 0 1 0 1796925702 194326528 45053 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 47443 45053 145 145 0 47298 0
[pid=24799] vsize: 189772
Current children cumulated CPU time (s) 1096.29
Current children cumulated vsize (Kb) 191896

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 45733 0 0 0 110320 305 0 0 25 0 1 0 1796925702 195514368 45343 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 47733 45343 145 145 0 47588 0
[pid=24799] vsize: 190932
Current children cumulated CPU time (s) 1106.27
Current children cumulated vsize (Kb) 193056

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 46072 0 0 0 111315 308 0 0 25 0 1 0 1796925702 196894720 45682 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 48070 45682 145 145 0 47925 0
[pid=24799] vsize: 192280
Current children cumulated CPU time (s) 1116.25
Current children cumulated vsize (Kb) 194404

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 46420 0 0 0 112310 309 0 0 25 0 1 0 1796925702 198316032 46030 4294967295 134512640 135094434 3221224448 3221223040 134556928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 48417 46030 145 145 0 48272 0
[pid=24799] vsize: 193668
Current children cumulated CPU time (s) 1126.21
Current children cumulated vsize (Kb) 195792

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 46734 0 0 0 113304 312 0 0 25 0 1 0 1796925702 199593984 46344 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 48729 46344 145 145 0 48584 0
[pid=24799] vsize: 194916
Current children cumulated CPU time (s) 1136.18
Current children cumulated vsize (Kb) 197040

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 46982 0 0 0 114300 314 0 0 25 0 1 0 1796925702 200601600 46592 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 48975 46592 145 145 0 48830 0
[pid=24799] vsize: 195900
Current children cumulated CPU time (s) 1146.16
Current children cumulated vsize (Kb) 198024

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 47207 0 0 0 115296 316 0 0 25 0 1 0 1796925702 201519104 46817 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 49199 46817 145 145 0 49054 0
[pid=24799] vsize: 196796
Current children cumulated CPU time (s) 1156.14
Current children cumulated vsize (Kb) 198920

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 47472 0 0 0 116293 318 0 0 25 0 1 0 1796925702 202600448 47082 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 49463 47082 145 145 0 49318 0
[pid=24799] vsize: 197852
Current children cumulated CPU time (s) 1166.13
Current children cumulated vsize (Kb) 199976

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 47795 0 0 0 117288 320 0 0 25 0 1 0 1796925702 203931648 47405 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 49788 47405 145 145 0 49643 0
[pid=24799] vsize: 199152
Current children cumulated CPU time (s) 1176.1
Current children cumulated vsize (Kb) 201276

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 48147 0 0 0 118283 322 0 0 25 0 1 0 1796925702 205361152 47757 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 50137 47757 145 145 0 49992 0
[pid=24799] vsize: 200548
Current children cumulated CPU time (s) 1186.07
Current children cumulated vsize (Kb) 202672

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 48457 0 0 0 119278 324 0 0 25 0 1 0 1796925702 206630912 48067 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 50447 48067 145 145 0 50302 0
[pid=24799] vsize: 201788
Current children cumulated CPU time (s) 1196.04
Current children cumulated vsize (Kb) 203912

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 48731 0 0 0 120274 326 0 0 25 0 1 0 1796925702 207745024 48341 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 50719 48341 145 145 0 50574 0
[pid=24799] vsize: 202876
Current children cumulated CPU time (s) 1206.02
Current children cumulated vsize (Kb) 205000



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24799
Raw data (/proc/24795/stat): 24795 (minisat+_script) S 24794 24795 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796925697 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24795/statm): 531 226 485 147 0 384 0
[pid=24795] vsize: 2124
Raw data (/proc/24799/stat): 24799 (minisat+_64-bit) R 24795 24795 824 0 -1 0 48731 0 0 0 120274 326 0 0 25 0 1 0 1796925702 207745024 48341 4294967295 134512640 135094434 3221224448 3221223040 134552003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24799/statm): 50719 48341 145 145 0 50574 0
[pid=24799] vsize: 202876
Current children cumulated CPU time (s) 1206.02
Current children cumulated vsize (Kb) 205000

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1206.09
CPU user time (s): 1202.74
CPU system time (s): 3.35049
CPU usage (%): 99.6605
Max. virtual memory (cumulated for all children) (Kb): 205000

Verifier Data

ERROR: no interpretation found !