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/MIPLIB/miplib2003/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM	2d8f46b77d84c45a7178d4a463744176
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.128979
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 18394

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 14:47:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18101 boxname=wulflinc10 idbench=1393 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  2d8f46b77d84c45a7178d4a463744176  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-tr12-30.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-tr12-30.opb
IDLAUNCH: 18101
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        790932 kB
Buffers:         10240 kB
Cached:         211576 kB
SwapCached:          0 kB
Active:          23552 kB
Inactive:       200792 kB
HighTotal:      131008 kB
HighFree:        34440 kB
LowTotal:       903652 kB
LowFree:        756492 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13848 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:07:40 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 18101 7 1200.28 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1108]---> BDD-cost:   71
c ---[1106]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1102]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1100]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1098]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1096]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1094]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1092]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1090]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1088]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1086]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1084]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1082]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1080]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1078]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1076]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1074]---> Sorter-cost:  445     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]---> BDD-cost:   52
c ---[1056]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1054]---> Sorter-cost:  433     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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1016]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1014]---> Sorter-cost:  445     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]---> BDD-cost:   65
c ---[ 990]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 988]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 986]---> BDD-cost:  166
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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 956]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost:  445     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]---> BDD-cost:   67
c ---[ 924]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 920]---> BDD-cost:  166
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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 896]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 894]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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]---> BDD-cost:  159
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]---> BDD-cost:   63
c ---[ 856]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 854]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 852]---> BDD-cost:  166
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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 836]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost:  445     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]---> BDD-cost:   71
c ---[ 790]---> BDD-cost:  159
c ---[ 788]---> Sorter-cost:  433     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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 776]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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]---> BDD-cost:   52
c ---[ 724]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> BDD-cost:  164
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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 716]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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:  433     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:   71
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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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]---> BDD-cost:   67
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:  419     Base: 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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 596]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 594]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> BDD-cost:   52
c ---[ 590]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> BDD-cost:  166
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]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 536]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 527]---> BDD-cost:   28
c ---[ 526]---> BDD-cost:   28
c ---[ 525]---> BDD-cost:   28
c ---[ 524]---> BDD-cost:   28
c ---[ 523]---> BDD-cost:   28
c ---[ 522]---> BDD-cost:   28
c ---[ 521]---> BDD-cost:   28
c ---[ 520]---> BDD-cost:   28
c ---[ 519]---> BDD-cost:   28
c ---[ 517]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> BDD-cost:   28
c ---[ 515]---> BDD-cost:   28
c ---[ 514]---> BDD-cost:   28
c ---[ 513]---> BDD-cost:   28
c ---[ 512]---> BDD-cost:   28
c ---[ 511]---> BDD-cost:   28
c ---[ 510]---> BDD-cost:   28
c ---[ 509]---> BDD-cost:   28
c ---[ 508]---> BDD-cost:   28
c ---[ 507]---> BDD-cost:   28
c ---[ 505]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> BDD-cost:   28
c ---[ 503]---> BDD-cost:   28
c ---[ 502]---> BDD-cost:   28
c ---[ 501]---> BDD-cost:   28
c ---[ 500]---> BDD-cost:   28
c ---[ 499]---> BDD-cost:   28
c ---[ 498]---> BDD-cost:   28
c ---[ 497]---> BDD-cost:   28
c ---[ 496]---> BDD-cost:   28
c ---[ 495]---> BDD-cost:   28
c ---[ 493]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> BDD-cost:   28
c ---[ 491]---> BDD-cost:   27
c ---[ 490]---> BDD-cost:   27
c ---[ 489]---> BDD-cost:   27
c ---[ 488]---> BDD-cost:   27
c ---[ 487]---> BDD-cost:   27
c ---[ 486]---> BDD-cost:   27
c ---[ 485]---> BDD-cost:   27
c ---[ 484]---> BDD-cost:   27
c ---[ 483]---> BDD-cost:   27
c ---[ 481]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> 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:   27
c ---[ 477]---> BDD-cost:   27
c ---[ 476]---> BDD-cost:   27
c ---[ 475]---> BDD-cost:   27
c ---[ 474]---> BDD-cost:   27
c ---[ 473]---> BDD-cost:   27
c ---[ 472]---> BDD-cost:   27
c ---[ 471]---> BDD-cost:   27
c ---[ 470]---> BDD-cost:   27
c ---[ 469]---> BDD-cost:   27
c ---[ 467]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> BDD-cost:   27
c ---[ 465]---> BDD-cost:   27
c ---[ 464]---> BDD-cost:   27
c ---[ 463]---> BDD-cost:   27
c ---[ 462]---> BDD-cost:   27
c ---[ 461]---> BDD-cost:   27
c ---[ 460]---> BDD-cost:   27
c ---[ 459]---> BDD-cost:   27
c ---[ 458]---> BDD-cost:   27
c ---[ 457]---> BDD-cost:   27
c ---[ 455]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> BDD-cost:   27
c ---[ 453]---> BDD-cost:   25
c ---[ 452]---> BDD-cost:   25
c ---[ 451]---> BDD-cost:   25
c ---[ 450]---> BDD-cost:   25
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> BDD-cost:   25
c ---[ 447]---> BDD-cost:   25
c ---[ 446]---> BDD-cost:   25
c ---[ 445]---> BDD-cost:   25
c ---[ 443]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> BDD-cost:   25
c ---[ 441]---> BDD-cost:   25
c ---[ 440]---> BDD-cost:   25
c ---[ 439]---> BDD-cost:   25
c ---[ 438]---> BDD-cost:   25
c ---[ 437]---> BDD-cost:   25
c ---[ 436]---> BDD-cost:   25
c ---[ 435]---> BDD-cost:   25
c ---[ 434]---> BDD-cost:   25
c ---[ 433]---> BDD-cost:   25
c ---[ 431]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> BDD-cost:   25
c ---[ 429]---> BDD-cost:   25
c ---[ 428]---> BDD-cost:   25
c ---[ 427]---> BDD-cost:   25
c ---[ 426]---> BDD-cost:   25
c ---[ 425]---> BDD-cost:   25
c ---[ 424]---> BDD-cost:   25
c ---[ 423]---> BDD-cost:   25
c ---[ 422]---> BDD-cost:   25
c ---[ 421]---> BDD-cost:   25
c ---[ 419]---> 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:   25
c ---[ 417]---> BDD-cost:   28
c ---[ 416]---> BDD-cost:   28
c ---[ 415]---> BDD-cost:   28
c ---[ 414]---> BDD-cost:   28
c ---[ 413]---> BDD-cost:   28
c ---[ 412]---> BDD-cost:   28
c ---[ 411]---> BDD-cost:   28
c ---[ 410]---> BDD-cost:   28
c ---[ 409]---> BDD-cost:   28
c ---[ 407]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> BDD-cost:   28
c ---[ 405]---> BDD-cost:   28
c ---[ 404]---> BDD-cost:   28
c ---[ 403]---> BDD-cost:   28
c ---[ 402]---> BDD-cost:   28
c ---[ 401]---> BDD-cost:   28
c ---[ 400]---> BDD-cost:   28
c ---[ 399]---> BDD-cost:   28
c ---[ 398]---> BDD-cost:   28
c ---[ 397]---> BDD-cost:   28
c ---[ 395]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   28
c ---[ 393]---> BDD-cost:   28
c ---[ 392]---> BDD-cost:   28
c ---[ 391]---> BDD-cost:   28
c ---[ 390]---> BDD-cost:   28
c ---[ 389]---> BDD-cost:   28
c ---[ 388]---> BDD-cost:   28
c ---[ 387]---> BDD-cost:   28
c ---[ 386]---> BDD-cost:   28
c ---[ 385]---> BDD-cost:   28
c ---[ 383]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> BDD-cost:   28
c ---[ 381]---> BDD-cost:   28
c ---[ 380]---> BDD-cost:   28
c ---[ 379]---> BDD-cost:   28
c ---[ 378]---> BDD-cost:   28
c ---[ 377]---> BDD-cost:   28
c ---[ 376]---> BDD-cost:   28
c ---[ 375]---> BDD-cost:   28
c ---[ 374]---> BDD-cost:   28
c ---[ 373]---> BDD-cost:   28
c ---[ 371]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> BDD-cost:   28
c ---[ 369]---> BDD-cost:   28
c ---[ 368]---> BDD-cost:   28
c ---[ 367]---> BDD-cost:   28
c ---[ 366]---> BDD-cost:   28
c ---[ 365]---> BDD-cost:   28
c ---[ 364]---> BDD-cost:   28
c ---[ 363]---> BDD-cost:   28
c ---[ 362]---> BDD-cost:   28
c ---[ 361]---> BDD-cost:   28
c ---[ 359]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 357]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 345]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 333]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:   28
c ---[ 331]---> BDD-cost:   28
c ---[ 330]---> BDD-cost:   28
c ---[ 329]---> BDD-cost:   28
c ---[ 328]---> BDD-cost:   28
c ---[ 327]---> BDD-cost:   28
c ---[ 326]---> BDD-cost:   28
c ---[ 325]---> BDD-cost:   28
c ---[ 324]---> BDD-cost:   28
c ---[ 323]---> BDD-cost:   28
c ---[ 321]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> BDD-cost:   28
c ---[ 319]---> BDD-cost:   28
c ---[ 318]---> BDD-cost:   28
c ---[ 317]---> BDD-cost:   28
c ---[ 316]---> BDD-cost:   28
c ---[ 315]---> BDD-cost:   28
c ---[ 314]---> BDD-cost:   28
c ---[ 313]---> BDD-cost:   28
c ---[ 312]---> BDD-cost:   28
c ---[ 311]---> BDD-cost:   28
c ---[ 309]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> BDD-cost:   28
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:   27
c ---[ 297]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> BDD-cost:   27
c ---[ 295]---> BDD-cost:   27
c ---[ 294]---> BDD-cost:   27
c ---[ 293]---> BDD-cost:   27
c ---[ 292]---> BDD-cost:   27
c ---[ 291]---> BDD-cost:   27
c ---[ 290]---> BDD-cost:   27
c ---[ 289]---> BDD-cost:   27
c ---[ 288]---> BDD-cost:   27
c ---[ 287]---> BDD-cost:   27
c ---[ 285]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> BDD-cost:   27
c ---[ 283]---> BDD-cost:   27
c ---[ 282]---> BDD-cost:   27
c ---[ 281]---> BDD-cost:   27
c ---[ 280]---> BDD-cost:   27
c ---[ 279]---> BDD-cost:   27
c ---[ 278]---> BDD-cost:   27
c ---[ 277]---> BDD-cost:   27
c ---[ 276]---> BDD-cost:   27
c ---[ 275]---> BDD-cost:   27
c ---[ 273]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> BDD-cost:   27
c ---[ 271]---> BDD-cost:   27
c ---[ 270]---> BDD-cost:   27
c ---[ 269]---> BDD-cost:   27
c ---[ 268]---> BDD-cost:   27
c ---[ 267]---> BDD-cost:   27
c ---[ 266]---> BDD-cost:   27
c ---[ 265]---> BDD-cost:   27
c ---[ 264]---> BDD-cost:   27
c ---[ 263]---> BDD-cost:   27
c ---[ 261]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> BDD-cost:   27
c ---[ 259]---> BDD-cost:   27
c ---[ 258]---> BDD-cost:   27
c ---[ 257]---> BDD-cost:   27
c ---[ 256]---> BDD-cost:   27
c ---[ 255]---> BDD-cost:   27
c ---[ 254]---> BDD-cost:   27
c ---[ 253]---> BDD-cost:   27
c ---[ 252]---> BDD-cost:   27
c ---[ 251]---> BDD-cost:   27
c ---[ 249]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> BDD-cost:   27
c ---[ 247]---> BDD-cost:   27
c ---[ 246]---> BDD-cost:   27
c ---[ 245]---> BDD-cost:   27
c ---[ 244]---> BDD-cost:   27
c ---[ 243]---> BDD-cost:   27
c ---[ 242]---> BDD-cost:   27
c ---[ 241]---> BDD-cost:   27
c ---[ 240]---> BDD-cost:   27
c ---[ 239]---> BDD-cost:   27
c ---[ 237]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 234]---> BDD-cost:   27
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 ---[ 223]---> BDD-cost:   52
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 ---[ 211]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 199]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   25
c ---[ 196]---> BDD-cost:   25
c ---[ 195]---> BDD-cost:   25
c ---[ 194]---> BDD-cost:   25
c ---[ 193]---> BDD-cost:   25
c ---[ 192]---> BDD-cost:   25
c ---[ 191]---> BDD-cost:   25
c ---[ 190]---> BDD-cost:   25
c ---[ 189]---> BDD-cost:   25
c ---[ 187]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> BDD-cost:   25
c ---[ 185]---> BDD-cost:   25
c ---[ 184]---> BDD-cost:   25
c ---[ 183]---> BDD-cost:   25
c ---[ 182]---> BDD-cost:   25
c ---[ 181]---> BDD-cost:   25
c ---[ 180]---> BDD-cost:   25
c ---[ 179]---> BDD-cost:   25
c ---[ 178]---> BDD-cost:   25
c ---[ 177]---> BDD-cost:   25
c ---[ 175]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> BDD-cost:   25
c ---[ 173]---> BDD-cost:   25
c ---[ 172]---> BDD-cost:   25
c ---[ 171]---> BDD-cost:   25
c ---[ 170]---> BDD-cost:   25
c ---[ 169]---> BDD-cost:   25
c ---[ 168]---> BDD-cost:   25
c ---[ 167]---> BDD-cost:   25
c ---[ 166]---> BDD-cost:   25
c ---[ 165]---> BDD-cost:   25
c ---[ 163]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> BDD-cost:   25
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 ---[ 151]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 139]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 127]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   25
c ---[ 124]---> BDD-cost:   25
c ---[ 123]---> BDD-cost:   25
c ---[ 122]---> BDD-cost:   25
c ---[ 121]---> BDD-cost:   25
c ---[ 120]---> BDD-cost:   25
c ---[ 119]---> BDD-cost:   25
c ---[ 118]---> BDD-cost:   25
c ---[ 117]---> BDD-cost:   25
c ---[ 115]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:   25
c ---[ 111]---> BDD-cost:   25
c ---[ 110]---> BDD-cost:   25
c ---[ 109]---> BDD-cost:   25
c ---[ 108]---> BDD-cost:   25
c ---[ 107]---> BDD-cost:   25
c ---[ 106]---> BDD-cost:   25
c ---[ 105]---> BDD-cost:   25
c ---[ 104]---> BDD-cost:   25
c ---[ 103]---> BDD-cost:   25
c ---[ 101]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> BDD-cost:   25
c ---[  99]---> BDD-cost:   25
c ---[  98]---> BDD-cost:   25
c ---[  97]---> BDD-cost:   25
c ---[  96]---> BDD-cost:   25
c ---[  95]---> BDD-cost:   25
c ---[  94]---> BDD-cost:   25
c ---[  93]---> BDD-cost:   25
c ---[  92]---> BDD-cost:   25
c ---[  91]---> BDD-cost:   25
c ---[  89]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> BDD-cost:   25
c ---[  87]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  86]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  85]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  84]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  83]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  82]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  81]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  80]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  79]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  77]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  75]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  74]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  73]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  72]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  71]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  70]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  69]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  68]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  67]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  65]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  63]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  62]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  61]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  60]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  59]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  58]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  57]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  56]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  55]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  50]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> BDD-cost:   71
c ---[  14]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> BDD-cost:  164
c ---[  10]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 |  455836  1196462 |  167301      48      156     3.2 | 11.194 % |
c |       250 |  455212  1195070 |  184031     120      379     3.2 | 11.307 % |
c |       475 |  454578  1193658 |  202434     263      814     3.1 | 11.423 % |
c |       812 |  453309  1190823 |  222677     448     1402     3.1 | 11.647 % |
c |      1318 |  452194  1188304 |  244945     825     2824     3.4 | 11.843 % |
c |      2078 |  450937  1185423 |  269440    1425     5233     3.7 | 12.062 % |
c |      3217 |  450426  1184224 |  296384    2487    10557     4.2 | 12.149 % |
c |      4925 |  448640  1180153 |  326022    3970    16534     4.2 | 12.462 % |
c |      7487 |  446282  1174844 |  358624    6246    30308     4.9 | 12.880 % |
c |     11334 |  442000  1165069 |  394487    9552    48645     5.1 | 13.629 % |
c |     17103 |  439405  1159133 |  433936   15016   121247     8.1 | 14.080 % |
c |     25753 |  436011  1151451 |  477329   23265   240011    10.3 | 14.683 % |
c |     38727 |  430170  1138294 |  525062   35187   403103    11.5 | 15.733 % |
c |     58188 |  423615  1123363 |  577569   53852   644156    12.0 | 16.883 % |
c |     87383 |  423157  1122330 |  635326   82987  1618669    19.5 | 16.963 % |
c |    131173 |  423116  1122201 |  698858  126768  2746373    21.7 | 16.968 % |
c |    196858 |  422900  1121648 |  768744  192341  5490223    28.5 | 17.003 % |
#### 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.80 0.94 0.93 2/54 930
Raw data (stat): 930 (runsolver) R 929 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487702995 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99936 s]
Raw data (loadavg): 0.83 0.94 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14266 0 0 0 962 36 0 0 25 0 1 0 487702995 65818624 13518 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16069 13518 603 41 0 16028 0
vsize: 64276
[startup+20.0004 s]
Raw data (loadavg): 0.85 0.94 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14275 0 0 0 1962 36 0 0 25 0 1 0 487702995 65818624 13527 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16069 13527 603 41 0 16028 0
vsize: 64276
[startup+30.0009 s]
Raw data (loadavg): 0.88 0.94 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14275 0 0 0 2962 36 0 0 25 0 1 0 487702995 65818624 13527 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16069 13527 603 41 0 16028 0
vsize: 64276
[startup+40.0011 s]
Raw data (loadavg): 0.89 0.94 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14275 0 0 0 3962 37 0 0 25 0 1 0 487702995 65818624 13527 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16069 13527 603 41 0 16028 0
vsize: 64276
[startup+50.002 s]
Raw data (loadavg): 0.91 0.94 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14284 0 0 0 4962 37 0 0 25 0 1 0 487702995 65818624 13536 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16069 13536 603 41 0 16028 0
vsize: 64276
[startup+60.0016 s]
Raw data (loadavg): 0.92 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14321 0 0 0 5961 38 0 0 25 0 1 0 487702995 65953792 13573 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16102 13573 603 41 0 16061 0
vsize: 64408
[startup+70.0018 s]
Raw data (loadavg): 0.93 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14373 0 0 0 6960 39 0 0 25 0 1 0 487702995 66088960 13625 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16135 13625 603 41 0 16094 0
vsize: 64540
[startup+80.0028 s]
Raw data (loadavg): 0.94 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14406 0 0 0 7960 39 0 0 25 0 1 0 487702995 66224128 13658 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16168 13658 603 41 0 16127 0
vsize: 64672
[startup+90.0033 s]
Raw data (loadavg): 0.95 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14443 0 0 0 8959 40 0 0 25 0 1 0 487702995 66359296 13695 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16201 13695 603 41 0 16160 0
vsize: 64804
[startup+100.003 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14467 0 0 0 9959 40 0 0 25 0 1 0 487702995 66359296 13719 4294967295 134512640 134672761 3221224624 3221223812 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16201 13719 603 41 0 16160 0
vsize: 64804
[startup+110.004 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14480 0 0 0 10959 40 0 0 25 0 1 0 487702995 66523136 13732 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16241 13732 603 41 0 16200 0
vsize: 64964
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14499 0 0 0 11958 41 0 0 25 0 1 0 487702995 66523136 13751 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16241 13751 603 41 0 16200 0
vsize: 64964
[startup+130.004 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14503 0 0 0 12958 42 0 0 25 0 1 0 487702995 66523136 13755 4294967295 134512640 134672761 3221224624 3221223796 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16241 13755 603 41 0 16200 0
vsize: 64964
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14508 0 0 0 13958 42 0 0 25 0 1 0 487702995 66523136 13760 4294967295 134512640 134672761 3221224624 3221223816 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16241 13760 603 41 0 16200 0
vsize: 64964
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14520 0 0 0 14957 42 0 0 25 0 1 0 487702995 66658304 13772 4294967295 134512640 134672761 3221224624 3221223760 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16274 13772 603 41 0 16233 0
vsize: 65096
[startup+160.005 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14523 0 0 0 15957 42 0 0 25 0 1 0 487702995 66658304 13775 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16274 13775 603 41 0 16233 0
vsize: 65096
[startup+170.005 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14528 0 0 0 16957 43 0 0 25 0 1 0 487702995 66658304 13780 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16274 13780 603 41 0 16233 0
vsize: 65096
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14545 0 0 0 17957 43 0 0 25 0 1 0 487702995 66658304 13797 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16274 13797 603 41 0 16233 0
vsize: 65096
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14547 0 0 0 18957 43 0 0 25 0 1 0 487702995 66658304 13799 4294967295 134512640 134672761 3221224624 3221223760 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16274 13799 603 41 0 16233 0
vsize: 65096
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14551 0 0 0 19958 43 0 0 25 0 1 0 487702995 66658304 13803 4294967295 134512640 134672761 3221224624 3221223796 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16274 13803 603 41 0 16233 0
vsize: 65096
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14557 0 0 0 20958 43 0 0 25 0 1 0 487702995 66793472 13809 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16307 13809 603 41 0 16266 0
vsize: 65228
[startup+220.018 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14563 0 0 0 21959 43 0 0 25 0 1 0 487702995 66793472 13815 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16307 13815 603 41 0 16266 0
vsize: 65228
[startup+230.018 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14571 0 0 0 22959 43 0 0 25 0 1 0 487702995 66793472 13823 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16307 13823 603 41 0 16266 0
vsize: 65228
[startup+240.019 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14617 0 0 0 23959 43 0 0 25 0 1 0 487702995 66928640 13869 4294967295 134512640 134672761 3221224624 3221223816 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16340 13869 603 41 0 16299 0
vsize: 65360
[startup+250.019 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14651 0 0 0 24959 43 0 0 25 0 1 0 487702995 67063808 13903 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16373 13903 603 41 0 16332 0
vsize: 65492
[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14702 0 0 0 25959 43 0 0 25 0 1 0 487702995 67330048 13954 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16438 13954 603 41 0 16397 0
vsize: 65752
[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14732 0 0 0 26959 43 0 0 25 0 1 0 487702995 67534848 13984 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16488 13984 603 41 0 16447 0
vsize: 65952
[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14733 0 0 0 27960 43 0 0 25 0 1 0 487702995 67534848 13985 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16488 13985 603 41 0 16447 0
vsize: 65952
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14799 0 0 0 28959 44 0 0 25 0 1 0 487702995 67670016 14051 4294967295 134512640 134672761 3221224624 3221223776 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 14051 603 41 0 16480 0
vsize: 66084
[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14846 0 0 0 29959 44 0 0 25 0 1 0 487702995 67940352 14098 4294967295 134512640 134672761 3221224624 3221223808 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16587 14098 603 41 0 16546 0
vsize: 66348
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14849 0 0 0 30959 44 0 0 25 0 1 0 487702995 67940352 14101 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16587 14101 603 41 0 16546 0
vsize: 66348
[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14867 0 0 0 31960 44 0 0 25 0 1 0 487702995 67940352 14119 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16587 14119 603 41 0 16546 0
vsize: 66348
[startup+330.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14887 0 0 0 32961 44 0 0 25 0 1 0 487702995 68075520 14139 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16620 14139 603 41 0 16579 0
vsize: 66480
[startup+340.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14910 0 0 0 33961 44 0 0 25 0 1 0 487702995 68210688 14162 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16653 14162 603 41 0 16612 0
vsize: 66612
[startup+350.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14926 0 0 0 34961 44 0 0 25 0 1 0 487702995 68210688 14178 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16653 14178 603 41 0 16612 0
vsize: 66612
[startup+360.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 14999 0 0 0 35962 45 0 0 25 0 1 0 487702995 68481024 14251 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16719 14251 603 41 0 16678 0
vsize: 66876
[startup+370.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15015 0 0 0 36963 45 0 0 25 0 1 0 487702995 68616192 14267 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16752 14267 603 41 0 16711 0
vsize: 67008
[startup+380.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15025 0 0 0 37963 45 0 0 25 0 1 0 487702995 68616192 14277 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16752 14277 603 41 0 16711 0
vsize: 67008
[startup+390.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15068 0 0 0 38963 45 0 0 25 0 1 0 487702995 68751360 14320 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16785 14320 603 41 0 16744 0
vsize: 67140
[startup+400.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15083 0 0 0 39963 45 0 0 25 0 1 0 487702995 68898816 14335 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16821 14335 603 41 0 16780 0
vsize: 67284
[startup+410.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15105 0 0 0 40963 45 0 0 25 0 1 0 487702995 68898816 14357 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16821 14357 603 41 0 16780 0
vsize: 67284
[startup+420.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15148 0 0 0 41963 45 0 0 25 0 1 0 487702995 69292032 14400 4294967295 134512640 134672761 3221224624 3221223840 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16917 14400 603 41 0 16876 0
vsize: 67668
[startup+430.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15150 0 0 0 42963 45 0 0 25 0 1 0 487702995 69292032 14402 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16917 14402 603 41 0 16876 0
vsize: 67668
[startup+440.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15160 0 0 0 43964 45 0 0 25 0 1 0 487702995 69292032 14412 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16917 14412 603 41 0 16876 0
vsize: 67668
[startup+450.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15165 0 0 0 44964 45 0 0 25 0 1 0 487702995 69292032 14417 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16917 14417 603 41 0 16876 0
vsize: 67668
[startup+460.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15176 0 0 0 45963 45 0 0 25 0 1 0 487702995 69292032 14428 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16917 14428 603 41 0 16876 0
vsize: 67668
[startup+470.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15194 0 0 0 46964 45 0 0 25 0 1 0 487702995 69427200 14446 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 14446 603 41 0 16909 0
vsize: 67800
[startup+480.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15205 0 0 0 47964 45 0 0 25 0 1 0 487702995 69427200 14457 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 14457 603 41 0 16909 0
vsize: 67800
[startup+490.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15248 0 0 0 48964 46 0 0 25 0 1 0 487702995 69562368 14500 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16983 14500 603 41 0 16942 0
vsize: 67932
[startup+500.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15275 0 0 0 49964 46 0 0 25 0 1 0 487702995 69697536 14527 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17016 14527 603 41 0 16975 0
vsize: 68064
[startup+510.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15293 0 0 0 50964 46 0 0 25 0 1 0 487702995 69832704 14545 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17049 14545 603 41 0 17008 0
vsize: 68196
[startup+520.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15321 0 0 0 51964 46 0 0 25 0 1 0 487702995 69967872 14573 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17082 14573 603 41 0 17041 0
vsize: 68328
[startup+530.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15350 0 0 0 52964 46 0 0 25 0 1 0 487702995 69967872 14602 4294967295 134512640 134672761 3221224624 3221223776 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17082 14602 603 41 0 17041 0
vsize: 68328
[startup+540.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15359 0 0 0 53964 46 0 0 25 0 1 0 487702995 70103040 14611 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17115 14611 603 41 0 17074 0
vsize: 68460
[startup+550.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15398 0 0 0 54964 46 0 0 25 0 1 0 487702995 70238208 14650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17148 14650 603 41 0 17107 0
vsize: 68592
[startup+560.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15449 0 0 0 55964 46 0 0 25 0 1 0 487702995 70373376 14701 4294967295 134512640 134672761 3221224624 3221223792 134561136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17181 14701 603 41 0 17140 0
vsize: 68724
[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15463 0 0 0 56965 46 0 0 25 0 1 0 487702995 70508544 14715 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17214 14715 603 41 0 17173 0
vsize: 68856
[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15472 0 0 0 57965 46 0 0 25 0 1 0 487702995 70508544 14724 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17214 14724 603 41 0 17173 0
vsize: 68856
[startup+590.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15484 0 0 0 58965 46 0 0 25 0 1 0 487702995 70508544 14736 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17214 14736 603 41 0 17173 0
vsize: 68856
[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15489 0 0 0 59965 46 0 0 25 0 1 0 487702995 70508544 14741 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17214 14741 603 41 0 17173 0
vsize: 68856
[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15514 0 0 0 60965 46 0 0 25 0 1 0 487702995 70643712 14766 4294967295 134512640 134672761 3221224624 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17247 14766 603 41 0 17206 0
vsize: 68988
[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15551 0 0 0 61966 46 0 0 25 0 1 0 487702995 70774784 14803 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 14803 603 41 0 17238 0
vsize: 69116
[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15590 0 0 0 62965 47 0 0 25 0 1 0 487702995 70909952 14842 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17312 14842 603 41 0 17271 0
vsize: 69248
[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15674 0 0 0 63965 47 0 0 25 0 1 0 487702995 71311360 14926 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17410 14926 603 41 0 17369 0
vsize: 69640
[startup+650.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 15872 0 0 0 64965 48 0 0 25 0 1 0 487702995 72130560 15124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17610 15124 603 41 0 17569 0
vsize: 70440
[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 16195 0 0 0 65964 49 0 0 25 0 1 0 487702995 73719808 15447 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17998 15447 603 41 0 17957 0
vsize: 71992
[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 16488 0 0 0 66963 50 0 0 25 0 1 0 487702995 74956800 15740 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18300 15740 603 41 0 18259 0
vsize: 73200
[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 16694 0 0 0 67963 50 0 0 25 0 1 0 487702995 75796480 15946 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18505 15946 603 41 0 18464 0
vsize: 74020
[startup+690.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 16849 0 0 0 68962 51 0 0 25 0 1 0 487702995 76333056 16101 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18636 16101 603 41 0 18595 0
vsize: 74544
[startup+700.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 17032 0 0 0 69961 52 0 0 25 0 1 0 487702995 77209600 16284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18850 16284 603 41 0 18809 0
vsize: 75400
[startup+710.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 17214 0 0 0 70960 53 0 0 25 0 1 0 487702995 77881344 16466 4294967295 134512640 134672761 3221224624 3221223804 134559056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19014 16466 603 41 0 18973 0
vsize: 76056
[startup+720.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 17362 0 0 0 71960 54 0 0 25 0 1 0 487702995 78426112 16614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19147 16614 603 41 0 19106 0
vsize: 76588
[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 17524 0 0 0 72960 54 0 0 25 0 1 0 487702995 79110144 16776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19314 16776 603 41 0 19273 0
vsize: 77256
[startup+740.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 930
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 17702 0 0 0 73960 55 0 0 25 0 1 0 487702995 79888384 16954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19504 16954 603 41 0 19463 0
vsize: 78016
[startup+750.06 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 983
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 17852 0 0 0 74958 57 0 0 25 0 1 0 487702995 80429056 17104 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19636 17104 603 41 0 19595 0
vsize: 78544
[startup+760.06 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 983
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 17998 0 0 0 75957 57 0 0 25 0 1 0 487702995 81092608 17250 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19798 17250 603 41 0 19757 0
vsize: 79192
[startup+770.06 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 983
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 18166 0 0 0 76957 58 0 0 25 0 1 0 487702995 81764352 17418 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19962 17418 603 41 0 19921 0
vsize: 79848
[startup+780.061 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 983
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 18267 0 0 0 77957 58 0 0 25 0 1 0 487702995 82210816 17519 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20071 17519 603 41 0 20030 0
vsize: 80284
[startup+790.062 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 983
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 18389 0 0 0 78957 59 0 0 25 0 1 0 487702995 82771968 17641 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20208 17641 603 41 0 20167 0
vsize: 80832
[startup+800.062 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 983
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 18555 0 0 0 79956 59 0 0 25 0 1 0 487702995 83464192 17807 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20377 17807 603 41 0 20336 0
vsize: 81508
[startup+810.062 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 983
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 19102 0 0 0 80955 60 0 0 25 0 1 0 487702995 86151168 18354 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 18354 603 41 0 20992 0
vsize: 84132
[startup+820.062 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 19207 0 0 0 81955 61 0 0 25 0 1 0 487702995 86700032 18459 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21167 18459 603 41 0 21126 0
vsize: 84668
[startup+830.062 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 19419 0 0 0 82954 61 0 0 25 0 1 0 487702995 87498752 18671 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21362 18671 603 41 0 21321 0
vsize: 85448
[startup+840.063 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 19541 0 0 0 83954 62 0 0 25 0 1 0 487702995 87904256 18793 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21461 18793 603 41 0 21420 0
vsize: 85844
[startup+850.063 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 19686 0 0 0 84953 62 0 0 25 0 1 0 487702995 88608768 18938 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21633 18938 603 41 0 21592 0
vsize: 86532
[startup+860.062 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 20098 0 0 0 85952 64 0 0 25 0 1 0 487702995 90214400 19350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22025 19350 603 41 0 21984 0
vsize: 88100
[startup+870.062 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 20465 0 0 0 86951 65 0 0 25 0 1 0 487702995 91693056 19717 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22386 19717 603 41 0 22345 0
vsize: 89544
[startup+880.062 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 20766 0 0 0 87951 66 0 0 25 0 1 0 487702995 92946432 20018 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22692 20018 603 41 0 22651 0
vsize: 90768
[startup+890.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21063 0 0 0 88950 66 0 0 25 0 1 0 487702995 94150656 20315 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22986 20315 603 41 0 22945 0
vsize: 91944
[startup+900.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21306 0 0 0 89949 68 0 0 25 0 1 0 487702995 95219712 20558 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23247 20558 603 41 0 23206 0
vsize: 92988
[startup+910.061 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21377 0 0 0 90949 68 0 0 25 0 1 0 487702995 95494144 20629 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23314 20629 603 41 0 23273 0
vsize: 93256
[startup+920.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21455 0 0 0 91949 68 0 0 25 0 1 0 487702995 95760384 20707 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23379 20707 603 41 0 23338 0
vsize: 93516
[startup+930.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21551 0 0 0 92949 68 0 0 25 0 1 0 487702995 96161792 20803 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23477 20803 603 41 0 23436 0
vsize: 93908
[startup+940.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21645 0 0 0 93949 68 0 0 25 0 1 0 487702995 96559104 20897 4294967295 134512640 134672761 3221224624 3221223728 134560171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23574 20897 603 41 0 23533 0
vsize: 94296
[startup+950.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21752 0 0 0 94949 69 0 0 25 0 1 0 487702995 97189888 21004 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23728 21004 603 41 0 23687 0
vsize: 94912
[startup+960.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21828 0 0 0 95949 69 0 0 25 0 1 0 487702995 97456128 21080 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23793 21080 603 41 0 23752 0
vsize: 95172
[startup+970.063 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 21909 0 0 0 96948 70 0 0 25 0 1 0 487702995 97722368 21161 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23858 21161 603 41 0 23817 0
vsize: 95432
[startup+980.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22003 0 0 0 97948 70 0 0 25 0 1 0 487702995 98140160 21255 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 21255 603 41 0 23919 0
vsize: 95840
[startup+990.063 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22088 0 0 0 98947 70 0 0 25 0 1 0 487702995 98549760 21340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24060 21340 603 41 0 24019 0
vsize: 96240
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22162 0 0 0 99948 70 0 0 25 0 1 0 487702995 98816000 21414 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24125 21414 603 41 0 24084 0
vsize: 96500
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22244 0 0 0 100947 71 0 0 25 0 1 0 487702995 99143680 21496 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24205 21496 603 41 0 24164 0
vsize: 96820
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22316 0 0 0 101948 71 0 0 25 0 1 0 487702995 99422208 21568 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24273 21568 603 41 0 24232 0
vsize: 97092
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22399 0 0 0 102947 71 0 0 25 0 1 0 487702995 99708928 21651 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24343 21651 603 41 0 24302 0
vsize: 97372
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22481 0 0 0 103947 71 0 0 25 0 1 0 487702995 99975168 21733 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24408 21733 603 41 0 24367 0
vsize: 97632
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22567 0 0 0 104947 72 0 0 25 0 1 0 487702995 100450304 21819 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24524 21819 603 41 0 24483 0
vsize: 98096
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22630 0 0 0 105947 72 0 0 25 0 1 0 487702995 100720640 21882 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24590 21882 603 41 0 24549 0
vsize: 98360
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22706 0 0 0 106948 72 0 0 25 0 1 0 487702995 100986880 21958 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24655 21958 603 41 0 24614 0
vsize: 98620
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22837 0 0 0 107947 72 0 0 25 0 1 0 487702995 101650432 22089 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24817 22089 603 41 0 24776 0
vsize: 99268
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 985
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22888 0 0 0 108947 73 0 0 25 0 1 0 487702995 101785600 22140 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24850 22140 603 41 0 24809 0
vsize: 99400
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 22958 0 0 0 109947 73 0 0 25 0 1 0 487702995 102051840 22210 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24915 22210 603 41 0 24874 0
vsize: 99660
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23021 0 0 0 110947 73 0 0 25 0 1 0 487702995 102346752 22273 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24987 22273 603 41 0 24946 0
vsize: 99948
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23152 0 0 0 111947 73 0 0 25 0 1 0 487702995 103063552 22404 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25162 22404 603 41 0 25121 0
vsize: 100648
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23201 0 0 0 112947 74 0 0 25 0 1 0 487702995 103194624 22453 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25194 22453 603 41 0 25153 0
vsize: 100776
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23315 0 0 0 113947 74 0 0 25 0 1 0 487702995 103788544 22567 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25339 22567 603 41 0 25298 0
vsize: 101356
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23406 0 0 0 114947 74 0 0 25 0 1 0 487702995 104091648 22658 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25413 22658 603 41 0 25372 0
vsize: 101652
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23490 0 0 0 115947 75 0 0 25 0 1 0 487702995 104488960 22742 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25510 22742 603 41 0 25469 0
vsize: 102040
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23578 0 0 0 116947 75 0 0 25 0 1 0 487702995 104759296 22830 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25576 22830 603 41 0 25535 0
vsize: 102304
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23655 0 0 0 117947 75 0 0 25 0 1 0 487702995 105164800 22907 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25675 22907 603 41 0 25634 0
vsize: 102700
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23753 0 0 0 118947 75 0 0 25 0 1 0 487702995 105562112 23005 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25772 23005 603 41 0 25731 0
vsize: 103088
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 987
Raw data (stat): 930 (minisat+) R 929 25347 25346 0 -1 0 23842 0 0 0 119947 75 0 0 25 0 1 0 487702995 105832448 23094 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25838 23094 603 41 0 25797 0
vsize: 103352
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 987
Raw data (stat): 930 (minisat+) Z 929 25347 25346 0 -1 12 23844 0 0 0 119947 80 0 0 25 0 1 0 487702995 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.11
CPU time (s): 1200.28
CPU user time (s): 1199.47
CPU system time (s): 0.802877
CPU usage (%): 100.014
Max. virtual memory (Kb): 103352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####