Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mkc.opb |
MD5SUM | b9e9aa470fdb3341d7e10860fcc70cec |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2946 |
Biggest coefficient in the objective function | 20000 |
Number of bits for the biggest coefficient in the objective function | 15 |
Sum of the numbers in the objective function | 31442101 |
Number of bits of the sum of numbers in the objective function | 25 |
Biggest number in a constraint | 65536000 |
Number of bits of the biggest number in a constraint | 26 |
Biggest sum of numbers in a constraint | 629010691 |
Number of bits of the biggest sum of numbers | 30 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.24 |
Number of variables | 5363 |
Total number of constraints | 8734 |
Number of constraints which are clauses | 2977 |
Number of constraints which are cardinality constraints (but not clauses) | 5731 |
Number of constraints which are nor clauses,nor cardinality constraints | 26 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2942 |
LAUNCH ON wulflinc9 THE 2005-09-20 04:30:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3374 boxname=wulflinc9 idbench=1030 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b9e9aa470fdb3341d7e10860fcc70cec /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-mkc.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-mkc.opb IDLAUNCH: 3374 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 869792 kB Buffers: 37044 kB Cached: 98592 kB SwapCached: 1044 kB Active: 66800 kB Inactive: 71556 kB HighTotal: 131008 kB HighFree: 36848 kB LowTotal: 903652 kB LowFree: 832944 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5672 kB Slab: 20916 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:50:30 (client local time) WITH STATUS 0 IN 1208.86 SECONDS stats: 3374 7 1208.86 0
c Parsing PB file... c Converting 3225 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ## c -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c ---[3223]---> Adder-cost: 26498 maxlim: 479706816 bits: 29/29 c ---[3222]---> BDD-cost: 2265 c ---[3221]---> BDD-cost: 25 c ---[3210]---> BDD-cost: 23 c ---[3199]---> BDD-cost: 9 c ---[3188]---> BDD-cost: 21 c ---[3177]---> BDD-cost: 27 c ---[3138]---> BDD-cost: 461 c ---[3135]---> BDD-cost: 5 c ---[3114]---> Adder-cost: 1804 maxlim: 2264275 bits: 22/22 c ---[3113]---> BDD-cost: 29 c ---[3102]---> BDD-cost: 19 c ---[3091]---> BDD-cost: 7 c ---[3080]---> BDD-cost: 5 c ---[3069]---> BDD-cost: 5 c ---[3058]---> BDD-cost: 5 c ---[3037]---> BDD-cost: 29 c ---[3026]---> BDD-cost: 27 c ---[3015]---> BDD-cost: 27 c ---[3004]---> BDD-cost: 3790 c ---[3003]---> BDD-cost: 5 c ---[2992]---> BDD-cost: 5 c ---[2981]---> BDD-cost: 29 c ---[2970]---> BDD-cost: 27 c ---[2959]---> BDD-cost: 11 c ---[2948]---> BDD-cost: 9 c ---[2930]---> BDD-cost: 485 c ---[2927]---> BDD-cost: 19 c ---[2916]---> BDD-cost: 19 c ---[2905]---> BDD-cost: 27 c ---[2894]---> BDD-cost: 1005 c ---[2893]---> BDD-cost: 19 c ---[2872]---> BDD-cost: 21 c ---[2839]---> BDD-cost: 19 c ---[2828]---> BDD-cost: 19 c ---[2796]---> BDD-cost: 21 c ---[2785]---> Sorter-cost:17311 Base: 5 2 5 2 3 2 2 2 2 2 c ---[2784]---> BDD-cost: 3 c ---[2773]---> BDD-cost: 29 c ---[2752]---> BDD-cost: 29 c ---[2741]---> BDD-cost: 27 c ---[2730]---> BDD-cost: 29 c ---[2711]---> BDD-cost: 461 c ---[2699]---> BDD-cost: 3 c ---[2688]---> BDD-cost: 13 c ---[2677]---> Adder-cost: 1438 maxlim: 1767687 bits: 21/21 c ---[2665]---> BDD-cost: 3 c ---[2654]---> BDD-cost: 3 c ---[2632]---> BDD-cost: 3 c ---[2621]---> BDD-cost: 3 c ---[2610]---> BDD-cost: 21 c ---[2589]---> BDD-cost: 23 c ---[2568]---> Adder-cost: 1090 maxlim: 131883 bits: 18/18 c ---[2567]---> BDD-cost: 3 c ---[2524]---> BDD-cost: 3 c ---[2505]---> BDD-cost: 461 c ---[2503]---> BDD-cost: 23 c ---[2472]---> BDD-cost: 29 c ---[2461]---> Sorter-cost:10972 Base: 2 5 5 3 11 3 2 c ---[2460]---> BDD-cost: 29 c ---[2438]---> BDD-cost: 3 c ---[2367]---> BDD-cost: 27 c ---[2356]---> BDD-cost: 1027 c ---[2355]---> BDD-cost: 29 c ---[2324]---> BDD-cost: 3 c ---[2305]---> BDD-cost: 461 c ---[2283]---> BDD-cost: 3 c ---[2261]---> BDD-cost: 3 c ---[2250]---> BDD-cost: 196 c ---[2239]---> BDD-cost: 5 c ---[2218]---> BDD-cost: 11 c ---[2207]---> BDD-cost: 7 c ---[2196]---> BDD-cost: 15 c ---[2166]---> BDD-cost: 19 c ---[2143]---> Adder-cost: 477 maxlim: 2053920 bits: 22/21 c ---[2142]---> BDD-cost: 81 c ---[2141]---> BDD-cost: 19 c ---[2130]---> BDD-cost: 19 c ---[2119]---> BDD-cost: 17 c ---[2108]---> BDD-cost: 17 c ---[2099]---> BDD-cost: 527 c ---[2097]---> BDD-cost: 19 c ---[2086]---> BDD-cost: 19 c ---[2075]---> BDD-cost: 19 c ---[2033]---> BDD-cost: 171 c ---[2011]---> BDD-cost: 19 c ---[2000]---> BDD-cost: 17 c ---[1989]---> BDD-cost: 19 c ---[1978]---> BDD-cost: 19 c ---[1967]---> BDD-cost: 19 c ---[1946]---> BDD-cost: 21 c ---[1935]---> BDD-cost: 19 c ---[1924]---> BDD-cost: 131 c ---[1923]---> BDD-cost: 17 c ---[1912]---> BDD-cost: 19 c ---[1880]---> BDD-cost: 3 c ---[1869]---> BDD-cost: 15 c ---[1865]---> BDD-cost: 551 c ---[1858]---> BDD-cost: 13 c ---[1848]---> BDD-cost: 19 c ---[1827]---> BDD-cost: 19 c ---[1816]---> BDD-cost: 74 c ---[1815]---> BDD-cost: 19 c ---[1794]---> BDD-cost: 19 c ---[1773]---> BDD-cost: 19 c ---[1752]---> BDD-cost: 19 c ---[1741]---> BDD-cost: 19 c ---[1712]---> BDD-cost: 51 c ---[1711]---> BDD-cost: 15 c ---[1693]---> BDD-cost: 19 c ---[1672]---> BDD-cost: 3 c ---[1661]---> BDD-cost: 15 c ---[1650]---> BDD-cost: 19 c ---[1639]---> BDD-cost: 19 c ---[1628]---> BDD-cost: 19 c ---[1627]---> BDD-cost: 488 c ---[1612]---> BDD-cost: 29 c ---[1611]---> BDD-cost: 17 c ---[1602]---> BDD-cost: 19 c ---[1594]---> BDD-cost: 19 c ---[1577]---> BDD-cost: 19 c ---[1558]---> BDD-cost: 19 c ---[1547]---> BDD-cost: 15 c ---[1526]---> BDD-cost: 17 c ---[1518]---> BDD-cost: 3 c ---[1513]---> BDD-cost: 17 c ---[1482]---> BDD-cost: 7 c ---[1462]---> BDD-cost: 335 c ---[1451]---> BDD-cost: 3 c ---[1430]---> BDD-cost: 17 c ---[1339]---> BDD-cost: 17 c ---[1338]---> BDD-cost: 11 c ---[1327]---> BDD-cost: 7 c ---[1316]---> BDD-cost: 416 c ---[1306]---> BDD-cost: 17 c ---[1295]---> BDD-cost: 5 c ---[1284]---> BDD-cost: 3 c ---[1273]---> BDD-cost: 3 c ---[1262]---> BDD-cost: 7 c ---[1251]---> BDD-cost: 7 c ---[1240]---> BDD-cost: 19 c ---[1229]---> BDD-cost: 19 c ---[1218]---> BDD-cost: 19 c ---[1207]---> BDD-cost: 5 c ---[1196]---> BDD-cost: 17 c ---[1185]---> BDD-cost: 19 c ---[1163]---> BDD-cost: 29 c ---[1152]---> BDD-cost: 29 c ---[1141]---> BDD-cost: 29 c ---[1130]---> BDD-cost: 29 c ---[1128]---> BDD-cost: 260 c ---[1119]---> Adder-cost: 2340 maxlim: 3201964 bits: 22/22 c ---[1118]---> BDD-cost: 21 c ---[1117]---> BDD-cost: 29 c ---[1106]---> BDD-cost: 23 c ---[1095]---> BDD-cost: 17 c ---[1084]---> BDD-cost: 17 c ---[1073]---> BDD-cost: 17 c ---[1062]---> BDD-cost: 7 c ---[1051]---> BDD-cost: 7 c ---[1019]---> BDD-cost: 21 c ---[1008]---> BDD-cost: 29 c ---[1007]---> BDD-cost: 7 c ---[ 996]---> BDD-cost: 5 c ---[ 988]---> BDD-cost: 212 c ---[ 985]---> BDD-cost: 5 c ---[ 974]---> BDD-cost: 5 c ---[ 963]---> BDD-cost: 7 c ---[ 952]---> BDD-cost: 9 c ---[ 931]---> BDD-cost: 5 c ---[ 920]---> BDD-cost: 21 c ---[ 909]---> BDD-cost: 17 c ---[ 891]---> BDD-cost: 161 c ---[ 888]---> BDD-cost: 27 c ---[ 877]---> BDD-cost: 17 c ---[ 866]---> BDD-cost: 17 c ---[ 855]---> BDD-cost: 27 c ---[ 844]---> BDD-cost: 23 c ---[ 814]---> BDD-cost: 65 c ---[ 813]---> BDD-cost: 27 c ---[ 802]---> BDD-cost: 19 c ---[ 790]---> BDD-cost: 29 c ---[ 780]---> BDD-cost: 32 c ---[ 779]---> BDD-cost: 23 c ---[ 761]---> BDD-cost: 50 c ---[ 739]---> BDD-cost: 38 c ---[ 738]---> BDD-cost: 21 c ---[ 727]---> BDD-cost: 23 c ---[ 719]---> BDD-cost: 26 c ---[ 704]---> BDD-cost: 17 c ---[ 695]---> BDD-cost: 21 c ---[ 689]---> BDD-cost: 17 c ---[ 684]---> BDD-cost: 11 c ---[ 683]---> BDD-cost: 23 c ---[ 678]---> BDD-cost: 14 c ---[ 672]---> BDD-cost: 11 c ---[ 669]---> BDD-cost: 19 c ---[ 666]---> BDD-cost: 19 c ---[ 664]---> BDD-cost: 29 c ---[ 663]---> BDD-cost: 29 c ---[ 662]---> BDD-cost: 19 c ---[ 661]---> BDD-cost: 29 c ---[ 660]---> BDD-cost: 29 c ---[ 659]---> BDD-cost: 23 c ---[ 658]---> BDD-cost: 25 c ---[ 657]---> BDD-cost: 29 c ---[ 656]---> BDD-cost: 27 c ---[ 655]---> BDD-cost: 19 c ---[ 654]---> BDD-cost: 19 c ---[ 653]---> BDD-cost: 19 c ---[ 652]---> BDD-cost: 19 c ---[ 651]---> BDD-cost: 19 c ---[ 650]---> BDD-cost: 17 c ---[ 649]---> BDD-cost: 19 c ---[ 648]---> BDD-cost: 9 c ---[ 647]---> BDD-cost: 19 c ---[ 644]---> BDD-cost: 23 c ---[ 643]---> BDD-cost: 27 c ---[ 642]---> BDD-cost: 3 c ---[ 641]---> BDD-cost: 19 c ---[ 640]---> BDD-cost: 3 c ---[ 639]---> BDD-cost: 25 c ---[ 637]---> BDD-cost: 23 c ---[ 636]---> BDD-cost: 27 c ---[ 635]---> BDD-cost: 21 c ---[ 634]---> BDD-cost: 15 c ---[ 633]---> BDD-cost: 15 c ---[ 628]---> BDD-cost: 3 c ---[ 627]---> BDD-cost: 1925 c ---[ 626]---> BDD-cost: 5 c ---[ 625]---> BDD-cost: 29 c ---[ 624]---> BDD-cost: 29 c ---[ 623]---> BDD-cost: 29 c ---[ 622]---> BDD-cost: 29 c ---[ 621]---> BDD-cost: 19 c ---[ 620]---> BDD-cost: 21 c ---[ 619]---> BDD-cost: 19 c ---[ 618]---> BDD-cost: 19 c ---[ 616]---> BDD-cost: 19 c ---[ 615]---> BDD-cost: 19 c ---[ 614]---> BDD-cost: 17 c ---[ 613]---> BDD-cost: 19 c ---[ 612]---> BDD-cost: 15 c ---[ 611]---> BDD-cost: 27 c ---[ 610]---> BDD-cost: 3 c ---[ 609]---> BDD-cost: 9 c ---[ 608]---> BDD-cost: 9 c ---[ 607]---> BDD-cost: 7 c ---[ 606]---> BDD-cost: 19 c ---[ 604]---> BDD-cost: 29 c ---[ 603]---> BDD-cost: 23 c ---[ 602]---> BDD-cost: 21 c ---[ 601]---> BDD-cost: 27 c ---[ 600]---> BDD-cost: 23 c ---[ 598]---> BDD-cost: 23 c ---[ 597]---> BDD-cost: 19 c ---[ 596]---> BDD-cost: 29 c ---[ 595]---> BDD-cost: 27 c ---[ 594]---> BDD-cost: 23 c ---[ 593]---> BDD-cost: 25 c ---[ 592]---> BDD-cost: 19 c ---[ 591]---> BDD-cost: 23 c ---[ 590]---> BDD-cost: 27 c ---[ 584]---> BDD-cost: 23 c ---[ 581]---> BDD-cost: 23 c ---[ 580]---> BDD-cost: 19 c ---[ 579]---> BDD-cost: 659 c ---[ 575]---> BDD-cost: 29 c ---[ 554]---> BDD-cost: 19 c ---[ 543]---> Adder-cost: 1584 maxlim: 1898736 bits: 21/21 c ---[ 542]---> BDD-cost: 19 c ---[ 477]---> BDD-cost: 29 c ---[ 466]---> BDD-cost: 23 c ---[ 444]---> BDD-cost: 15 c ---[ 433]---> Adder-cost: 1568 maxlim: 1898736 bits: 21/21 c ---[ 422]---> BDD-cost: 23 c ---[ 400]---> BDD-cost: 5 c ---[ 378]---> BDD-cost: 27 c ---[ 367]---> BDD-cost: 11 c ---[ 356]---> BDD-cost: 29 c ---[ 345]---> BDD-cost: 19 c ---[ 324]---> Adder-cost: 1704 maxlim: 2180627 bits: 22/22 c ---[ 312]---> BDD-cost: 21 c ---[ 279]---> BDD-cost: 9 c ---[ 268]---> BDD-cost: 29 c ---[ 260]---> BDD-cost: 305 c ---[ 246]---> BDD-cost: 29 c ---[ 235]---> BDD-cost: 27 c ---[ 224]---> BDD-cost: 29 c ---[ 213]---> Adder-cost: 1576 maxlim: 1898736 bits: 21/21 c ---[ 212]---> BDD-cost: 15 c ---[ 201]---> BDD-cost: 15 c ---[ 190]---> BDD-cost: 23 c ---[ 179]---> BDD-cost: 23 c ---[ 158]---> BDD-cost: 9 c ---[ 118]---> BDD-cost: 461 c ---[ 115]---> BDD-cost: 5 c ---[ 105]---> Adder-cost: 1630 maxlim: 1978736 bits: 21/21 c ---[ 83]---> BDD-cost: 29 c ---[ 72]---> BDD-cost: 27 c ---[ 61]---> BDD-cost: 5 c ---[ 40]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 412444 1339233 | 137481 0 0 nan | 0.000 % | c | 101 | 412404 1339099 | 151229 96 298 3.1 | 0.714 % | c | 251 | 411996 1337793 | 166352 201 8264 41.1 | 0.807 % | c | 476 | 411996 1337793 | 182987 426 15953 37.4 | 0.807 % | c | 814 | 411523 1336710 | 201285 589 14598 24.8 | 0.951 % | c | 1320 | 411523 1336710 | 221414 1095 33853 30.9 | 0.951 % | c | 2079 | 411523 1336710 | 243555 1854 57475 31.0 | 0.951 % | c | 3220 | 411515 1336684 | 267911 2994 87576 29.3 | 0.952 % | c | 4928 | 411515 1336684 | 294702 4702 140804 29.9 | 0.952 % | c | 7493 | 411515 1336684 | 324173 7267 270478 37.2 | 0.952 % | c | 11338 | 411515 1336684 | 356590 11112 409874 36.9 | 0.952 % | c | 17104 | 410719 1334080 | 392249 13076 397285 30.4 | 1.119 % | c | 25755 | 410426 1333029 | 431474 21587 676127 31.3 | 1.169 % | c | 38730 | 409921 1331539 | 474621 34454 1130992 32.8 | 1.275 % | c | 58191 | 409623 1330662 | 522083 53875 1831052 34.0 | 1.343 % | c | 87383 | 409253 1329565 | 574292 82956 2941040 35.5 | 1.428 % | c | 131173 | 407943 1325181 | 631721 126260 4482630 35.5 | 1.677 % | c | 196858 | 403226 1312621 | 694893 191317 6968041 36.4 | 3.041 % |
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/331/stat): 331 (minisat+_script) R 330 331 30740 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1797441912 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/331/statm): 174 3 169 147 0 27 0 [pid=331] 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=332 New process pid=333 New process pid=334 execve syscall for /bin/sed executable One traced child (pid=333) 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=334) exited with status: 0 One traced child (pid=332) exited with status: 0 New process pid=335 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-mkc.opb [startup+10.0041 s] Raw data (loadavg): 0.94 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 970 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221152 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 12112 [startup+20.0049 s] Raw data (loadavg): 0.95 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 1970 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221220768 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 12112 [startup+30.0056 s] Raw data (loadavg): 0.95 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 2971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221220592 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 29.84 Current children cumulated vsize (Kb) 12112 [startup+40.0064 s] Raw data (loadavg): 0.96 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 3971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221648 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 39.84 Current children cumulated vsize (Kb) 12112 [startup+50.0082 s] Raw data (loadavg): 0.97 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 4971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221296 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 49.84 Current children cumulated vsize (Kb) 12112 [startup+60.009 s] Raw data (loadavg): 0.97 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 5970 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221648 134600301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 12112 [startup+70.0098 s] Raw data (loadavg): 0.98 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 6971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221220992 134677375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 69.84 Current children cumulated vsize (Kb) 12112 [startup+80.0106 s] Raw data (loadavg): 0.98 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 7971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221824 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 79.84 Current children cumulated vsize (Kb) 12112 [startup+90.0103 s] Raw data (loadavg): 0.98 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 8971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221296 134601029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 89.84 Current children cumulated vsize (Kb) 12112 [startup+100.011 s] Raw data (loadavg): 0.98 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 9971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221220944 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 99.84 Current children cumulated vsize (Kb) 12112 [startup+110.012 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 10971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221472 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 109.84 Current children cumulated vsize (Kb) 12112 [startup+120.012 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 11972 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221120 134600191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 119.85 Current children cumulated vsize (Kb) 12112 [startup+130.012 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 12971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221040 134676321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 129.84 Current children cumulated vsize (Kb) 12112 [startup+140.013 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 13971 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221472 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 139.84 Current children cumulated vsize (Kb) 12112 [startup+150.014 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 3777 0 0 0 14972 13 0 0 25 0 1 0 1797441917 10227712 2288 4294967295 134512640 135094434 3221224448 3221221296 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 2497 2288 145 145 0 2352 0 [pid=335] vsize: 9988 Current children cumulated CPU time (s) 149.85 Current children cumulated vsize (Kb) 12112 [startup+160.015 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 8688 0 0 0 15949 29 0 0 25 0 1 0 1797441917 25575424 5877 4294967295 134512640 135094434 3221224448 3221221536 134677086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 6244 5877 145 145 0 6099 0 [pid=335] vsize: 24976 Current children cumulated CPU time (s) 159.78 Current children cumulated vsize (Kb) 27100 [startup+170.016 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 8856 0 0 0 16947 30 0 0 25 0 1 0 1797441917 25575424 5877 4294967295 134512640 135094434 3221224448 3221222352 134600904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 6244 5877 145 145 0 6099 0 [pid=335] vsize: 24976 Current children cumulated CPU time (s) 169.77 Current children cumulated vsize (Kb) 27100 [startup+180.016 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 9024 0 0 0 17947 31 0 0 25 0 1 0 1797441917 25575424 5877 4294967295 134512640 135094434 3221224448 3221222144 134676245 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 6244 5877 145 145 0 6099 0 [pid=335] vsize: 24976 Current children cumulated CPU time (s) 179.78 Current children cumulated vsize (Kb) 27100 [startup+190.017 s] Raw data (loadavg): 0.99 0.99 0.92 1/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) T 331 331 30740 0 -1 0 16077 0 0 0 18887 60 0 0 25 0 1 0 1797441917 57573376 12909 4294967295 134512640 135094434 3221224448 3221223144 134801757 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/335/statm): 14056 12909 145 145 0 13911 0 [pid=335] vsize: 56224 Current children cumulated CPU time (s) 189.47 Current children cumulated vsize (Kb) 58348 [startup+200.019 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 16476 0 0 0 19881 63 0 0 25 0 1 0 1797441917 59224064 13308 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 14459 13308 145 145 0 14314 0 [pid=335] vsize: 57836 Current children cumulated CPU time (s) 199.44 Current children cumulated vsize (Kb) 59960 [startup+210.02 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 16698 0 0 0 20878 64 0 0 25 0 1 0 1797441917 60088320 13530 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 14670 13530 145 145 0 14525 0 [pid=335] vsize: 58680 Current children cumulated CPU time (s) 209.42 Current children cumulated vsize (Kb) 60804 [startup+220.02 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 16770 0 0 0 21877 65 0 0 25 0 1 0 1797441917 60436480 13602 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 14755 13602 145 145 0 14610 0 [pid=335] vsize: 59020 Current children cumulated CPU time (s) 219.42 Current children cumulated vsize (Kb) 61144 [startup+230.022 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 16984 0 0 0 22873 66 0 0 25 0 1 0 1797441917 61296640 13816 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 14965 13816 145 145 0 14820 0 [pid=335] vsize: 59860 Current children cumulated CPU time (s) 229.39 Current children cumulated vsize (Kb) 61984 [startup+240.022 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 17264 0 0 0 23868 69 0 0 25 0 1 0 1797441917 62418944 14096 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 15239 14096 145 145 0 15094 0 [pid=335] vsize: 60956 Current children cumulated CPU time (s) 239.37 Current children cumulated vsize (Kb) 63080 [startup+250.024 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 17443 0 0 0 24865 70 0 0 25 0 1 0 1797441917 63135744 14275 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 15414 14275 145 145 0 15269 0 [pid=335] vsize: 61656 Current children cumulated CPU time (s) 249.35 Current children cumulated vsize (Kb) 63780 [startup+260.026 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 17647 0 0 0 25862 71 0 0 25 0 1 0 1797441917 64086016 14479 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 15646 14479 145 145 0 15501 0 [pid=335] vsize: 62584 Current children cumulated CPU time (s) 259.33 Current children cumulated vsize (Kb) 64708 [startup+270.025 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 17905 0 0 0 26857 74 0 0 25 0 1 0 1797441917 65118208 14737 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 15898 14737 145 145 0 15753 0 [pid=335] vsize: 63592 Current children cumulated CPU time (s) 269.31 Current children cumulated vsize (Kb) 65716 [startup+280.026 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18124 0 0 0 27853 75 0 0 25 0 1 0 1797441917 65998848 14956 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 16113 14956 145 145 0 15968 0 [pid=335] vsize: 64452 Current children cumulated CPU time (s) 279.28 Current children cumulated vsize (Kb) 66576 [startup+290.027 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18256 0 0 0 28850 77 0 0 25 0 1 0 1797441917 66531328 15088 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 16243 15088 145 145 0 16098 0 [pid=335] vsize: 64972 Current children cumulated CPU time (s) 289.27 Current children cumulated vsize (Kb) 67096 [startup+300.029 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18370 0 0 0 29848 78 0 0 25 0 1 0 1797441917 66990080 15202 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 16355 15202 145 145 0 16210 0 [pid=335] vsize: 65420 Current children cumulated CPU time (s) 299.26 Current children cumulated vsize (Kb) 67544 [startup+310.029 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18513 0 0 0 30845 79 0 0 25 0 1 0 1797441917 67575808 15345 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 16498 15345 145 145 0 16353 0 [pid=335] vsize: 65992 Current children cumulated CPU time (s) 309.24 Current children cumulated vsize (Kb) 68116 [startup+320.03 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18645 0 0 0 31842 81 0 0 25 0 1 0 1797441917 68100096 15477 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 16626 15477 145 145 0 16481 0 [pid=335] vsize: 66504 Current children cumulated CPU time (s) 319.23 Current children cumulated vsize (Kb) 68628 [startup+330.032 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18786 0 0 0 32839 82 0 0 25 0 1 0 1797441917 68665344 15618 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 16764 15618 145 145 0 16619 0 [pid=335] vsize: 67056 Current children cumulated CPU time (s) 329.21 Current children cumulated vsize (Kb) 69180 [startup+340.033 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18897 0 0 0 33836 84 0 0 25 0 1 0 1797441917 69120000 15729 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 16875 15729 145 145 0 16730 0 [pid=335] vsize: 67500 Current children cumulated CPU time (s) 339.2 Current children cumulated vsize (Kb) 69624 [startup+350.035 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 18995 0 0 0 34835 85 0 0 25 0 1 0 1797441917 69808128 15827 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 17043 15827 145 145 0 16898 0 [pid=335] vsize: 68172 Current children cumulated CPU time (s) 349.2 Current children cumulated vsize (Kb) 70296 [startup+360.035 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 19089 0 0 0 35832 87 0 0 25 0 1 0 1797441917 70184960 15921 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 17135 15921 145 145 0 16990 0 [pid=335] vsize: 68540 Current children cumulated CPU time (s) 359.19 Current children cumulated vsize (Kb) 70664 [startup+370.037 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 19257 0 0 0 36828 89 0 0 25 0 1 0 1797441917 70868992 16089 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 17302 16089 145 145 0 17157 0 [pid=335] vsize: 69208 Current children cumulated CPU time (s) 369.17 Current children cumulated vsize (Kb) 71332 [startup+380.039 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 19506 0 0 0 37823 92 0 0 25 0 1 0 1797441917 71876608 16338 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 17548 16338 145 145 0 17403 0 [pid=335] vsize: 70192 Current children cumulated CPU time (s) 379.15 Current children cumulated vsize (Kb) 72316 [startup+390.04 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 19651 0 0 0 38820 93 0 0 25 0 1 0 1797441917 72466432 16483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 17692 16483 145 145 0 17547 0 [pid=335] vsize: 70768 Current children cumulated CPU time (s) 389.13 Current children cumulated vsize (Kb) 72892 [startup+400.041 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 19831 0 0 0 39817 95 0 0 25 0 1 0 1797441917 73183232 16663 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 17867 16663 145 145 0 17722 0 [pid=335] vsize: 71468 Current children cumulated CPU time (s) 399.12 Current children cumulated vsize (Kb) 73592 [startup+410.042 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 19934 0 0 0 40816 96 0 0 25 0 1 0 1797441917 73605120 16766 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 17970 16766 145 145 0 17825 0 [pid=335] vsize: 71880 Current children cumulated CPU time (s) 409.12 Current children cumulated vsize (Kb) 74004 [startup+420.042 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20040 0 0 0 41814 97 0 0 25 0 1 0 1797441917 74035200 16872 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18075 16872 145 145 0 17930 0 [pid=335] vsize: 72300 Current children cumulated CPU time (s) 419.11 Current children cumulated vsize (Kb) 74424 [startup+430.043 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20121 0 0 0 42812 97 0 0 25 0 1 0 1797441917 74366976 16953 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18156 16953 145 145 0 18011 0 [pid=335] vsize: 72624 Current children cumulated CPU time (s) 429.09 Current children cumulated vsize (Kb) 74748 [startup+440.043 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20208 0 0 0 43811 98 0 0 25 0 1 0 1797441917 74727424 17040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18244 17040 145 145 0 18099 0 [pid=335] vsize: 72976 Current children cumulated CPU time (s) 439.09 Current children cumulated vsize (Kb) 75100 [startup+450.044 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20274 0 0 0 44810 99 0 0 25 0 1 0 1797441917 74997760 17106 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18310 17106 145 145 0 18165 0 [pid=335] vsize: 73240 Current children cumulated CPU time (s) 449.09 Current children cumulated vsize (Kb) 75364 [startup+460.045 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20352 0 0 0 45809 99 0 0 25 0 1 0 1797441917 75304960 17184 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18385 17184 145 145 0 18240 0 [pid=335] vsize: 73540 Current children cumulated CPU time (s) 459.08 Current children cumulated vsize (Kb) 75664 [startup+470.046 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20455 0 0 0 46807 100 0 0 25 0 1 0 1797441917 75739136 17287 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18491 17287 145 145 0 18346 0 [pid=335] vsize: 73964 Current children cumulated CPU time (s) 469.07 Current children cumulated vsize (Kb) 76088 [startup+480.047 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20566 0 0 0 47805 101 0 0 25 0 1 0 1797441917 76197888 17398 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18603 17398 145 145 0 18458 0 [pid=335] vsize: 74412 Current children cumulated CPU time (s) 479.06 Current children cumulated vsize (Kb) 76536 [startup+490.047 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20629 0 0 0 48805 101 0 0 25 0 1 0 1797441917 76460032 17461 4294967295 134512640 135094434 3221224448 3221223104 134558094 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18667 17461 145 145 0 18522 0 [pid=335] vsize: 74668 Current children cumulated CPU time (s) 489.06 Current children cumulated vsize (Kb) 76792 [startup+500.049 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20698 0 0 0 49804 101 0 0 25 0 1 0 1797441917 76750848 17530 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18738 17530 145 145 0 18593 0 [pid=335] vsize: 74952 Current children cumulated CPU time (s) 499.05 Current children cumulated vsize (Kb) 77076 [startup+510.05 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20755 0 0 0 50804 102 0 0 25 0 1 0 1797441917 76992512 17587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18797 17587 145 145 0 18652 0 [pid=335] vsize: 75188 Current children cumulated CPU time (s) 509.06 Current children cumulated vsize (Kb) 77312 [startup+520.051 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20808 0 0 0 51803 102 0 0 25 0 1 0 1797441917 77197312 17640 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18847 17640 145 145 0 18702 0 [pid=335] vsize: 75388 Current children cumulated CPU time (s) 519.05 Current children cumulated vsize (Kb) 77512 [startup+530.051 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20858 0 0 0 52803 102 0 0 25 0 1 0 1797441917 77402112 17690 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18897 17690 145 145 0 18752 0 [pid=335] vsize: 75588 Current children cumulated CPU time (s) 529.05 Current children cumulated vsize (Kb) 77712 [startup+540.052 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 20958 0 0 0 53801 103 0 0 25 0 1 0 1797441917 77795328 17790 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 18993 17790 145 145 0 18848 0 [pid=335] vsize: 75972 Current children cumulated CPU time (s) 539.04 Current children cumulated vsize (Kb) 78096 [startup+550.053 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21085 0 0 0 54799 104 0 0 25 0 1 0 1797441917 78315520 17917 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19120 17917 145 145 0 18975 0 [pid=335] vsize: 76480 Current children cumulated CPU time (s) 549.03 Current children cumulated vsize (Kb) 78604 [startup+560.054 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21167 0 0 0 55798 105 0 0 25 0 1 0 1797441917 78651392 17999 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19202 17999 145 145 0 19057 0 [pid=335] vsize: 76808 Current children cumulated CPU time (s) 559.03 Current children cumulated vsize (Kb) 78932 [startup+570.053 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21221 0 0 0 56797 105 0 0 25 0 1 0 1797441917 78872576 18053 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19256 18053 145 145 0 19111 0 [pid=335] vsize: 77024 Current children cumulated CPU time (s) 569.02 Current children cumulated vsize (Kb) 79148 [startup+580.055 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21306 0 0 0 57796 105 0 0 25 0 1 0 1797441917 79200256 18138 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19336 18138 145 145 0 19191 0 [pid=335] vsize: 77344 Current children cumulated CPU time (s) 579.01 Current children cumulated vsize (Kb) 79468 [startup+590.056 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21385 0 0 0 58795 106 0 0 25 0 1 0 1797441917 79523840 18217 4294967295 134512640 135094434 3221224448 3221223128 134553525 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19415 18217 145 145 0 19270 0 [pid=335] vsize: 77660 Current children cumulated CPU time (s) 589.01 Current children cumulated vsize (Kb) 79784 [startup+600.057 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21457 0 0 0 59795 106 0 0 25 0 1 0 1797441917 79835136 18289 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19491 18289 145 145 0 19346 0 [pid=335] vsize: 77964 Current children cumulated CPU time (s) 599.01 Current children cumulated vsize (Kb) 80088 [startup+610.058 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21533 0 0 0 60794 107 0 0 25 0 1 0 1797441917 80162816 18365 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19571 18365 145 145 0 19426 0 [pid=335] vsize: 78284 Current children cumulated CPU time (s) 609.01 Current children cumulated vsize (Kb) 80408 [startup+620.058 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21628 0 0 0 61793 107 0 0 25 0 1 0 1797441917 80539648 18460 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19663 18460 145 145 0 19518 0 [pid=335] vsize: 78652 Current children cumulated CPU time (s) 619 Current children cumulated vsize (Kb) 80776 [startup+630.059 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21686 0 0 0 62792 108 0 0 25 0 1 0 1797441917 80781312 18518 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19722 18518 145 145 0 19577 0 [pid=335] vsize: 78888 Current children cumulated CPU time (s) 629 Current children cumulated vsize (Kb) 81012 [startup+640.06 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21748 0 0 0 63791 108 0 0 25 0 1 0 1797441917 81027072 18580 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19782 18580 145 145 0 19637 0 [pid=335] vsize: 79128 Current children cumulated CPU time (s) 638.99 Current children cumulated vsize (Kb) 81252 [startup+650.061 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21818 0 0 0 64790 108 0 0 25 0 1 0 1797441917 81317888 18650 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 19853 18650 145 145 0 19708 0 [pid=335] vsize: 79412 Current children cumulated CPU time (s) 648.98 Current children cumulated vsize (Kb) 81536 [startup+660.062 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 21913 0 0 0 65789 109 0 0 25 0 1 0 1797441917 81702912 18745 4294967295 134512640 135094434 3221224448 3221223088 134556681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/335/statm): 19947 18745 145 145 0 19802 0 [pid=335] vsize: 79788 Current children cumulated CPU time (s) 658.98 Current children cumulated vsize (Kb) 81912 [startup+670.062 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22017 0 0 0 66787 110 0 0 25 0 1 0 1797441917 82075648 18849 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20038 18849 145 145 0 19893 0 [pid=335] vsize: 80152 Current children cumulated CPU time (s) 668.97 Current children cumulated vsize (Kb) 82276 [startup+680.064 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22140 0 0 0 67786 110 0 0 25 0 1 0 1797441917 82604032 18972 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20167 18972 145 145 0 20022 0 [pid=335] vsize: 80668 Current children cumulated CPU time (s) 678.96 Current children cumulated vsize (Kb) 82792 [startup+690.065 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22174 0 0 0 68786 110 0 0 25 0 1 0 1797441917 82739200 19006 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20200 19006 145 145 0 20055 0 [pid=335] vsize: 80800 Current children cumulated CPU time (s) 688.96 Current children cumulated vsize (Kb) 82924 [startup+700.066 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22242 0 0 0 69785 111 0 0 25 0 1 0 1797441917 83595264 19074 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20409 19074 145 145 0 20264 0 [pid=335] vsize: 81636 Current children cumulated CPU time (s) 698.96 Current children cumulated vsize (Kb) 83760 [startup+710.066 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22304 0 0 0 70785 111 0 0 25 0 1 0 1797441917 83836928 19136 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20468 19136 145 145 0 20323 0 [pid=335] vsize: 81872 Current children cumulated CPU time (s) 708.96 Current children cumulated vsize (Kb) 83996 [startup+720.066 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22364 0 0 0 71784 111 0 0 25 0 1 0 1797441917 84078592 19196 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20527 19196 145 145 0 20382 0 [pid=335] vsize: 82108 Current children cumulated CPU time (s) 718.95 Current children cumulated vsize (Kb) 84232 [startup+730.067 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22437 0 0 0 72783 112 0 0 25 0 1 0 1797441917 84365312 19269 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20597 19269 145 145 0 20452 0 [pid=335] vsize: 82388 Current children cumulated CPU time (s) 728.95 Current children cumulated vsize (Kb) 84512 [startup+740.068 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22489 0 0 0 73782 112 0 0 25 0 1 0 1797441917 84594688 19321 4294967295 134512640 135094434 3221224448 3221223108 134553528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20653 19321 145 145 0 20508 0 [pid=335] vsize: 82612 Current children cumulated CPU time (s) 738.94 Current children cumulated vsize (Kb) 84736 [startup+750.068 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22539 0 0 0 74782 112 0 0 25 0 1 0 1797441917 84799488 19371 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20703 19371 145 145 0 20558 0 [pid=335] vsize: 82812 Current children cumulated CPU time (s) 748.94 Current children cumulated vsize (Kb) 84936 [startup+760.069 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22594 0 0 0 75781 112 0 0 25 0 1 0 1797441917 85024768 19426 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20758 19426 145 145 0 20613 0 [pid=335] vsize: 83032 Current children cumulated CPU time (s) 758.93 Current children cumulated vsize (Kb) 85156 [startup+770.07 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22661 0 0 0 76780 113 0 0 25 0 1 0 1797441917 85307392 19493 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20827 19493 145 145 0 20682 0 [pid=335] vsize: 83308 Current children cumulated CPU time (s) 768.93 Current children cumulated vsize (Kb) 85432 [startup+780.071 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22735 0 0 0 77779 114 0 0 25 0 1 0 1797441917 85639168 19567 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20908 19567 145 145 0 20763 0 [pid=335] vsize: 83632 Current children cumulated CPU time (s) 778.93 Current children cumulated vsize (Kb) 85756 [startup+790.072 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22815 0 0 0 78778 114 0 0 25 0 1 0 1797441917 85950464 19647 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 20984 19647 145 145 0 20839 0 [pid=335] vsize: 83936 Current children cumulated CPU time (s) 788.92 Current children cumulated vsize (Kb) 86060 [startup+800.073 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22869 0 0 0 79778 114 0 0 25 0 1 0 1797441917 86192128 19701 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21043 19701 145 145 0 20898 0 [pid=335] vsize: 84172 Current children cumulated CPU time (s) 798.92 Current children cumulated vsize (Kb) 86296 [startup+810.074 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 22953 0 0 0 80777 115 0 0 25 0 1 0 1797441917 86556672 19785 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21132 19785 145 145 0 20987 0 [pid=335] vsize: 84528 Current children cumulated CPU time (s) 808.92 Current children cumulated vsize (Kb) 86652 [startup+820.075 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23009 0 0 0 81777 115 0 0 25 0 1 0 1797441917 86781952 19841 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21187 19841 145 145 0 21042 0 [pid=335] vsize: 84748 Current children cumulated CPU time (s) 818.92 Current children cumulated vsize (Kb) 86872 [startup+830.076 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23076 0 0 0 82776 115 0 0 25 0 1 0 1797441917 87056384 19908 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21254 19908 145 145 0 21109 0 [pid=335] vsize: 85016 Current children cumulated CPU time (s) 828.91 Current children cumulated vsize (Kb) 87140 [startup+840.076 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23239 0 0 0 83773 116 0 0 25 0 1 0 1797441917 87711744 20071 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21414 20071 145 145 0 21269 0 [pid=335] vsize: 85656 Current children cumulated CPU time (s) 838.89 Current children cumulated vsize (Kb) 87780 [startup+850.078 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23270 0 0 0 84773 116 0 0 25 0 1 0 1797441917 87863296 20102 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21451 20102 145 145 0 21306 0 [pid=335] vsize: 85804 Current children cumulated CPU time (s) 848.89 Current children cumulated vsize (Kb) 87928 [startup+860.079 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23321 0 0 0 85772 117 0 0 25 0 1 0 1797441917 88059904 20153 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21499 20153 145 145 0 21354 0 [pid=335] vsize: 85996 Current children cumulated CPU time (s) 858.89 Current children cumulated vsize (Kb) 88120 [startup+870.079 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23376 0 0 0 86771 117 0 0 25 0 1 0 1797441917 88293376 20208 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21556 20208 145 145 0 21411 0 [pid=335] vsize: 86224 Current children cumulated CPU time (s) 868.88 Current children cumulated vsize (Kb) 88348 [startup+880.081 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23437 0 0 0 87771 117 0 0 25 0 1 0 1797441917 88551424 20269 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21619 20269 145 145 0 21474 0 [pid=335] vsize: 86476 Current children cumulated CPU time (s) 878.88 Current children cumulated vsize (Kb) 88600 [startup+890.081 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23506 0 0 0 88770 118 0 0 25 0 1 0 1797441917 88825856 20338 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21686 20338 145 145 0 21541 0 [pid=335] vsize: 86744 Current children cumulated CPU time (s) 888.88 Current children cumulated vsize (Kb) 88868 [startup+900.082 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23570 0 0 0 89770 118 0 0 25 0 1 0 1797441917 89133056 20402 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21761 20402 145 145 0 21616 0 [pid=335] vsize: 87044 Current children cumulated CPU time (s) 898.88 Current children cumulated vsize (Kb) 89168 [startup+910.083 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23640 0 0 0 90770 119 0 0 25 0 1 0 1797441917 89419776 20472 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21831 20472 145 145 0 21686 0 [pid=335] vsize: 87324 Current children cumulated CPU time (s) 908.89 Current children cumulated vsize (Kb) 89448 [startup+920.084 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23693 0 0 0 91769 119 0 0 25 0 1 0 1797441917 89681920 20525 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21895 20525 145 145 0 21750 0 [pid=335] vsize: 87580 Current children cumulated CPU time (s) 918.88 Current children cumulated vsize (Kb) 89704 [startup+930.084 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23733 0 0 0 92769 119 0 0 25 0 1 0 1797441917 89829376 20565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21931 20565 145 145 0 21786 0 [pid=335] vsize: 87724 Current children cumulated CPU time (s) 928.88 Current children cumulated vsize (Kb) 89848 [startup+940.085 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23797 0 0 0 93768 120 0 0 25 0 1 0 1797441917 90083328 20629 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 21993 20629 145 145 0 21848 0 [pid=335] vsize: 87972 Current children cumulated CPU time (s) 938.88 Current children cumulated vsize (Kb) 90096 [startup+950.087 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23867 0 0 0 94767 120 0 0 25 0 1 0 1797441917 90382336 20699 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22066 20699 145 145 0 21921 0 [pid=335] vsize: 88264 Current children cumulated CPU time (s) 948.87 Current children cumulated vsize (Kb) 90388 [startup+960.088 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23924 0 0 0 95767 120 0 0 25 0 1 0 1797441917 90652672 20756 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22132 20756 145 145 0 21987 0 [pid=335] vsize: 88528 Current children cumulated CPU time (s) 958.87 Current children cumulated vsize (Kb) 90652 [startup+970.088 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 23995 0 0 0 96766 121 0 0 25 0 1 0 1797441917 90931200 20827 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22200 20827 145 145 0 22055 0 [pid=335] vsize: 88800 Current children cumulated CPU time (s) 968.87 Current children cumulated vsize (Kb) 90924 [startup+980.09 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24050 0 0 0 97766 121 0 0 25 0 1 0 1797441917 91115520 20882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22245 20882 145 145 0 22100 0 [pid=335] vsize: 88980 Current children cumulated CPU time (s) 978.87 Current children cumulated vsize (Kb) 91104 [startup+990.091 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24112 0 0 0 98765 122 0 0 25 0 1 0 1797441917 91385856 20944 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22311 20944 145 145 0 22166 0 [pid=335] vsize: 89244 Current children cumulated CPU time (s) 988.87 Current children cumulated vsize (Kb) 91368 [startup+1000.09 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24187 0 0 0 99765 122 0 0 25 0 1 0 1797441917 91709440 21019 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22390 21019 145 145 0 22245 0 [pid=335] vsize: 89560 Current children cumulated CPU time (s) 998.87 Current children cumulated vsize (Kb) 91684 [startup+1010.09 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24269 0 0 0 100763 123 0 0 25 0 1 0 1797441917 92057600 21101 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22475 21101 145 145 0 22330 0 [pid=335] vsize: 89900 Current children cumulated CPU time (s) 1008.86 Current children cumulated vsize (Kb) 92024 [startup+1020.09 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24366 0 0 0 101762 123 0 0 25 0 1 0 1797441917 92405760 21198 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22560 21198 145 145 0 22415 0 [pid=335] vsize: 90240 Current children cumulated CPU time (s) 1018.85 Current children cumulated vsize (Kb) 92364 [startup+1030.09 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24432 0 0 0 102761 124 0 0 25 0 1 0 1797441917 92659712 21264 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22622 21264 145 145 0 22477 0 [pid=335] vsize: 90488 Current children cumulated CPU time (s) 1028.85 Current children cumulated vsize (Kb) 92612 [startup+1040.09 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24496 0 0 0 103760 125 0 0 25 0 1 0 1797441917 92913664 21328 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22684 21328 145 145 0 22539 0 [pid=335] vsize: 90736 Current children cumulated CPU time (s) 1038.85 Current children cumulated vsize (Kb) 92860 [startup+1050.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24563 0 0 0 104759 125 0 0 25 0 1 0 1797441917 93179904 21395 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22749 21395 145 145 0 22604 0 [pid=335] vsize: 90996 Current children cumulated CPU time (s) 1048.84 Current children cumulated vsize (Kb) 93120 [startup+1060.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24584 0 0 0 105759 125 0 0 25 0 1 0 1797441917 93261824 21416 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22769 21416 145 145 0 22624 0 [pid=335] vsize: 91076 Current children cumulated CPU time (s) 1058.84 Current children cumulated vsize (Kb) 93200 [startup+1070.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24683 0 0 0 106759 126 0 0 25 0 1 0 1797441917 93749248 21515 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22888 21515 145 145 0 22743 0 [pid=335] vsize: 91552 Current children cumulated CPU time (s) 1068.85 Current children cumulated vsize (Kb) 93676 [startup+1080.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24729 0 0 0 107759 126 0 0 25 0 1 0 1797441917 93970432 21561 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 22942 21561 145 145 0 22797 0 [pid=335] vsize: 91768 Current children cumulated CPU time (s) 1078.85 Current children cumulated vsize (Kb) 93892 [startup+1090.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24791 0 0 0 108759 126 0 0 25 0 1 0 1797441917 94212096 21623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23001 21623 145 145 0 22856 0 [pid=335] vsize: 92004 Current children cumulated CPU time (s) 1088.85 Current children cumulated vsize (Kb) 94128 [startup+1100.1 s] Raw data (loadavg): 0.99 0.99 0.92 1/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) T 331 331 30740 0 -1 0 24867 0 0 0 109758 127 0 0 25 0 1 0 1797441917 94556160 21699 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/335/statm): 23085 21699 145 145 0 22940 0 [pid=335] vsize: 92340 Current children cumulated CPU time (s) 1098.85 Current children cumulated vsize (Kb) 94464 [startup+1110.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24928 0 0 0 110757 127 0 0 25 0 1 0 1797441917 94801920 21760 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23145 21760 145 145 0 23000 0 [pid=335] vsize: 92580 Current children cumulated CPU time (s) 1108.84 Current children cumulated vsize (Kb) 94704 [startup+1120.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 24979 0 0 0 111756 128 0 0 25 0 1 0 1797441917 95019008 21811 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23198 21811 145 145 0 23053 0 [pid=335] vsize: 92792 Current children cumulated CPU time (s) 1118.84 Current children cumulated vsize (Kb) 94916 [startup+1130.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25031 0 0 0 112756 128 0 0 25 0 1 0 1797441917 95248384 21863 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23254 21863 145 145 0 23109 0 [pid=335] vsize: 93016 Current children cumulated CPU time (s) 1128.84 Current children cumulated vsize (Kb) 95140 [startup+1140.1 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25072 0 0 0 113755 128 0 0 25 0 1 0 1797441917 95416320 21904 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23295 21904 145 145 0 23150 0 [pid=335] vsize: 93180 Current children cumulated CPU time (s) 1138.83 Current children cumulated vsize (Kb) 95304 [startup+1150.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25110 0 0 0 114755 129 0 0 25 0 1 0 1797441917 95555584 21942 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23329 21942 145 145 0 23184 0 [pid=335] vsize: 93316 Current children cumulated CPU time (s) 1148.84 Current children cumulated vsize (Kb) 95440 [startup+1160.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25160 0 0 0 115754 129 0 0 25 0 1 0 1797441917 95760384 21992 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23379 21992 145 145 0 23234 0 [pid=335] vsize: 93516 Current children cumulated CPU time (s) 1158.83 Current children cumulated vsize (Kb) 95640 [startup+1170.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25235 0 0 0 116753 130 0 0 25 0 1 0 1797441917 96079872 22067 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23457 22067 145 145 0 23312 0 [pid=335] vsize: 93828 Current children cumulated CPU time (s) 1168.83 Current children cumulated vsize (Kb) 95952 [startup+1180.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25277 0 0 0 117752 130 0 0 25 0 1 0 1797441917 96256000 22109 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23500 22109 145 145 0 23355 0 [pid=335] vsize: 94000 Current children cumulated CPU time (s) 1178.82 Current children cumulated vsize (Kb) 96124 [startup+1190.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25343 0 0 0 118751 130 0 0 25 0 1 0 1797441917 96518144 22175 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23564 22175 145 145 0 23419 0 [pid=335] vsize: 94256 Current children cumulated CPU time (s) 1188.81 Current children cumulated vsize (Kb) 96380 [startup+1200.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25401 0 0 0 119750 130 0 0 25 0 1 0 1797441917 96747520 22233 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23620 22233 145 145 0 23475 0 [pid=335] vsize: 94480 Current children cumulated CPU time (s) 1198.8 Current children cumulated vsize (Kb) 96604 [startup+1210.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25459 0 0 0 120750 131 0 0 25 0 1 0 1797441917 96985088 22291 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23678 22291 145 145 0 23533 0 [pid=335] vsize: 94712 Current children cumulated CPU time (s) 1208.81 Current children cumulated vsize (Kb) 96836 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.99 0.92 2/57 335 Raw data (/proc/331/stat): 331 (minisat+_script) S 330 331 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797441912 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/331/statm): 531 226 485 147 0 384 0 [pid=331] vsize: 2124 Raw data (/proc/335/stat): 335 (minisat+_64-bit) R 331 331 30740 0 -1 0 25459 0 0 0 120750 131 0 0 25 0 1 0 1797441917 96985088 22291 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/335/statm): 23678 22291 145 145 0 23533 0 [pid=335] vsize: 94712 Current children cumulated CPU time (s) 1208.81 Current children cumulated vsize (Kb) 96836 Sending SIGTERM to -331 Sleeping 2 seconds One traced child (pid=331) ended because it received signal 15 (SIGTERM) One traced child (pid=335) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.16 CPU time (s): 1208.86 CPU user time (s): 1207.5 CPU system time (s): 1.35879 CPU usage (%): 99.893 Max. virtual memory (cumulated for all children) (Kb): 96836
ERROR: no interpretation found !