Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-aflow30a.opb
MD5SUMb74fb9cd57e8b4068255c4ac98aa23ca
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3432
Optimality of the best value was proved NO
Number of terms in the objective function 421
Biggest coefficient in the objective function 500
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 72290
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 12800
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 416734
Number of bits of the biggest sum of numbers19
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.05
Number of variables5932
Total number of constraints1321
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)450
Number of constraints which are nor clauses,nor cardinality constraints871
Minimum length of a constraint1
Maximum length of a constraint453

Trace number 6120

Launcher Data

LAUNCH ON wulflinc2 THE 2005-09-20 03:29:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3283 boxname=wulflinc2 idbench=939 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b74fb9cd57e8b4068255c4ac98aa23ca  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-aflow30a.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-aflow30a.opb
IDLAUNCH: 3283
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        919624 kB
Buffers:          8476 kB
Cached:          81772 kB
SwapCached:        872 kB
Active:          13060 kB
Inactive:        79636 kB
HighTotal:      131008 kB
HighFree:        45304 kB
LowTotal:       903652 kB
LowFree:        874320 kB
SwapTotal:     2097136 kB
SwapFree:      2095548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5516 kB
Slab:            16560 kB
Committed_AS:    72324 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:50:06 (client local time) WITH STATUS 0 IN 1207.19 SECONDS
stats: 3283 7 1207.19 0

Solver Data

c Parsing PB file...
c Converting 958 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1020]---> BDD-cost:   13
c ---[1019]---> BDD-cost:   11
c ---[1018]---> BDD-cost:   11
c ---[1017]---> BDD-cost:   12
c ---[1016]---> BDD-cost:   13
c ---[1015]---> BDD-cost:   12
c ---[1014]---> BDD-cost:   13
c ---[1013]---> BDD-cost:   12
c ---[1012]---> BDD-cost:   13
c ---[1011]---> BDD-cost:   11
c ---[1010]---> BDD-cost:   13
c ---[1009]---> BDD-cost:   13
c ---[1008]---> BDD-cost:   12
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   12
c ---[1005]---> BDD-cost:   13
c ---[1004]---> BDD-cost:   13
c ---[1002]---> BDD-cost:   13
c ---[1001]---> BDD-cost:   13
c ---[1000]---> BDD-cost:   12
c ---[ 999]---> BDD-cost:   13
c ---[ 998]---> BDD-cost:   13
c ---[ 996]---> BDD-cost:   13
c ---[ 995]---> BDD-cost:   12
c ---[ 993]---> BDD-cost:   12
c ---[ 992]---> BDD-cost:   13
c ---[ 991]---> BDD-cost:   12
c ---[ 990]---> BDD-cost:   13
c ---[ 989]---> BDD-cost:   12
c ---[ 988]---> BDD-cost:   12
c ---[ 987]---> BDD-cost:   13
c ---[ 986]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:   12
c ---[ 984]---> BDD-cost:   13
c ---[ 981]---> BDD-cost:   13
c ---[ 980]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   13
c ---[ 977]---> BDD-cost:   12
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   12
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   13
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   13
c ---[ 968]---> BDD-cost:   13
c ---[ 967]---> BDD-cost:   13
c ---[ 966]---> BDD-cost:   12
c ---[ 964]---> BDD-cost:   13
c ---[ 963]---> BDD-cost:   13
c ---[ 962]---> BDD-cost:   12
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   13
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   13
c ---[ 956]---> BDD-cost:   12
c ---[ 955]---> BDD-cost:   13
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   13
c ---[ 952]---> BDD-cost:   13
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   13
c ---[ 949]---> BDD-cost:   13
c ---[ 948]---> BDD-cost:   13
c ---[ 947]---> BDD-cost:   13
c ---[ 946]---> BDD-cost:   13
c ---[ 945]---> BDD-cost:   13
c ---[ 944]---> BDD-cost:   12
c ---[ 943]---> BDD-cost:   13
c ---[ 942]---> BDD-cost:   13
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   13
c ---[ 939]---> BDD-cost:   13
c ---[ 937]---> BDD-cost:   13
c ---[ 936]---> BDD-cost:   12
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   13
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   12
c ---[ 931]---> BDD-cost:   12
c ---[ 930]---> BDD-cost:   13
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   13
c ---[ 926]---> BDD-cost:   13
c ---[ 925]---> BDD-cost:   13
c ---[ 924]---> BDD-cost:   13
c ---[ 923]---> BDD-cost:   11
c ---[ 922]---> BDD-cost:   12
c ---[ 921]---> BDD-cost:   12
c ---[ 919]---> BDD-cost:   12
c ---[ 918]---> BDD-cost:   12
c ---[ 917]---> BDD-cost:   13
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   12
c ---[ 914]---> BDD-cost:   13
c ---[ 913]---> BDD-cost:   13
c ---[ 912]---> BDD-cost:   13
c ---[ 911]---> BDD-cost:   13
c ---[ 910]---> BDD-cost:   12
c ---[ 908]---> BDD-cost:   13
c ---[ 907]---> BDD-cost:   13
c ---[ 906]---> BDD-cost:   12
c ---[ 905]---> BDD-cost:   13
c ---[ 903]---> BDD-cost:   13
c ---[ 902]---> BDD-cost:   13
c ---[ 900]---> BDD-cost:   13
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   12
c ---[ 897]---> BDD-cost:   12
c ---[ 896]---> BDD-cost:   12
c ---[ 895]---> BDD-cost:   13
c ---[ 893]---> BDD-cost:   12
c ---[ 892]---> BDD-cost:   13
c ---[ 891]---> BDD-cost:   11
c ---[ 890]---> BDD-cost:   13
c ---[ 889]---> BDD-cost:   13
c ---[ 888]---> BDD-cost:   13
c ---[ 887]---> BDD-cost:   13
c ---[ 886]---> BDD-cost:   11
c ---[ 885]---> BDD-cost:   13
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   11
c ---[ 881]---> BDD-cost:   13
c ---[ 880]---> BDD-cost:   13
c ---[ 879]---> BDD-cost:   13
c ---[ 878]---> BDD-cost:   12
c ---[ 877]---> BDD-cost:   11
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   13
c ---[ 874]---> BDD-cost:   13
c ---[ 873]---> BDD-cost:   11
c ---[ 871]---> BDD-cost:   12
c ---[ 870]---> BDD-cost:   13
c ---[ 869]---> BDD-cost:   12
c ---[ 867]---> BDD-cost:   11
c ---[ 866]---> BDD-cost:   13
c ---[ 865]---> BDD-cost:   13
c ---[ 863]---> BDD-cost:   13
c ---[ 862]---> BDD-cost:   13
c ---[ 861]---> BDD-cost:   12
c ---[ 860]---> BDD-cost:   13
c ---[ 859]---> BDD-cost:   12
c ---[ 858]---> BDD-cost:   13
c ---[ 857]---> BDD-cost:   12
c ---[ 856]---> BDD-cost:   13
c ---[ 855]---> BDD-cost:   12
c ---[ 853]---> BDD-cost:   13
c ---[ 851]---> BDD-cost:   13
c ---[ 850]---> BDD-cost:   12
c ---[ 849]---> BDD-cost:   11
c ---[ 848]---> BDD-cost:   12
c ---[ 847]---> BDD-cost:   13
c ---[ 846]---> BDD-cost:   12
c ---[ 845]---> BDD-cost:   13
c ---[ 844]---> BDD-cost:   12
c ---[ 843]---> BDD-cost:   12
c ---[ 842]---> BDD-cost:   11
c ---[ 841]---> BDD-cost:   11
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   13
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   12
c ---[ 835]---> BDD-cost:   13
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   13
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 829]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   12
c ---[ 825]---> BDD-cost:   11
c ---[ 824]---> BDD-cost:   13
c ---[ 823]---> BDD-cost:   13
c ---[ 822]---> BDD-cost:   12
c ---[ 821]---> BDD-cost:   13
c ---[ 820]---> BDD-cost:   13
c ---[ 819]---> BDD-cost:   13
c ---[ 818]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:   13
c ---[ 816]---> BDD-cost:   13
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   13
c ---[ 811]---> BDD-cost:   11
c ---[ 809]---> BDD-cost:   12
c ---[ 808]---> BDD-cost:   12
c ---[ 807]---> BDD-cost:   13
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:   12
c ---[ 804]---> BDD-cost:   12
c ---[ 803]---> BDD-cost:   13
c ---[ 801]---> BDD-cost:   13
c ---[ 800]---> BDD-cost:   13
c ---[ 799]---> BDD-cost:   11
c ---[ 798]---> BDD-cost:   12
c ---[ 797]---> BDD-cost:   13
c ---[ 796]---> BDD-cost:   11
c ---[ 795]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   12
c ---[ 791]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   12
c ---[ 789]---> BDD-cost:   11
c ---[ 788]---> BDD-cost:   13
c ---[ 787]---> BDD-cost:   13
c ---[ 786]---> BDD-cost:   13
c ---[ 785]---> BDD-cost:   13
c ---[ 784]---> BDD-cost:   11
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   13
c ---[ 780]---> BDD-cost:   11
c ---[ 779]---> BDD-cost:   13
c ---[ 778]---> BDD-cost:   13
c ---[ 777]---> BDD-cost:   11
c ---[ 776]---> BDD-cost:   11
c ---[ 774]---> BDD-cost:   13
c ---[ 772]---> BDD-cost:   12
c ---[ 771]---> BDD-cost:   13
c ---[ 770]---> BDD-cost:   13
c ---[ 769]---> BDD-cost:   13
c ---[ 768]---> BDD-cost:   13
c ---[ 767]---> BDD-cost:   11
c ---[ 766]---> BDD-cost:   13
c ---[ 764]---> BDD-cost:   13
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   13
c ---[ 761]---> BDD-cost:   13
c ---[ 760]---> BDD-cost:   13
c ---[ 759]---> BDD-cost:   12
c ---[ 758]---> BDD-cost:   12
c ---[ 757]---> BDD-cost:   11
c ---[ 756]---> BDD-cost:   12
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   13
c ---[ 752]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   12
c ---[ 749]---> BDD-cost:   13
c ---[ 747]---> BDD-cost:   12
c ---[ 746]---> BDD-cost:   12
c ---[ 745]---> BDD-cost:   12
c ---[ 744]---> BDD-cost:   11
c ---[ 743]---> BDD-cost:   12
c ---[ 742]---> BDD-cost:   13
c ---[ 741]---> BDD-cost:   11
c ---[ 740]---> BDD-cost:   12
c ---[ 738]---> BDD-cost:   12
c ---[ 737]---> BDD-cost:   12
c ---[ 736]---> BDD-cost:   12
c ---[ 734]---> BDD-cost:   11
c ---[ 733]---> BDD-cost:   12
c ---[ 732]---> BDD-cost:   11
c ---[ 730]---> BDD-cost:   12
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   12
c ---[ 727]---> BDD-cost:   12
c ---[ 726]---> BDD-cost:   12
c ---[ 725]---> BDD-cost:   11
c ---[ 723]---> BDD-cost:   13
c ---[ 722]---> BDD-cost:   12
c ---[ 721]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   13
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   13
c ---[ 717]---> BDD-cost:   12
c ---[ 716]---> BDD-cost:   11
c ---[ 713]---> BDD-cost:   12
c ---[ 712]---> BDD-cost:   11
c ---[ 711]---> BDD-cost:   12
c ---[ 710]---> BDD-cost:   12
c ---[ 708]---> BDD-cost:   13
c ---[ 706]---> BDD-cost:   13
c ---[ 705]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   13
c ---[ 702]---> BDD-cost:   13
c ---[ 701]---> BDD-cost:   13
c ---[ 700]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:   12
c ---[ 698]---> BDD-cost:   13
c ---[ 695]---> BDD-cost:   11
c ---[ 694]---> BDD-cost:   12
c ---[ 693]---> BDD-cost:   13
c ---[ 692]---> BDD-cost:   13
c ---[ 691]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   12
c ---[ 688]---> BDD-cost:   12
c ---[ 687]---> BDD-cost:   11
c ---[ 686]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 683]---> BDD-cost:   11
c ---[ 682]---> BDD-cost:   11
c ---[ 681]---> BDD-cost:   13
c ---[ 680]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:   12
c ---[ 678]---> BDD-cost:   12
c ---[ 677]---> BDD-cost:   12
c ---[ 676]---> BDD-cost:   13
c ---[ 675]---> BDD-cost:   12
c ---[ 673]---> BDD-cost:   11
c ---[ 672]---> BDD-cost:   13
c ---[ 671]---> BDD-cost:   13
c ---[ 670]---> BDD-cost:   13
c ---[ 668]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:   13
c ---[ 666]---> BDD-cost:   11
c ---[ 665]---> BDD-cost:   12
c ---[ 664]---> BDD-cost:   12
c ---[ 663]---> BDD-cost:   13
c ---[ 662]---> BDD-cost:   13
c ---[ 661]---> BDD-cost:   12
c ---[ 660]---> BDD-cost:   11
c ---[ 659]---> BDD-cost:   13
c ---[ 658]---> BDD-cost:   13
c ---[ 657]---> BDD-cost:   12
c ---[ 656]---> BDD-cost:   13
c ---[ 655]---> BDD-cost:   12
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   12
c ---[ 649]---> BDD-cost:   12
c ---[ 648]---> BDD-cost:   12
c ---[ 647]---> BDD-cost:   13
c ---[ 645]---> BDD-cost:   13
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   13
c ---[ 642]---> BDD-cost:   13
c ---[ 640]---> BDD-cost:   12
c ---[ 638]---> BDD-cost:   13
c ---[ 637]---> BDD-cost:   12
c ---[ 636]---> BDD-cost:   13
c ---[ 635]---> BDD-cost:   12
c ---[ 634]---> BDD-cost:   11
c ---[ 633]---> BDD-cost:   12
c ---[ 632]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:   12
c ---[ 630]---> BDD-cost:   13
c ---[ 628]---> BDD-cost:   12
c ---[ 627]---> BDD-cost:   13
c ---[ 625]---> BDD-cost:   13
c ---[ 624]---> BDD-cost:   13
c ---[ 623]---> BDD-cost:   12
c ---[ 622]---> BDD-cost:   12
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   12
c ---[ 619]---> BDD-cost:   13
c ---[ 618]---> BDD-cost:   11
c ---[ 617]---> BDD-cost:   11
c ---[ 616]---> BDD-cost:   13
c ---[ 615]---> BDD-cost:   13
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   12
c ---[ 608]---> BDD-cost:   12
c ---[ 607]---> BDD-cost:   13
c ---[ 606]---> BDD-cost:   11
c ---[ 605]---> BDD-cost:   13
c ---[ 604]---> BDD-cost:   11
c ---[ 603]---> BDD-cost:   13
c ---[ 602]---> BDD-cost:   13
c ---[ 601]---> BDD-cost:   13
c ---[ 600]---> BDD-cost:   10
c ---[ 598]---> BDD-cost:   17
c ---[ 596]---> BDD-cost:   25
c ---[ 595]---> BDD-cost:    8
c ---[ 594]---> BDD-cost:    4
c ---[ 593]---> BDD-cost:    8
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    6
c ---[ 590]---> BDD-cost:    8
c ---[ 589]---> BDD-cost:    8
c ---[ 588]---> BDD-cost:    8
c ---[ 587]---> BDD-cost:    5
c ---[ 586]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:   27
c ---[ 583]---> BDD-cost:    8
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    6
c ---[ 577]---> BDD-cost:    6
c ---[ 576]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    8
c ---[ 572]---> BDD-cost:   29
c ---[ 571]---> BDD-cost:    8
c ---[ 570]---> BDD-cost:    5
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    6
c ---[ 567]---> BDD-cost:   18
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    5
c ---[ 562]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:   27
c ---[ 559]---> BDD-cost:    8
c ---[ 558]---> BDD-cost:    8
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    6
c ---[ 554]---> BDD-cost:    5
c ---[ 553]---> BDD-cost:   15
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   17
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    6
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    6
c ---[ 541]---> BDD-cost:    8
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 538]---> BDD-cost:    8
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   16
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   15
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   17
c ---[ 524]---> BDD-cost:   27
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    8
c ---[ 521]---> BDD-cost:    6
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    6
c ---[ 514]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:    5
c ---[ 510]---> BDD-cost:    5
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    6
c ---[ 506]---> BDD-cost:    5
c ---[ 505]---> BDD-cost:    6
c ---[ 504]---> BDD-cost:    6
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    4
c ---[ 500]---> BDD-cost:   31
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:   18
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   15
c ---[ 493]---> BDD-cost:   18
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    6
c ---[ 490]---> BDD-cost:    8
c ---[ 488]---> BDD-cost:   25
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    8
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    8
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    5
c ---[ 480]---> BDD-cost:    8
c ---[ 479]---> BDD-cost:   16
c ---[ 478]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   33
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    4
c ---[ 471]---> BDD-cost:    6
c ---[ 470]---> BDD-cost:    6
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    6
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    8
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:   18
c ---[ 456]---> BDD-cost:    4
c ---[ 455]---> BDD-cost:    4
c ---[ 454]---> BDD-cost:    6
c ---[ 453]---> BDD-cost:    4
c ---[ 452]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:   17
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    8
c ---[ 441]---> BDD-cost:    8
c ---[ 440]---> BDD-cost:    8
c ---[ 438]---> BDD-cost:   35
c ---[ 437]---> BDD-cost:   16
c ---[ 436]---> BDD-cost:    8
c ---[ 435]---> BDD-cost:    6
c ---[ 434]---> BDD-cost:    8
c ---[ 433]---> BDD-cost:    8
c ---[ 432]---> BDD-cost:    8
c ---[ 431]---> BDD-cost:    8
c ---[ 430]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    8
c ---[ 426]---> BDD-cost:   27
c ---[ 425]---> BDD-cost:   17
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:   17
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:   17
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:   31
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    8
c ---[ 398]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    5
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    4
c ---[ 392]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost:   17
c ---[ 388]---> BDD-cost:   17
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    5
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:   16
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    8
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    5
c ---[ 371]---> BDD-cost:    5
c ---[ 370]---> BDD-cost:    8
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    5
c ---[ 366]---> BDD-cost:   33
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    5
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   16
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> Adder-cost: 693   maxlim: 102262   bits: 18/17
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   19
c ---[ 347]---> BDD-cost:   15
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> Adder-cost: 572   maxlim: 148723   bits: 18/18
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   17
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:   19
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> Adder-cost: 880   maxlim: 181231   bits: 19/18
c ---[ 327]---> BDD-cost:    5
c ---[ 326]---> BDD-cost:    7
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    5
c ---[ 322]---> BDD-cost:    6
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    3
c ---[ 318]---> BDD-cost:    6
c ---[ 316]---> Adder-cost: 820   maxlim: 146161   bits: 19/18
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   16
c ---[ 312]---> BDD-cost:   16
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    4
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:   19
c ---[ 304]---> Adder-cost: 838   maxlim: 185456   bits: 19/18
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   14
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> Adder-cost: 546   maxlim: 93302   bits: 18/17
c ---[ 291]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    8
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> Adder-cost: 720   maxlim: 163185   bits: 19/18
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   15
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    6
c ---[ 268]---> Adder-cost: 768   maxlim: 162802   bits: 19/18
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   17
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   19
c ---[ 259]---> BDD-cost:   19
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> Adder-cost: 800   maxlim: 202094   bits: 19/18
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   14
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> Adder-cost: 670   maxlim: 163442   bits: 19/18
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    7
c ---[ 239]---> BDD-cost:    5
c ---[ 238]---> BDD-cost:    7
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    4
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> Adder-cost: 706   maxlim: 157169   bits: 19/18
c ---[ 229]---> BDD-cost:    5
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    4
c ---[ 225]---> BDD-cost:    5
c ---[ 224]---> BDD-cost:   19
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   18
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> Adder-cost: 762   maxlim: 147056   bits: 19/18
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   17
c ---[ 215]---> BDD-cost:    6
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    7
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 206]---> Adder-cost: 759   maxlim: 130929   bits: 18/17
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> Adder-cost: 696   maxlim: 101365   bits: 18/17
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    6
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:    5
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:   18
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> Adder-cost: 614   maxlim: 144627   bits: 19/18
c ---[ 181]---> BDD-cost:    6
c ---[ 180]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    6
c ---[ 178]---> BDD-cost:    7
c ---[ 177]---> BDD-cost:    3
c ---[ 176]---> BDD-cost:    4
c ---[ 175]---> BDD-cost:    7
c ---[ 174]---> BDD-cost:    8
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    6
c ---[ 170]---> Adder-cost: 764   maxlim: 174961   bits: 19/18
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   17
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    5
c ---[ 163]---> BDD-cost:    5
c ---[ 162]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    7
c ---[ 160]---> BDD-cost:   17
c ---[ 158]---> Adder-cost: 548   maxlim: 159603   bits: 18/18
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:    7
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    4
c ---[ 149]---> BDD-cost:   19
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> Adder-cost: 824   maxlim: 173423   bits: 19/18
c ---[ 145]---> BDD-cost:    6
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    4
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    7
c ---[ 140]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> Adder-cost: 858   maxlim: 137074   bits: 19/18
c ---[ 132]---> Adder-cost: 786   maxlim: 177902   bits: 19/18
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> Adder-cost: 602   maxlim: 120053   bits: 18/17
c ---[ 126]---> Adder-cost: 646   maxlim: 154865   bits: 18/18
c ---[ 124]---> Adder-cost: 864   maxlim: 214125   bits: 19/18
c ---[ 122]---> Adder-cost: 710   maxlim: 143089   bits: 19/18
c ---[ 120]---> Adder-cost: 614   maxlim: 83701   bits: 18/17
c ---[ 118]---> Adder-cost: 706   maxlim: 144239   bits: 19/18
c ---[ 116]---> Adder-cost: 826   maxlim: 169330   bits: 19/18
c ---[ 114]---> Adder-cost: 604   maxlim: 130932   bits: 18/17
c ---[ 112]---> Adder-cost: 816   maxlim: 175726   bits: 19/18
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   17
c ---[ 105]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    5
c ---[ 103]---> BDD-cost:    6
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  97]---> BDD-cost:   27
c ---[  96]---> BDD-cost:    6
c ---[  95]---> BDD-cost:    7
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    6
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    6
c ---[  80]---> BDD-cost:    7
c ---[  79]---> BDD-cost:    7
c ---[  78]---> BDD-cost:   19
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   19
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    6
c ---[  63]---> BDD-cost:    4
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  154476   536995 |   51492       0        0     nan |  0.000 % |
c |       100 |  154450   536907 |   56641      93     1380    14.8 |  6.247 % |
c |       250 |  154450   536907 |   62305     243     2994    12.3 |  6.247 % |
c |       475 |  154441   536876 |   68535     465     3905     8.4 |  6.250 % |
c |       815 |  154409   536768 |   75389     797    20804    26.1 |  6.263 % |
c |      1322 |  154400   536737 |   82928    1302    40396    31.0 |  6.266 % |
c |      2084 |  154383   536680 |   91221    2060    93577    45.4 |  6.272 % |
c |      3224 |  154357   536592 |  100343    3195   214305    67.1 |  6.282 % |
c |      4932 |  154348   536561 |  110377    4899   357619    73.0 |  6.285 % |
c |      7494 |  154338   536523 |  121415    7449   459667    61.7 |  6.289 % |
c |     11341 |  154313   536440 |  133556   11292   982431    87.0 |  6.298 % |
c |     17108 |  154313   536440 |  146912   17059  1987803   116.5 |  6.298 % |
c |     25759 |  154313   536440 |  161603   25710  3433341   133.5 |  6.298 % |
c |     38734 |  154313   536440 |  177764   38685  5706055   147.5 |  6.298 % |
c |     58196 |  154305   536414 |  195540   58146  9180394   157.9 |  6.302 % |
c |     87389 |  154305   536414 |  215094   87339 14190965   162.5 |  6.302 % |
c |    131179 |  154296   536383 |  236604  131127 21427368   163.4 |  6.305 % |

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/7999/stat): 7999 (minisat+_script) R 7998 7999 6872 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797091657 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7999/statm): 174 3 169 147 0 27 0
[pid=7999] 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=8000
New process pid=8001
New process pid=8002
execve syscall for /bin/sed executable
One traced child (pid=8001) 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=8002) exited with status: 0
One traced child (pid=8000) exited with status: 0
New process pid=8003
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-aflow30a.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.95 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 3514 0 0 0 964 15 0 0 25 0 1 0 1797091662 15343616 3420 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 3746 3420 145 145 0 3601 0
[pid=8003] vsize: 14984
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 17108

[startup+20.0055 s]
Raw data (loadavg): 0.94 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 3771 0 0 0 1958 18 0 0 25 0 1 0 1797091662 16396288 3677 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 4003 3677 145 145 0 3858 0
[pid=8003] vsize: 16012
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 18136

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 4186 0 0 0 2950 22 0 0 25 0 1 0 1797091662 18108416 4092 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 4421 4092 145 145 0 4276 0
[pid=8003] vsize: 17684
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 19808

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 4722 0 0 0 3941 26 0 0 25 0 1 0 1797091662 20291584 4628 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 4954 4628 145 145 0 4809 0
[pid=8003] vsize: 19816
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 21940

[startup+50.0076 s]
Raw data (loadavg): 0.96 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 5210 0 0 0 4931 30 0 0 25 0 1 0 1797091662 22282240 5116 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 5440 5116 145 145 0 5295 0
[pid=8003] vsize: 21760
Current children cumulated CPU time (s) 49.63
Current children cumulated vsize (Kb) 23884

[startup+60.0083 s]
Raw data (loadavg): 0.97 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 5659 0 0 0 5922 34 0 0 25 0 1 0 1797091662 24178688 5565 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 5903 5565 145 145 0 5758 0
[pid=8003] vsize: 23612
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 25736

[startup+70.01 s]
Raw data (loadavg): 0.97 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 6073 0 0 0 6912 37 0 0 25 0 1 0 1797091662 25866240 5979 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 6315 5979 145 145 0 6170 0
[pid=8003] vsize: 25260
Current children cumulated CPU time (s) 69.51
Current children cumulated vsize (Kb) 27384

[startup+80.0107 s]
Raw data (loadavg): 0.98 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 6513 0 0 0 7904 40 0 0 25 0 1 0 1797091662 27660288 6419 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 6753 6419 145 145 0 6608 0
[pid=8003] vsize: 27012
Current children cumulated CPU time (s) 79.46
Current children cumulated vsize (Kb) 29136

[startup+90.0104 s]
Raw data (loadavg): 0.98 0.96 0.86 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 6911 0 0 0 8897 43 0 0 25 0 1 0 1797091662 29282304 6817 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 7149 6817 145 145 0 7004 0
[pid=8003] vsize: 28596
Current children cumulated CPU time (s) 89.42
Current children cumulated vsize (Kb) 30720

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 7289 0 0 0 9889 46 0 0 25 0 1 0 1797091662 30822400 7195 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 7525 7195 145 145 0 7380 0
[pid=8003] vsize: 30100
Current children cumulated CPU time (s) 99.37
Current children cumulated vsize (Kb) 32224

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 7686 0 0 0 10883 48 0 0 25 0 1 0 1797091662 32444416 7592 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 7921 7592 145 145 0 7776 0
[pid=8003] vsize: 31684
Current children cumulated CPU time (s) 109.33
Current children cumulated vsize (Kb) 33808

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 8092 0 0 0 11876 51 0 0 25 0 1 0 1797091662 34115584 7998 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 8329 7998 145 145 0 8184 0
[pid=8003] vsize: 33316
Current children cumulated CPU time (s) 119.29
Current children cumulated vsize (Kb) 35440

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 8557 0 0 0 12868 54 0 0 25 0 1 0 1797091662 36151296 8463 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 8826 8463 145 145 0 8681 0
[pid=8003] vsize: 35304
Current children cumulated CPU time (s) 129.24
Current children cumulated vsize (Kb) 37428

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 8905 0 0 0 13861 58 0 0 25 0 1 0 1797091662 37593088 8811 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 9178 8811 145 145 0 9033 0
[pid=8003] vsize: 36712
Current children cumulated CPU time (s) 139.21
Current children cumulated vsize (Kb) 38836

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 9230 0 0 0 14856 61 0 0 25 0 1 0 1797091662 38916096 9136 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 9501 9136 145 145 0 9356 0
[pid=8003] vsize: 38004
Current children cumulated CPU time (s) 149.19
Current children cumulated vsize (Kb) 40128

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 9604 0 0 0 15850 63 0 0 25 0 1 0 1797091662 40448000 9510 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 9875 9510 145 145 0 9730 0
[pid=8003] vsize: 39500
Current children cumulated CPU time (s) 159.15
Current children cumulated vsize (Kb) 41624

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 9948 0 0 0 16845 65 0 0 25 0 1 0 1797091662 41873408 9854 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 10223 9854 145 145 0 10078 0
[pid=8003] vsize: 40892
Current children cumulated CPU time (s) 169.12
Current children cumulated vsize (Kb) 43016

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 10247 0 0 0 17839 68 0 0 25 0 1 0 1797091662 43126784 10153 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 10529 10153 145 145 0 10384 0
[pid=8003] vsize: 42116
Current children cumulated CPU time (s) 179.09
Current children cumulated vsize (Kb) 44240

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 10512 0 0 0 18836 69 0 0 25 0 1 0 1797091662 44216320 10418 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 10795 10418 145 145 0 10650 0
[pid=8003] vsize: 43180
Current children cumulated CPU time (s) 189.07
Current children cumulated vsize (Kb) 45304

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 10823 0 0 0 19829 72 0 0 25 0 1 0 1797091662 45494272 10729 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 11107 10729 145 145 0 10962 0
[pid=8003] vsize: 44428
Current children cumulated CPU time (s) 199.03
Current children cumulated vsize (Kb) 46552

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 11137 0 0 0 20823 74 0 0 25 0 1 0 1797091662 46764032 11043 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 11417 11043 145 145 0 11272 0
[pid=8003] vsize: 45668
Current children cumulated CPU time (s) 208.99
Current children cumulated vsize (Kb) 47792

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 11412 0 0 0 21817 76 0 0 25 0 1 0 1797091662 47886336 11318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 11691 11318 145 145 0 11546 0
[pid=8003] vsize: 46764
Current children cumulated CPU time (s) 218.95
Current children cumulated vsize (Kb) 48888

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 11664 0 0 0 22813 78 0 0 25 0 1 0 1797091662 48910336 11570 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 11941 11570 145 145 0 11796 0
[pid=8003] vsize: 47764
Current children cumulated CPU time (s) 228.93
Current children cumulated vsize (Kb) 49888

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 11903 0 0 0 23808 79 0 0 25 0 1 0 1797091662 49905664 11809 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 12184 11809 145 145 0 12039 0
[pid=8003] vsize: 48736
Current children cumulated CPU time (s) 238.89
Current children cumulated vsize (Kb) 50860

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 12114 0 0 0 24805 80 0 0 25 0 1 0 1797091662 50778112 12020 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 12397 12020 145 145 0 12252 0
[pid=8003] vsize: 49588
Current children cumulated CPU time (s) 248.87
Current children cumulated vsize (Kb) 51712

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 12352 0 0 0 25801 83 0 0 25 0 1 0 1797091662 51757056 12258 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 12636 12258 145 145 0 12491 0
[pid=8003] vsize: 50544
Current children cumulated CPU time (s) 258.86
Current children cumulated vsize (Kb) 52668

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 12582 0 0 0 26796 84 0 0 25 0 1 0 1797091662 52703232 12488 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 12867 12488 145 145 0 12722 0
[pid=8003] vsize: 51468
Current children cumulated CPU time (s) 268.82
Current children cumulated vsize (Kb) 53592

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 12819 0 0 0 27793 85 0 0 25 0 1 0 1797091662 53673984 12725 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 13104 12725 145 145 0 12959 0
[pid=8003] vsize: 52416
Current children cumulated CPU time (s) 278.8
Current children cumulated vsize (Kb) 54540

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 13050 0 0 0 28789 87 0 0 25 0 1 0 1797091662 54628352 12956 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 13337 12956 145 145 0 13192 0
[pid=8003] vsize: 53348
Current children cumulated CPU time (s) 288.78
Current children cumulated vsize (Kb) 55472

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.88 1/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) T 7999 7999 6872 0 -1 0 13281 0 0 0 29784 89 0 0 25 0 1 0 1797091662 55578624 13187 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8003/statm): 13569 13187 145 145 0 13424 0
[pid=8003] vsize: 54276
Current children cumulated CPU time (s) 298.75
Current children cumulated vsize (Kb) 56400

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 13510 0 0 0 30780 91 0 0 25 0 1 0 1797091662 56504320 13416 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 13795 13416 145 145 0 13650 0
[pid=8003] vsize: 55180
Current children cumulated CPU time (s) 308.73
Current children cumulated vsize (Kb) 57304

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 13764 0 0 0 31775 93 0 0 25 0 1 0 1797091662 57552896 13670 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 14051 13670 145 145 0 13906 0
[pid=8003] vsize: 56204
Current children cumulated CPU time (s) 318.7
Current children cumulated vsize (Kb) 58328

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 13998 0 0 0 32770 96 0 0 25 0 1 0 1797091662 58511360 13904 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 14285 13904 145 145 0 14140 0
[pid=8003] vsize: 57140
Current children cumulated CPU time (s) 328.68
Current children cumulated vsize (Kb) 59264

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 14231 0 0 0 33766 97 0 0 25 0 1 0 1797091662 59482112 14137 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 14522 14137 145 145 0 14377 0
[pid=8003] vsize: 58088
Current children cumulated CPU time (s) 338.65
Current children cumulated vsize (Kb) 60212

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 14439 0 0 0 34763 98 0 0 25 0 1 0 1797091662 60338176 14345 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 14731 14345 145 145 0 14586 0
[pid=8003] vsize: 58924
Current children cumulated CPU time (s) 348.63
Current children cumulated vsize (Kb) 61048

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 14655 0 0 0 35759 100 0 0 25 0 1 0 1797091662 61214720 14561 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 14945 14561 145 145 0 14800 0
[pid=8003] vsize: 59780
Current children cumulated CPU time (s) 358.61
Current children cumulated vsize (Kb) 61904

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 14881 0 0 0 36756 101 0 0 25 0 1 0 1797091662 62410752 14787 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 15237 14787 145 145 0 15092 0
[pid=8003] vsize: 60948
Current children cumulated CPU time (s) 368.59
Current children cumulated vsize (Kb) 63072

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 15076 0 0 0 37753 103 0 0 25 0 1 0 1797091662 63221760 14982 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 15435 14982 145 145 0 15290 0
[pid=8003] vsize: 61740
Current children cumulated CPU time (s) 378.58
Current children cumulated vsize (Kb) 63864

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 15316 0 0 0 38750 104 0 0 25 0 1 0 1797091662 64217088 15222 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 15678 15222 145 145 0 15533 0
[pid=8003] vsize: 62712
Current children cumulated CPU time (s) 388.56
Current children cumulated vsize (Kb) 64836

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 15568 0 0 0 39745 106 0 0 25 0 1 0 1797091662 65228800 15474 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 15925 15474 145 145 0 15780 0
[pid=8003] vsize: 63700
Current children cumulated CPU time (s) 398.53
Current children cumulated vsize (Kb) 65824

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 15803 0 0 0 40740 109 0 0 25 0 1 0 1797091662 66195456 15709 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 16161 15709 145 145 0 16016 0
[pid=8003] vsize: 64644
Current children cumulated CPU time (s) 408.51
Current children cumulated vsize (Kb) 66768

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 16044 0 0 0 41737 110 0 0 25 0 1 0 1797091662 67203072 15950 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 16407 15950 145 145 0 16262 0
[pid=8003] vsize: 65628
Current children cumulated CPU time (s) 418.49
Current children cumulated vsize (Kb) 67752

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 16293 0 0 0 42732 112 0 0 25 0 1 0 1797091662 68210688 16199 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 16653 16199 145 145 0 16508 0
[pid=8003] vsize: 66612
Current children cumulated CPU time (s) 428.46
Current children cumulated vsize (Kb) 68736

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 16527 0 0 0 43727 114 0 0 25 0 1 0 1797091662 69160960 16433 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 16885 16433 145 145 0 16740 0
[pid=8003] vsize: 67540
Current children cumulated CPU time (s) 438.43
Current children cumulated vsize (Kb) 69664

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 16779 0 0 0 44723 116 0 0 25 0 1 0 1797091662 70189056 16685 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 17136 16685 145 145 0 16991 0
[pid=8003] vsize: 68544
Current children cumulated CPU time (s) 448.41
Current children cumulated vsize (Kb) 70668

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 17051 0 0 0 45719 118 0 0 25 0 1 0 1797091662 71278592 16957 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 17402 16957 145 145 0 17257 0
[pid=8003] vsize: 69608
Current children cumulated CPU time (s) 458.39
Current children cumulated vsize (Kb) 71732

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 17298 0 0 0 46716 119 0 0 25 0 1 0 1797091662 72298496 17204 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 17651 17204 145 145 0 17506 0
[pid=8003] vsize: 70604
Current children cumulated CPU time (s) 468.37
Current children cumulated vsize (Kb) 72728

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.90 1/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) T 7999 7999 6872 0 -1 0 17515 0 0 0 47712 121 0 0 25 0 1 0 1797091662 73216000 17421 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8003/statm): 17875 17421 145 145 0 17730 0
[pid=8003] vsize: 71500
Current children cumulated CPU time (s) 478.35
Current children cumulated vsize (Kb) 73624

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 17766 0 0 0 48707 123 0 0 25 0 1 0 1797091662 74289152 17672 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 18137 17672 145 145 0 17992 0
[pid=8003] vsize: 72548
Current children cumulated CPU time (s) 488.32
Current children cumulated vsize (Kb) 74672

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 18005 0 0 0 49704 124 0 0 25 0 1 0 1797091662 75251712 17911 4294967295 134512640 135094434 3221224432 3221223120 134554715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 18372 17911 145 145 0 18227 0
[pid=8003] vsize: 73488
Current children cumulated CPU time (s) 498.3
Current children cumulated vsize (Kb) 75612

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 18247 0 0 0 50699 126 0 0 25 0 1 0 1797091662 76234752 18153 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 18612 18153 145 145 0 18467 0
[pid=8003] vsize: 74448
Current children cumulated CPU time (s) 508.27
Current children cumulated vsize (Kb) 76572

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 18498 0 0 0 51695 127 0 0 25 0 1 0 1797091662 77291520 18404 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 18870 18404 145 145 0 18725 0
[pid=8003] vsize: 75480
Current children cumulated CPU time (s) 518.24
Current children cumulated vsize (Kb) 77604

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 18738 0 0 0 52691 129 0 0 25 0 1 0 1797091662 78290944 18644 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 19114 18644 145 145 0 18969 0
[pid=8003] vsize: 76456
Current children cumulated CPU time (s) 528.22
Current children cumulated vsize (Kb) 78580

[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 18957 0 0 0 53687 131 0 0 25 0 1 0 1797091662 79179776 18863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 19331 18863 145 145 0 19186 0
[pid=8003] vsize: 77324
Current children cumulated CPU time (s) 538.2
Current children cumulated vsize (Kb) 79448

[startup+550.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 19181 0 0 0 54683 132 0 0 25 0 1 0 1797091662 80146432 19087 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 19567 19087 145 145 0 19422 0
[pid=8003] vsize: 78268
Current children cumulated CPU time (s) 548.17
Current children cumulated vsize (Kb) 80392

[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 19352 0 0 0 55680 133 0 0 25 0 1 0 1797091662 80842752 19258 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 19737 19258 145 145 0 19592 0
[pid=8003] vsize: 78948
Current children cumulated CPU time (s) 558.15
Current children cumulated vsize (Kb) 81072

[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 19530 0 0 0 56677 135 0 0 25 0 1 0 1797091662 81604608 19436 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 19923 19436 145 145 0 19778 0
[pid=8003] vsize: 79692
Current children cumulated CPU time (s) 568.14
Current children cumulated vsize (Kb) 81816

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 19719 0 0 0 57675 136 0 0 25 0 1 0 1797091662 82403328 19625 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 20118 19625 145 145 0 19973 0
[pid=8003] vsize: 80472
Current children cumulated CPU time (s) 578.13
Current children cumulated vsize (Kb) 82596

[startup+590.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 19886 0 0 0 58672 137 0 0 25 0 1 0 1797091662 83083264 19792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 20284 19792 145 145 0 20139 0
[pid=8003] vsize: 81136
Current children cumulated CPU time (s) 588.11
Current children cumulated vsize (Kb) 83260

[startup+600.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 20091 0 0 0 59669 138 0 0 25 0 1 0 1797091662 83927040 19997 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 20490 19997 145 145 0 20345 0
[pid=8003] vsize: 81960
Current children cumulated CPU time (s) 598.09
Current children cumulated vsize (Kb) 84084

[startup+610.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 20304 0 0 0 60666 140 0 0 25 0 1 0 1797091662 84791296 20210 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 20701 20210 145 145 0 20556 0
[pid=8003] vsize: 82804
Current children cumulated CPU time (s) 608.08
Current children cumulated vsize (Kb) 84928

[startup+620.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 20507 0 0 0 61662 141 0 0 25 0 1 0 1797091662 85630976 20413 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 20906 20413 145 145 0 20761 0
[pid=8003] vsize: 83624
Current children cumulated CPU time (s) 618.05
Current children cumulated vsize (Kb) 85748

[startup+630.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 20736 0 0 0 62657 144 0 0 25 0 1 0 1797091662 86556672 20642 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 21132 20642 145 145 0 20987 0
[pid=8003] vsize: 84528
Current children cumulated CPU time (s) 628.03
Current children cumulated vsize (Kb) 86652

[startup+640.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 20941 0 0 0 63654 145 0 0 25 0 1 0 1797091662 87437312 20847 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 21347 20847 145 145 0 21202 0
[pid=8003] vsize: 85388
Current children cumulated CPU time (s) 638.01
Current children cumulated vsize (Kb) 87512

[startup+650.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 21147 0 0 0 64650 146 0 0 25 0 1 0 1797091662 88297472 21053 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 21557 21053 145 145 0 21412 0
[pid=8003] vsize: 86228
Current children cumulated CPU time (s) 647.98
Current children cumulated vsize (Kb) 88352

[startup+660.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 21390 0 0 0 65647 147 0 0 25 0 1 0 1797091662 89296896 21296 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 21801 21296 145 145 0 21656 0
[pid=8003] vsize: 87204
Current children cumulated CPU time (s) 657.96
Current children cumulated vsize (Kb) 89328

[startup+670.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 21625 0 0 0 66644 149 0 0 25 0 1 0 1797091662 90271744 21531 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 22039 21531 145 145 0 21894 0
[pid=8003] vsize: 88156
Current children cumulated CPU time (s) 667.95
Current children cumulated vsize (Kb) 90280

[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 21818 0 0 0 67641 150 0 0 25 0 1 0 1797091662 91049984 21724 4294967295 134512640 135094434 3221224432 3221223024 134552003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 22229 21724 145 145 0 22084 0
[pid=8003] vsize: 88916
Current children cumulated CPU time (s) 677.93
Current children cumulated vsize (Kb) 91040

[startup+690.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 21965 0 0 0 68639 151 0 0 25 0 1 0 1797091662 91676672 21871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 22382 21871 145 145 0 22237 0
[pid=8003] vsize: 89528
Current children cumulated CPU time (s) 687.92
Current children cumulated vsize (Kb) 91652

[startup+700.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 22156 0 0 0 69637 152 0 0 25 0 1 0 1797091662 92483584 22062 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 22579 22062 145 145 0 22434 0
[pid=8003] vsize: 90316
Current children cumulated CPU time (s) 697.91
Current children cumulated vsize (Kb) 92440

[startup+710.059 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 22351 0 0 0 70633 153 0 0 25 0 1 0 1797091662 93274112 22257 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 22772 22257 145 145 0 22627 0
[pid=8003] vsize: 91088
Current children cumulated CPU time (s) 707.88
Current children cumulated vsize (Kb) 93212

[startup+720.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 22569 0 0 0 71630 154 0 0 25 0 1 0 1797091662 94175232 22475 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 22992 22475 145 145 0 22847 0
[pid=8003] vsize: 91968
Current children cumulated CPU time (s) 717.86
Current children cumulated vsize (Kb) 94092

[startup+730.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 22756 0 0 0 72627 156 0 0 25 0 1 0 1797091662 94937088 22662 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 23178 22662 145 145 0 23033 0
[pid=8003] vsize: 92712
Current children cumulated CPU time (s) 727.85
Current children cumulated vsize (Kb) 94836

[startup+740.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 22921 0 0 0 73624 157 0 0 25 0 1 0 1797091662 95641600 22827 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 23350 22827 145 145 0 23205 0
[pid=8003] vsize: 93400
Current children cumulated CPU time (s) 737.83
Current children cumulated vsize (Kb) 95524

[startup+750.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 23097 0 0 0 74622 158 0 0 25 0 1 0 1797091662 96350208 23003 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 23523 23003 145 145 0 23378 0
[pid=8003] vsize: 94092
Current children cumulated CPU time (s) 747.82
Current children cumulated vsize (Kb) 96216

[startup+760.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 23294 0 0 0 75619 159 0 0 25 0 1 0 1797091662 97148928 23200 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 23718 23200 145 145 0 23573 0
[pid=8003] vsize: 94872
Current children cumulated CPU time (s) 757.8
Current children cumulated vsize (Kb) 96996

[startup+770.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 23491 0 0 0 76616 161 0 0 25 0 1 0 1797091662 97927168 23397 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 23908 23397 145 145 0 23763 0
[pid=8003] vsize: 95632
Current children cumulated CPU time (s) 767.79
Current children cumulated vsize (Kb) 97756

[startup+780.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 23693 0 0 0 77613 162 0 0 25 0 1 0 1797091662 98758656 23599 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 24111 23599 145 145 0 23966 0
[pid=8003] vsize: 96444
Current children cumulated CPU time (s) 777.77
Current children cumulated vsize (Kb) 98568

[startup+790.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 23900 0 0 0 78608 165 0 0 25 0 1 0 1797091662 99594240 23806 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 24315 23806 145 145 0 24170 0
[pid=8003] vsize: 97260
Current children cumulated CPU time (s) 787.75
Current children cumulated vsize (Kb) 99384

[startup+800.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 24133 0 0 0 79604 166 0 0 25 0 1 0 1797091662 100593664 24039 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 24559 24039 145 145 0 24414 0
[pid=8003] vsize: 98236
Current children cumulated CPU time (s) 797.72
Current children cumulated vsize (Kb) 100360

[startup+810.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 24318 0 0 0 80601 168 0 0 25 0 1 0 1797091662 101343232 24224 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 24742 24224 145 145 0 24597 0
[pid=8003] vsize: 98968
Current children cumulated CPU time (s) 807.71
Current children cumulated vsize (Kb) 101092

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 24515 0 0 0 81597 169 0 0 25 0 1 0 1797091662 102158336 24421 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 24941 24421 145 145 0 24796 0
[pid=8003] vsize: 99764
Current children cumulated CPU time (s) 817.68
Current children cumulated vsize (Kb) 101888

[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 24721 0 0 0 82594 171 0 0 25 0 1 0 1797091662 103038976 24627 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 25156 24627 145 145 0 25011 0
[pid=8003] vsize: 100624
Current children cumulated CPU time (s) 827.67
Current children cumulated vsize (Kb) 102748

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 24921 0 0 0 83591 172 0 0 25 0 1 0 1797091662 103841792 24827 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 25352 24827 145 145 0 25207 0
[pid=8003] vsize: 101408
Current children cumulated CPU time (s) 837.65
Current children cumulated vsize (Kb) 103532

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 25114 0 0 0 84588 173 0 0 25 0 1 0 1797091662 104607744 25020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 25539 25020 145 145 0 25394 0
[pid=8003] vsize: 102156
Current children cumulated CPU time (s) 847.63
Current children cumulated vsize (Kb) 104280

[startup+860.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 25307 0 0 0 85586 174 0 0 25 0 1 0 1797091662 105472000 25213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 25750 25213 145 145 0 25605 0
[pid=8003] vsize: 103000
Current children cumulated CPU time (s) 857.62
Current children cumulated vsize (Kb) 105124

[startup+870.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 25490 0 0 0 86584 175 0 0 25 0 1 0 1797091662 106303488 25396 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 25953 25396 145 145 0 25808 0
[pid=8003] vsize: 103812
Current children cumulated CPU time (s) 867.61
Current children cumulated vsize (Kb) 105936

[startup+880.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 25613 0 0 0 87583 175 0 0 25 0 1 0 1797091662 106754048 25519 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 26063 25519 145 145 0 25918 0
[pid=8003] vsize: 104252
Current children cumulated CPU time (s) 877.6
Current children cumulated vsize (Kb) 106376

[startup+890.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 25761 0 0 0 88581 176 0 0 25 0 1 0 1797091662 107413504 25667 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 26224 25667 145 145 0 26079 0
[pid=8003] vsize: 104896
Current children cumulated CPU time (s) 887.59
Current children cumulated vsize (Kb) 107020

[startup+900.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 25903 0 0 0 89577 178 0 0 25 0 1 0 1797091662 108019712 25809 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 26372 25809 145 145 0 26227 0
[pid=8003] vsize: 105488
Current children cumulated CPU time (s) 897.57
Current children cumulated vsize (Kb) 107612

[startup+910.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26037 0 0 0 90576 178 0 0 25 0 1 0 1797091662 108617728 25943 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 26518 25943 145 145 0 26373 0
[pid=8003] vsize: 106072
Current children cumulated CPU time (s) 907.56
Current children cumulated vsize (Kb) 108196

[startup+920.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26185 0 0 0 91573 179 0 0 25 0 1 0 1797091662 109236224 26091 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 26669 26091 145 145 0 26524 0
[pid=8003] vsize: 106676
Current children cumulated CPU time (s) 917.54
Current children cumulated vsize (Kb) 108800

[startup+930.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26318 0 0 0 92571 180 0 0 25 0 1 0 1797091662 109776896 26224 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 26801 26224 145 145 0 26656 0
[pid=8003] vsize: 107204
Current children cumulated CPU time (s) 927.53
Current children cumulated vsize (Kb) 109328

[startup+940.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26432 0 0 0 93569 181 0 0 25 0 1 0 1797091662 110227456 26338 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 26911 26338 145 145 0 26766 0
[pid=8003] vsize: 107644
Current children cumulated CPU time (s) 937.52
Current children cumulated vsize (Kb) 109768

[startup+950.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26554 0 0 0 94567 182 0 0 25 0 1 0 1797091662 110731264 26460 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 27034 26460 145 145 0 26889 0
[pid=8003] vsize: 108136
Current children cumulated CPU time (s) 947.51
Current children cumulated vsize (Kb) 110260

[startup+960.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26670 0 0 0 95565 183 0 0 25 0 1 0 1797091662 111230976 26576 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 27156 26576 145 145 0 27011 0
[pid=8003] vsize: 108624
Current children cumulated CPU time (s) 957.5
Current children cumulated vsize (Kb) 110748

[startup+970.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26806 0 0 0 96563 183 0 0 25 0 1 0 1797091662 111763456 26712 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 27286 26712 145 145 0 27141 0
[pid=8003] vsize: 109144
Current children cumulated CPU time (s) 967.48
Current children cumulated vsize (Kb) 111268

[startup+980.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 26970 0 0 0 97560 185 0 0 25 0 1 0 1797091662 112476160 26876 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 27460 26876 145 145 0 27315 0
[pid=8003] vsize: 109840
Current children cumulated CPU time (s) 977.47
Current children cumulated vsize (Kb) 111964

[startup+990.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 27101 0 0 0 98558 186 0 0 25 0 1 0 1797091662 113049600 27007 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 27600 27007 145 145 0 27455 0
[pid=8003] vsize: 110400
Current children cumulated CPU time (s) 987.46
Current children cumulated vsize (Kb) 112524

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 27217 0 0 0 99555 187 0 0 25 0 1 0 1797091662 114049024 27123 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 27844 27123 145 145 0 27699 0
[pid=8003] vsize: 111376
Current children cumulated CPU time (s) 997.44
Current children cumulated vsize (Kb) 113500

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 27369 0 0 0 100552 188 0 0 25 0 1 0 1797091662 114659328 27275 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 27993 27275 145 145 0 27848 0
[pid=8003] vsize: 111972
Current children cumulated CPU time (s) 1007.42
Current children cumulated vsize (Kb) 114096

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 27452 0 0 0 101550 188 0 0 25 0 1 0 1797091662 115011584 27358 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 28079 27358 145 145 0 27934 0
[pid=8003] vsize: 112316
Current children cumulated CPU time (s) 1017.4
Current children cumulated vsize (Kb) 114440

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 27578 0 0 0 102548 190 0 0 25 0 1 0 1797091662 115511296 27484 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 28201 27484 145 145 0 28056 0
[pid=8003] vsize: 112804
Current children cumulated CPU time (s) 1027.4
Current children cumulated vsize (Kb) 114928

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 27753 0 0 0 103546 190 0 0 25 0 1 0 1797091662 116264960 27659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 28385 27659 145 145 0 28240 0
[pid=8003] vsize: 113540
Current children cumulated CPU time (s) 1037.38
Current children cumulated vsize (Kb) 115664

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 27901 0 0 0 104543 192 0 0 25 0 1 0 1797091662 116867072 27807 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 28532 27807 145 145 0 28387 0
[pid=8003] vsize: 114128
Current children cumulated CPU time (s) 1047.37
Current children cumulated vsize (Kb) 116252

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 28064 0 0 0 105540 193 0 0 25 0 1 0 1797091662 117518336 27970 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 28691 27970 145 145 0 28546 0
[pid=8003] vsize: 114764
Current children cumulated CPU time (s) 1057.35
Current children cumulated vsize (Kb) 116888

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 28241 0 0 0 106536 194 0 0 25 0 1 0 1797091662 118239232 28147 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 28867 28147 145 145 0 28722 0
[pid=8003] vsize: 115468
Current children cumulated CPU time (s) 1067.32
Current children cumulated vsize (Kb) 117592

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 28397 0 0 0 107534 195 0 0 25 0 1 0 1797091662 118865920 28303 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 29020 28303 145 145 0 28875 0
[pid=8003] vsize: 116080
Current children cumulated CPU time (s) 1077.31
Current children cumulated vsize (Kb) 118204

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 28546 0 0 0 108531 196 0 0 25 0 1 0 1797091662 119468032 28452 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 29167 28452 145 145 0 29022 0
[pid=8003] vsize: 116668
Current children cumulated CPU time (s) 1087.29
Current children cumulated vsize (Kb) 118792

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 28710 0 0 0 109528 197 0 0 25 0 1 0 1797091662 120135680 28616 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 29330 28616 145 145 0 29185 0
[pid=8003] vsize: 117320
Current children cumulated CPU time (s) 1097.27
Current children cumulated vsize (Kb) 119444

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 28904 0 0 0 110524 199 0 0 25 0 1 0 1797091662 120926208 28810 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 29523 28810 145 145 0 29378 0
[pid=8003] vsize: 118092
Current children cumulated CPU time (s) 1107.25
Current children cumulated vsize (Kb) 120216

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29056 0 0 0 111522 200 0 0 25 0 1 0 1797091662 121540608 28962 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 29673 28962 145 145 0 29528 0
[pid=8003] vsize: 118692
Current children cumulated CPU time (s) 1117.24
Current children cumulated vsize (Kb) 120816

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29190 0 0 0 112519 201 0 0 25 0 1 0 1797091662 122105856 29096 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 29811 29096 145 145 0 29666 0
[pid=8003] vsize: 119244
Current children cumulated CPU time (s) 1127.22
Current children cumulated vsize (Kb) 121368

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8003
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29305 0 0 0 113517 202 0 0 25 0 1 0 1797091662 122568704 29211 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 29924 29211 145 145 0 29779 0
[pid=8003] vsize: 119696
Current children cumulated CPU time (s) 1137.21
Current children cumulated vsize (Kb) 121820

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 3/60 8042
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29410 0 0 0 114506 211 0 0 25 0 1 0 1797091662 122990592 29316 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8003/statm): 30027 29316 145 145 0 29882 0
[pid=8003] vsize: 120108
Current children cumulated CPU time (s) 1147.19
Current children cumulated vsize (Kb) 122232

[startup+1160.09 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 8054
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29510 0 0 0 115500 216 0 0 25 0 1 0 1797091662 123396096 29416 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 30126 29416 145 145 0 29981 0
[pid=8003] vsize: 120504
Current children cumulated CPU time (s) 1157.18
Current children cumulated vsize (Kb) 122628

[startup+1170.09 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 8054
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29619 0 0 0 116498 217 0 0 25 0 1 0 1797091662 123842560 29525 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 30235 29525 145 145 0 30090 0
[pid=8003] vsize: 120940
Current children cumulated CPU time (s) 1167.17
Current children cumulated vsize (Kb) 123064

[startup+1180.09 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 8054
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29728 0 0 0 117496 218 0 0 25 0 1 0 1797091662 124280832 29634 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 30342 29634 145 145 0 30197 0
[pid=8003] vsize: 121368
Current children cumulated CPU time (s) 1177.16
Current children cumulated vsize (Kb) 123492

[startup+1190.09 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 8054
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29824 0 0 0 118495 219 0 0 25 0 1 0 1797091662 124694528 29730 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 30443 29730 145 145 0 30298 0
[pid=8003] vsize: 121772
Current children cumulated CPU time (s) 1187.16
Current children cumulated vsize (Kb) 123896

[startup+1200.09 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 8054
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 29959 0 0 0 119493 220 0 0 25 0 1 0 1797091662 125239296 29865 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 30576 29865 145 145 0 30431 0
[pid=8003] vsize: 122304
Current children cumulated CPU time (s) 1197.15
Current children cumulated vsize (Kb) 124428

[startup+1210.09 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 8054
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 30070 0 0 0 120492 220 0 0 25 0 1 0 1797091662 125685760 29976 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 30685 29976 145 145 0 30540 0
[pid=8003] vsize: 122740
Current children cumulated CPU time (s) 1207.14
Current children cumulated vsize (Kb) 124864



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 8054
Raw data (/proc/7999/stat): 7999 (minisat+_script) S 7998 7999 6872 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1797091657 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7999/statm): 531 226 485 147 0 384 0
[pid=7999] vsize: 2124
Raw data (/proc/8003/stat): 8003 (minisat+_64-bit) R 7999 7999 6872 0 -1 0 30070 0 0 0 120492 220 0 0 25 0 1 0 1797091662 125685760 29976 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8003/statm): 30685 29976 145 145 0 30540 0
[pid=8003] vsize: 122740
Current children cumulated CPU time (s) 1207.14
Current children cumulated vsize (Kb) 124864

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1207.19
CPU user time (s): 1204.92
CPU system time (s): 2.26566
CPU usage (%): 99.7551
Max. virtual memory (cumulated for all children) (Kb): 124864

Verifier Data

ERROR: no interpretation found !