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/miplib2003/normalized-mps-v2-13-7-mkc.opb
MD5SUM44934b498b6e9897bcf8e950d9d30136
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.32
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 6143

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        920716 kB
Buffers:          3304 kB
Cached:          82980 kB
SwapCached:        756 kB
Active:          19508 kB
Inactive:        69344 kB
HighTotal:      131008 kB
HighFree:        43848 kB
LowTotal:       903652 kB
LowFree:        876868 kB
SwapTotal:     2097892 kB
SwapFree:      2096608 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19336 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:07:03 (client local time) WITH STATUS 0 IN 1209.59 SECONDS
stats: 3305 7 1209.59 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/6528/stat): 6528 (minisat+_script) R 6527 6528 20728 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855409152 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6528/statm): 174 3 169 147 0 27 0
[pid=6528] 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=6529
New process pid=6530
New process pid=6531
execve syscall for /bin/sed executable
One traced child (pid=6530) 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=6531) exited with status: 0
One traced child (pid=6529) exited with status: 0
New process pid=6532
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-mkc.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.95 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 970 13 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221216 134677049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 12112

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 1970 14 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221220832 134676336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 12112

[startup+30.006 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 2969 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221120 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 12112

[startup+40.0057 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 3969 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221648 134600191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 39.84
Current children cumulated vsize (Kb) 12112

[startup+50.0074 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 4969 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221296 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 49.84
Current children cumulated vsize (Kb) 12112

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 5970 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221568 134677138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 12112

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 6970 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221472 134600228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 69.85
Current children cumulated vsize (Kb) 12112

[startup+80.0095 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 7970 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221920 134677042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 79.85
Current children cumulated vsize (Kb) 12112

[startup+90.0092 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 8970 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221296 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 89.85
Current children cumulated vsize (Kb) 12112

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 9970 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221364 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 99.85
Current children cumulated vsize (Kb) 12112

[startup+110.011 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 10970 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221472 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 109.85
Current children cumulated vsize (Kb) 12112

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6532
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 11971 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221220944 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 119.86
Current children cumulated vsize (Kb) 12112

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 6533
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 12971 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221220992 134676465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 129.86
Current children cumulated vsize (Kb) 12112

[startup+140.015 s]
Raw data (loadavg): 1.06 0.98 0.94 2/57 6583
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 13971 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221472 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 139.86
Current children cumulated vsize (Kb) 12112

[startup+150.015 s]
Raw data (loadavg): 1.05 0.98 0.94 2/57 6583
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 3777 0 0 0 14972 15 0 0 25 0 1 0 1855409157 10227712 2288 4294967295 134512640 135094434 3221224448 3221221724 134676331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 2497 2288 145 145 0 2352 0
[pid=6532] vsize: 9988
Current children cumulated CPU time (s) 149.87
Current children cumulated vsize (Kb) 12112

[startup+160.015 s]
Raw data (loadavg): 1.04 0.98 0.94 2/57 6583
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 8688 0 0 0 15950 30 0 0 25 0 1 0 1855409157 25575424 5877 4294967295 134512640 135094434 3221224448 3221221472 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6532/statm): 6244 5877 145 145 0 6099 0
[pid=6532] vsize: 24976
Current children cumulated CPU time (s) 159.8
Current children cumulated vsize (Kb) 27100

[startup+170.017 s]
Raw data (loadavg): 1.04 0.98 0.94 2/57 6583
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 8898 0 0 0 16948 32 0 0 25 0 1 0 1855409157 25575424 5877 4294967295 134512640 135094434 3221224448 3221220944 134677327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6532/statm): 6244 5877 145 145 0 6099 0
[pid=6532] vsize: 24976
Current children cumulated CPU time (s) 169.8
Current children cumulated vsize (Kb) 27100

[startup+180.018 s]
Raw data (loadavg): 1.03 0.98 0.94 2/57 6583
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 9129 0 0 0 17946 32 0 0 25 0 1 0 1855409157 25944064 5962 4294967295 134512640 135094434 3221224448 3221216352 134552178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 6334 5963 145 145 0 6189 0
[pid=6532] vsize: 25336
Current children cumulated CPU time (s) 179.78
Current children cumulated vsize (Kb) 27460

[startup+190.018 s]
Raw data (loadavg): 1.03 0.98 0.94 2/57 6583
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 16092 0 0 0 18877 66 0 0 25 0 1 0 1855409157 57634816 12924 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 14071 12924 145 145 0 13926 0
[pid=6532] vsize: 56284
Current children cumulated CPU time (s) 189.43
Current children cumulated vsize (Kb) 58408

[startup+200.019 s]
Raw data (loadavg): 1.02 0.98 0.94 2/57 6585
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 16493 0 0 0 19869 71 0 0 25 0 1 0 1855409157 59293696 13325 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 14476 13325 145 145 0 14331 0
[pid=6532] vsize: 57904
Current children cumulated CPU time (s) 199.4
Current children cumulated vsize (Kb) 60028

[startup+210.02 s]
Raw data (loadavg): 1.02 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 16698 0 0 0 20867 73 0 0 25 0 1 0 1855409157 60088320 13530 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 14670 13530 145 145 0 14525 0
[pid=6532] vsize: 58680
Current children cumulated CPU time (s) 209.4
Current children cumulated vsize (Kb) 60804

[startup+220.021 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 16780 0 0 0 21865 74 0 0 25 0 1 0 1855409157 60477440 13612 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 14765 13612 145 145 0 14620 0
[pid=6532] vsize: 59060
Current children cumulated CPU time (s) 219.39
Current children cumulated vsize (Kb) 61184

[startup+230.022 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 16984 0 0 0 22861 75 0 0 25 0 1 0 1855409157 61296640 13816 4294967295 134512640 135094434 3221224448 3221223152 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 14965 13816 145 145 0 14820 0
[pid=6532] vsize: 59860
Current children cumulated CPU time (s) 229.36
Current children cumulated vsize (Kb) 61984

[startup+240.023 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 17263 0 0 0 23856 78 0 0 25 0 1 0 1855409157 62414848 14095 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 15238 14095 145 145 0 15093 0
[pid=6532] vsize: 60952
Current children cumulated CPU time (s) 239.34
Current children cumulated vsize (Kb) 63076

[startup+250.023 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 17438 0 0 0 24854 79 0 0 25 0 1 0 1855409157 63115264 14270 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 15409 14270 145 145 0 15264 0
[pid=6532] vsize: 61636
Current children cumulated CPU time (s) 249.33
Current children cumulated vsize (Kb) 63760

[startup+260.024 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 17642 0 0 0 25850 80 0 0 25 0 1 0 1855409157 64065536 14474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 15641 14474 145 145 0 15496 0
[pid=6532] vsize: 62564
Current children cumulated CPU time (s) 259.3
Current children cumulated vsize (Kb) 64688

[startup+270.025 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 17885 0 0 0 26846 82 0 0 25 0 1 0 1855409157 65036288 14717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 15878 14717 145 145 0 15733 0
[pid=6532] vsize: 63512
Current children cumulated CPU time (s) 269.28
Current children cumulated vsize (Kb) 65636

[startup+280.025 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18111 0 0 0 27842 84 0 0 25 0 1 0 1855409157 65945600 14943 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16100 14943 145 145 0 15955 0
[pid=6532] vsize: 64400
Current children cumulated CPU time (s) 279.26
Current children cumulated vsize (Kb) 66524

[startup+290.026 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18237 0 0 0 28840 85 0 0 25 0 1 0 1855409157 66457600 15069 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16225 15069 145 145 0 16080 0
[pid=6532] vsize: 64900
Current children cumulated CPU time (s) 289.25
Current children cumulated vsize (Kb) 67024

[startup+300.027 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18356 0 0 0 29837 87 0 0 25 0 1 0 1855409157 66936832 15188 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16342 15188 145 145 0 16197 0
[pid=6532] vsize: 65368
Current children cumulated CPU time (s) 299.24
Current children cumulated vsize (Kb) 67492

[startup+310.028 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18495 0 0 0 30835 88 0 0 25 0 1 0 1855409157 67493888 15327 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16478 15327 145 145 0 16333 0
[pid=6532] vsize: 65912
Current children cumulated CPU time (s) 309.23
Current children cumulated vsize (Kb) 68036

[startup+320.029 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18621 0 0 0 31833 89 0 0 25 0 1 0 1855409157 68001792 15453 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16602 15453 145 145 0 16457 0
[pid=6532] vsize: 66408
Current children cumulated CPU time (s) 319.22
Current children cumulated vsize (Kb) 68532

[startup+330.03 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18752 0 0 0 32831 90 0 0 25 0 1 0 1855409157 68526080 15584 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16730 15584 145 145 0 16585 0
[pid=6532] vsize: 66920
Current children cumulated CPU time (s) 329.21
Current children cumulated vsize (Kb) 69044

[startup+340.031 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18868 0 0 0 33829 91 0 0 25 0 1 0 1855409157 69001216 15700 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16846 15700 145 145 0 16701 0
[pid=6532] vsize: 67384
Current children cumulated CPU time (s) 339.2
Current children cumulated vsize (Kb) 69508

[startup+350.031 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 18964 0 0 0 34828 91 0 0 25 0 1 0 1855409157 69410816 15796 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 16946 15796 145 145 0 16801 0
[pid=6532] vsize: 67784
Current children cumulated CPU time (s) 349.19
Current children cumulated vsize (Kb) 69908

[startup+360.032 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 19044 0 0 0 35827 92 0 0 25 0 1 0 1855409157 70000640 15876 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 17090 15876 145 145 0 16945 0
[pid=6532] vsize: 68360
Current children cumulated CPU time (s) 359.19
Current children cumulated vsize (Kb) 70484

[startup+370.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 19193 0 0 0 36825 93 0 0 25 0 1 0 1855409157 70610944 16025 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 17239 16025 145 145 0 17094 0
[pid=6532] vsize: 68956
Current children cumulated CPU time (s) 369.18
Current children cumulated vsize (Kb) 71080

[startup+380.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 19330 0 0 0 37823 94 0 0 25 0 1 0 1855409157 71176192 16162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 17377 16162 145 145 0 17232 0
[pid=6532] vsize: 69508
Current children cumulated CPU time (s) 379.17
Current children cumulated vsize (Kb) 71632

[startup+390.035 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 19569 0 0 0 38819 96 0 0 25 0 1 0 1855409157 72134656 16401 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 17611 16401 145 145 0 17466 0
[pid=6532] vsize: 70444
Current children cumulated CPU time (s) 389.15
Current children cumulated vsize (Kb) 72568

[startup+400.036 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 19741 0 0 0 39817 96 0 0 25 0 1 0 1855409157 72822784 16573 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 17779 16573 145 145 0 17634 0
[pid=6532] vsize: 71116
Current children cumulated CPU time (s) 399.13
Current children cumulated vsize (Kb) 73240

[startup+410.036 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 19892 0 0 0 40815 97 0 0 25 0 1 0 1855409157 73437184 16724 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 17929 16724 145 145 0 17784 0
[pid=6532] vsize: 71716
Current children cumulated CPU time (s) 409.12
Current children cumulated vsize (Kb) 73840

[startup+420.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 19968 0 0 0 41814 98 0 0 25 0 1 0 1855409157 73736192 16800 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18002 16800 145 145 0 17857 0
[pid=6532] vsize: 72008
Current children cumulated CPU time (s) 419.12
Current children cumulated vsize (Kb) 74132

[startup+430.038 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20062 0 0 0 42812 99 0 0 25 0 1 0 1855409157 74129408 16894 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18098 16894 145 145 0 17953 0
[pid=6532] vsize: 72392
Current children cumulated CPU time (s) 429.11
Current children cumulated vsize (Kb) 74516

[startup+440.039 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20157 0 0 0 43811 100 0 0 25 0 1 0 1855409157 74522624 16989 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18194 16989 145 145 0 18049 0
[pid=6532] vsize: 72776
Current children cumulated CPU time (s) 439.11
Current children cumulated vsize (Kb) 74900

[startup+450.039 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6587
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20230 0 0 0 44809 101 0 0 25 0 1 0 1855409157 74813440 17062 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18265 17062 145 145 0 18120 0
[pid=6532] vsize: 73060
Current children cumulated CPU time (s) 449.1
Current children cumulated vsize (Kb) 75184

[startup+460.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20300 0 0 0 45809 101 0 0 25 0 1 0 1855409157 75104256 17132 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18336 17132 145 145 0 18191 0
[pid=6532] vsize: 73344
Current children cumulated CPU time (s) 459.1
Current children cumulated vsize (Kb) 75468

[startup+470.041 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20375 0 0 0 46807 102 0 0 25 0 1 0 1855409157 75399168 17207 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18408 17207 145 145 0 18263 0
[pid=6532] vsize: 73632
Current children cumulated CPU time (s) 469.09
Current children cumulated vsize (Kb) 75756

[startup+480.041 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20480 0 0 0 47805 102 0 0 25 0 1 0 1855409157 75841536 17312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18516 17312 145 145 0 18371 0
[pid=6532] vsize: 74064
Current children cumulated CPU time (s) 479.07
Current children cumulated vsize (Kb) 76188

[startup+490.042 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20573 0 0 0 48804 103 0 0 25 0 1 0 1855409157 76230656 17405 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18611 17405 145 145 0 18466 0
[pid=6532] vsize: 74444
Current children cumulated CPU time (s) 489.07
Current children cumulated vsize (Kb) 76568

[startup+500.044 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20655 0 0 0 49803 103 0 0 25 0 1 0 1855409157 76566528 17487 4294967295 134512640 135094434 3221224448 3221223040 134556760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18693 17487 145 145 0 18548 0
[pid=6532] vsize: 74772
Current children cumulated CPU time (s) 499.06
Current children cumulated vsize (Kb) 76896

[startup+510.044 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20713 0 0 0 50802 104 0 0 25 0 1 0 1855409157 76824576 17545 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18756 17545 145 145 0 18611 0
[pid=6532] vsize: 75024
Current children cumulated CPU time (s) 509.06
Current children cumulated vsize (Kb) 77148

[startup+520.045 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20760 0 0 0 51801 104 0 0 25 0 1 0 1855409157 77012992 17592 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18802 17592 145 145 0 18657 0
[pid=6532] vsize: 75208
Current children cumulated CPU time (s) 519.05
Current children cumulated vsize (Kb) 77332

[startup+530.046 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20813 0 0 0 52800 105 0 0 25 0 1 0 1855409157 77217792 17645 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18852 17645 145 145 0 18707 0
[pid=6532] vsize: 75408
Current children cumulated CPU time (s) 529.05
Current children cumulated vsize (Kb) 77532

[startup+540.047 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20863 0 0 0 53800 105 0 0 25 0 1 0 1855409157 77418496 17695 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 18901 17695 145 145 0 18756 0
[pid=6532] vsize: 75604
Current children cumulated CPU time (s) 539.05
Current children cumulated vsize (Kb) 77728

[startup+550.047 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 20970 0 0 0 54799 106 0 0 25 0 1 0 1855409157 77856768 17802 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19008 17802 145 145 0 18863 0
[pid=6532] vsize: 76032
Current children cumulated CPU time (s) 549.05
Current children cumulated vsize (Kb) 78156

[startup+560.048 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21088 0 0 0 55797 107 0 0 25 0 1 0 1855409157 78327808 17920 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19123 17920 145 145 0 18978 0
[pid=6532] vsize: 76492
Current children cumulated CPU time (s) 559.04
Current children cumulated vsize (Kb) 78616

[startup+570.05 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21169 0 0 0 56797 107 0 0 25 0 1 0 1855409157 78659584 18001 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19204 18001 145 145 0 19059 0
[pid=6532] vsize: 76816
Current children cumulated CPU time (s) 569.04
Current children cumulated vsize (Kb) 78940

[startup+580.051 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21216 0 0 0 57797 108 0 0 25 0 1 0 1855409157 78848000 18048 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19250 18048 145 145 0 19105 0
[pid=6532] vsize: 77000
Current children cumulated CPU time (s) 579.05
Current children cumulated vsize (Kb) 79124

[startup+590.052 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21301 0 0 0 58795 109 0 0 25 0 1 0 1855409157 79179776 18133 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19331 18133 145 145 0 19186 0
[pid=6532] vsize: 77324
Current children cumulated CPU time (s) 589.04
Current children cumulated vsize (Kb) 79448

[startup+600.054 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21372 0 0 0 59794 110 0 0 25 0 1 0 1855409157 79470592 18204 4294967295 134512640 135094434 3221224448 3221223152 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19402 18204 145 145 0 19257 0
[pid=6532] vsize: 77608
Current children cumulated CPU time (s) 599.04
Current children cumulated vsize (Kb) 79732

[startup+610.054 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21450 0 0 0 60794 110 0 0 25 0 1 0 1855409157 79806464 18282 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19484 18282 145 145 0 19339 0
[pid=6532] vsize: 77936
Current children cumulated CPU time (s) 609.04
Current children cumulated vsize (Kb) 80060

[startup+620.055 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21526 0 0 0 61793 111 0 0 25 0 1 0 1855409157 80134144 18358 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19564 18358 145 145 0 19419 0
[pid=6532] vsize: 78256
Current children cumulated CPU time (s) 619.04
Current children cumulated vsize (Kb) 80380

[startup+630.056 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21603 0 0 0 62792 111 0 0 25 0 1 0 1855409157 80420864 18435 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19634 18435 145 145 0 19489 0
[pid=6532] vsize: 78536
Current children cumulated CPU time (s) 629.03
Current children cumulated vsize (Kb) 80660

[startup+640.057 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21672 0 0 0 63791 111 0 0 25 0 1 0 1855409157 80723968 18504 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19708 18504 145 145 0 19563 0
[pid=6532] vsize: 78832
Current children cumulated CPU time (s) 639.02
Current children cumulated vsize (Kb) 80956

[startup+650.057 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21733 0 0 0 64790 112 0 0 25 0 1 0 1855409157 80965632 18565 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19767 18565 145 145 0 19622 0
[pid=6532] vsize: 79068
Current children cumulated CPU time (s) 649.02
Current children cumulated vsize (Kb) 81192

[startup+660.058 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21802 0 0 0 65789 113 0 0 25 0 1 0 1855409157 81252352 18634 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19837 18634 145 145 0 19692 0
[pid=6532] vsize: 79348
Current children cumulated CPU time (s) 659.02
Current children cumulated vsize (Kb) 81472

[startup+670.06 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21871 0 0 0 66788 113 0 0 25 0 1 0 1855409157 81522688 18703 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 19903 18703 145 145 0 19758 0
[pid=6532] vsize: 79612
Current children cumulated CPU time (s) 669.01
Current children cumulated vsize (Kb) 81736

[startup+680.06 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 21986 0 0 0 67785 114 0 0 25 0 1 0 1855409157 81936384 18818 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20004 18818 145 145 0 19859 0
[pid=6532] vsize: 80016
Current children cumulated CPU time (s) 678.99
Current children cumulated vsize (Kb) 82140

[startup+690.06 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22140 0 0 0 68783 115 0 0 25 0 1 0 1855409157 82604032 18972 4294967295 134512640 135094434 3221224448 3221223108 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20167 18972 145 145 0 20022 0
[pid=6532] vsize: 80668
Current children cumulated CPU time (s) 688.98
Current children cumulated vsize (Kb) 82792

[startup+700.062 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22161 0 0 0 69782 116 0 0 25 0 1 0 1855409157 82685952 18993 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20187 18993 145 145 0 20042 0
[pid=6532] vsize: 80748
Current children cumulated CPU time (s) 698.98
Current children cumulated vsize (Kb) 82872

[startup+710.062 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22218 0 0 0 70782 116 0 0 25 0 1 0 1855409157 83468288 19050 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20378 19050 145 145 0 20233 0
[pid=6532] vsize: 81512
Current children cumulated CPU time (s) 708.98
Current children cumulated vsize (Kb) 83636

[startup+720.064 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22277 0 0 0 71781 116 0 0 25 0 1 0 1855409157 83730432 19109 4294967295 134512640 135094434 3221224448 3221223040 134552168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20442 19109 145 145 0 20297 0
[pid=6532] vsize: 81768
Current children cumulated CPU time (s) 718.97
Current children cumulated vsize (Kb) 83892

[startup+730.065 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22335 0 0 0 72781 117 0 0 25 0 1 0 1855409157 83959808 19167 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20498 19167 145 145 0 20353 0
[pid=6532] vsize: 81992
Current children cumulated CPU time (s) 728.98
Current children cumulated vsize (Kb) 84116

[startup+740.066 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22404 0 0 0 73779 118 0 0 25 0 1 0 1855409157 84234240 19236 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20565 19236 145 145 0 20420 0
[pid=6532] vsize: 82260
Current children cumulated CPU time (s) 738.97
Current children cumulated vsize (Kb) 84384

[startup+750.066 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22459 0 0 0 74778 118 0 0 25 0 1 0 1855409157 84451328 19291 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20618 19291 145 145 0 20473 0
[pid=6532] vsize: 82472
Current children cumulated CPU time (s) 748.96
Current children cumulated vsize (Kb) 84596

[startup+760.067 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22511 0 0 0 75777 119 0 0 25 0 1 0 1855409157 84672512 19343 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20672 19343 145 145 0 20527 0
[pid=6532] vsize: 82688
Current children cumulated CPU time (s) 758.96
Current children cumulated vsize (Kb) 84812

[startup+770.069 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22561 0 0 0 76777 120 0 0 25 0 1 0 1855409157 84889600 19393 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20725 19393 145 145 0 20580 0
[pid=6532] vsize: 82900
Current children cumulated CPU time (s) 768.97
Current children cumulated vsize (Kb) 85024

[startup+780.069 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22612 0 0 0 77777 120 0 0 25 0 1 0 1855409157 85118976 19444 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20781 19444 145 145 0 20636 0
[pid=6532] vsize: 83124
Current children cumulated CPU time (s) 778.97
Current children cumulated vsize (Kb) 85248

[startup+790.07 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22682 0 0 0 78775 120 0 0 25 0 1 0 1855409157 85389312 19514 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20847 19514 145 145 0 20702 0
[pid=6532] vsize: 83388
Current children cumulated CPU time (s) 788.95
Current children cumulated vsize (Kb) 85512

[startup+800.072 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22765 0 0 0 79772 123 0 0 25 0 1 0 1855409157 85757952 19597 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 20937 19597 145 145 0 20792 0
[pid=6532] vsize: 83748
Current children cumulated CPU time (s) 798.95
Current children cumulated vsize (Kb) 85872

[startup+810.072 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22825 0 0 0 80771 124 0 0 25 0 1 0 1855409157 86020096 19657 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21001 19657 145 145 0 20856 0
[pid=6532] vsize: 84004
Current children cumulated CPU time (s) 808.95
Current children cumulated vsize (Kb) 86128

[startup+820.074 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22898 0 0 0 81771 124 0 0 25 0 1 0 1855409157 86335488 19730 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21078 19730 145 145 0 20933 0
[pid=6532] vsize: 84312
Current children cumulated CPU time (s) 818.95
Current children cumulated vsize (Kb) 86436

[startup+830.075 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 22964 0 0 0 82769 126 0 0 25 0 1 0 1855409157 86601728 19796 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21143 19796 145 145 0 20998 0
[pid=6532] vsize: 84572
Current children cumulated CPU time (s) 828.95
Current children cumulated vsize (Kb) 86696

[startup+840.075 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23021 0 0 0 83768 126 0 0 25 0 1 0 1855409157 86835200 19853 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21200 19853 145 145 0 21055 0
[pid=6532] vsize: 84800
Current children cumulated CPU time (s) 838.94
Current children cumulated vsize (Kb) 86924

[startup+850.076 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23085 0 0 0 84767 127 0 0 25 0 1 0 1855409157 87093248 19917 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21263 19917 145 145 0 21118 0
[pid=6532] vsize: 85052
Current children cumulated CPU time (s) 848.94
Current children cumulated vsize (Kb) 87176

[startup+860.077 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23239 0 0 0 85764 128 0 0 25 0 1 0 1855409157 87711744 20071 4294967295 134512640 135094434 3221224448 3221223152 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21414 20071 145 145 0 21269 0
[pid=6532] vsize: 85656
Current children cumulated CPU time (s) 858.92
Current children cumulated vsize (Kb) 87780

[startup+870.078 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23274 0 0 0 86763 128 0 0 25 0 1 0 1855409157 87871488 20106 4294967295 134512640 135094434 3221224448 3221223104 134558026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21453 20106 145 145 0 21308 0
[pid=6532] vsize: 85812
Current children cumulated CPU time (s) 868.91
Current children cumulated vsize (Kb) 87936

[startup+880.079 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23323 0 0 0 87762 129 0 0 25 0 1 0 1855409157 88068096 20155 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21501 20155 145 145 0 21356 0
[pid=6532] vsize: 86004
Current children cumulated CPU time (s) 878.91
Current children cumulated vsize (Kb) 88128

[startup+890.08 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23379 0 0 0 88762 129 0 0 25 0 1 0 1855409157 88305664 20211 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21559 20211 145 145 0 21414 0
[pid=6532] vsize: 86236
Current children cumulated CPU time (s) 888.91
Current children cumulated vsize (Kb) 88360

[startup+900.082 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23439 0 0 0 89762 129 0 0 25 0 1 0 1855409157 88559616 20271 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21621 20271 145 145 0 21476 0
[pid=6532] vsize: 86484
Current children cumulated CPU time (s) 898.91
Current children cumulated vsize (Kb) 88608

[startup+910.082 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23505 0 0 0 90761 131 0 0 25 0 1 0 1855409157 88821760 20337 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21685 20337 145 145 0 21540 0
[pid=6532] vsize: 86740
Current children cumulated CPU time (s) 908.92
Current children cumulated vsize (Kb) 88864

[startup+920.089 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23570 0 0 0 91760 131 0 0 25 0 1 0 1855409157 89133056 20402 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21761 20402 145 145 0 21616 0
[pid=6532] vsize: 87044
Current children cumulated CPU time (s) 918.91
Current children cumulated vsize (Kb) 89168

[startup+930.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23627 0 0 0 92759 132 0 0 25 0 1 0 1855409157 89350144 20459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21814 20459 145 145 0 21669 0
[pid=6532] vsize: 87256
Current children cumulated CPU time (s) 928.91
Current children cumulated vsize (Kb) 89380

[startup+940.089 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23688 0 0 0 93791 132 0 0 25 0 1 0 1855409157 89649152 20520 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21887 20520 145 145 0 21742 0
[pid=6532] vsize: 87548
Current children cumulated CPU time (s) 939.23
Current children cumulated vsize (Kb) 89672

[startup+950.419 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23728 0 0 0 94802 132 0 0 25 0 1 0 1855409157 89808896 20560 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21926 20560 145 145 0 21781 0
[pid=6532] vsize: 87704
Current children cumulated CPU time (s) 949.34
Current children cumulated vsize (Kb) 89828

[startup+960.533 s]
Raw data (loadavg): 1.00 0.98 0.94 1/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) T 6528 6528 20728 0 -1 0 23782 0 0 0 95810 133 0 0 25 0 1 0 1855409157 90009600 20614 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6532/statm): 21975 20614 145 145 0 21830 0
[pid=6532] vsize: 87900
Current children cumulated CPU time (s) 959.43
Current children cumulated vsize (Kb) 90024

[startup+970.619 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23857 0 0 0 96810 133 0 0 25 0 1 0 1855409157 90345472 20689 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22057 20689 145 145 0 21912 0
[pid=6532] vsize: 88228
Current children cumulated CPU time (s) 969.43
Current children cumulated vsize (Kb) 90352

[startup+980.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23912 0 0 0 97809 134 0 0 25 0 1 0 1855409157 90607616 20744 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22121 20744 145 145 0 21976 0
[pid=6532] vsize: 88484
Current children cumulated CPU time (s) 979.43
Current children cumulated vsize (Kb) 90608

[startup+990.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 23978 0 0 0 98808 134 0 0 25 0 1 0 1855409157 90865664 20810 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22184 20810 145 145 0 22039 0
[pid=6532] vsize: 88736
Current children cumulated CPU time (s) 989.42
Current children cumulated vsize (Kb) 90860

[startup+1000.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24036 0 0 0 99807 134 0 0 25 0 1 0 1855409157 91066368 20868 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22233 20868 145 145 0 22088 0
[pid=6532] vsize: 88932
Current children cumulated CPU time (s) 999.41
Current children cumulated vsize (Kb) 91056

[startup+1010.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24091 0 0 0 100807 134 0 0 25 0 1 0 1855409157 91303936 20923 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22291 20923 145 145 0 22146 0
[pid=6532] vsize: 89164
Current children cumulated CPU time (s) 1009.41
Current children cumulated vsize (Kb) 91288

[startup+1020.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24163 0 0 0 101806 135 0 0 25 0 1 0 1855409157 91619328 20995 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22368 20995 145 145 0 22223 0
[pid=6532] vsize: 89472
Current children cumulated CPU time (s) 1019.41
Current children cumulated vsize (Kb) 91596

[startup+1030.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24235 0 0 0 102805 136 0 0 25 0 1 0 1855409157 91901952 21067 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22437 21067 145 145 0 22292 0
[pid=6532] vsize: 89748
Current children cumulated CPU time (s) 1029.41
Current children cumulated vsize (Kb) 91872

[startup+1040.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24333 0 0 0 103804 136 0 0 25 0 1 0 1855409157 92270592 21165 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22527 21165 145 145 0 22382 0
[pid=6532] vsize: 90108
Current children cumulated CPU time (s) 1039.4
Current children cumulated vsize (Kb) 92232

[startup+1050.62 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24402 0 0 0 104803 137 0 0 25 0 1 0 1855409157 92540928 21234 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22593 21234 145 145 0 22448 0
[pid=6532] vsize: 90372
Current children cumulated CPU time (s) 1049.4
Current children cumulated vsize (Kb) 92496

[startup+1060.63 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24468 0 0 0 105802 137 0 0 25 0 1 0 1855409157 92803072 21300 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22657 21300 145 145 0 22512 0
[pid=6532] vsize: 90628
Current children cumulated CPU time (s) 1059.39
Current children cumulated vsize (Kb) 92752

[startup+1070.63 s]
Raw data (loadavg): 1.08 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) T 6528 6528 20728 0 -1 0 24526 0 0 0 106820 138 0 0 25 0 1 0 1855409157 93036544 21358 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22714 21358 145 145 0 22569 0
[pid=6532] vsize: 90856
Current children cumulated CPU time (s) 1069.58
Current children cumulated vsize (Kb) 92980

[startup+1081.02 s]
Raw data (loadavg): 1.07 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24584 0 0 0 107818 139 0 0 25 0 1 0 1855409157 93261824 21416 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22769 21416 145 145 0 22624 0
[pid=6532] vsize: 91076
Current children cumulated CPU time (s) 1079.57
Current children cumulated vsize (Kb) 93200

[startup+1091.02 s]
Raw data (loadavg): 1.06 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24604 0 0 0 108818 139 0 0 25 0 1 0 1855409157 93343744 21436 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22789 21436 145 145 0 22644 0
[pid=6532] vsize: 91156
Current children cumulated CPU time (s) 1089.57
Current children cumulated vsize (Kb) 93280

[startup+1101.02 s]
Raw data (loadavg): 1.05 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24702 0 0 0 109817 140 0 0 25 0 1 0 1855409157 93827072 21534 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22907 21534 145 145 0 22762 0
[pid=6532] vsize: 91628
Current children cumulated CPU time (s) 1099.57
Current children cumulated vsize (Kb) 93752

[startup+1111.02 s]
Raw data (loadavg): 1.04 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24748 0 0 0 110817 140 0 0 25 0 1 0 1855409157 94044160 21580 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 22960 21580 145 145 0 22815 0
[pid=6532] vsize: 91840
Current children cumulated CPU time (s) 1109.57
Current children cumulated vsize (Kb) 93964

[startup+1121.02 s]
Raw data (loadavg): 1.03 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24821 0 0 0 111816 141 0 0 25 0 1 0 1855409157 94330880 21653 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23030 21653 145 145 0 22885 0
[pid=6532] vsize: 92120
Current children cumulated CPU time (s) 1119.57
Current children cumulated vsize (Kb) 94244

[startup+1131.02 s]
Raw data (loadavg): 1.03 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24889 0 0 0 112815 141 0 0 25 0 1 0 1855409157 94646272 21721 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23107 21721 145 145 0 22962 0
[pid=6532] vsize: 92428
Current children cumulated CPU time (s) 1129.56
Current children cumulated vsize (Kb) 94552

[startup+1141.02 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24944 0 0 0 113814 142 0 0 25 0 1 0 1855409157 94863360 21776 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23160 21776 145 145 0 23015 0
[pid=6532] vsize: 92640
Current children cumulated CPU time (s) 1139.56
Current children cumulated vsize (Kb) 94764

[startup+1151.02 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 24993 0 0 0 114814 142 0 0 25 0 1 0 1855409157 95076352 21825 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23212 21825 145 145 0 23067 0
[pid=6532] vsize: 92848
Current children cumulated CPU time (s) 1149.56
Current children cumulated vsize (Kb) 94972

[startup+1161.02 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 25041 0 0 0 115813 143 0 0 25 0 1 0 1855409157 95289344 21873 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23264 21873 145 145 0 23119 0
[pid=6532] vsize: 93056
Current children cumulated CPU time (s) 1159.56
Current children cumulated vsize (Kb) 95180

[startup+1171.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 25081 0 0 0 116813 143 0 0 25 0 1 0 1855409157 95444992 21913 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23302 21913 145 145 0 23157 0
[pid=6532] vsize: 93208
Current children cumulated CPU time (s) 1169.56
Current children cumulated vsize (Kb) 95332

[startup+1181.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 25115 0 0 0 117812 143 0 0 25 0 1 0 1855409157 95576064 21947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23334 21947 145 145 0 23189 0
[pid=6532] vsize: 93336
Current children cumulated CPU time (s) 1179.55
Current children cumulated vsize (Kb) 95460

[startup+1191.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 25167 0 0 0 118811 144 0 0 25 0 1 0 1855409157 95801344 21999 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23389 21999 145 145 0 23244 0
[pid=6532] vsize: 93556
Current children cumulated CPU time (s) 1189.55
Current children cumulated vsize (Kb) 95680

[startup+1201.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 25241 0 0 0 119810 145 0 0 25 0 1 0 1855409157 96104448 22073 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23463 22073 145 145 0 23318 0
[pid=6532] vsize: 93852
Current children cumulated CPU time (s) 1199.55
Current children cumulated vsize (Kb) 95976

[startup+1211.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 25282 0 0 0 120809 145 0 0 25 0 1 0 1855409157 96276480 22114 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23505 22114 145 145 0 23360 0
[pid=6532] vsize: 94020
Current children cumulated CPU time (s) 1209.54
Current children cumulated vsize (Kb) 96144



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1211.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 6589
Raw data (/proc/6528/stat): 6528 (minisat+_script) S 6527 6528 20728 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855409152 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6528/statm): 531 226 485 147 0 384 0
[pid=6528] vsize: 2124
Raw data (/proc/6532/stat): 6532 (minisat+_64-bit) R 6528 6528 20728 0 -1 0 25282 0 0 0 120809 145 0 0 25 0 1 0 1855409157 96276480 22114 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6532/statm): 23505 22114 145 145 0 23360 0
[pid=6532] vsize: 94020
Current children cumulated CPU time (s) 1209.54
Current children cumulated vsize (Kb) 96144

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

Child status: 0
Real time (s): 1211.07
CPU time (s): 1209.59
CPU user time (s): 1208.1
CPU system time (s): 1.49777
CPU usage (%): 99.8781
Max. virtual memory (cumulated for all children) (Kb): 96144

Verifier Data

ERROR: no interpretation found !