Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-danoint.opb
MD5SUMcdd5642b047e784e87a00fe758efc418
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 30
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 1073741823
Number of bits of the sum of numbers in the objective function 30
Biggest number in a constraint 13421772800
Number of bits of the biggest number in a constraint 34
Biggest sum of numbers in a constraint 53690300878
Number of bits of the biggest sum of numbers36
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables13898
Total number of constraints728
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)72
Number of constraints which are nor clauses,nor cardinality constraints656
Minimum length of a constraint1
Maximum length of a constraint1500

Trace number 4507

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        878352 kB
Buffers:         36800 kB
Cached:          92784 kB
SwapCached:       1044 kB
Active:          65548 kB
Inactive:        66796 kB
HighTotal:      131008 kB
HighFree:        42560 kB
LowTotal:       903652 kB
LowFree:        835792 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            18408 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:05:57 (client local time) WITH STATUS 0 IN 1207.59 SECONDS
stats: 2966 7 1207.59 0

Solver Data

c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: pppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssss
c ---[ 833]---> BDD-cost:   15
c ---[ 832]---> BDD-cost:   16
c ---[ 831]---> BDD-cost:   16
c ---[ 828]---> BDD-cost:   16
c ---[ 827]---> BDD-cost:   16
c ---[ 825]---> Adder-cost: 400   maxlim: 645113   bits: 21/20
c ---[ 823]---> Adder-cost: 400   maxlim: 648185   bits: 21/20
c ---[ 821]---> Adder-cost: 394   maxlim: 707577   bits: 21/20
c ---[ 819]---> Adder-cost: 394   maxlim: 708601   bits: 21/20
c ---[ 817]---> Adder-cost: 394   maxlim: 707577   bits: 21/20
c ---[ 815]---> Adder-cost: 400   maxlim: 649209   bits: 21/20
c ---[ 813]---> Adder-cost: 394   maxlim: 707577   bits: 21/20
c ---[ 811]---> Adder-cost: 408   maxlim: 903161   bits: 21/20
c ---[ 809]---> Adder-cost: 408   maxlim: 902137   bits: 21/20
c ---[ 807]---> Adder-cost: 408   maxlim: 904185   bits: 21/20
c ---[ 805]---> Adder-cost: 408   maxlim: 905209   bits: 21/20
c ---[ 803]---> Adder-cost: 408   maxlim: 908281   bits: 21/20
c ---[ 801]---> Adder-cost: 408   maxlim: 908281   bits: 21/20
c ---[ 799]---> Adder-cost: 408   maxlim: 908281   bits: 21/20
c ---[ 797]---> Adder-cost: 384   maxlim: 445433   bits: 20/19
c ---[ 795]---> Adder-cost: 384   maxlim: 449529   bits: 20/19
c ---[ 793]---> Adder-cost: 384   maxlim: 447481   bits: 20/19
c ---[ 791]---> Adder-cost: 384   maxlim: 452601   bits: 20/19
c ---[ 789]---> Adder-cost: 384   maxlim: 453625   bits: 20/19
c ---[ 787]---> Adder-cost: 384   maxlim: 447481   bits: 20/19
c ---[ 785]---> Adder-cost: 384   maxlim: 450553   bits: 20/19
c ---[ 783]---> Adder-cost: 384   maxlim: 451577   bits: 20/19
c ---[ 781]---> Adder-cost: 384   maxlim: 450553   bits: 20/19
c ---[ 779]---> Adder-cost: 384   maxlim: 443385   bits: 20/19
c ---[ 777]---> Adder-cost: 384   maxlim: 451577   bits: 20/19
c ---[ 775]---> Adder-cost: 384   maxlim: 452601   bits: 20/19
c ---[ 773]---> Adder-cost: 384   maxlim: 447481   bits: 20/19
c ---[ 771]---> Adder-cost: 384   maxlim: 449529   bits: 20/19
c ---[ 769]---> Adder-cost: 402   maxlim: 712697   bits: 21/20
c ---[ 767]---> Adder-cost: 394   maxlim: 774137   bits: 21/20
c ---[ 765]---> Adder-cost: 394   maxlim: 774137   bits: 21/20
c ---[ 763]---> Adder-cost: 402   maxlim: 711673   bits: 21/20
c ---[ 761]---> Adder-cost: 402   maxlim: 711673   bits: 21/20
c ---[ 759]---> Adder-cost: 394   maxlim: 772089   bits: 21/20
c ---[ 757]---> Adder-cost: 402   maxlim: 709625   bits: 21/20
c ---[ 755]---> Adder-cost: 395   maxlim: 519161   bits: 20/19
c ---[ 753]---> Adder-cost: 386   maxlim: 578553   bits: 20/20
c ---[ 751]---> Adder-cost: 386   maxlim: 578553   bits: 20/20
c ---[ 749]---> Adder-cost: 386   maxlim: 582649   bits: 20/20
c ---[ 747]---> Adder-cost: 386   maxlim: 580601   bits: 20/20
c ---[ 745]---> Adder-cost: 386   maxlim: 574457   bits: 20/20
c ---[ 743]---> Adder-cost: 386   maxlim: 577529   bits: 20/20
c ---[ 741]---> Adder-cost: 384   maxlim: 518137   bits: 20/19
c ---[ 739]---> Adder-cost: 384   maxlim: 515065   bits: 20/19
c ---[ 737]---> Adder-cost: 384   maxlim: 517113   bits: 20/19
c ---[ 735]---> Adder-cost: 384   maxlim: 509945   bits: 20/19
c ---[ 733]---> Adder-cost: 384   maxlim: 514041   bits: 20/19
c ---[ 731]---> Adder-cost: 384   maxlim: 511993   bits: 20/19
c ---[ 729]---> Adder-cost: 384   maxlim: 517113   bits: 20/19
c ---[ 727]---> Adder-cost: 384   maxlim: 447481   bits: 20/19
c ---[ 725]---> Adder-cost: 384   maxlim: 451577   bits: 20/19
c ---[ 723]---> Adder-cost: 384   maxlim: 450553   bits: 20/19
c ---[ 721]---> Adder-cost: 384   maxlim: 452601   bits: 20/19
c ---[ 719]---> Adder-cost: 384   maxlim: 448505   bits: 20/19
c ---[ 717]---> Adder-cost: 384   maxlim: 453625   bits: 20/19
c ---[ 715]---> Adder-cost: 384   maxlim: 444409   bits: 20/19
c ---[ 714]---> BDD-cost:  145
c ---[ 713]---> BDD-cost:  145
c ---[ 712]---> BDD-cost:  145
c ---[ 711]---> BDD-cost:  145
c ---[ 710]---> BDD-cost:  145
c ---[ 709]---> BDD-cost:  145
c ---[ 708]---> BDD-cost:  145
c ---[ 707]---> BDD-cost:  145
c ---[ 706]---> BDD-cost:  145
c ---[ 705]---> BDD-cost:  145
c ---[ 704]---> BDD-cost:  145
c ---[ 703]---> BDD-cost:  145
c ---[ 702]---> BDD-cost:  145
c ---[ 701]---> BDD-cost:  145
c ---[ 700]---> BDD-cost:  145
c ---[ 699]---> BDD-cost:  145
c ---[ 698]---> BDD-cost:  145
c ---[ 697]---> BDD-cost:  145
c ---[ 696]---> BDD-cost:  145
c ---[ 695]---> BDD-cost:  145
c ---[ 694]---> BDD-cost:  145
c ---[ 693]---> BDD-cost:  145
c ---[ 692]---> BDD-cost:  145
c ---[ 691]---> BDD-cost:  145
c ---[ 690]---> BDD-cost:  145
c ---[ 689]---> BDD-cost:  145
c ---[ 688]---> BDD-cost:  145
c ---[ 687]---> BDD-cost:  145
c ---[ 686]---> BDD-cost:  145
c ---[ 685]---> BDD-cost:  145
c ---[ 684]---> BDD-cost:  145
c ---[ 683]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  145
c ---[ 681]---> BDD-cost:  145
c ---[ 680]---> BDD-cost:  145
c ---[ 679]---> BDD-cost:  145
c ---[ 678]---> BDD-cost:  145
c ---[ 677]---> BDD-cost:  145
c ---[ 676]---> BDD-cost:  145
c ---[ 675]---> BDD-cost:  145
c ---[ 674]---> BDD-cost:  145
c ---[ 673]---> BDD-cost:  145
c ---[ 672]---> BDD-cost:  145
c ---[ 671]---> BDD-cost:  145
c ---[ 670]---> BDD-cost:  145
c ---[ 669]---> BDD-cost:  145
c ---[ 668]---> BDD-cost:  145
c ---[ 667]---> BDD-cost:  145
c ---[ 666]---> BDD-cost:  145
c ---[ 665]---> BDD-cost:  145
c ---[ 664]---> BDD-cost:  145
c ---[ 663]---> BDD-cost:  145
c ---[ 662]---> BDD-cost:  145
c ---[ 661]---> BDD-cost:  145
c ---[ 660]---> BDD-cost:  145
c ---[ 659]---> BDD-cost:  145
c ---[ 657]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost: 2183     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost: 2183     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost: 2183     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> Sorter-cost: 2183     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 637]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 621]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 619]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 617]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 607]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 605]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 583]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 579]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 577]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 571]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 567]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> Sorter-cost: 2151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 559]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 553]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost: 2099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost: 2127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Adder-cost: 1495   maxlim: 8388607   bits: 24/23
c ---[ 543]---> Adder-cost: 1507   maxlim: 8388607   bits: 24/23
c ---[ 541]---> Adder-cost: 1419   maxlim: 4194303   bits: 23/22
c ---[ 539]---> Adder-cost: 1419   maxlim: 4194303   bits: 23/22
c ---[ 537]---> Adder-cost: 1438   maxlim: 8388607   bits: 24/23
c ---[ 535]---> Adder-cost: 1403   maxlim: 4194303   bits: 23/22
c ---[ 533]---> Adder-cost: 1395   maxlim: 4194303   bits: 23/22
c ---[ 531]---> Adder-cost: 1387   maxlim: 4194303   bits: 23/22
c ---[ 529]---> BDD-cost:   15
c ---[ 527]---> BDD-cost:   15
c ---[ 525]---> BDD-cost:   15
c ---[ 523]---> BDD-cost:   15
c ---[ 521]---> BDD-cost:   15
c ---[ 519]---> BDD-cost:   15
c ---[ 517]---> BDD-cost:   15
c ---[ 515]---> BDD-cost:   15
c ---[ 513]---> BDD-cost:   15
c ---[ 511]---> BDD-cost:   15
c ---[ 509]---> BDD-cost:   15
c ---[ 507]---> BDD-cost:   15
c ---[ 505]---> BDD-cost:   15
c ---[ 503]---> BDD-cost:   15
c ---[ 501]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:   15
c ---[ 498]---> Sorter-cost: 1899     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost: 1690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost: 1899     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Sorter-cost: 1912     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1936     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1888     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 487]---> Sorter-cost: 1910     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost: 1910     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost: 1910     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost: 1790     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost: 1779     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1790     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Sorter-cost: 1744     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 476]---> Sorter-cost: 1744     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost: 1816     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost: 1779     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost: 1790     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost: 1690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost: 1690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost: 1910     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost: 1910     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> Sorter-cost: 1714     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost: 1910     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost: 1712     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost: 1738     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost: 1690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost: 1712     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Sorter-cost: 1714     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost: 1690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> Sorter-cost: 1744     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost: 1779     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost: 1779     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost: 1790     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 443]---> Sorter-cost: 1792     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost: 2323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Sorter-cost: 2324     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost: 2322     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost: 2322     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost: 2324     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost: 2323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost: 2322     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost: 2322     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> BDD-cost:   25
c ---[ 409]---> BDD-cost:   25
c ---[ 408]---> BDD-cost:   25
c ---[ 407]---> BDD-cost:   25
c ---[ 406]---> BDD-cost:   25
c ---[ 405]---> BDD-cost:   25
c ---[ 404]---> BDD-cost:   25
c ---[ 403]---> BDD-cost:   18
c ---[ 402]---> BDD-cost:   18
c ---[ 401]---> BDD-cost:   18
c ---[ 400]---> BDD-cost:   18
c ---[ 399]---> BDD-cost:   18
c ---[ 398]---> BDD-cost:   18
c ---[ 397]---> BDD-cost:   25
c ---[ 396]---> BDD-cost:   25
c ---[ 395]---> BDD-cost:   25
c ---[ 394]---> BDD-cost:   25
c ---[ 393]---> BDD-cost:   25
c ---[ 392]---> BDD-cost:   25
c ---[ 391]---> BDD-cost:   22
c ---[ 390]---> BDD-cost:   22
c ---[ 389]---> BDD-cost:   22
c ---[ 388]---> BDD-cost:   22
c ---[ 387]---> BDD-cost:   22
c ---[ 386]---> BDD-cost:   22
c ---[ 385]---> BDD-cost:   21
c ---[ 384]---> BDD-cost:   21
c ---[ 383]---> BDD-cost:   21
c ---[ 382]---> BDD-cost:   21
c ---[ 381]---> BDD-cost:   21
c ---[ 380]---> BDD-cost:   21
c ---[ 379]---> BDD-cost:   22
c ---[ 378]---> BDD-cost:   22
c ---[ 377]---> BDD-cost:   22
c ---[ 376]---> BDD-cost:   22
c ---[ 375]---> BDD-cost:   22
c ---[ 374]---> BDD-cost:   22
c ---[ 373]---> BDD-cost:   25
c ---[ 372]---> BDD-cost:   25
c ---[ 371]---> BDD-cost:   25
c ---[ 370]---> BDD-cost:   25
c ---[ 369]---> BDD-cost:   25
c ---[ 368]---> BDD-cost:   25
c ---[ 367]---> BDD-cost:   22
c ---[ 366]---> BDD-cost:   22
c ---[ 365]---> BDD-cost:   22
c ---[ 364]---> BDD-cost:   22
c ---[ 363]---> BDD-cost:   22
c ---[ 362]---> BDD-cost:   22
c ---[ 361]---> BDD-cost:   25
c ---[ 360]---> BDD-cost:   25
c ---[ 359]---> BDD-cost:   25
c ---[ 358]---> BDD-cost:   25
c ---[ 357]---> BDD-cost:   25
c ---[ 356]---> BDD-cost:   25
c ---[ 355]---> BDD-cost:   25
c ---[ 354]---> BDD-cost:   25
c ---[ 353]---> BDD-cost:   25
c ---[ 352]---> BDD-cost:   25
c ---[ 351]---> BDD-cost:   25
c ---[ 350]---> BDD-cost:   25
c ---[ 349]---> BDD-cost:   25
c ---[ 348]---> BDD-cost:   23
c ---[ 347]---> BDD-cost:   23
c ---[ 346]---> BDD-cost:   23
c ---[ 345]---> BDD-cost:   23
c ---[ 344]---> BDD-cost:   23
c ---[ 343]---> BDD-cost:   23
c ---[ 342]---> BDD-cost:   25
c ---[ 341]---> BDD-cost:   25
c ---[ 340]---> BDD-cost:   25
c ---[ 339]---> BDD-cost:   25
c ---[ 338]---> BDD-cost:   25
c ---[ 337]---> BDD-cost:   25
c ---[ 336]---> BDD-cost:   25
c ---[ 335]---> BDD-cost:   25
c ---[ 334]---> BDD-cost:   25
c ---[ 333]---> BDD-cost:   25
c ---[ 332]---> BDD-cost:   25
c ---[ 331]---> BDD-cost:   25
c ---[ 330]---> BDD-cost:   25
c ---[ 329]---> BDD-cost:   25
c ---[ 328]---> BDD-cost:   25
c ---[ 327]---> BDD-cost:   25
c ---[ 326]---> BDD-cost:   25
c ---[ 325]---> BDD-cost:   25
c ---[ 324]---> BDD-cost:   25
c ---[ 323]---> BDD-cost:   25
c ---[ 322]---> BDD-cost:   25
c ---[ 321]---> BDD-cost:   25
c ---[ 320]---> BDD-cost:   25
c ---[ 319]---> BDD-cost:   25
c ---[ 318]---> BDD-cost:   25
c ---[ 317]---> BDD-cost:   25
c ---[ 316]---> BDD-cost:   25
c ---[ 315]---> BDD-cost:   25
c ---[ 314]---> BDD-cost:   25
c ---[ 313]---> BDD-cost:   25
c ---[ 312]---> BDD-cost:   21
c ---[ 311]---> BDD-cost:   21
c ---[ 310]---> BDD-cost:   21
c ---[ 309]---> BDD-cost:   21
c ---[ 308]---> BDD-cost:   21
c ---[ 307]---> BDD-cost:   21
c ---[ 306]---> BDD-cost:   21
c ---[ 305]---> BDD-cost:   21
c ---[ 304]---> BDD-cost:   21
c ---[ 303]---> BDD-cost:   21
c ---[ 302]---> BDD-cost:   21
c ---[ 301]---> BDD-cost:   21
c ---[ 300]---> BDD-cost:   22
c ---[ 299]---> BDD-cost:   22
c ---[ 298]---> BDD-cost:   22
c ---[ 297]---> BDD-cost:   22
c ---[ 296]---> BDD-cost:   22
c ---[ 295]---> BDD-cost:   22
c ---[ 294]---> BDD-cost:   22
c ---[ 293]---> BDD-cost:   20
c ---[ 292]---> BDD-cost:   20
c ---[ 291]---> BDD-cost:   20
c ---[ 290]---> BDD-cost:   20
c ---[ 289]---> BDD-cost:   20
c ---[ 288]---> BDD-cost:   20
c ---[ 287]---> BDD-cost:   22
c ---[ 286]---> BDD-cost:   22
c ---[ 285]---> BDD-cost:   22
c ---[ 284]---> BDD-cost:   22
c ---[ 283]---> BDD-cost:   22
c ---[ 282]---> BDD-cost:   22
c ---[ 281]---> BDD-cost:   21
c ---[ 280]---> BDD-cost:   21
c ---[ 279]---> BDD-cost:   21
c ---[ 278]---> BDD-cost:   21
c ---[ 277]---> BDD-cost:   21
c ---[ 276]---> BDD-cost:   21
c ---[ 275]---> BDD-cost:   20
c ---[ 274]---> BDD-cost:   20
c ---[ 273]---> BDD-cost:   20
c ---[ 272]---> BDD-cost:   20
c ---[ 271]---> BDD-cost:   20
c ---[ 270]---> BDD-cost:   20
c ---[ 269]---> BDD-cost:   22
c ---[ 268]---> BDD-cost:   22
c ---[ 267]---> BDD-cost:   22
c ---[ 266]---> BDD-cost:   22
c ---[ 265]---> BDD-cost:   22
c ---[ 264]---> BDD-cost:   22
c ---[ 263]---> BDD-cost:   19
c ---[ 262]---> BDD-cost:   19
c ---[ 261]---> BDD-cost:   19
c ---[ 260]---> BDD-cost:   19
c ---[ 259]---> BDD-cost:   19
c ---[ 258]---> BDD-cost:   19
c ---[ 257]---> BDD-cost:   22
c ---[ 256]---> BDD-cost:   22
c ---[ 255]---> BDD-cost:   22
c ---[ 254]---> BDD-cost:   22
c ---[ 253]---> BDD-cost:   22
c ---[ 252]---> BDD-cost:   22
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:   18
c ---[ 248]---> BDD-cost:   18
c ---[ 247]---> BDD-cost:   18
c ---[ 246]---> BDD-cost:   18
c ---[ 245]---> BDD-cost:   22
c ---[ 244]---> BDD-cost:   22
c ---[ 243]---> BDD-cost:   22
c ---[ 242]---> BDD-cost:   22
c ---[ 241]---> BDD-cost:   22
c ---[ 240]---> BDD-cost:   22
c ---[ 239]---> BDD-cost:   22
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   19
c ---[ 235]---> BDD-cost:   19
c ---[ 234]---> BDD-cost:   19
c ---[ 233]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   22
c ---[ 231]---> BDD-cost:   22
c ---[ 230]---> BDD-cost:   22
c ---[ 229]---> BDD-cost:   22
c ---[ 228]---> BDD-cost:   22
c ---[ 227]---> BDD-cost:   22
c ---[ 226]---> BDD-cost:   20
c ---[ 225]---> BDD-cost:   20
c ---[ 224]---> BDD-cost:   20
c ---[ 223]---> BDD-cost:   20
c ---[ 222]---> BDD-cost:   20
c ---[ 221]---> BDD-cost:   20
c ---[ 220]---> BDD-cost:   21
c ---[ 219]---> BDD-cost:   21
c ---[ 218]---> BDD-cost:   21
c ---[ 217]---> BDD-cost:   21
c ---[ 216]---> BDD-cost:   21
c ---[ 215]---> BDD-cost:   21
c ---[ 214]---> BDD-cost:   25
c ---[ 213]---> BDD-cost:   25
c ---[ 212]---> BDD-cost:   25
c ---[ 211]---> BDD-cost:   25
c ---[ 210]---> BDD-cost:   25
c ---[ 209]---> BDD-cost:   25
c ---[ 208]---> BDD-cost:   22
c ---[ 207]---> BDD-cost:   22
c ---[ 206]---> BDD-cost:   22
c ---[ 205]---> BDD-cost:   22
c ---[ 204]---> BDD-cost:   22
c ---[ 203]---> BDD-cost:   22
c ---[ 202]---> BDD-cost:   22
c ---[ 201]---> BDD-cost:   22
c ---[ 200]---> BDD-cost:   22
c ---[ 199]---> BDD-cost:   22
c ---[ 198]---> BDD-cost:   22
c ---[ 197]---> BDD-cost:   22
c ---[ 196]---> BDD-cost:   23
c ---[ 195]---> BDD-cost:   23
c ---[ 194]---> BDD-cost:   23
c ---[ 193]---> BDD-cost:   23
c ---[ 192]---> BDD-cost:   23
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   25
c ---[ 189]---> BDD-cost:   25
c ---[ 188]---> BDD-cost:   25
c ---[ 187]---> BDD-cost:   25
c ---[ 186]---> BDD-cost:   25
c ---[ 185]---> BDD-cost:   25
c ---[ 184]---> BDD-cost:   25
c ---[ 183]---> BDD-cost:   23
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   23
c ---[ 178]---> BDD-cost:   23
c ---[ 177]---> BDD-cost:   22
c ---[ 176]---> BDD-cost:   22
c ---[ 175]---> BDD-cost:   22
c ---[ 174]---> BDD-cost:   22
c ---[ 173]---> BDD-cost:   22
c ---[ 172]---> BDD-cost:   22
c ---[ 171]---> BDD-cost:   18
c ---[ 170]---> BDD-cost:   18
c ---[ 169]---> BDD-cost:   18
c ---[ 168]---> BDD-cost:   18
c ---[ 167]---> BDD-cost:   18
c ---[ 166]---> BDD-cost:   18
c ---[ 165]---> BDD-cost:   24
c ---[ 164]---> BDD-cost:   24
c ---[ 163]---> BDD-cost:   24
c ---[ 162]---> BDD-cost:   24
c ---[ 161]---> BDD-cost:   24
c ---[ 160]---> BDD-cost:   24
c ---[ 159]---> BDD-cost:   22
c ---[ 158]---> BDD-cost:   22
c ---[ 157]---> BDD-cost:   22
c ---[ 156]---> BDD-cost:   22
c ---[ 155]---> BDD-cost:   22
c ---[ 154]---> BDD-cost:   22
c ---[ 153]---> BDD-cost:   22
c ---[ 152]---> BDD-cost:   22
c ---[ 151]---> BDD-cost:   22
c ---[ 150]---> BDD-cost:   22
c ---[ 149]---> BDD-cost:   22
c ---[ 148]---> BDD-cost:   22
c ---[ 147]---> BDD-cost:   22
c ---[ 146]---> BDD-cost:   22
c ---[ 145]---> BDD-cost:   22
c ---[ 144]---> BDD-cost:   22
c ---[ 143]---> BDD-cost:   22
c ---[ 142]---> BDD-cost:   22
c ---[ 141]---> BDD-cost:   22
c ---[ 140]---> BDD-cost:   22
c ---[ 139]---> BDD-cost:   22
c ---[ 138]---> BDD-cost:   22
c ---[ 137]---> BDD-cost:   22
c ---[ 136]---> BDD-cost:   22
c ---[ 135]---> BDD-cost:   25
c ---[ 134]---> BDD-cost:   25
c ---[ 133]---> BDD-cost:   25
c ---[ 132]---> BDD-cost:   25
c ---[ 131]---> BDD-cost:   25
c ---[ 130]---> BDD-cost:   25
c ---[ 129]---> BDD-cost:   25
c ---[ 128]---> BDD-cost:   22
c ---[ 127]---> BDD-cost:   22
c ---[ 126]---> BDD-cost:   22
c ---[ 125]---> BDD-cost:   22
c ---[ 124]---> BDD-cost:   22
c ---[ 123]---> BDD-cost:   22
c ---[ 122]---> BDD-cost:   21
c ---[ 121]---> BDD-cost:   21
c ---[ 120]---> BDD-cost:   21
c ---[ 119]---> BDD-cost:   21
c ---[ 118]---> BDD-cost:   21
c ---[ 117]---> BDD-cost:   21
c ---[ 116]---> BDD-cost:   22
c ---[ 115]---> BDD-cost:   22
c ---[ 114]---> BDD-cost:   22
c ---[ 113]---> BDD-cost:   22
c ---[ 112]---> BDD-cost:   22
c ---[ 111]---> BDD-cost:   22
c ---[ 110]---> BDD-cost:   19
c ---[ 109]---> BDD-cost:   19
c ---[ 108]---> BDD-cost:   19
c ---[ 107]---> BDD-cost:   19
c ---[ 106]---> BDD-cost:   19
c ---[ 105]---> BDD-cost:   19
c ---[ 104]---> BDD-cost:   21
c ---[ 103]---> BDD-cost:   21
c ---[ 102]---> BDD-cost:   21
c ---[ 101]---> BDD-cost:   21
c ---[ 100]---> BDD-cost:   21
c ---[  99]---> BDD-cost:   21
c ---[  98]---> BDD-cost:   22
c ---[  97]---> BDD-cost:   22
c ---[  96]---> BDD-cost:   22
c ---[  95]---> BDD-cost:   22
c ---[  94]---> BDD-cost:   22
c ---[  93]---> BDD-cost:   22
c ---[  92]---> BDD-cost:   22
c ---[  91]---> BDD-cost:   22
c ---[  90]---> BDD-cost:   22
c ---[  89]---> BDD-cost:   22
c ---[  88]---> BDD-cost:   22
c ---[  87]---> BDD-cost:   22
c ---[  86]---> BDD-cost:   22
c ---[  85]---> BDD-cost:   22
c ---[  84]---> BDD-cost:   22
c ---[  83]---> BDD-cost:   22
c ---[  82]---> BDD-cost:   22
c ---[  81]---> BDD-cost:   22
c ---[  80]---> BDD-cost:   24
c ---[  79]---> BDD-cost:   24
c ---[  78]---> BDD-cost:   24
c ---[  77]---> BDD-cost:   24
c ---[  76]---> BDD-cost:   24
c ---[  75]---> BDD-cost:   24
c ---[  74]---> BDD-cost:   24
c ---[  73]---> BDD-cost:   21
c ---[  72]---> BDD-cost:   21
c ---[  71]---> BDD-cost:   21
c ---[  70]---> BDD-cost:   21
c ---[  69]---> BDD-cost:   21
c ---[  68]---> BDD-cost:   21
c ---[  67]---> BDD-cost:   21
c ---[  66]---> BDD-cost:   21
c ---[  65]---> BDD-cost:   21
c ---[  64]---> BDD-cost:   21
c ---[  63]---> BDD-cost:   21
c ---[  62]---> BDD-cost:   21
c ---[  61]---> BDD-cost:   21
c ---[  60]---> BDD-cost:   21
c ---[  59]---> BDD-cost:   21
c ---[  58]---> BDD-cost:   21
c ---[  57]---> BDD-cost:   21
c ---[  56]---> BDD-cost:   21
c ---[  55]---> BDD-cost:   22
c ---[  54]---> BDD-cost:   22
c ---[  53]---> BDD-cost:   22
c ---[  52]---> BDD-cost:   22
c ---[  51]---> BDD-cost:   22
c ---[  50]---> BDD-cost:   22
c ---[  49]---> BDD-cost:   22
c ---[  48]---> BDD-cost:   22
c ---[  47]---> BDD-cost:   22
c ---[  46]---> BDD-cost:   22
c ---[  45]---> BDD-cost:   22
c ---[  44]---> BDD-cost:   22
c ---[  43]---> BDD-cost:   22
c ---[  42]---> BDD-cost:   22
c ---[  41]---> BDD-cost:   22
c ---[  40]---> BDD-cost:   22
c ---[  39]---> BDD-cost:   22
c ---[  38]---> BDD-cost:   22
c ---[  37]---> BDD-cost:   19
c ---[  36]---> BDD-cost:   19
c ---[  35]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   19
c ---[  33]---> BDD-cost:   19
c ---[  32]---> BDD-cost:   19
c ---[  31]---> BDD-cost:   22
c ---[  30]---> BDD-cost:   22
c ---[  29]---> BDD-cost:   22
c ---[  28]---> BDD-cost:   22
c ---[  27]---> BDD-cost:   22
c ---[  26]---> BDD-cost:   22
c ---[  25]---> BDD-cost:   22
c ---[  24]---> BDD-cost:   22
c ---[  23]---> BDD-cost:   22
c ---[  22]---> BDD-cost:   22
c ---[  21]---> BDD-cost:   22
c ---[  20]---> BDD-cost:   22
c ---[  19]---> BDD-cost:   22
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   13
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   58
c ---[  14]---> BDD-cost:   60
c ---[  13]---> BDD-cost:   63
c ---[  12]---> BDD-cost:   63
c ---[  11]---> BDD-cost:   60
c ---[  10]---> BDD-cost:   58
c ---[   9]---> BDD-cost:   63
c ---[   8]---> BDD-cost:   63
c ---[   7]---> BDD-cost:  123
c ---[   6]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[   5]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  381     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  846996  2262333 |  282332       0        0     nan |  0.000 % |
c |       100 |  846881  2262075 |  310565      87      326     3.7 |  4.643 % |
c |       250 |  846689  2261663 |  341621     219      839     3.8 |  4.666 % |
c |       475 |  846600  2261466 |  375783     437     1777     4.1 |  4.675 % |
c |       812 |  846482  2261214 |  413362     759     5366     7.1 |  4.690 % |
c |      1318 |  846474  2261188 |  454698    1264    13759    10.9 |  4.690 % |
c |      2077 |  846279  2260757 |  500168    2015    26139    13.0 |  4.709 % |
c |      3216 |  845923  2259977 |  550185    3121    37580    12.0 |  4.747 % |
c |      4924 |  845212  2258409 |  605203    4743    51824    10.9 |  4.823 % |
c |      7486 |  844789  2257448 |  665724    7283    75727    10.4 |  4.863 % |
c |     11330 |  844351  2256468 |  732296   11073   137214    12.4 |  4.909 % |
c |     17098 |  843982  2255655 |  805526   16802   365193    21.7 |  4.947 % |
c |     25747 |  842540  2252426 |  886078   25267   539057    21.3 |  5.101 % |
c |     38722 |  841729  2250612 |  974686   38164   947119    24.8 |  5.188 % |
c |     58184 |  841043  2249110 | 1072155   57562  1482885    25.8 |  5.262 % |
c |     87376 |  840158  2247147 | 1179370   86686  3104618    35.8 |  5.353 % |
c |    131165 |  840078  2246973 | 1297307  130466 10578116    81.1 |  5.361 % |

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/14891/stat): 14891 (minisat+_script) R 14890 14891 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793574118 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/14891/statm): 174 3 169 147 0 27 0
[pid=14891] 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=14892
New process pid=14893
New process pid=14894
execve syscall for /bin/sed executable
One traced child (pid=14893) 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=14894) exited with status: 0
One traced child (pid=14892) exited with status: 0
New process pid=14895
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-danoint.opb

[startup+10.0052 s]
Raw data (loadavg): 0.93 0.95 0.70 1/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) T 14891 14891 30740 0 -1 0 13781 0 3 0 869 58 0 0 22 0 1 0 1793574123 65777664 13100 4294967295 134512640 135094434 3221224432 3221209852 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/14895/statm): 16059 13100 145 145 0 15914 0
[pid=14895] vsize: 64236
Current children cumulated CPU time (s) 9.27
Current children cumulated vsize (Kb) 66360

[startup+20.006 s]
Raw data (loadavg): 0.94 0.96 0.70 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 22994 0 3 0 1787 98 0 0 25 0 1 0 1793574123 113037312 22313 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 27597 22313 145 145 0 27452 0
[pid=14895] vsize: 110388
Current children cumulated CPU time (s) 18.85
Current children cumulated vsize (Kb) 112512

[startup+30.0088 s]
Raw data (loadavg): 0.95 0.96 0.71 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23043 0 3 0 2785 99 0 0 25 0 1 0 1793574123 113238016 22362 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 27646 22362 145 145 0 27501 0
[pid=14895] vsize: 110584
Current children cumulated CPU time (s) 28.84
Current children cumulated vsize (Kb) 112708

[startup+40.0096 s]
Raw data (loadavg): 0.96 0.96 0.71 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23101 0 3 0 3783 100 0 0 25 0 1 0 1793574123 113475584 22420 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27704 22420 145 145 0 27559 0
[pid=14895] vsize: 110816
Current children cumulated CPU time (s) 38.83
Current children cumulated vsize (Kb) 112940

[startup+50.0103 s]
Raw data (loadavg): 0.96 0.96 0.71 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23145 0 3 0 4782 101 0 0 25 0 1 0 1793574123 113623040 22464 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27740 22464 145 145 0 27595 0
[pid=14895] vsize: 110960
Current children cumulated CPU time (s) 48.83
Current children cumulated vsize (Kb) 113084

[startup+60.0111 s]
Raw data (loadavg): 0.97 0.96 0.71 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23158 0 3 0 5783 102 0 0 25 0 1 0 1793574123 113684480 22477 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27755 22477 145 145 0 27610 0
[pid=14895] vsize: 111020
Current children cumulated CPU time (s) 58.85
Current children cumulated vsize (Kb) 113144

[startup+70.0219 s]
Raw data (loadavg): 0.97 0.96 0.72 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23173 0 3 0 6782 102 0 0 25 0 1 0 1793574123 113745920 22492 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27770 22492 145 145 0 27625 0
[pid=14895] vsize: 111080
Current children cumulated CPU time (s) 68.84
Current children cumulated vsize (Kb) 113204

[startup+80.0227 s]
Raw data (loadavg): 0.98 0.96 0.72 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23220 0 3 0 7781 103 0 0 25 0 1 0 1793574123 113930240 22539 4294967295 134512640 135094434 3221224432 3221223092 134553454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27815 22539 145 145 0 27670 0
[pid=14895] vsize: 111260
Current children cumulated CPU time (s) 78.84
Current children cumulated vsize (Kb) 113384

[startup+90.0235 s]
Raw data (loadavg): 0.98 0.96 0.72 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23238 0 3 0 8781 103 0 0 25 0 1 0 1793574123 114003968 22557 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27833 22557 145 145 0 27688 0
[pid=14895] vsize: 111332
Current children cumulated CPU time (s) 88.84
Current children cumulated vsize (Kb) 113456

[startup+100.023 s]
Raw data (loadavg): 0.98 0.96 0.73 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23264 0 3 0 9780 103 0 0 25 0 1 0 1793574123 114139136 22583 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27866 22583 145 145 0 27721 0
[pid=14895] vsize: 111464
Current children cumulated CPU time (s) 98.83
Current children cumulated vsize (Kb) 113588

[startup+110.024 s]
Raw data (loadavg): 0.98 0.96 0.73 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23295 0 3 0 10780 103 0 0 25 0 1 0 1793574123 114257920 22614 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27895 22614 145 145 0 27750 0
[pid=14895] vsize: 111580
Current children cumulated CPU time (s) 108.83
Current children cumulated vsize (Kb) 113704

[startup+120.025 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23378 0 3 0 11779 104 0 0 25 0 1 0 1793574123 114589696 22697 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 27976 22697 145 145 0 27831 0
[pid=14895] vsize: 111904
Current children cumulated CPU time (s) 118.83
Current children cumulated vsize (Kb) 114028

[startup+130.026 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23513 0 3 0 12777 105 0 0 25 0 1 0 1793574123 115134464 22832 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28109 22832 145 145 0 27964 0
[pid=14895] vsize: 112436
Current children cumulated CPU time (s) 128.82
Current children cumulated vsize (Kb) 114560

[startup+140.027 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23541 0 3 0 13777 105 0 0 25 0 1 0 1793574123 115249152 22860 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28137 22860 145 145 0 27992 0
[pid=14895] vsize: 112548
Current children cumulated CPU time (s) 138.82
Current children cumulated vsize (Kb) 114672

[startup+150.027 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23566 0 3 0 14776 106 0 0 25 0 1 0 1793574123 115347456 22885 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28161 22885 145 145 0 28016 0
[pid=14895] vsize: 112644
Current children cumulated CPU time (s) 148.82
Current children cumulated vsize (Kb) 114768

[startup+160.028 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23593 0 3 0 15776 106 0 0 25 0 1 0 1793574123 115458048 22912 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28188 22912 145 145 0 28043 0
[pid=14895] vsize: 112752
Current children cumulated CPU time (s) 158.82
Current children cumulated vsize (Kb) 114876

[startup+170.029 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23648 0 3 0 16775 106 0 0 25 0 1 0 1793574123 115720192 22967 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28252 22967 145 145 0 28107 0
[pid=14895] vsize: 113008
Current children cumulated CPU time (s) 168.81
Current children cumulated vsize (Kb) 115132

[startup+180.03 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23674 0 3 0 17775 107 0 0 25 0 1 0 1793574123 115818496 22993 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28276 22993 145 145 0 28131 0
[pid=14895] vsize: 113104
Current children cumulated CPU time (s) 178.82
Current children cumulated vsize (Kb) 115228

[startup+190.031 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23721 0 3 0 18774 107 0 0 25 0 1 0 1793574123 116006912 23040 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28322 23040 145 145 0 28177 0
[pid=14895] vsize: 113288
Current children cumulated CPU time (s) 188.81
Current children cumulated vsize (Kb) 115412

[startup+200.031 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23768 0 3 0 19774 108 0 0 25 0 1 0 1793574123 116195328 23087 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28368 23087 145 145 0 28223 0
[pid=14895] vsize: 113472
Current children cumulated CPU time (s) 198.82
Current children cumulated vsize (Kb) 115596

[startup+210.032 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23809 0 3 0 20774 108 0 0 25 0 1 0 1793574123 116363264 23128 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28409 23128 145 145 0 28264 0
[pid=14895] vsize: 113636
Current children cumulated CPU time (s) 208.82
Current children cumulated vsize (Kb) 115760

[startup+220.033 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23850 0 3 0 21773 108 0 0 25 0 1 0 1793574123 116523008 23169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28448 23169 145 145 0 28303 0
[pid=14895] vsize: 113792
Current children cumulated CPU time (s) 218.81
Current children cumulated vsize (Kb) 115916

[startup+230.034 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23868 0 3 0 22773 108 0 0 25 0 1 0 1793574123 116588544 23187 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28464 23187 145 145 0 28319 0
[pid=14895] vsize: 113856
Current children cumulated CPU time (s) 228.81
Current children cumulated vsize (Kb) 115980

[startup+240.035 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23878 0 3 0 23773 108 0 0 25 0 1 0 1793574123 116625408 23197 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28473 23197 145 145 0 28328 0
[pid=14895] vsize: 113892
Current children cumulated CPU time (s) 238.81
Current children cumulated vsize (Kb) 116016

[startup+250.035 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23895 0 3 0 24773 108 0 0 25 0 1 0 1793574123 116690944 23214 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28489 23214 145 145 0 28344 0
[pid=14895] vsize: 113956
Current children cumulated CPU time (s) 248.81
Current children cumulated vsize (Kb) 116080

[startup+260.036 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23905 0 3 0 25773 108 0 0 25 0 1 0 1793574123 116731904 23224 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28499 23224 145 145 0 28354 0
[pid=14895] vsize: 113996
Current children cumulated CPU time (s) 258.81
Current children cumulated vsize (Kb) 116120

[startup+270.037 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23946 0 3 0 26772 109 0 0 25 0 1 0 1793574123 116883456 23265 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28536 23265 145 145 0 28391 0
[pid=14895] vsize: 114144
Current children cumulated CPU time (s) 268.81
Current children cumulated vsize (Kb) 116268

[startup+280.038 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23977 0 3 0 27772 109 0 0 25 0 1 0 1793574123 117002240 23296 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28565 23296 145 145 0 28420 0
[pid=14895] vsize: 114260
Current children cumulated CPU time (s) 278.81
Current children cumulated vsize (Kb) 116384

[startup+290.039 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23993 0 3 0 28772 109 0 0 25 0 1 0 1793574123 117067776 23312 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28581 23312 145 145 0 28436 0
[pid=14895] vsize: 114324
Current children cumulated CPU time (s) 288.81
Current children cumulated vsize (Kb) 116448

[startup+300.039 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24068 0 3 0 29771 110 0 0 25 0 1 0 1793574123 117309440 23387 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28640 23387 145 145 0 28495 0
[pid=14895] vsize: 114560
Current children cumulated CPU time (s) 298.81
Current children cumulated vsize (Kb) 116684

[startup+310.04 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24137 0 3 0 30770 110 0 0 25 0 1 0 1793574123 117587968 23456 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28708 23456 145 145 0 28563 0
[pid=14895] vsize: 114832
Current children cumulated CPU time (s) 308.8
Current children cumulated vsize (Kb) 116956

[startup+320.04 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24251 0 3 0 31769 111 0 0 25 0 1 0 1793574123 118173696 23570 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28851 23570 145 145 0 28706 0
[pid=14895] vsize: 115404
Current children cumulated CPU time (s) 318.8
Current children cumulated vsize (Kb) 117528

[startup+330.042 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24337 0 3 0 32768 111 0 0 25 0 1 0 1793574123 118517760 23656 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 28935 23656 145 145 0 28790 0
[pid=14895] vsize: 115740
Current children cumulated CPU time (s) 328.79
Current children cumulated vsize (Kb) 117864

[startup+340.042 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24483 0 3 0 33764 113 0 0 25 0 1 0 1793574123 119111680 23802 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29080 23802 145 145 0 28935 0
[pid=14895] vsize: 116320
Current children cumulated CPU time (s) 338.77
Current children cumulated vsize (Kb) 118444

[startup+350.042 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24539 0 3 0 34763 113 0 0 25 0 1 0 1793574123 119336960 23858 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29135 23858 145 145 0 28990 0
[pid=14895] vsize: 116540
Current children cumulated CPU time (s) 348.76
Current children cumulated vsize (Kb) 118664

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24616 0 3 0 35762 114 0 0 25 0 1 0 1793574123 119640064 23935 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29209 23935 145 145 0 29064 0
[pid=14895] vsize: 116836
Current children cumulated CPU time (s) 358.76
Current children cumulated vsize (Kb) 118960

[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24739 0 3 0 36760 115 0 0 25 0 1 0 1793574123 120131584 24058 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29329 24058 145 145 0 29184 0
[pid=14895] vsize: 117316
Current children cumulated CPU time (s) 368.75
Current children cumulated vsize (Kb) 119440

[startup+380.045 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24842 0 3 0 37758 117 0 0 25 0 1 0 1793574123 120541184 24161 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29429 24161 145 145 0 29284 0
[pid=14895] vsize: 117716
Current children cumulated CPU time (s) 378.75
Current children cumulated vsize (Kb) 119840

[startup+390.045 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24898 0 3 0 38757 117 0 0 25 0 1 0 1793574123 120766464 24217 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29484 24217 145 145 0 29339 0
[pid=14895] vsize: 117936
Current children cumulated CPU time (s) 388.74
Current children cumulated vsize (Kb) 120060

[startup+400.046 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25033 0 3 0 39756 118 0 0 25 0 1 0 1793574123 121303040 24352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29615 24352 145 145 0 29470 0
[pid=14895] vsize: 118460
Current children cumulated CPU time (s) 398.74
Current children cumulated vsize (Kb) 120584

[startup+410.047 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25071 0 3 0 40756 118 0 0 25 0 1 0 1793574123 121454592 24390 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 29652 24390 145 145 0 29507 0
[pid=14895] vsize: 118608
Current children cumulated CPU time (s) 408.74
Current children cumulated vsize (Kb) 120732

[startup+420.048 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25240 0 3 0 41753 119 0 0 25 0 1 0 1793574123 122134528 24559 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 29818 24559 145 145 0 29673 0
[pid=14895] vsize: 119272
Current children cumulated CPU time (s) 418.72
Current children cumulated vsize (Kb) 121396

[startup+430.049 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25300 0 3 0 42751 120 0 0 25 0 1 0 1793574123 122372096 24619 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 29876 24619 145 145 0 29731 0
[pid=14895] vsize: 119504
Current children cumulated CPU time (s) 428.71
Current children cumulated vsize (Kb) 121628

[startup+440.049 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25386 0 3 0 43749 121 0 0 25 0 1 0 1793574123 122720256 24705 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 29961 24705 145 145 0 29816 0
[pid=14895] vsize: 119844
Current children cumulated CPU time (s) 438.7
Current children cumulated vsize (Kb) 121968

[startup+450.05 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25452 0 3 0 44747 123 0 0 25 0 1 0 1793574123 122990592 24771 4294967295 134512640 135094434 3221224432 3221223088 134557853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30027 24771 145 145 0 29882 0
[pid=14895] vsize: 120108
Current children cumulated CPU time (s) 448.7
Current children cumulated vsize (Kb) 122232

[startup+460.051 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25509 0 3 0 45746 123 0 0 25 0 1 0 1793574123 123219968 24828 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30083 24828 145 145 0 29938 0
[pid=14895] vsize: 120332
Current children cumulated CPU time (s) 458.69
Current children cumulated vsize (Kb) 122456

[startup+470.052 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25582 0 3 0 46744 124 0 0 25 0 1 0 1793574123 123514880 24901 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30155 24901 145 145 0 30010 0
[pid=14895] vsize: 120620
Current children cumulated CPU time (s) 468.68
Current children cumulated vsize (Kb) 122744

[startup+480.053 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25666 0 3 0 47743 125 0 0 25 0 1 0 1793574123 123854848 24985 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30238 24985 145 145 0 30093 0
[pid=14895] vsize: 120952
Current children cumulated CPU time (s) 478.68
Current children cumulated vsize (Kb) 123076

[startup+490.054 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25761 0 3 0 48741 126 0 0 25 0 1 0 1793574123 124239872 25080 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30332 25080 145 145 0 30187 0
[pid=14895] vsize: 121328
Current children cumulated CPU time (s) 488.67
Current children cumulated vsize (Kb) 123452

[startup+500.055 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25850 0 3 0 49739 127 0 0 25 0 1 0 1793574123 124604416 25169 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30421 25169 145 145 0 30276 0
[pid=14895] vsize: 121684
Current children cumulated CPU time (s) 498.66
Current children cumulated vsize (Kb) 123808

[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25926 0 3 0 50737 128 0 0 25 0 1 0 1793574123 125173760 25245 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30560 25245 145 145 0 30415 0
[pid=14895] vsize: 122240
Current children cumulated CPU time (s) 508.65
Current children cumulated vsize (Kb) 124364

[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26001 0 3 0 51736 129 0 0 25 0 1 0 1793574123 125476864 25320 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30634 25320 145 145 0 30489 0
[pid=14895] vsize: 122536
Current children cumulated CPU time (s) 518.65
Current children cumulated vsize (Kb) 124660

[startup+530.058 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26086 0 3 0 52733 130 0 0 25 0 1 0 1793574123 125820928 25405 4294967295 134512640 135094434 3221224432 3221223056 134557702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30718 25405 145 145 0 30573 0
[pid=14895] vsize: 122872
Current children cumulated CPU time (s) 528.63
Current children cumulated vsize (Kb) 124996

[startup+540.06 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26158 0 3 0 53731 131 0 0 25 0 1 0 1793574123 126107648 25477 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 30788 25477 145 145 0 30643 0
[pid=14895] vsize: 123152
Current children cumulated CPU time (s) 538.62
Current children cumulated vsize (Kb) 125276

[startup+550.061 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26667 0 3 0 54721 135 0 0 25 0 1 0 1793574123 128172032 25986 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31292 25986 145 145 0 31147 0
[pid=14895] vsize: 125168
Current children cumulated CPU time (s) 548.56
Current children cumulated vsize (Kb) 127292

[startup+560.062 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26778 0 3 0 55719 136 0 0 25 0 1 0 1793574123 128622592 26097 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31402 26097 145 145 0 31257 0
[pid=14895] vsize: 125608
Current children cumulated CPU time (s) 558.55
Current children cumulated vsize (Kb) 127732

[startup+570.062 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26852 0 3 0 56717 137 0 0 25 0 1 0 1793574123 128917504 26171 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31474 26171 145 145 0 31329 0
[pid=14895] vsize: 125896
Current children cumulated CPU time (s) 568.54
Current children cumulated vsize (Kb) 128020

[startup+580.064 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26887 0 3 0 57716 138 0 0 25 0 1 0 1793574123 129056768 26206 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31508 26206 145 145 0 31363 0
[pid=14895] vsize: 126032
Current children cumulated CPU time (s) 578.54
Current children cumulated vsize (Kb) 128156

[startup+590.065 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26979 0 3 0 58715 138 0 0 25 0 1 0 1793574123 129421312 26298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31597 26298 145 145 0 31452 0
[pid=14895] vsize: 126388
Current children cumulated CPU time (s) 588.53
Current children cumulated vsize (Kb) 128512

[startup+600.066 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27078 0 3 0 59713 140 0 0 25 0 1 0 1793574123 129818624 26397 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31694 26397 145 145 0 31549 0
[pid=14895] vsize: 126776
Current children cumulated CPU time (s) 598.53
Current children cumulated vsize (Kb) 128900

[startup+610.067 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27166 0 3 0 60710 142 0 0 25 0 1 0 1793574123 130170880 26485 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31780 26485 145 145 0 31635 0
[pid=14895] vsize: 127120
Current children cumulated CPU time (s) 608.52
Current children cumulated vsize (Kb) 129244

[startup+620.068 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27230 0 3 0 61709 142 0 0 25 0 1 0 1793574123 130424832 26549 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 31842 26549 145 145 0 31697 0
[pid=14895] vsize: 127368
Current children cumulated CPU time (s) 618.51
Current children cumulated vsize (Kb) 129492

[startup+630.07 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27480 0 3 0 62705 144 0 0 25 0 1 0 1793574123 131440640 26799 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 32090 26799 145 145 0 31945 0
[pid=14895] vsize: 128360
Current children cumulated CPU time (s) 628.49
Current children cumulated vsize (Kb) 130484

[startup+640.071 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 28223 0 3 0 63691 151 0 0 25 0 1 0 1793574123 134463488 27542 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 32828 27542 145 145 0 32683 0
[pid=14895] vsize: 131312
Current children cumulated CPU time (s) 638.42
Current children cumulated vsize (Kb) 133436

[startup+650.074 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 28928 0 3 0 64678 156 0 0 25 0 1 0 1793574123 137334784 28247 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 33529 28247 145 145 0 33384 0
[pid=14895] vsize: 134116
Current children cumulated CPU time (s) 648.34
Current children cumulated vsize (Kb) 136240

[startup+660.074 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 29627 0 3 0 65667 160 0 0 25 0 1 0 1793574123 140189696 28946 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 34226 28946 145 145 0 34081 0
[pid=14895] vsize: 136904
Current children cumulated CPU time (s) 658.27
Current children cumulated vsize (Kb) 139028

[startup+670.075 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 30280 0 3 0 66654 165 0 0 25 0 1 0 1793574123 142856192 29599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 34877 29599 145 145 0 34732 0
[pid=14895] vsize: 139508
Current children cumulated CPU time (s) 668.19
Current children cumulated vsize (Kb) 141632

[startup+680.077 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 30882 0 3 0 67643 170 0 0 25 0 1 0 1793574123 145309696 30201 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 35476 30201 145 145 0 35331 0
[pid=14895] vsize: 141904
Current children cumulated CPU time (s) 678.13
Current children cumulated vsize (Kb) 144028

[startup+690.078 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 31548 0 3 0 68632 174 0 0 25 0 1 0 1793574123 148021248 30867 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 36138 30867 145 145 0 35993 0
[pid=14895] vsize: 144552
Current children cumulated CPU time (s) 688.06
Current children cumulated vsize (Kb) 146676

[startup+700.077 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 32363 0 3 0 69619 181 0 0 25 0 1 0 1793574123 151343104 31682 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 36949 31682 145 145 0 36804 0
[pid=14895] vsize: 147796
Current children cumulated CPU time (s) 698
Current children cumulated vsize (Kb) 149920

[startup+710.078 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 32924 0 3 0 70609 185 0 0 25 0 1 0 1793574123 153628672 32243 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 37507 32243 145 145 0 37362 0
[pid=14895] vsize: 150028
Current children cumulated CPU time (s) 707.94
Current children cumulated vsize (Kb) 152152

[startup+720.079 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 33542 0 3 0 71600 188 0 0 25 0 1 0 1793574123 156155904 32861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 38124 32861 145 145 0 37979 0
[pid=14895] vsize: 152496
Current children cumulated CPU time (s) 717.88
Current children cumulated vsize (Kb) 154620

[startup+730.08 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 34180 0 3 0 72589 192 0 0 25 0 1 0 1793574123 158765056 33499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 38761 33499 145 145 0 38616 0
[pid=14895] vsize: 155044
Current children cumulated CPU time (s) 727.81
Current children cumulated vsize (Kb) 157168

[startup+740.081 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 34891 0 3 0 73577 196 0 0 25 0 1 0 1793574123 161673216 34210 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 39471 34210 145 145 0 39326 0
[pid=14895] vsize: 157884
Current children cumulated CPU time (s) 737.73
Current children cumulated vsize (Kb) 160008

[startup+750.081 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 34999 0 3 0 74576 198 0 0 25 0 1 0 1793574123 162123776 34318 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 39581 34318 145 145 0 39436 0
[pid=14895] vsize: 158324
Current children cumulated CPU time (s) 747.74
Current children cumulated vsize (Kb) 160448

[startup+760.082 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35053 0 3 0 75575 198 0 0 25 0 1 0 1793574123 162344960 34372 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14895/statm): 39635 34372 145 145 0 39490 0
[pid=14895] vsize: 158540
Current children cumulated CPU time (s) 757.73
Current children cumulated vsize (Kb) 160664

[startup+770.083 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35096 0 3 0 76574 198 0 0 25 0 1 0 1793574123 163041280 34415 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 39805 34415 145 145 0 39660 0
[pid=14895] vsize: 159220
Current children cumulated CPU time (s) 767.72
Current children cumulated vsize (Kb) 161344

[startup+780.085 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35132 0 3 0 77573 199 0 0 25 0 1 0 1793574123 163184640 34451 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 39840 34451 145 145 0 39695 0
[pid=14895] vsize: 159360
Current children cumulated CPU time (s) 777.72
Current children cumulated vsize (Kb) 161484

[startup+790.086 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35281 0 3 0 78571 200 0 0 25 0 1 0 1793574123 163786752 34600 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 39987 34600 145 145 0 39842 0
[pid=14895] vsize: 159948
Current children cumulated CPU time (s) 787.71
Current children cumulated vsize (Kb) 162072

[startup+800.085 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35307 0 3 0 79571 200 0 0 25 0 1 0 1793574123 163889152 34626 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40012 34626 145 145 0 39867 0
[pid=14895] vsize: 160048
Current children cumulated CPU time (s) 797.71
Current children cumulated vsize (Kb) 162172

[startup+810.086 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35357 0 3 0 80570 201 0 0 25 0 1 0 1793574123 164093952 34676 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40062 34676 145 145 0 39917 0
[pid=14895] vsize: 160248
Current children cumulated CPU time (s) 807.71
Current children cumulated vsize (Kb) 162372

[startup+820.087 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35465 0 3 0 81568 202 0 0 25 0 1 0 1793574123 164528128 34784 4294967295 134512640 135094434 3221224432 3221223056 134557660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40168 34784 145 145 0 40023 0
[pid=14895] vsize: 160672
Current children cumulated CPU time (s) 817.7
Current children cumulated vsize (Kb) 162796

[startup+830.088 s]
Raw data (loadavg): 0.99 0.97 0.84 1/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) T 14891 14891 30740 0 -1 0 35556 0 3 0 82567 202 0 0 25 0 1 0 1793574123 164896768 34875 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40258 34875 145 145 0 40113 0
[pid=14895] vsize: 161032
Current children cumulated CPU time (s) 827.69
Current children cumulated vsize (Kb) 163156

[startup+840.088 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35664 0 3 0 83565 203 0 0 25 0 1 0 1793574123 165335040 34983 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40365 34983 145 145 0 40220 0
[pid=14895] vsize: 161460
Current children cumulated CPU time (s) 837.68
Current children cumulated vsize (Kb) 163584

[startup+850.088 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35771 0 3 0 84564 204 0 0 25 0 1 0 1793574123 165769216 35090 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40471 35090 145 145 0 40326 0
[pid=14895] vsize: 161884
Current children cumulated CPU time (s) 847.68
Current children cumulated vsize (Kb) 164008

[startup+860.089 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35889 0 3 0 85563 204 0 0 25 0 1 0 1793574123 166252544 35208 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40589 35208 145 145 0 40444 0
[pid=14895] vsize: 162356
Current children cumulated CPU time (s) 857.67
Current children cumulated vsize (Kb) 164480

[startup+870.09 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35995 0 3 0 86561 206 0 0 25 0 1 0 1793574123 166682624 35314 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40694 35314 145 145 0 40549 0
[pid=14895] vsize: 162776
Current children cumulated CPU time (s) 867.67
Current children cumulated vsize (Kb) 164900

[startup+880.091 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36103 0 3 0 87559 207 0 0 25 0 1 0 1793574123 167120896 35422 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40801 35422 145 145 0 40656 0
[pid=14895] vsize: 163204
Current children cumulated CPU time (s) 877.66
Current children cumulated vsize (Kb) 165328

[startup+890.091 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36231 0 3 0 88557 208 0 0 25 0 1 0 1793574123 167641088 35550 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 40928 35550 145 145 0 40783 0
[pid=14895] vsize: 163712
Current children cumulated CPU time (s) 887.65
Current children cumulated vsize (Kb) 165836

[startup+900.092 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36351 0 3 0 89555 208 0 0 25 0 1 0 1793574123 168120320 35670 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41045 35670 145 145 0 40900 0
[pid=14895] vsize: 164180
Current children cumulated CPU time (s) 897.63
Current children cumulated vsize (Kb) 166304

[startup+910.093 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36459 0 3 0 90554 209 0 0 25 0 1 0 1793574123 168570880 35778 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41155 35778 145 145 0 41010 0
[pid=14895] vsize: 164620
Current children cumulated CPU time (s) 907.63
Current children cumulated vsize (Kb) 166744

[startup+920.094 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36563 0 3 0 91553 210 0 0 25 0 1 0 1793574123 169013248 35882 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41263 35882 145 145 0 41118 0
[pid=14895] vsize: 165052
Current children cumulated CPU time (s) 917.63
Current children cumulated vsize (Kb) 167176

[startup+930.095 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36653 0 3 0 92552 210 0 0 25 0 1 0 1793574123 169381888 35972 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41353 35972 145 145 0 41208 0
[pid=14895] vsize: 165412
Current children cumulated CPU time (s) 927.62
Current children cumulated vsize (Kb) 167536

[startup+940.096 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36747 0 3 0 93550 211 0 0 25 0 1 0 1793574123 169758720 36066 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41445 36066 145 145 0 41300 0
[pid=14895] vsize: 165780
Current children cumulated CPU time (s) 937.61
Current children cumulated vsize (Kb) 167904

[startup+950.096 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36858 0 3 0 94549 212 0 0 25 0 1 0 1793574123 170201088 36177 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41553 36177 145 145 0 41408 0
[pid=14895] vsize: 166212
Current children cumulated CPU time (s) 947.61
Current children cumulated vsize (Kb) 168336

[startup+960.098 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36929 0 3 0 95548 212 0 0 25 0 1 0 1793574123 170491904 36248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41624 36248 145 145 0 41479 0
[pid=14895] vsize: 166496
Current children cumulated CPU time (s) 957.6
Current children cumulated vsize (Kb) 168620

[startup+970.099 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36982 0 3 0 96547 213 0 0 25 0 1 0 1793574123 170704896 36301 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41676 36301 145 145 0 41531 0
[pid=14895] vsize: 166704
Current children cumulated CPU time (s) 967.6
Current children cumulated vsize (Kb) 168828

[startup+980.099 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37039 0 3 0 97546 214 0 0 25 0 1 0 1793574123 170938368 36358 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41733 36358 145 145 0 41588 0
[pid=14895] vsize: 166932
Current children cumulated CPU time (s) 977.6
Current children cumulated vsize (Kb) 169056

[startup+990.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37091 0 3 0 98546 214 0 0 25 0 1 0 1793574123 171147264 36410 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41784 36410 145 145 0 41639 0
[pid=14895] vsize: 167136
Current children cumulated CPU time (s) 987.6
Current children cumulated vsize (Kb) 169260

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37137 0 3 0 99545 214 0 0 25 0 1 0 1793574123 171335680 36456 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41830 36456 145 145 0 41685 0
[pid=14895] vsize: 167320
Current children cumulated CPU time (s) 997.59
Current children cumulated vsize (Kb) 169444

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37222 0 3 0 100545 215 0 0 25 0 1 0 1793574123 171679744 36541 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41914 36541 145 145 0 41769 0
[pid=14895] vsize: 167656
Current children cumulated CPU time (s) 1007.6
Current children cumulated vsize (Kb) 169780

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37298 0 3 0 101543 216 0 0 25 0 1 0 1793574123 171986944 36617 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 41989 36617 145 145 0 41844 0
[pid=14895] vsize: 167956
Current children cumulated CPU time (s) 1017.59
Current children cumulated vsize (Kb) 170080

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37354 0 3 0 102542 216 0 0 25 0 1 0 1793574123 172216320 36673 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42045 36673 145 145 0 41900 0
[pid=14895] vsize: 168180
Current children cumulated CPU time (s) 1027.58
Current children cumulated vsize (Kb) 170304

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37420 0 3 0 103540 218 0 0 25 0 1 0 1793574123 172482560 36739 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42110 36739 145 145 0 41965 0
[pid=14895] vsize: 168440
Current children cumulated CPU time (s) 1037.58
Current children cumulated vsize (Kb) 170564

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37481 0 3 0 104539 218 0 0 25 0 1 0 1793574123 172732416 36800 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42171 36800 145 145 0 42026 0
[pid=14895] vsize: 168684
Current children cumulated CPU time (s) 1047.57
Current children cumulated vsize (Kb) 170808

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37542 0 3 0 105538 219 0 0 25 0 1 0 1793574123 172978176 36861 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42231 36861 145 145 0 42086 0
[pid=14895] vsize: 168924
Current children cumulated CPU time (s) 1057.57
Current children cumulated vsize (Kb) 171048

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37601 0 3 0 106537 219 0 0 25 0 1 0 1793574123 173219840 36920 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42290 36920 145 145 0 42145 0
[pid=14895] vsize: 169160
Current children cumulated CPU time (s) 1067.56
Current children cumulated vsize (Kb) 171284

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37665 0 3 0 107536 220 0 0 25 0 1 0 1793574123 173490176 36984 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42356 36984 145 145 0 42211 0
[pid=14895] vsize: 169424
Current children cumulated CPU time (s) 1077.56
Current children cumulated vsize (Kb) 171548

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37734 0 3 0 108535 220 0 0 25 0 1 0 1793574123 173776896 37053 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42426 37053 145 145 0 42281 0
[pid=14895] vsize: 169704
Current children cumulated CPU time (s) 1087.55
Current children cumulated vsize (Kb) 171828

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37801 0 3 0 109535 220 0 0 25 0 1 0 1793574123 174047232 37120 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42492 37120 145 145 0 42347 0
[pid=14895] vsize: 169968
Current children cumulated CPU time (s) 1097.55
Current children cumulated vsize (Kb) 172092

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37859 0 3 0 110534 221 0 0 25 0 1 0 1793574123 174284800 37178 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42550 37178 145 145 0 42405 0
[pid=14895] vsize: 170200
Current children cumulated CPU time (s) 1107.55
Current children cumulated vsize (Kb) 172324

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37919 0 3 0 111533 221 0 0 25 0 1 0 1793574123 174526464 37238 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42609 37238 145 145 0 42464 0
[pid=14895] vsize: 170436
Current children cumulated CPU time (s) 1117.54
Current children cumulated vsize (Kb) 172560

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37983 0 3 0 112532 222 0 0 25 0 1 0 1793574123 174796800 37302 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42675 37302 145 145 0 42530 0
[pid=14895] vsize: 170700
Current children cumulated CPU time (s) 1127.54
Current children cumulated vsize (Kb) 172824

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38041 0 3 0 113532 222 0 0 25 0 1 0 1793574123 175030272 37360 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42732 37360 145 145 0 42587 0
[pid=14895] vsize: 170928
Current children cumulated CPU time (s) 1137.54
Current children cumulated vsize (Kb) 173052

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38100 0 3 0 114530 223 0 0 25 0 1 0 1793574123 175271936 37419 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42791 37419 145 145 0 42646 0
[pid=14895] vsize: 171164
Current children cumulated CPU time (s) 1147.53
Current children cumulated vsize (Kb) 173288

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38168 0 3 0 115530 224 0 0 25 0 1 0 1793574123 175554560 37487 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42860 37487 145 145 0 42715 0
[pid=14895] vsize: 171440
Current children cumulated CPU time (s) 1157.54
Current children cumulated vsize (Kb) 173564

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38233 0 3 0 116528 225 0 0 25 0 1 0 1793574123 175824896 37552 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42926 37552 145 145 0 42781 0
[pid=14895] vsize: 171704
Current children cumulated CPU time (s) 1167.53
Current children cumulated vsize (Kb) 173828

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38308 0 3 0 117527 225 0 0 25 0 1 0 1793574123 176119808 37627 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 42998 37627 145 145 0 42853 0
[pid=14895] vsize: 171992
Current children cumulated CPU time (s) 1177.52
Current children cumulated vsize (Kb) 174116

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38388 0 3 0 118526 226 0 0 25 0 1 0 1793574123 176455680 37707 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 43080 37707 145 145 0 42935 0
[pid=14895] vsize: 172320
Current children cumulated CPU time (s) 1187.52
Current children cumulated vsize (Kb) 174444

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38439 0 3 0 119525 226 0 0 25 0 1 0 1793574123 176664576 37758 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 43131 37758 145 145 0 42986 0
[pid=14895] vsize: 172524
Current children cumulated CPU time (s) 1197.51
Current children cumulated vsize (Kb) 174648

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38490 0 3 0 120524 227 0 0 25 0 1 0 1793574123 176869376 37809 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 43181 37809 145 145 0 43036 0
[pid=14895] vsize: 172724
Current children cumulated CPU time (s) 1207.51
Current children cumulated vsize (Kb) 174848



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 14895
Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14891/statm): 531 226 485 147 0 384 0
[pid=14891] vsize: 2124
Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38490 0 3 0 120524 227 0 0 25 0 1 0 1793574123 176869376 37809 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14895/statm): 43181 37809 145 145 0 43036 0
[pid=14895] vsize: 172724
Current children cumulated CPU time (s) 1207.51
Current children cumulated vsize (Kb) 174848

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1207.59
CPU user time (s): 1205.25
CPU system time (s): 2.34364
CPU usage (%): 99.7849
Max. virtual memory (cumulated for all children) (Kb): 174848

Verifier Data

ERROR: no interpretation found !