Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mkc.opb
MD5SUMb9e9aa470fdb3341d7e10860fcc70cec
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers30
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.24
Number of variables5363
Total number of constraints8734
Number of constraints which are clauses2977
Number of constraints which are cardinality constraints (but not clauses)5731
Number of constraints which are nor clauses,nor cardinality constraints26
Minimum length of a constraint1
Maximum length of a constraint2942

Trace number 6218

Launcher Data

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

Solver Data

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 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/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

Verifier Data

ERROR: no interpretation found !