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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-fit1d.opb
MD5SUM6bb160e5eb0ef9c02ca7232f62836f2b
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 8436
Biggest coefficient in the objective function 368640
Number of bits for the biggest coefficient in the objective function 19
Sum of the numbers in the objective function 57614442
Number of bits of the sum of numbers in the objective function 26
Biggest number in a constraint 483840
Number of bits of the biggest number in a constraint 19
Biggest sum of numbers in a constraint 72412534
Number of bits of the biggest sum of numbers27
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1194.95
Number of variables8436
Total number of constraints1050
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1050
Minimum length of a constraint8
Maximum length of a constraint8436

Trace number 6014

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-20 02:37:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3156 boxname=wulflinc20 idbench=812 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6bb160e5eb0ef9c02ca7232f62836f2b  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-fit1d.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-fit1d.opb
IDLAUNCH: 3156
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        922908 kB
Buffers:          1868 kB
Cached:          80476 kB
SwapCached:        820 kB
Active:          21296 kB
Inactive:        63628 kB
HighTotal:      131008 kB
HighFree:        46452 kB
LowTotal:       903652 kB
LowFree:        876456 kB
SwapTotal:     2097892 kB
SwapFree:      2096508 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5640 kB
Slab:            21084 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:58:01 (client local time) WITH STATUS 0 IN 1205.35 SECONDS
stats: 3156 7 1205.35 0

Solver Data

c Parsing PB file...
c Converting 1051 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): (none)
c ---[1050]---> BDD-cost:    7
c ---[1049]---> BDD-cost:    7
c ---[1048]---> BDD-cost:    7
c ---[1047]---> BDD-cost:    7
c ---[1046]---> BDD-cost:    7
c ---[1045]---> BDD-cost:    7
c ---[1044]---> BDD-cost:    7
c ---[1043]---> BDD-cost:    7
c ---[1042]---> BDD-cost:    7
c ---[1041]---> BDD-cost:    7
c ---[1040]---> BDD-cost:    7
c ---[1039]---> BDD-cost:    7
c ---[1038]---> BDD-cost:    7
c ---[1037]---> BDD-cost:    7
c ---[1036]---> BDD-cost:    7
c ---[1035]---> BDD-cost:    7
c ---[1034]---> BDD-cost:    7
c ---[1033]---> BDD-cost:    7
c ---[1032]---> BDD-cost:    7
c ---[1031]---> BDD-cost:    7
c ---[1030]---> BDD-cost:    7
c ---[1029]---> BDD-cost:    7
c ---[1028]---> BDD-cost:    7
c ---[1027]---> BDD-cost:    7
c ---[1026]---> BDD-cost:    7
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    7
c ---[1023]---> BDD-cost:    7
c ---[1022]---> BDD-cost:    7
c ---[1021]---> BDD-cost:    7
c ---[1020]---> BDD-cost:    7
c ---[1019]---> BDD-cost:    7
c ---[1018]---> BDD-cost:    7
c ---[1017]---> BDD-cost:    7
c ---[1016]---> BDD-cost:    7
c ---[1015]---> BDD-cost:    7
c ---[1014]---> BDD-cost:    7
c ---[1013]---> BDD-cost:    7
c ---[1012]---> BDD-cost:    7
c ---[1011]---> BDD-cost:    7
c ---[1010]---> BDD-cost:    7
c ---[1009]---> BDD-cost:    7
c ---[1008]---> BDD-cost:    7
c ---[1007]---> BDD-cost:    7
c ---[1006]---> BDD-cost:    7
c ---[1005]---> BDD-cost:    7
c ---[1004]---> BDD-cost:    7
c ---[1003]---> BDD-cost:    7
c ---[1002]---> BDD-cost:    7
c ---[1001]---> BDD-cost:    7
c ---[1000]---> BDD-cost:    7
c ---[ 999]---> BDD-cost:    7
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:    7
c ---[ 996]---> BDD-cost:    7
c ---[ 995]---> BDD-cost:    7
c ---[ 994]---> BDD-cost:    7
c ---[ 993]---> BDD-cost:    7
c ---[ 992]---> BDD-cost:    7
c ---[ 991]---> BDD-cost:    7
c ---[ 990]---> BDD-cost:    7
c ---[ 989]---> BDD-cost:    7
c ---[ 988]---> BDD-cost:    7
c ---[ 987]---> BDD-cost:    7
c ---[ 986]---> BDD-cost:    7
c ---[ 985]---> BDD-cost:    7
c ---[ 984]---> BDD-cost:    7
c ---[ 983]---> BDD-cost:    7
c ---[ 982]---> BDD-cost:    7
c ---[ 981]---> BDD-cost:    7
c ---[ 980]---> BDD-cost:    7
c ---[ 979]---> BDD-cost:    7
c ---[ 978]---> BDD-cost:    7
c ---[ 977]---> BDD-cost:    7
c ---[ 976]---> BDD-cost:    7
c ---[ 975]---> BDD-cost:    7
c ---[ 974]---> BDD-cost:    7
c ---[ 973]---> BDD-cost:    7
c ---[ 972]---> BDD-cost:    7
c ---[ 971]---> BDD-cost:    7
c ---[ 970]---> BDD-cost:    7
c ---[ 969]---> BDD-cost:    7
c ---[ 968]---> BDD-cost:    7
c ---[ 967]---> BDD-cost:    7
c ---[ 966]---> BDD-cost:    7
c ---[ 965]---> BDD-cost:    7
c ---[ 964]---> BDD-cost:    7
c ---[ 963]---> BDD-cost:    7
c ---[ 962]---> BDD-cost:    7
c ---[ 961]---> BDD-cost:    7
c ---[ 960]---> BDD-cost:    7
c ---[ 959]---> BDD-cost:    7
c ---[ 958]---> BDD-cost:    7
c ---[ 957]---> BDD-cost:    7
c ---[ 956]---> BDD-cost:    7
c ---[ 955]---> BDD-cost:    7
c ---[ 954]---> BDD-cost:    7
c ---[ 953]---> BDD-cost:    7
c ---[ 952]---> BDD-cost:    7
c ---[ 951]---> BDD-cost:    7
c ---[ 950]---> BDD-cost:    7
c ---[ 949]---> BDD-cost:    7
c ---[ 948]---> BDD-cost:    7
c ---[ 947]---> BDD-cost:    7
c ---[ 946]---> BDD-cost:    7
c ---[ 945]---> BDD-cost:    7
c ---[ 944]---> BDD-cost:    7
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    7
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    7
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    7
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    7
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    7
c ---[ 933]---> BDD-cost:    7
c ---[ 932]---> BDD-cost:    7
c ---[ 931]---> BDD-cost:    7
c ---[ 930]---> BDD-cost:    7
c ---[ 929]---> BDD-cost:    7
c ---[ 928]---> BDD-cost:    7
c ---[ 927]---> BDD-cost:    7
c ---[ 926]---> BDD-cost:    7
c ---[ 925]---> BDD-cost:    7
c ---[ 924]---> BDD-cost:    7
c ---[ 923]---> BDD-cost:    7
c ---[ 922]---> BDD-cost:    7
c ---[ 921]---> BDD-cost:    7
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:    7
c ---[ 918]---> BDD-cost:    7
c ---[ 917]---> BDD-cost:    7
c ---[ 916]---> BDD-cost:    7
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    7
c ---[ 913]---> BDD-cost:    7
c ---[ 912]---> BDD-cost:    7
c ---[ 911]---> BDD-cost:    7
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    7
c ---[ 907]---> BDD-cost:    7
c ---[ 906]---> BDD-cost:    7
c ---[ 905]---> BDD-cost:    7
c ---[ 904]---> BDD-cost:    7
c ---[ 903]---> BDD-cost:    7
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    7
c ---[ 900]---> BDD-cost:    7
c ---[ 899]---> BDD-cost:    7
c ---[ 898]---> BDD-cost:    7
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:    7
c ---[ 895]---> BDD-cost:    7
c ---[ 894]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:    7
c ---[ 892]---> BDD-cost:    7
c ---[ 891]---> BDD-cost:    7
c ---[ 890]---> BDD-cost:    7
c ---[ 889]---> BDD-cost:    7
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    7
c ---[ 885]---> BDD-cost:    7
c ---[ 884]---> BDD-cost:    7
c ---[ 883]---> BDD-cost:    7
c ---[ 882]---> BDD-cost:    7
c ---[ 881]---> BDD-cost:    7
c ---[ 880]---> BDD-cost:    7
c ---[ 879]---> BDD-cost:    7
c ---[ 878]---> BDD-cost:    7
c ---[ 877]---> BDD-cost:    7
c ---[ 876]---> BDD-cost:    7
c ---[ 875]---> BDD-cost:    7
c ---[ 874]---> BDD-cost:    7
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    7
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    7
c ---[ 869]---> BDD-cost:    7
c ---[ 868]---> BDD-cost:    7
c ---[ 867]---> BDD-cost:    7
c ---[ 866]---> BDD-cost:    7
c ---[ 865]---> BDD-cost:    7
c ---[ 864]---> BDD-cost:    7
c ---[ 863]---> BDD-cost:    7
c ---[ 862]---> BDD-cost:    7
c ---[ 861]---> BDD-cost:    7
c ---[ 860]---> BDD-cost:    7
c ---[ 859]---> BDD-cost:    7
c ---[ 858]---> BDD-cost:    7
c ---[ 857]---> BDD-cost:    7
c ---[ 856]---> BDD-cost:    7
c ---[ 855]---> BDD-cost:    7
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    7
c ---[ 852]---> BDD-cost:    7
c ---[ 851]---> BDD-cost:    7
c ---[ 850]---> BDD-cost:    7
c ---[ 849]---> BDD-cost:    7
c ---[ 848]---> BDD-cost:    7
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    7
c ---[ 845]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:    7
c ---[ 842]---> BDD-cost:    7
c ---[ 841]---> BDD-cost:    7
c ---[ 840]---> BDD-cost:    7
c ---[ 839]---> BDD-cost:    7
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    7
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    7
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:    7
c ---[ 832]---> BDD-cost:    7
c ---[ 831]---> BDD-cost:    7
c ---[ 830]---> BDD-cost:    7
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    7
c ---[ 827]---> BDD-cost:    7
c ---[ 826]---> BDD-cost:    7
c ---[ 825]---> BDD-cost:    7
c ---[ 824]---> BDD-cost:    7
c ---[ 823]---> BDD-cost:    7
c ---[ 822]---> BDD-cost:    7
c ---[ 821]---> BDD-cost:    7
c ---[ 820]---> BDD-cost:    7
c ---[ 819]---> BDD-cost:    7
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    7
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    7
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    7
c ---[ 810]---> BDD-cost:    7
c ---[ 809]---> BDD-cost:    7
c ---[ 808]---> BDD-cost:    7
c ---[ 807]---> BDD-cost:    7
c ---[ 806]---> BDD-cost:    7
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    7
c ---[ 803]---> BDD-cost:    7
c ---[ 802]---> BDD-cost:    7
c ---[ 801]---> BDD-cost:    7
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:    7
c ---[ 796]---> BDD-cost:    7
c ---[ 795]---> BDD-cost:    7
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    7
c ---[ 792]---> BDD-cost:    7
c ---[ 791]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:    7
c ---[ 789]---> BDD-cost:    7
c ---[ 788]---> BDD-cost:    7
c ---[ 787]---> BDD-cost:    7
c ---[ 786]---> BDD-cost:    7
c ---[ 785]---> BDD-cost:    7
c ---[ 784]---> BDD-cost:    7
c ---[ 783]---> BDD-cost:    7
c ---[ 782]---> BDD-cost:    7
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:    7
c ---[ 779]---> BDD-cost:    7
c ---[ 778]---> BDD-cost:    7
c ---[ 777]---> BDD-cost:    7
c ---[ 776]---> BDD-cost:    7
c ---[ 775]---> BDD-cost:    7
c ---[ 774]---> BDD-cost:    7
c ---[ 773]---> BDD-cost:    7
c ---[ 772]---> BDD-cost:    7
c ---[ 771]---> BDD-cost:    7
c ---[ 770]---> BDD-cost:    7
c ---[ 769]---> BDD-cost:    7
c ---[ 768]---> BDD-cost:    7
c ---[ 767]---> BDD-cost:    7
c ---[ 766]---> BDD-cost:    7
c ---[ 765]---> BDD-cost:    7
c ---[ 764]---> BDD-cost:    7
c ---[ 763]---> BDD-cost:    7
c ---[ 762]---> BDD-cost:    7
c ---[ 761]---> BDD-cost:    7
c ---[ 760]---> BDD-cost:    7
c ---[ 759]---> BDD-cost:    7
c ---[ 758]---> BDD-cost:    7
c ---[ 757]---> BDD-cost:    7
c ---[ 756]---> BDD-cost:    7
c ---[ 755]---> BDD-cost:    7
c ---[ 754]---> BDD-cost:    7
c ---[ 753]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:    7
c ---[ 751]---> BDD-cost:    7
c ---[ 750]---> BDD-cost:    7
c ---[ 749]---> BDD-cost:    7
c ---[ 748]---> BDD-cost:    7
c ---[ 747]---> BDD-cost:    7
c ---[ 746]---> BDD-cost:    7
c ---[ 745]---> BDD-cost:    7
c ---[ 744]---> BDD-cost:    7
c ---[ 743]---> BDD-cost:    7
c ---[ 742]---> BDD-cost:    7
c ---[ 741]---> BDD-cost:    7
c ---[ 740]---> BDD-cost:    7
c ---[ 739]---> BDD-cost:    7
c ---[ 738]---> BDD-cost:    7
c ---[ 737]---> BDD-cost:    7
c ---[ 736]---> BDD-cost:    7
c ---[ 735]---> BDD-cost:    7
c ---[ 734]---> BDD-cost:    7
c ---[ 733]---> BDD-cost:    7
c ---[ 732]---> BDD-cost:    7
c ---[ 731]---> BDD-cost:    7
c ---[ 730]---> BDD-cost:    7
c ---[ 729]---> BDD-cost:    7
c ---[ 728]---> BDD-cost:    7
c ---[ 727]---> BDD-cost:    7
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    7
c ---[ 724]---> BDD-cost:    7
c ---[ 723]---> BDD-cost:    7
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:    7
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    7
c ---[ 718]---> BDD-cost:    7
c ---[ 717]---> BDD-cost:    7
c ---[ 716]---> BDD-cost:    7
c ---[ 715]---> BDD-cost:    7
c ---[ 714]---> BDD-cost:    7
c ---[ 713]---> BDD-cost:    7
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    7
c ---[ 710]---> BDD-cost:    7
c ---[ 709]---> BDD-cost:    7
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:    7
c ---[ 706]---> BDD-cost:    7
c ---[ 705]---> BDD-cost:    7
c ---[ 704]---> BDD-cost:    7
c ---[ 703]---> BDD-cost:    7
c ---[ 702]---> BDD-cost:    7
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    7
c ---[ 699]---> BDD-cost:    7
c ---[ 698]---> BDD-cost:    7
c ---[ 697]---> BDD-cost:    7
c ---[ 696]---> BDD-cost:    7
c ---[ 695]---> BDD-cost:    7
c ---[ 694]---> BDD-cost:    7
c ---[ 693]---> BDD-cost:    7
c ---[ 692]---> BDD-cost:    7
c ---[ 691]---> BDD-cost:    7
c ---[ 690]---> BDD-cost:    7
c ---[ 689]---> BDD-cost:    7
c ---[ 688]---> BDD-cost:    7
c ---[ 687]---> BDD-cost:    7
c ---[ 686]---> BDD-cost:    7
c ---[ 685]---> BDD-cost:    7
c ---[ 684]---> BDD-cost:    7
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    7
c ---[ 681]---> BDD-cost:    7
c ---[ 680]---> BDD-cost:    7
c ---[ 679]---> BDD-cost:    7
c ---[ 678]---> BDD-cost:    7
c ---[ 677]---> BDD-cost:    7
c ---[ 676]---> BDD-cost:    7
c ---[ 675]---> BDD-cost:    7
c ---[ 674]---> BDD-cost:    7
c ---[ 673]---> BDD-cost:    7
c ---[ 672]---> BDD-cost:    7
c ---[ 671]---> BDD-cost:    7
c ---[ 670]---> BDD-cost:    7
c ---[ 669]---> BDD-cost:    7
c ---[ 668]---> BDD-cost:    7
c ---[ 667]---> BDD-cost:    7
c ---[ 666]---> BDD-cost:    7
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    7
c ---[ 662]---> BDD-cost:    7
c ---[ 661]---> BDD-cost:    7
c ---[ 660]---> BDD-cost:    7
c ---[ 659]---> BDD-cost:    7
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:    7
c ---[ 656]---> BDD-cost:    7
c ---[ 655]---> BDD-cost:    7
c ---[ 654]---> BDD-cost:    7
c ---[ 653]---> BDD-cost:    7
c ---[ 652]---> BDD-cost:    7
c ---[ 651]---> BDD-cost:    7
c ---[ 650]---> BDD-cost:    7
c ---[ 649]---> BDD-cost:    7
c ---[ 648]---> BDD-cost:    7
c ---[ 647]---> BDD-cost:    7
c ---[ 646]---> BDD-cost:    7
c ---[ 645]---> BDD-cost:    7
c ---[ 644]---> BDD-cost:    7
c ---[ 643]---> BDD-cost:    7
c ---[ 642]---> BDD-cost:    7
c ---[ 641]---> BDD-cost:    7
c ---[ 640]---> BDD-cost:    7
c ---[ 639]---> BDD-cost:    7
c ---[ 638]---> BDD-cost:    7
c ---[ 637]---> BDD-cost:    7
c ---[ 636]---> BDD-cost:    7
c ---[ 635]---> BDD-cost:    7
c ---[ 634]---> BDD-cost:    7
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:    7
c ---[ 631]---> BDD-cost:    7
c ---[ 630]---> BDD-cost:    7
c ---[ 629]---> BDD-cost:    7
c ---[ 628]---> BDD-cost:    7
c ---[ 627]---> BDD-cost:    7
c ---[ 626]---> BDD-cost:    7
c ---[ 625]---> BDD-cost:    7
c ---[ 624]---> BDD-cost:    7
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    7
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    7
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    7
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    7
c ---[ 615]---> BDD-cost:    7
c ---[ 614]---> BDD-cost:    7
c ---[ 613]---> BDD-cost:    7
c ---[ 612]---> BDD-cost:    7
c ---[ 611]---> BDD-cost:    7
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    7
c ---[ 606]---> BDD-cost:    7
c ---[ 605]---> BDD-cost:    7
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    7
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    7
c ---[ 600]---> BDD-cost:    7
c ---[ 599]---> BDD-cost:    7
c ---[ 598]---> BDD-cost:    7
c ---[ 597]---> BDD-cost:    7
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:    7
c ---[ 594]---> BDD-cost:    7
c ---[ 593]---> BDD-cost:    7
c ---[ 592]---> BDD-cost:    7
c ---[ 591]---> BDD-cost:    7
c ---[ 590]---> BDD-cost:    7
c ---[ 589]---> BDD-cost:    7
c ---[ 588]---> BDD-cost:    7
c ---[ 587]---> BDD-cost:    7
c ---[ 586]---> BDD-cost:    7
c ---[ 585]---> BDD-cost:    7
c ---[ 584]---> BDD-cost:    7
c ---[ 583]---> BDD-cost:    7
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    7
c ---[ 580]---> BDD-cost:    7
c ---[ 579]---> BDD-cost:    7
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:    7
c ---[ 576]---> BDD-cost:    7
c ---[ 575]---> BDD-cost:    7
c ---[ 574]---> BDD-cost:    7
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> BDD-cost:    7
c ---[ 571]---> BDD-cost:    7
c ---[ 570]---> BDD-cost:    7
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    7
c ---[ 567]---> BDD-cost:    7
c ---[ 566]---> BDD-cost:    7
c ---[ 565]---> BDD-cost:    7
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    7
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:    7
c ---[ 559]---> BDD-cost:    7
c ---[ 558]---> BDD-cost:    7
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    7
c ---[ 554]---> BDD-cost:    7
c ---[ 553]---> BDD-cost:    7
c ---[ 552]---> BDD-cost:    7
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    7
c ---[ 549]---> BDD-cost:    7
c ---[ 548]---> BDD-cost:    7
c ---[ 547]---> BDD-cost:    7
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    7
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:    7
c ---[ 542]---> BDD-cost:    7
c ---[ 541]---> BDD-cost:    7
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    7
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    7
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    7
c ---[ 531]---> BDD-cost:    7
c ---[ 530]---> BDD-cost:    7
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:    7
c ---[ 525]---> BDD-cost:    7
c ---[ 524]---> BDD-cost:    7
c ---[ 523]---> BDD-cost:    7
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    7
c ---[ 520]---> BDD-cost:    7
c ---[ 519]---> BDD-cost:    7
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    7
c ---[ 514]---> BDD-cost:    7
c ---[ 513]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:    7
c ---[ 511]---> BDD-cost:    7
c ---[ 510]---> BDD-cost:    7
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    7
c ---[ 506]---> BDD-cost:    7
c ---[ 505]---> BDD-cost:    7
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    7
c ---[ 501]---> BDD-cost:    7
c ---[ 500]---> BDD-cost:    7
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    7
c ---[ 497]---> BDD-cost:    7
c ---[ 496]---> BDD-cost:    7
c ---[ 495]---> BDD-cost:    7
c ---[ 494]---> BDD-cost:    7
c ---[ 493]---> BDD-cost:    7
c ---[ 492]---> BDD-cost:    7
c ---[ 491]---> BDD-cost:    7
c ---[ 490]---> BDD-cost:    7
c ---[ 489]---> BDD-cost:    7
c ---[ 488]---> BDD-cost:    7
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    7
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:    7
c ---[ 475]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 470]---> BDD-cost:    7
c ---[ 469]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    7
c ---[ 463]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    7
c ---[ 455]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    7
c ---[ 442]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 438]---> BDD-cost:    7
c ---[ 437]---> BDD-cost:    7
c ---[ 436]---> BDD-cost:    7
c ---[ 435]---> BDD-cost:    7
c ---[ 434]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> BDD-cost:    7
c ---[ 430]---> BDD-cost:    7
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 426]---> BDD-cost:    7
c ---[ 425]---> BDD-cost:    7
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    7
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 414]---> BDD-cost:    7
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    7
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 407]---> BDD-cost:    7
c ---[ 406]---> BDD-cost:    7
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    7
c ---[ 403]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    7
c ---[ 398]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 395]---> BDD-cost:    7
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:    7
c ---[ 388]---> BDD-cost:    7
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:    7
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 377]---> BDD-cost:    7
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 371]---> BDD-cost:    7
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 363]---> BDD-cost:    7
c ---[ 362]---> BDD-cost:    7
c ---[ 361]---> BDD-cost:    7
c ---[ 360]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:    7
c ---[ 356]---> BDD-cost:    7
c ---[ 355]---> BDD-cost:    7
c ---[ 354]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 352]---> BDD-cost:    7
c ---[ 351]---> BDD-cost:    7
c ---[ 350]---> BDD-cost:    7
c ---[ 349]---> BDD-cost:    7
c ---[ 348]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:    7
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:    7
c ---[ 342]---> BDD-cost:    7
c ---[ 341]---> BDD-cost:    7
c ---[ 340]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    7
c ---[ 336]---> BDD-cost:    7
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 332]---> BDD-cost:    7
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    7
c ---[ 329]---> BDD-cost:    7
c ---[ 328]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 326]---> BDD-cost:    7
c ---[ 325]---> BDD-cost:    7
c ---[ 324]---> BDD-cost:    7
c ---[ 323]---> BDD-cost:    7
c ---[ 322]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 320]---> BDD-cost:    7
c ---[ 319]---> BDD-cost:    7
c ---[ 318]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:    7
c ---[ 316]---> BDD-cost:    7
c ---[ 315]---> BDD-cost:    7
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:    7
c ---[ 312]---> BDD-cost:    7
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    7
c ---[ 309]---> BDD-cost:    7
c ---[ 308]---> BDD-cost:    7
c ---[ 307]---> BDD-cost:    7
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:    7
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    7
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    7
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    7
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    7
c ---[ 294]---> BDD-cost:    7
c ---[ 293]---> BDD-cost:    7
c ---[ 292]---> BDD-cost:    7
c ---[ 291]---> BDD-cost:    7
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    7
c ---[ 288]---> BDD-cost:    7
c ---[ 287]---> BDD-cost:    7
c ---[ 286]---> BDD-cost:    7
c ---[ 285]---> BDD-cost:    7
c ---[ 284]---> BDD-cost:    7
c ---[ 283]---> BDD-cost:    7
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    7
c ---[ 280]---> BDD-cost:    7
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    7
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    7
c ---[ 275]---> BDD-cost:    7
c ---[ 274]---> BDD-cost:    7
c ---[ 273]---> BDD-cost:    7
c ---[ 272]---> BDD-cost:    7
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    7
c ---[ 269]---> BDD-cost:    7
c ---[ 268]---> BDD-cost:    7
c ---[ 267]---> BDD-cost:    7
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    7
c ---[ 264]---> BDD-cost:    7
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    7
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:    7
c ---[ 259]---> BDD-cost:    7
c ---[ 258]---> BDD-cost:    7
c ---[ 257]---> BDD-cost:    7
c ---[ 256]---> BDD-cost:    7
c ---[ 255]---> BDD-cost:    7
c ---[ 254]---> BDD-cost:    7
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:    8
c ---[ 251]---> BDD-cost:    8
c ---[ 250]---> BDD-cost:    8
c ---[ 249]---> BDD-cost:    8
c ---[ 248]---> BDD-cost:    8
c ---[ 247]---> BDD-cost:    8
c ---[ 246]---> BDD-cost:    8
c ---[ 245]---> BDD-cost:    8
c ---[ 244]---> BDD-cost:    8
c ---[ 243]---> BDD-cost:    8
c ---[ 242]---> BDD-cost:    8
c ---[ 241]---> BDD-cost:    8
c ---[ 240]---> BDD-cost:    8
c ---[ 239]---> BDD-cost:    8
c ---[ 238]---> BDD-cost:    8
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    8
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    8
c ---[ 233]---> BDD-cost:    8
c ---[ 232]---> BDD-cost:    8
c ---[ 231]---> BDD-cost:    8
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:    8
c ---[ 228]---> BDD-cost:    8
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:    8
c ---[ 223]---> BDD-cost:    8
c ---[ 222]---> BDD-cost:    8
c ---[ 221]---> BDD-cost:    8
c ---[ 220]---> BDD-cost:    8
c ---[ 219]---> BDD-cost:    8
c ---[ 218]---> BDD-cost:    8
c ---[ 217]---> BDD-cost:    8
c ---[ 216]---> BDD-cost:    8
c ---[ 215]---> BDD-cost:    8
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    8
c ---[ 212]---> BDD-cost:    8
c ---[ 211]---> BDD-cost:    8
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    8
c ---[ 207]---> BDD-cost:    8
c ---[ 206]---> BDD-cost:    8
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    8
c ---[ 203]---> BDD-cost:    8
c ---[ 202]---> BDD-cost:    8
c ---[ 201]---> BDD-cost:    8
c ---[ 200]---> BDD-cost:    8
c ---[ 199]---> BDD-cost:    8
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:    8
c ---[ 196]---> BDD-cost:    8
c ---[ 195]---> BDD-cost:    8
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    8
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    8
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:    8
c ---[ 184]---> BDD-cost:    8
c ---[ 183]---> BDD-cost:    8
c ---[ 182]---> BDD-cost:    8
c ---[ 181]---> BDD-cost:    8
c ---[ 180]---> BDD-cost:    8
c ---[ 179]---> BDD-cost:    8
c ---[ 178]---> BDD-cost:    8
c ---[ 177]---> BDD-cost:    8
c ---[ 176]---> BDD-cost:    8
c ---[ 175]---> BDD-cost:    8
c ---[ 174]---> BDD-cost:    8
c ---[ 173]---> BDD-cost:    8
c ---[ 172]---> BDD-cost:    8
c ---[ 171]---> BDD-cost:    8
c ---[ 170]---> BDD-cost:    8
c ---[ 169]---> BDD-cost:    8
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    8
c ---[ 164]---> BDD-cost:    8
c ---[ 163]---> BDD-cost:    8
c ---[ 162]---> BDD-cost:    8
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:    8
c ---[ 159]---> BDD-cost:    8
c ---[ 158]---> BDD-cost:    8
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    8
c ---[ 155]---> BDD-cost:    8
c ---[ 154]---> BDD-cost:    8
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    8
c ---[ 151]---> BDD-cost:    8
c ---[ 150]---> BDD-cost:    8
c ---[ 149]---> BDD-cost:    8
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    8
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 139]---> BDD-cost:    8
c ---[ 138]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 136]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:    8
c ---[ 134]---> BDD-cost:    8
c ---[ 133]---> BDD-cost:    8
c ---[ 132]---> BDD-cost:    8
c ---[ 131]---> BDD-cost:    8
c ---[ 130]---> BDD-cost:    8
c ---[ 129]---> BDD-cost:    8
c ---[ 128]---> BDD-cost:    8
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:    8
c ---[ 125]---> BDD-cost:    8
c ---[ 124]---> BDD-cost:    8
c ---[ 123]---> BDD-cost:    8
c ---[ 122]---> BDD-cost:    8
c ---[ 121]---> BDD-cost:    8
c ---[ 120]---> BDD-cost:    8
c ---[ 119]---> BDD-cost:    8
c ---[ 118]---> BDD-cost:    8
c ---[ 117]---> BDD-cost:    8
c ---[ 116]---> BDD-cost:    8
c ---[ 115]---> BDD-cost:    8
c ---[ 114]---> BDD-cost:    8
c ---[ 113]---> BDD-cost:    8
c ---[ 112]---> BDD-cost:    8
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 108]---> BDD-cost:    8
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:    8
c ---[ 105]---> BDD-cost:    8
c ---[ 104]---> BDD-cost:    8
c ---[ 103]---> BDD-cost:    8
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    8
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    8
c ---[  98]---> BDD-cost:    8
c ---[  97]---> BDD-cost:    8
c ---[  96]---> BDD-cost:    8
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    8
c ---[  90]---> BDD-cost:    8
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:    8
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:    8
c ---[  84]---> BDD-cost:    8
c ---[  83]---> BDD-cost:    8
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    8
c ---[  80]---> BDD-cost:    8
c ---[  79]---> BDD-cost:    8
c ---[  78]---> BDD-cost:    8
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    8
c ---[  73]---> BDD-cost:    8
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    8
c ---[  70]---> BDD-cost:    8
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    8
c ---[  65]---> BDD-cost:    8
c ---[  64]---> BDD-cost:    8
c ---[  63]---> BDD-cost:    8
c ---[  62]---> BDD-cost:    8
c ---[  61]---> BDD-cost:    8
c ---[  60]---> BDD-cost:    8
c ---[  59]---> BDD-cost:    8
c ---[  58]---> BDD-cost:    8
c ---[  57]---> BDD-cost:    8
c ---[  56]---> BDD-cost:    8
c ---[  55]---> BDD-cost:    8
c ---[  54]---> BDD-cost:    8
c ---[  53]---> BDD-cost:    8
c ---[  52]---> BDD-cost:    8
c ---[  51]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:    8
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:    8
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    8
c ---[  43]---> BDD-cost:    8
c ---[  42]---> BDD-cost:    8
c ---[  41]---> BDD-cost:    8
c ---[  40]---> BDD-cost:    8
c ---[  39]---> BDD-cost:    8
c ---[  38]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    8
c ---[  36]---> BDD-cost:    8
c ---[  35]---> BDD-cost:    8
c ---[  34]---> BDD-cost:    8
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    8
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:    8
c ---[  23]---> Adder-cost: 16837   maxlim: 101745   bits: 18/17
c ---[  22]---> Adder-cost: 35787   maxlim: 6633569   bits: 24/23
c ---[  21]---> Adder-cost: 18126   maxlim: 4660379   bits: 24/23
c ---[  20]---> Adder-cost: 13526   maxlim: 7782034   bits: 24/23
c ---[  19]---> Adder-cost: 46920   maxlim: 49412548   bits: 27/26
c ---[  18]---> Adder-cost: 7270   maxlim: 202757   bits: 18/18
c ---[  17]---> Adder-cost: 28854   maxlim: 3340290   bits: 23/22
c ---[  16]---> Adder-cost: 44525   maxlim: 3367019   bits: 23/22
c ---[  15]---> Adder-cost: 37629   maxlim: 7305239   bits: 24/23
c ---[  14]---> Adder-cost: 14038   maxlim: 171104   bits: 19/18
c ---[  13]---> Adder-cost: 18310   maxlim: 585650   bits: 20/20
c ---[  12]---> Adder-cost: 51276   maxlim: 48594727   bits: 27/26
c ---[  11]---> Adder-cost: 2096   maxlim: 88902   bits: 17/17
c ---[  10]---> Adder-cost: 8416   maxlim: 4571464   bits: 23/23
c ---[   9]---> Adder-cost: 28701   maxlim: 3985139   bits: 23/22
c ---[   8]---> Adder-cost: 4168   maxlim: 64077   bits: 17/16
c ---[   7]---> Adder-cost: 4299   maxlim: 30599   bits: 16/15
c ---[   6]---> Adder-cost: 4676   maxlim: 35189   bits: 17/16
c ---[   5]---> Adder-cost: 8358   maxlim: 67319   bits: 18/17
c ---[   4]---> Adder-cost: 4270   maxlim: 73024   bits: 17/17
c ---[   3]---> Adder-cost: 3309   maxlim: 24989   bits: 16/15
c ---[   2]---> Adder-cost: 2149   maxlim: 15809   bits: 15/14
c ---[   1]---> Adder-cost: 5642   maxlim: 93949   bits: 18/17
c ---[   0]---> Adder-cost: 3842   maxlim: 34424   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2897016 10335363 |  965672       0        0     nan |  0.000 % |
c |       100 | 2897016 10335363 | 1062239     100      316     3.2 |  0.309 % |
c |       250 | 2897016 10335363 | 1168463     250      805     3.2 |  0.309 % |
c |       475 | 2897016 10335363 | 1285309     475     1622     3.4 |  0.309 % |
c |       812 | 2897016 10335363 | 1413840     812     2791     3.4 |  0.309 % |
c |      1318 | 2897016 10335363 | 1555224    1318     4644     3.5 |  0.309 % |
c |      2078 | 2897016 10335363 | 1710746    2078     8307     4.0 |  0.309 % |
c |      3217 | 2897016 10335363 | 1881821    3217    12398     3.9 |  0.309 % |
c |      4926 | 2897016 10335363 | 2070003    4926    20547     4.2 |  0.309 % |
c |      7488 | 2897016 10335363 | 2277004    7488    31967     4.3 |  0.309 % |
c |     11332 | 2897016 10335363 | 2504704   11332    46641     4.1 |  0.309 % |
c |     17098 | 2897016 10335363 | 2755174   17098   118769     6.9 |  0.309 % |
c |     25748 | 2897016 10335363 | 3030692   25748   521490    20.3 |  0.309 % |
c |     38722 | 2897016 10335363 | 3333761   38722   599222    15.5 |  0.309 % |
c |     58183 | 2897016 10335363 | 3667137   58183  1594932    27.4 |  0.309 % |
c |     87375 | 2897002 10335317 | 4033851   87373  2712476    31.0 |  0.309 % |
c |    131165 | 2896996 10335300 | 4437236  131160  5322261    40.6 |  0.309 % |
c |    196849 | 2896984 10335266 | 4880960  196842  7921653    40.2 |  0.310 % |
c |    295376 | 2896984 10335266 | 5369056  295369 17704313    59.9 |  0.310 % |

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/28078/stat): 28078 (minisat+_script) R 28077 28078 2660 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1854994383 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/28078/statm): 174 3 169 147 0 27 0
[pid=28078] 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=28079
New process pid=28080
New process pid=28081
execve syscall for /bin/sed executable
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
One traced child (pid=28080) exited with status: 0
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=28081) exited with status: 0
One traced child (pid=28079) exited with status: 0
New process pid=28082
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-fit1d.opb

[startup+10.0037 s]
Raw data (loadavg): 0.80 0.94 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 7653 0 0 0 948 28 0 0 25 0 1 0 1854994388 21917696 4147 4294967295 134512640 135094434 3221224432 3221222688 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 5351 4147 145 145 0 5206 0
[pid=28082] vsize: 21404
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 23528

[startup+20.0044 s]
Raw data (loadavg): 0.83 0.94 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 1919 46 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221220752 134676510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 19.67
Current children cumulated vsize (Kb) 41368

[startup+30.0051 s]
Raw data (loadavg): 0.85 0.94 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 2919 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 29.68
Current children cumulated vsize (Kb) 41368

[startup+40.0058 s]
Raw data (loadavg): 0.88 0.94 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 3919 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221552 134676349 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 39.68
Current children cumulated vsize (Kb) 41368

[startup+50.0066 s]
Raw data (loadavg): 0.89 0.94 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 4919 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221024 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 49.68
Current children cumulated vsize (Kb) 41368

[startup+60.0073 s]
Raw data (loadavg): 0.91 0.94 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 5919 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221808 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 59.68
Current children cumulated vsize (Kb) 41368

[startup+70.008 s]
Raw data (loadavg): 0.92 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 6920 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 69.69
Current children cumulated vsize (Kb) 41368

[startup+80.0088 s]
Raw data (loadavg): 0.93 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 7920 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 41368

[startup+90.0095 s]
Raw data (loadavg): 0.94 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 8920 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 41368

[startup+100.009 s]
Raw data (loadavg): 0.95 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 12367 0 0 0 9920 47 0 0 25 0 1 0 1854994388 40185856 7156 4294967295 134512640 135094434 3221224432 3221221984 134600225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 9811 7156 145 145 0 9666 0
[pid=28082] vsize: 39244
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 41368

[startup+110.01 s]
Raw data (loadavg): 0.96 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 20166 0 0 0 10875 73 0 0 25 0 1 0 1854994388 70807552 13389 4294967295 134512640 135094434 3221224432 3221221912 134541445 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 17287 13389 145 145 0 17142 0
[pid=28082] vsize: 69148
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 71272

[startup+120.011 s]
Raw data (loadavg): 0.97 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 21303 0 0 0 11869 77 0 0 25 0 1 0 1854994388 71090176 13414 4294967295 134512640 135094434 3221224432 3221221328 134519153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 17356 13414 145 145 0 17211 0
[pid=28082] vsize: 69424
Current children cumulated CPU time (s) 119.48
Current children cumulated vsize (Kb) 71548

[startup+130.01 s]
Raw data (loadavg): 0.97 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 21718 0 0 0 12867 78 0 0 25 0 1 0 1854994388 70762496 13372 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 17276 13372 145 145 0 17131 0
[pid=28082] vsize: 69104
Current children cumulated CPU time (s) 129.47
Current children cumulated vsize (Kb) 71228

[startup+140.011 s]
Raw data (loadavg): 0.97 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 22718 0 0 0 13863 81 0 0 25 0 1 0 1854994388 70762496 13372 4294967295 134512640 135094434 3221224432 3221221704 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 17276 13372 145 145 0 17131 0
[pid=28082] vsize: 69104
Current children cumulated CPU time (s) 139.46
Current children cumulated vsize (Kb) 71228

[startup+150.012 s]
Raw data (loadavg): 0.98 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 22718 0 0 0 14862 82 0 0 25 0 1 0 1854994388 70762496 13372 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 17276 13372 145 145 0 17131 0
[pid=28082] vsize: 69104
Current children cumulated CPU time (s) 149.46
Current children cumulated vsize (Kb) 71228

[startup+160.013 s]
Raw data (loadavg): 0.98 0.95 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 22718 0 0 0 15861 83 0 0 25 0 1 0 1854994388 70762496 13372 4294967295 134512640 135094434 3221224432 3221221552 134676280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 17276 13372 145 145 0 17131 0
[pid=28082] vsize: 69104
Current children cumulated CPU time (s) 159.46
Current children cumulated vsize (Kb) 71228

[startup+170.013 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 22718 0 0 0 16862 83 0 0 25 0 1 0 1854994388 70762496 13372 4294967295 134512640 135094434 3221224432 3221221984 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 17276 13372 145 145 0 17131 0
[pid=28082] vsize: 69104
Current children cumulated CPU time (s) 169.47
Current children cumulated vsize (Kb) 71228

[startup+180.014 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 23799 0 0 0 17855 86 0 0 25 0 1 0 1854994388 71684096 13715 4294967295 134512640 135094434 3221224432 3221221952 134518677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 17501 13715 145 145 0 17356 0
[pid=28082] vsize: 70004
Current children cumulated CPU time (s) 179.43
Current children cumulated vsize (Kb) 72128

[startup+190.015 s]
Raw data (loadavg): 0.99 0.96 0.92 1/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) T 28078 28078 2660 0 -1 0 39088 0 0 0 18729 147 0 0 22 0 1 0 1854994388 139714560 28674 4294967295 134512640 135094434 3221224432 3221215292 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28082/statm): 34110 28674 145 145 0 33965 0
[pid=28082] vsize: 136440
Current children cumulated CPU time (s) 188.78
Current children cumulated vsize (Kb) 138564

[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 64108 0 0 0 19499 256 0 0 25 0 1 0 1854994388 244875264 53694 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 59784 53694 145 145 0 59639 0
[pid=28082] vsize: 239136
Current children cumulated CPU time (s) 197.57
Current children cumulated vsize (Kb) 241260

[startup+210.016 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 64757 0 0 0 20488 260 0 0 25 0 1 0 1854994388 247533568 54343 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 60433 54343 145 145 0 60288 0
[pid=28082] vsize: 241732
Current children cumulated CPU time (s) 207.5
Current children cumulated vsize (Kb) 243856

[startup+220.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 65197 0 0 0 21481 263 0 0 25 0 1 0 1854994388 249372672 54783 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 60882 54783 145 145 0 60737 0
[pid=28082] vsize: 243528
Current children cumulated CPU time (s) 217.46
Current children cumulated vsize (Kb) 245652

[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.92 1/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) T 28078 28078 2660 0 -1 0 65601 0 0 0 22471 268 0 0 25 0 1 0 1854994388 251011072 55187 4294967295 134512640 135094434 3221224432 3221222844 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28082/statm): 61282 55187 145 145 0 61137 0
[pid=28082] vsize: 245128
Current children cumulated CPU time (s) 227.41
Current children cumulated vsize (Kb) 247252

[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 65949 0 0 0 23466 270 0 0 25 0 1 0 1854994388 252424192 55535 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 61627 55535 145 145 0 61482 0
[pid=28082] vsize: 246508
Current children cumulated CPU time (s) 237.38
Current children cumulated vsize (Kb) 248632

[startup+250.018 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 66386 0 0 0 24459 273 0 0 25 0 1 0 1854994388 254259200 55972 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 62075 55972 145 145 0 61930 0
[pid=28082] vsize: 248300
Current children cumulated CPU time (s) 247.34
Current children cumulated vsize (Kb) 250424

[startup+260.019 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 66736 0 0 0 25452 276 0 0 25 0 1 0 1854994388 255672320 56322 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 62420 56322 145 145 0 62275 0
[pid=28082] vsize: 249680
Current children cumulated CPU time (s) 257.3
Current children cumulated vsize (Kb) 251804

[startup+270.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 66897 0 0 0 26449 278 0 0 25 0 1 0 1854994388 256323584 56483 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 62579 56483 145 145 0 62434 0
[pid=28082] vsize: 250316
Current children cumulated CPU time (s) 267.29
Current children cumulated vsize (Kb) 252440

[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67044 0 0 0 27446 279 0 0 25 0 1 0 1854994388 256921600 56630 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 62725 56630 145 145 0 62580 0
[pid=28082] vsize: 250900
Current children cumulated CPU time (s) 277.27
Current children cumulated vsize (Kb) 253024

[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67144 0 0 0 28445 280 0 0 25 0 1 0 1854994388 257314816 56730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 62821 56730 145 145 0 62676 0
[pid=28082] vsize: 251284
Current children cumulated CPU time (s) 287.27
Current children cumulated vsize (Kb) 253408

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67252 0 0 0 29443 281 0 0 25 0 1 0 1854994388 257863680 56838 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 62955 56838 145 145 0 62810 0
[pid=28082] vsize: 251820
Current children cumulated CPU time (s) 297.26
Current children cumulated vsize (Kb) 253944

[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67340 0 0 0 30441 282 0 0 25 0 1 0 1854994388 258207744 56926 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 63039 56926 145 145 0 62894 0
[pid=28082] vsize: 252156
Current children cumulated CPU time (s) 307.25
Current children cumulated vsize (Kb) 254280

[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67424 0 0 0 31440 283 0 0 25 0 1 0 1854994388 258535424 57010 4294967295 134512640 135094434 3221224432 3221223080 134558037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 63119 57010 145 145 0 62974 0
[pid=28082] vsize: 252476
Current children cumulated CPU time (s) 317.25
Current children cumulated vsize (Kb) 254600

[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67503 0 0 0 32438 284 0 0 25 0 1 0 1854994388 258846720 57089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 63195 57089 145 145 0 63050 0
[pid=28082] vsize: 252780
Current children cumulated CPU time (s) 327.24
Current children cumulated vsize (Kb) 254904

[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67598 0 0 0 33436 285 0 0 25 0 1 0 1854994388 259227648 57184 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 63288 57184 145 145 0 63143 0
[pid=28082] vsize: 253152
Current children cumulated CPU time (s) 337.23
Current children cumulated vsize (Kb) 255276

[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 67802 0 0 0 34432 286 0 0 25 0 1 0 1854994388 260046848 57388 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 63488 57388 145 145 0 63343 0
[pid=28082] vsize: 253952
Current children cumulated CPU time (s) 347.2
Current children cumulated vsize (Kb) 256076

[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 68543 0 0 0 35420 292 0 0 25 0 1 0 1854994388 263061504 58129 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 64224 58129 145 145 0 64079 0
[pid=28082] vsize: 256896
Current children cumulated CPU time (s) 357.14
Current children cumulated vsize (Kb) 259020

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 68887 0 0 0 36414 295 0 0 25 0 1 0 1854994388 264458240 58473 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 64565 58473 145 145 0 64420 0
[pid=28082] vsize: 258260
Current children cumulated CPU time (s) 367.11
Current children cumulated vsize (Kb) 260384

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 69314 0 0 0 37405 298 0 0 25 0 1 0 1854994388 266436608 58900 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 65048 58900 145 145 0 64903 0
[pid=28082] vsize: 260192
Current children cumulated CPU time (s) 377.05
Current children cumulated vsize (Kb) 262316

[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 69679 0 0 0 38400 300 0 0 25 0 1 0 1854994388 267931648 59265 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 65413 59265 145 145 0 65268 0
[pid=28082] vsize: 261652
Current children cumulated CPU time (s) 387.02
Current children cumulated vsize (Kb) 263776

[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 69874 0 0 0 39397 302 0 0 25 0 1 0 1854994388 268718080 59460 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 65605 59460 145 145 0 65460 0
[pid=28082] vsize: 262420
Current children cumulated CPU time (s) 397.01
Current children cumulated vsize (Kb) 264544

[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 70245 0 0 0 40391 305 0 0 25 0 1 0 1854994388 270217216 59831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 65971 59831 145 145 0 65826 0
[pid=28082] vsize: 263884
Current children cumulated CPU time (s) 406.98
Current children cumulated vsize (Kb) 266008

[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 70438 0 0 0 41387 306 0 0 25 0 1 0 1854994388 270987264 60024 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 66159 60024 145 145 0 66014 0
[pid=28082] vsize: 264636
Current children cumulated CPU time (s) 416.95
Current children cumulated vsize (Kb) 266760

[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 70521 0 0 0 42385 307 0 0 25 0 1 0 1854994388 271323136 60107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 66241 60107 145 145 0 66096 0
[pid=28082] vsize: 264964
Current children cumulated CPU time (s) 426.94
Current children cumulated vsize (Kb) 267088

[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 70674 0 0 0 43383 308 0 0 25 0 1 0 1854994388 271945728 60260 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 66393 60260 145 145 0 66248 0
[pid=28082] vsize: 265572
Current children cumulated CPU time (s) 436.93
Current children cumulated vsize (Kb) 267696

[startup+450.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 71021 0 0 0 44377 311 0 0 25 0 1 0 1854994388 273346560 60607 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 66735 60607 145 145 0 66590 0
[pid=28082] vsize: 266940
Current children cumulated CPU time (s) 446.9
Current children cumulated vsize (Kb) 269064

[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 71620 0 0 0 45368 315 0 0 25 0 1 0 1854994388 275767296 61206 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67326 61206 145 145 0 67181 0
[pid=28082] vsize: 269304
Current children cumulated CPU time (s) 456.85
Current children cumulated vsize (Kb) 271428

[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 71697 0 0 0 46366 315 0 0 25 0 1 0 1854994388 276074496 61283 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67401 61283 145 145 0 67256 0
[pid=28082] vsize: 269604
Current children cumulated CPU time (s) 466.83
Current children cumulated vsize (Kb) 271728

[startup+480.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 71778 0 0 0 47365 316 0 0 25 0 1 0 1854994388 276393984 61364 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67479 61364 145 145 0 67334 0
[pid=28082] vsize: 269916
Current children cumulated CPU time (s) 476.83
Current children cumulated vsize (Kb) 272040

[startup+490.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 71836 0 0 0 48364 317 0 0 25 0 1 0 1854994388 276627456 61422 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67536 61422 145 145 0 67391 0
[pid=28082] vsize: 270144
Current children cumulated CPU time (s) 486.83
Current children cumulated vsize (Kb) 272268

[startup+500.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 71929 0 0 0 49361 318 0 0 25 0 1 0 1854994388 276996096 61515 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67626 61515 145 145 0 67481 0
[pid=28082] vsize: 270504
Current children cumulated CPU time (s) 496.81
Current children cumulated vsize (Kb) 272628

[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 72005 0 0 0 50360 319 0 0 25 0 1 0 1854994388 277266432 61591 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67692 61591 145 145 0 67547 0
[pid=28082] vsize: 270768
Current children cumulated CPU time (s) 506.81
Current children cumulated vsize (Kb) 272892

[startup+520.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 72075 0 0 0 51359 319 0 0 25 0 1 0 1854994388 277524480 61661 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67755 61661 145 145 0 67610 0
[pid=28082] vsize: 271020
Current children cumulated CPU time (s) 516.8
Current children cumulated vsize (Kb) 273144

[startup+530.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 72123 0 0 0 52359 320 0 0 25 0 1 0 1854994388 277712896 61709 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67801 61709 145 145 0 67656 0
[pid=28082] vsize: 271204
Current children cumulated CPU time (s) 526.81
Current children cumulated vsize (Kb) 273328

[startup+540.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 72183 0 0 0 53358 320 0 0 25 0 1 0 1854994388 277950464 61769 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 67859 61769 145 145 0 67714 0
[pid=28082] vsize: 271436
Current children cumulated CPU time (s) 536.8
Current children cumulated vsize (Kb) 273560

[startup+550.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 72808 0 0 0 54348 325 0 0 25 0 1 0 1854994388 280485888 62394 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 68478 62394 145 145 0 68333 0
[pid=28082] vsize: 273912
Current children cumulated CPU time (s) 546.75
Current children cumulated vsize (Kb) 276036

[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 73586 0 0 0 55335 330 0 0 25 0 1 0 1854994388 283660288 63172 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 69253 63172 145 145 0 69108 0
[pid=28082] vsize: 277012
Current children cumulated CPU time (s) 556.67
Current children cumulated vsize (Kb) 279136

[startup+570.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 73932 0 0 0 56328 333 0 0 25 0 1 0 1854994388 285622272 63518 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 69732 63518 145 145 0 69587 0
[pid=28082] vsize: 278928
Current children cumulated CPU time (s) 566.63
Current children cumulated vsize (Kb) 281052

[startup+580.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 74018 0 0 0 57325 334 0 0 25 0 1 0 1854994388 285958144 63604 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 69814 63604 145 145 0 69669 0
[pid=28082] vsize: 279256
Current children cumulated CPU time (s) 576.61
Current children cumulated vsize (Kb) 281380

[startup+590.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 74334 0 0 0 58320 335 0 0 25 0 1 0 1854994388 287244288 63920 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 70128 63920 145 145 0 69983 0
[pid=28082] vsize: 280512
Current children cumulated CPU time (s) 586.57
Current children cumulated vsize (Kb) 282636

[startup+600.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 74577 0 0 0 59315 338 0 0 25 0 1 0 1854994388 288202752 64163 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 70362 64163 145 145 0 70217 0
[pid=28082] vsize: 281448
Current children cumulated CPU time (s) 596.55
Current children cumulated vsize (Kb) 283572

[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 74844 0 0 0 60310 339 0 0 25 0 1 0 1854994388 289275904 64430 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 70624 64430 145 145 0 70479 0
[pid=28082] vsize: 282496
Current children cumulated CPU time (s) 606.51
Current children cumulated vsize (Kb) 284620

[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 75083 0 0 0 61307 341 0 0 25 0 1 0 1854994388 290263040 64669 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 70865 64669 145 145 0 70720 0
[pid=28082] vsize: 283460
Current children cumulated CPU time (s) 616.5
Current children cumulated vsize (Kb) 285584

[startup+630.041 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) T 28078 28078 2660 0 -1 0 75292 0 0 0 62303 343 0 0 25 0 1 0 1854994388 291106816 64878 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28082/statm): 71071 64878 145 145 0 70926 0
[pid=28082] vsize: 284284
Current children cumulated CPU time (s) 626.48
Current children cumulated vsize (Kb) 286408

[startup+640.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 75498 0 0 0 63299 345 0 0 25 0 1 0 1854994388 291971072 65084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 71282 65084 145 145 0 71137 0
[pid=28082] vsize: 285128
Current children cumulated CPU time (s) 636.46
Current children cumulated vsize (Kb) 287252

[startup+650.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 75693 0 0 0 64296 346 0 0 25 0 1 0 1854994388 292769792 65279 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 71477 65279 145 145 0 71332 0
[pid=28082] vsize: 285908
Current children cumulated CPU time (s) 646.44
Current children cumulated vsize (Kb) 288032

[startup+660.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 75866 0 0 0 65294 347 0 0 21 0 1 0 1854994388 293482496 65452 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 71651 65452 145 145 0 71506 0
[pid=28082] vsize: 286604
Current children cumulated CPU time (s) 656.43
Current children cumulated vsize (Kb) 288728

[startup+670.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 76065 0 0 0 66291 348 0 0 25 0 1 0 1854994388 294330368 65651 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 71858 65651 145 145 0 71713 0
[pid=28082] vsize: 287432
Current children cumulated CPU time (s) 666.41
Current children cumulated vsize (Kb) 289556

[startup+680.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 76222 0 0 0 67289 349 0 0 25 0 1 0 1854994388 295002112 65808 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 72022 65808 145 145 0 71877 0
[pid=28082] vsize: 288088
Current children cumulated CPU time (s) 676.4
Current children cumulated vsize (Kb) 290212

[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 76397 0 0 0 68286 350 0 0 25 0 1 0 1854994388 295706624 65983 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 72194 65983 145 145 0 72049 0
[pid=28082] vsize: 288776
Current children cumulated CPU time (s) 686.38
Current children cumulated vsize (Kb) 290900

[startup+700.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 76560 0 0 0 69284 351 0 0 25 0 1 0 1854994388 296374272 66146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 72357 66146 145 145 0 72212 0
[pid=28082] vsize: 289428
Current children cumulated CPU time (s) 696.37
Current children cumulated vsize (Kb) 291552

[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 76733 0 0 0 70282 352 0 0 25 0 1 0 1854994388 297107456 66319 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 72536 66319 145 145 0 72391 0
[pid=28082] vsize: 290144
Current children cumulated CPU time (s) 706.36
Current children cumulated vsize (Kb) 292268

[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 76867 0 0 0 71279 354 0 0 25 0 1 0 1854994388 297635840 66453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 72665 66453 145 145 0 72520 0
[pid=28082] vsize: 290660
Current children cumulated CPU time (s) 716.35
Current children cumulated vsize (Kb) 292784

[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 76997 0 0 0 72278 355 0 0 25 0 1 0 1854994388 298205184 66583 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 72804 66583 145 145 0 72659 0
[pid=28082] vsize: 291216
Current children cumulated CPU time (s) 726.35
Current children cumulated vsize (Kb) 293340

[startup+740.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77156 0 0 0 73274 356 0 0 25 0 1 0 1854994388 298893312 66742 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 72972 66742 145 145 0 72827 0
[pid=28082] vsize: 291888
Current children cumulated CPU time (s) 736.32
Current children cumulated vsize (Kb) 294012

[startup+750.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77198 0 0 0 74272 358 0 0 25 0 1 0 1854994388 299061248 66784 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73013 66784 145 145 0 72868 0
[pid=28082] vsize: 292052
Current children cumulated CPU time (s) 746.32
Current children cumulated vsize (Kb) 294176

[startup+760.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77235 0 0 0 75271 359 0 0 25 0 1 0 1854994388 299208704 66821 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73049 66821 145 145 0 72904 0
[pid=28082] vsize: 292196
Current children cumulated CPU time (s) 756.32
Current children cumulated vsize (Kb) 294320

[startup+770.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77272 0 0 0 76270 360 0 0 25 0 1 0 1854994388 299352064 66858 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73084 66858 145 145 0 72939 0
[pid=28082] vsize: 292336
Current children cumulated CPU time (s) 766.32
Current children cumulated vsize (Kb) 294460

[startup+780.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77386 0 0 0 77268 361 0 0 25 0 1 0 1854994388 299810816 66972 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73196 66972 145 145 0 73051 0
[pid=28082] vsize: 292784
Current children cumulated CPU time (s) 776.31
Current children cumulated vsize (Kb) 294908

[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77429 0 0 0 78267 362 0 0 25 0 1 0 1854994388 299978752 67015 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73237 67015 145 145 0 73092 0
[pid=28082] vsize: 292948
Current children cumulated CPU time (s) 786.31
Current children cumulated vsize (Kb) 295072

[startup+800.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77465 0 0 0 79266 362 0 0 25 0 1 0 1854994388 300122112 67051 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73272 67051 145 145 0 73127 0
[pid=28082] vsize: 293088
Current children cumulated CPU time (s) 796.3
Current children cumulated vsize (Kb) 295212

[startup+810.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77520 0 0 0 80265 363 0 0 25 0 1 0 1854994388 300339200 67106 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73325 67106 145 145 0 73180 0
[pid=28082] vsize: 293300
Current children cumulated CPU time (s) 806.3
Current children cumulated vsize (Kb) 295424

[startup+820.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77566 0 0 0 81265 363 0 0 25 0 1 0 1854994388 300498944 67152 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73364 67152 145 145 0 73219 0
[pid=28082] vsize: 293456
Current children cumulated CPU time (s) 816.3
Current children cumulated vsize (Kb) 295580

[startup+830.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77601 0 0 0 82264 364 0 0 25 0 1 0 1854994388 300638208 67187 4294967295 134512640 135094434 3221224432 3221223080 134558260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73398 67187 145 145 0 73253 0
[pid=28082] vsize: 293592
Current children cumulated CPU time (s) 826.3
Current children cumulated vsize (Kb) 295716

[startup+840.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77639 0 0 0 83263 364 0 0 25 0 1 0 1854994388 300785664 67225 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73434 67225 145 145 0 73289 0
[pid=28082] vsize: 293736
Current children cumulated CPU time (s) 836.29
Current children cumulated vsize (Kb) 295860

[startup+850.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77674 0 0 0 84263 364 0 0 25 0 1 0 1854994388 300924928 67260 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73468 67260 145 145 0 73323 0
[pid=28082] vsize: 293872
Current children cumulated CPU time (s) 846.29
Current children cumulated vsize (Kb) 295996

[startup+860.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77702 0 0 0 85263 365 0 0 25 0 1 0 1854994388 301031424 67288 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73494 67288 145 145 0 73349 0
[pid=28082] vsize: 293976
Current children cumulated CPU time (s) 856.3
Current children cumulated vsize (Kb) 296100

[startup+870.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77738 0 0 0 86262 365 0 0 25 0 1 0 1854994388 301170688 67324 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73528 67324 145 145 0 73383 0
[pid=28082] vsize: 294112
Current children cumulated CPU time (s) 866.29
Current children cumulated vsize (Kb) 296236

[startup+880.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77773 0 0 0 87262 365 0 0 25 0 1 0 1854994388 301305856 67359 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73561 67359 145 145 0 73416 0
[pid=28082] vsize: 294244
Current children cumulated CPU time (s) 876.29
Current children cumulated vsize (Kb) 296368

[startup+890.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77838 0 0 0 88260 366 0 0 25 0 1 0 1854994388 301563904 67424 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73624 67424 145 145 0 73479 0
[pid=28082] vsize: 294496
Current children cumulated CPU time (s) 886.28
Current children cumulated vsize (Kb) 296620

[startup+900.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77905 0 0 0 89260 367 0 0 25 0 1 0 1854994388 301817856 67491 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73686 67491 145 145 0 73541 0
[pid=28082] vsize: 294744
Current children cumulated CPU time (s) 896.29
Current children cumulated vsize (Kb) 296868

[startup+910.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77940 0 0 0 90259 367 0 0 25 0 1 0 1854994388 301953024 67526 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73719 67526 145 145 0 73574 0
[pid=28082] vsize: 294876
Current children cumulated CPU time (s) 906.28
Current children cumulated vsize (Kb) 297000

[startup+920.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 77985 0 0 0 91258 367 0 0 25 0 1 0 1854994388 302129152 67571 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 73762 67571 145 145 0 73617 0
[pid=28082] vsize: 295048
Current children cumulated CPU time (s) 916.27
Current children cumulated vsize (Kb) 297172

[startup+930.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 78535 0 0 0 92248 372 0 0 25 0 1 0 1854994388 304357376 68121 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 74306 68121 145 145 0 74161 0
[pid=28082] vsize: 297224
Current children cumulated CPU time (s) 926.22
Current children cumulated vsize (Kb) 299348

[startup+940.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 79319 0 0 0 93234 378 0 0 25 0 1 0 1854994388 307548160 68905 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 75085 68905 145 145 0 74940 0
[pid=28082] vsize: 300340
Current children cumulated CPU time (s) 936.14
Current children cumulated vsize (Kb) 302464

[startup+950.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 79833 0 0 0 94226 381 0 0 25 0 1 0 1854994388 309641216 69419 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 75596 69419 145 145 0 75451 0
[pid=28082] vsize: 302384
Current children cumulated CPU time (s) 946.09
Current children cumulated vsize (Kb) 304508

[startup+960.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 80481 0 0 0 95216 386 0 0 25 0 1 0 1854994388 312279040 70067 4294967295 134512640 135094434 3221224432 3221223056 134539544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 76240 70067 145 145 0 76095 0
[pid=28082] vsize: 304960
Current children cumulated CPU time (s) 956.04
Current children cumulated vsize (Kb) 307084

[startup+970.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 81065 0 0 0 96205 390 0 0 25 0 1 0 1854994388 314650624 70651 4294967295 134512640 135094434 3221224432 3221223024 134551897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 76819 70651 145 145 0 76674 0
[pid=28082] vsize: 307276
Current children cumulated CPU time (s) 965.97
Current children cumulated vsize (Kb) 309400

[startup+980.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 81738 0 0 0 97193 396 0 0 25 0 1 0 1854994388 317382656 71324 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 77486 71324 145 145 0 77341 0
[pid=28082] vsize: 309944
Current children cumulated CPU time (s) 975.91
Current children cumulated vsize (Kb) 312068

[startup+990.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 82331 0 0 0 98181 401 0 0 25 0 1 0 1854994388 319795200 71917 4294967295 134512640 135094434 3221224432 3221222896 134780607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 78075 71917 145 145 0 77930 0
[pid=28082] vsize: 312300
Current children cumulated CPU time (s) 985.84
Current children cumulated vsize (Kb) 314424

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 82889 0 0 0 99171 406 0 0 25 0 1 0 1854994388 323112960 72475 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 78885 72475 145 145 0 78740 0
[pid=28082] vsize: 315540
Current children cumulated CPU time (s) 995.79
Current children cumulated vsize (Kb) 317664

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 83402 0 0 0 100163 409 0 0 25 0 1 0 1854994388 325201920 72988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 79395 72988 145 145 0 79250 0
[pid=28082] vsize: 317580
Current children cumulated CPU time (s) 1005.74
Current children cumulated vsize (Kb) 319704

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 83949 0 0 0 101154 412 0 0 25 0 1 0 1854994388 327434240 73535 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 79940 73535 145 145 0 79795 0
[pid=28082] vsize: 319760
Current children cumulated CPU time (s) 1015.68
Current children cumulated vsize (Kb) 321884

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 84477 0 0 0 102143 418 0 0 25 0 1 0 1854994388 329596928 74063 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 80468 74063 145 145 0 80323 0
[pid=28082] vsize: 321872
Current children cumulated CPU time (s) 1025.63
Current children cumulated vsize (Kb) 323996

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) T 28078 28078 2660 0 -1 0 84977 0 0 0 103134 422 0 0 25 0 1 0 1854994388 331644928 74563 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28082/statm): 80968 74563 145 145 0 80823 0
[pid=28082] vsize: 323872
Current children cumulated CPU time (s) 1035.58
Current children cumulated vsize (Kb) 325996

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 85453 0 0 0 104126 426 0 0 25 0 1 0 1854994388 333598720 75039 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 81445 75039 145 145 0 81300 0
[pid=28082] vsize: 325780
Current children cumulated CPU time (s) 1045.54
Current children cumulated vsize (Kb) 327904

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 85878 0 0 0 105118 430 0 0 25 0 1 0 1854994388 335347712 75464 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 81872 75464 145 145 0 81727 0
[pid=28082] vsize: 327488
Current children cumulated CPU time (s) 1055.5
Current children cumulated vsize (Kb) 329612

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 86331 0 0 0 106110 433 0 0 25 0 1 0 1854994388 337211392 75917 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28082/statm): 82327 75917 145 145 0 82182 0
[pid=28082] vsize: 329308
Current children cumulated CPU time (s) 1065.45
Current children cumulated vsize (Kb) 331432

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 86769 0 0 0 107102 436 0 0 21 0 1 0 1854994388 338993152 76355 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 82762 76355 145 145 0 82617 0
[pid=28082] vsize: 331048
Current children cumulated CPU time (s) 1075.4
Current children cumulated vsize (Kb) 333172

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 87199 0 0 0 108094 441 0 0 25 0 1 0 1854994388 340742144 76785 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 83189 76785 145 145 0 83044 0
[pid=28082] vsize: 332756
Current children cumulated CPU time (s) 1085.37
Current children cumulated vsize (Kb) 334880

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 87589 0 0 0 109087 444 0 0 25 0 1 0 1854994388 342335488 77175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 83578 77175 145 145 0 83433 0
[pid=28082] vsize: 334312
Current children cumulated CPU time (s) 1095.33
Current children cumulated vsize (Kb) 336436

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88008 0 0 0 110080 447 0 0 25 0 1 0 1854994388 344047616 77594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 83996 77594 145 145 0 83851 0
[pid=28082] vsize: 335984
Current children cumulated CPU time (s) 1105.29
Current children cumulated vsize (Kb) 338108

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88153 0 0 0 111078 448 0 0 25 0 1 0 1854994388 344670208 77739 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84148 77739 145 145 0 84003 0
[pid=28082] vsize: 336592
Current children cumulated CPU time (s) 1115.28
Current children cumulated vsize (Kb) 338716

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88246 0 0 0 112076 449 0 0 25 0 1 0 1854994388 345022464 77832 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84234 77832 145 145 0 84089 0
[pid=28082] vsize: 336936
Current children cumulated CPU time (s) 1125.27
Current children cumulated vsize (Kb) 339060

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88353 0 0 0 113075 449 0 0 25 0 1 0 1854994388 345460736 77939 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84341 77939 145 145 0 84196 0
[pid=28082] vsize: 337364
Current children cumulated CPU time (s) 1135.26
Current children cumulated vsize (Kb) 339488

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88475 0 0 0 114073 450 0 0 25 0 1 0 1854994388 345948160 78061 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84460 78061 145 145 0 84315 0
[pid=28082] vsize: 337840
Current children cumulated CPU time (s) 1145.25
Current children cumulated vsize (Kb) 339964

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88586 0 0 0 115072 451 0 0 25 0 1 0 1854994388 346415104 78172 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84574 78172 145 145 0 84429 0
[pid=28082] vsize: 338296
Current children cumulated CPU time (s) 1155.25
Current children cumulated vsize (Kb) 340420

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88697 0 0 0 116070 452 0 0 25 0 1 0 1854994388 346857472 78283 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84682 78283 145 145 0 84537 0
[pid=28082] vsize: 338728
Current children cumulated CPU time (s) 1165.24
Current children cumulated vsize (Kb) 340852

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88805 0 0 0 117069 452 0 0 25 0 1 0 1854994388 347283456 78391 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84786 78391 145 145 0 84641 0
[pid=28082] vsize: 339144
Current children cumulated CPU time (s) 1175.23
Current children cumulated vsize (Kb) 341268

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 88905 0 0 0 118067 453 0 0 25 0 1 0 1854994388 347680768 78491 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84883 78491 145 145 0 84738 0
[pid=28082] vsize: 339532
Current children cumulated CPU time (s) 1185.22
Current children cumulated vsize (Kb) 341656

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 89001 0 0 0 119066 453 0 0 25 0 1 0 1854994388 348057600 78587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 84975 78587 145 145 0 84830 0
[pid=28082] vsize: 339900
Current children cumulated CPU time (s) 1195.21
Current children cumulated vsize (Kb) 342024

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 89111 0 0 0 120065 454 0 0 25 0 1 0 1854994388 348520448 78697 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 85088 78697 145 145 0 84943 0
[pid=28082] vsize: 340352
Current children cumulated CPU time (s) 1205.21
Current children cumulated vsize (Kb) 342476



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28082
Raw data (/proc/28078/stat): 28078 (minisat+_script) S 28077 28078 2660 0 -1 0 289 239 0 0 0 1 0 1 19 0 1 0 1854994383 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28078/statm): 531 226 485 147 0 384 0
[pid=28078] vsize: 2124
Raw data (/proc/28082/stat): 28082 (minisat+_64-bit) R 28078 28078 2660 0 -1 0 89111 0 0 0 120065 454 0 0 25 0 1 0 1854994388 348520448 78697 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28082/statm): 85088 78697 145 145 0 84943 0
[pid=28082] vsize: 340352
Current children cumulated CPU time (s) 1205.21
Current children cumulated vsize (Kb) 342476

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

Child status: 0
Real time (s): 1210.23
CPU time (s): 1205.35
CPU user time (s): 1200.66
CPU system time (s): 4.69229
CPU usage (%): 99.5966
Max. virtual memory (cumulated for all children) (Kb): 342476

Verifier Data

ERROR: no interpretation found !