Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ar98.opb
MD5SUM181a05258ae35e5f3b5b834240f1847a
Bench Categoryoptimization, big integers (OPTBIGINT)
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 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 83886080000000
Number of bits of the biggest number in a constraint 47
Biggest sum of numbers in a constraint 572975239517507
Number of bits of the biggest sum of numbers50
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables20024
Total number of constraints17064
Number of constraints which are clauses1
Number of constraints which are cardinality constraints (but not clauses)16718
Number of constraints which are nor clauses,nor cardinality constraints345
Minimum length of a constraint1
Maximum length of a constraint15837

Trace number 5918

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        905060 kB
Buffers:           152 kB
Cached:          90424 kB
SwapCached:      11084 kB
Active:          22236 kB
Inactive:        80996 kB
HighTotal:      131008 kB
HighFree:        37044 kB
LowTotal:       903652 kB
LowFree:        868016 kB
SwapTotal:     2097892 kB
SwapFree:      2086124 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5416 kB
Slab:            20616 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:16:33 (client local time) WITH STATUS 0 IN 881.832 SECONDS
stats: 3095 7 881.832 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 32096] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1473 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss.
c ---[1475]---> BDD-cost:   12
c ---[1474]---> BDD-cost:   12
c ---[1473]---> BDD-cost:   12
c ---[1472]---> BDD-cost:   13
c ---[1470]---> BDD-cost:   13
c ---[1469]---> BDD-cost:   12
c ---[1468]---> BDD-cost:   13
c ---[1467]---> BDD-cost:   12
c ---[1466]---> BDD-cost:   13
c ---[1465]---> BDD-cost:   13
c ---[1464]---> BDD-cost:   12
c ---[1463]---> BDD-cost:   13
c ---[1462]---> BDD-cost:   13
c ---[1461]---> BDD-cost:   12
c ---[1460]---> BDD-cost:   13
c ---[1459]---> BDD-cost:   13
c ---[1458]---> BDD-cost:   13
c ---[1457]---> BDD-cost:   13
c ---[1456]---> BDD-cost:   13
c ---[1455]---> BDD-cost:   12
c ---[1454]---> BDD-cost:   11
c ---[1453]---> BDD-cost:   12
c ---[1452]---> BDD-cost:   13
c ---[1451]---> BDD-cost:   13
c ---[1450]---> BDD-cost:   13
c ---[1449]---> BDD-cost:   13
c ---[1448]---> BDD-cost:   12
c ---[1447]---> BDD-cost:   13
c ---[1446]---> BDD-cost:   13
c ---[1445]---> BDD-cost:   13
c ---[1444]---> BDD-cost:   13
c ---[1443]---> BDD-cost:   13
c ---[1442]---> BDD-cost:   13
c ---[1441]---> BDD-cost:   13
c ---[1440]---> BDD-cost:   13
c ---[1439]---> BDD-cost:   13
c ---[1438]---> BDD-cost:   13
c ---[1437]---> BDD-cost:   13
c ---[1436]---> BDD-cost:   12
c ---[1435]---> BDD-cost:   13
c ---[1434]---> BDD-cost:   13
c ---[1433]---> BDD-cost:   13
c ---[1432]---> BDD-cost:   13
c ---[1431]---> BDD-cost:   13
c ---[1430]---> BDD-cost:   13
c ---[1429]---> BDD-cost:   13
c ---[1428]---> BDD-cost:   13
c ---[1427]---> BDD-cost:   12
c ---[1426]---> BDD-cost:   13
c ---[1425]---> BDD-cost:   13
c ---[1424]---> BDD-cost:   13
c ---[1423]---> BDD-cost:   12
c ---[1422]---> BDD-cost:   12
c ---[1421]---> BDD-cost:   13
c ---[1420]---> BDD-cost:   13
c ---[1419]---> BDD-cost:   13
c ---[1418]---> BDD-cost:   13
c ---[1417]---> BDD-cost:   13
c ---[1416]---> BDD-cost:   13
c ---[1415]---> BDD-cost:   13
c ---[1414]---> BDD-cost:   13
c ---[1413]---> BDD-cost:   13
c ---[1412]---> BDD-cost:   13
c ---[1411]---> BDD-cost:   13
c ---[1410]---> BDD-cost:   12
c ---[1409]---> BDD-cost:   13
c ---[1408]---> BDD-cost:   13
c ---[1407]---> BDD-cost:   13
c ---[1406]---> BDD-cost:   13
c ---[1405]---> BDD-cost:   13
c ---[1404]---> BDD-cost:   12
c ---[1403]---> BDD-cost:   12
c ---[1402]---> BDD-cost:   13
c ---[1401]---> BDD-cost:   13
c ---[1400]---> BDD-cost:   13
c ---[1399]---> BDD-cost:   12
c ---[1398]---> BDD-cost:   13
c ---[1397]---> BDD-cost:   13
c ---[1396]---> BDD-cost:   13
c ---[1395]---> BDD-cost:   13
c ---[1394]---> BDD-cost:   13
c ---[1393]---> BDD-cost:   12
c ---[1392]---> BDD-cost:   13
c ---[1391]---> BDD-cost:   13
c ---[1390]---> BDD-cost:   13
c ---[1389]---> BDD-cost:   13
c ---[1388]---> BDD-cost:   13
c ---[1387]---> BDD-cost:   13
c ---[1386]---> BDD-cost:   13
c ---[1385]---> BDD-cost:   13
c ---[1384]---> BDD-cost:   13
c ---[1383]---> BDD-cost:   13
c ---[1381]---> BDD-cost:   13
c ---[1380]---> BDD-cost:   13
c ---[1379]---> BDD-cost:   13
c ---[1378]---> BDD-cost:   13
c ---[1377]---> BDD-cost:   13
c ---[1376]---> BDD-cost:   12
c ---[1375]---> BDD-cost:   13
c ---[1374]---> BDD-cost:   13
c ---[1373]---> BDD-cost:   12
c ---[1372]---> BDD-cost:   12
c ---[1371]---> BDD-cost:   12
c ---[1370]---> BDD-cost:   13
c ---[1369]---> BDD-cost:   13
c ---[1368]---> BDD-cost:   13
c ---[1367]---> BDD-cost:   13
c ---[1366]---> BDD-cost:   13
c ---[1365]---> BDD-cost:   12
c ---[1364]---> BDD-cost:   12
c ---[1362]---> BDD-cost:   13
c ---[1361]---> BDD-cost:   13
c ---[1360]---> BDD-cost:   13
c ---[1359]---> BDD-cost:   13
c ---[1358]---> BDD-cost:   13
c ---[1357]---> BDD-cost:   13
c ---[1356]---> BDD-cost:   13
c ---[1355]---> BDD-cost:   13
c ---[1354]---> BDD-cost:   13
c ---[1353]---> BDD-cost:   11
c ---[1352]---> BDD-cost:   13
c ---[1351]---> BDD-cost:   13
c ---[1350]---> BDD-cost:   12
c ---[1349]---> BDD-cost:   13
c ---[1348]---> BDD-cost:   13
c ---[1347]---> BDD-cost:   13
c ---[1346]---> BDD-cost:   13
c ---[1344]---> Adder-cost: 4370   maxlim: 4711424   bits: 23/23
c ---[1342]---> Adder-cost: 3378   maxlim: 4420608   bits: 23/23
c ---[1340]---> Adder-cost: 3212   maxlim: 3318784   bits: 22/22
c ---[1338]---> Adder-cost: 3118   maxlim: 3374080   bits: 22/22
c ---[1336]---> Adder-cost: 2686   maxlim: 2925568   bits: 22/22
c ---[1334]---> Adder-cost: 1564   maxlim: 1969152   bits: 21/21
c ---[1332]---> Adder-cost: 756   maxlim: 929792   bits: 20/20
c ---[1330]---> Adder-cost: 704   maxlim: 756736   bits: 20/20
c ---[1328]---> Adder-cost: 1236   maxlim: 1556480   bits: 21/21
c ---[1326]---> Adder-cost: 2132   maxlim: 2252800   bits: 22/22
c ---[1324]---> Adder-cost: 1340   maxlim: 1588224   bits: 21/21
c ---[1322]---> Adder-cost: 3828   maxlim: 4342784   bits: 23/23
c ---[1320]---> Adder-cost: 1388   maxlim: 1639424   bits: 21/21
c ---[1318]---> Adder-cost: 782   maxlim: 794624   bits: 20/20
c ---[1316]---> Adder-cost: 562   maxlim: 758784   bits: 20/20
c ---[1314]---> Adder-cost: 330   maxlim: 414720   bits: 19/19
c ---[1312]---> Adder-cost: 176   maxlim: 212992   bits: 18/18
c ---[1310]---> Adder-cost: 232   maxlim: 228352   bits: 18/18
c ---[1308]---> Adder-cost: 522   maxlim: 563200   bits: 20/20
c ---[1306]---> Adder-cost: 924   maxlim: 1088512   bits: 21/21
c ---[1304]---> Adder-cost: 4884   maxlim: 7817216   bits: 23/23
c ---[1302]---> Adder-cost: 3826   maxlim: 6107136   bits: 23/23
c ---[1300]---> Adder-cost: 776   maxlim: 4420608   bits: 23/23
c ---[1298]---> Adder-cost: 2220   maxlim: 3396608   bits: 22/22
c ---[1296]---> Adder-cost: 452   maxlim: 452608   bits: 19/19
c ---[1294]---> Adder-cost: 524   maxlim: 532480   bits: 20/20
c ---[1292]---> Adder-cost: 1474   maxlim: 2452480   bits: 22/22
c ---[1290]---> Adder-cost: 1944   maxlim: 3654656   bits: 22/22
c ---[1288]---> Adder-cost: 362   maxlim: 369664   bits: 19/19
c ---[1286]---> Sorter-cost: 1180     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1284]---> Adder-cost: 1814   maxlim: 2660352   bits: 22/22
c ---[1282]---> Adder-cost: 1258   maxlim: 2051072   bits: 21/21
c ---[1280]---> Adder-cost: 498   maxlim: 541696   bits: 20/20
c ---[1278]---> Adder-cost: 712   maxlim: 857088   bits: 20/20
c ---[1276]---> Adder-cost: 810   maxlim: 1186816   bits: 21/21
c ---[1274]---> Adder-cost: 250   maxlim: 271360   bits: 19/19
c ---[1272]---> Adder-cost: 210   maxlim: 271360   bits: 19/19
c ---[1270]---> Adder-cost: 342   maxlim: 493568   bits: 19/19
c ---[1268]---> Adder-cost: 476   maxlim: 559104   bits: 20/20
c ---[1266]---> Adder-cost: 1820   maxlim: 1997824   bits: 21/21
c ---[1264]---> Adder-cost: 2086   maxlim: 2534400   bits: 22/22
c ---[1262]---> BDD-cost:   79
c ---[1260]---> Adder-cost: 224   maxlim: 318464   bits: 19/19
c ---[1258]---> Adder-cost: 258   maxlim: 433152   bits: 19/19
c ---[1256]---> Adder-cost: 896   maxlim: 1175552   bits: 21/21
c ---[1254]---> Adder-cost: 1424   maxlim: 1523712   bits: 21/21
c ---[1252]---> Adder-cost: 3020   maxlim: 3462144   bits: 22/22
c ---[1250]---> Adder-cost: 1796   maxlim: 2198528   bits: 22/22
c ---[1248]---> Adder-cost: 4044   maxlim: 5436416   bits: 23/23
c ---[1246]---> Adder-cost: 192   maxlim: 269312   bits: 19/19
c ---[1244]---> Adder-cost: 228   maxlim: 289792   bits: 19/19
c ---[1242]---> Adder-cost: 334   maxlim: 496640   bits: 19/19
c ---[1240]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1238]---> Adder-cost: 656   maxlim: 825344   bits: 20/20
c ---[1236]---> Adder-cost: 270   maxlim: 825344   bits: 20/20
c ---[1234]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1232]---> Adder-cost: 1774   maxlim: 2400256   bits: 22/22
c ---[1230]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1228]---> Adder-cost: 380   maxlim: 538624   bits: 20/20
c ---[1226]---> Adder-cost: 142   maxlim: 188416   bits: 18/18
c ---[1224]---> Adder-cost: 464   maxlim: 786432   bits: 20/20
c ---[1222]---> Adder-cost: 152   maxlim: 148480   bits: 18/18
c ---[1220]---> Adder-cost: 466   maxlim: 531456   bits: 20/20
c ---[1218]---> Adder-cost: 2418   maxlim: 3253248   bits: 22/22
c ---[1216]---> Adder-cost: 1274   maxlim: 1677312   bits: 21/21
c ---[1214]---> Adder-cost: 4864   maxlim: 6126592   bits: 23/23
c ---[1212]---> Adder-cost: 1392   maxlim: 1899520   bits: 21/21
c ---[1210]---> Adder-cost: 3074   maxlim: 4076544   bits: 22/22
c ---[1208]---> Adder-cost: 4114   maxlim: 6376448   bits: 23/23
c ---[1206]---> Adder-cost: 1758   maxlim: 2183168   bits: 22/22
c ---[1204]---> Adder-cost: 2902   maxlim: 3851264   bits: 22/22
c ---[1202]---> Adder-cost: 1576   maxlim: 2208768   bits: 22/22
c ---[1200]---> Adder-cost: 3600   maxlim: 5413888   bits: 23/23
c ---[1198]---> Adder-cost: 232   maxlim: 271360   bits: 19/19
c ---[1196]---> Adder-cost: 156   maxlim: 174080   bits: 18/18
c ---[1194]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1192]---> Adder-cost: 1542   maxlim: 2054144   bits: 21/21
c ---[1190]---> Adder-cost: 1494   maxlim: 2045952   bits: 21/21
c ---[1188]---> Adder-cost: 758   maxlim: 1026048   bits: 20/20
c ---[1186]---> Adder-cost: 1014   maxlim: 1204224   bits: 21/21
c ---[1184]---> Adder-cost: 1460   maxlim: 2139136   bits: 22/22
c ---[1182]---> Adder-cost: 542   maxlim: 750   bits: 10/10
c ---[1180]---> Adder-cost: 860   maxlim: 1327104   bits: 21/21
c ---[1178]---> Adder-cost: 600   maxlim: 952320   bits: 20/20
c ---[1176]---> Sorter-cost: 1393     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1174]---> Adder-cost: 656   maxlim: 883712   bits: 20/20
c ---[1172]---> Adder-cost: 562   maxlim: 715776   bits: 20/20
c ---[1170]---> Adder-cost: 272   maxlim: 371712   bits: 19/19
c ---[1168]---> Adder-cost: 1440   maxlim: 1993728   bits: 21/21
c ---[1166]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost: 1051     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1162]---> Adder-cost: 246   maxlim: 434176   bits: 19/19
c ---[1160]---> Adder-cost: 608   maxlim: 1158144   bits: 21/21
c ---[1158]---> Adder-cost: 1120   maxlim: 2419712   bits: 22/22
c ---[1156]---> Adder-cost: 360   maxlim: 365568   bits: 19/19
c ---[1154]---> Adder-cost: 490   maxlim: 513024   bits: 20/19
c ---[1152]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1150]---> Sorter-cost: 1721     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1148]---> Sorter-cost: 1430     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Adder-cost: 832   maxlim: 963584   bits: 20/20
c ---[1144]---> Adder-cost: 1850   maxlim: 3003392   bits: 22/22
c ---[1142]---> Adder-cost: 1194   maxlim: 2665472   bits: 22/22
c ---[1140]---> Adder-cost: 206   maxlim: 242688   bits: 18/18
c ---[1138]---> Adder-cost: 254   maxlim: 491   bits: 9/9
c ---[1136]---> Adder-cost: 758   maxlim: 1467392   bits: 21/21
c ---[1134]---> Adder-cost: 120   maxlim: 178176   bits: 18/18
c ---[1132]---> Adder-cost: 192   maxlim: 324608   bits: 19/19
c ---[1130]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1128]---> Adder-cost: 1596   maxlim: 2703360   bits: 22/22
c ---[1126]---> Adder-cost: 856   maxlim: 1112064   bits: 21/21
c ---[1124]---> Adder-cost: 294   maxlim: 335872   bits: 19/19
c ---[1122]---> Adder-cost: 332   maxlim: 421888   bits: 19/19
c ---[1120]---> Adder-cost: 1674   maxlim: 2615296   bits: 22/22
c ---[1118]---> Adder-cost: 1610   maxlim: 2498560   bits: 22/22
c ---[1116]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1114]---> Adder-cost: 172   maxlim: 182272   bits: 18/18
c ---[1112]---> Adder-cost: 130   maxlim: 123904   bits: 18/17
c ---[1110]---> Adder-cost: 1116   maxlim: 1618944   bits: 21/21
c ---[1108]---> Adder-cost: 908   maxlim: 1317888   bits: 21/21
c ---[1106]---> Sorter-cost:  201     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Adder-cost: 444   maxlim: 544768   bits: 20/20
c ---[1102]---> BDD-cost:   53
c ---[1100]---> Adder-cost: 298   maxlim: 356352   bits: 19/19
c ---[1098]---> Adder-cost: 260   maxlim: 367616   bits: 19/19
c ---[1096]---> Adder-cost: 2140

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/32333/stat): 32333 (minisat+_script) R 32332 32333 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854705466 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/32333/statm): 174 3 169 147 0 27 0
[pid=32333] 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=32334
New process pid=32335
New process pid=32336
execve syscall for /bin/sed executable
One traced child (pid=32335) 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=32336) exited with status: 0
One traced child (pid=32334) exited with status: 0
New process pid=32337
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-blp-ar98.opb

[startup+10.0032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32337
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 346 0 0 0 986 3 0 0 25 0 1 0 1854705471 1810432 332 4294967295 134512640 135094434 3221224432 3221223328 134587994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 442 332 145 145 0 297 0
[pid=32337] vsize: 1768
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 3892

[startup+20.0051 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32337
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 478 0 0 0 1985 5 0 0 25 0 1 0 1854705471 2682880 461 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 655 461 145 145 0 510 0
[pid=32337] vsize: 2620
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 4744

[startup+30.0061 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32337
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 555 0 0 0 2982 6 0 0 25 0 1 0 1854705471 2854912 538 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 697 538 145 145 0 552 0
[pid=32337] vsize: 2788
Current children cumulated CPU time (s) 29.88
Current children cumulated vsize (Kb) 4912

[startup+40.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32337
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 581 0 0 0 3981 6 0 0 25 0 1 0 1854705471 2875392 564 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 702 564 145 145 0 557 0
[pid=32337] vsize: 2808
Current children cumulated CPU time (s) 39.87
Current children cumulated vsize (Kb) 4932

[startup+50.0079 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32337
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 628 0 0 0 4979 8 0 0 25 0 1 0 1854705471 3010560 611 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 735 611 145 145 0 590 0
[pid=32337] vsize: 2940
Current children cumulated CPU time (s) 49.87
Current children cumulated vsize (Kb) 5064

[startup+60.0089 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32339
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 662 0 0 0 5978 9 0 0 25 0 1 0 1854705471 3088384 645 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 754 645 145 145 0 609 0
[pid=32337] vsize: 3016
Current children cumulated CPU time (s) 59.87
Current children cumulated vsize (Kb) 5140

[startup+70.0098 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32339
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 848 0 0 0 6976 10 0 0 25 0 1 0 1854705471 4722688 824 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1153 824 145 145 0 1008 0
[pid=32337] vsize: 4612
Current children cumulated CPU time (s) 69.86
Current children cumulated vsize (Kb) 6736

[startup+80.0107 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32339
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 865 0 0 0 7975 11 0 0 25 0 1 0 1854705471 4722688 841 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1153 841 145 145 0 1008 0
[pid=32337] vsize: 4612
Current children cumulated CPU time (s) 79.86
Current children cumulated vsize (Kb) 6736

[startup+90.0126 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32339
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 927 0 0 0 8974 12 0 0 25 0 1 0 1854705471 5054464 903 4294967295 134512640 135094434 3221224432 3221223344 134587864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1234 903 145 145 0 1089 0
[pid=32337] vsize: 4936
Current children cumulated CPU time (s) 89.86
Current children cumulated vsize (Kb) 7060

[startup+100.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32339
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1034 0 0 0 9972 13 0 0 25 0 1 0 1854705471 5525504 1010 4294967295 134512640 135094434 3221224432 3221223316 134796016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1349 1010 145 145 0 1204 0
[pid=32337] vsize: 5396
Current children cumulated CPU time (s) 99.85
Current children cumulated vsize (Kb) 7520

[startup+110.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32339
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1100 0 0 0 10971 15 0 0 25 0 1 0 1854705471 5804032 1076 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1417 1076 145 145 0 1272 0
[pid=32337] vsize: 5668
Current children cumulated CPU time (s) 109.86
Current children cumulated vsize (Kb) 7792

[startup+120.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32341
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1181 0 0 0 11969 17 0 0 25 0 1 0 1854705471 6111232 1104 4294967295 134512640 135094434 3221224432 3221223316 134796016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1492 1104 145 145 0 1347 0
[pid=32337] vsize: 5968
Current children cumulated CPU time (s) 119.86
Current children cumulated vsize (Kb) 8092

[startup+130.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32341
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1218 0 0 0 12967 18 0 0 25 0 1 0 1854705471 6279168 1141 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1533 1141 145 145 0 1388 0
[pid=32337] vsize: 6132
Current children cumulated CPU time (s) 129.85
Current children cumulated vsize (Kb) 8256

[startup+140.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32341
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1218 0 0 0 13967 19 0 0 25 0 1 0 1854705471 6279168 1141 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1533 1141 145 145 0 1388 0
[pid=32337] vsize: 6132
Current children cumulated CPU time (s) 139.86
Current children cumulated vsize (Kb) 8256

[startup+150.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32341
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1346 0 0 0 14965 19 0 0 25 0 1 0 1854705471 6733824 1189 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1644 1189 145 145 0 1499 0
[pid=32337] vsize: 6576
Current children cumulated CPU time (s) 149.84
Current children cumulated vsize (Kb) 8700

[startup+160.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32341
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1489 0 0 0 15964 20 0 0 25 0 1 0 1854705471 7155712 1210 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1747 1210 145 145 0 1602 0
[pid=32337] vsize: 6988
Current children cumulated CPU time (s) 159.84
Current children cumulated vsize (Kb) 9112

[startup+170.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32341
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1548 0 0 0 16963 21 0 0 25 0 1 0 1854705471 7446528 1269 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1818 1269 145 145 0 1673 0
[pid=32337] vsize: 7272
Current children cumulated CPU time (s) 169.84
Current children cumulated vsize (Kb) 9396

[startup+180.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32343
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1586 0 0 0 17961 22 0 0 25 0 1 0 1854705471 7630848 1307 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1863 1307 145 145 0 1718 0
[pid=32337] vsize: 7452
Current children cumulated CPU time (s) 179.83
Current children cumulated vsize (Kb) 9576

[startup+190.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32343
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1692 0 0 0 18958 23 0 0 25 0 1 0 1854705471 8105984 1413 4294967295 134512640 135094434 3221224432 3221223324 134795992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 1979 1413 145 145 0 1834 0
[pid=32337] vsize: 7916
Current children cumulated CPU time (s) 189.81
Current children cumulated vsize (Kb) 10040

[startup+200.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32343
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1826 0 0 0 19955 25 0 0 25 0 1 0 1854705471 8695808 1547 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2123 1547 145 145 0 1978 0
[pid=32337] vsize: 8492
Current children cumulated CPU time (s) 199.8
Current children cumulated vsize (Kb) 10616

[startup+210.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32343
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 1901 0 0 0 20954 26 0 0 25 0 1 0 1854705471 9015296 1572 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2201 1572 145 145 0 2056 0
[pid=32337] vsize: 8804
Current children cumulated CPU time (s) 209.8
Current children cumulated vsize (Kb) 10928

[startup+220.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32343
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2018 0 0 0 21951 27 0 0 25 0 1 0 1854705471 9482240 1689 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2315 1689 145 145 0 2170 0
[pid=32337] vsize: 9260
Current children cumulated CPU time (s) 219.78
Current children cumulated vsize (Kb) 11384

[startup+230.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32343
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2139 0 0 0 22949 28 0 0 25 0 1 0 1854705471 9912320 1740 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2420 1740 145 145 0 2275 0
[pid=32337] vsize: 9680
Current children cumulated CPU time (s) 229.77
Current children cumulated vsize (Kb) 11804

[startup+240.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32345
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2297 0 0 0 23946 30 0 0 25 0 1 0 1854705471 10481664 1824 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2559 1824 145 145 0 2414 0
[pid=32337] vsize: 10236
Current children cumulated CPU time (s) 239.76
Current children cumulated vsize (Kb) 12360

[startup+250.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32345
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2369 0 0 0 24945 31 0 0 25 0 1 0 1854705471 10805248 1896 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2638 1896 145 145 0 2493 0
[pid=32337] vsize: 10552
Current children cumulated CPU time (s) 249.76
Current children cumulated vsize (Kb) 12676

[startup+260.029 s]
Raw data (loadavg): 1.00 1.00 0.95 1/58 32345
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) T 32333 32333 9102 0 -1 0 2524 0 0 0 25942 33 0 0 25 0 1 0 1854705471 11501568 2002 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2808 2002 145 145 0 2663 0
[pid=32337] vsize: 11232
Current children cumulated CPU time (s) 259.75
Current children cumulated vsize (Kb) 13356

[startup+270.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32345
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2592 0 0 0 26941 34 0 0 25 0 1 0 1854705471 11882496 2070 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 2901 2070 145 145 0 2756 0
[pid=32337] vsize: 11604
Current children cumulated CPU time (s) 269.75
Current children cumulated vsize (Kb) 13728

[startup+280.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32345
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2682 0 0 0 27939 35 0 0 25 0 1 0 1854705471 12292096 2160 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 3001 2160 145 145 0 2856 0
[pid=32337] vsize: 12004
Current children cumulated CPU time (s) 279.74
Current children cumulated vsize (Kb) 14128

[startup+290.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32345
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2762 0 0 0 28938 36 0 0 25 0 1 0 1854705471 12673024 2240 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 3094 2240 145 145 0 2949 0
[pid=32337] vsize: 12376
Current children cumulated CPU time (s) 289.74
Current children cumulated vsize (Kb) 14500

[startup+300.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32347
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2849 0 0 0 29935 38 0 0 25 0 1 0 1854705471 13082624 2327 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 3194 2327 145 145 0 3049 0
[pid=32337] vsize: 12776
Current children cumulated CPU time (s) 299.73
Current children cumulated vsize (Kb) 14900

[startup+310.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32347
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 2953 0 0 0 30933 39 0 0 25 0 1 0 1854705471 13537280 2431 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 3305 2431 145 145 0 3160 0
[pid=32337] vsize: 13220
Current children cumulated CPU time (s) 309.72
Current children cumulated vsize (Kb) 15344

[startup+320.035 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32347
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854705466 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32333/statm): 531 226 485 147 0 384 0
[pid=32333] vsize: 2124
Raw data (/proc/32337/stat): 32337 (minisat+_64-bit) R 32333 32333 9102 0 -1 0 3115 0 0 0 31931 40 0 0 25 0 1 0 1854705471 14073856 2479 4294967295 134512640 135094434 3221224432 3221223316 134796026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32337/statm): 3436 2479 145 145 0 3291 0
[pid=32337] vsize: 13744
Current children cumulated CPU time (s) 319.71
Current children cumulated vsize (Kb) 15868
One traced child (pid=32337) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=32348
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-blp-ar98.opb

[startup+330.036 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32348
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 327 0 0 0 662 3 0 0 25 0 1 0 1854737802 1851392 312 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 452 312 162 162 0 290 0
[pid=32348] vsize: 1808
Current children cumulated CPU time (s) 329.66
Current children cumulated vsize (Kb) 3936

[startup+340.037 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32348
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 478 0 0 0 1660 5 0 0 25 0 1 0 1854737802 2760704 460 4294967295 134512640 135167914 3221224448 3221223284 134860164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 674 460 162 162 0 512 0
[pid=32348] vsize: 2696
Current children cumulated CPU time (s) 339.66
Current children cumulated vsize (Kb) 4824

[startup+350.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32348
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 553 0 0 0 2659 6 0 0 25 0 1 0 1854737802 2932736 535 4294967295 134512640 135167914 3221224448 3221223268 134860169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 716 535 162 162 0 554 0
[pid=32348] vsize: 2864
Current children cumulated CPU time (s) 349.66
Current children cumulated vsize (Kb) 4992

[startup+360.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32350
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 575 0 0 0 3658 6 0 0 25 0 1 0 1854737802 2932736 557 4294967295 134512640 135167914 3221224448 3221223292 134860190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 716 557 162 162 0 554 0
[pid=32348] vsize: 2864
Current children cumulated CPU time (s) 359.65
Current children cumulated vsize (Kb) 4992

[startup+370.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32350
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 615 0 0 0 4657 8 0 0 25 0 1 0 1854737802 3022848 597 4294967295 134512640 135167914 3221224448 3221223296 134608465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 738 597 162 162 0 576 0
[pid=32348] vsize: 2952
Current children cumulated CPU time (s) 369.66
Current children cumulated vsize (Kb) 5080

[startup+380.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32350
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 660 0 0 0 5656 8 0 0 25 0 1 0 1854737802 3117056 642 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 761 642 162 162 0 599 0
[pid=32348] vsize: 3044
Current children cumulated CPU time (s) 379.65
Current children cumulated vsize (Kb) 5172

[startup+390.043 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32350
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 691 0 0 0 6655 9 0 0 25 0 1 0 1854737802 3198976 673 4294967295 134512640 135167914 3221224448 3221223296 134608428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 781 673 162 162 0 619 0
[pid=32348] vsize: 3124
Current children cumulated CPU time (s) 389.65
Current children cumulated vsize (Kb) 5252

[startup+400.043 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32350
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 881 0 0 0 7654 10 0 0 25 0 1 0 1854737802 4833280 856 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 1180 856 162 162 0 1018 0
[pid=32348] vsize: 4720
Current children cumulated CPU time (s) 399.65
Current children cumulated vsize (Kb) 6848

[startup+410.044 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32350
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 1075 0 0 0 8651 11 0 0 25 0 1 0 1854737802 5070848 924 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 1238 924 162 162 0 1076 0
[pid=32348] vsize: 4952
Current children cumulated CPU time (s) 409.63
Current children cumulated vsize (Kb) 7080

[startup+420.045 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32352
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 1277 0 0 0 9648 13 0 0 25 0 1 0 1854737802 5898240 1126 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 1440 1126 162 162 0 1278 0
[pid=32348] vsize: 5760
Current children cumulated CPU time (s) 419.62
Current children cumulated vsize (Kb) 7888

[startup+430.046 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32352
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 1350 0 0 0 10644 15 0 0 25 0 1 0 1854737802 6197248 1199 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 1513 1199 162 162 0 1351 0
[pid=32348] vsize: 6052
Current children cumulated CPU time (s) 429.6
Current children cumulated vsize (Kb) 8180

[startup+440.047 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32352
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 1411 0 0 0 11642 16 0 0 25 0 1 0 1854737802 6447104 1260 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 1574 1260 162 162 0 1412 0
[pid=32348] vsize: 6296
Current children cumulated CPU time (s) 439.59
Current children cumulated vsize (Kb) 8424

[startup+450.048 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32352
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 1546 0 0 0 12640 17 0 0 25 0 1 0 1854737802 7020544 1395 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 1714 1395 162 162 0 1552 0
[pid=32348] vsize: 6856
Current children cumulated CPU time (s) 449.58
Current children cumulated vsize (Kb) 8984

[startup+460.048 s]
Raw data (loadavg): 1.00 1.00 0.95 3/58 32352
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 1557 0 0 0 13639 18 0 0 25 0 1 0 1854737802 7045120 1406 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 1720 1406 162 162 0 1558 0
[pid=32348] vsize: 6880
Current children cumulated CPU time (s) 459.58
Current children cumulated vsize (Kb) 9008

[startup+470.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32352
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 1830 0 0 0 14636 20 0 0 25 0 1 0 1854737802 8167424 1679 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 1994 1679 162 162 0 1832 0
[pid=32348] vsize: 7976
Current children cumulated CPU time (s) 469.57
Current children cumulated vsize (Kb) 10104

[startup+480.051 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32354
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2005 0 0 0 15634 21 0 0 25 0 1 0 1854737802 8368128 1726 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 2043 1726 162 162 0 1881 0
[pid=32348] vsize: 8172
Current children cumulated CPU time (s) 479.56
Current children cumulated vsize (Kb) 10300

[startup+490.052 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32354
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2029 0 0 0 16632 22 0 0 25 0 1 0 1854737802 8474624 1750 4294967295 134512640 135167914 3221224448 3221223292 134860190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 2069 1750 162 162 0 1907 0
[pid=32348] vsize: 8276
Current children cumulated CPU time (s) 489.55
Current children cumulated vsize (Kb) 10404

[startup+500.053 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32354
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2080 0 0 0 17631 23 0 0 25 0 1 0 1854737802 8671232 1801 4294967295 134512640 135167914 3221224448 3221223284 134860174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 2117 1801 162 162 0 1955 0
[pid=32348] vsize: 8468
Current children cumulated CPU time (s) 499.55
Current children cumulated vsize (Kb) 10596

[startup+510.054 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32354
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2158 0 0 0 18629 23 0 0 25 0 1 0 1854737802 8982528 1879 4294967295 134512640 135167914 3221224448 3221223312 134608332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 2193 1879 162 162 0 2031 0
[pid=32348] vsize: 8772
Current children cumulated CPU time (s) 509.53
Current children cumulated vsize (Kb) 10900

[startup+520.055 s]
Raw data (loadavg): 1.00 1.00 0.95 3/58 32354
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2295 0 0 0 19625 25 0 0 25 0 1 0 1854737802 9543680 2016 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 2330 2016 162 162 0 2168 0
[pid=32348] vsize: 9320
Current children cumulated CPU time (s) 519.51
Current children cumulated vsize (Kb) 11448

[startup+530.056 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32354
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2483 0 0 0 20623 27 0 0 25 0 1 0 1854737802 10313728 2204 4294967295 134512640 135167914 3221224448 3221223284 134860174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 2518 2204 162 162 0 2356 0
[pid=32348] vsize: 10072
Current children cumulated CPU time (s) 529.51
Current children cumulated vsize (Kb) 12200

[startup+540.058 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32356
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2488 0 0 0 21621 28 0 0 25 0 1 0 1854737802 10334208 2209 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 2523 2209 162 162 0 2361 0
[pid=32348] vsize: 10092
Current children cumulated CPU time (s) 539.5
Current children cumulated vsize (Kb) 12220

[startup+550.058 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32356
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 2754 0 0 0 22616 30 0 0 25 0 1 0 1854737802 11059200 2385 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 2700 2385 162 162 0 2538 0
[pid=32348] vsize: 10800
Current children cumulated CPU time (s) 549.47
Current children cumulated vsize (Kb) 12928

[startup+560.059 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32356
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 3046 0 0 0 23610 33 0 0 25 0 1 0 1854737802 12259328 2677 4294967295 134512640 135167914 3221224448 3221222144 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 2993 2677 162 162 0 2831 0
[pid=32348] vsize: 11972
Current children cumulated CPU time (s) 559.44
Current children cumulated vsize (Kb) 14100

[startup+570.061 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32356
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 3186 0 0 0 24608 34 0 0 25 0 1 0 1854737802 12386304 2710 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 3024 2710 162 162 0 2862 0
[pid=32348] vsize: 12096
Current children cumulated CPU time (s) 569.43
Current children cumulated vsize (Kb) 14224

[startup+580.062 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32356
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 3369 0 0 0 25606 36 0 0 25 0 1 0 1854737802 13135872 2893 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 3207 2893 162 162 0 3045 0
[pid=32348] vsize: 12828
Current children cumulated CPU time (s) 579.43
Current children cumulated vsize (Kb) 14956

[startup+590.064 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32356
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) T 32333 32333 9102 0 -1 0 3574 0 0 0 26602 38 0 0 25 0 1 0 1854737802 13606912 3008 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32348/statm): 3322 3008 162 162 0 3160 0
[pid=32348] vsize: 13288
Current children cumulated CPU time (s) 589.41
Current children cumulated vsize (Kb) 15416

[startup+600.065 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32358
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 3709 0 0 0 27598 40 0 0 25 0 1 0 1854737802 14159872 3143 4294967295 134512640 135167914 3221224448 3221223296 134608317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 3457 3143 162 162 0 3295 0
[pid=32348] vsize: 13828
Current children cumulated CPU time (s) 599.39
Current children cumulated vsize (Kb) 15956

[startup+610.066 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32358
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 3853 0 0 0 28595 41 0 0 25 0 1 0 1854737802 14749696 3287 4294967295 134512640 135167914 3221224448 3221223284 134860174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 3601 3287 162 162 0 3439 0
[pid=32348] vsize: 14404
Current children cumulated CPU time (s) 609.37
Current children cumulated vsize (Kb) 16532

[startup+620.067 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32358
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 3946 0 0 0 29593 42 0 0 25 0 1 0 1854737802 15134720 3380 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 3695 3380 162 162 0 3533 0
[pid=32348] vsize: 14780
Current children cumulated CPU time (s) 619.36
Current children cumulated vsize (Kb) 16908

[startup+630.068 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32358
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 4063 0 0 0 30589 45 0 0 25 0 1 0 1854737802 15613952 3497 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 3812 3497 162 162 0 3650 0
[pid=32348] vsize: 15248
Current children cumulated CPU time (s) 629.35
Current children cumulated vsize (Kb) 17376

[startup+640.069 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32358
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 4191 0 0 0 31584 48 0 0 25 0 1 0 1854737802 16134144 3625 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 3939 3625 162 162 0 3777 0
[pid=32348] vsize: 15756
Current children cumulated CPU time (s) 639.33
Current children cumulated vsize (Kb) 17884

[startup+650.07 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32358
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) T 32333 32333 9102 0 -1 0 4357 0 0 0 32580 50 0 0 25 0 1 0 1854737802 16592896 3737 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32348/statm): 4051 3737 162 162 0 3889 0
[pid=32348] vsize: 16204
Current children cumulated CPU time (s) 649.31
Current children cumulated vsize (Kb) 18332

[startup+660.071 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32360
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 4636 0 0 0 33576 52 0 0 25 0 1 0 1854737802 17747968 4016 4294967295 134512640 135167914 3221224448 3221223292 134860190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 4333 4016 162 162 0 4171 0
[pid=32348] vsize: 17332
Current children cumulated CPU time (s) 659.29
Current children cumulated vsize (Kb) 19460

[startup+670.072 s]
Raw data (loadavg): 1.00 1.00 0.95 3/58 32360
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 4636 0 0 0 34574 53 0 0 25 0 1 0 1854737802 17747968 4016 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 4333 4016 162 162 0 4171 0
[pid=32348] vsize: 17332
Current children cumulated CPU time (s) 669.28
Current children cumulated vsize (Kb) 19460

[startup+680.073 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32360
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 4636 0 0 0 35572 54 0 0 25 0 1 0 1854737802 17747968 4016 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 4333 4016 162 162 0 4171 0
[pid=32348] vsize: 17332
Current children cumulated CPU time (s) 679.27
Current children cumulated vsize (Kb) 19460

[startup+690.074 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32360
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 4636 0 0 0 36570 55 0 0 25 0 1 0 1854737802 17747968 4016 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 4333 4016 162 162 0 4171 0
[pid=32348] vsize: 17332
Current children cumulated CPU time (s) 689.26
Current children cumulated vsize (Kb) 19460

[startup+700.074 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32360
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 4639 0 0 0 37568 56 0 0 25 0 1 0 1854737802 17747968 4019 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 4333 4019 162 162 0 4171 0
[pid=32348] vsize: 17332
Current children cumulated CPU time (s) 699.25
Current children cumulated vsize (Kb) 19460

[startup+710.075 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32360
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6305 0 0 0 38553 63 0 0 25 0 1 0 1854737802 20553728 4611 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 5018 4611 162 162 0 4856 0
[pid=32348] vsize: 20072
Current children cumulated CPU time (s) 709.17
Current children cumulated vsize (Kb) 22200

[startup+720.076 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32362
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6306 0 0 0 39550 64 0 0 25 0 1 0 1854737802 20553728 4612 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5018 4612 162 162 0 4856 0
[pid=32348] vsize: 20072
Current children cumulated CPU time (s) 719.15
Current children cumulated vsize (Kb) 22200

[startup+730.077 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32362
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6376 0 0 0 40549 64 0 0 25 0 1 0 1854737802 20844544 4682 4294967295 134512640 135167914 3221224448 3221223312 134608325 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5089 4682 162 162 0 4927 0
[pid=32348] vsize: 20356
Current children cumulated CPU time (s) 729.14
Current children cumulated vsize (Kb) 22484

[startup+740.077 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32362
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6498 0 0 0 41546 66 0 0 25 0 1 0 1854737802 21344256 4804 4294967295 134512640 135167914 3221224448 3221222784 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5211 4804 162 162 0 5049 0
[pid=32348] vsize: 20844
Current children cumulated CPU time (s) 739.13
Current children cumulated vsize (Kb) 22972

[startup+750.078 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32362
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6503 0 0 0 42544 67 0 0 25 0 1 0 1854737802 21344256 4809 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5211 4809 162 162 0 5049 0
[pid=32348] vsize: 20844
Current children cumulated CPU time (s) 749.12
Current children cumulated vsize (Kb) 22972

[startup+760.078 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32362
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6769 0 0 0 43541 69 0 0 25 0 1 0 1854737802 22433792 5075 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5477 5075 162 162 0 5315 0
[pid=32348] vsize: 21908
Current children cumulated CPU time (s) 759.11
Current children cumulated vsize (Kb) 24036

[startup+770.079 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32362
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6769 0 0 0 44540 69 0 0 25 0 1 0 1854737802 22433792 5075 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5477 5075 162 162 0 5315 0
[pid=32348] vsize: 21908
Current children cumulated CPU time (s) 769.1
Current children cumulated vsize (Kb) 24036

[startup+780.08 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32364
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6842 0 0 0 45538 71 0 0 25 0 1 0 1854737802 22749184 5148 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5554 5148 162 162 0 5392 0
[pid=32348] vsize: 22216
Current children cumulated CPU time (s) 779.1
Current children cumulated vsize (Kb) 24344

[startup+790.08 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32364
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6865 0 0 0 46536 71 0 0 25 0 1 0 1854737802 22822912 5171 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5572 5171 162 162 0 5410 0
[pid=32348] vsize: 22288
Current children cumulated CPU time (s) 789.08
Current children cumulated vsize (Kb) 24416

[startup+800.081 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32364
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 6975 0 0 0 47534 73 0 0 25 0 1 0 1854737802 23269376 5281 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5681 5281 162 162 0 5519 0
[pid=32348] vsize: 22724
Current children cumulated CPU time (s) 799.08
Current children cumulated vsize (Kb) 24852

[startup+810.082 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32364
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 7119 0 0 0 48531 74 0 0 25 0 1 0 1854737802 23851008 5425 4294967295 134512640 135167914 3221224448 3221223292 134860190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5823 5425 162 162 0 5661 0
[pid=32348] vsize: 23292
Current children cumulated CPU time (s) 809.06
Current children cumulated vsize (Kb) 25420

[startup+820.083 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32364
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 7236 0 0 0 49528 76 0 0 25 0 1 0 1854737802 24305664 5542 4294967295 134512640 135167914 3221224448 3221223288 134860153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 5934 5542 162 162 0 5772 0
[pid=32348] vsize: 23736
Current children cumulated CPU time (s) 819.05
Current children cumulated vsize (Kb) 25864

[startup+830.084 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32364
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 7396 0 0 0 50526 77 0 0 25 0 1 0 1854737802 24969216 5702 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 6096 5702 162 162 0 5934 0
[pid=32348] vsize: 24384
Current children cumulated CPU time (s) 829.04
Current children cumulated vsize (Kb) 26512

[startup+840.085 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32366
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 7532 0 0 0 51524 78 0 0 25 0 1 0 1854737802 25501696 5838 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 6226 5838 162 162 0 6064 0
[pid=32348] vsize: 24904
Current children cumulated CPU time (s) 839.03
Current children cumulated vsize (Kb) 27032

[startup+850.085 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32366
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 7691 0 0 0 52522 79 0 0 25 0 1 0 1854737802 26161152 5997 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 6387 5997 162 162 0 6225 0
[pid=32348] vsize: 25548
Current children cumulated CPU time (s) 849.02
Current children cumulated vsize (Kb) 27676

[startup+860.085 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32366
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 7756 0 0 0 53520 81 0 0 25 0 1 0 1854737802 26415104 6062 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 6449 6062 162 162 0 6287 0
[pid=32348] vsize: 25796
Current children cumulated CPU time (s) 859.02
Current children cumulated vsize (Kb) 27924

[startup+870.086 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32366
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 7858 0 0 0 54516 82 0 0 25 0 1 0 1854737802 26828800 6164 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 6550 6164 162 162 0 6388 0
[pid=32348] vsize: 26200
Current children cumulated CPU time (s) 868.99
Current children cumulated vsize (Kb) 28328

[startup+880.087 s]
Raw data (loadavg): 1.00 1.00 0.95 1/58 32366
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) T 32333 32333 9102 0 -1 0 7956 0 0 0 55514 83 0 0 25 0 1 0 1854737802 27217920 6262 4294967295 134512640 135167914 3221224448 3221222652 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32348/statm): 6645 6262 162 162 0 6483 0
[pid=32348] vsize: 26580
Current children cumulated CPU time (s) 878.98
Current children cumulated vsize (Kb) 28708

[startup+890.087 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32366
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 8064 0 0 0 56511 85 0 0 25 0 1 0 1854737802 27643904 6370 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 6749 6370 162 162 0 6587 0
[pid=32348] vsize: 26996
Current children cumulated CPU time (s) 888.97
Current children cumulated vsize (Kb) 29124

[startup+900.088 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32368
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 8282 0 0 0 57508 87 0 0 25 0 1 0 1854737802 28311552 6535 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 6912 6535 162 162 0 6750 0
[pid=32348] vsize: 27648
Current children cumulated CPU time (s) 898.96
Current children cumulated vsize (Kb) 29776

[startup+910.089 s]
Raw data (loadavg): 1.00 1.00 0.95 3/58 32368
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 8461 0 0 0 58507 87 0 0 25 0 1 0 1854737802 29069312 6714 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 7097 6714 162 162 0 6935 0
[pid=32348] vsize: 28388
Current children cumulated CPU time (s) 908.95
Current children cumulated vsize (Kb) 30516

[startup+920.091 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32368
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 8565 0 0 0 59504 89 0 0 25 0 1 0 1854737802 29470720 6818 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 7195 6818 162 162 0 7033 0
[pid=32348] vsize: 28780
Current children cumulated CPU time (s) 918.94
Current children cumulated vsize (Kb) 30908

[startup+930.092 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32368
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 8565 0 0 0 60502 90 0 0 25 0 1 0 1854737802 29470720 6818 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 7195 6818 162 162 0 7033 0
[pid=32348] vsize: 28780
Current children cumulated CPU time (s) 928.93
Current children cumulated vsize (Kb) 30908

[startup+940.092 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32368
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 8599 0 0 0 61500 91 0 0 25 0 1 0 1854737802 29470720 6818 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 7195 6818 162 162 0 7033 0
[pid=32348] vsize: 28780
Current children cumulated CPU time (s) 938.92
Current children cumulated vsize (Kb) 30908

[startup+950.093 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32368
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 8694 0 0 0 62496 93 0 0 25 0 1 0 1854737802 29863936 6913 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 7291 6913 162 162 0 7129 0
[pid=32348] vsize: 29164
Current children cumulated CPU time (s) 948.9
Current children cumulated vsize (Kb) 31292

[startup+960.094 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32370
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 10774 0 0 0 63483 101 0 0 25 0 1 0 1854737802 36892672 8585 4294967295 134512640 135167914 3221224448 3221222980 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 9007 8585 162 162 0 8845 0
[pid=32348] vsize: 36028
Current children cumulated CPU time (s) 958.85
Current children cumulated vsize (Kb) 38156

[startup+970.095 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32370
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 10938 0 0 0 64482 102 0 0 25 0 1 0 1854737802 38866944 8749 4294967295 134512640 135167914 3221224448 3221221856 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 9489 8749 162 162 0 9327 0
[pid=32348] vsize: 37956
Current children cumulated CPU time (s) 968.85
Current children cumulated vsize (Kb) 40084

[startup+980.096 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32370
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 12322 0 0 0 65475 107 0 0 25 0 1 0 1854737802 41750528 9588 4294967295 134512640 135167914 3221224448 3221220864 134723229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 10193 9588 162 162 0 10031 0
[pid=32348] vsize: 40772
Current children cumulated CPU time (s) 978.83
Current children cumulated vsize (Kb) 42900

[startup+990.096 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32370
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 12322 0 0 0 66475 107 0 0 25 0 1 0 1854737802 41750528 9588 4294967295 134512640 135167914 3221224448 3221223184 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 10193 9588 162 162 0 10031 0
[pid=32348] vsize: 40772
Current children cumulated CPU time (s) 988.83
Current children cumulated vsize (Kb) 42900

[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32370
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 12330 0 0 0 67476 107 0 0 25 0 1 0 1854737802 41791488 9596 4294967295 134512640 135167914 3221224448 3221223120 134617172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 10203 9596 162 162 0 10041 0
[pid=32348] vsize: 40812
Current children cumulated CPU time (s) 998.84
Current children cumulated vsize (Kb) 42940

[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32370
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 12724 0 0 0 68472 108 0 0 25 0 1 0 1854737802 42258432 9797 4294967295 134512640 135167914 3221224448 3221223152 134623290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 10317 9797 162 162 0 10155 0
[pid=32348] vsize: 41268
Current children cumulated CPU time (s) 1008.81
Current children cumulated vsize (Kb) 43396

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32372
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 12730 0 0 0 69472 108 0 0 25 0 1 0 1854737802 41820160 9698 4294967295 134512640 135167914 3221224448 3221222688 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 10210 9698 162 162 0 10048 0
[pid=32348] vsize: 40840
Current children cumulated CPU time (s) 1018.81
Current children cumulated vsize (Kb) 42968

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32372
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 13067 0 0 0 70470 109 0 0 25 0 1 0 1854737802 42655744 10035 4294967295 134512640 135167914 3221224448 3221221440 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 10414 10035 162 162 0 10252 0
[pid=32348] vsize: 41656
Current children cumulated CPU time (s) 1028.8
Current children cumulated vsize (Kb) 43784

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32372
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 13855 0 0 0 71465 112 0 0 25 0 1 0 1854737802 46424064 10313 4294967295 134512640 135167914 3221224448 3221223232 134694511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 11334 10313 162 162 0 11172 0
[pid=32348] vsize: 45336
Current children cumulated CPU time (s) 1038.78
Current children cumulated vsize (Kb) 47464

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32372
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 19902 0 0 0 72415 135 0 0 25 0 1 0 1854737802 68653056 15740 4294967295 134512640 135167914 3221224448 3220488176 134844775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 16761 15740 162 162 0 16599 0
[pid=32348] vsize: 67044
Current children cumulated CPU time (s) 1048.51
Current children cumulated vsize (Kb) 69172

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32372
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 24698 0 0 0 73373 154 0 0 25 0 1 0 1854737802 85598208 19877 4294967295 134512640 135167914 3221224448 3220639760 134619147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 20898 19877 162 162 0 20736 0
[pid=32348] vsize: 83592
Current children cumulated CPU time (s) 1058.28
Current children cumulated vsize (Kb) 85720

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32372
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 30561 0 0 0 74332 176 0 0 25 0 1 0 1854737802 104214528 24422 4294967295 134512640 135167914 3221224448 3218907520 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 25443 24422 162 162 0 25281 0
[pid=32348] vsize: 101772
Current children cumulated CPU time (s) 1068.09
Current children cumulated vsize (Kb) 103900

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32374
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 34347 0 0 0 75291 193 0 0 25 0 1 0 1854737802 119721984 28208 4294967295 134512640 135167914 3221224448 3220291424 134847173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 29229 28208 162 162 0 29067 0
[pid=32348] vsize: 116916
Current children cumulated CPU time (s) 1077.85
Current children cumulated vsize (Kb) 119044

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32374
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 42522 0 0 0 76244 221 0 0 25 0 1 0 1854737802 142405632 33746 4294967295 134512640 135167914 3221224448 3218487968 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32348/statm): 34767 33746 162 162 0 34605 0
[pid=32348] vsize: 139068
Current children cumulated CPU time (s) 1087.66
Current children cumulated vsize (Kb) 141196

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32374
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 46548 0 0 0 77198 242 0 0 25 0 1 0 1854737802 158896128 37772 4294967295 134512640 135167914 3221224448 3217694048 134844682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 38793 37772 162 162 0 38631 0
[pid=32348] vsize: 155172
Current children cumulated CPU time (s) 1097.41
Current children cumulated vsize (Kb) 157300

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32374
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 50488 0 0 0 78152 262 0 0 25 0 1 0 1854737802 175034368 41712 4294967295 134512640 135167914 3221224448 3217678368 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 42733 41712 162 162 0 42571 0
[pid=32348] vsize: 170932
Current children cumulated CPU time (s) 1107.15
Current children cumulated vsize (Kb) 173060

[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32374
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 54402 0 0 0 79106 285 0 0 25 0 1 0 1854737802 191066112 45626 4294967295 134512640 135167914 3221224448 3218437968 134843012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 46647 45626 162 162 0 46485 0
[pid=32348] vsize: 186588
Current children cumulated CPU time (s) 1116.92
Current children cumulated vsize (Kb) 188716

[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32374
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 68098 0 0 0 80045 323 0 0 25 0 1 0 1854737802 247164928 59322 4294967295 134512640 135167914 3221224448 3217678640 134694428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 60343 59322 162 162 0 60181 0
[pid=32348] vsize: 241372
Current children cumulated CPU time (s) 1126.69
Current children cumulated vsize (Kb) 243500

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32376
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 71424 0 0 0 81005 340 0 0 25 0 1 0 1854737802 239190016 57375 4294967295 134512640 135167914 3221224448 3217675772 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 58396 57375 162 162 0 58234 0
[pid=32348] vsize: 233584
Current children cumulated CPU time (s) 1136.46
Current children cumulated vsize (Kb) 235712

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32376
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 75488 0 0 0 81959 361 0 0 25 0 1 0 1854737802 255836160 61439 4294967295 134512640 135167914 3221224448 3218522256 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 62460 61439 162 162 0 62298 0
[pid=32348] vsize: 249840
Current children cumulated CPU time (s) 1146.21
Current children cumulated vsize (Kb) 251968

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32376
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 79732 0 0 0 82908 382 0 0 25 0 1 0 1854737802 273219584 65683 4294967295 134512640 135167914 3221224448 3217711104 134522502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 66704 65683 162 162 0 66542 0
[pid=32348] vsize: 266816
Current children cumulated CPU time (s) 1155.91
Current children cumulated vsize (Kb) 268944

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32376
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) T 32333 32333 9102 0 -1 0 83926 0 0 0 83859 404 0 0 25 0 1 0 1854737802 290398208 69877 4294967295 134512640 135167914 3221224448 3220423420 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32348/statm): 70898 69877 162 162 0 70736 0
[pid=32348] vsize: 283592
Current children cumulated CPU time (s) 1165.64
Current children cumulated vsize (Kb) 285720

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.95 1/58 32376
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) T 32333 32333 9102 0 -1 0 88116 0 0 0 84811 424 0 0 25 0 1 0 1854737802 307560448 74067 4294967295 134512640 135167914 3221224448 3217685916 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32348/statm): 75088 74067 162 162 0 74926 0
[pid=32348] vsize: 300352
Current children cumulated CPU time (s) 1175.36
Current children cumulated vsize (Kb) 302480

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32376
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 92272 0 0 0 85763 445 0 0 25 0 1 0 1854737802 324583424 78223 4294967295 134512640 135167914 3221224448 3217742656 134695191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 79244 78223 162 162 0 79082 0
[pid=32348] vsize: 316976
Current children cumulated CPU time (s) 1185.09
Current children cumulated vsize (Kb) 319104

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32378
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 96419 0 0 0 86716 464 0 0 25 0 1 0 1854737802 341569536 82370 4294967295 134512640 135167914 3221224448 3217716304 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 83391 82370 162 162 0 83229 0
[pid=32348] vsize: 333564
Current children cumulated CPU time (s) 1194.81
Current children cumulated vsize (Kb) 335692

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32378
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 120984 0 0 0 87632 530 0 0 25 0 1 0 1854737802 442187776 106935 4294967295 134512640 135167914 3221224448 3217679084 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 107956 106935 162 162 0 107794 0
[pid=32348] vsize: 431824
Current children cumulated CPU time (s) 1204.63
Current children cumulated vsize (Kb) 433952



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 32378
Raw data (/proc/32333/stat): 32333 (minisat+_script) S 32332 32333 9102 0 -1 0 314 3368 0 0 0 0 32259 42 19 0 1 0 1854705466 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32333/statm): 532 234 485 147 0 385 0
[pid=32333] vsize: 2128
Raw data (/proc/32348/stat): 32348 (minisat+_bignum) R 32333 32333 9102 0 -1 0 120984 0 0 0 87632 530 0 0 25 0 1 0 1854737802 442187776 106935 4294967295 134512640 135167914 3221224448 3217679084 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32348/statm): 107956 106935 162 162 0 107794 0
[pid=32348] vsize: 431824
Current children cumulated CPU time (s) 1204.63
Current children cumulated vsize (Kb) 433952

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

Child status: 0
Real time (s): 1210.32
CPU time (s): 881.832
CPU user time (s): 876.326
CPU system time (s): 5.50616
CPU usage (%): 72.8594
Max. virtual memory (cumulated for all children) (Kb): 433952

Verifier Data

ERROR: no interpretation found !