Some explanations

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

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-blp-ar98.opb
MD5SUM53176d06e1e99afe2d28ec1484235311
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 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 81920000000
Number of bits of the biggest number in a constraint 37
Biggest sum of numbers in a constraint 40410384871329
Number of bits of the biggest sum of numbers46
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables18824
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 constraint15827

Trace number 6301

Launcher Data

LAUNCH ON wulflinc19 THE 2005-09-20 05:29:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3480 boxname=wulflinc19 idbench=1136 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  53176d06e1e99afe2d28ec1484235311  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-blp-ar98.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-blp-ar98.opb
IDLAUNCH: 3480
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898756 kB
Buffers:         21880 kB
Cached:          85732 kB
SwapCached:        848 kB
Active:          31360 kB
Inactive:        78872 kB
HighTotal:      131008 kB
HighFree:        44128 kB
LowTotal:       903652 kB
LowFree:        854628 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5508 kB
Slab:            19996 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:40:11 (client local time) WITH STATUS 139 IN 646.088 SECONDS
stats: 3480 7 646.088 139

Solver Data

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:    9
c ---[1474]---> BDD-cost:    9
c ---[1473]---> BDD-cost:    9
c ---[1472]---> BDD-cost:   10
c ---[1470]---> BDD-cost:   10
c ---[1469]---> BDD-cost:    9
c ---[1468]---> BDD-cost:   10
c ---[1467]---> BDD-cost:    9
c ---[1466]---> BDD-cost:   10
c ---[1465]---> BDD-cost:   10
c ---[1464]---> BDD-cost:    9
c ---[1463]---> BDD-cost:   10
c ---[1462]---> BDD-cost:   10
c ---[1461]---> BDD-cost:    9
c ---[1460]---> BDD-cost:   10
c ---[1459]---> BDD-cost:   10
c ---[1458]---> BDD-cost:   10
c ---[1457]---> BDD-cost:   10
c ---[1456]---> BDD-cost:   10
c ---[1455]---> BDD-cost:    9
c ---[1454]---> BDD-cost:    8
c ---[1453]---> BDD-cost:    9
c ---[1452]---> BDD-cost:   10
c ---[1451]---> BDD-cost:   10
c ---[1450]---> BDD-cost:   10
c ---[1449]---> BDD-cost:   10
c ---[1448]---> BDD-cost:    9
c ---[1447]---> BDD-cost:   10
c ---[1446]---> BDD-cost:   10
c ---[1445]---> BDD-cost:   10
c ---[1444]---> BDD-cost:   10
c ---[1443]---> BDD-cost:   10
c ---[1442]---> BDD-cost:   10
c ---[1441]---> BDD-cost:   10
c ---[1440]---> BDD-cost:   10
c ---[1439]---> BDD-cost:   10
c ---[1438]---> BDD-cost:   10
c ---[1437]---> BDD-cost:   10
c ---[1436]---> BDD-cost:    9
c ---[1435]---> BDD-cost:   10
c ---[1434]---> BDD-cost:   10
c ---[1433]---> BDD-cost:   10
c ---[1432]---> BDD-cost:   10
c ---[1431]---> BDD-cost:   10
c ---[1430]---> BDD-cost:   10
c ---[1429]---> BDD-cost:   10
c ---[1428]---> BDD-cost:   10
c ---[1427]---> BDD-cost:    9
c ---[1426]---> BDD-cost:   10
c ---[1425]---> BDD-cost:   10
c ---[1424]---> BDD-cost:   10
c ---[1423]---> BDD-cost:    9
c ---[1422]---> BDD-cost:    9
c ---[1421]---> BDD-cost:   10
c ---[1420]---> BDD-cost:   10
c ---[1419]---> BDD-cost:   10
c ---[1418]---> BDD-cost:   10
c ---[1417]---> BDD-cost:   10
c ---[1416]---> BDD-cost:   10
c ---[1415]---> BDD-cost:   10
c ---[1414]---> BDD-cost:   10
c ---[1413]---> BDD-cost:   10
c ---[1412]---> BDD-cost:   10
c ---[1411]---> BDD-cost:   10
c ---[1410]---> BDD-cost:    9
c ---[1409]---> BDD-cost:   10
c ---[1408]---> BDD-cost:   10
c ---[1407]---> BDD-cost:   10
c ---[1406]---> BDD-cost:   10
c ---[1405]---> BDD-cost:   10
c ---[1404]---> BDD-cost:    9
c ---[1403]---> BDD-cost:    9
c ---[1402]---> BDD-cost:   10
c ---[1401]---> BDD-cost:   10
c ---[1400]---> BDD-cost:   10
c ---[1399]---> BDD-cost:    9
c ---[1398]---> BDD-cost:   10
c ---[1397]---> BDD-cost:   10
c ---[1396]---> BDD-cost:   10
c ---[1395]---> BDD-cost:   10
c ---[1394]---> BDD-cost:   10
c ---[1393]---> BDD-cost:    9
c ---[1392]---> BDD-cost:   10
c ---[1391]---> BDD-cost:   10
c ---[1390]---> BDD-cost:   10
c ---[1389]---> BDD-cost:   10
c ---[1388]---> BDD-cost:   10
c ---[1387]---> BDD-cost:   10
c ---[1386]---> BDD-cost:   10
c ---[1385]---> BDD-cost:   10
c ---[1384]---> BDD-cost:   10
c ---[1383]---> BDD-cost:   10
c ---[1381]---> BDD-cost:   10
c ---[1380]---> BDD-cost:   10
c ---[1379]---> BDD-cost:   10
c ---[1378]---> BDD-cost:   10
c ---[1377]---> BDD-cost:   10
c ---[1376]---> BDD-cost:    9
c ---[1375]---> BDD-cost:   10
c ---[1374]---> BDD-cost:   10
c ---[1373]---> BDD-cost:    9
c ---[1372]---> BDD-cost:    9
c ---[1371]---> BDD-cost:    9
c ---[1370]---> BDD-cost:   10
c ---[1369]---> BDD-cost:   10
c ---[1368]---> BDD-cost:   10
c ---[1367]---> BDD-cost:   10
c ---[1366]---> BDD-cost:   10
c ---[1365]---> BDD-cost:    9
c ---[1364]---> BDD-cost:    9
c ---[1362]---> BDD-cost:   10
c ---[1361]---> BDD-cost:   10
c ---[1360]---> BDD-cost:   10
c ---[1359]---> BDD-cost:   10
c ---[1358]---> BDD-cost:   10
c ---[1357]---> BDD-cost:   10
c ---[1356]---> BDD-cost:   10
c ---[1355]---> BDD-cost:   10
c ---[1354]---> BDD-cost:   10
c ---[1353]---> BDD-cost:    8
c ---[1352]---> BDD-cost:   10
c ---[1351]---> BDD-cost:   10
c ---[1350]---> BDD-cost:    9
c ---[1349]---> BDD-cost:   10
c ---[1348]---> BDD-cost:   10
c ---[1347]---> BDD-cost:   10
c ---[1346]---> BDD-cost:   10
c ---[1344]---> Adder-cost: 4370   maxlim: 588928   bits: 20/20
c ---[1342]---> Adder-cost: 3378   maxlim: 552576   bits: 20/20
c ---[1340]---> Adder-cost: 3212   maxlim: 414848   bits: 19/19
c ---[1338]---> Adder-cost: 3118   maxlim: 421760   bits: 19/19
c ---[1336]---> Adder-cost: 2686   maxlim: 365696   bits: 19/19
c ---[1334]---> Adder-cost: 1564   maxlim: 246144   bits: 18/18
c ---[1332]---> Adder-cost: 756   maxlim: 116224   bits: 17/17
c ---[1330]---> Adder-cost: 704   maxlim: 94592   bits: 17/17
c ---[1328]---> Adder-cost: 1236   maxlim: 194560   bits: 18/18
c ---[1326]---> Adder-cost: 2132   maxlim: 281600   bits: 19/19
c ---[1324]---> Adder-cost: 1340   maxlim: 198528   bits: 18/18
c ---[1322]---> Adder-cost: 3828   maxlim: 542848   bits: 20/20
c ---[1320]---> Adder-cost: 1388   maxlim: 204928   bits: 18/18
c ---[1318]---> Adder-cost: 782   maxlim: 99328   bits: 17/17
c ---[1316]---> Adder-cost: 562   maxlim: 94848   bits: 17/17
c ---[1314]---> Adder-cost: 330   maxlim: 51840   bits: 16/16
c ---[1312]---> Adder-cost: 176   maxlim: 26624   bits: 15/15
c ---[1310]---> Adder-cost: 232   maxlim: 28544   bits: 15/15
c ---[1308]---> Adder-cost: 522   maxlim: 70400   bits: 17/17
c ---[1306]---> Adder-cost: 924   maxlim: 136064   bits: 18/18
c ---[1304]---> Adder-cost: 4884   maxlim: 977152   bits: 20/20
c ---[1302]---> Adder-cost: 3826   maxlim: 763392   bits: 20/20
c ---[1300]---> Adder-cost: 776   maxlim: 552576   bits: 20/20
c ---[1298]---> Adder-cost: 2220   maxlim: 424576   bits: 19/19
c ---[1296]---> Adder-cost: 452   maxlim: 56576   bits: 16/16
c ---[1294]---> Adder-cost: 524   maxlim: 66560   bits: 17/17
c ---[1292]---> Adder-cost: 1474   maxlim: 306560   bits: 19/19
c ---[1290]---> Adder-cost: 1944   maxlim: 456832   bits: 19/19
c ---[1288]---> Adder-cost: 362   maxlim: 46208   bits: 16/16
c ---[1286]---> Sorter-cost: 1180     Base: 2 2 2 2 2 2 2 2
c ---[1284]---> Adder-cost: 1814   maxlim: 332544   bits: 19/19
c ---[1282]---> Adder-cost: 1258   maxlim: 256384   bits: 18/18
c ---[1280]---> Adder-cost: 498   maxlim: 67712   bits: 17/17
c ---[1278]---> Adder-cost: 712   maxlim: 107136   bits: 17/17
c ---[1276]---> Adder-cost: 810   maxlim: 148352   bits: 18/18
c ---[1274]---> Adder-cost: 250   maxlim: 33920   bits: 16/16
c ---[1272]---> Adder-cost: 210   maxlim: 33920   bits: 16/16
c ---[1270]---> Adder-cost: 342   maxlim: 61696   bits: 16/16
c ---[1268]---> Adder-cost: 476   maxlim: 69888   bits: 17/17
c ---[1266]---> Adder-cost: 1820   maxlim: 249728   bits: 18/18
c ---[1264]---> Adder-cost: 2086   maxlim: 316800   bits: 19/19
c ---[1262]---> Sorter-cost:  151     Base: 2 2 2 2 2 2 2 2 2
c ---[1260]---> Adder-cost: 224   maxlim: 39808   bits: 16/16
c ---[1258]---> Adder-cost: 258   maxlim: 54144   bits: 16/16
c ---[1256]---> Adder-cost: 896   maxlim: 146944   bits: 18/18
c ---[1254]---> Adder-cost: 1424   maxlim: 190464   bits: 18/18
c ---[1252]---> Adder-cost: 3020   maxlim: 432768   bits: 19/19
c ---[1250]---> Adder-cost: 1796   maxlim: 274816   bits: 19/19
c ---[1248]---> Adder-cost: 4044   maxlim: 679552   bits: 20/20
c ---[1246]---> Adder-cost: 192   maxlim: 33664   bits: 16/16
c ---[1244]---> Adder-cost: 228   maxlim: 36224   bits: 16/16
c ---[1242]---> Adder-cost: 334   maxlim: 62080   bits: 16/16
c ---[1240]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2
c ---[1238]---> Adder-cost: 656   maxlim: 103168   bits: 17/17
c ---[1236]---> Adder-cost: 270   maxlim: 103168   bits: 17/17
c ---[1234]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2
c ---[1232]---> Adder-cost: 1774   maxlim: 300032   bits: 19/19
c ---[1230]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 2 2
c ---[1228]---> Adder-cost: 380   maxlim: 67328   bits: 17/17
c ---[1226]---> Adder-cost: 142   maxlim: 23552   bits: 15/15
c ---[1224]---> Adder-cost: 464   maxlim: 98304   bits: 17/17
c ---[1222]---> Adder-cost: 152   maxlim: 18560   bits: 15/15
c ---[1220]---> Adder-cost: 466   maxlim: 66432   bits: 17/17
c ---[1218]---> Adder-cost: 2418   maxlim: 406656   bits: 19/19
c ---[1216]---> Adder-cost: 1274   maxlim: 209664   bits: 18/18
c ---[1214]---> Adder-cost: 4864   maxlim: 765824   bits: 20/20
c ---[1212]---> Adder-cost: 1392   maxlim: 237440   bits: 18/18
c ---[1210]---> Adder-cost: 3074   maxlim: 509568   bits: 19/19
c ---[1208]---> Adder-cost: 4114   maxlim: 797056   bits: 20/20
c ---[1206]---> Adder-cost: 1758   maxlim: 272896   bits: 19/19
c ---[1204]---> Adder-cost: 2902   maxlim: 481408   bits: 19/19
c ---[1202]---> Adder-cost: 1576   maxlim: 276096   bits: 19/19
c ---[1200]---> Adder-cost: 3600   maxlim: 676736   bits: 20/20
c ---[1198]---> Adder-cost: 232   maxlim: 33920   bits: 16/16
c ---[1196]---> Adder-cost: 156   maxlim: 21760   bits: 15/15
c ---[1194]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2
c ---[1192]---> Adder-cost: 1542   maxlim: 256768   bits: 18/18
c ---[1190]---> Adder-cost: 1494   maxlim: 255744   bits: 18/18
c ---[1188]---> Adder-cost: 758   maxlim: 128256   bits: 17/17
c ---[1186]---> Adder-cost: 1014   maxlim: 150528   bits: 18/18
c ---[1184]---> Adder-cost: 1460   maxlim: 267392   bits: 19/19
c ---[1182]---> Adder-cost: 542   maxlim: 750   bits: 10/10
c ---[1180]---> Adder-cost: 860   maxlim: 165888   bits: 18/18
c ---[1178]---> Adder-cost: 600   maxlim: 119040   bits: 17/17
c ---[1176]---> Sorter-cost: 1393     Base: 2 2 2 2 2 2 2 2 2
c ---[1174]---> Adder-cost: 656   maxlim: 110464   bits: 17/17
c ---[1172]---> Adder-cost: 562   maxlim: 89472   bits: 17/17
c ---[1170]---> Adder-cost: 272   maxlim: 46464   bits: 16/16
c ---[1168]---> Adder-cost: 1440   maxlim: 249216   bits: 18/18
c ---[1166]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost: 1051     Base: 2 2 2 2 2 2 2 2 2
c ---[1162]---> Adder-cost: 246   maxlim: 54272   bits: 16/16
c ---[1160]---> Adder-cost: 608   maxlim: 144768   bits: 18/18
c ---[1158]---> Adder-cost: 1120   maxlim: 302464   bits: 19/19
c ---[1156]---> Adder-cost: 360   maxlim: 45696   bits: 16/16
c ---[1154]---> Adder-cost: 490   maxlim: 64128   bits: 17/16
c ---[1152]---> Sorter-cost:  367     Base: 2 2 2 2 2 2 2 2 2
c ---[1150]---> Adder-cost: 134   maxlim: 19456   bits: 15/15
c ---[1148]---> Sorter-cost: 1434     Base: 2 2 2 2 2 2 2 2 2
c ---[1146]---> Adder-cost: 832   maxlim: 120448   bits: 17/17
c ---[1144]---> Adder-cost: 1850   maxlim: 375424   bits: 19/19
c ---[1142]---> Adder-cost: 1194   maxlim: 333184   bits: 19/19
c ---[1140]---> Adder-cost: 206   maxlim: 30336   bits: 15/15
c ---[1138]---> Adder-cost: 254   maxlim: 491   bits: 9/9
c ---[1136]---> Adder-cost: 758   maxlim: 183424   bits: 18/18
c ---[1134]---> Adder-cost: 120   maxlim: 22272   bits: 15/15
c ---[1132]---> Adder-cost: 192   maxlim: 40576   bits: 16/16
c ---[1130]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2
c ---[1128]---> Adder-cost: 1596   maxlim: 337920   bits: 19/19
c ---[1126]---> Adder-cost: 856   maxlim: 139008   bits: 18/18
c ---[1124]---> Adder-cost: 294   maxlim: 41984   bits: 16/16
c ---[1122]---> Adder-cost: 332   maxlim: 52736   bits: 16/16
c ---[1120]---> Adder-cost: 1674   maxlim: 326912   bits: 19/19
c ---[1118]---> Adder-cost: 1610   maxlim: 312320   bits: 19/19
c ---[1116]---> Sorter-cost:  945     Base: 2 2 2 2 2 2 2 2 2
c ---[1114]---> Adder-cost: 172   maxlim: 22784   bits: 15/15
c ---[1112]---> Adder-cost: 130   maxlim: 15488   bits: 15/14
c ---[1110]---> Adder-cost: 1116   maxlim: 202368   bits: 18/18
c ---[1108]---> Adder-cost: 908   maxlim: 164736   bits: 18/18
c ---[1106]---> Sorter-cost:  201     Base: 2 2 2 2 2 2 2 2 2
c ---[1104]---> Adder-cost: 444   maxlim: 68096   bits: 17/17
c ---[1102]---> BDD-cost:   53
c ---[1100]---> Adder-cost: 292   maxlim: 44544   bits: 16/16
c ---[1098]---> Adder-cost: 260   maxlim: 45952   bits: 16/16
c ---[1096]---> Adder-cost: 2140   maxlim: 3369   bits: 12/12
c ---[1094]---> Adder-cost: 1600   maxlim: 385792   bits: 19/19
c ---[1092]---> Sorter-cost:  195     Base: 2 2 2 2 2 2 2 2 /oldhome/oroussel/solvers/minisat+_script: line 9:  1136 Segmentation fault      $XDIR/minisat+_64-bit_static -try "$@"

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/1132/stat): 1132 (minisat+_script) R 1131 1132 5929 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856007290 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/1132/statm): 174 3 169 147 0 27 0
[pid=1132] 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=1133
New process pid=1134
New process pid=1135
execve syscall for /bin/sed executable
One traced child (pid=1134) 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=1135) exited with status: 0
One traced child (pid=1133) exited with status: 0
New process pid=1136
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-blp-ar98.opb

[startup+10.004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 342 0 0 0 986 4 0 0 25 0 1 0 1856007295 1806336 328 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 441 328 145 145 0 296 0
[pid=1136] vsize: 1764
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 3888

[startup+20.0048 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 477 0 0 0 1984 5 0 0 25 0 1 0 1856007295 2682880 460 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 655 460 145 145 0 510 0
[pid=1136] vsize: 2620
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 4744

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 553 0 0 0 2983 6 0 0 25 0 1 0 1856007295 2854912 536 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 697 536 145 145 0 552 0
[pid=1136] vsize: 2788
Current children cumulated CPU time (s) 29.9
Current children cumulated vsize (Kb) 4912

[startup+40.0065 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 583 0 0 0 3982 7 0 0 25 0 1 0 1856007295 2879488 566 4294967295 134512640 135094434 3221224432 3221223300 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 703 566 145 145 0 558 0
[pid=1136] vsize: 2812
Current children cumulated CPU time (s) 39.9
Current children cumulated vsize (Kb) 4936

[startup+50.0073 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 628 0 0 0 4981 7 0 0 25 0 1 0 1856007295 3014656 611 4294967295 134512640 135094434 3221224432 3221223328 134587994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 736 611 145 145 0 591 0
[pid=1136] vsize: 2944
Current children cumulated CPU time (s) 49.89
Current children cumulated vsize (Kb) 5068

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 660 0 0 0 5979 8 0 0 25 0 1 0 1856007295 3088384 643 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 754 643 145 145 0 609 0
[pid=1136] vsize: 3016
Current children cumulated CPU time (s) 59.88
Current children cumulated vsize (Kb) 5140

[startup+70.0079 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 848 0 0 0 6977 10 0 0 25 0 1 0 1856007295 4726784 824 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1154 824 145 145 0 1009 0
[pid=1136] vsize: 4616
Current children cumulated CPU time (s) 69.88
Current children cumulated vsize (Kb) 6740

[startup+80.0087 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) T 1132 1132 5929 0 -1 0 881 0 0 0 7975 11 0 0 25 0 1 0 1856007295 4812800 857 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1175 857 145 145 0 1030 0
[pid=1136] vsize: 4700
Current children cumulated CPU time (s) 79.87
Current children cumulated vsize (Kb) 6824

[startup+90.0095 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 964 0 0 0 8973 12 0 0 25 0 1 0 1856007295 5083136 889 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1241 889 145 145 0 1096 0
[pid=1136] vsize: 4964
Current children cumulated CPU time (s) 89.86
Current children cumulated vsize (Kb) 7088

[startup+100.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1069 0 0 0 9971 13 0 0 25 0 1 0 1856007295 5574656 994 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1361 994 145 145 0 1216 0
[pid=1136] vsize: 5444
Current children cumulated CPU time (s) 99.85
Current children cumulated vsize (Kb) 7568

[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1113 0 0 0 10969 15 0 0 25 0 1 0 1856007295 5758976 1038 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1406 1038 145 145 0 1261 0
[pid=1136] vsize: 5624
Current children cumulated CPU time (s) 109.85
Current children cumulated vsize (Kb) 7748

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1207 0 0 0 11967 16 0 0 25 0 1 0 1856007295 6119424 1080 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1494 1080 145 145 0 1349 0
[pid=1136] vsize: 5976
Current children cumulated CPU time (s) 119.84
Current children cumulated vsize (Kb) 8100

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1235 0 0 0 12966 17 0 0 25 0 1 0 1856007295 6234112 1108 4294967295 134512640 135094434 3221224432 3221223344 134587875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1522 1108 145 145 0 1377 0
[pid=1136] vsize: 6088
Current children cumulated CPU time (s) 129.84
Current children cumulated vsize (Kb) 8212

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1364 0 0 0 13964 18 0 0 25 0 1 0 1856007295 6688768 1155 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1633 1155 145 145 0 1488 0
[pid=1136] vsize: 6532
Current children cumulated CPU time (s) 139.83
Current children cumulated vsize (Kb) 8656

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1452 0 0 0 14962 19 0 0 25 0 1 0 1856007295 6959104 1173 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1699 1173 145 145 0 1554 0
[pid=1136] vsize: 6796
Current children cumulated CPU time (s) 149.82
Current children cumulated vsize (Kb) 8920

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1535 0 0 0 15960 20 0 0 25 0 1 0 1856007295 7262208 1206 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1773 1206 145 145 0 1628 0
[pid=1136] vsize: 7092
Current children cumulated CPU time (s) 159.81
Current children cumulated vsize (Kb) 9216

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1601 0 0 0 16959 21 0 0 25 0 1 0 1856007295 7557120 1272 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1845 1272 145 145 0 1700 0
[pid=1136] vsize: 7380
Current children cumulated CPU time (s) 169.81
Current children cumulated vsize (Kb) 9504

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1670 0 0 0 17956 23 0 0 25 0 1 0 1856007295 7888896 1341 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 1926 1341 145 145 0 1781 0
[pid=1136] vsize: 7704
Current children cumulated CPU time (s) 179.8
Current children cumulated vsize (Kb) 9828

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1774 0 0 0 18955 24 0 0 25 0 1 0 1856007295 8355840 1445 4294967295 134512640 135094434 3221224432 3221223344 134587864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 2040 1445 145 145 0 1895 0
[pid=1136] vsize: 8160
Current children cumulated CPU time (s) 189.8
Current children cumulated vsize (Kb) 10284

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1841 0 0 0 19953 25 0 0 25 0 1 0 1856007295 8646656 1512 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2111 1512 145 145 0 1966 0
[pid=1136] vsize: 8444
Current children cumulated CPU time (s) 199.79
Current children cumulated vsize (Kb) 10568

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 1971 0 0 0 20951 26 0 0 25 0 1 0 1856007295 9166848 1591 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2238 1591 145 145 0 2093 0
[pid=1136] vsize: 8952
Current children cumulated CPU time (s) 209.78
Current children cumulated vsize (Kb) 11076

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2043 0 0 0 21948 28 0 0 25 0 1 0 1856007295 9474048 1663 4294967295 134512640 135094434 3221224432 3221223344 134587864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2313 1663 145 145 0 2168 0
[pid=1136] vsize: 9252
Current children cumulated CPU time (s) 219.77
Current children cumulated vsize (Kb) 11376

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2205 0 0 0 22945 30 0 0 25 0 1 0 1856007295 10055680 1753 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2455 1753 145 145 0 2310 0
[pid=1136] vsize: 9820
Current children cumulated CPU time (s) 229.76
Current children cumulated vsize (Kb) 11944

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2361 0 0 0 23943 32 0 0 25 0 1 0 1856007295 10637312 1837 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2597 1837 145 145 0 2452 0
[pid=1136] vsize: 10388
Current children cumulated CPU time (s) 239.76
Current children cumulated vsize (Kb) 12512

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2489 0 0 0 24940 33 0 0 25 0 1 0 1856007295 11157504 1916 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2724 1916 145 145 0 2579 0
[pid=1136] vsize: 10896
Current children cumulated CPU time (s) 249.74
Current children cumulated vsize (Kb) 13020

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2595 0 0 0 25937 35 0 0 25 0 1 0 1856007295 11751424 2022 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2869 2022 145 145 0 2724 0
[pid=1136] vsize: 11476
Current children cumulated CPU time (s) 259.73
Current children cumulated vsize (Kb) 13600

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2657 0 0 0 26935 37 0 0 25 0 1 0 1856007295 12034048 2084 4294967295 134512640 135094434 3221224432 3221223344 134587864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 2938 2084 145 145 0 2793 0
[pid=1136] vsize: 11752
Current children cumulated CPU time (s) 269.73
Current children cumulated vsize (Kb) 13876

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2746 0 0 0 27934 37 0 0 25 0 1 0 1856007295 12398592 2173 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3027 2173 145 145 0 2882 0
[pid=1136] vsize: 12108
Current children cumulated CPU time (s) 279.72
Current children cumulated vsize (Kb) 14232

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2860 0 0 0 28932 39 0 0 25 0 1 0 1856007295 12922880 2287 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3155 2287 145 145 0 3010 0
[pid=1136] vsize: 12620
Current children cumulated CPU time (s) 289.72
Current children cumulated vsize (Kb) 14744

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 2985 0 0 0 29930 40 0 0 25 0 1 0 1856007295 13455360 2412 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3285 2412 145 145 0 3140 0
[pid=1136] vsize: 13140
Current children cumulated CPU time (s) 299.71
Current children cumulated vsize (Kb) 15264

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 3059 0 0 0 30928 40 0 0 25 0 1 0 1856007295 13737984 2438 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3354 2438 145 145 0 3209 0
[pid=1136] vsize: 13416
Current children cumulated CPU time (s) 309.69
Current children cumulated vsize (Kb) 15540

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 3149 0 0 0 31926 41 0 0 25 0 1 0 1856007295 14000128 2463 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3418 2463 145 145 0 3273 0
[pid=1136] vsize: 13672
Current children cumulated CPU time (s) 319.68
Current children cumulated vsize (Kb) 15796

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 3167 0 0 0 32924 43 0 0 25 0 1 0 1856007295 14098432 2481 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3442 2481 145 145 0 3297 0
[pid=1136] vsize: 13768
Current children cumulated CPU time (s) 329.68
Current children cumulated vsize (Kb) 15892

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 3173 0 0 0 33922 44 0 0 25 0 1 0 1856007295 14098432 2487 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3442 2487 145 145 0 3297 0
[pid=1136] vsize: 13768
Current children cumulated CPU time (s) 339.67
Current children cumulated vsize (Kb) 15892

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 3204 0 0 0 34921 44 0 0 25 0 1 0 1856007295 14295040 2518 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3490 2518 145 145 0 3345 0
[pid=1136] vsize: 13960
Current children cumulated CPU time (s) 349.66
Current children cumulated vsize (Kb) 16084

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 3871 0 0 0 35915 48 0 0 25 0 1 0 1856007295 16019456 2655 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3911 2655 145 145 0 3766 0
[pid=1136] vsize: 15644
Current children cumulated CPU time (s) 359.64
Current children cumulated vsize (Kb) 17768

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) T 1132 1132 5929 0 -1 0 3928 0 0 0 36913 49 0 0 25 0 1 0 1856007295 16375808 2712 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/1136/statm): 3998 2712 145 145 0 3853 0
[pid=1136] vsize: 15992
Current children cumulated CPU time (s) 369.63
Current children cumulated vsize (Kb) 18116

[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 3973 0 0 0 37912 50 0 0 25 0 1 0 1856007295 16609280 2757 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4055 2757 145 145 0 3910 0
[pid=1136] vsize: 16220
Current children cumulated CPU time (s) 379.63
Current children cumulated vsize (Kb) 18344

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4056 0 0 0 38911 50 0 0 25 0 1 0 1856007295 16920576 2792 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4131 2792 145 145 0 3986 0
[pid=1136] vsize: 16524
Current children cumulated CPU time (s) 389.62
Current children cumulated vsize (Kb) 18648

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4072 0 0 0 39909 51 0 0 25 0 1 0 1856007295 17002496 2808 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4151 2808 145 145 0 4006 0
[pid=1136] vsize: 16604
Current children cumulated CPU time (s) 399.61
Current children cumulated vsize (Kb) 18728

[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4198 0 0 0 40907 52 0 0 25 0 1 0 1856007295 17453056 2854 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4261 2854 145 145 0 4116 0
[pid=1136] vsize: 17044
Current children cumulated CPU time (s) 409.6
Current children cumulated vsize (Kb) 19168

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4286 0 0 0 41906 52 0 0 25 0 1 0 1856007295 17723392 2872 4294967295 134512640 135094434 3221224432 3221223320 134795993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4327 2872 145 145 0 4182 0
[pid=1136] vsize: 17308
Current children cumulated CPU time (s) 419.59
Current children cumulated vsize (Kb) 19432

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4370 0 0 0 42905 53 0 0 25 0 1 0 1856007295 18038784 2908 4294967295 134512640 135094434 3221224432 3221223344 134587905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4404 2908 145 145 0 4259 0
[pid=1136] vsize: 17616
Current children cumulated CPU time (s) 429.59
Current children cumulated vsize (Kb) 19740

[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4436 0 0 0 43904 54 0 0 25 0 1 0 1856007295 18362368 2974 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4483 2974 145 145 0 4338 0
[pid=1136] vsize: 17932
Current children cumulated CPU time (s) 439.59
Current children cumulated vsize (Kb) 20056

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4502 0 0 0 44902 55 0 0 25 0 1 0 1856007295 18685952 3040 4294967295 134512640 135094434 3221224432 3221223320 134795993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4562 3040 145 145 0 4417 0
[pid=1136] vsize: 18248
Current children cumulated CPU time (s) 449.58
Current children cumulated vsize (Kb) 20372

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4620 0 0 0 45899 56 0 0 25 0 1 0 1856007295 19189760 3158 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4685 3158 145 145 0 4540 0
[pid=1136] vsize: 18740
Current children cumulated CPU time (s) 459.56
Current children cumulated vsize (Kb) 20864

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4712 0 0 0 46898 56 0 0 25 0 1 0 1856007295 19546112 3198 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4772 3198 145 145 0 4627 0
[pid=1136] vsize: 19088
Current children cumulated CPU time (s) 469.55
Current children cumulated vsize (Kb) 21212

[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4810 0 0 0 47896 58 0 0 25 0 1 0 1856007295 19943424 3296 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 4869 3296 145 145 0 4724 0
[pid=1136] vsize: 19476
Current children cumulated CPU time (s) 479.55
Current children cumulated vsize (Kb) 21600

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 4977 0 0 0 48894 58 0 0 25 0 1 0 1856007295 20512768 3339 4294967295 134512640 135094434 3221224432 3221223320 134795993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5008 3339 145 145 0 4863 0
[pid=1136] vsize: 20032
Current children cumulated CPU time (s) 489.53
Current children cumulated vsize (Kb) 22156

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5074 0 0 0 49891 60 0 0 25 0 1 0 1856007295 20926464 3436 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5109 3436 145 145 0 4964 0
[pid=1136] vsize: 20436
Current children cumulated CPU time (s) 499.52
Current children cumulated vsize (Kb) 22560

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5168 0 0 0 50890 61 0 0 25 0 1 0 1856007295 21311488 3530 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5203 3530 145 145 0 5058 0
[pid=1136] vsize: 20812
Current children cumulated CPU time (s) 509.52
Current children cumulated vsize (Kb) 22936

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5245 0 0 0 51888 62 0 0 25 0 1 0 1856007295 21643264 3607 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5284 3607 145 145 0 5139 0
[pid=1136] vsize: 21136
Current children cumulated CPU time (s) 519.51
Current children cumulated vsize (Kb) 23260

[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5362 0 0 0 52886 63 0 0 25 0 1 0 1856007295 22134784 3724 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5404 3724 145 145 0 5259 0
[pid=1136] vsize: 21616
Current children cumulated CPU time (s) 529.5
Current children cumulated vsize (Kb) 23740

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5430 0 0 0 53883 65 0 0 25 0 1 0 1856007295 22437888 3792 4294967295 134512640 135094434 3221224432 3221222960 134588344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 5478 3792 145 145 0 5333 0
[pid=1136] vsize: 21912
Current children cumulated CPU time (s) 539.49
Current children cumulated vsize (Kb) 24036

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5580 0 0 0 54880 66 0 0 25 0 1 0 1856007295 22904832 3830 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5592 3830 145 145 0 5447 0
[pid=1136] vsize: 22368
Current children cumulated CPU time (s) 549.47
Current children cumulated vsize (Kb) 24492

[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5614 0 0 0 55879 67 0 0 25 0 1 0 1856007295 23023616 3864 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5621 3864 145 145 0 5476 0
[pid=1136] vsize: 22484
Current children cumulated CPU time (s) 559.47
Current children cumulated vsize (Kb) 24608

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5657 0 0 0 56878 68 0 0 25 0 1 0 1856007295 23224320 3907 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5670 3907 145 145 0 5525 0
[pid=1136] vsize: 22680
Current children cumulated CPU time (s) 569.47
Current children cumulated vsize (Kb) 24804

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 5735 0 0 0 57875 69 0 0 25 0 1 0 1856007295 23543808 3985 4294967295 134512640 135094434 3221224432 3221223332 134587879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 5748 3985 145 145 0 5603 0
[pid=1136] vsize: 22992
Current children cumulated CPU time (s) 579.45
Current children cumulated vsize (Kb) 25116

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 8802 0 0 0 58856 81 0 0 25 0 1 0 1856007295 34074624 6321 4294967295 134512640 135094434 3221224432 3221220816 134519312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 8319 6321 145 145 0 8174 0
[pid=1136] vsize: 33276
Current children cumulated CPU time (s) 589.38
Current children cumulated vsize (Kb) 35400

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 11262 0 0 0 59843 89 0 0 25 0 1 0 1856007295 44941312 8400 4294967295 134512640 135094434 3221224432 3219347920 134597368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1136/statm): 10972 8400 145 145 0 10827 0
[pid=1136] vsize: 43888
Current children cumulated CPU time (s) 599.33
Current children cumulated vsize (Kb) 46012

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) T 1132 1132 5929 0 -1 0 50017 0 0 0 60594 228 0 0 21 0 1 0 1856007295 160587776 36773 4294967295 134512640 135094434 3221224432 3218517036 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1136/statm): 39206 36773 145 145 0 39061 0
[pid=1136] vsize: 156824
Current children cumulated CPU time (s) 608.23
Current children cumulated vsize (Kb) 158948

[startup+620.055 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) T 1132 1132 5929 0 -1 0 89846 0 0 0 61336 370 0 0 18 0 1 0 1856007295 280526848 66056 4294967295 134512640 135094434 3221224432 3218451916 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/1136/statm): 68488 66056 145 145 0 68343 0
[pid=1136] vsize: 273952
Current children cumulated CPU time (s) 617.07
Current children cumulated vsize (Kb) 276076

[startup+630.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 148163 0 0 0 62068 541 0 0 25 0 1 0 1856007295 519393280 124373 4294967295 134512640 135094434 3221224432 3218438880 134597447 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 126805 124373 145 145 0 126660 0
[pid=1136] vsize: 507220
Current children cumulated CPU time (s) 626.1
Current children cumulated vsize (Kb) 509344

[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) R 1132 1132 5929 0 -1 0 169857 0 0 0 62828 647 0 0 21 0 1 0 1856007295 521863168 124976 4294967295 134512640 135094434 3221224432 3218446460 134870330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1136/statm): 127408 124976 145 145 0 127263 0
[pid=1136] vsize: 509632
Current children cumulated CPU time (s) 634.76
Current children cumulated vsize (Kb) 511756

[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 1136
Raw data (/proc/1132/stat): 1132 (minisat+_script) S 1131 1132 5929 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856007290 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1132/statm): 531 226 485 147 0 384 0
[pid=1132] vsize: 2124
Raw data (/proc/1136/stat): 1136 (minisat+_64-bit) T 1132 1132 5929 0 -1 0 194559 0 0 0 63562 765 0 0 18 0 1 0 1856007295 623042560 149678 4294967295 134512640 135094434 3221224432 3218446988 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/1136/statm): 152110 149678 145 145 0 151965 0
[pid=1136] vsize: 608440
Current children cumulated CPU time (s) 643.28
Current children cumulated vsize (Kb) 610564
One traced child (pid=1136) ended because it received signal 11 (SIGSEGV)
One traced child (pid=1132) exited with status: 139
All traced children have exited ! Game is over.

Child status: 139
Real time (s): 653.289
CPU time (s): 646.088
CPU user time (s): 637.783
CPU system time (s): 8.30474
CPU usage (%): 98.8976
Max. virtual memory (cumulated for all children) (Kb): 610564

Verifier Data

ERROR: no interpretation found !