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 14214

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-20 23:17:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20285 boxname=wulflinc24 idbench=1561 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  9136d330eaa53552ba154b6915193b35  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-tr12-30.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-tr12-30.opb
IDLAUNCH: 20285
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        719228 kB
Buffers:         31404 kB
Cached:         249812 kB
SwapCached:        508 kB
Active:          30168 kB
Inactive:       253196 kB
HighTotal:      131008 kB
HighFree:        40096 kB
LowTotal:       903652 kB
LowFree:        679132 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            26284 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:37:54 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 20285 7 1200.21 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 |  456278  1197453 |  152092       0        0     nan |  0.000 % |
c |       100 |  455995  1196818 |  167301      61      197     3.2 | 11.170 % |
c |       250 |  455216  1195078 |  184031     129      417     3.2 | 11.304 % |
c |       475 |  454686  1193863 |  202434     290     1031     3.6 | 11.395 % |
c |       812 |  453751  1191753 |  222677     517     1868     3.6 | 11.562 % |
c |      1318 |  452613  1189203 |  244945     883     3515     4.0 | 11.766 % |
c |      2077 |  450447  1184360 |  269440    1370     5358     3.9 | 12.153 % |
c |      3216 |  448180  1179291 |  296384    2226     8782     3.9 | 12.563 % |
c |      4924 |  443526  1168890 |  326022    3393    13694     4.0 | 13.394 % |
c |      7487 |  440289  1161542 |  358624    5579    24360     4.4 | 13.960 % |
c |     11331 |  437912  1156091 |  394487    9137    70581     7.7 | 14.372 % |
c |     17097 |  437097  1154267 |  433936   14803   166363    11.2 | 14.515 % |
c |     25746 |  433324  1145809 |  477329   23001   274073    11.9 | 15.188 % |
c |     38720 |  429536  1137214 |  525062   35396   449377    12.7 | 15.858 % |
c |     58181 |  426242  1129719 |  577569   54447   727565    13.4 | 16.442 % |
c |     87373 |  422153  1120248 |  635326   83119  1083438    13.0 | 17.148 % |
c |    131162 |  420192  1115178 |  698858  125572  1640647    13.1 | 17.452 % |
c |    196846 |  417809  1109423 |  768744  190752  2542997    13.3 | 17.846 % |
#### 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.66 0.88 0.92 2/54 20786
Raw data (stat): 20786 (runsolver) R 20785 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540333563 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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+10.0001 s]
Raw data (loadavg): 0.71 0.89 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14328 0 0 0 960 39 0 0 25 0 1 0 540333563 66330624 13599 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16194 13599 603 41 0 16153 0
vsize: 64776
[startup+20.0018 s]
Raw data (loadavg): 0.75 0.89 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14329 0 0 0 1960 39 0 0 25 0 1 0 540333563 66330624 13600 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16194 13600 603 41 0 16153 0
vsize: 64776
[startup+30.0021 s]
Raw data (loadavg): 0.79 0.89 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14352 0 0 0 2960 40 0 0 25 0 1 0 540333563 66330624 13623 4294967295 134512640 134672761 3221224624 3221223820 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16194 13623 603 41 0 16153 0
vsize: 64776
[startup+40.0022 s]
Raw data (loadavg): 0.82 0.89 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14359 0 0 0 3959 40 0 0 25 0 1 0 540333563 66465792 13630 4294967295 134512640 134672761 3221224624 3221223796 134556609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16227 13630 603 41 0 16186 0
vsize: 64908
[startup+50.0067 s]
Raw data (loadavg): 0.85 0.90 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14365 0 0 0 4959 40 0 0 25 0 1 0 540333563 66465792 13636 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16227 13636 603 41 0 16186 0
vsize: 64908
[startup+60.0062 s]
Raw data (loadavg): 0.87 0.90 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14375 0 0 0 5959 41 0 0 25 0 1 0 540333563 66465792 13646 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16227 13646 603 41 0 16186 0
vsize: 64908
[startup+70.0063 s]
Raw data (loadavg): 0.89 0.90 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14389 0 0 0 6959 41 0 0 25 0 1 0 540333563 66465792 13660 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16227 13660 603 41 0 16186 0
vsize: 64908
[startup+80.0069 s]
Raw data (loadavg): 0.91 0.91 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14399 0 0 0 7958 41 0 0 25 0 1 0 540333563 66600960 13670 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16260 13670 603 41 0 16219 0
vsize: 65040
[startup+90.0062 s]
Raw data (loadavg): 0.92 0.91 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14407 0 0 0 8958 42 0 0 25 0 1 0 540333563 66600960 13678 4294967295 134512640 134672761 3221224624 3221223840 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16260 13678 603 41 0 16219 0
vsize: 65040
[startup+100.007 s]
Raw data (loadavg): 0.93 0.91 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14422 0 0 0 9958 42 0 0 25 0 1 0 540333563 66600960 13693 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16260 13693 603 41 0 16219 0
vsize: 65040
[startup+110.008 s]
Raw data (loadavg): 0.94 0.91 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14428 0 0 0 10957 43 0 0 25 0 1 0 540333563 66600960 13699 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16260 13699 603 41 0 16219 0
vsize: 65040
[startup+120.008 s]
Raw data (loadavg): 0.95 0.92 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14442 0 0 0 11957 43 0 0 25 0 1 0 540333563 66732032 13713 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16292 13713 603 41 0 16251 0
vsize: 65168
[startup+130.008 s]
Raw data (loadavg): 0.96 0.92 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14465 0 0 0 12957 43 0 0 25 0 1 0 540333563 66732032 13736 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16292 13736 603 41 0 16251 0
vsize: 65168
[startup+140.008 s]
Raw data (loadavg): 0.96 0.92 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14470 0 0 0 13957 43 0 0 25 0 1 0 540333563 66732032 13741 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16292 13741 603 41 0 16251 0
vsize: 65168
[startup+150.008 s]
Raw data (loadavg): 0.97 0.92 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14475 0 0 0 14957 44 0 0 25 0 1 0 540333563 66732032 13746 4294967295 134512640 134672761 3221224624 3221223728 134555357 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16292 13746 603 41 0 16251 0
vsize: 65168
[startup+160.009 s]
Raw data (loadavg): 0.97 0.92 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14478 0 0 0 15957 44 0 0 25 0 1 0 540333563 66732032 13749 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16292 13749 603 41 0 16251 0
vsize: 65168
[startup+170.008 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14482 0 0 0 16957 44 0 0 25 0 1 0 540333563 66867200 13753 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16325 13753 603 41 0 16284 0
vsize: 65300
[startup+180.008 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14495 0 0 0 17957 45 0 0 25 0 1 0 540333563 66867200 13766 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16325 13766 603 41 0 16284 0
vsize: 65300
[startup+190.008 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14504 0 0 0 18957 45 0 0 25 0 1 0 540333563 66867200 13775 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16325 13775 603 41 0 16284 0
vsize: 65300
[startup+200.009 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14518 0 0 0 19957 45 0 0 25 0 1 0 540333563 66867200 13789 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16325 13789 603 41 0 16284 0
vsize: 65300
[startup+210.009 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14522 0 0 0 20957 45 0 0 25 0 1 0 540333563 67002368 13793 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16358 13793 603 41 0 16317 0
vsize: 65432
[startup+220.01 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14551 0 0 0 21956 45 0 0 25 0 1 0 540333563 67002368 13822 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16358 13822 603 41 0 16317 0
vsize: 65432
[startup+230.01 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14581 0 0 0 22956 46 0 0 25 0 1 0 540333563 67137536 13852 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16391 13852 603 41 0 16350 0
vsize: 65564
[startup+240.01 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14586 0 0 0 23956 46 0 0 25 0 1 0 540333563 67137536 13857 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16391 13857 603 41 0 16350 0
vsize: 65564
[startup+250.011 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14604 0 0 0 24956 47 0 0 25 0 1 0 540333563 67330048 13875 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16438 13875 603 41 0 16397 0
vsize: 65752
[startup+260.011 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14619 0 0 0 25955 47 0 0 25 0 1 0 540333563 67330048 13890 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16438 13890 603 41 0 16397 0
vsize: 65752
[startup+270.011 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14753 0 0 0 26954 48 0 0 25 0 1 0 540333563 67870720 14024 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16570 14024 603 41 0 16529 0
vsize: 66280
[startup+280.012 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14770 0 0 0 27954 48 0 0 25 0 1 0 540333563 67870720 14041 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16570 14041 603 41 0 16529 0
vsize: 66280
[startup+290.013 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14775 0 0 0 28954 49 0 0 25 0 1 0 540333563 67870720 14046 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16570 14046 603 41 0 16529 0
vsize: 66280
[startup+300.013 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14803 0 0 0 29954 49 0 0 25 0 1 0 540333563 68157440 14074 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16640 14074 603 41 0 16599 0
vsize: 66560
[startup+310.014 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14804 0 0 0 30954 49 0 0 25 0 1 0 540333563 68157440 14075 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16640 14075 603 41 0 16599 0
vsize: 66560
[startup+320.013 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14867 0 0 0 31953 50 0 0 25 0 1 0 540333563 68292608 14138 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16673 14138 603 41 0 16632 0
vsize: 66692
[startup+330.014 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14878 0 0 0 32953 50 0 0 25 0 1 0 540333563 68427776 14149 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16706 14149 603 41 0 16665 0
vsize: 66824
[startup+340.014 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14900 0 0 0 33953 51 0 0 25 0 1 0 540333563 68427776 14171 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16706 14171 603 41 0 16665 0
vsize: 66824
[startup+350.015 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14941 0 0 0 34952 52 0 0 25 0 1 0 540333563 68689920 14212 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16770 14212 603 41 0 16729 0
vsize: 67080
[startup+360.015 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 14964 0 0 0 35952 52 0 0 25 0 1 0 540333563 68689920 14235 4294967295 134512640 134672761 3221224624 3221223832 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16770 14235 603 41 0 16729 0
vsize: 67080
[startup+370.015 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15019 0 0 0 36951 53 0 0 25 0 1 0 540333563 68956160 14290 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16835 14290 603 41 0 16794 0
vsize: 67340
[startup+380.015 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15023 0 0 0 37951 53 0 0 25 0 1 0 540333563 68956160 14294 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16835 14294 603 41 0 16794 0
vsize: 67340
[startup+390.015 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15030 0 0 0 38951 53 0 0 25 0 1 0 540333563 68956160 14301 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16835 14301 603 41 0 16794 0
vsize: 67340
[startup+400.016 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15079 0 0 0 39951 54 0 0 25 0 1 0 540333563 69226496 14350 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16901 14350 603 41 0 16860 0
vsize: 67604
[startup+410.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15173 0 0 0 40950 55 0 0 25 0 1 0 540333563 69496832 14444 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16967 14444 603 41 0 16926 0
vsize: 67868
[startup+420.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15211 0 0 0 41949 55 0 0 25 0 1 0 540333563 69758976 14482 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17031 14482 603 41 0 16990 0
vsize: 68124
[startup+430.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15212 0 0 0 42949 56 0 0 25 0 1 0 540333563 69758976 14483 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17031 14483 603 41 0 16990 0
vsize: 68124
[startup+440.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15241 0 0 0 43949 56 0 0 25 0 1 0 540333563 69906432 14512 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17067 14512 603 41 0 17026 0
vsize: 68268
[startup+450.018 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15347 0 0 0 44948 56 0 0 25 0 1 0 540333563 70307840 14618 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17165 14618 603 41 0 17124 0
vsize: 68660
[startup+460.018 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15406 0 0 0 45948 57 0 0 25 0 1 0 540333563 70582272 14677 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17232 14677 603 41 0 17191 0
vsize: 68928
[startup+470.018 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15420 0 0 0 46948 57 0 0 25 0 1 0 540333563 70582272 14691 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17232 14691 603 41 0 17191 0
vsize: 68928
[startup+480.019 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15443 0 0 0 47948 57 0 0 25 0 1 0 540333563 70717440 14714 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17265 14714 603 41 0 17224 0
vsize: 69060
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15476 0 0 0 48948 58 0 0 25 0 1 0 540333563 70856704 14747 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17299 14747 603 41 0 17258 0
vsize: 69196
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15591 0 0 0 49947 58 0 0 25 0 1 0 540333563 71286784 14862 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17404 14862 603 41 0 17363 0
vsize: 69616
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15608 0 0 0 50947 58 0 0 25 0 1 0 540333563 71421952 14879 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17437 14879 603 41 0 17396 0
vsize: 69748
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15628 0 0 0 51947 59 0 0 25 0 1 0 540333563 71421952 14899 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17437 14899 603 41 0 17396 0
vsize: 69748
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15638 0 0 0 52947 59 0 0 25 0 1 0 540333563 71421952 14909 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17437 14909 603 41 0 17396 0
vsize: 69748
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15661 0 0 0 53947 59 0 0 25 0 1 0 540333563 71557120 14932 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17470 14932 603 41 0 17429 0
vsize: 69880
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15722 0 0 0 54947 59 0 0 25 0 1 0 540333563 71827456 14993 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17536 14993 603 41 0 17495 0
vsize: 70144
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15734 0 0 0 55946 59 0 0 25 0 1 0 540333563 71827456 15005 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17536 15005 603 41 0 17495 0
vsize: 70144
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15748 0 0 0 56947 59 0 0 25 0 1 0 540333563 71962624 15019 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17569 15019 603 41 0 17528 0
vsize: 70276
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15800 0 0 0 57947 59 0 0 25 0 1 0 540333563 72097792 15071 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17602 15071 603 41 0 17561 0
vsize: 70408
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15859 0 0 0 58946 60 0 0 25 0 1 0 540333563 72380416 15130 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17671 15130 603 41 0 17630 0
vsize: 70684
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 15958 0 0 0 59946 60 0 0 25 0 1 0 540333563 72798208 15229 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17773 15229 603 41 0 17732 0
vsize: 71092
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16027 0 0 0 60946 61 0 0 25 0 1 0 540333563 73351168 15298 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17908 15298 603 41 0 17867 0
vsize: 71632
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16042 0 0 0 61946 61 0 0 25 0 1 0 540333563 73351168 15313 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17908 15313 603 41 0 17867 0
vsize: 71632
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16077 0 0 0 62946 61 0 0 25 0 1 0 540333563 73486336 15348 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17941 15348 603 41 0 17900 0
vsize: 71764
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16103 0 0 0 63946 61 0 0 25 0 1 0 540333563 73621504 15374 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17974 15374 603 41 0 17933 0
vsize: 71896
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16130 0 0 0 64947 61 0 0 25 0 1 0 540333563 73756672 15401 4294967295 134512640 134672761 3221224624 3221223840 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18007 15401 603 41 0 17966 0
vsize: 72028
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16175 0 0 0 65947 61 0 0 25 0 1 0 540333563 73891840 15446 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18040 15446 603 41 0 17999 0
vsize: 72160
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16191 0 0 0 66947 61 0 0 25 0 1 0 540333563 73891840 15462 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18040 15462 603 41 0 17999 0
vsize: 72160
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16239 0 0 0 67947 62 0 0 25 0 1 0 540333563 74162176 15510 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18106 15510 603 41 0 18065 0
vsize: 72424
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16264 0 0 0 68947 62 0 0 25 0 1 0 540333563 74293248 15535 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18138 15535 603 41 0 18097 0
vsize: 72552
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16313 0 0 0 69947 62 0 0 25 0 1 0 540333563 74428416 15584 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18171 15584 603 41 0 18130 0
vsize: 72684
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16334 0 0 0 70947 62 0 0 25 0 1 0 540333563 74428416 15605 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18171 15605 603 41 0 18130 0
vsize: 72684
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16344 0 0 0 71947 62 0 0 25 0 1 0 540333563 74563584 15615 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18204 15615 603 41 0 18163 0
vsize: 72816
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16380 0 0 0 72947 62 0 0 25 0 1 0 540333563 74694656 15651 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18236 15651 603 41 0 18195 0
vsize: 72944
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16445 0 0 0 73946 63 0 0 25 0 1 0 540333563 74960896 15716 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18301 15716 603 41 0 18260 0
vsize: 73204
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16478 0 0 0 74946 63 0 0 25 0 1 0 540333563 75096064 15749 4294967295 134512640 134672761 3221224624 3221223840 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18334 15749 603 41 0 18293 0
vsize: 73336
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16545 0 0 0 75946 63 0 0 25 0 1 0 540333563 75362304 15816 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18399 15816 603 41 0 18358 0
vsize: 73596
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16585 0 0 0 76946 63 0 0 25 0 1 0 540333563 75493376 15856 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18431 15856 603 41 0 18390 0
vsize: 73724
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16632 0 0 0 77946 64 0 0 25 0 1 0 540333563 75636736 15903 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18466 15903 603 41 0 18425 0
vsize: 73864
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16677 0 0 0 78946 64 0 0 25 0 1 0 540333563 75907072 15948 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18532 15948 603 41 0 18491 0
vsize: 74128
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16766 0 0 0 79946 64 0 0 25 0 1 0 540333563 76169216 16037 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18596 16037 603 41 0 18555 0
vsize: 74384
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16830 0 0 0 80946 64 0 0 25 0 1 0 540333563 76435456 16101 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18661 16101 603 41 0 18620 0
vsize: 74644
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16895 0 0 0 81946 65 0 0 25 0 1 0 540333563 76705792 16166 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18727 16166 603 41 0 18686 0
vsize: 74908
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 16959 0 0 0 82946 65 0 0 25 0 1 0 540333563 76976128 16230 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18793 16230 603 41 0 18752 0
vsize: 75172
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17043 0 0 0 83946 65 0 0 25 0 1 0 540333563 77295616 16314 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18871 16314 603 41 0 18830 0
vsize: 75484
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17104 0 0 0 84946 65 0 0 25 0 1 0 540333563 77565952 16375 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18937 16375 603 41 0 18896 0
vsize: 75748
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17175 0 0 0 85946 65 0 0 25 0 1 0 540333563 77836288 16446 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19003 16446 603 41 0 18962 0
vsize: 76012
[startup+870.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17281 0 0 0 86946 66 0 0 25 0 1 0 540333563 78241792 16552 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19102 16552 603 41 0 19061 0
vsize: 76408
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17325 0 0 0 87946 66 0 0 25 0 1 0 540333563 78372864 16596 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19134 16596 603 41 0 19093 0
vsize: 76536
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17368 0 0 0 88945 66 0 0 25 0 1 0 540333563 78508032 16639 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 16639 603 41 0 19126 0
vsize: 76668
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17394 0 0 0 89945 67 0 0 25 0 1 0 540333563 78639104 16665 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19199 16665 603 41 0 19158 0
vsize: 76796
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17462 0 0 0 90945 67 0 0 25 0 1 0 540333563 78909440 16733 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19265 16733 603 41 0 19224 0
vsize: 77060
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17514 0 0 0 91945 67 0 0 25 0 1 0 540333563 79568896 16785 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19426 16785 603 41 0 19385 0
vsize: 77704
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17690 0 0 0 92944 68 0 0 25 0 1 0 540333563 80375808 16961 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19623 16961 603 41 0 19582 0
vsize: 78492
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17799 0 0 0 93944 68 0 0 25 0 1 0 540333563 80777216 17070 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19721 17070 603 41 0 19680 0
vsize: 78884
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17873 0 0 0 94944 68 0 0 25 0 1 0 540333563 81043456 17144 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19786 17144 603 41 0 19745 0
vsize: 79144
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 17949 0 0 0 95944 68 0 0 25 0 1 0 540333563 81309696 17220 4294967295 134512640 134672761 3221224624 3221223840 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19851 17220 603 41 0 19810 0
vsize: 79404
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18022 0 0 0 96944 68 0 0 25 0 1 0 540333563 81575936 17293 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19916 17293 603 41 0 19875 0
vsize: 79664
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18101 0 0 0 97944 69 0 0 25 0 1 0 540333563 81973248 17372 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20013 17372 603 41 0 19972 0
vsize: 80052
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18162 0 0 0 98944 69 0 0 25 0 1 0 540333563 82108416 17433 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20046 17433 603 41 0 20005 0
vsize: 80184
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18210 0 0 0 99944 69 0 0 25 0 1 0 540333563 82374656 17481 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20111 17481 603 41 0 20070 0
vsize: 80444
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18259 0 0 0 100945 69 0 0 25 0 1 0 540333563 82505728 17530 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20143 17530 603 41 0 20102 0
vsize: 80572
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18309 0 0 0 101945 69 0 0 25 0 1 0 540333563 82776064 17580 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20209 17580 603 41 0 20168 0
vsize: 80836
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18356 0 0 0 102945 69 0 0 25 0 1 0 540333563 82911232 17627 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20242 17627 603 41 0 20201 0
vsize: 80968
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18405 0 0 0 103945 70 0 0 25 0 1 0 540333563 83181568 17676 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20308 17676 603 41 0 20267 0
vsize: 81232
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18464 0 0 0 104945 70 0 0 25 0 1 0 540333563 83316736 17735 4294967295 134512640 134672761 3221224624 3221223748 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20341 17735 603 41 0 20300 0
vsize: 81364
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18511 0 0 0 105944 70 0 0 25 0 1 0 540333563 83587072 17782 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20407 17782 603 41 0 20366 0
vsize: 81628
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18575 0 0 0 106944 70 0 0 25 0 1 0 540333563 83861504 17846 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20474 17846 603 41 0 20433 0
vsize: 81896
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18624 0 0 0 107944 71 0 0 25 0 1 0 540333563 83992576 17895 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20506 17895 603 41 0 20465 0
vsize: 82024
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18646 0 0 0 108944 71 0 0 25 0 1 0 540333563 84127744 17917 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20539 17917 603 41 0 20498 0
vsize: 82156
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18711 0 0 0 109945 71 0 0 25 0 1 0 540333563 84398080 17982 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20605 17982 603 41 0 20564 0
vsize: 82420
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18782 0 0 0 110945 71 0 0 25 0 1 0 540333563 84664320 18053 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20670 18053 603 41 0 20629 0
vsize: 82680
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18844 0 0 0 111945 71 0 0 25 0 1 0 540333563 84799488 18115 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20703 18115 603 41 0 20662 0
vsize: 82812
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18891 0 0 0 112945 72 0 0 25 0 1 0 540333563 85065728 18162 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20768 18162 603 41 0 20727 0
vsize: 83072
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 18966 0 0 0 113944 72 0 0 25 0 1 0 540333563 85331968 18237 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20833 18237 603 41 0 20792 0
vsize: 83332
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 19040 0 0 0 114943 72 0 0 25 0 1 0 540333563 85602304 18311 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20899 18311 603 41 0 20858 0
vsize: 83596
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 19081 0 0 0 115943 73 0 0 25 0 1 0 540333563 85737472 18352 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20932 18352 603 41 0 20891 0
vsize: 83728
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 19147 0 0 0 116943 73 0 0 25 0 1 0 540333563 86003712 18418 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20997 18418 603 41 0 20956 0
vsize: 83988
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 19191 0 0 0 117942 73 0 0 25 0 1 0 540333563 86138880 18462 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21030 18462 603 41 0 20989 0
vsize: 84120
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 19235 0 0 0 118942 74 0 0 25 0 1 0 540333563 86409216 18506 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21096 18506 603 41 0 21055 0
vsize: 84384
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20786
Raw data (stat): 20786 (minisat+) R 20785 28546 28545 0 -1 0 19284 0 0 0 119942 74 0 0 25 0 1 0 540333563 86544384 18555 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21129 18555 603 41 0 21088 0
vsize: 84516
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 20786
Raw data (stat): 20786 (minisat+) Z 20785 28546 28545 0 -1 12 19286 0 0 0 119942 78 0 0 25 0 1 0 540333563 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.08
CPU time (s): 1200.21
CPU user time (s): 1199.43
CPU system time (s): 0.781881
CPU usage (%): 100.011
Max. virtual memory (Kb): 84516
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####