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/miplib3/normalized-mps-v2-13-7-misc06.opb
MD5SUMa9bcf0b6d0323d251b7b3500c52602fc
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 6211

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        853472 kB
Buffers:         26508 kB
Cached:         121552 kB
SwapCached:        860 kB
Active:          41336 kB
Inactive:       109332 kB
HighTotal:      131008 kB
HighFree:        23996 kB
LowTotal:       903652 kB
LowFree:        829476 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5772 kB
Slab:            24972 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:45:10 (client local time) WITH STATUS 0 IN 933.876 SECONDS
stats: 3371 7 933.876 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/28232/stat): 28232 (minisat+_script) R 28231 28232 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855629576 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/28232/statm): 174 3 169 147 0 27 0
[pid=28232] 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=28233
New process pid=28234
New process pid=28235
execve syscall for /bin/sed executable
One traced child (pid=28234) 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=28235) exited with status: 0
One traced child (pid=28233) exited with status: 0
New process pid=28236
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-misc06.opb
One traced child (pid=28236) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=28237
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-misc06.opb

[startup+10.0044 s]
Raw data (loadavg): 0.87 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 3670 0 0 0 874 21 0 0 25 0 1 0 1855629660 15233024 3130 4294967295 134512640 135167914 3221224448 3221222784 134694386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28237/statm): 3719 3130 162 162 0 3557 0
[pid=28237] vsize: 14876
Current children cumulated CPU time (s) 9.67
Current children cumulated vsize (Kb) 17004

[startup+20.0053 s]
Raw data (loadavg): 0.89 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4138 0 0 0 1870 23 0 0 25 0 1 0 1855629660 16039936 3347 4294967295 134512640 135167914 3221224448 3221221264 134694545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 3916 3347 162 162 0 3754 0
[pid=28237] vsize: 15664
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 17792

[startup+30.0062 s]
Raw data (loadavg): 0.91 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4138 0 0 0 2870 23 0 0 25 0 1 0 1855629660 16039936 3347 4294967295 134512640 135167914 3221224448 3221220464 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 3916 3347 162 162 0 3754 0
[pid=28237] vsize: 15664
Current children cumulated CPU time (s) 29.65
Current children cumulated vsize (Kb) 17792

[startup+40.0071 s]
Raw data (loadavg): 0.92 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4138 0 0 0 3870 23 0 0 25 0 1 0 1855629660 16039936 3347 4294967295 134512640 135167914 3221224448 3221221396 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 3916 3347 162 162 0 3754 0
[pid=28237] vsize: 15664
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 17792

[startup+50.0081 s]
Raw data (loadavg): 0.93 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4198 0 0 0 4870 23 0 0 25 0 1 0 1855629660 16433152 3407 4294967295 134512640 135167914 3221224448 3221222088 134693621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 4012 3407 162 162 0 3850 0
[pid=28237] vsize: 16048
Current children cumulated CPU time (s) 49.65
Current children cumulated vsize (Kb) 18176

[startup+60.009 s]
Raw data (loadavg): 0.94 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4291 0 0 0 5870 24 0 0 25 0 1 0 1855629660 16773120 3500 4294967295 134512640 135167914 3221224448 3221220700 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 4095 3500 162 162 0 3933 0
[pid=28237] vsize: 16380
Current children cumulated CPU time (s) 59.66
Current children cumulated vsize (Kb) 18508

[startup+70.0099 s]
Raw data (loadavg): 0.95 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4298 0 0 0 6870 24 0 0 25 0 1 0 1855629660 16773120 3507 4294967295 134512640 135167914 3221224448 3221221200 134843012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 4095 3507 162 162 0 3933 0
[pid=28237] vsize: 16380
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 18508

[startup+80.0118 s]
Raw data (loadavg): 0.96 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4332 0 0 0 7870 24 0 0 25 0 1 0 1855629660 17166336 3541 4294967295 134512640 135167914 3221224448 3221221904 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 4191 3541 162 162 0 4029 0
[pid=28237] vsize: 16764
Current children cumulated CPU time (s) 79.66
Current children cumulated vsize (Kb) 18892

[startup+90.0128 s]
Raw data (loadavg): 0.96 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4561 0 0 0 8869 25 0 0 25 0 1 0 1855629660 17608704 3687 4294967295 134512640 135167914 3221224448 3221220864 134696248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 4299 3687 162 162 0 4137 0
[pid=28237] vsize: 17196
Current children cumulated CPU time (s) 89.66
Current children cumulated vsize (Kb) 19324

[startup+100.013 s]
Raw data (loadavg): 0.97 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 4721 0 0 0 9868 25 0 0 25 0 1 0 1855629660 18808832 3847 4294967295 134512640 135167914 3221224448 3221221420 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 4592 3847 162 162 0 4430 0
[pid=28237] vsize: 18368
Current children cumulated CPU time (s) 99.65
Current children cumulated vsize (Kb) 20496

[startup+110.014 s]
Raw data (loadavg): 0.97 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 5321 0 0 0 10865 27 0 0 25 0 1 0 1855629660 20189184 4282 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28237/statm): 4929 4282 162 162 0 4767 0
[pid=28237] vsize: 19716
Current children cumulated CPU time (s) 109.64
Current children cumulated vsize (Kb) 21844

[startup+120.015 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 5606 0 0 0 11862 29 0 0 25 0 1 0 1855629660 22503424 4567 4294967295 134512640 135167914 3221224448 3221221792 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 5494 4567 162 162 0 5332 0
[pid=28237] vsize: 21976
Current children cumulated CPU time (s) 119.63
Current children cumulated vsize (Kb) 24104

[startup+130.015 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 5816 0 0 0 12860 30 0 0 25 0 1 0 1855629660 23060480 4777 4294967295 134512640 135167914 3221224448 3221222576 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 5630 4777 162 162 0 5468 0
[pid=28237] vsize: 22520
Current children cumulated CPU time (s) 129.62
Current children cumulated vsize (Kb) 24648

[startup+140.016 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 6649 0 0 0 13857 32 0 0 25 0 1 0 1855629660 24854528 5280 4294967295 134512640 135167914 3221224448 3221222140 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 6068 5280 162 162 0 5906 0
[pid=28237] vsize: 24272
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 26400

[startup+150.016 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 6846 0 0 0 14856 33 0 0 25 0 1 0 1855629660 25358336 5477 4294967295 134512640 135167914 3221224448 3221222176 134629172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 6191 5477 162 162 0 6029 0
[pid=28237] vsize: 24764
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 26892

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 7040 0 0 0 15855 34 0 0 25 0 1 0 1855629660 25870336 5671 4294967295 134512640 135167914 3221224448 3221222360 134629265 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 6316 5671 162 162 0 6154 0
[pid=28237] vsize: 25264
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 27392

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 7183 0 0 0 16854 35 0 0 25 0 1 0 1855629660 26357760 5814 4294967295 134512640 135167914 3221224448 3221220912 134694504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 6435 5814 162 162 0 6273 0
[pid=28237] vsize: 25740
Current children cumulated CPU time (s) 169.61
Current children cumulated vsize (Kb) 27868

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 7419 0 0 0 17853 35 0 0 25 0 1 0 1855629660 26812416 5966 4294967295 134512640 135167914 3221224448 3221222352 134628657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 6546 5966 162 162 0 6384 0
[pid=28237] vsize: 26184
Current children cumulated CPU time (s) 179.6
Current children cumulated vsize (Kb) 28312

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 7540 0 0 0 18852 37 0 0 25 0 1 0 1855629660 30109696 6045 4294967295 134512640 135167914 3221224448 3221220672 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 7351 6045 162 162 0 7189 0
[pid=28237] vsize: 29404
Current children cumulated CPU time (s) 189.61
Current children cumulated vsize (Kb) 31532

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 7574 0 0 0 19852 37 0 0 25 0 1 0 1855629660 30187520 6079 4294967295 134512640 135167914 3221224448 3221220876 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 7370 6079 162 162 0 7208 0
[pid=28237] vsize: 29480
Current children cumulated CPU time (s) 199.61
Current children cumulated vsize (Kb) 31608

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 7814 0 0 0 20851 38 0 0 25 0 1 0 1855629660 30654464 6235 4294967295 134512640 135167914 3221224448 3221221648 134629123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 7484 6235 162 162 0 7322 0
[pid=28237] vsize: 29936
Current children cumulated CPU time (s) 209.61
Current children cumulated vsize (Kb) 32064

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 7938 0 0 0 21850 38 0 0 25 0 1 0 1855629660 30810112 6317 4294967295 134512640 135167914 3221224448 3221220340 134723216 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 7522 6317 162 162 0 7360 0
[pid=28237] vsize: 30088
Current children cumulated CPU time (s) 219.6
Current children cumulated vsize (Kb) 32216

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 8105 0 0 0 22849 39 0 0 25 0 1 0 1855629660 31182848 6442 4294967295 134512640 135167914 3221224448 3221221616 134694489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 7613 6442 162 162 0 7451 0
[pid=28237] vsize: 30452
Current children cumulated CPU time (s) 229.6
Current children cumulated vsize (Kb) 32580

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 8202 0 0 0 23849 39 0 0 25 0 1 0 1855629660 31322112 6497 4294967295 134512640 135167914 3221224448 3221220864 134696613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 7647 6497 162 162 0 7485 0
[pid=28237] vsize: 30588
Current children cumulated CPU time (s) 239.6
Current children cumulated vsize (Kb) 32716

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 9662 0 0 0 24845 43 0 0 25 0 1 0 1855629660 34250752 7256 4294967295 134512640 135167914 3221224448 3221221780 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8362 7256 162 162 0 8200 0
[pid=28237] vsize: 33448
Current children cumulated CPU time (s) 249.6
Current children cumulated vsize (Kb) 35576

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 9876 0 0 0 25844 44 0 0 25 0 1 0 1855629660 34619392 7386 4294967295 134512640 135167914 3221224448 3221221376 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8452 7386 162 162 0 8290 0
[pid=28237] vsize: 33808
Current children cumulated CPU time (s) 259.6
Current children cumulated vsize (Kb) 35936

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 9979 0 0 0 26843 44 0 0 25 0 1 0 1855629660 34779136 7447 4294967295 134512640 135167914 3221224448 3221220880 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8491 7447 162 162 0 8329 0
[pid=28237] vsize: 33964
Current children cumulated CPU time (s) 269.59
Current children cumulated vsize (Kb) 36092

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 10079 0 0 0 27843 45 0 0 25 0 1 0 1855629660 35000320 7547 4294967295 134512640 135167914 3221224448 3221220892 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8545 7547 162 162 0 8383 0
[pid=28237] vsize: 34180
Current children cumulated CPU time (s) 279.6
Current children cumulated vsize (Kb) 36308

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 10286 0 0 0 28842 45 0 0 25 0 1 0 1855629660 35344384 7670 4294967295 134512640 135167914 3221224448 3221220700 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8629 7670 162 162 0 8467 0
[pid=28237] vsize: 34516
Current children cumulated CPU time (s) 289.59
Current children cumulated vsize (Kb) 36644

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 10405 0 0 0 29842 46 0 0 25 0 1 0 1855629660 35500032 7747 4294967295 134512640 135167914 3221224448 3221173488 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8667 7747 162 162 0 8505 0
[pid=28237] vsize: 34668
Current children cumulated CPU time (s) 299.6
Current children cumulated vsize (Kb) 36796

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 10467 0 0 0 30841 46 0 0 25 0 1 0 1855629660 35643392 7809 4294967295 134512640 135167914 3221224448 3221220924 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8702 7809 162 162 0 8540 0
[pid=28237] vsize: 34808
Current children cumulated CPU time (s) 309.59
Current children cumulated vsize (Kb) 36936

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 10642 0 0 0 31840 47 0 0 25 0 1 0 1855629660 36048896 7942 4294967295 134512640 135167914 3221224448 3221221104 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8801 7942 162 162 0 8639 0
[pid=28237] vsize: 35204
Current children cumulated CPU time (s) 319.59
Current children cumulated vsize (Kb) 37332

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 10842 0 0 0 32840 47 0 0 25 0 1 0 1855629660 36347904 8058 4294967295 134512640 135167914 3221224448 3221220492 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8874 8058 162 162 0 8712 0
[pid=28237] vsize: 35496
Current children cumulated CPU time (s) 329.59
Current children cumulated vsize (Kb) 37624

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 10920 0 0 0 33840 47 0 0 25 0 1 0 1855629660 36532224 8136 4294967295 134512640 135167914 3221224448 3221221264 134694428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8919 8136 162 162 0 8757 0
[pid=28237] vsize: 35676
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 37804

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 11117 0 0 0 34840 48 0 0 25 0 1 0 1855629660 36835328 8249 4294967295 134512640 135167914 3221224448 3221220872 134723211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 8993 8249 162 162 0 8831 0
[pid=28237] vsize: 35972
Current children cumulated CPU time (s) 349.6
Current children cumulated vsize (Kb) 38100

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 11531 0 0 0 35837 50 0 0 25 0 1 0 1855629660 37740544 8621 4294967295 134512640 135167914 3221224448 3221221812 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 9214 8621 162 162 0 9052 0
[pid=28237] vsize: 36856
Current children cumulated CPU time (s) 359.59
Current children cumulated vsize (Kb) 38984

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 12456 0 0 0 36828 54 0 0 25 0 1 0 1855629660 46424064 9546 4294967295 134512640 135167914 3221224448 3221221712 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 11334 9546 162 162 0 11172 0
[pid=28237] vsize: 45336
Current children cumulated CPU time (s) 369.54
Current children cumulated vsize (Kb) 47464

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 18966 0 0 0 37794 72 0 0 25 0 1 0 1855629660 64356352 14118 4294967295 134512640 135167914 3221224448 3221105468 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 15712 14118 162 162 0 15550 0
[pid=28237] vsize: 62848
Current children cumulated CPU time (s) 379.38
Current children cumulated vsize (Kb) 64976

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 23789 0 0 0 38752 93 0 0 25 0 1 0 1855629660 81412096 18282 4294967295 134512640 135167914 3221224448 3221105180 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 19876 18282 162 162 0 19714 0
[pid=28237] vsize: 79504
Current children cumulated CPU time (s) 389.17
Current children cumulated vsize (Kb) 81632

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 29454 0 0 0 39713 113 0 0 25 0 1 0 1855629660 99217408 22629 4294967295 134512640 135167914 3221224448 3221106312 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28237/statm): 24223 22629 162 162 0 24061 0
[pid=28237] vsize: 96892
Current children cumulated CPU time (s) 398.98
Current children cumulated vsize (Kb) 99020

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 33168 0 0 0 40673 129 0 0 25 0 1 0 1855629660 114429952 26343 4294967295 134512640 135167914 3221224448 3221106216 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 27937 26343 162 162 0 27775 0
[pid=28237] vsize: 111748
Current children cumulated CPU time (s) 408.74
Current children cumulated vsize (Kb) 113876

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 36392 0 0 0 41641 142 0 0 25 0 1 0 1855629660 127635456 29567 4294967295 134512640 135167914 3221224448 3221107228 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 31161 29567 162 162 0 30999 0
[pid=28237] vsize: 124644
Current children cumulated CPU time (s) 418.55
Current children cumulated vsize (Kb) 126772

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 44621 0 0 0 42594 169 0 0 25 0 1 0 1855629660 150540288 35159 4294967295 134512640 135167914 3221224448 3221105244 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 36753 35159 162 162 0 36591 0
[pid=28237] vsize: 147012
Current children cumulated CPU time (s) 428.35
Current children cumulated vsize (Kb) 149140

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 48127 0 0 0 43557 185 0 0 25 0 1 0 1855629660 164900864 38665 4294967295 134512640 135167914 3221224448 3221105468 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 40259 38665 162 162 0 40097 0
[pid=28237] vsize: 161036
Current children cumulated CPU time (s) 438.14
Current children cumulated vsize (Kb) 163164

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 51426 0 0 0 44519 199 0 0 25 0 1 0 1855629660 178413568 41964 4294967295 134512640 135167914 3221224448 3221105724 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 43558 41964 162 162 0 43396 0
[pid=28237] vsize: 174232
Current children cumulated CPU time (s) 447.9
Current children cumulated vsize (Kb) 176360

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 54588 0 0 0 45486 212 0 0 25 0 1 0 1855629660 191365120 45126 4294967295 134512640 135167914 3221224448 3221107092 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 46720 45126 162 162 0 46558 0
[pid=28237] vsize: 186880
Current children cumulated CPU time (s) 457.7
Current children cumulated vsize (Kb) 189008

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 68403 0 0 0 46429 248 0 0 25 0 1 0 1855629660 247951360 58941 4294967295 134512640 135167914 3221224448 3221107856 134694428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 60535 58941 162 162 0 60373 0
[pid=28237] vsize: 242140
Current children cumulated CPU time (s) 467.49
Current children cumulated vsize (Kb) 244268

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 70783 0 0 0 47401 261 0 0 25 0 1 0 1855629660 236101632 56048 4294967295 134512640 135167914 3221224448 3221108128 134847373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 57642 56048 162 162 0 57480 0
[pid=28237] vsize: 230568
Current children cumulated CPU time (s) 477.34
Current children cumulated vsize (Kb) 232696

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 74100 0 0 0 48366 275 0 0 25 0 1 0 1855629660 249688064 59365 4294967295 134512640 135167914 3221224448 3221109424 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 60959 59365 162 162 0 60797 0
[pid=28237] vsize: 243836
Current children cumulated CPU time (s) 487.13
Current children cumulated vsize (Kb) 245964

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 77431 0 0 0 49330 290 0 0 25 0 1 0 1855629660 263331840 62696 4294967295 134512640 135167914 3221224448 3221106080 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 64290 62696 162 162 0 64128 0
[pid=28237] vsize: 257160
Current children cumulated CPU time (s) 496.92
Current children cumulated vsize (Kb) 259288

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 80623 0 0 0 50298 304 0 0 25 0 1 0 1855629660 276406272 65888 4294967295 134512640 135167914 3221224448 3221105468 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 67482 65888 162 162 0 67320 0
[pid=28237] vsize: 269928
Current children cumulated CPU time (s) 506.74
Current children cumulated vsize (Kb) 272056

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 84055 0 0 0 51262 320 0 0 25 0 1 0 1855629660 290463744 69320 4294967295 134512640 135167914 3221224448 3221106044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 70914 69320 162 162 0 70752 0
[pid=28237] vsize: 283656
Current children cumulated CPU time (s) 516.54
Current children cumulated vsize (Kb) 285784

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 87441 0 0 0 52227 333 0 0 25 0 1 0 1855629660 304332800 72706 4294967295 134512640 135167914 3221224448 3221105916 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 74300 72706 162 162 0 74138 0
[pid=28237] vsize: 297200
Current children cumulated CPU time (s) 526.32
Current children cumulated vsize (Kb) 299328

[startup+540.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 90628 0 0 0 53192 348 0 0 25 0 1 0 1855629660 317386752 75893 4294967295 134512640 135167914 3221224448 3221108544 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 77487 75893 162 162 0 77325 0
[pid=28237] vsize: 309948
Current children cumulated CPU time (s) 536.12
Current children cumulated vsize (Kb) 312076

[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 93933 0 0 0 54156 362 0 0 25 0 1 0 1855629660 330924032 79198 4294967295 134512640 135167914 3221224448 3221105244 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 80792 79198 162 162 0 80630 0
[pid=28237] vsize: 323168
Current children cumulated CPU time (s) 545.9
Current children cumulated vsize (Kb) 325296

[startup+560.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 97193 0 0 0 55122 377 0 0 25 0 1 0 1855629660 344276992 82458 4294967295 134512640 135167914 3221224448 3221106416 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 84052 82458 162 162 0 83890 0
[pid=28237] vsize: 336208
Current children cumulated CPU time (s) 555.71
Current children cumulated vsize (Kb) 338336

[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 121290 0 0 0 56044 439 0 0 25 0 1 0 1855629660 442978304 106555 4294967295 134512640 135167914 3221224448 3221107232 134625423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 108149 106555 162 162 0 107987 0
[pid=28237] vsize: 432596
Current children cumulated CPU time (s) 565.55
Current children cumulated vsize (Kb) 434724

[startup+580.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 122255 0 0 0 57032 445 0 0 25 0 1 0 1855629660 403734528 96974 4294967295 134512640 135167914 3221224448 3221106544 134694338 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 98568 96974 162 162 0 98406 0
[pid=28237] vsize: 394272
Current children cumulated CPU time (s) 575.49
Current children cumulated vsize (Kb) 396400

[startup+590.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 125468 0 0 0 57996 460 0 0 25 0 1 0 1855629660 416894976 100187 4294967295 134512640 135167914 3221224448 3221110560 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 101781 100187 162 162 0 101619 0
[pid=28237] vsize: 407124
Current children cumulated CPU time (s) 585.28
Current children cumulated vsize (Kb) 409252

[startup+600.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 128846 0 0 0 58958 475 0 0 25 0 1 0 1855629660 430731264 103565 4294967295 134512640 135167914 3221224448 3221107180 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 105159 103565 162 162 0 104997 0
[pid=28237] vsize: 420636
Current children cumulated CPU time (s) 595.05
Current children cumulated vsize (Kb) 422764

[startup+610.051 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 132061 0 0 0 59923 490 0 0 25 0 1 0 1855629660 443904000 106780 4294967295 134512640 135167914 3221224448 3221105628 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 108375 106780 162 162 0 108213 0
[pid=28237] vsize: 433500
Current children cumulated CPU time (s) 604.85
Current children cumulated vsize (Kb) 435628

[startup+620.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 135174 0 0 0 60888 504 0 0 25 0 1 0 1855629660 456650752 109893 4294967295 134512640 135167914 3221224448 3221108232 134846924 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 111487 109893 162 162 0 111325 0
[pid=28237] vsize: 445948
Current children cumulated CPU time (s) 614.64
Current children cumulated vsize (Kb) 448076

[startup+630.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 138353 0 0 0 61855 517 0 0 25 0 1 0 1855629660 469671936 113072 4294967295 134512640 135167914 3221224448 3221106072 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 114666 113072 162 162 0 114504 0
[pid=28237] vsize: 458664
Current children cumulated CPU time (s) 624.44
Current children cumulated vsize (Kb) 460792

[startup+640.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 141471 0 0 0 62819 532 0 0 25 0 1 0 1855629660 482443264 116190 4294967295 134512640 135167914 3221224448 3221105916 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 117784 116190 162 162 0 117622 0
[pid=28237] vsize: 471136
Current children cumulated CPU time (s) 634.23
Current children cumulated vsize (Kb) 473264

[startup+650.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 144537 0 0 0 63786 546 0 0 25 0 1 0 1855629660 495001600 119256 4294967295 134512640 135167914 3221224448 3221110480 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 120850 119256 162 162 0 120688 0
[pid=28237] vsize: 483400
Current children cumulated CPU time (s) 644.04
Current children cumulated vsize (Kb) 485528

[startup+660.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 147588 0 0 0 64751 558 0 0 25 0 1 0 1855629660 507498496 122307 4294967295 134512640 135167914 3221224448 3221107232 134620920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 123901 122307 162 162 0 123739 0
[pid=28237] vsize: 495604
Current children cumulated CPU time (s) 653.81
Current children cumulated vsize (Kb) 497732

[startup+670.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 150707 0 0 0 65718 571 0 0 25 0 1 0 1855629660 520273920 125426 4294967295 134512640 135167914 3221224448 3221107104 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 127020 125426 162 162 0 126858 0
[pid=28237] vsize: 508080
Current children cumulated CPU time (s) 663.61
Current children cumulated vsize (Kb) 510208

[startup+680.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 153978 0 0 0 66681 588 0 0 25 0 1 0 1855629660 533671936 128697 4294967295 134512640 135167914 3221224448 3221106196 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 130291 128697 162 162 0 130129 0
[pid=28237] vsize: 521164
Current children cumulated CPU time (s) 673.41
Current children cumulated vsize (Kb) 523292

[startup+690.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 156983 0 0 0 67648 601 0 0 25 0 1 0 1855629660 545980416 131702 4294967295 134512640 135167914 3221224448 3221107328 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 133296 131702 162 162 0 133134 0
[pid=28237] vsize: 533184
Current children cumulated CPU time (s) 683.21
Current children cumulated vsize (Kb) 535312

[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 159794 0 0 0 68620 612 0 0 25 0 1 0 1855629660 557494272 134513 4294967295 134512640 135167914 3221224448 3221106800 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 136107 134513 162 162 0 135945 0
[pid=28237] vsize: 544428
Current children cumulated CPU time (s) 693.04
Current children cumulated vsize (Kb) 546556

[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 162590 0 0 0 69592 624 0 0 25 0 1 0 1855629660 568946688 137309 4294967295 134512640 135167914 3221224448 3221111744 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 138903 137309 162 162 0 138741 0
[pid=28237] vsize: 555612
Current children cumulated CPU time (s) 702.88
Current children cumulated vsize (Kb) 557740

[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 165420 0 0 0 70562 636 0 0 25 0 1 0 1855629660 580538368 140139 4294967295 134512640 135167914 3221224448 3221105500 134934490 0 0 5 16386 3222434789 0 0 17 0 0 0
Raw data (/proc/28237/statm): 141733 140139 162 162 0 141571 0
[pid=28237] vsize: 566932
Current children cumulated CPU time (s) 712.7
Current children cumulated vsize (Kb) 569060

[startup+730.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 168151 0 0 0 71533 647 0 0 25 0 1 0 1855629660 591724544 142870 4294967295 134512640 135167914 3221224448 3221106508 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 144464 142870 162 162 0 144302 0
[pid=28237] vsize: 577856
Current children cumulated CPU time (s) 722.52
Current children cumulated vsize (Kb) 579984

[startup+740.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 171012 0 0 0 72503 660 0 0 25 0 1 0 1855629660 603443200 145731 4294967295 134512640 135167914 3221224448 3221107872 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 147325 145731 162 162 0 147163 0
[pid=28237] vsize: 589300
Current children cumulated CPU time (s) 732.35
Current children cumulated vsize (Kb) 591428

[startup+750.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 173656 0 0 0 73478 671 0 0 25 0 1 0 1855629660 614273024 148375 4294967295 134512640 135167914 3221224448 3221106876 134722542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 149969 148375 162 162 0 149807 0
[pid=28237] vsize: 599876
Current children cumulated CPU time (s) 742.21
Current children cumulated vsize (Kb) 602004

[startup+760.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 176458 0 0 0 74446 683 0 0 25 0 1 0 1855629660 625750016 151177 4294967295 134512640 135167914 3221224448 3221106856 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 152771 151177 162 162 0 152609 0
[pid=28237] vsize: 611084
Current children cumulated CPU time (s) 752.01
Current children cumulated vsize (Kb) 613212

[startup+770.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 179227 0 0 0 75418 695 0 0 25 0 1 0 1855629660 637091840 153946 4294967295 134512640 135167914 3221224448 3221108192 134722521 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 155540 153946 162 162 0 155378 0
[pid=28237] vsize: 622160
Current children cumulated CPU time (s) 761.85
Current children cumulated vsize (Kb) 624288

[startup+780.063 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 181980 0 0 0 76388 708 0 0 25 0 1 0 1855629660 648368128 156699 4294967295 134512640 135167914 3221224448 3221108768 134694394 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 158293 156699 162 162 0 158131 0
[pid=28237] vsize: 633172
Current children cumulated CPU time (s) 771.68
Current children cumulated vsize (Kb) 635300

[startup+790.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 227065 0 0 0 77262 816 0 0 25 0 1 0 1855629660 833036288 201784 4294967295 134512640 135167914 3221224448 3221107008 134625423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 203378 201784 162 162 0 203216 0
[pid=28237] vsize: 813512
Current children cumulated CPU time (s) 781.5
Current children cumulated vsize (Kb) 815640

[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 227065 0 0 0 78262 816 0 0 25 0 1 0 1855629660 833036288 201784 4294967295 134512640 135167914 3221224448 3221106956 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 203378 201784 162 162 0 203216 0
[pid=28237] vsize: 813512
Current children cumulated CPU time (s) 791.5
Current children cumulated vsize (Kb) 815640

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 229110 0 0 0 79236 830 0 0 25 0 1 0 1855629660 755023872 182738 4294967295 134512640 135167914 3221224448 3221106548 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 184332 182738 162 162 0 184170 0
[pid=28237] vsize: 737328
Current children cumulated CPU time (s) 801.38
Current children cumulated vsize (Kb) 739456

[startup+820.065 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 232441 0 0 0 80203 846 0 0 25 0 1 0 1855629660 768667648 186069 4294967295 134512640 135167914 3221224448 3221111788 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 187663 186069 162 162 0 187501 0
[pid=28237] vsize: 750652
Current children cumulated CPU time (s) 811.21
Current children cumulated vsize (Kb) 752780

[startup+830.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 235662 0 0 0 81167 861 0 0 25 0 1 0 1855629660 781860864 189290 4294967295 134512640 135167914 3221224448 3221112732 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 190884 189290 162 162 0 190722 0
[pid=28237] vsize: 763536
Current children cumulated CPU time (s) 821
Current children cumulated vsize (Kb) 765664

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 238308 0 0 0 82139 874 0 0 25 0 1 0 1855629660 792698880 191936 4294967295 134512640 135167914 3221224448 3221106880 134849193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 193530 191936 162 162 0 193368 0
[pid=28237] vsize: 774120
Current children cumulated CPU time (s) 830.85
Current children cumulated vsize (Kb) 776248

[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 240875 0 0 0 83110 886 0 0 25 0 1 0 1855629660 803213312 194503 4294967295 134512640 135167914 3221224448 3221107312 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28237/statm): 196097 194503 162 162 0 195935 0
[pid=28237] vsize: 784388
Current children cumulated CPU time (s) 840.68
Current children cumulated vsize (Kb) 786516

[startup+860.067 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 244063 0 0 0 84075 902 0 0 25 0 1 0 1855629660 816271360 197691 4294967295 134512640 135167914 3221224448 3221109824 134624782 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 199285 197691 162 162 0 199123 0
[pid=28237] vsize: 797140
Current children cumulated CPU time (s) 850.49
Current children cumulated vsize (Kb) 799268

[startup+870.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 247671 0 0 0 85037 917 0 0 25 0 1 0 1855629660 831049728 201299 4294967295 134512640 135167914 3221224448 3221106080 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 202893 201299 162 162 0 202731 0
[pid=28237] vsize: 811572
Current children cumulated CPU time (s) 860.26
Current children cumulated vsize (Kb) 813700

[startup+880.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 251338 0 0 0 85999 933 0 0 25 0 1 0 1855629660 846069760 204966 4294967295 134512640 135167914 3221224448 3221106784 134621101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 206560 204966 162 162 0 206398 0
[pid=28237] vsize: 826240
Current children cumulated CPU time (s) 870.04
Current children cumulated vsize (Kb) 828368

[startup+890.07 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 255075 0 0 0 86958 950 0 0 25 0 1 0 1855629660 861376512 208703 4294967295 134512640 135167914 3221224448 3221106620 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 210297 208703 162 162 0 210135 0
[pid=28237] vsize: 841188
Current children cumulated CPU time (s) 879.8
Current children cumulated vsize (Kb) 843316

[startup+900.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 258438 0 0 0 87921 965 0 0 25 0 1 0 1855629660 875151360 212066 4294967295 134512640 135167914 3221224448 3221106128 134619544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28237/statm): 213660 212066 162 162 0 213498 0
[pid=28237] vsize: 854640
Current children cumulated CPU time (s) 889.58
Current children cumulated vsize (Kb) 856768

[startup+910.073 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 261860 0 35 0 88850 984 0 0 18 0 1 0 1855629660 888340480 215189 4294967295 134512640 135167914 3221224448 3221110016 134843012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 216880 215189 162 162 0 216718 0
[pid=28237] vsize: 867520
Current children cumulated CPU time (s) 899.06
Current children cumulated vsize (Kb) 869648

[startup+920.074 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 265449 0 47 0 89789 1003 0 0 25 0 1 0 1855629660 902799360 218076 4294967295 134512640 135167914 3221224448 3221106396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 220410 218076 162 162 0 220248 0
[pid=28237] vsize: 881640
Current children cumulated CPU time (s) 908.64
Current children cumulated vsize (Kb) 883768

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 269168 0 66 0 90731 1022 0 0 25 0 1 0 1855629660 917942272 220607 4294967295 134512640 135167914 3221224448 3221111560 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 224107 220607 162 162 0 223945 0
[pid=28237] vsize: 896428
Current children cumulated CPU time (s) 918.25
Current children cumulated vsize (Kb) 898556

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) R 28232 28232 31027 0 -1 0 272710 0 104 0 91656 1039 0 0 22 0 1 0 1855629660 932212736 222933 4294967295 134512640 135167914 3221224448 3221105792 134844691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28237/statm): 227591 222933 162 162 0 227429 0
[pid=28237] vsize: 910364
Current children cumulated CPU time (s) 927.67
Current children cumulated vsize (Kb) 912492



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+948.288 s]
Raw data (loadavg): 1.07 0.99 0.94 1/57 28237
Raw data (/proc/28232/stat): 28232 (minisat+_script) S 28231 28232 31027 0 -1 0 314 2384 0 0 0 1 60 11 18 0 1 0 1855629576 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28232/statm): 532 234 485 147 0 385 0
[pid=28232] vsize: 2128
Raw data (/proc/28237/stat): 28237 (minisat+_bignum) T 28232 28232 31027 0 -1 0 275408 0 266 0 92289 1055 0 0 21 0 1 0 1855629660 941543424 224763 4294967295 134512640 135167914 3221224448 3221105852 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28237/statm): 229869 224763 162 162 0 229707 0
[pid=28237] vsize: 919476
Current children cumulated CPU time (s) 934.16
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 948.718
CPU time (s): 933.876
CPU user time (s): 922.898
CPU system time (s): 10.9783
CPU usage (%): 98.4355
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !