PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        575444 kB
Buffers:         33632 kB
Cached:         381784 kB
SwapCached:       3532 kB
Active:          89504 kB
Inactive:       332388 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        575192 kB
SwapTotal:     2097892 kB
SwapFree:      2094360 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            31640 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:21:34 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 20291 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1109]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1108]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1107]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1106]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1105]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1104]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1103]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1102]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1101]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1100]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1099]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1098]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1097]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1096]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1095]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1094]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1093]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1092]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1091]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1090]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1089]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1088]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1087]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1086]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1085]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1084]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1083]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1082]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1081]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1080]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1078]---> BDD-cost:   71
c ---[1076]---> BDD-cost:  159
c ---[1074]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1072]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1070]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1068]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1066]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1064]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1062]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1060]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1058]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1056]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1054]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1052]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1050]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1048]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1046]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1044]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1042]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1040]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1038]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1036]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1034]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1032]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1030]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1028]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1026]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1024]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1020]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1018]---> BDD-cost:   67
c ---[1016]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1014]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1012]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1010]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1008]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1006]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1004]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1002]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1000]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 998]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 996]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 994]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 992]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 990]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 988]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 986]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 984]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 982]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 980]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 978]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 976]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 974]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 972]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 970]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 968]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 966]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 964]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 962]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 960]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 958]---> BDD-cost:   52
c ---[ 956]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 950]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 948]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 946]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 944]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 942]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 940]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 934]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 928]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 926]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 924]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 920]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 918]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 916]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 914]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 912]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 910]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 908]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 906]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 904]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 902]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 900]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 898]---> BDD-cost:   71
c ---[ 896]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 894]---> BDD-cost:  164
c ---[ 892]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 890]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 888]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 886]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 884]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 880]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 878]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 876]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 874]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 872]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 870]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 868]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 866]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 864]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 862]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 860]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 858]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 856]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 854]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 852]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 850]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 848]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 846]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 844]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 842]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 840]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 838]---> BDD-cost:   52
c ---[ 836]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 832]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 830]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 828]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 826]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 824]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 822]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 820]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 818]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 816]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 814]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 810]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 808]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 806]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 804]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 800]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 798]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 796]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 794]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 792]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 790]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 788]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> BDD-cost:   65
c ---[ 776]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> BDD-cost:  166
c ---[ 770]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 740]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 724]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 720]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> BDD-cost:   67
c ---[ 716]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> BDD-cost:  166
c ---[ 710]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 692]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 670]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 668]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> BDD-cost:   63
c ---[ 656]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> BDD-cost:  166
c ---[ 650]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 644]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 598]---> BDD-cost:   71
c ---[ 596]---> BDD-cost:  159
c ---[ 594]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> BDD-cost:   52
c ---[ 536]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> BDD-cost:  164
c ---[ 532]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> BDD-cost:   71
c ---[ 476]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> BDD-cost:   52
c ---[ 416]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> BDD-cost:  166
c ---[ 410]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 408]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> BDD-cost:   28
c ---[ 358]---> BDD-cost:   28
c ---[ 357]---> BDD-cost:   28
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   28
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   28
c ---[ 352]---> BDD-cost:   28
c ---[ 351]---> BDD-cost:   28
c ---[ 350]---> BDD-cost:   28
c ---[ 349]---> BDD-cost:   28
c ---[ 348]---> BDD-cost:   28
c ---[ 347]---> BDD-cost:   28
c ---[ 346]---> BDD-cost:   28
c ---[ 345]---> BDD-cost:   28
c ---[ 344]---> BDD-cost:   28
c ---[ 343]---> BDD-cost:   28
c ---[ 342]---> BDD-cost:   28
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:   28
c ---[ 339]---> BDD-cost:   28
c ---[ 338]---> BDD-cost:   28
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   28
c ---[ 335]---> BDD-cost:   28
c ---[ 334]---> BDD-cost:   28
c ---[ 333]---> BDD-cost:   28
c ---[ 332]---> BDD-cost:   28
c ---[ 331]---> BDD-cost:   28
c ---[ 330]---> BDD-cost:   28
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   27
c ---[ 327]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:   27
c ---[ 325]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   27
c ---[ 322]---> BDD-cost:   27
c ---[ 321]---> BDD-cost:   27
c ---[ 320]---> BDD-cost:   27
c ---[ 319]---> BDD-cost:   27
c ---[ 318]---> BDD-cost:   27
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   27
c ---[ 315]---> BDD-cost:   27
c ---[ 314]---> BDD-cost:   27
c ---[ 313]---> BDD-cost:   27
c ---[ 312]---> BDD-cost:   27
c ---[ 311]---> BDD-cost:   27
c ---[ 310]---> BDD-cost:   27
c ---[ 309]---> BDD-cost:   27
c ---[ 308]---> BDD-cost:   27
c ---[ 307]---> BDD-cost:   27
c ---[ 306]---> BDD-cost:   27
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   27
c ---[ 303]---> BDD-cost:   27
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   27
c ---[ 299]---> BDD-cost:   25
c ---[ 298]---> BDD-cost:   25
c ---[ 297]---> BDD-cost:   25
c ---[ 296]---> BDD-cost:   25
c ---[ 295]---> BDD-cost:   25
c ---[ 294]---> BDD-cost:   25
c ---[ 293]---> BDD-cost:   25
c ---[ 292]---> BDD-cost:   25
c ---[ 291]---> BDD-cost:   25
c ---[ 290]---> BDD-cost:   25
c ---[ 289]---> BDD-cost:   25
c ---[ 288]---> BDD-cost:   25
c ---[ 287]---> BDD-cost:   25
c ---[ 286]---> BDD-cost:   25
c ---[ 285]---> BDD-cost:   25
c ---[ 284]---> BDD-cost:   25
c ---[ 283]---> BDD-cost:   25
c ---[ 282]---> BDD-cost:   25
c ---[ 281]---> BDD-cost:   25
c ---[ 280]---> BDD-cost:   25
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   25
c ---[ 277]---> BDD-cost:   25
c ---[ 276]---> BDD-cost:   25
c ---[ 275]---> BDD-cost:   25
c ---[ 274]---> BDD-cost:   25
c ---[ 273]---> BDD-cost:   25
c ---[ 272]---> BDD-cost:   25
c ---[ 271]---> BDD-cost:   25
c ---[ 270]---> BDD-cost:   25
c ---[ 269]---> BDD-cost:   28
c ---[ 268]---> BDD-cost:   28
c ---[ 267]---> BDD-cost:   28
c ---[ 266]---> BDD-cost:   28
c ---[ 265]---> BDD-cost:   28
c ---[ 264]---> BDD-cost:   28
c ---[ 263]---> BDD-cost:   28
c ---[ 262]---> BDD-cost:   28
c ---[ 261]---> BDD-cost:   28
c ---[ 260]---> BDD-cost:   28
c ---[ 259]---> BDD-cost:   28
c ---[ 258]---> BDD-cost:   28
c ---[ 257]---> BDD-cost:   28
c ---[ 256]---> BDD-cost:   28
c ---[ 255]---> BDD-cost:   28
c ---[ 254]---> BDD-cost:   28
c ---[ 253]---> BDD-cost:   28
c ---[ 252]---> BDD-cost:   28
c ---[ 251]---> BDD-cost:   28
c ---[ 250]---> BDD-cost:   28
c ---[ 249]---> BDD-cost:   28
c ---[ 248]---> BDD-cost:   28
c ---[ 247]---> BDD-cost:   28
c ---[ 246]---> BDD-cost:   28
c ---[ 245]---> BDD-cost:   28
c ---[ 244]---> BDD-cost:   28
c ---[ 243]---> BDD-cost:   28
c ---[ 242]---> BDD-cost:   28
c ---[ 241]---> BDD-cost:   28
c ---[ 240]---> BDD-cost:   28
c ---[ 239]---> BDD-cost:   28
c ---[ 238]---> BDD-cost:   28
c ---[ 237]---> BDD-cost:   28
c ---[ 236]---> BDD-cost:   28
c ---[ 235]---> BDD-cost:   28
c ---[ 234]---> BDD-cost:   28
c ---[ 233]---> BDD-cost:   28
c ---[ 232]---> BDD-cost:   28
c ---[ 231]---> BDD-cost:   28
c ---[ 230]---> BDD-cost:   28
c ---[ 229]---> BDD-cost:   28
c ---[ 228]---> BDD-cost:   28
c ---[ 227]---> BDD-cost:   28
c ---[ 226]---> BDD-cost:   28
c ---[ 225]---> BDD-cost:   28
c ---[ 224]---> BDD-cost:   28
c ---[ 223]---> BDD-cost:   28
c ---[ 222]---> BDD-cost:   28
c ---[ 221]---> BDD-cost:   28
c ---[ 220]---> BDD-cost:   28
c ---[ 219]---> BDD-cost:   28
c ---[ 218]---> BDD-cost:   28
c ---[ 217]---> BDD-cost:   28
c ---[ 216]---> BDD-cost:   28
c ---[ 215]---> BDD-cost:   28
c ---[ 214]---> BDD-cost:   28
c ---[ 213]---> BDD-cost:   28
c ---[ 212]---> BDD-cost:   28
c ---[ 211]---> BDD-cost:   28
c ---[ 210]---> BDD-cost:   28
c ---[ 209]---> BDD-cost:   28
c ---[ 208]---> BDD-cost:   28
c ---[ 207]---> BDD-cost:   28
c ---[ 206]---> BDD-cost:   28
c ---[ 205]---> BDD-cost:   28
c ---[ 204]---> BDD-cost:   28
c ---[ 203]---> BDD-cost:   28
c ---[ 202]---> BDD-cost:   28
c ---[ 201]---> BDD-cost:   28
c ---[ 200]---> BDD-cost:   28
c ---[ 199]---> BDD-cost:   28
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   28
c ---[ 196]---> BDD-cost:   28
c ---[ 195]---> BDD-cost:   28
c ---[ 194]---> BDD-cost:   28
c ---[ 193]---> BDD-cost:   28
c ---[ 192]---> BDD-cost:   28
c ---[ 191]---> BDD-cost:   28
c ---[ 190]---> BDD-cost:   28
c ---[ 189]---> BDD-cost:   28
c ---[ 188]---> BDD-cost:   28
c ---[ 187]---> BDD-cost:   28
c ---[ 186]---> BDD-cost:   28
c ---[ 185]---> BDD-cost:   28
c ---[ 184]---> BDD-cost:   28
c ---[ 183]---> BDD-cost:   28
c ---[ 182]---> BDD-cost:   28
c ---[ 181]---> BDD-cost:   28
c ---[ 180]---> BDD-cost:   28
c ---[ 179]---> BDD-cost:   27
c ---[ 178]---> BDD-cost:   27
c ---[ 177]---> BDD-cost:   27
c ---[ 176]---> BDD-cost:   27
c ---[ 175]---> BDD-cost:   27
c ---[ 174]---> BDD-cost:   27
c ---[ 173]---> BDD-cost:   27
c ---[ 172]---> BDD-cost:   27
c ---[ 171]---> BDD-cost:   27
c ---[ 170]---> BDD-cost:   27
c ---[ 169]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:   27
c ---[ 167]---> BDD-cost:   27
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   27
c ---[ 164]---> BDD-cost:   27
c ---[ 163]---> BDD-cost:   27
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:   27
c ---[ 160]---> BDD-cost:   27
c ---[ 159]---> BDD-cost:   27
c ---[ 158]---> BDD-cost:   27
c ---[ 157]---> BDD-cost:   27
c ---[ 156]---> BDD-cost:   27
c ---[ 155]---> BDD-cost:   27
c ---[ 154]---> BDD-cost:   27
c ---[ 153]---> BDD-cost:   27
c ---[ 152]---> BDD-cost:   27
c ---[ 151]---> BDD-cost:   27
c ---[ 150]---> BDD-cost:   27
c ---[ 149]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   27
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   27
c ---[ 144]---> BDD-cost:   27
c ---[ 143]---> BDD-cost:   27
c ---[ 142]---> BDD-cost:   27
c ---[ 141]---> BDD-cost:   27
c ---[ 140]---> BDD-cost:   27
c ---[ 139]---> BDD-cost:   27
c ---[ 138]---> BDD-cost:   27
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   27
c ---[ 131]---> BDD-cost:   27
c ---[ 130]---> BDD-cost:   27
c ---[ 129]---> BDD-cost:   27
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   27
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   28
c ---[ 118]---> BDD-cost:   28
c ---[ 117]---> BDD-cost:   28
c ---[ 116]---> BDD-cost:   28
c ---[ 115]---> BDD-cost:   28
c ---[ 114]---> BDD-cost:   28
c ---[ 113]---> BDD-cost:   28
c ---[ 112]---> BDD-cost:   28
c ---[ 111]---> BDD-cost:   28
c ---[ 110]---> BDD-cost:   28
c ---[ 109]---> BDD-cost:   28
c ---[ 108]---> BDD-cost:   28
c ---[ 107]---> BDD-cost:   28
c ---[ 106]---> BDD-cost:   28
c ---[ 105]---> BDD-cost:   28
c ---[ 104]---> BDD-cost:   28
c ---[ 103]---> BDD-cost:   28
c ---[ 102]---> BDD-cost:   28
c ---[ 101]---> BDD-cost:   28
c ---[ 100]---> BDD-cost:   28
c ---[  99]---> BDD-cost:   28
c ---[  98]---> BDD-cost:   28
c ---[  97]---> BDD-cost:   28
c ---[  96]---> BDD-cost:   28
c ---[  95]---> BDD-cost:   28
c ---[  94]---> BDD-cost:   28
c ---[  93]---> BDD-cost:   28
c ---[  92]---> BDD-cost:   28
c ---[  91]---> BDD-cost:   28
c ---[  90]---> BDD-cost:   28
c ---[  89]---> BDD-cost:   25
c ---[  88]---> BDD-cost:   25
c ---[  87]---> BDD-cost:   25
c ---[  86]---> BDD-cost:   25
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   25
c ---[  83]---> BDD-cost:   25
c ---[  82]---> BDD-cost:   25
c ---[  81]---> BDD-cost:   25
c ---[  80]---> BDD-cost:   25
c ---[  79]---> BDD-cost:   25
c ---[  78]---> BDD-cost:   25
c ---[  77]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   25
c ---[  75]---> BDD-cost:   25
c ---[  74]---> BDD-cost:   25
c ---[  73]---> BDD-cost:   25
c ---[  72]---> BDD-cost:   25
c ---[  71]---> BDD-cost:   25
c ---[  70]---> BDD-cost:   25
c ---[  69]---> BDD-cost:   25
c ---[  68]---> BDD-cost:   25
c ---[  67]---> BDD-cost:   25
c ---[  66]---> BDD-cost:   25
c ---[  65]---> BDD-cost:   25
c ---[  64]---> BDD-cost:   25
c ---[  63]---> BDD-cost:   25
c ---[  62]---> BDD-cost:   25
c ---[  61]---> BDD-cost:   25
c ---[  60]---> BDD-cost:   25
c ---[  59]---> BDD-cost:   27
c ---[  58]---> BDD-cost:   27
c ---[  57]---> BDD-cost:   27
c ---[  56]---> BDD-cost:   27
c ---[  55]---> BDD-cost:   27
c ---[  54]---> BDD-cost:   27
c ---[  53]---> BDD-cost:   27
c ---[  52]---> BDD-cost:   27
c ---[  51]---> BDD-cost:   27
c ---[  50]---> BDD-cost:   27
c ---[  49]---> BDD-cost:   27
c ---[  48]---> BDD-cost:   27
c ---[  47]---> BDD-cost:   27
c ---[  46]---> BDD-cost:   27
c ---[  45]---> BDD-cost:   27
c ---[  44]---> BDD-cost:   27
c ---[  43]---> BDD-cost:   27
c ---[  42]---> BDD-cost:   27
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   27
c ---[  34]---> BDD-cost:   27
c ---[  33]---> BDD-cost:   27
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   25
c ---[  28]---> BDD-cost:   25
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   25
c ---[  25]---> BDD-cost:   25
c ---[  24]---> BDD-cost:   25
c ---[  23]---> BDD-cost:   25
c ---[  22]---> BDD-cost:   25
c ---[  21]---> BDD-cost:   25
c ---[  20]---> BDD-cost:   25
c ---[  19]---> BDD-cost:   25
c ---[  18]---> BDD-cost:   25
c ---[  17]---> BDD-cost:   25
c ---[  16]---> BDD-cost:   25
c ---[  15]---> BDD-cost:   25
c ---[  14]---> BDD-cost:   25
c ---[  13]---> BDD-cost:   25
c ---[  12]---> BDD-cost:   25
c ---[  11]---> BDD-cost:   25
c ---[  10]---> BDD-cost:   25
c ---[   9]---> BDD-cost:   25
c ---[   8]---> BDD-cost:   25
c ---[   7]---> BDD-cost:   25
c ---[   6]---> BDD-cost:   25
c ---[   5]---> BDD-cost:   25
c ---[   4]---> BDD-cost:   25
c ---[   3]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   25
c ---[   1]---> BDD-cost:   25
c ---[   0]---> BDD-cost:   25
c =================================[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/66217          
c   -- var.elim.:  2000/66217          
c   -- var.elim.:  3000/66217          
c   -- var.elim.:  4000/66217          
c   -- var.elim.:  5000/66217          
c   -- var.elim.:  6000/66217          
c   -- var.elim.:  7000/66217          
c   -- var.elim.:  8000/66217          
c   -- var.elim.:  9000/66217          
c   -- var.elim.:  10000/66217          
c   -- var.elim.:  11000/66217          
c   -- var.elim.:  12000/66217          
c   -- var.elim.:  13000/66217          
c   -- var.elim.:  14000/66217          
c   -- var.elim.:  15000/66217          
c   -- var.elim.:  16000/66217          
c   -- var.elim.:  17000/66217          
c   -- var.elim.:  18000/66217          
c   -- var.elim.:  19000/66217          
c   -- var.elim.:  20000/66217          
c   -- var.elim.:  21000/66217          
c   -- var.elim.:  22000/66217          
c   -- var.elim.:  23000/66217          
c   -- var.elim.:  24000/66217          
c   -- var.elim.:  25000/66217          
c   -- var.elim.:  26000/66217          
c   -- var.elim.:  27000/66217          
c   -- var.elim.:  28000/66217          
c   -- var.elim.:  29000/66217          
c   -- var.elim.:  30000/66217          
c   -- var.elim.:  31000/66217          
c   -- var.elim.:  32000/66217          
c   -- var.elim.:  33000/66217          
c   -- var.elim.:  34000/66217          
c   -- var.elim.:  35000/66217          
c   -- var.elim.:  36000/66217          
c   -- var.elim.:  37000/66217          
c   -- var.elim.:  38000/66217          
c   -- var.elim.:  39000/66217          
c   -- var.elim.:  40000/66217          
c   -- var.elim.:  41000/66217          
c   -- var.elim.:  42000/66217          
c   -- var.elim.:  43000/66217          
c   -- var.elim.:  44000/66217          
c   -- var.elim.:  45000/66217          
c   -- var.elim.:  46000/66217          
c   -- var.elim.:  47000/66217          
c   -- var.elim.:  48000/66217          
c   -- var.elim.:  49000/66217          
c   -- var.elim.:  50000/66217          
c   -- var.elim.:  51000/66217          
c   -- var.elim.:  52000/66217          
c   -- var.elim.:  53000/66217          
c   -- var.elim.:  54000/66217          
c   -- var.elim.:  55000/66217          
c   -- var.elim.:  56000/66217          
c   -- var.elim.:  57000/66217          
c   -- var.elim.:  58000/66217          
c   -- var.elim.:  59000/66217          
c   -- var.elim.:  60000/66217          
c   -- var.elim.:  61000/66217          
c   -- var.elim.:  62000/66217          
c   -- var.elim.:  63000/66217          
c   -- var.elim.:  64000/66217          
c   -- var.elim.:  65000/66217          
c   -- var.elim.:  66000/66217          
c   -- var.elim.:  66217/66217          
c   -- var.elim.:  1000/5142          
c   -- var.elim.:  2000/5142          
c   -- var.elim.:  3000/5142          
c   -- var.elim.:  4000/5142          
c   -- var.elim.:  5000/5142          
c   -- var.elim.:  5142/5142          
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/41326          
c   -- var.elim.:  2000/41326          
c   -- var.elim.:  3000/41326          
c   -- var.elim.:  4000/41326          
c   -- var.elim.:  5000/41326          
c   -- var.elim.:  6000/41326          
c   -- var.elim.:  7000/41326          
c   -- var.elim.:  8000/41326          
c   -- var.elim.:  9000/41326          
c   -- var.elim.:  10000/41326          
c   -- var.elim.:  11000/41326          
c   -- var.elim.:  12000/41326          
c   -- var.elim.:  13000/41326          
c   -- var.elim.:  14000/41326          
c   -- var.elim.:  15000/41326          
c   -- var.elim.:  16000/41326          
c   -- var.elim.:  17000/41326          
c   -- var.elim.:  18000/41326          
c   -- var.elim.:  19000/41326          
c   -- var.elim.:  20000/41326          
c   -- var.elim.:  21000/41326          
c   -- var.elim.:  22000/41326          
c   -- var.elim.:  23000/41326          
c   -- var.elim.:  24000/41326          
c   -- var.elim.:  25000/41326          
c   -- var.elim.:  26000/41326          
c   -- var.elim.:  27000/41326          
c   -- var.elim.:  28000/41326          
c   -- var.elim.:  29000/41326          
c   -- var.elim.:  30000/41326          
c   -- var.elim.:  31000/41326          
c   -- var.elim.:  32000/41326          
c   -- var.elim.:  33000/41326          
c   -- var.elim.:  34000/41326          
c   -- var.elim.:  35000/41326          
c   -- var.elim.:  36000/41326          
c   -- var.elim.:  37000/41326          
c   -- var.elim.:  38000/41326          
c   -- var.elim.:  39000/41326          
c   -- var.elim.:  40000/41326          
c   -- var.elim.:  41000/41326          
c   -- var.elim.:  41326/41326          
c   -- var.elim.:  1000/30340          
c   -- var.elim.:  2000/30340          
c   -- var.elim.:  3000/30340          
c   -- var.elim.:  4000/30340          
c   -- var.elim.:  5000/30340          
c   -- var.elim.:  6000/30340          
c   -- var.elim.:  7000/30340          
c   -- var.elim.:  8000/30340          
c   -- var.elim.:  9000/30340          
c   -- var.elim.:  10000/30340          
c   -- var.elim.:  11000/30340          
c   -- var.elim.:  12000/30340          
c   -- var.elim.:  13000/30340          
c   -- var.elim.:  14000/30340          
c   -- var.elim.:  15000/30340          
c   -- var.elim.:  16000/30340          
c   -- var.elim.:  17000/30340          
c   -- var.elim.:  18000/30340          
c   -- var.elim.:  19000/30340          
c   -- var.elim.:  20000/30340          
c   -- var.elim.:  21000/30340          
c   -- var.elim.:  22000/30340          
c   -- var.elim.:  23000/30340          
c   -- var.elim.:  24000/30340          
c   -- var.elim.:  25000/30340          
c   -- var.elim.:  26000/30340          
c   -- var.elim.:  27000/30340          
c   -- var.elim.:  28000/30340          
c   -- var.elim.:  29000/30340          
c   -- var.elim.:  30000/30340          
c   -- var.elim.:  30340/30340          
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 |  296783   938453 |  130584      98      320     3.3 | 27.381 % |
c |       250 |  296783   938453 |  143642     248      840     3.4 | 27.381 % |
c |       475 |  296783   938453 |  158007     473     1603     3.4 | 27.381 % |
c |       812 |  296772   938416 |  173801     809     2970     3.7 | 27.383 % |
c |      1318 |  296772   938416 |  191181    1315     5107     3.9 | 27.383 % |
c |      2078 |  296755   938365 |  210287    2074     9503     4.6 | 27.384 % |
c |      3217 |  296723   938250 |  231291    3212    15610     4.#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.91 2/54 5064
Raw data (stat): 5064 (runsolver) R 5063 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539876018 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.88 0.94 0.91 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 25656 0 0 0 932 66 0 0 25 0 1 0 539876018 116154368 24505 4294967295 134512640 134672761 3221224544 3221222544 134621186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28358 24505 603 41 0 28317 0
vsize: 113432
[startup+20.0003 s]
Raw data (loadavg): 1.05 0.98 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 25795 0 0 0 1917 81 0 0 25 0 1 0 539876018 116105216 24439 4294967295 134512640 134672761 3221224544 3221223312 134624165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28346 24439 603 41 0 28305 0
vsize: 113384
[startup+30.0016 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27512 0 0 0 2908 90 0 0 25 0 1 0 539876018 115056640 24357 4294967295 134512640 134672761 3221224544 3221223680 134614488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28090 24357 603 41 0 28049 0
vsize: 112360
[startup+40.0014 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27512 0 0 0 3907 90 0 0 25 0 1 0 539876018 115056640 24357 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24357 603 41 0 28049 0
vsize: 112360
[startup+50.0017 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27512 0 0 0 4908 90 0 0 25 0 1 0 539876018 115056640 24357 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24357 603 41 0 28049 0
vsize: 112360
[startup+60.0018 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27512 0 0 0 5908 90 0 0 25 0 1 0 539876018 115056640 24357 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24357 603 41 0 28049 0
vsize: 112360
[startup+70.0013 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27512 0 0 0 6908 90 0 0 25 0 1 0 539876018 115056640 24357 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24357 603 41 0 28049 0
vsize: 112360
[startup+80.0021 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27514 0 0 0 7908 90 0 0 25 0 1 0 539876018 115056640 24359 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24359 603 41 0 28049 0
vsize: 112360
[startup+90.0022 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27514 0 0 0 8908 90 0 0 25 0 1 0 539876018 115056640 24359 4294967295 134512640 134672761 3221224544 3221223712 134565029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24359 603 41 0 28049 0
vsize: 112360
[startup+100.003 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27514 0 0 0 9909 90 0 0 25 0 1 0 539876018 115056640 24359 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24359 603 41 0 28049 0
vsize: 112360
[startup+110.003 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27514 0 0 0 10909 90 0 0 25 0 1 0 539876018 115056640 24359 4294967295 134512640 134672761 3221224544 3221223712 134564499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24359 603 41 0 28049 0
vsize: 112360
[startup+120.004 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27515 0 0 0 11909 90 0 0 25 0 1 0 539876018 115056640 24360 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24360 603 41 0 28049 0
vsize: 112360
[startup+130.004 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27515 0 0 0 12909 90 0 0 25 0 1 0 539876018 115056640 24360 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 24360 603 41 0 28049 0
vsize: 112360
[startup+140.004 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27557 0 0 0 13909 90 0 0 25 0 1 0 539876018 115326976 24402 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28156 24402 603 41 0 28115 0
vsize: 112624
[startup+150.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27651 0 0 0 14909 90 0 0 25 0 1 0 539876018 115851264 24496 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28284 24496 603 41 0 28243 0
vsize: 113136
[startup+160.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 27821 0 0 0 15909 91 0 0 25 0 1 0 539876018 116523008 24666 4294967295 134512640 134672761 3221224544 3221223688 134616269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28448 24666 603 41 0 28407 0
vsize: 113792
[startup+170.004 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 28246 0 0 0 16908 92 0 0 25 0 1 0 539876018 118296576 25091 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28881 25091 603 41 0 28840 0
vsize: 115524
[startup+180.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 28514 0 0 0 17907 93 0 0 25 0 1 0 539876018 119427072 25359 4294967295 134512640 134672761 3221224544 3221223584 134612999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29157 25359 603 41 0 29116 0
vsize: 116628
[startup+190.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 28811 0 0 0 18907 94 0 0 25 0 1 0 539876018 120623104 25656 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29449 25656 603 41 0 29408 0
vsize: 117796
[startup+200.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 29185 0 0 0 19906 95 0 0 25 0 1 0 539876018 122208256 26030 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29836 26030 603 41 0 29795 0
vsize: 119344
[startup+210.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 29591 0 0 0 20905 95 0 0 25 0 1 0 539876018 123789312 26436 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30222 26436 603 41 0 30181 0
vsize: 120888
[startup+220.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 29944 0 0 0 21904 97 0 0 25 0 1 0 539876018 125263872 26789 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30582 26789 603 41 0 30541 0
vsize: 122328
[startup+230.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 30319 0 0 0 22902 99 0 0 25 0 1 0 539876018 126844928 27164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30968 27164 603 41 0 30927 0
vsize: 123872
[startup+240.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 30644 0 0 0 23902 100 0 0 25 0 1 0 539876018 128172032 27489 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31292 27489 603 41 0 31251 0
vsize: 125168
[startup+250.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 30884 0 0 0 24901 100 0 0 25 0 1 0 539876018 129097728 27729 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31518 27729 603 41 0 31477 0
vsize: 126072
[startup+260.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5064
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 31134 0 0 0 25900 101 0 0 25 0 1 0 539876018 130158592 27979 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31777 27979 603 41 0 31736 0
vsize: 127108
[startup+270.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 31384 0 0 0 26900 102 0 0 25 0 1 0 539876018 131211264 28229 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32034 28229 603 41 0 31993 0
vsize: 128136
[startup+280.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 31654 0 0 0 27899 103 0 0 25 0 1 0 539876018 132349952 28499 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32312 28499 603 41 0 32271 0
vsize: 129248
[startup+290.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 31891 0 0 0 28898 105 0 0 25 0 1 0 539876018 133824512 28736 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32672 28736 603 41 0 32631 0
vsize: 130688
[startup+300.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 32089 0 0 0 29898 105 0 0 25 0 1 0 539876018 134754304 28934 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32899 28934 603 41 0 32858 0
vsize: 131596
[startup+310.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 32297 0 0 0 30897 106 0 0 25 0 1 0 539876018 135585792 29142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33102 29142 603 41 0 33061 0
vsize: 132408
[startup+320.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 32550 0 0 0 31899 106 0 0 25 0 1 0 539876018 136642560 29395 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33360 29395 603 41 0 33319 0
vsize: 133440
[startup+330.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 32760 0 0 0 32899 106 0 0 25 0 1 0 539876018 137428992 29605 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33552 29605 603 41 0 33511 0
vsize: 134208
[startup+340.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 33003 0 0 0 33898 108 0 0 25 0 1 0 539876018 138371072 29848 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33782 29848 603 41 0 33741 0
vsize: 135128
[startup+350.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 33185 0 0 0 34898 108 0 0 25 0 1 0 539876018 139186176 30030 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33981 30030 603 41 0 33940 0
vsize: 135924
[startup+360.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 33399 0 0 0 35897 109 0 0 25 0 1 0 539876018 139972608 30244 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34173 30244 603 41 0 34132 0
vsize: 136692
[startup+370.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 33597 0 0 0 36897 109 0 0 25 0 1 0 539876018 140849152 30442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34387 30442 603 41 0 34346 0
vsize: 137548
[startup+380.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 33758 0 0 0 37897 110 0 0 25 0 1 0 539876018 141504512 30603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34547 30603 603 41 0 34506 0
vsize: 138188
[startup+390.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 33934 0 0 0 38897 110 0 0 25 0 1 0 539876018 142299136 30779 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34741 30779 603 41 0 34700 0
vsize: 138964
[startup+400.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 34106 0 0 0 39897 111 0 0 25 0 1 0 539876018 142958592 30951 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34902 30951 603 41 0 34861 0
vsize: 139608
[startup+410.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 34281 0 0 0 40897 111 0 0 25 0 1 0 539876018 143736832 31126 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35092 31126 603 41 0 35051 0
vsize: 140368
[startup+420.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 34471 0 0 0 41896 112 0 0 25 0 1 0 539876018 144523264 31316 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35284 31316 603 41 0 35243 0
vsize: 141136
[startup+430.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 34642 0 0 0 42897 112 0 0 25 0 1 0 539876018 145182720 31487 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35445 31487 603 41 0 35404 0
vsize: 141780
[startup+440.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 34825 0 0 0 43896 113 0 0 25 0 1 0 539876018 145973248 31670 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35638 31670 603 41 0 35597 0
vsize: 142552
[startup+450.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 35002 0 0 0 44896 114 0 0 25 0 1 0 539876018 146657280 31847 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35805 31847 603 41 0 35764 0
vsize: 143220
[startup+460.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 35211 0 0 0 45895 114 0 0 25 0 1 0 539876018 147443712 32056 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35997 32056 603 41 0 35956 0
vsize: 143988
[startup+470.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 35437 0 0 0 46896 115 0 0 25 0 1 0 539876018 148365312 32282 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36222 32282 603 41 0 36181 0
vsize: 144888
[startup+480.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 35601 0 0 0 47896 116 0 0 25 0 1 0 539876018 149024768 32446 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36383 32446 603 41 0 36342 0
vsize: 145532
[startup+490.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 35785 0 0 0 48895 116 0 0 25 0 1 0 539876018 149823488 32630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36578 32630 603 41 0 36537 0
vsize: 146312
[startup+500.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 35937 0 0 0 49895 117 0 0 25 0 1 0 539876018 150487040 32782 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36740 32782 603 41 0 36699 0
vsize: 146960
[startup+510.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 36099 0 0 0 50895 117 0 0 25 0 1 0 539876018 151154688 32944 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36903 32944 603 41 0 36862 0
vsize: 147612
[startup+520.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 36236 0 0 0 51894 118 0 0 25 0 1 0 539876018 151715840 33081 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37040 33081 603 41 0 36999 0
vsize: 148160
[startup+530.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 36394 0 0 0 52894 118 0 0 25 0 1 0 539876018 152383488 33239 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37203 33239 603 41 0 37162 0
vsize: 148812
[startup+540.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 36528 0 0 0 53894 118 0 0 25 0 1 0 539876018 153042944 33373 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37364 33373 603 41 0 37323 0
vsize: 149456
[startup+550.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 36662 0 0 0 54894 119 0 0 25 0 1 0 539876018 153452544 33507 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37464 33507 603 41 0 37423 0
vsize: 149856
[startup+560.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 36811 0 0 0 55894 119 0 0 25 0 1 0 539876018 154271744 33656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37664 33656 603 41 0 37623 0
vsize: 150656
[startup+570.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 36933 0 0 0 56893 119 0 0 25 0 1 0 539876018 154669056 33778 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37761 33778 603 41 0 37720 0
vsize: 151044
[startup+580.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 37054 0 0 0 57893 120 0 0 25 0 1 0 539876018 155217920 33899 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37895 33899 603 41 0 37854 0
vsize: 151580
[startup+590.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 37192 0 0 0 58893 120 0 0 25 0 1 0 539876018 155803648 34037 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38038 34037 603 41 0 37997 0
vsize: 152152
[startup+600.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 37327 0 0 0 59893 121 0 0 25 0 1 0 539876018 156348416 34172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38171 34172 603 41 0 38130 0
vsize: 152684
[startup+610.075 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 37466 0 0 0 60892 122 0 0 25 0 1 0 539876018 156872704 34311 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38299 34311 603 41 0 38258 0
vsize: 153196
[startup+620.075 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 37589 0 0 0 61892 122 0 0 25 0 1 0 539876018 157417472 34434 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38432 34434 603 41 0 38391 0
vsize: 153728
[startup+630.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 37700 0 0 0 62893 122 0 0 25 0 1 0 539876018 157851648 34545 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38538 34545 603 41 0 38497 0
vsize: 154152
[startup+640.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 37826 0 0 0 63892 123 0 0 25 0 1 0 539876018 158375936 34671 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38666 34671 603 41 0 38625 0
vsize: 154664
[startup+650.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 38007 0 0 0 64892 123 0 0 25 0 1 0 539876018 159219712 34852 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38872 34852 603 41 0 38831 0
vsize: 155488
[startup+660.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 38213 0 0 0 65891 124 0 0 25 0 1 0 539876018 160022528 35058 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39068 35058 603 41 0 39027 0
vsize: 156272
[startup+670.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 38422 0 0 0 66891 125 0 0 25 0 1 0 539876018 160813056 35267 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39261 35267 603 41 0 39220 0
vsize: 157044
[startup+680.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 38687 0 0 0 67890 126 0 0 25 0 1 0 539876018 161869824 35532 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39519 35532 603 41 0 39478 0
vsize: 158076
[startup+690.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 38886 0 0 0 68889 126 0 0 25 0 1 0 539876018 162664448 35731 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39713 35731 603 41 0 39672 0
vsize: 158852
[startup+700.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 38989 0 0 0 69889 127 0 0 25 0 1 0 539876018 163205120 35834 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39845 35834 603 41 0 39804 0
vsize: 159380
[startup+710.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 39105 0 0 0 70889 127 0 0 25 0 1 0 539876018 163602432 35950 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39942 35950 603 41 0 39901 0
vsize: 159768
[startup+720.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 39303 0 0 0 71888 128 0 0 25 0 1 0 539876018 164405248 36148 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40138 36148 603 41 0 40097 0
vsize: 160552
[startup+730.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 39416 0 0 0 72888 129 0 0 25 0 1 0 539876018 164802560 36261 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40235 36261 603 41 0 40194 0
vsize: 160940
[startup+740.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 39556 0 0 0 73888 129 0 0 25 0 1 0 539876018 165457920 36401 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40395 36401 603 41 0 40354 0
vsize: 161580
[startup+750.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 39754 0 0 0 74888 129 0 0 25 0 1 0 539876018 166248448 36599 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40588 36599 603 41 0 40547 0
vsize: 162352
[startup+760.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 39876 0 0 0 75888 130 0 0 25 0 1 0 539876018 166641664 36721 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40684 36721 603 41 0 40643 0
vsize: 162736
[startup+770.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 40073 0 0 0 76887 131 0 0 25 0 1 0 539876018 167432192 36918 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40877 36918 603 41 0 40836 0
vsize: 163508
[startup+780.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 40230 0 0 0 77886 131 0 0 25 0 1 0 539876018 168091648 37075 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41038 37075 603 41 0 40997 0
vsize: 164152
[startup+790.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 40385 0 0 0 78886 132 0 0 25 0 1 0 539876018 168751104 37230 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41199 37230 603 41 0 41158 0
vsize: 164796
[startup+800.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 40561 0 0 0 79886 132 0 0 25 0 1 0 539876018 169545728 37406 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41393 37406 603 41 0 41352 0
vsize: 165572
[startup+810.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 40723 0 0 0 80886 132 0 0 25 0 1 0 539876018 170201088 37568 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41553 37568 603 41 0 41512 0
vsize: 166212
[startup+820.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 40882 0 0 0 81885 133 0 0 25 0 1 0 539876018 170876928 37727 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41718 37727 603 41 0 41677 0
vsize: 166872
[startup+830.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 41032 0 0 0 82885 133 0 0 25 0 1 0 539876018 171409408 37877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41848 37877 603 41 0 41807 0
vsize: 167392
[startup+840.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 41174 0 0 0 83885 134 0 0 25 0 1 0 539876018 171937792 38019 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41977 38019 603 41 0 41936 0
vsize: 167908
[startup+850.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 41319 0 0 0 84884 134 0 0 25 0 1 0 539876018 172601344 38164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42139 38164 603 41 0 42098 0
vsize: 168556
[startup+860.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 41470 0 0 0 85884 135 0 0 25 0 1 0 539876018 173260800 38315 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42300 38315 603 41 0 42259 0
vsize: 169200
[startup+870.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 41628 0 0 0 86883 136 0 0 25 0 1 0 539876018 173924352 38473 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42462 38473 603 41 0 42421 0
vsize: 169848
[startup+880.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 41800 0 0 0 87883 136 0 0 25 0 1 0 539876018 174718976 38645 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42656 38645 603 41 0 42615 0
vsize: 170624
[startup+890.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 41939 0 0 0 88883 137 0 0 25 0 1 0 539876018 175247360 38784 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42785 38784 603 41 0 42744 0
vsize: 171140
[startup+900.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 42081 0 0 0 89883 137 0 0 25 0 1 0 539876018 175800320 38926 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42920 38926 603 41 0 42879 0
vsize: 171680
[startup+910.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 42249 0 0 0 90882 137 0 0 25 0 1 0 539876018 176455680 39094 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43080 39094 603 41 0 43039 0
vsize: 172320
[startup+920.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 42421 0 0 0 91882 138 0 0 25 0 1 0 539876018 177246208 39266 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43273 39266 603 41 0 43232 0
vsize: 173092
[startup+930.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 42577 0 0 0 92882 138 0 0 25 0 1 0 539876018 177778688 39422 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43403 39422 603 41 0 43362 0
vsize: 173612
[startup+940.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 42734 0 0 0 93882 139 0 0 25 0 1 0 539876018 178434048 39579 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43563 39579 603 41 0 43522 0
vsize: 174252
[startup+950.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 42932 0 0 0 94882 139 0 0 25 0 1 0 539876018 179224576 39777 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43756 39777 603 41 0 43715 0
vsize: 175024
[startup+960.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 43075 0 0 0 95881 140 0 0 25 0 1 0 539876018 180801536 39920 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44141 39920 603 41 0 44100 0
vsize: 176564
[startup+970.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 43245 0 0 0 96881 140 0 0 25 0 1 0 539876018 181592064 40090 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44334 40090 603 41 0 44293 0
vsize: 177336
[startup+980.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 43423 0 0 0 97881 140 0 0 25 0 1 0 539876018 182259712 40268 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44497 40268 603 41 0 44456 0
vsize: 177988
[startup+990.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 43618 0 0 0 98880 141 0 0 25 0 1 0 539876018 183050240 40463 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44690 40463 603 41 0 44649 0
vsize: 178760
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 43799 0 0 0 99880 141 0 0 25 0 1 0 539876018 183836672 40644 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44882 40644 603 41 0 44841 0
vsize: 179528
[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 43972 0 0 0 100880 142 0 0 25 0 1 0 539876018 184557568 40817 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45058 40817 603 41 0 45017 0
vsize: 180232
[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 44132 0 0 0 101879 143 0 0 25 0 1 0 539876018 185225216 40977 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45221 40977 603 41 0 45180 0
vsize: 180884
[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 44291 0 0 0 102879 143 0 0 25 0 1 0 539876018 185901056 41136 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45386 41136 603 41 0 45345 0
vsize: 181544
[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 44446 0 0 0 103879 143 0 0 25 0 1 0 539876018 186470400 41291 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45525 41291 603 41 0 45484 0
vsize: 182100
[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 44585 0 0 0 104878 144 0 0 25 0 1 0 539876018 186994688 41430 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45653 41430 603 41 0 45612 0
vsize: 182612
[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 44733 0 0 0 105878 145 0 0 25 0 1 0 539876018 187670528 41578 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45818 41578 603 41 0 45777 0
vsize: 183272
[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 44895 0 0 0 106878 145 0 0 25 0 1 0 539876018 188338176 41740 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 41740 603 41 0 45940 0
vsize: 183924
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45021 0 0 0 107878 145 0 0 25 0 1 0 539876018 188911616 41866 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46121 41866 603 41 0 46080 0
vsize: 184484
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45161 0 0 0 108877 146 0 0 25 0 1 0 539876018 189435904 42006 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46249 42006 603 41 0 46208 0
vsize: 184996
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45323 0 0 0 109877 146 0 0 25 0 1 0 539876018 190103552 42168 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46412 42168 603 41 0 46371 0
vsize: 185648
[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45450 0 0 0 110878 146 0 0 25 0 1 0 539876018 190627840 42295 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46540 42295 603 41 0 46499 0
vsize: 186160
[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45575 0 0 0 111877 147 0 0 25 0 1 0 539876018 191160320 42420 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46670 42420 603 41 0 46629 0
vsize: 186680
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45707 0 0 0 112877 147 0 0 25 0 1 0 539876018 191688704 42552 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46799 42552 603 41 0 46758 0
vsize: 187196
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45852 0 0 0 113877 148 0 0 25 0 1 0 539876018 192217088 42697 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46928 42697 603 41 0 46887 0
vsize: 187712
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 45991 0 0 0 114877 148 0 0 25 0 1 0 539876018 192757760 42836 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47060 42836 603 41 0 47019 0
vsize: 188240
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 46131 0 0 0 115876 149 0 0 25 0 1 0 539876018 193417216 42976 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47221 42976 603 41 0 47180 0
vsize: 188884
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 46271 0 0 0 116876 149 0 0 25 0 1 0 539876018 193945600 43116 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47350 43116 603 41 0 47309 0
vsize: 189400
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 46405 0 0 0 117876 149 0 0 25 0 1 0 539876018 194555904 43250 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47499 43250 603 41 0 47458 0
vsize: 189996
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 46619 0 0 0 118875 150 0 0 25 0 1 0 539876018 195428352 43464 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47712 43464 603 41 0 47671 0
vsize: 190848
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5066
Raw data (stat): 5064 (minisat+) R 5063 11931 11930 0 -1 0 46707 0 0 0 119875 150 0 0 25 0 1 0 539876018 195907584 43552 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47829 43552 603 41 0 47788 0
vsize: 191316
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 5066
Raw data (stat): 5064 (minisat+) Z 5063 11931 11930 0 -1 12 46707 0 0 0 119875 160 0 0 25 0 1 0 539876018 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.19
CPU time (s): 1200.36
CPU user time (s): 1198.76
CPU system time (s): 1.60576
CPU usage (%): 100.015
Max. virtual memory (Kb): 191316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####