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 18385

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        567000 kB
Buffers:         33564 kB
Cached:         412720 kB
SwapCached:          0 kB
Active:         154088 kB
Inactive:       294992 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        566748 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            12872 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:04:39 (client local time) WITH STATUS 0 IN 1200.56 SECONDS
stats: 18107 7 1200.56 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  497986  1290313 |  149395       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/143286          
c   -- var.elim.:  2000/143286          
c   -- var.elim.:  3000/143286          
c   -- var.elim.:  4000/143286          
c   -- var.elim.:  5000/143286          
c   -- var.elim.:  6000/143286          
c   -- var.elim.:  7000/143286          
c   -- var.elim.:  8000/143286          
c   -- var.elim.:  9000/143286          
c   -- var.elim.:  10000/143286          
c   -- var.elim.:  11000/143286          
c   -- var.elim.:  12000/143286          
c   -- var.elim.:  13000/143286          
c   -- var.elim.:  14000/143286          
c   -- var.elim.:  15000/143286          
c   -- var.elim.:  16000/143286          
c   -- var.elim.:  17000/143286          
c   -- var.elim.:  18000/143286          
c   -- var.elim.:  19000/143286          
c   -- var.elim.:  20000/143286          
c   -- var.elim.:  21000/143286          
c   -- var.elim.:  22000/143286          
c   -- var.elim.:  23000/143286          
c   -- var.elim.:  24000/143286          
c   -- var.elim.:  25000/143286          
c   -- var.elim.:  26000/143286          
c   -- var.elim.:  27000/143286          
c   -- var.elim.:  28000/143286          
c   -- var.elim.:  29000/143286          
c   -- var.elim.:  30000/143286          
c   -- var.elim.:  31000/143286          
c   -- var.elim.:  32000/143286          
c   -- var.elim.:  33000/143286          
c   -- var.elim.:  34000/143286          
c   -- var.elim.:  35000/143286          
c   -- var.elim.:  36000/143286          
c   -- var.elim.:  37000/143286          
c   -- var.elim.:  38000/143286          
c   -- var.elim.:  39000/143286          
c   -- var.elim.:  40000/143286          
c   -- var.elim.:  41000/143286          
c   -- var.elim.:  42000/143286          
c   -- var.elim.:  43000/143286          
c   -- var.elim.:  44000/143286          
c   -- var.elim.:  45000/143286          
c   -- var.elim.:  46000/143286          
c   -- var.elim.:  47000/143286          
c   -- var.elim.:  48000/143286          
c   -- var.elim.:  49000/143286          
c   -- var.elim.:  50000/143286          
c   -- var.elim.:  51000/143286          
c   -- var.elim.:  52000/143286          
c   -- var.elim.:  53000/143286          
c   -- var.elim.:  54000/143286          
c   -- var.elim.:  55000/143286          
c   -- var.elim.:  56000/143286          
c   -- var.elim.:  57000/143286          
c   -- var.elim.:  58000/143286          
c   -- var.elim.:  59000/143286          
c   -- var.elim.:  60000/143286          
c   -- var.elim.:  61000/143286          
c   -- var.elim.:  62000/143286          
c   -- var.elim.:  63000/143286          
c   -- var.elim.:  64000/143286          
c   -- var.elim.:  65000/143286          
c   -- var.elim.:  66000/143286          
c   -- var.elim.:  67000/143286          
c   -- var.elim.:  68000/143286          
c   -- var.elim.:  69000/143286          
c   -- var.elim.:  70000/143286          
c   -- var.elim.:  71000/143286          
c   -- var.elim.:  72000/143286          
c   -- var.elim.:  73000/143286          
c   -- var.elim.:  74000/143286          
c   -- var.elim.:  75000/143286          
c   -- var.elim.:  76000/143286          
c   -- var.elim.:  77000/143286          
c   -- var.elim.:  78000/143286          
c   -- var.elim.:  79000/143286          
c   -- var.elim.:  80000/143286          
c   -- var.elim.:  81000/143286          
c   -- var.elim.:  82000/143286          
c   -- var.elim.:  83000/143286          
c   -- var.elim.:  84000/143286          
c   -- var.elim.:  85000/143286          
c   -- var.elim.:  86000/143286          
c   -- var.elim.:  87000/143286          
c   -- var.elim.:  88000/143286          
c   -- var.elim.:  89000/143286          
c   -- var.elim.:  90000/143286          
c   -- var.elim.:  91000/143286          
c   -- var.elim.:  92000/143286          
c   -- var.elim.:  93000/143286          
c   -- var.elim.:  94000/143286          
c   -- var.elim.:  95000/143286          
c   -- var.elim.:  96000/143286          
c   -- var.elim.:  97000/143286          
c   -- var.elim.:  98000/143286          
c   -- var.elim.:  99000/143286          
c   -- var.elim.:  100000/143286          
c   -- var.elim.:  101000/143286          
c   -- var.elim.:  102000/143286          
c   -- var.elim.:  103000/143286          
c   -- var.elim.:  104000/143286          
c   -- var.elim.:  105000/143286          
c   -- var.elim.:  106000/143286          
c   -- var.elim.:  107000/143286          
c   -- var.elim.:  108000/143286          
c   -- var.elim.:  109000/143286          
c   -- var.elim.:  110000/143286          
c   -- var.elim.:  111000/143286          
c   -- var.elim.:  112000/143286          
c   -- var.elim.:  113000/143286          
c   -- var.elim.:  114000/143286          
c   -- var.elim.:  115000/143286          
c   -- var.elim.:  116000/143286          
c   -- var.elim.:  117000/143286          
c   -- var.elim.:  118000/143286          
c   -- var.elim.:  119000/143286          
c   -- var.elim.:  120000/143286          
c   -- var.elim.:  121000/143286          
c   -- var.elim.:  122000/143286          
c   -- var.elim.:  123000/143286          
c   -- var.elim.:  124000/143286          
c   -- var.elim.:  125000/143286          
c   -- var.elim.:  126000/143286          
c   -- var.elim.:  127000/143286          
c   -- var.elim.:  128000/143286          
c   -- var.elim.:  129000/143286          
c   -- var.elim.:  130000/143286          
c   -- var.elim.:  131000/143286          
c   -- var.elim.:  132000/143286          
c   -- var.elim.:  133000/143286          
c   -- var.elim.:  134000/143286          
c   -- var.elim.:  135000/143286          
c   -- var.elim.:  136000/143286          
c   -- var.elim.:  137000/143286          
c   -- var.elim.:  138000/143286          
c   -- var.elim.:  139000/143286          
c   -- var.elim.:  140000/143286          
c   -- var.elim.:  141000/143286          
c   -- var.elim.:  142000/143286          
c   -- var.elim.:  143000/143286          
c   -- var.elim.:  143286/143286          
c   -- var.elim.:  1000/66222          
c   -- var.elim.:  2000/66222          
c   -- var.elim.:  3000/66222          
c   -- var.elim.:  4000/66222          
c   -- var.elim.:  5000/66222          
c   -- var.elim.:  6000/66222          
c   -- var.elim.:  7000/66222          
c   -- var.elim.:  8000/66222          
c   -- var.elim.:  9000/66222          
c   -- var.elim.:  10000/66222          
c   -- var.elim.:  11000/66222          
c   -- var.elim.:  12000/66222          
c   -- var.elim.:  13000/66222          
c   -- var.elim.:  14000/66222          
c   -- var.elim.:  15000/66222          
c   -- var.elim.:  16000/66222          
c   -- var.elim.:  17000/66222          
c   -- var.elim.:  18000/66222          
c   -- var.elim.:  19000/66222          
c   -- var.elim.:  20000/66222          
c   -- var.elim.:  21000/66222          
c   -- var.elim.:  22000/66222          
c   -- var.elim.:  23000/66222          
c   -- var.elim.:  24000/66222          
c   -- var.elim.:  25000/66222          
c   -- var.elim.:  26000/66222          
c   -- var.elim.:  27000/66222          
c   -- var.elim.:  28000/66222          
c   -- var.elim.:  29000/66222          
c   -- var.elim.:  30000/66222          
c   -- var.elim.:  31000/66222          
c   -- var.elim.:  32000/66222          
c   -- var.elim.:  33000/66222          
c   -- var.elim.:  34000/66222          
c   -- var.elim.:  35000/66222          
c   -- var.elim.:  36000/66222          
c   -- var.elim.:  37000/66222          
c   -- var.elim.:  38000/66222          
c   -- var.elim.:  39000/66222          
c   -- var.elim.:  40000/66222          
c   -- var.elim.:  41000/66222          
c   -- var.elim.:  42000/66222          
c   -- var.elim.:  43000/66222          
c   -- var.elim.:  44000/66222          
c   -- var.elim.:  45000/66222          
c   -- var.elim.:  46000/66222          
c   -- var.elim.:  47000/66222          
c   -- var.elim.:  48000/66222          
c   -- var.elim.:  49000/66222          
c   -- var.elim.:  50000/66222          
c   -- var.elim.:  51000/66222          
c   -- var.elim.:  52000/66222          
c   -- var.elim.:  53000/66222          
c   -- var.elim.:  54000/66222          
c   -- var.elim.:  55000/66222          
c   -- var.elim.:  56000/66222          
c   -- var.elim.:  57000/66222          
c   -- var.elim.:  58000/66222          
c   -- var.elim.:  59000/66222          
c   -- var.elim.:  60000/66222          
c   -- var.elim.:  61000/66222          
c   -- var.elim.:  62000/66222          
c   -- var.elim.:  63000/66222          
c   -- var.elim.:  64000/66222          
c   -- var.elim.:  65000/66222          
c   -- var.elim.:  66000/66222          
c   -- var.elim.:  66222/66222          
c   -- var.elim.:  1000/5139          
c   -- var.elim.:  2000/5139          
c   -- var.elim.:  3000/5139          
c   -- var.elim.:  4000/5139          
c   -- var.elim.:  5000/5139          
c   -- var.elim.:  5139/5139          
c   -- var.elim.:  1000/5780          
c   -- var.elim.:  2000/5780          
c   -- var.elim.:  3000/5780          
c   -- var.elim.:  4000/5780          
c   -- var.elim.:  5000/5780          
c   -- var.elim.:  5780/5780          
c   -- var.elim.:  1000/7158          
c   -- var.elim.:  2000/7158          
c   -- var.elim.:  3000/7158          
c   -- var.elim.:  4000/7158          
c   -- var.elim.:  5000/7158          
c   -- var.elim.:  6000/7158          
c   -- var.elim.:  7000/7158          
c   -- var.elim.:  7158/7158          
c   -- var.elim.:  1000/8196          
c   -- var.elim.:  2000/8196          
c   -- var.elim.:  3000/8196          
c   -- var.elim.:  4000/8196          
c   -- var.elim.:  5000/8196          
c   -- var.elim.:  6000/8196          
c   -- var.elim.:  7000/8196          
c   -- var.elim.:  8000/8196          
c   -- var.elim.:  8196/8196          
c   -- var.elim.:  1000/7425          
c   -- var.elim.:  2000/7425          
c   -- var.elim.:  3000/7425          
c   -- var.elim.:  4000/7425          
c   -- var.elim.:  5000/7425          
c   -- var.elim.:  6000/7425          
c   -- var.elim.:  7000/7425          
c   -- var.elim.:  7425/7425          
c   -- var.elim.:  1000/7271          
c   -- var.elim.:  2000/7271          
c   -- var.elim.:  3000/7271          
c   -- var.elim.:  4000/7271          
c   -- var.elim.:  5000/7271          
c   -- var.elim.:  6000/7271          
c   -- var.elim.:  7000/7271          
c   -- var.elim.:  7271/7271          
c   -- var.elim.:  1000/4492          
c   -- var.elim.:  2000/4492          
c   -- var.elim.:  3000/4492          
c   -- var.elim.:  4000/4492          
c   -- var.elim.:  4492/4492          
c   -- var.elim.:  1000/2385          
c   -- var.elim.:  2000/2385          
c   -- var.elim.:  2385/2385          
c   -- var.elim.:  1000/1155          
c   -- var.elim.:  1155/1155          
c   -- var.elim.:  549/549          
c   -- var.elim.:  220/220          
c   -- var.elim.:  40/40          
c   -- subsuming                       
c   -- var.elim.:  1000/41339          
c   -- var.elim.:  2000/41339          
c   -- var.elim.:  3000/41339          
c   -- var.elim.:  4000/41339          
c   -- var.elim.:  5000/41339          
c   -- var.elim.:  6000/41339          
c   -- var.elim.:  7000/41339          
c   -- var.elim.:  8000/41339          
c   -- var.elim.:  9000/41339          
c   -- var.elim.:  10000/41339          
c   -- var.elim.:  11000/41339          
c   -- var.elim.:  12000/41339          
c   -- var.elim.:  13000/41339          
c   -- var.elim.:  14000/41339          
c   -- var.elim.:  15000/41339          
c   -- var.elim.:  16000/41339          
c   -- var.elim.:  17000/41339          
c   -- var.elim.:  18000/41339          
c   -- var.elim.:  19000/41339          
c   -- var.elim.:  20000/41339          
c   -- var.elim.:  21000/41339          
c   -- var.elim.:  22000/41339          
c   -- var.elim.:  23000/41339          
c   -- var.elim.:  24000/41339          
c   -- var.elim.:  25000/41339          
c   -- var.elim.:  26000/41339          
c   -- var.elim.:  27000/41339          
c   -- var.elim.:  28000/41339          
c   -- var.elim.:  29000/41339          
c   -- var.elim.:  30000/41339          
c   -- var.elim.:  31000/41339          
c   -- var.elim.:  32000/41339          
c   -- var.elim.:  33000/41339          
c   -- var.elim.:  34000/41339          
c   -- var.elim.:  35000/41339          
c   -- var.elim.:  36000/41339          
c   -- var.elim.:  37000/41339          
c   -- var.elim.:  38000/41339          
c   -- var.elim.:  39000/41339          
c   -- var.elim.:  40000/41339          
c   -- var.elim.:  41000/41339          
c   -- var.elim.:  41339/41339          
c   -- var.elim.:  1000/30353          
c   -- var.elim.:  2000/30353          
c   -- var.elim.:  3000/30353          
c   -- var.elim.:  4000/30353          
c   -- var.elim.:  5000/30353          
c   -- var.elim.:  6000/30353          
c   -- var.elim.:  7000/30353          
c   -- var.elim.:  8000/30353          
c   -- var.elim.:  9000/30353          
c   -- var.elim.:  10000/30353          
c   -- var.elim.:  11000/30353          
c   -- var.elim.:  12000/30353          
c   -- var.elim.:  13000/30353          
c   -- var.elim.:  14000/30353          
c   -- var.elim.:  15000/30353          
c   -- var.elim.:  16000/30353          
c   -- var.elim.:  17000/30353          
c   -- var.elim.:  18000/30353          
c   -- var.elim.:  19000/30353          
c   -- var.elim.:  20000/30353          
c   -- var.elim.:  21000/30353          
c   -- var.elim.:  22000/30353          
c   -- var.elim.:  23000/30353          
c   -- var.elim.:  24000/30353          
c   -- var.elim.:  25000/30353          
c   -- var.elim.:  26000/30353          
c   -- var.elim.:  27000/30353          
c   -- var.elim.:  28000/30353          
c   -- var.elim.:  29000/30353          
c   -- var.elim.:  30000/30353          
c   -- var.elim.:  30353/30353          
c   -- subsuming                       
c   -- var.elim.:  1000/14452          
c   -- var.elim.:  2000/14452          
c   -- var.elim.:  3000/14452          
c   -- var.elim.:  4000/14452          
c   -- var.elim.:  5000/14452          
c   -- var.elim.:  6000/14452          
c   -- var.elim.:  7000/14452          
c   -- var.elim.:  8000/14452          
c   -- var.elim.:  9000/14452          
c   -- var.elim.:  10000/14452          
c   -- var.elim.:  11000/14452          
c   -- var.elim.:  12000/14452          
c   -- var.elim.:  13000/14452          
c   -- var.elim.:  14000/14452          
c   -- var.elim.:  14452/14452          
c |         0 |  296812   938543 |      --       0       --      -- |     --   | -159436/-246746
c |         0 |  296812   938543 |  118724       0        0     nan |  0.000 % |
c |       100 |  296794   938490 |  130589      99      354     3.6 | 27.380 % |
c |       250 |  296794   938490 |  143648     249      816     3.3 | 27.380 % |
c |       475 |  296772   938416 |  158001     472     1586     3.4 | 27.383 % |
c |       813 |  296772   938416 |  173801     810     3083     3.8 | 27.383 % |
c |      1319 |  296761   938379 |  191174    1315     5561     4.2 | 27.384 % |
c |      2078 |  296739   938305 |  210276    2072    10180     4.9 | 27.386 % |
c |      3217 |  296685   938122 |  231262    3205  #### 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): 1.13 1.04 0.94 2/54 4388
Raw data (stat): 4388 (runsolver) R 4387 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487674287 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0036 s]
Raw data (loadavg): 1.11 1.04 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 25933 0 0 0 931 68 0 0 25 0 1 0 487674287 115286016 24430 4294967295 134512640 134672761 3221224544 3221222720 134604488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28146 24430 603 41 0 28105 0
vsize: 112584
[startup+20.0107 s]
Raw data (loadavg): 1.09 1.04 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 26073 0 0 0 1913 85 0 0 25 0 1 0 487674287 115236864 24365 4294967295 134512640 134672761 3221224544 3221222552 1075349707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28134 24365 603 41 0 28093 0
vsize: 112536
[startup+30.0112 s]
Raw data (loadavg): 1.08 1.03 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 27794 0 0 0 2905 92 0 0 25 0 1 0 487674287 114188288 24287 4294967295 134512640 134672761 3221224544 3221223680 134614715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27878 24287 603 41 0 27837 0
vsize: 111512
[startup+40.0121 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 27794 0 0 0 3905 93 0 0 25 0 1 0 487674287 114188288 24287 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27878 24287 603 41 0 27837 0
vsize: 111512
[startup+50.0127 s]
Raw data (loadavg): 1.05 1.03 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 27795 0 0 0 4905 93 0 0 25 0 1 0 487674287 114188288 24288 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27878 24288 603 41 0 27837 0
vsize: 111512
[startup+60.0125 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 27795 0 0 0 5905 93 0 0 25 0 1 0 487674287 114188288 24288 4294967295 134512640 134672761 3221224544 3221223584 134612619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27878 24288 603 41 0 27837 0
vsize: 111512
[startup+70.0122 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 27865 0 0 0 6905 93 0 0 25 0 1 0 487674287 114737152 24358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28012 24358 603 41 0 27971 0
vsize: 112048
[startup+80.013 s]
Raw data (loadavg): 1.03 1.03 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 27935 0 0 0 7905 94 0 0 25 0 1 0 487674287 114880512 24428 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28047 24428 603 41 0 28006 0
vsize: 112188
[startup+90.0128 s]
Raw data (loadavg): 1.03 1.03 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 28040 0 0 0 8904 94 0 0 25 0 1 0 487674287 115318784 24533 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28154 24533 603 41 0 28113 0
vsize: 112616
[startup+100.014 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 28331 0 0 0 9904 95 0 0 25 0 1 0 487674287 116518912 24824 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28447 24824 603 41 0 28406 0
vsize: 113788
[startup+110.014 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 28581 0 0 0 10903 95 0 0 25 0 1 0 487674287 117604352 25074 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28712 25074 603 41 0 28671 0
vsize: 114848
[startup+120.014 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 28934 0 0 0 11902 97 0 0 25 0 1 0 487674287 119316480 25427 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29130 25427 603 41 0 29089 0
vsize: 116520
[startup+130.014 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 29184 0 0 0 12902 97 0 0 25 0 1 0 487674287 120250368 25677 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29358 25677 603 41 0 29317 0
vsize: 117432
[startup+140.015 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 29347 0 0 0 13902 98 0 0 25 0 1 0 487674287 120930304 25840 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29524 25840 603 41 0 29483 0
vsize: 118096
[startup+150.016 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 29557 0 0 0 14901 98 0 0 25 0 1 0 487674287 122003456 26050 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29786 26050 603 41 0 29745 0
vsize: 119144
[startup+160.016 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 29712 0 0 0 15901 99 0 0 25 0 1 0 487674287 122531840 26205 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29915 26205 603 41 0 29874 0
vsize: 119660
[startup+170.015 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 29915 0 0 0 16901 99 0 0 25 0 1 0 487674287 123457536 26408 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30141 26408 603 41 0 30100 0
vsize: 120564
[startup+180.016 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 30117 0 0 0 17900 100 0 0 25 0 1 0 487674287 124248064 26610 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30334 26610 603 41 0 30293 0
vsize: 121336
[startup+190.016 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 30258 0 0 0 18900 100 0 0 25 0 1 0 487674287 124792832 26751 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30467 26751 603 41 0 30426 0
vsize: 121868
[startup+200.017 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 30379 0 0 0 19900 101 0 0 25 0 1 0 487674287 125325312 26872 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30597 26872 603 41 0 30556 0
vsize: 122388
[startup+210.016 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 30528 0 0 0 20900 101 0 0 25 0 1 0 487674287 125853696 27021 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30726 27021 603 41 0 30685 0
vsize: 122904
[startup+220.017 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 30723 0 0 0 21899 101 0 0 25 0 1 0 487674287 126644224 27216 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30919 27216 603 41 0 30878 0
vsize: 123676
[startup+230.017 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 30887 0 0 0 22899 103 0 0 25 0 1 0 487674287 127303680 27380 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 27380 603 41 0 31039 0
vsize: 124320
[startup+240.017 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 31259 0 0 0 23897 104 0 0 25 0 1 0 487674287 128782336 27752 4294967295 134512640 134672761 3221224544 3221223584 134612771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31441 27752 603 41 0 31400 0
vsize: 125764
[startup+250.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 31424 0 0 0 24896 105 0 0 25 0 1 0 487674287 129449984 27917 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31604 27917 603 41 0 31563 0
vsize: 126416
[startup+260.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 31677 0 0 0 25896 106 0 0 25 0 1 0 487674287 130502656 28170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31861 28170 603 41 0 31820 0
vsize: 127444
[startup+270.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 31991 0 0 0 26894 107 0 0 25 0 1 0 487674287 131829760 28484 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32185 28484 603 41 0 32144 0
vsize: 128740
[startup+280.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 32435 0 0 0 27894 108 0 0 25 0 1 0 487674287 133545984 28928 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32604 28928 603 41 0 32563 0
vsize: 130416
[startup+290.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 33107 0 0 0 28892 110 0 0 25 0 1 0 487674287 136327168 29600 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33283 29600 603 41 0 33242 0
vsize: 133132
[startup+300.017 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 33241 0 0 0 29892 110 0 0 25 0 1 0 487674287 137392128 29734 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33543 29734 603 41 0 33502 0
vsize: 134172
[startup+310.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 33394 0 0 0 30891 111 0 0 25 0 1 0 487674287 138055680 29887 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33705 29887 603 41 0 33664 0
vsize: 134820
[startup+320.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 33558 0 0 0 31891 111 0 0 25 0 1 0 487674287 138715136 30051 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33866 30051 603 41 0 33825 0
vsize: 135464
[startup+330.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 33773 0 0 0 32891 112 0 0 25 0 1 0 487674287 139501568 30266 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34058 30266 603 41 0 34017 0
vsize: 136232
[startup+340.126 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 34036 0 0 0 33901 112 0 0 25 0 1 0 487674287 140562432 30529 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34317 30529 603 41 0 34276 0
vsize: 137268
[startup+350.125 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 34357 0 0 0 34900 114 0 0 25 0 1 0 487674287 141942784 30850 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34654 30850 603 41 0 34613 0
vsize: 138616
[startup+360.126 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 34746 0 0 0 35899 115 0 0 25 0 1 0 487674287 143527936 31239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35041 31239 603 41 0 35000 0
vsize: 140164
[startup+370.126 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 35273 0 0 0 36898 117 0 0 25 0 1 0 487674287 145645568 31766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35558 31766 603 41 0 35517 0
vsize: 142232
[startup+380.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 35752 0 0 0 37897 118 0 0 25 0 1 0 487674287 147640320 32245 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36045 32245 603 41 0 36004 0
vsize: 144180
[startup+390.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 36064 0 0 0 38896 119 0 0 25 0 1 0 487674287 148959232 32557 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36367 32557 603 41 0 36326 0
vsize: 145468
[startup+400.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 36241 0 0 0 39895 120 0 0 25 0 1 0 487674287 149618688 32734 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36528 32734 603 41 0 36487 0
vsize: 146112
[startup+410.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 36444 0 0 0 40895 120 0 0 25 0 1 0 487674287 150568960 32937 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36760 32937 603 41 0 36719 0
vsize: 147040
[startup+420.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 36970 0 0 0 41893 122 0 0 25 0 1 0 487674287 152690688 33463 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37278 33463 603 41 0 37237 0
vsize: 149112
[startup+430.128 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 37416 0 0 0 42892 124 0 0 25 0 1 0 487674287 154546176 33909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37731 33909 603 41 0 37690 0
vsize: 150924
[startup+440.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 37910 0 0 0 43891 125 0 0 25 0 1 0 487674287 156524544 34403 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38214 34403 603 41 0 38173 0
vsize: 152856
[startup+450.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 38266 0 0 0 44890 126 0 0 25 0 1 0 487674287 157974528 34759 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38568 34759 603 41 0 38527 0
vsize: 154272
[startup+460.128 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 38748 0 0 0 45889 127 0 0 25 0 1 0 487674287 159985664 35241 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39059 35241 603 41 0 39018 0
vsize: 156236
[startup+470.128 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 39139 0 0 0 46888 128 0 0 25 0 1 0 487674287 161591296 35632 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39451 35632 603 41 0 39410 0
vsize: 157804
[startup+480.128 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 39462 0 0 0 47888 129 0 0 25 0 1 0 487674287 162914304 35955 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39774 35955 603 41 0 39733 0
vsize: 159096
[startup+490.127 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 39826 0 0 0 48887 129 0 0 25 0 1 0 487674287 164388864 36319 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40134 36319 603 41 0 40093 0
vsize: 160536
[startup+500.142 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 40145 0 0 0 49888 130 0 0 25 0 1 0 487674287 165707776 36638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40456 36638 603 41 0 40415 0
vsize: 161824
[startup+510.148 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 40327 0 0 0 50888 130 0 0 25 0 1 0 487674287 166391808 36820 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40623 36820 603 41 0 40582 0
vsize: 162492
[startup+520.165 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 40500 0 0 0 51890 131 0 0 25 0 1 0 487674287 167063552 36993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40787 36993 603 41 0 40746 0
vsize: 163148
[startup+530.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 40693 0 0 0 52901 131 0 0 25 0 1 0 487674287 167858176 37186 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40981 37186 603 41 0 40940 0
vsize: 163924
[startup+540.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 40896 0 0 0 53900 132 0 0 25 0 1 0 487674287 168796160 37389 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41210 37389 603 41 0 41169 0
vsize: 164840
[startup+550.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 41097 0 0 0 54900 133 0 0 25 0 1 0 487674287 169594880 37590 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41405 37590 603 41 0 41364 0
vsize: 165620
[startup+560.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 41739 0 0 0 55898 135 0 0 25 0 1 0 487674287 172118016 38232 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42021 38232 603 41 0 41980 0
vsize: 168084
[startup+570.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 42080 0 0 0 56897 136 0 0 25 0 1 0 487674287 173584384 38573 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42379 38573 603 41 0 42338 0
vsize: 169516
[startup+580.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 42423 0 0 0 57897 136 0 0 25 0 1 0 487674287 174956544 38916 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42714 38916 603 41 0 42673 0
vsize: 170856
[startup+590.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 42678 0 0 0 58897 137 0 0 25 0 1 0 487674287 176021504 39171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42974 39171 603 41 0 42933 0
vsize: 171896
[startup+600.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 42798 0 0 0 59896 137 0 0 25 0 1 0 487674287 176427008 39291 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43073 39291 603 41 0 43032 0
vsize: 172292
[startup+610.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 42907 0 0 0 60896 138 0 0 25 0 1 0 487674287 176951296 39400 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43201 39400 603 41 0 43160 0
vsize: 172804
[startup+620.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43029 0 0 0 61896 138 0 0 25 0 1 0 487674287 177479680 39522 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43330 39522 603 41 0 43289 0
vsize: 173320
[startup+630.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43153 0 0 0 62895 139 0 0 25 0 1 0 487674287 178008064 39646 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43459 39646 603 41 0 43418 0
vsize: 173836
[startup+640.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43295 0 0 0 63895 139 0 0 25 0 1 0 487674287 178540544 39788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43589 39788 603 41 0 43548 0
vsize: 174356
[startup+650.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43457 0 0 0 64895 140 0 0 25 0 1 0 487674287 179331072 39950 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43782 39950 603 41 0 43741 0
vsize: 175128
[startup+660.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43567 0 0 0 65895 140 0 0 25 0 1 0 487674287 179916800 40060 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43925 40060 603 41 0 43884 0
vsize: 175700
[startup+670.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43678 0 0 0 66895 140 0 0 25 0 1 0 487674287 180326400 40171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44025 40171 603 41 0 43984 0
vsize: 176100
[startup+680.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43817 0 0 0 67894 141 0 0 25 0 1 0 487674287 180887552 40310 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44162 40310 603 41 0 44121 0
vsize: 176648
[startup+690.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 43960 0 0 0 68894 141 0 0 25 0 1 0 487674287 181420032 40453 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44292 40453 603 41 0 44251 0
vsize: 177168
[startup+700.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 44098 0 0 0 69894 141 0 0 25 0 1 0 487674287 182079488 40591 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44453 40591 603 41 0 44412 0
vsize: 177812
[startup+710.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 44256 0 0 0 70894 142 0 0 25 0 1 0 487674287 182669312 40749 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44597 40749 603 41 0 44556 0
vsize: 178388
[startup+720.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 44426 0 0 0 71894 142 0 0 25 0 1 0 487674287 183332864 40919 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44759 40919 603 41 0 44718 0
vsize: 179036
[startup+730.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 44586 0 0 0 72894 142 0 0 25 0 1 0 487674287 183996416 41079 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44921 41079 603 41 0 44880 0
vsize: 179684
[startup+740.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 44761 0 0 0 73893 143 0 0 25 0 1 0 487674287 184786944 41254 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45114 41254 603 41 0 45073 0
vsize: 180456
[startup+750.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 44920 0 0 0 74893 143 0 0 25 0 1 0 487674287 185454592 41413 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45277 41413 603 41 0 45236 0
vsize: 181108
[startup+760.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45042 0 0 0 75893 144 0 0 25 0 1 0 487674287 185880576 41535 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45381 41535 603 41 0 45340 0
vsize: 181524
[startup+770.281 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45164 0 0 0 76893 144 0 0 25 0 1 0 487674287 186404864 41657 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45509 41657 603 41 0 45468 0
vsize: 182036
[startup+780.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45282 0 0 0 77892 144 0 0 25 0 1 0 487674287 186933248 41775 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45638 41775 603 41 0 45597 0
vsize: 182552
[startup+790.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45440 0 0 0 78892 145 0 0 25 0 1 0 487674287 187584512 41933 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45797 41933 603 41 0 45756 0
vsize: 183188
[startup+800.282 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45601 0 0 0 79892 146 0 0 25 0 1 0 487674287 188334080 42094 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45980 42094 603 41 0 45939 0
vsize: 183920
[startup+810.283 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45718 0 0 0 80891 146 0 0 25 0 1 0 487674287 188862464 42211 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46109 42211 603 41 0 46068 0
vsize: 184436
[startup+820.283 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45840 0 0 0 81890 147 0 0 25 0 1 0 487674287 189259776 42333 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46206 42333 603 41 0 46165 0
vsize: 184824
[startup+830.283 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 45995 0 0 0 82890 148 0 0 25 0 1 0 487674287 189980672 42488 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46382 42488 603 41 0 46341 0
vsize: 185528
[startup+840.283 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 46103 0 0 0 83890 148 0 0 25 0 1 0 487674287 190504960 42596 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46510 42596 603 41 0 46469 0
vsize: 186040
[startup+850.283 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 46225 0 0 0 84890 148 0 0 25 0 1 0 487674287 190898176 42718 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46606 42718 603 41 0 46565 0
vsize: 186424
[startup+860.284 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 46366 0 0 0 85890 148 0 0 25 0 1 0 487674287 191557632 42859 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46767 42859 603 41 0 46726 0
vsize: 187068
[startup+870.283 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 46500 0 0 0 86890 148 0 0 25 0 1 0 487674287 192094208 42993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46898 42993 603 41 0 46857 0
vsize: 187592
[startup+880.284 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 46640 0 0 0 87890 149 0 0 25 0 1 0 487674287 193589248 43133 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47263 43133 603 41 0 47222 0
vsize: 189052
[startup+890.284 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 46765 0 0 0 88890 149 0 0 25 0 1 0 487674287 194252800 43258 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47425 43258 603 41 0 47384 0
vsize: 189700
[startup+900.284 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 46899 0 0 0 89889 150 0 0 25 0 1 0 487674287 194650112 43392 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47522 43392 603 41 0 47481 0
vsize: 190088
[startup+910.284 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47020 0 0 0 90889 150 0 0 25 0 1 0 487674287 195440640 43513 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47715 43513 603 41 0 47674 0
vsize: 190860
[startup+920.285 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 4388
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47132 0 0 0 91889 151 0 0 25 0 1 0 487674287 195854336 43625 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47816 43625 603 41 0 47775 0
vsize: 191264
[startup+930.286 s]
Raw data (loadavg): 1.00 1.00 0.94 3/57 4437
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47252 0 0 0 92888 151 0 0 25 0 1 0 487674287 196378624 43745 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47944 43745 603 41 0 47903 0
vsize: 191776
[startup+940.286 s]
Raw data (loadavg): 1.15 1.03 0.95 2/54 4441
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47368 0 0 0 93888 152 0 0 25 0 1 0 487674287 196919296 43861 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48076 43861 603 41 0 48035 0
vsize: 192304
[startup+950.286 s]
Raw data (loadavg): 1.12 1.03 0.95 2/54 4441
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47490 0 0 0 94887 153 0 0 25 0 1 0 487674287 197316608 43983 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48173 43983 603 41 0 48132 0
vsize: 192692
[startup+960.285 s]
Raw data (loadavg): 1.10 1.03 0.95 2/54 4441
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47602 0 0 0 95887 154 0 0 25 0 1 0 487674287 197885952 44095 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48312 44095 603 41 0 48271 0
vsize: 193248
[startup+970.285 s]
Raw data (loadavg): 1.09 1.03 0.95 2/54 4441
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47719 0 0 0 96886 155 0 0 25 0 1 0 487674287 198283264 44212 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48409 44212 603 41 0 48368 0
vsize: 193636
[startup+980.285 s]
Raw data (loadavg): 1.07 1.03 0.95 2/54 4441
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47845 0 0 0 97885 155 0 0 25 0 1 0 487674287 198815744 44338 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48539 44338 603 41 0 48498 0
vsize: 194156
[startup+990.286 s]
Raw data (loadavg): 1.06 1.03 0.95 2/54 4441
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 47983 0 0 0 98884 156 0 0 25 0 1 0 487674287 199340032 44476 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48667 44476 603 41 0 48626 0
vsize: 194668
[startup+1000.29 s]
Raw data (loadavg): 1.05 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48112 0 0 0 99884 157 0 0 25 0 1 0 487674287 199868416 44605 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48796 44605 603 41 0 48755 0
vsize: 195184
[startup+1010.29 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48254 0 0 0 100884 157 0 0 25 0 1 0 487674287 200540160 44747 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48960 44747 603 41 0 48919 0
vsize: 195840
[startup+1020.29 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48342 0 0 0 101883 158 0 0 25 0 1 0 487674287 200941568 44835 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49058 44835 603 41 0 49017 0
vsize: 196232
[startup+1030.28 s]
Raw data (loadavg): 1.03 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48462 0 0 0 102883 159 0 0 25 0 1 0 487674287 201469952 44955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49187 44955 603 41 0 49146 0
vsize: 196748
[startup+1040.29 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48574 0 0 0 103882 159 0 0 25 0 1 0 487674287 201867264 45067 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49284 45067 603 41 0 49243 0
vsize: 197136
[startup+1050.28 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48700 0 0 0 104881 160 0 0 25 0 1 0 487674287 202395648 45193 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49413 45193 603 41 0 49372 0
vsize: 197652
[startup+1060.29 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48823 0 0 0 105881 161 0 0 25 0 1 0 487674287 202919936 45316 4294967295 134512640 134672761 3221224544 3221223728 134615722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49541 45316 603 41 0 49500 0
vsize: 198164
[startup+1070.29 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 48927 0 0 0 106880 162 0 0 25 0 1 0 487674287 203329536 45420 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49641 45420 603 41 0 49600 0
vsize: 198564
[startup+1080.28 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49038 0 0 0 107880 162 0 0 25 0 1 0 487674287 203857920 45531 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49770 45531 603 41 0 49729 0
vsize: 199080
[startup+1090.29 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49165 0 0 0 108879 163 0 0 25 0 1 0 487674287 204382208 45658 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49898 45658 603 41 0 49857 0
vsize: 199592
[startup+1100.29 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49302 0 0 0 109879 163 0 0 25 0 1 0 487674287 204984320 45795 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50045 45795 603 41 0 50004 0
vsize: 200180
[startup+1110.29 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49417 0 0 0 110879 164 0 0 25 0 1 0 487674287 205508608 45910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50173 45910 603 41 0 50132 0
vsize: 200692
[startup+1120.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49534 0 0 0 111878 164 0 0 25 0 1 0 487674287 206041088 46027 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50303 46027 603 41 0 50262 0
vsize: 201212
[startup+1130.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49647 0 0 0 112878 165 0 0 25 0 1 0 487674287 206434304 46140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50399 46140 603 41 0 50358 0
vsize: 201596
[startup+1140.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49817 0 0 0 113877 166 0 0 25 0 1 0 487674287 207114240 46310 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50565 46310 603 41 0 50524 0
vsize: 202260
[startup+1150.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 49900 0 0 0 114877 166 0 0 25 0 1 0 487674287 207519744 46393 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50664 46393 603 41 0 50623 0
vsize: 202656
[startup+1160.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 50028 0 0 0 115877 167 0 0 25 0 1 0 487674287 208064512 46521 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50797 46521 603 41 0 50756 0
vsize: 203188
[startup+1170.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 50192 0 0 0 116876 168 0 0 25 0 1 0 487674287 208760832 46685 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50967 46685 603 41 0 50926 0
vsize: 203868
[startup+1180.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 50267 0 0 0 117876 168 0 0 25 0 1 0 487674287 209027072 46760 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51032 46760 603 41 0 50991 0
vsize: 204128
[startup+1190.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 50339 0 0 0 118875 169 0 0 25 0 1 0 487674287 209293312 46832 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51097 46832 603 41 0 51056 0
vsize: 204388
[startup+1200.29 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 4443
Raw data (stat): 4388 (minisat+) R 4387 32461 32460 0 -1 0 50409 0 0 0 119875 169 0 0 25 0 1 0 487674287 209555456 46902 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51161 46902 603 41 0 51120 0
vsize: 204644
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.39 s]
Raw data (loadavg): 1.00 1.01 0.95 1/54 4443
Raw data (stat): 4388 (minisat+) Z 4387 32461 32460 0 -1 12 50409 0 0 0 119875 180 0 0 25 0 1 0 487674287 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.39
CPU time (s): 1200.56
CPU user time (s): 1198.76
CPU system time (s): 1.80073
CPU usage (%): 100.014
Max. virtual memory (Kb): 204644
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####