PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM	9136d330eaa53552ba154b6915193b35
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	7560
Biggest coefficient in the objective function	2097152
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	876993750
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	2097152
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	876993750
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.131979
Number of variables	14760
Total number of constraints	1110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	360
Number of constraints which are nor clauses,nor cardinality constraints	750
Minimum length of a constraint	1
Maximum length of a constraint	252
Trace number 14216

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-20 23:18:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20293 boxname=wulflinc6 idbench=1561 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9136d330eaa53552ba154b6915193b35  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-tr12-30.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-tr12-30.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-tr12-30.opb
IDLAUNCH: 20293
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        868232 kB
Buffers:         29372 kB
Cached:         115124 kB
SwapCached:          4 kB
Active:          26316 kB
Inactive:       120684 kB
HighTotal:      131008 kB
HighFree:        37408 kB
LowTotal:       903652 kB
LowFree:        830824 kB
SwapTotal:     2097136 kB
SwapFree:      2096768 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5920 kB
Slab:            13764 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:38:09 (client local time) WITH STATUS 0 IN 1200.44 SECONDS
stats: 20293 7 1200.44 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1109]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1108]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1107]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1106]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1105]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1104]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1103]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1102]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1101]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1100]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1099]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1098]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1097]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1096]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1095]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1094]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1093]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1092]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1091]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1090]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1089]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1088]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1087]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1086]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1085]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1084]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1083]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1082]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1081]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1080]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1078]---> BDD-cost:   71
c ---[1076]---> BDD-cost:  159
c ---[1074]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1072]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1070]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1068]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1066]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1064]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1062]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1060]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1058]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1056]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1054]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1052]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1050]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1048]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1046]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1044]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1042]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1040]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1038]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1036]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1034]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1032]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1030]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1028]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1026]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1024]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1020]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1018]---> BDD-cost:   67
c ---[1016]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1014]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1012]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1010]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1008]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1006]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1004]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1002]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1000]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 998]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 996]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 994]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 992]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 990]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 988]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 986]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 984]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 982]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 980]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 978]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 976]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 974]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 972]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 970]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 968]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 966]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 964]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 962]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 960]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 958]---> BDD-cost:   52
c ---[ 956]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 950]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 948]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 946]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 944]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 942]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 940]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 934]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 928]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 926]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 924]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 920]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 918]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 916]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 914]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 912]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 910]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 908]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 906]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 904]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 902]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 900]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 898]---> BDD-cost:   71
c ---[ 896]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 894]---> BDD-cost:  164
c ---[ 892]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 890]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 888]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 886]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 884]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 880]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 878]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 876]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 874]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 872]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 870]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 868]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 866]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 864]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 862]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 860]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 858]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 856]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 854]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 852]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 850]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 848]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 846]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 844]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 842]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 840]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 838]---> BDD-cost:   52
c ---[ 836]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 832]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 830]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 828]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 826]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 824]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 822]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 820]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 818]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 816]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 814]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 810]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 808]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 806]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 804]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 800]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 798]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 796]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 794]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 792]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 790]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 788]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> BDD-cost:   65
c ---[ 776]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> BDD-cost:  166
c ---[ 770]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 740]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 724]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 720]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> BDD-cost:   67
c ---[ 716]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> BDD-cost:  166
c ---[ 710]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 692]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 670]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 668]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> BDD-cost:   63
c ---[ 656]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> BDD-cost:  166
c ---[ 650]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 644]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 598]---> BDD-cost:   71
c ---[ 596]---> BDD-cost:  159
c ---[ 594]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> BDD-cost:   52
c ---[ 536]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> BDD-cost:  164
c ---[ 532]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> BDD-cost:   71
c ---[ 476]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> BDD-cost:   52
c ---[ 416]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> BDD-cost:  166
c ---[ 410]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 408]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> BDD-cost:   28
c ---[ 358]---> BDD-cost:   28
c ---[ 357]---> BDD-cost:   28
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   28
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   28
c ---[ 352]---> BDD-cost:   28
c ---[ 351]---> BDD-cost:   28
c ---[ 350]---> BDD-cost:   28
c ---[ 349]---> BDD-cost:   28
c ---[ 348]---> BDD-cost:   28
c ---[ 347]---> BDD-cost:   28
c ---[ 346]---> BDD-cost:   28
c ---[ 345]---> BDD-cost:   28
c ---[ 344]---> BDD-cost:   28
c ---[ 343]---> BDD-cost:   28
c ---[ 342]---> BDD-cost:   28
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:   28
c ---[ 339]---> BDD-cost:   28
c ---[ 338]---> BDD-cost:   28
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   28
c ---[ 335]---> BDD-cost:   28
c ---[ 334]---> BDD-cost:   28
c ---[ 333]---> BDD-cost:   28
c ---[ 332]---> BDD-cost:   28
c ---[ 331]---> BDD-cost:   28
c ---[ 330]---> BDD-cost:   28
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   27
c ---[ 327]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:   27
c ---[ 325]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   27
c ---[ 322]---> BDD-cost:   27
c ---[ 321]---> BDD-cost:   27
c ---[ 320]---> BDD-cost:   27
c ---[ 319]---> BDD-cost:   27
c ---[ 318]---> BDD-cost:   27
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   27
c ---[ 315]---> BDD-cost:   27
c ---[ 314]---> BDD-cost:   27
c ---[ 313]---> BDD-cost:   27
c ---[ 312]---> BDD-cost:   27
c ---[ 311]---> BDD-cost:   27
c ---[ 310]---> BDD-cost:   27
c ---[ 309]---> BDD-cost:   27
c ---[ 308]---> BDD-cost:   27
c ---[ 307]---> BDD-cost:   27
c ---[ 306]---> BDD-cost:   27
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   27
c ---[ 303]---> BDD-cost:   27
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   27
c ---[ 299]---> BDD-cost:   25
c ---[ 298]---> BDD-cost:   25
c ---[ 297]---> BDD-cost:   25
c ---[ 296]---> BDD-cost:   25
c ---[ 295]---> BDD-cost:   25
c ---[ 294]---> BDD-cost:   25
c ---[ 293]---> BDD-cost:   25
c ---[ 292]---> BDD-cost:   25
c ---[ 291]---> BDD-cost:   25
c ---[ 290]---> BDD-cost:   25
c ---[ 289]---> BDD-cost:   25
c ---[ 288]---> BDD-cost:   25
c ---[ 287]---> BDD-cost:   25
c ---[ 286]---> BDD-cost:   25
c ---[ 285]---> BDD-cost:   25
c ---[ 284]---> BDD-cost:   25
c ---[ 283]---> BDD-cost:   25
c ---[ 282]---> BDD-cost:   25
c ---[ 281]---> BDD-cost:   25
c ---[ 280]---> BDD-cost:   25
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   25
c ---[ 277]---> BDD-cost:   25
c ---[ 276]---> BDD-cost:   25
c ---[ 275]---> BDD-cost:   25
c ---[ 274]---> BDD-cost:   25
c ---[ 273]---> BDD-cost:   25
c ---[ 272]---> BDD-cost:   25
c ---[ 271]---> BDD-cost:   25
c ---[ 270]---> BDD-cost:   25
c ---[ 269]---> BDD-cost:   28
c ---[ 268]---> BDD-cost:   28
c ---[ 267]---> BDD-cost:   28
c ---[ 266]---> BDD-cost:   28
c ---[ 265]---> BDD-cost:   28
c ---[ 264]---> BDD-cost:   28
c ---[ 263]---> BDD-cost:   28
c ---[ 262]---> BDD-cost:   28
c ---[ 261]---> BDD-cost:   28
c ---[ 260]---> BDD-cost:   28
c ---[ 259]---> BDD-cost:   28
c ---[ 258]---> BDD-cost:   28
c ---[ 257]---> BDD-cost:   28
c ---[ 256]---> BDD-cost:   28
c ---[ 255]---> BDD-cost:   28
c ---[ 254]---> BDD-cost:   28
c ---[ 253]---> BDD-cost:   28
c ---[ 252]---> BDD-cost:   28
c ---[ 251]---> BDD-cost:   28
c ---[ 250]---> BDD-cost:   28
c ---[ 249]---> BDD-cost:   28
c ---[ 248]---> BDD-cost:   28
c ---[ 247]---> BDD-cost:   28
c ---[ 246]---> BDD-cost:   28
c ---[ 245]---> BDD-cost:   28
c ---[ 244]---> BDD-cost:   28
c ---[ 243]---> BDD-cost:   28
c ---[ 242]---> BDD-cost:   28
c ---[ 241]---> BDD-cost:   28
c ---[ 240]---> BDD-cost:   28
c ---[ 239]---> BDD-cost:   28
c ---[ 238]---> BDD-cost:   28
c ---[ 237]---> BDD-cost:   28
c ---[ 236]---> BDD-cost:   28
c ---[ 235]---> BDD-cost:   28
c ---[ 234]---> BDD-cost:   28
c ---[ 233]---> BDD-cost:   28
c ---[ 232]---> BDD-cost:   28
c ---[ 231]---> BDD-cost:   28
c ---[ 230]---> BDD-cost:   28
c ---[ 229]---> BDD-cost:   28
c ---[ 228]---> BDD-cost:   28
c ---[ 227]---> BDD-cost:   28
c ---[ 226]---> BDD-cost:   28
c ---[ 225]---> BDD-cost:   28
c ---[ 224]---> BDD-cost:   28
c ---[ 223]---> BDD-cost:   28
c ---[ 222]---> BDD-cost:   28
c ---[ 221]---> BDD-cost:   28
c ---[ 220]---> BDD-cost:   28
c ---[ 219]---> BDD-cost:   28
c ---[ 218]---> BDD-cost:   28
c ---[ 217]---> BDD-cost:   28
c ---[ 216]---> BDD-cost:   28
c ---[ 215]---> BDD-cost:   28
c ---[ 214]---> BDD-cost:   28
c ---[ 213]---> BDD-cost:   28
c ---[ 212]---> BDD-cost:   28
c ---[ 211]---> BDD-cost:   28
c ---[ 210]---> BDD-cost:   28
c ---[ 209]---> BDD-cost:   28
c ---[ 208]---> BDD-cost:   28
c ---[ 207]---> BDD-cost:   28
c ---[ 206]---> BDD-cost:   28
c ---[ 205]---> BDD-cost:   28
c ---[ 204]---> BDD-cost:   28
c ---[ 203]---> BDD-cost:   28
c ---[ 202]---> BDD-cost:   28
c ---[ 201]---> BDD-cost:   28
c ---[ 200]---> BDD-cost:   28
c ---[ 199]---> BDD-cost:   28
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   28
c ---[ 196]---> BDD-cost:   28
c ---[ 195]---> BDD-cost:   28
c ---[ 194]---> BDD-cost:   28
c ---[ 193]---> BDD-cost:   28
c ---[ 192]---> BDD-cost:   28
c ---[ 191]---> BDD-cost:   28
c ---[ 190]---> BDD-cost:   28
c ---[ 189]---> BDD-cost:   28
c ---[ 188]---> BDD-cost:   28
c ---[ 187]---> BDD-cost:   28
c ---[ 186]---> BDD-cost:   28
c ---[ 185]---> BDD-cost:   28
c ---[ 184]---> BDD-cost:   28
c ---[ 183]---> BDD-cost:   28
c ---[ 182]---> BDD-cost:   28
c ---[ 181]---> BDD-cost:   28
c ---[ 180]---> BDD-cost:   28
c ---[ 179]---> BDD-cost:   27
c ---[ 178]---> BDD-cost:   27
c ---[ 177]---> BDD-cost:   27
c ---[ 176]---> BDD-cost:   27
c ---[ 175]---> BDD-cost:   27
c ---[ 174]---> BDD-cost:   27
c ---[ 173]---> BDD-cost:   27
c ---[ 172]---> BDD-cost:   27
c ---[ 171]---> BDD-cost:   27
c ---[ 170]---> BDD-cost:   27
c ---[ 169]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:   27
c ---[ 167]---> BDD-cost:   27
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   27
c ---[ 164]---> BDD-cost:   27
c ---[ 163]---> BDD-cost:   27
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:   27
c ---[ 160]---> BDD-cost:   27
c ---[ 159]---> BDD-cost:   27
c ---[ 158]---> BDD-cost:   27
c ---[ 157]---> BDD-cost:   27
c ---[ 156]---> BDD-cost:   27
c ---[ 155]---> BDD-cost:   27
c ---[ 154]---> BDD-cost:   27
c ---[ 153]---> BDD-cost:   27
c ---[ 152]---> BDD-cost:   27
c ---[ 151]---> BDD-cost:   27
c ---[ 150]---> BDD-cost:   27
c ---[ 149]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   27
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   27
c ---[ 144]---> BDD-cost:   27
c ---[ 143]---> BDD-cost:   27
c ---[ 142]---> BDD-cost:   27
c ---[ 141]---> BDD-cost:   27
c ---[ 140]---> BDD-cost:   27
c ---[ 139]---> BDD-cost:   27
c ---[ 138]---> BDD-cost:   27
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   27
c ---[ 131]---> BDD-cost:   27
c ---[ 130]---> BDD-cost:   27
c ---[ 129]---> BDD-cost:   27
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   27
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   28
c ---[ 118]---> BDD-cost:   28
c ---[ 117]---> BDD-cost:   28
c ---[ 116]---> BDD-cost:   28
c ---[ 115]---> BDD-cost:   28
c ---[ 114]---> BDD-cost:   28
c ---[ 113]---> BDD-cost:   28
c ---[ 112]---> BDD-cost:   28
c ---[ 111]---> BDD-cost:   28
c ---[ 110]---> BDD-cost:   28
c ---[ 109]---> BDD-cost:   28
c ---[ 108]---> BDD-cost:   28
c ---[ 107]---> BDD-cost:   28
c ---[ 106]---> BDD-cost:   28
c ---[ 105]---> BDD-cost:   28
c ---[ 104]---> BDD-cost:   28
c ---[ 103]---> BDD-cost:   28
c ---[ 102]---> BDD-cost:   28
c ---[ 101]---> BDD-cost:   28
c ---[ 100]---> BDD-cost:   28
c ---[  99]---> BDD-cost:   28
c ---[  98]---> BDD-cost:   28
c ---[  97]---> BDD-cost:   28
c ---[  96]---> BDD-cost:   28
c ---[  95]---> BDD-cost:   28
c ---[  94]---> BDD-cost:   28
c ---[  93]---> BDD-cost:   28
c ---[  92]---> BDD-cost:   28
c ---[  91]---> BDD-cost:   28
c ---[  90]---> BDD-cost:   28
c ---[  89]---> BDD-cost:   25
c ---[  88]---> BDD-cost:   25
c ---[  87]---> BDD-cost:   25
c ---[  86]---> BDD-cost:   25
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   25
c ---[  83]---> BDD-cost:   25
c ---[  82]---> BDD-cost:   25
c ---[  81]---> BDD-cost:   25
c ---[  80]---> BDD-cost:   25
c ---[  79]---> BDD-cost:   25
c ---[  78]---> BDD-cost:   25
c ---[  77]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   25
c ---[  75]---> BDD-cost:   25
c ---[  74]---> BDD-cost:   25
c ---[  73]---> BDD-cost:   25
c ---[  72]---> BDD-cost:   25
c ---[  71]---> BDD-cost:   25
c ---[  70]---> BDD-cost:   25
c ---[  69]---> BDD-cost:   25
c ---[  68]---> BDD-cost:   25
c ---[  67]---> BDD-cost:   25
c ---[  66]---> BDD-cost:   25
c ---[  65]---> BDD-cost:   25
c ---[  64]---> BDD-cost:   25
c ---[  63]---> BDD-cost:   25
c ---[  62]---> BDD-cost:   25
c ---[  61]---> BDD-cost:   25
c ---[  60]---> BDD-cost:   25
c ---[  59]---> BDD-cost:   27
c ---[  58]---> BDD-cost:   27
c ---[  57]---> BDD-cost:   27
c ---[  56]---> BDD-cost:   27
c ---[  55]---> BDD-cost:   27
c ---[  54]---> BDD-cost:   27
c ---[  53]---> BDD-cost:   27
c ---[  52]---> BDD-cost:   27
c ---[  51]---> BDD-cost:   27
c ---[  50]---> BDD-cost:   27
c ---[  49]---> BDD-cost:   27
c ---[  48]---> BDD-cost:   27
c ---[  47]---> BDD-cost:   27
c ---[  46]---> BDD-cost:   27
c ---[  45]---> BDD-cost:   27
c ---[  44]---> BDD-cost:   27
c ---[  43]---> BDD-cost:   27
c ---[  42]---> BDD-cost:   27
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   27
c ---[  34]---> BDD-cost:   27
c ---[  33]---> BDD-cost:   27
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   25
c ---[  28]---> BDD-cost:   25
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   25
c ---[  25]---> BDD-cost:   25
c ---[  24]---> BDD-cost:   25
c ---[  23]---> BDD-cost:   25
c ---[  22]---> BDD-cost:   25
c ---[  21]---> BDD-cost:   25
c ---[  20]---> BDD-cost:   25
c ---[  19]---> BDD-cost:   25
c ---[  18]---> BDD-cost:   25
c ---[  17]---> BDD-cost:   25
c ---[  16]---> BDD-cost:   25
c ---[  15]---> BDD-cost:   25
c ---[  14]---> BDD-cost:   25
c ---[  13]---> BDD-cost:   25
c ---[  12]---> BDD-cost:   25
c ---[  11]---> BDD-cost:   25
c ---[  10]---> BDD-cost:   25
c ---[   9]---> BDD-cost:   25
c ---[   8]---> BDD-cost:   25
c ---[   7]---> BDD-cost:   25
c ---[   6]---> BDD-cost:   25
c ---[   5]---> BDD-cost:   25
c ---[   4]---> BDD-cost:   25
c ---[   3]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   25
c ---[   1]---> BDD-cost:   25
c ---[   0]---> BDD-cost:   25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  466205  1229635 |  155401       0        0     nan |  0.000 % |
c |       101 |  465930  1229014 |  170941      70      221     3.2 | 11.163 % |
c |       252 |  465699  1228504 |  188035     185      576     3.1 | 11.207 % |
c |       477 |  464873  1226659 |  206838     307      996     3.2 | 11.353 % |
c |       814 |  464118  1224908 |  227522     559     1883     3.4 | 11.482 % |
c |      1320 |  463021  1222456 |  250274     932     3438     3.7 | 11.678 % |
c |      2080 |  461131  1218209 |  275302    1465     5564     3.8 | 12.011 % |
c |      3221 |  457907  1211011 |  302832    2208     8313     3.8 | 12.588 % |
c |      4929 |  455001  1204504 |  333115    3569    15415     4.3 | 13.106 % |
c |      7491 |  449529  1192284 |  366427    5470    23997     4.4 | 14.083 % |
c |     11335 |  445165  1182225 |  403070    8755    50772     5.8 | 14.830 % |
c |     17102 |  443948  1179412 |  443377   14354   147741    10.3 | 15.039 % |
c |     25752 |  440235  1170997 |  487714   22557   253522    11.2 | 15.687 % |
c |     38726 |  436699  1162897 |  536486   35104   451429    12.9 | 16.291 % |
c |     58188 |  436633  1162729 |  590135   54557   924663    16.9 | 16.302 % |
c |     87380 |  436515  1162416 |  649148   83730  1694437    20.2 | 16.318 % |
c |    131169 |  436473  1162301 |  714063  127513  2798560    21.9 | 16.323 % |
c |    196854 |  436347  1162001 |  785469  193185  4656374    24.1 | 16.344 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.99 0.93 2/54 25035
Raw data (stat): 25035 (runsolver) R 25034 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482116481 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99991 s]
Raw data (loadavg): 0.94 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14403 0 0 0 959 39 0 0 25 0 1 0 482116481 67510272 13674 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16482 13674 603 41 0 16441 0
vsize: 65928
[startup+20.0001 s]
Raw data (loadavg): 0.95 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14407 0 0 0 1959 40 0 0 25 0 1 0 482116481 67645440 13678 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16515 13678 603 41 0 16474 0
vsize: 66060
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14419 0 0 0 2960 40 0 0 25 0 1 0 482116481 67645440 13690 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16515 13690 603 41 0 16474 0
vsize: 66060
[startup+40.0004 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14424 0 0 0 3958 40 0 0 25 0 1 0 482116481 67645440 13695 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16515 13695 603 41 0 16474 0
vsize: 66060
[startup+50.0009 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14431 0 0 0 4958 41 0 0 25 0 1 0 482116481 67645440 13702 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16515 13702 603 41 0 16474 0
vsize: 66060
[startup+60.0011 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14438 0 0 0 5958 41 0 0 25 0 1 0 482116481 67780608 13709 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16548 13709 603 41 0 16507 0
vsize: 66192
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14448 0 0 0 6958 41 0 0 25 0 1 0 482116481 67780608 13719 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16548 13719 603 41 0 16507 0
vsize: 66192
[startup+80.0019 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14451 0 0 0 7958 42 0 0 25 0 1 0 482116481 67780608 13722 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16548 13722 603 41 0 16507 0
vsize: 66192
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14462 0 0 0 8959 42 0 0 25 0 1 0 482116481 67780608 13733 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16548 13733 603 41 0 16507 0
vsize: 66192
[startup+100.002 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14465 0 0 0 9958 42 0 0 25 0 1 0 482116481 67780608 13736 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16548 13736 603 41 0 16507 0
vsize: 66192
[startup+110.014 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14473 0 0 0 10960 42 0 0 25 0 1 0 482116481 67915776 13744 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16581 13744 603 41 0 16540 0
vsize: 66324
[startup+120.026 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14479 0 0 0 11961 43 0 0 25 0 1 0 482116481 67915776 13750 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16581 13750 603 41 0 16540 0
vsize: 66324
[startup+130.026 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14485 0 0 0 12961 43 0 0 25 0 1 0 482116481 67915776 13756 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16581 13756 603 41 0 16540 0
vsize: 66324
[startup+140.026 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14486 0 0 0 13961 43 0 0 25 0 1 0 482116481 67915776 13757 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16581 13757 603 41 0 16540 0
vsize: 66324
[startup+150.031 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14495 0 0 0 14962 43 0 0 25 0 1 0 482116481 67915776 13766 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16581 13766 603 41 0 16540 0
vsize: 66324
[startup+160.031 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14501 0 0 0 15962 43 0 0 25 0 1 0 482116481 67915776 13772 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16581 13772 603 41 0 16540 0
vsize: 66324
[startup+170.033 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14509 0 0 0 16962 43 0 0 25 0 1 0 482116481 68050944 13780 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16614 13780 603 41 0 16573 0
vsize: 66456
[startup+180.033 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14516 0 0 0 17962 43 0 0 25 0 1 0 482116481 68050944 13787 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16614 13787 603 41 0 16573 0
vsize: 66456
[startup+190.034 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14526 0 0 0 18962 44 0 0 25 0 1 0 482116481 68050944 13797 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16614 13797 603 41 0 16573 0
vsize: 66456
[startup+200.034 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14535 0 0 0 19962 44 0 0 25 0 1 0 482116481 68050944 13806 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16614 13806 603 41 0 16573 0
vsize: 66456
[startup+210.034 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14547 0 0 0 20962 44 0 0 25 0 1 0 482116481 68186112 13818 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13818 603 41 0 16606 0
vsize: 66588
[startup+220.035 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14552 0 0 0 21963 44 0 0 25 0 1 0 482116481 68186112 13823 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13823 603 41 0 16606 0
vsize: 66588
[startup+230.036 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14554 0 0 0 22963 44 0 0 25 0 1 0 482116481 68186112 13825 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13825 603 41 0 16606 0
vsize: 66588
[startup+240.037 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14556 0 0 0 23963 45 0 0 25 0 1 0 482116481 68186112 13827 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13827 603 41 0 16606 0
vsize: 66588
[startup+250.036 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14562 0 0 0 24963 45 0 0 25 0 1 0 482116481 68186112 13833 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13833 603 41 0 16606 0
vsize: 66588
[startup+260.037 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14579 0 0 0 25963 45 0 0 25 0 1 0 482116481 68186112 13850 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13850 603 41 0 16606 0
vsize: 66588
[startup+270.037 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14584 0 0 0 26963 45 0 0 25 0 1 0 482116481 68186112 13855 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13855 603 41 0 16606 0
vsize: 66588
[startup+280.037 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14588 0 0 0 27963 45 0 0 25 0 1 0 482116481 68186112 13859 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13859 603 41 0 16606 0
vsize: 66588
[startup+290.038 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14589 0 0 0 28963 46 0 0 25 0 1 0 482116481 68186112 13860 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16647 13860 603 41 0 16606 0
vsize: 66588
[startup+300.039 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14599 0 0 0 29963 46 0 0 25 0 1 0 482116481 68321280 13870 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16680 13870 603 41 0 16639 0
vsize: 66720
[startup+310.038 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14622 0 0 0 30963 46 0 0 25 0 1 0 482116481 68321280 13893 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16680 13893 603 41 0 16639 0
vsize: 66720
[startup+320.039 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14702 0 0 0 31963 47 0 0 25 0 1 0 482116481 68726784 13973 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16779 13973 603 41 0 16738 0
vsize: 67116
[startup+330.04 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14756 0 0 0 32962 48 0 0 25 0 1 0 482116481 68857856 14027 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16811 14027 603 41 0 16770 0
vsize: 67244
[startup+340.04 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14792 0 0 0 33962 48 0 0 25 0 1 0 482116481 68993024 14063 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16844 14063 603 41 0 16803 0
vsize: 67376
[startup+350.041 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14805 0 0 0 34962 48 0 0 25 0 1 0 482116481 69128192 14076 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16877 14076 603 41 0 16836 0
vsize: 67508
[startup+360.042 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14848 0 0 0 35962 49 0 0 25 0 1 0 482116481 69357568 14119 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16933 14119 603 41 0 16892 0
vsize: 67732
[startup+370.041 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14857 0 0 0 36962 49 0 0 25 0 1 0 482116481 69357568 14128 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16933 14128 603 41 0 16892 0
vsize: 67732
[startup+380.042 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14876 0 0 0 37962 49 0 0 25 0 1 0 482116481 69357568 14147 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16933 14147 603 41 0 16892 0
vsize: 67732
[startup+390.042 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14899 0 0 0 38962 50 0 0 25 0 1 0 482116481 69492736 14170 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 14170 603 41 0 16925 0
vsize: 67864
[startup+400.043 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14912 0 0 0 39962 50 0 0 25 0 1 0 482116481 69627904 14183 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16999 14183 603 41 0 16958 0
vsize: 67996
[startup+410.044 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14936 0 0 0 40962 50 0 0 25 0 1 0 482116481 69627904 14207 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16999 14207 603 41 0 16958 0
vsize: 67996
[startup+420.046 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14951 0 0 0 41962 51 0 0 25 0 1 0 482116481 69758976 14222 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17031 14222 603 41 0 16990 0
vsize: 68124
[startup+430.046 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14966 0 0 0 42962 51 0 0 25 0 1 0 482116481 69758976 14237 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17031 14237 603 41 0 16990 0
vsize: 68124
[startup+440.047 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 14996 0 0 0 43962 52 0 0 25 0 1 0 482116481 69902336 14267 4294967295 134512640 134672761 3221224544 3221223668 134566095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17066 14267 603 41 0 17025 0
vsize: 68264
[startup+450.047 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15021 0 0 0 44962 52 0 0 25 0 1 0 482116481 70037504 14292 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17099 14292 603 41 0 17058 0
vsize: 68396
[startup+460.047 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15046 0 0 0 45961 52 0 0 25 0 1 0 482116481 70037504 14317 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17099 14317 603 41 0 17058 0
vsize: 68396
[startup+470.048 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15081 0 0 0 46962 52 0 0 25 0 1 0 482116481 70172672 14352 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17132 14352 603 41 0 17091 0
vsize: 68528
[startup+480.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15097 0 0 0 47962 53 0 0 25 0 1 0 482116481 70307840 14368 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17165 14368 603 41 0 17124 0
vsize: 68660
[startup+490.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15149 0 0 0 48961 53 0 0 25 0 1 0 482116481 70443008 14420 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17198 14420 603 41 0 17157 0
vsize: 68792
[startup+500.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15186 0 0 0 49961 54 0 0 25 0 1 0 482116481 70705152 14457 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17262 14457 603 41 0 17221 0
vsize: 69048
[startup+510.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15196 0 0 0 50961 54 0 0 25 0 1 0 482116481 70705152 14467 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17262 14467 603 41 0 17221 0
vsize: 69048
[startup+520.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15356 0 0 0 51961 54 0 0 25 0 1 0 482116481 71524352 14627 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17462 14627 603 41 0 17421 0
vsize: 69848
[startup+530.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15644 0 0 0 52960 56 0 0 25 0 1 0 482116481 72704000 14915 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17750 14915 603 41 0 17709 0
vsize: 71000
[startup+540.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 15898 0 0 0 53959 57 0 0 25 0 1 0 482116481 73641984 15169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17979 15169 603 41 0 17938 0
vsize: 71916
[startup+550.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 16155 0 0 0 54959 57 0 0 25 0 1 0 482116481 74715136 15426 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18241 15426 603 41 0 18200 0
vsize: 72964
[startup+560.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 16337 0 0 0 55959 58 0 0 25 0 1 0 482116481 75513856 15608 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18436 15608 603 41 0 18395 0
vsize: 73744
[startup+570.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 16519 0 0 0 56958 59 0 0 25 0 1 0 482116481 76439552 15790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18662 15790 603 41 0 18621 0
vsize: 74648
[startup+580.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 16708 0 0 0 57957 60 0 0 25 0 1 0 482116481 77299712 15979 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 15979 603 41 0 18831 0
vsize: 75488
[startup+590.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 16925 0 0 0 58957 61 0 0 25 0 1 0 482116481 78258176 16196 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19106 16196 603 41 0 19065 0
vsize: 76424
[startup+600.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 17114 0 0 0 59956 62 0 0 25 0 1 0 482116481 79093760 16385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19310 16385 603 41 0 19269 0
vsize: 77240
[startup+610.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 17331 0 0 0 60955 63 0 0 25 0 1 0 482116481 79925248 16602 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19513 16602 603 41 0 19472 0
vsize: 78052
[startup+620.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 17508 0 0 0 61955 63 0 0 25 0 1 0 482116481 80658432 16779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19692 16779 603 41 0 19651 0
vsize: 78768
[startup+630.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 17612 0 0 0 62955 64 0 0 25 0 1 0 482116481 81063936 16883 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19791 16883 603 41 0 19750 0
vsize: 79164
[startup+640.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 17734 0 0 0 63954 65 0 0 25 0 1 0 482116481 81588224 17005 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19919 17005 603 41 0 19878 0
vsize: 79676
[startup+650.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 17844 0 0 0 64954 65 0 0 25 0 1 0 482116481 82001920 17115 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20020 17115 603 41 0 19979 0
vsize: 80080
[startup+660.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 17965 0 0 0 65954 66 0 0 25 0 1 0 482116481 82399232 17236 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20117 17236 603 41 0 20076 0
vsize: 80468
[startup+670.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18102 0 0 0 66954 67 0 0 25 0 1 0 482116481 83013632 17373 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20267 17373 603 41 0 20226 0
vsize: 81068
[startup+680.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18229 0 0 0 67954 67 0 0 25 0 1 0 482116481 83587072 17500 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20407 17500 603 41 0 20366 0
vsize: 81628
[startup+690.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18331 0 0 0 68953 68 0 0 25 0 1 0 482116481 83984384 17602 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20504 17602 603 41 0 20463 0
vsize: 82016
[startup+700.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18451 0 0 0 69953 68 0 0 25 0 1 0 482116481 84414464 17722 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20609 17722 603 41 0 20568 0
vsize: 82436
[startup+710.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18574 0 0 0 70953 69 0 0 25 0 1 0 482116481 84951040 17845 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20740 17845 603 41 0 20699 0
vsize: 82960
[startup+720.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18683 0 0 0 71953 69 0 0 25 0 1 0 482116481 85528576 17954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20881 17954 603 41 0 20840 0
vsize: 83524
[startup+730.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18835 0 0 0 72952 70 0 0 25 0 1 0 482116481 86614016 18106 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21146 18106 603 41 0 21105 0
vsize: 84584
[startup+740.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 18932 0 0 0 73952 70 0 0 25 0 1 0 482116481 87171072 18203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21282 18203 603 41 0 21241 0
vsize: 85128
[startup+750.065 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19031 0 0 0 74953 71 0 0 25 0 1 0 482116481 87465984 18302 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21354 18302 603 41 0 21313 0
vsize: 85416
[startup+760.065 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19137 0 0 0 75953 71 0 0 25 0 1 0 482116481 87879680 18408 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21455 18408 603 41 0 21414 0
vsize: 85820
[startup+770.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19288 0 0 0 76952 72 0 0 25 0 1 0 482116481 88576000 18559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21625 18559 603 41 0 21584 0
vsize: 86500
[startup+780.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19372 0 0 0 77953 72 0 0 25 0 1 0 482116481 88842240 18643 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21690 18643 603 41 0 21649 0
vsize: 86760
[startup+790.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19536 0 0 0 78952 72 0 0 25 0 1 0 482116481 89513984 18807 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21854 18807 603 41 0 21813 0
vsize: 87416
[startup+800.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19686 0 0 0 79952 73 0 0 25 0 1 0 482116481 90079232 18957 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21992 18957 603 41 0 21951 0
vsize: 87968
[startup+810.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19809 0 0 0 80953 73 0 0 25 0 1 0 482116481 90615808 19080 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22123 19080 603 41 0 22082 0
vsize: 88492
[startup+820.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 19910 0 0 0 81953 73 0 0 25 0 1 0 482116481 91037696 19181 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22226 19181 603 41 0 22185 0
vsize: 88904
[startup+830.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20002 0 0 0 82953 73 0 0 25 0 1 0 482116481 91508736 19273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22341 19273 603 41 0 22300 0
vsize: 89364
[startup+840.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20090 0 0 0 83953 74 0 0 25 0 1 0 482116481 91774976 19361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22406 19361 603 41 0 22365 0
vsize: 89624
[startup+850.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20179 0 0 0 84953 74 0 0 25 0 1 0 482116481 92176384 19450 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22504 19450 603 41 0 22463 0
vsize: 90016
[startup+860.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20270 0 0 0 85952 75 0 0 25 0 1 0 482116481 92467200 19541 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22575 19541 603 41 0 22534 0
vsize: 90300
[startup+870.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20350 0 0 0 86952 75 0 0 25 0 1 0 482116481 92872704 19621 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22674 19621 603 41 0 22633 0
vsize: 90696
[startup+880.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20432 0 0 0 87952 76 0 0 25 0 1 0 482116481 93138944 19703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22739 19703 603 41 0 22698 0
vsize: 90956
[startup+890.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20512 0 0 0 88952 76 0 0 25 0 1 0 482116481 93532160 19783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22835 19783 603 41 0 22794 0
vsize: 91340
[startup+900.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20609 0 0 0 89953 76 0 0 25 0 1 0 482116481 94199808 19880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22998 19880 603 41 0 22957 0
vsize: 91992
[startup+910.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20773 0 0 0 90952 77 0 0 25 0 1 0 482116481 94736384 20044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23129 20044 603 41 0 23088 0
vsize: 92516
[startup+920.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 20889 0 0 0 91952 77 0 0 25 0 1 0 482116481 95272960 20160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23260 20160 603 41 0 23219 0
vsize: 93040
[startup+930.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21021 0 0 0 92952 78 0 0 25 0 1 0 482116481 95801344 20292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23389 20292 603 41 0 23348 0
vsize: 93556
[startup+940.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21086 0 0 0 93952 78 0 0 25 0 1 0 482116481 96063488 20357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23453 20357 603 41 0 23412 0
vsize: 93812
[startup+950.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21176 0 0 0 94952 78 0 0 25 0 1 0 482116481 96428032 20447 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23542 20447 603 41 0 23501 0
vsize: 94168
[startup+960.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21255 0 0 0 95951 79 0 0 25 0 1 0 482116481 96862208 20526 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23648 20526 603 41 0 23607 0
vsize: 94592
[startup+970.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21315 0 0 0 96951 79 0 0 25 0 1 0 482116481 97124352 20586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23712 20586 603 41 0 23671 0
vsize: 94848
[startup+980.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21422 0 0 0 97951 80 0 0 25 0 1 0 482116481 97546240 20693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23815 20693 603 41 0 23774 0
vsize: 95260
[startup+990.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21573 0 0 0 98950 80 0 0 25 0 1 0 482116481 98217984 20844 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23979 20844 603 41 0 23938 0
vsize: 95916
[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21690 0 0 0 99950 81 0 0 25 0 1 0 482116481 98623488 20961 4294967295 134512640 134672761 3221224544 3221223712 134561086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24078 20961 603 41 0 24037 0
vsize: 96312
[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21789 0 0 0 100950 81 0 0 25 0 1 0 482116481 99024896 21060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24176 21060 603 41 0 24135 0
vsize: 96704
[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 21873 0 0 0 101950 82 0 0 25 0 1 0 482116481 99295232 21144 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24242 21144 603 41 0 24201 0
vsize: 96968
[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22046 0 0 0 102950 82 0 0 25 0 1 0 482116481 100106240 21317 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24440 21317 603 41 0 24399 0
vsize: 97760
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22157 0 0 0 103950 82 0 0 25 0 1 0 482116481 100507648 21428 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24538 21428 603 41 0 24497 0
vsize: 98152
[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22245 0 0 0 104950 83 0 0 25 0 1 0 482116481 100909056 21516 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24636 21516 603 41 0 24595 0
vsize: 98544
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22351 0 0 0 105950 83 0 0 25 0 1 0 482116481 101314560 21622 4294967295 134512640 134672761 3221224544 3221223600 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24735 21622 603 41 0 24694 0
vsize: 98940
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22465 0 0 0 106950 84 0 0 25 0 1 0 482116481 101715968 21736 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24833 21736 603 41 0 24792 0
vsize: 99332
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22575 0 0 0 107949 84 0 0 25 0 1 0 482116481 102146048 21846 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24938 21846 603 41 0 24897 0
vsize: 99752
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22660 0 0 0 108950 85 0 0 25 0 1 0 482116481 102416384 21931 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25004 21931 603 41 0 24963 0
vsize: 100016
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22767 0 0 0 109950 85 0 0 25 0 1 0 482116481 102821888 22038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25103 22038 603 41 0 25062 0
vsize: 100412
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 22886 0 0 0 110950 85 0 0 25 0 1 0 482116481 103354368 22157 4294967295 134512640 134672761 3221224544 3221223648 134560039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 22157 603 41 0 25192 0
vsize: 100932
[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 23028 0 0 0 111949 86 0 0 25 0 1 0 482116481 103890944 22299 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25364 22299 603 41 0 25323 0
vsize: 101456
[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 23130 0 0 0 112950 86 0 0 25 0 1 0 482116481 104329216 22401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25471 22401 603 41 0 25430 0
vsize: 101884
[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 23244 0 0 0 113949 87 0 0 25 0 1 0 482116481 104734720 22515 4294967295 134512640 134672761 3221224544 3221223728 134559383 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25570 22515 603 41 0 25529 0
vsize: 102280
[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 23359 0 0 0 114950 87 0 0 25 0 1 0 482116481 105271296 22630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25701 22630 603 41 0 25660 0
vsize: 102804
[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 23673 0 0 0 115949 88 0 0 25 0 1 0 482116481 106475520 22944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25995 22944 603 41 0 25954 0
vsize: 103980
[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 24011 0 0 0 116949 89 0 0 25 0 1 0 482116481 107806720 23282 4294967295 134512640 134672761 3221224544 3221223728 134559390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26320 23282 603 41 0 26279 0
vsize: 105280
[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 24269 0 0 0 117949 90 0 0 25 0 1 0 482116481 108875776 23540 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26581 23540 603 41 0 26540 0
vsize: 106324
[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 24500 0 0 0 118948 90 0 0 25 0 1 0 482116481 109793280 23771 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26805 23771 603 41 0 26764 0
vsize: 107220
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25035
Raw data (stat): 25035 (minisat+) R 25034 29653 29652 0 -1 0 24715 0 0 0 119948 90 0 0 25 0 1 0 482116481 110727168 23986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27033 23986 603 41 0 26992 0
vsize: 108132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 25035
Raw data (stat): 25035 (minisat+) Z 25034 29653 29652 0 -1 12 24717 0 0 0 119948 95 0 0 25 0 1 0 482116481 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.13
CPU time (s): 1200.44
CPU user time (s): 1199.49
CPU system time (s): 0.955854
CPU usage (%): 100.026
Max. virtual memory (Kb): 108132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####