Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc06.opb
MD5SUMbdef34115ac72b2f3e13f56b51cc3420
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 206346968982065664
Number of bits of the biggest number in a constraint 58
Biggest sum of numbers in a constraint 22661639986845859840
Number of bits of the biggest sum of numbers65
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables34058
Total number of constraints932
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)112
Number of constraints which are nor clauses,nor cardinality constraints820
Minimum length of a constraint1
Maximum length of a constraint8981

Trace number 6088

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        914652 kB
Buffers:         10252 kB
Cached:          84756 kB
SwapCached:        872 kB
Active:          15872 kB
Inactive:        81612 kB
HighTotal:      131008 kB
HighFree:        42364 kB
LowTotal:       903652 kB
LowFree:        872288 kB
SwapTotal:     2097136 kB
SwapFree:      2095548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5516 kB
Slab:            16764 kB
Committed_AS:    72324 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:29:49 (client local time) WITH STATUS 0 IN 936.731 SECONDS
stats: 3250 7 936.731 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 2719] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1005 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .sssssssssssssss
c ---[1019]---> Sorter-cost: 1345     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1018]---> Adder-cost: 380   maxlim: 464747   bits: 20/19
c ---[1017]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1016]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1015]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1014]---> Sorter-cost: 1168     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1013]---> Adder-cost: 380   maxlim: 464747   bits: 20/19
c ---[1012]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1011]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1010]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1009]---> Sorter-cost: 1168     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1008]---> Adder-cost: 380   maxlim: 464747   bits: 20/19
c ---[1007]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1006]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1005]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1004]---> Sorter-cost: 1013     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1003]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1002]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1001]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[1000]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 999]---> Sorter-cost: 1111     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 998]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 997]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 996]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 995]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 993]---> Adder-cost: 380   maxlim: 464747   bits: 20/19
c ---[ 992]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 991]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 990]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 988]---> Adder-cost: 380   maxlim: 464747   bits: 20/19
c ---[ 987]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 986]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 985]---> Adder-cost: 381   maxlim: 606059   bits: 21/20
c ---[ 984]---> Sorter-cost:  704     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 983]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 982]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 981]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 980]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 979]---> Sorter-cost:  604     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 978]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 977]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 976]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 975]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 974]---> Sorter-cost:  604     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 973]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 972]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 971]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 970]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 968]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 967]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 966]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 965]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 963]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 962]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 961]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 960]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 958]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 957]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 956]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 955]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 953]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 951]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 950]---> Sorter-cost: 1197     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 948]---> Sorter-cost:  981     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 947]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 946]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 945]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 943]---> Sorter-cost:  981     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 942]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 941]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 940]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost:  985     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 937]---> Sorter-cost: 1122     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 935]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 934]---> BDD-cost:  103
c ---[ 933]---> Sorter-cost: 1122     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 931]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 929]---> BDD-cost:  175
c ---[ 928]---> Sorter-cost: 1122     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 927]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 926]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 925]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 923]---> Sorter-cost:  985     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost: 1122     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 921]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 920]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 918]---> Sorter-cost:  985     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 917]---> Sorter-cost: 1122     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 916]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 915]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 913]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 912]---> Sorter-cost:  833     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 911]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 910]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 908]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 907]---> Sorter-cost:  833     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 906]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 905]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 903]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 902]---> Sorter-cost:  833     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 901]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 900]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 899]---> BDD-cost:  203
c ---[ 898]---> Sorter-cost:  833     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 897]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 896]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 895]---> Sorter-cost:  797     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 894]---> BDD-cost:  132
c ---[ 893]---> Sorter-cost:  833     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 892]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 891]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 890]---> Sorter-cost:  797     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 888]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 887]---> Sorter-cost:  833     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 886]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 885]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 883]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 882]---> Sorter-cost:  833     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 881]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 880]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 879]---> Sorter-cost: 1662     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 878]---> Sorter-cost: 2152     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 877]---> Sorter-cost: 2152     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 876]---> Sorter-cost: 2152     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 875]---> Sorter-cost: 2152     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 874]---> Sorter-cost: 1445     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 873]---> Sorter-cost: 2019     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 872]---> Sorter-cost: 2019     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 871]---> Sorter-cost: 2019     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 870]---> Sorter-cost: 2019     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 869]---> Sorter-cost:  794     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2
c ---[ 868]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 867]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 866]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 865]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 863]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 862]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 861]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 860]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 858]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 857]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 856]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 855]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 853]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 852]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 851]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 850]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 848]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 847]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 846]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 845]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 844]---> Adder-cost: 252   maxlim: 110081   bits: 18/17
c ---[ 843]---> Sorter-cost: 3551     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 842]---> Sorter-cost: 3551     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 841]---> Sorter-cost: 3551     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 840]---> Sorter-cost: 3551     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 839]---> Adder-cost: 224   maxlim: 54913   bits: 17/16
c ---[ 838]---> Sorter-cost: 3436     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 837]---> Sorter-cost: 3436     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 836]---> Sorter-cost: 3436     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 835]---> Sorter-cost: 3436     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost: 1008     Base: 2 2 2 2 5 2 2 2 2 2 2
c ---[ 833]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 832]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 831]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 830]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 828]---> Sorter-cost: 1928     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2
c ---[ 827]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 826]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 825]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 823]---> Sorter-cost: 1928     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2
c ---[ 822]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 821]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 820]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 818]---> Sorter-cost: 1928     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2
c ---[ 817]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 816]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 815]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 813]---> Sorter-cost: 1928     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 811]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 810]---> Sorter-cost: 2222     Base: 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 809]---> Sorter-cost: 4455     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 808]---> Sorter-cost: 6633     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 807]---> Sorter-cost: 7156     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 806]---> Sorter-cost: 7454     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> Sorter-cost: 7454     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 804]---> Sorter-cost: 4729     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 803]---> Sorter-cost: 6913     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Sorter-cost: 7436     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost: 7734     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 800]---> Sorter-cost: 7734     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Sorter-cost: 4494     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 798]---> Sorter-cost: 6663     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 797]---> Sorter-cost: 7186     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 796]---> Sorter-cost: 7484     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 795]---> Sorter-cost: 7484     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 794]---> Sorter-cost: 6059     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 793]---> Sorter-cost: 7432     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 792]---> Sorter-cost: 7730     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 791]---> Sorter-cost: 7730     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 790]---> Sorter-cost: 8175     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 789]---> Sorter-cost: 5664     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 788]---> Sorter-cost: 7254     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 787]---> Sorter-cost: 7552     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost: 7552     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 785]---> Sorter-cost: 7997     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost: 4455     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost: 6633     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost: 7156     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost: 7454     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost: 7454     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> Sorter-cost: 4120     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> Sorter-cost: 6307     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 777]---> Sorter-cost: 6832     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 776]---> Sorter-cost: 7130     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Sorter-cost: 7130     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2
c ---[ 773]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 771]---> Sorter-cost: 1488     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 770]---> Sorter-cost: 1488     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 769]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost: 1419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 767]---> Sorter-cost: 1443     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost: 1466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 765]---> Sorter-cost: 1466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2
c ---[ 763]---> Sorter-cost: 1265     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 761]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 759]---> Sorter-cost:  397     Base: 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost: 1216     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 757]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 755]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  351     Base: 2 2 2 2 2
c ---[ 753]---> Sorter-cost: 1216     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 751]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost: 1193     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 747]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 745]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 743]---> Sorter-cost: 1193     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 741]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 740]---> Sorter-cost: 1312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 733]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 732]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 731]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 730]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 729]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 728]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 727]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 726]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 725]---> Adder-cost: 260   maxlim: 57336   bits: 16/16
c ---[ 724]---> Adder-cost: 282   maxlim: 114680   bits: 17/17
c ---[ 723]---> Adder-cost: 282   maxlim: 114680   bits: 17/17
c ---[ 722]---> Adder-cost: 282   maxlim: 114680   bits: 17/17
c ---[ 721]---> Adder-cost: 282   maxlim: 114680   bits: 17/17
c ---[ 720]---> Adder-cost: 282   maxlim: 114680   bits: 17/17
c ---[ 709]---> BDD-cost:    7
c ---[ 708]---> BDD-cost:   45
c ---[ 707]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 705]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> BDD-cost:    4
c ---[ 703]---> BDD-cost:   51
c ---[ 702]---> Sorter-cost:  247     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 701]---> Sorter-cost:  426     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  659     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 699]---> BDD-cost:    6
c ---[ 698]---> BDD-cost:   51
c ---[ 697]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 695]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> BDD-cost:   34
c ---[ 693]---> BDD-cost:   99
c ---[ 692]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 691]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> BDD-cost:   34
c ---[ 689]---> BDD-cost:   99
c ---[ 688]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> BDD-cost:   34
c ---[ 685]---> BDD-cost:   99
c ---[ 684]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 683]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> BDD-cost:   34
c ---[ 681]---> BDD-cost:   99
c ---[ 680]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 679]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 2
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:    6
c ---[ 672]---> BDD-cost:    6
c ---[ 671]---> BDD-cost:    6
c ---[ 670]---> BDD-cost:    6
c ---[ 669]---> BDD-cost:    6
c ---[ 668]---> BDD-cost:   38
c ---[ 667]---> Sorter-cost:  260     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 665]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 663]---> BDD-cost:   33
c ---[ 662]---> BDD-cost:  113
c ---[ 661]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> BDD-cost:   28
c ---[ 657]---> Sorter-cost:  258     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 656]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost:  672     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> BDD-cost:   94
c ---[ 652]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 650]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> BDD-cost:   94
c ---[ 648]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> BDD-cost:   94
c ---[ 644]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> BDD-cost:   94
c ---[ 640]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 637]---> BDD-cost:   31
c ---[ 636]---> BDD-cost:   95
c ---[ 635]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> BDD-cost:   31
c ---[ 632]---> BDD-cost:   95
c ---[ 631]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> BDD-cost:   31
c ---[ 628]---> BDD-cost:   95
c ---[ 627]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> BDD-cost:   51
c ---[ 623]---> Sorter-cost:  239     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  410     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 621]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> BDD-cost:    6
c ---[ 619]---> BDD-cost:   39
c ---[ 618]---> BDD-cost:  103
c ---[ 617]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 615]---> BDD-cost:   31
c ---[ 614]---> BDD-cost:   95
c ---[ 613]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> BDD-cost:   31
c ---[ 610]---> BDD-cost:   95
c ---[ 609]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 607]---> BDD-cost:   31
c ---[ 606]---> BDD-cost:   95
c ---[ 605]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> BDD-cost:   31
c ---[ 602]---> BDD-cost:   95
c ---[ 601]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> BDD-cost:   31
c ---[ 598]---> BDD-cost:   95
c ---[ 597]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 596]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 595]---> BDD-cost:    6
c ---[ 594]---> BDD-cost:   45
c ---[ 593]---> Sorter-cost:  247     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:   47
c ---[ 588]---> Sorter-cost:  244     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> BDD-cost:   31
c ---[ 584]---> BDD-cost:   95
c ---[ 583]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> BDD-cost:   31
c ---[ 580]---> BDD-cost:   95
c ---[ 579]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 577]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 2 2
c ---[ 571]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 2 2
c ---[ 567]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 559]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 553]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 543]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 541]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 539]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 535]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 533]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 529]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 527]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 523]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 521]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 519]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 511]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 499]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 487]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 447]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 445]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 443]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 441]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 439]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 437]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 435]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 433]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 431]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 429]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 427]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 425]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 423]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 421]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 419]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 417]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 415]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 413]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 411]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 409]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 407]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 405]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 403]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 401]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 399]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 397]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 395]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 5
c ---[ 393]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 391]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 389]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 387]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 385]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 383]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 381]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 379]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 377]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 375]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 373]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 371]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 369]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 367]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 365]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 363]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 361]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 359]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 357]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 355]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 353]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 351]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 349]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 347]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 345]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 343]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 341]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 339]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 3
c ---[ 337]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 331]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 329]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 327]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 325]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 323]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 317]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 315]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 313]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 309]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 307]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 295]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 293]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 283]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 281]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 279]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 277]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 275]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 273]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 271]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 269]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 267]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 265]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 263]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 261]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 259]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 257]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 239]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 237]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 233]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 231]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 229]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 227]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 157]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 155]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 133]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2
c ---[ 127]---> S

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/7885/stat): 7885 (minisat+_script) R 7884 7885 6872 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796996042 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7885/statm): 174 3 169 147 0 27 0
[pid=7885] 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=7886
New process pid=7887
New process pid=7888
execve syscall for /bin/sed executable
One traced child (pid=7887) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=7888) exited with status: 0
One traced child (pid=7886) exited with status: 0
New process pid=7889
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-misc06.opb
One traced child (pid=7889) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=7890
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-misc06.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.95 0.71 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 3670 0 0 0 874 19 0 0 25 0 1 0 1796996127 15233024 3130 4294967295 134512640 135167914 3221224448 3221221968 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 3719 3130 162 162 0 3557 0
[pid=7890] vsize: 14876
Current children cumulated CPU time (s) 9.66
Current children cumulated vsize (Kb) 17004

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.96 0.72 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4138 0 0 0 1869 23 0 0 25 0 1 0 1796996127 16039936 3347 4294967295 134512640 135167914 3221224448 3221220764 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 3916 3347 162 162 0 3754 0
[pid=7890] vsize: 15664
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 17792

[startup+30.006 s]
Raw data (loadavg): 0.95 0.96 0.72 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4138 0 0 0 2869 23 0 0 25 0 1 0 1796996127 16039936 3347 4294967295 134512640 135167914 3221224448 3221221932 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 3916 3347 162 162 0 3754 0
[pid=7890] vsize: 15664
Current children cumulated CPU time (s) 29.65
Current children cumulated vsize (Kb) 17792

[startup+40.0067 s]
Raw data (loadavg): 0.96 0.96 0.72 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4138 0 0 0 3869 23 0 0 25 0 1 0 1796996127 16039936 3347 4294967295 134512640 135167914 3221224448 3221221088 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 3916 3347 162 162 0 3754 0
[pid=7890] vsize: 15664
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 17792

[startup+50.0074 s]
Raw data (loadavg): 0.96 0.96 0.72 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4198 0 0 0 4869 23 0 0 25 0 1 0 1796996127 16433152 3407 4294967295 134512640 135167914 3221224448 3221221996 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 4012 3407 162 162 0 3850 0
[pid=7890] vsize: 16048
Current children cumulated CPU time (s) 49.65
Current children cumulated vsize (Kb) 18176

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.96 0.73 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4289 0 0 0 5870 23 0 0 25 0 1 0 1796996127 16773120 3498 4294967295 134512640 135167914 3221224448 3221221596 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 4095 3498 162 162 0 3933 0
[pid=7890] vsize: 16380
Current children cumulated CPU time (s) 59.66
Current children cumulated vsize (Kb) 18508

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.96 0.73 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4298 0 0 0 6870 23 0 0 25 0 1 0 1796996127 16773120 3507 4294967295 134512640 135167914 3221224448 3221221008 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 4095 3507 162 162 0 3933 0
[pid=7890] vsize: 16380
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 18508

[startup+80.0095 s]
Raw data (loadavg): 0.98 0.96 0.73 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4332 0 0 0 7870 24 0 0 25 0 1 0 1796996127 17166336 3541 4294967295 134512640 135167914 3221224448 3221221584 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 4191 3541 162 162 0 4029 0
[pid=7890] vsize: 16764
Current children cumulated CPU time (s) 79.67
Current children cumulated vsize (Kb) 18892

[startup+90.0102 s]
Raw data (loadavg): 0.98 0.96 0.73 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4561 0 0 0 8868 25 0 0 25 0 1 0 1796996127 17608704 3687 4294967295 134512640 135167914 3221224448 3221220572 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 4299 3687 162 162 0 4137 0
[pid=7890] vsize: 17196
Current children cumulated CPU time (s) 89.66
Current children cumulated vsize (Kb) 19324

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.74 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 4721 0 0 0 9867 25 0 0 25 0 1 0 1796996127 18808832 3847 4294967295 134512640 135167914 3221224448 3221221120 134629248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 4592 3847 162 162 0 4430 0
[pid=7890] vsize: 18368
Current children cumulated CPU time (s) 99.65
Current children cumulated vsize (Kb) 20496

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.74 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 5313 0 0 0 10864 27 0 0 25 0 1 0 1796996127 20168704 4274 4294967295 134512640 135167914 3221224448 3221221904 134696738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 4924 4274 162 162 0 4762 0
[pid=7890] vsize: 19696
Current children cumulated CPU time (s) 109.64
Current children cumulated vsize (Kb) 21824

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 5606 0 0 0 11862 29 0 0 25 0 1 0 1796996127 22503424 4567 4294967295 134512640 135167914 3221224448 3221216048 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 5494 4567 162 162 0 5332 0
[pid=7890] vsize: 21976
Current children cumulated CPU time (s) 119.64
Current children cumulated vsize (Kb) 24104

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 5816 0 0 0 12860 30 0 0 25 0 1 0 1796996127 23060480 4777 4294967295 134512640 135167914 3221224448 3221222144 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 5630 4777 162 162 0 5468 0
[pid=7890] vsize: 22520
Current children cumulated CPU time (s) 129.63
Current children cumulated vsize (Kb) 24648

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 6649 0 0 0 13857 32 0 0 25 0 1 0 1796996127 24854528 5280 4294967295 134512640 135167914 3221224448 3221221952 134722521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 6068 5280 162 162 0 5906 0
[pid=7890] vsize: 24272
Current children cumulated CPU time (s) 139.62
Current children cumulated vsize (Kb) 26400

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 6846 0 0 0 14856 33 0 0 25 0 1 0 1796996127 25358336 5477 4294967295 134512640 135167914 3221224448 3221221468 134693816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 6191 5477 162 162 0 6029 0
[pid=7890] vsize: 24764
Current children cumulated CPU time (s) 149.62
Current children cumulated vsize (Kb) 26892

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 7040 0 0 0 15855 34 0 0 25 0 1 0 1796996127 25870336 5671 4294967295 134512640 135167914 3221224448 3221220944 134629118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 6316 5671 162 162 0 6154 0
[pid=7890] vsize: 25264
Current children cumulated CPU time (s) 159.62
Current children cumulated vsize (Kb) 27392

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 7183 0 0 0 16855 34 0 0 25 0 1 0 1796996127 26357760 5814 4294967295 134512640 135167914 3221224448 3221220568 134722657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 6435 5814 162 162 0 6273 0
[pid=7890] vsize: 25740
Current children cumulated CPU time (s) 169.62
Current children cumulated vsize (Kb) 27868

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 7419 0 0 0 17854 34 0 0 25 0 1 0 1796996127 26812416 5966 4294967295 134512640 135167914 3221224448 3221221888 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 6546 5966 162 162 0 6384 0
[pid=7890] vsize: 26184
Current children cumulated CPU time (s) 179.61
Current children cumulated vsize (Kb) 28312

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 7540 0 0 0 18854 35 0 0 25 0 1 0 1796996127 30109696 6045 4294967295 134512640 135167914 3221224448 3221221008 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 7351 6045 162 162 0 7189 0
[pid=7890] vsize: 29404
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 31532

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 7574 0 0 0 19854 35 0 0 25 0 1 0 1796996127 30187520 6079 4294967295 134512640 135167914 3221224448 3221220704 134720472 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 7370 6079 162 162 0 7208 0
[pid=7890] vsize: 29480
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 31608

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 7814 0 0 0 20852 36 0 0 25 0 1 0 1796996127 30654464 6235 4294967295 134512640 135167914 3221224448 3221220496 134696335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 7484 6235 162 162 0 7322 0
[pid=7890] vsize: 29936
Current children cumulated CPU time (s) 209.61
Current children cumulated vsize (Kb) 32064

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 7938 0 0 0 21852 36 0 0 25 0 1 0 1796996127 30810112 6317 4294967295 134512640 135167914 3221224448 3221219968 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 7522 6317 162 162 0 7360 0
[pid=7890] vsize: 30088
Current children cumulated CPU time (s) 219.61
Current children cumulated vsize (Kb) 32216

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 8022 0 0 0 22852 36 0 0 25 0 1 0 1796996127 31019008 6401 4294967295 134512640 135167914 3221224448 3221175008 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 7573 6401 162 162 0 7411 0
[pid=7890] vsize: 30292
Current children cumulated CPU time (s) 229.61
Current children cumulated vsize (Kb) 32420

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 8202 0 0 0 23852 37 0 0 25 0 1 0 1796996127 31322112 6497 4294967295 134512640 135167914 3221224448 3221221960 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 7647 6497 162 162 0 7485 0
[pid=7890] vsize: 30588
Current children cumulated CPU time (s) 239.62
Current children cumulated vsize (Kb) 32716

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 9662 0 0 0 24848 41 0 0 25 0 1 0 1796996127 34250752 7256 4294967295 134512640 135167914 3221224448 3221221600 134522821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8362 7256 162 162 0 8200 0
[pid=7890] vsize: 33448
Current children cumulated CPU time (s) 249.62
Current children cumulated vsize (Kb) 35576

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 9876 0 0 0 25846 41 0 0 25 0 1 0 1796996127 34619392 7386 4294967295 134512640 135167914 3221224448 3221220484 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8452 7386 162 162 0 8290 0
[pid=7890] vsize: 33808
Current children cumulated CPU time (s) 259.6
Current children cumulated vsize (Kb) 35936

[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 9979 0 0 0 26846 42 0 0 25 0 1 0 1796996127 34779136 7447 4294967295 134512640 135167914 3221224448 3221221444 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8491 7447 162 162 0 8329 0
[pid=7890] vsize: 33964
Current children cumulated CPU time (s) 269.61
Current children cumulated vsize (Kb) 36092

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 10079 0 0 0 27846 42 0 0 25 0 1 0 1796996127 35000320 7547 4294967295 134512640 135167914 3221224448 3221220848 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8545 7547 162 162 0 8383 0
[pid=7890] vsize: 34180
Current children cumulated CPU time (s) 279.61
Current children cumulated vsize (Kb) 36308

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 10286 0 0 0 28846 42 0 0 25 0 1 0 1796996127 35344384 7670 4294967295 134512640 135167914 3221224448 3221220128 134843118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8629 7670 162 162 0 8467 0
[pid=7890] vsize: 34516
Current children cumulated CPU time (s) 289.61
Current children cumulated vsize (Kb) 36644

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 10388 0 0 0 29846 43 0 0 25 0 1 0 1796996127 35500032 7730 4294967295 134512640 135167914 3221224448 3221220752 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8667 7730 162 162 0 8505 0
[pid=7890] vsize: 34668
Current children cumulated CPU time (s) 299.62
Current children cumulated vsize (Kb) 36796

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 10467 0 0 0 30845 43 0 0 25 0 1 0 1796996127 35643392 7809 4294967295 134512640 135167914 3221224448 3221220832 134718181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 8702 7809 162 162 0 8540 0
[pid=7890] vsize: 34808
Current children cumulated CPU time (s) 309.61
Current children cumulated vsize (Kb) 36936

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 10642 0 0 0 31844 44 0 0 25 0 1 0 1796996127 36048896 7942 4294967295 134512640 135167914 3221224448 3221221632 134845453 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 8801 7942 162 162 0 8639 0
[pid=7890] vsize: 35204
Current children cumulated CPU time (s) 319.61
Current children cumulated vsize (Kb) 37332

[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 10842 0 0 0 32842 44 0 0 25 0 1 0 1796996127 36347904 8058 4294967295 134512640 135167914 3221224448 3221220160 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 8874 8058 162 162 0 8712 0
[pid=7890] vsize: 35496
Current children cumulated CPU time (s) 329.59
Current children cumulated vsize (Kb) 37624

[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 10920 0 0 0 33842 44 0 0 25 0 1 0 1796996127 36532224 8136 4294967295 134512640 135167914 3221224448 3221221292 134694320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8919 8136 162 162 0 8757 0
[pid=7890] vsize: 35676
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 37804

[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 11117 0 0 0 34842 45 0 0 25 0 1 0 1796996127 36835328 8249 4294967295 134512640 135167914 3221224448 3221220320 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 8993 8249 162 162 0 8831 0
[pid=7890] vsize: 35972
Current children cumulated CPU time (s) 349.6
Current children cumulated vsize (Kb) 38100

[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 11429 0 0 0 35840 46 0 0 25 0 1 0 1796996127 37478400 8519 4294967295 134512640 135167914 3221224448 3221222080 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 9150 8519 162 162 0 8988 0
[pid=7890] vsize: 36600
Current children cumulated CPU time (s) 359.59
Current children cumulated vsize (Kb) 38728

[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 12394 0 0 0 36833 49 0 0 25 0 1 0 1796996127 46264320 9484 4294967295 134512640 135167914 3221224448 3221222032 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 11295 9484 162 162 0 11133 0
[pid=7890] vsize: 45180
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 47308

[startup+380.03 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 18821 0 0 0 37799 69 0 0 25 0 1 0 1796996127 65114112 14303 4294967295 134512640 135167914 3221224448 3221106560 134625414 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 15897 14303 162 162 0 15735 0
[pid=7890] vsize: 63588
Current children cumulated CPU time (s) 379.41
Current children cumulated vsize (Kb) 65716

[startup+390.03 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 23584 0 0 0 38758 88 0 0 25 0 1 0 1796996127 80572416 18077 4294967295 134512640 135167914 3221224448 3221106320 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 19671 18077 162 162 0 19509 0
[pid=7890] vsize: 78684
Current children cumulated CPU time (s) 389.19
Current children cumulated vsize (Kb) 80812

[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 29246 0 0 0 39721 107 0 0 25 0 1 0 1796996127 98365440 22421 4294967295 134512640 135167914 3221224448 3221107328 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 24015 22421 162 162 0 23853 0
[pid=7890] vsize: 96060
Current children cumulated CPU time (s) 399.01
Current children cumulated vsize (Kb) 98188

[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 33001 0 0 0 40681 123 0 0 25 0 1 0 1796996127 113745920 26176 4294967295 134512640 135167914 3221224448 3221106832 134625630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 27770 26176 162 162 0 27608 0
[pid=7890] vsize: 111080
Current children cumulated CPU time (s) 408.77
Current children cumulated vsize (Kb) 113208

[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.80 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 36244 0 0 0 41644 138 0 0 25 0 1 0 1796996127 127033344 29419 4294967295 134512640 135167914 3221224448 3221105404 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7890/statm): 31014 29419 162 162 0 30852 0
[pid=7890] vsize: 124056
Current children cumulated CPU time (s) 418.55
Current children cumulated vsize (Kb) 126184

[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 44387 0 0 0 42597 164 0 0 25 0 1 0 1796996127 149581824 34925 4294967295 134512640 135167914 3221224448 3221106752 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 36519 34925 162 162 0 36357 0
[pid=7890] vsize: 146076
Current children cumulated CPU time (s) 428.34
Current children cumulated vsize (Kb) 148204

[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 47898 0 0 0 43560 180 0 0 25 0 1 0 1796996127 163962880 38436 4294967295 134512640 135167914 3221224448 3221107128 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 40030 38436 162 162 0 39868 0
[pid=7890] vsize: 160120
Current children cumulated CPU time (s) 438.13
Current children cumulated vsize (Kb) 162248

[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.80 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 51121 0 0 0 44527 195 0 0 25 0 1 0 1796996127 177168384 41659 4294967295 134512640 135167914 3221224448 3221105372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 43254 41659 162 162 0 43092 0
[pid=7890] vsize: 173016
Current children cumulated CPU time (s) 447.95
Current children cumulated vsize (Kb) 175144

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 54292 0 0 0 45496 208 0 0 25 0 1 0 1796996127 190152704 44830 4294967295 134512640 135167914 3221224448 3221107836 134695136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 46424 44830 162 162 0 46262 0
[pid=7890] vsize: 185696
Current children cumulated CPU time (s) 457.77
Current children cumulated vsize (Kb) 187824

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 59679 0 0 0 46450 229 0 0 25 0 1 0 1796996127 247951360 50218 4294967295 134512640 135167914 3221224448 3221107904 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 60535 50225 162 162 0 60373 0
[pid=7890] vsize: 242140
Current children cumulated CPU time (s) 467.52
Current children cumulated vsize (Kb) 244268

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 70513 0 0 0 47407 259 0 0 25 0 1 0 1796996127 234995712 55778 4294967295 134512640 135167914 3221224448 3221110896 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 57372 55778 162 162 0 57210 0
[pid=7890] vsize: 229488
Current children cumulated CPU time (s) 477.39
Current children cumulated vsize (Kb) 231616

[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 73866 0 0 0 48370 275 0 0 25 0 1 0 1796996127 248729600 59131 4294967295 134512640 135167914 3221224448 3221105824 134695581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 60725 59131 162 162 0 60563 0
[pid=7890] vsize: 242900
Current children cumulated CPU time (s) 487.18
Current children cumulated vsize (Kb) 245028

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 77205 0 0 0 49335 290 0 0 25 0 1 0 1796996127 262406144 62470 4294967295 134512640 135167914 3221224448 3221111324 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 64064 62470 162 162 0 63902 0
[pid=7890] vsize: 256256
Current children cumulated CPU time (s) 496.98
Current children cumulated vsize (Kb) 258384

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.82 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 80341 0 0 0 50302 303 0 0 25 0 1 0 1796996127 275251200 65606 4294967295 134512640 135167914 3221224448 3221105756 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 67200 65606 162 162 0 67038 0
[pid=7890] vsize: 268800
Current children cumulated CPU time (s) 506.78
Current children cumulated vsize (Kb) 270928

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 83851 0 0 0 51265 319 0 0 25 0 1 0 1796996127 289628160 69116 4294967295 134512640 135167914 3221224448 3221108384 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 70710 69116 162 162 0 70548 0
[pid=7890] vsize: 282840
Current children cumulated CPU time (s) 516.57
Current children cumulated vsize (Kb) 284968

[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 87190 0 0 0 52227 334 0 0 25 0 1 0 1796996127 303304704 72455 4294967295 134512640 135167914 3221224448 3221105756 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 74049 72455 162 162 0 73887 0
[pid=7890] vsize: 296196
Current children cumulated CPU time (s) 526.34
Current children cumulated vsize (Kb) 298324

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 90340 0 0 0 53194 347 0 0 25 0 1 0 1796996127 316207104 75605 4294967295 134512640 135167914 3221224448 3221106048 134695619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 77199 75605 162 162 0 77037 0
[pid=7890] vsize: 308796
Current children cumulated CPU time (s) 536.14
Current children cumulated vsize (Kb) 310924

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 93648 0 0 0 54162 360 0 0 25 0 1 0 1796996127 329756672 78913 4294967295 134512640 135167914 3221224448 3221106460 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 80507 78913 162 162 0 80345 0
[pid=7890] vsize: 322028
Current children cumulated CPU time (s) 545.95
Current children cumulated vsize (Kb) 324156

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 96788 0 0 0 55129 374 0 0 25 0 1 0 1796996127 342618112 82053 4294967295 134512640 135167914 3221224448 3221105980 134722208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 83647 82053 162 162 0 83485 0
[pid=7890] vsize: 334588
Current children cumulated CPU time (s) 555.76
Current children cumulated vsize (Kb) 336716

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 100102 0 0 0 56092 389 0 0 25 0 1 0 1796996127 356192256 85367 4294967295 134512640 135167914 3221224448 3221106284 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 86961 85367 162 162 0 86799 0
[pid=7890] vsize: 347844
Current children cumulated CPU time (s) 565.54
Current children cumulated vsize (Kb) 349972

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 121786 0 0 0 57033 443 0 0 25 0 1 0 1796996127 401813504 96505 4294967295 134512640 135167914 3221224448 3221106224 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 98099 96505 162 162 0 97937 0
[pid=7890] vsize: 392396
Current children cumulated CPU time (s) 575.49
Current children cumulated vsize (Kb) 394524

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 124962 0 0 0 58000 458 0 0 25 0 1 0 1796996127 414822400 99681 4294967295 134512640 135167914 3221224448 3221106336 134620458 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 101275 99681 162 162 0 101113 0
[pid=7890] vsize: 405100
Current children cumulated CPU time (s) 585.31
Current children cumulated vsize (Kb) 407228

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 128415 0 0 0 58961 473 0 0 25 0 1 0 1796996127 428965888 103134 4294967295 134512640 135167914 3221224448 3221107328 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 104728 103134 162 162 0 104566 0
[pid=7890] vsize: 418912
Current children cumulated CPU time (s) 595.07
Current children cumulated vsize (Kb) 421040

[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 131584 0 0 0 59926 487 0 0 25 0 1 0 1796996127 441946112 106303 4294967295 134512640 135167914 3221224448 3221110432 134844650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 107897 106303 162 162 0 107735 0
[pid=7890] vsize: 431588
Current children cumulated CPU time (s) 604.86
Current children cumulated vsize (Kb) 433716

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 134687 0 0 0 60890 503 0 0 25 0 1 0 1796996127 454656000 109406 4294967295 134512640 135167914 3221224448 3221107136 134624796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 111000 109406 162 162 0 110838 0
[pid=7890] vsize: 444000
Current children cumulated CPU time (s) 614.66
Current children cumulated vsize (Kb) 446128

[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 137706 0 0 0 61858 513 0 0 25 0 1 0 1796996127 467021824 112425 4294967295 134512640 135167914 3221224448 3221106336 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 114019 112425 162 162 0 113857 0
[pid=7890] vsize: 456076
Current children cumulated CPU time (s) 624.44
Current children cumulated vsize (Kb) 458204

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 140986 0 0 0 62824 529 0 0 25 0 1 0 1796996127 480456704 115705 4294967295 134512640 135167914 3221224448 3221106876 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 117299 115705 162 162 0 117137 0
[pid=7890] vsize: 469196
Current children cumulated CPU time (s) 634.26
Current children cumulated vsize (Kb) 471324

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 143981 0 0 0 63791 543 0 0 25 0 1 0 1796996127 492724224 118700 4294967295 134512640 135167914 3221224448 3221109888 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 120294 118700 162 162 0 120132 0
[pid=7890] vsize: 481176
Current children cumulated CPU time (s) 644.07
Current children cumulated vsize (Kb) 483304

[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.83 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 147020 0 0 0 64756 555 0 0 25 0 1 0 1796996127 505171968 121739 4294967295 134512640 135167914 3221224448 3221106620 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 123333 121739 162 162 0 123171 0
[pid=7890] vsize: 493332
Current children cumulated CPU time (s) 653.84
Current children cumulated vsize (Kb) 495460

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 150031 0 0 0 65727 567 0 0 25 0 1 0 1796996127 517505024 124750 4294967295 134512640 135167914 3221224448 3221106048 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 126344 124750 162 162 0 126182 0
[pid=7890] vsize: 505376
Current children cumulated CPU time (s) 663.67
Current children cumulated vsize (Kb) 507504

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 153393 0 0 0 66693 582 0 0 25 0 1 0 1796996127 531275776 128112 4294967295 134512640 135167914 3221224448 3221108188 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 129706 128112 162 162 0 129544 0
[pid=7890] vsize: 518824
Current children cumulated CPU time (s) 673.48
Current children cumulated vsize (Kb) 520952

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 156425 0 0 0 67660 596 0 0 25 0 1 0 1796996127 543694848 131144 4294967295 134512640 135167914 3221224448 3221107296 134849230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 132738 131144 162 162 0 132576 0
[pid=7890] vsize: 530952
Current children cumulated CPU time (s) 683.29
Current children cumulated vsize (Kb) 533080

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 159229 0 0 0 68629 609 0 0 25 0 1 0 1796996127 555180032 133948 4294967295 134512640 135167914 3221224448 3221105404 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 135542 133948 162 162 0 135380 0
[pid=7890] vsize: 542168
Current children cumulated CPU time (s) 693.11
Current children cumulated vsize (Kb) 544296

[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.84 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 162027 0 0 0 69599 621 0 0 25 0 1 0 1796996127 566640640 136746 4294967295 134512640 135167914 3221224448 3221108412 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 138340 136746 162 162 0 138178 0
[pid=7890] vsize: 553360
Current children cumulated CPU time (s) 702.93
Current children cumulated vsize (Kb) 555488

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 164862 0 0 0 70570 632 0 0 25 0 1 0 1796996127 578252800 139581 4294967295 134512640 135167914 3221224448 3221106748 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 141175 139581 162 162 0 141013 0
[pid=7890] vsize: 564700
Current children cumulated CPU time (s) 712.75
Current children cumulated vsize (Kb) 566828

[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 167583 0 0 0 71540 644 0 0 25 0 1 0 1796996127 589398016 142302 4294967295 134512640 135167914 3221224448 3221106592 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 143896 142302 162 162 0 143734 0
[pid=7890] vsize: 575584
Current children cumulated CPU time (s) 722.57
Current children cumulated vsize (Kb) 577712

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 170357 0 0 0 72509 657 0 0 25 0 1 0 1796996127 600760320 145076 4294967295 134512640 135167914 3221224448 3221105856 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 146670 145076 162 162 0 146508 0
[pid=7890] vsize: 586680
Current children cumulated CPU time (s) 732.39
Current children cumulated vsize (Kb) 588808

[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 172988 0 0 0 73479 669 0 0 25 0 1 0 1796996127 611536896 147707 4294967295 134512640 135167914 3221224448 3221106044 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 149301 147707 162 162 0 149139 0
[pid=7890] vsize: 597204
Current children cumulated CPU time (s) 742.21
Current children cumulated vsize (Kb) 599332

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 175725 0 0 0 74448 684 0 0 25 0 1 0 1796996127 622747648 150444 4294967295 134512640 135167914 3221224448 3221109356 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 152038 150444 162 162 0 151876 0
[pid=7890] vsize: 608152
Current children cumulated CPU time (s) 752.05
Current children cumulated vsize (Kb) 610280

[startup+770.056 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 178522 0 0 0 75418 696 0 0 25 0 1 0 1796996127 634204160 153241 4294967295 134512640 135167914 3221224448 3221107380 134697377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 154835 153241 162 162 0 154673 0
[pid=7890] vsize: 619340
Current children cumulated CPU time (s) 761.87
Current children cumulated vsize (Kb) 621468

[startup+780.057 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 181284 0 0 0 76392 706 0 0 25 0 1 0 1796996127 645517312 156003 4294967295 134512640 135167914 3221224448 3221106292 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 157597 156003 162 162 0 157435 0
[pid=7890] vsize: 630388
Current children cumulated CPU time (s) 771.71
Current children cumulated vsize (Kb) 632516

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 184586 0 0 0 77357 720 0 0 25 0 1 0 1796996127 659042304 159305 4294967295 134512640 135167914 3221224448 3221105632 134694435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 160899 159305 162 162 0 160737 0
[pid=7890] vsize: 643596
Current children cumulated CPU time (s) 781.5
Current children cumulated vsize (Kb) 645724

[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 227065 0 0 0 78254 822 0 0 25 0 1 0 1796996127 833036288 201784 4294967295 134512640 135167914 3221224448 3221106960 134694428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 203378 201784 162 162 0 203216 0
[pid=7890] vsize: 813512
Current children cumulated CPU time (s) 791.49
Current children cumulated vsize (Kb) 815640

[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 228140 0 0 0 79238 832 0 0 25 0 1 0 1796996127 751050752 181768 4294967295 134512640 135167914 3221224448 3221105972 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 183362 181768 162 162 0 183200 0
[pid=7890] vsize: 733448
Current children cumulated CPU time (s) 801.43
Current children cumulated vsize (Kb) 735576

[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.85 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 231621 0 0 0 80201 848 0 0 25 0 1 0 1796996127 765308928 185249 4294967295 134512640 135167914 3221224448 3221105692 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 186843 185249 162 162 0 186681 0
[pid=7890] vsize: 747372
Current children cumulated CPU time (s) 811.22
Current children cumulated vsize (Kb) 749500

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 234882 0 0 0 81168 862 0 0 25 0 1 0 1796996127 778665984 188510 4294967295 134512640 135167914 3221224448 3221108128 134847340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 190104 188510 162 162 0 189942 0
[pid=7890] vsize: 760416
Current children cumulated CPU time (s) 821.03
Current children cumulated vsize (Kb) 762544

[startup+840.061 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 237580 0 0 0 82143 872 0 0 25 0 1 0 1796996127 789716992 191208 4294967295 134512640 135167914 3221224448 3221107580 134722576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 192802 191208 162 162 0 192640 0
[pid=7890] vsize: 771208
Current children cumulated CPU time (s) 830.88
Current children cumulated vsize (Kb) 773336

[startup+850.062 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 240202 0 0 0 83113 884 0 0 25 0 1 0 1796996127 800456704 193830 4294967295 134512640 135167914 3221224448 3221106576 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 195424 193830 162 162 0 195262 0
[pid=7890] vsize: 781696
Current children cumulated CPU time (s) 840.7
Current children cumulated vsize (Kb) 783824

[startup+860.063 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 243139 0 0 0 84082 897 0 0 25 0 1 0 1796996127 812486656 196767 4294967295 134512640 135167914 3221224448 3221105308 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 198361 196767 162 162 0 198199 0
[pid=7890] vsize: 793444
Current children cumulated CPU time (s) 850.52
Current children cumulated vsize (Kb) 795572

[startup+870.064 s]
Raw data (loadavg): 0.99 0.97 0.85 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 246837 0 0 0 85040 915 0 0 25 0 1 0 1796996127 827633664 200465 4294967295 134512640 135167914 3221224448 3221105596 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 202059 200465 162 162 0 201897 0
[pid=7890] vsize: 808236
Current children cumulated CPU time (s) 860.28
Current children cumulated vsize (Kb) 810364

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 250304 0 0 0 86004 929 0 0 25 0 1 0 1796996127 841834496 203932 4294967295 134512640 135167914 3221224448 3221105868 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 205526 203932 162 162 0 205364 0
[pid=7890] vsize: 822104
Current children cumulated CPU time (s) 870.06
Current children cumulated vsize (Kb) 824232

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 254105 0 0 0 86965 947 0 0 25 0 1 0 1796996127 857403392 207733 4294967295 134512640 135167914 3221224448 3221107360 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 209327 207733 162 162 0 209165 0
[pid=7890] vsize: 837308
Current children cumulated CPU time (s) 879.85
Current children cumulated vsize (Kb) 839436

[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 257617 0 0 0 87929 962 0 0 25 0 1 0 1796996127 871788544 211245 4294967295 134512640 135167914 3221224448 3221107264 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7890/statm): 212839 211245 162 162 0 212677 0
[pid=7890] vsize: 851356
Current children cumulated CPU time (s) 889.64
Current children cumulated vsize (Kb) 853484

[startup+910.068 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 260955 0 0 0 88891 978 0 0 25 0 1 0 1796996127 885460992 214583 4294967295 134512640 135167914 3221224448 3221108192 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 216177 214583 162 162 0 216015 0
[pid=7890] vsize: 864708
Current children cumulated CPU time (s) 899.42
Current children cumulated vsize (Kb) 866836

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 264299 0 0 0 89854 994 0 0 25 0 1 0 1796996127 899158016 217927 4294967295 134512640 135167914 3221224448 3221106368 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 219521 217927 162 162 0 219359 0
[pid=7890] vsize: 878084
Current children cumulated CPU time (s) 909.21
Current children cumulated vsize (Kb) 880212

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 268019 0 0 0 90813 1010 0 0 25 0 1 0 1796996127 914395136 221647 4294967295 134512640 135167914 3221224448 3221108016 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 223241 221647 162 162 0 223079 0
[pid=7890] vsize: 892964
Current children cumulated CPU time (s) 918.96
Current children cumulated vsize (Kb) 895092

[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) R 7885 7885 6872 0 -1 0 271652 0 0 0 91773 1026 0 0 25 0 1 0 1796996127 929275904 225280 4294967295 134512640 135167914 3221224448 3221105568 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7890/statm): 226874 225280 162 162 0 226712 0
[pid=7890] vsize: 907496
Current children cumulated CPU time (s) 928.72
Current children cumulated vsize (Kb) 909624



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+948.622 s]
Raw data (loadavg): 0.99 0.97 0.86 1/57 7890
Raw data (/proc/7885/stat): 7885 (minisat+_script) S 7884 7885 6872 0 -1 0 314 2384 0 0 0 1 60 12 18 0 1 0 1796996042 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7885/statm): 532 234 485 147 0 385 0
[pid=7885] vsize: 2128
Raw data (/proc/7890/stat): 7890 (minisat+_bignum) T 7885 7885 6872 0 -1 0 274649 0 2 0 92589 1040 0 0 25 0 1 0 1796996127 941543424 228150 4294967295 134512640 135167914 3221224448 3221105852 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7890/statm): 229869 228150 162 162 0 229707 0
[pid=7890] vsize: 919476
Current children cumulated CPU time (s) 937.02
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 949.048
CPU time (s): 936.731
CPU user time (s): 925.898
CPU system time (s): 10.8324
CPU usage (%): 98.7021
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !