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-bg512142.opb
MD5SUM	0f3e1a19529370afcd1348994ae2c757
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	6480
Biggest coefficient in the objective function	5242880000
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	755791986840
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	5242880000
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	755791986840
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1246.02
Number of variables	11280
Total number of constraints	1307
Number of constraints which are clauses	11
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1296
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 13963

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        755604 kB
Buffers:         33396 kB
Cached:         221040 kB
SwapCached:       2060 kB
Active:          97084 kB
Inactive:       162204 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        755352 kB
SwapTotal:     2097136 kB
SwapFree:      2094988 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14100 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:49:11 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 19942 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1171 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1224]---> Sorter-cost: 1119     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1222]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1221]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1220]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost: 1205     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1218]---> Sorter-cost:  643     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1211]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1210]---> Sorter-cost:  940     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1208]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Sorter-cost: 1094     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> BDD-cost:  131
c ---[1205]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1200]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1199]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1198]---> Sorter-cost: 1142     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1197]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1188]---> Sorter-cost: 1221     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1182]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1181]---> Sorter-cost:  949     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1180]---> Sorter-cost: 1205     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1178]---> Sorter-cost:  953     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1177]---> Sorter-cost:  484     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1176]---> Sorter-cost:  666     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1175]---> Sorter-cost: 1136     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1173]---> Sorter-cost: 1324     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1172]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1171]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1168]---> Sorter-cost: 1029     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1167]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1166]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1165]---> Sorter-cost: 1127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1163]---> Sorter-cost:  672     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost:  708     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1153]---> Sorter-cost: 1331     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1152]---> Sorter-cost: 1244     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1147]---> Sorter-cost:  985     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1145]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1143]---> Sorter-cost: 1186     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1142]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1140]---> Sorter-cost:  710     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1139]---> BDD-cost:  113
c ---[1136]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost:  666     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1129]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1125]---> BDD-cost:  163
c ---[1123]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1119]---> Sorter-cost: 1140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1117]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1115]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1113]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1111]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1109]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1107]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1105]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1103]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1101]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1099]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1097]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1095]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1093]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1091]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1089]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1087]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1085]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1083]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1081]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1079]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1077]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1075]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1073]---> Sorter-cost: 1099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1071]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1069]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1067]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1065]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1063]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1061]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1059]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1057]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1055]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1053]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1051]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1049]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1047]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1045]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1043]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1041]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1039]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1037]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1035]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1033]---> Sorter-cost:  948     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1031]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1029]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1027]---> Sorter-cost: 1165     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1025]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1023]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1021]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1019]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1017]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1015]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1013]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1011]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1009]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1007]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1005]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1003]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1001]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 999]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 997]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 995]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 993]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 991]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 989]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 987]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 985]---> Sorter-cost:  967     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 983]---> Sorter-cost:  897     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 981]---> Sorter-cost:  742     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 979]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 977]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 975]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 973]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 971]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 969]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 967]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 965]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 963]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 961]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 959]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 957]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 955]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 953]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 951]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 949]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 947]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 945]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 943]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 941]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 939]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 937]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 935]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 933]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 931]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 929]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 927]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 925]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 923]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 921]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 919]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 917]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 915]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 913]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 911]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 909]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 907]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 905]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 903]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 901]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 899]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 897]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 895]---> Sorter-cost: 1018     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 893]---> Sorter-cost:  967     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 891]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 889]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 887]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 885]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 883]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 881]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 879]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 877]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 875]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 873]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 871]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 869]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 867]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 865]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 863]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 861]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 859]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 857]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 855]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 853]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 851]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 849]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 847]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 845]---> Sorter-cost:  948     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 843]---> BDD-cost:   71
c ---[ 841]---> BDD-cost:   62
c ---[ 839]---> BDD-cost:   71
c ---[ 837]---> BDD-cost:   76
c ---[ 835]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 833]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 831]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 829]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 827]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 825]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 823]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 821]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 819]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 817]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 815]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 813]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 811]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 809]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 807]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 803]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 797]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 795]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 793]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 791]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 789]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 787]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 785]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 777]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 773]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 771]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 769]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 767]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 765]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 763]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 761]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 759]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 757]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 755]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 753]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 751]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 749]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 747]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 745]---> Sorter-cost:  382     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 743]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 741]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 739]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 737]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 735]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 733]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 731]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 729]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 727]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 725]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 723]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 721]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 719]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 717]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 715]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 713]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 711]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 709]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 707]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 705]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 703]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 701]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 699]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 697]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 695]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 693]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 691]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 689]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 685]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 683]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 681]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 679]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 677]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 675]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 673]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 671]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 669]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 667]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 665]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 663]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 657]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> BDD-cost:   73
c ---[ 651]---> BDD-cost:   97
c ---[ 650]---> BDD-cost:   97
c ---[ 649]---> BDD-cost:   97
c ---[ 648]---> BDD-cost:   97
c ---[ 647]---> BDD-cost:   97
c ---[ 646]---> BDD-cost:   97
c ---[ 645]---> BDD-cost:   97
c ---[ 644]---> BDD-cost:   97
c ---[ 643]---> BDD-cost:   97
c ---[ 642]---> BDD-cost:   97
c ---[ 641]---> BDD-cost:   97
c ---[ 640]---> BDD-cost:   93
c ---[ 639]---> BDD-cost:   93
c ---[ 638]---> BDD-cost:   93
c ---[ 637]---> BDD-cost:   93
c ---[ 636]---> BDD-cost:   93
c ---[ 635]---> BDD-cost:   89
c ---[ 634]---> BDD-cost:   89
c ---[ 633]---> BDD-cost:   89
c ---[ 632]---> BDD-cost:   69
c ---[ 631]---> BDD-cost:   93
c ---[ 630]---> BDD-cost:   93
c ---[ 629]---> BDD-cost:   93
c ---[ 628]---> BDD-cost:   93
c ---[ 627]---> BDD-cost:   93
c ---[ 626]---> BDD-cost:   93
c ---[ 625]---> BDD-cost:   93
c ---[ 624]---> BDD-cost:   93
c ---[ 623]---> BDD-cost:   89
c ---[ 622]---> BDD-cost:   89
c ---[ 621]---> BDD-cost:   89
c ---[ 620]---> BDD-cost:   89
c ---[ 619]---> BDD-cost:   89
c ---[ 618]---> BDD-cost:   89
c ---[ 617]---> BDD-cost:   78
c ---[ 616]---> BDD-cost:   73
c ---[ 615]---> BDD-cost:  100
c ---[ 614]---> BDD-cost:  100
c ---[ 613]---> BDD-cost:  100
c ---[ 612]---> BDD-cost:  100
c ---[ 611]---> BDD-cost:  100
c ---[ 610]---> BDD-cost:  100
c ---[ 609]---> BDD-cost:   96
c ---[ 608]---> BDD-cost:   96
c ---[ 607]---> BDD-cost:   96
c ---[ 606]---> BDD-cost:   96
c ---[ 605]---> BDD-cost:   96
c ---[ 604]---> BDD-cost:   96
c ---[ 603]---> BDD-cost:   96
c ---[ 602]---> BDD-cost:   88
c ---[ 601]---> BDD-cost:   88
c ---[ 600]---> BDD-cost:   88
c ---[ 599]---> BDD-cost:   77
c ---[ 598]---> BDD-cost:  104
c ---[ 597]---> BDD-cost:  104
c ---[ 596]---> BDD-cost:  104
c ---[ 595]---> BDD-cost:  103
c ---[ 594]---> BDD-cost:  104
c ---[ 593]---> BDD-cost:  104
c ---[ 592]---> BDD-cost:  100
c ---[ 591]---> BDD-cost:  100
c ---[ 590]---> BDD-cost:   99
c ---[ 589]---> BDD-cost:   99
c ---[ 588]---> BDD-cost:  100
c ---[ 587]---> BDD-cost:  100
c ---[ 586]---> BDD-cost:  100
c ---[ 585]---> BDD-cost:   96
c ---[ 584]---> BDD-cost:   96
c ---[ 583]---> BDD-cost:   96
c ---[ 582]---> BDD-cost:   96
c ---[ 581]---> BDD-cost:   88
c ---[ 580]---> BDD-cost:   88
c ---[ 579]---> BDD-cost:   77
c ---[ 578]---> BDD-cost:  107
c ---[ 577]---> BDD-cost:  107
c ---[ 576]---> BDD-cost:  107
c ---[ 575]---> BDD-cost:  107
c ---[ 574]---> BDD-cost:  107
c ---[ 573]---> BDD-cost:  107
c ---[ 572]---> BDD-cost:  103
c ---[ 571]---> BDD-cost:  103
c ---[ 570]---> BDD-cost:  103
c ---[ 569]---> BDD-cost:  103
c ---[ 568]---> BDD-cost:  103
c ---[ 567]---> BDD-cost:  103
c ---[ 566]---> BDD-cost:  103
c ---[ 565]---> BDD-cost:   95
c ---[ 564]---> BDD-cost:   95
c ---[ 563]---> BDD-cost:   95
c ---[ 562]---> BDD-cost:   73
c ---[ 561]---> BDD-cost:   97
c ---[ 560]---> BDD-cost:   97
c ---[ 559]---> BDD-cost:   97
c ---[ 558]---> BDD-cost:   97
c ---[ 557]---> BDD-cost:   97
c ---[ 556]---> BDD-cost:   97
c ---[ 555]---> BDD-cost:   97
c ---[ 554]---> BDD-cost:   97
c ---[ 553]---> BDD-cost:   97
c ---[ 552]---> BDD-cost:   97
c ---[ 551]---> BDD-cost:   97
c ---[ 550]---> BDD-cost:   97
c ---[ 549]---> BDD-cost:   93
c ---[ 548]---> BDD-cost:   93
c ---[ 547]---> BDD-cost:   93
c ---[ 546]---> BDD-cost:   92
c ---[ 545]---> BDD-cost:   88
c ---[ 544]---> BDD-cost:   88
c ---[ 543]---> BDD-cost:   89
c ---[ 542]---> BDD-cost:   78
c ---[ 541]---> BDD-cost:   77
c ---[ 540]---> BDD-cost:  104
c ---[ 539]---> BDD-cost:  104
c ---[ 538]---> BDD-cost:  104
c ---[ 537]---> BDD-cost:  104
c ---[ 536]---> BDD-cost:  104
c ---[ 535]---> BDD-cost:  104
c ---[ 534]---> BDD-cost:  104
c ---[ 533]---> BDD-cost:  104
c ---[ 532]---> BDD-cost:  104
c ---[ 531]---> BDD-cost:  104
c ---[ 530]---> BDD-cost:  104
c ---[ 529]---> BDD-cost:  100
c ---[ 528]---> BDD-cost:  100
c ---[ 527]---> BDD-cost:  100
c ---[ 526]---> BDD-cost:  100
c ---[ 525]---> BDD-cost:   99
c ---[ 524]---> BDD-cost:   95
c ---[ 523]---> BDD-cost:   95
c ---[ 522]---> BDD-cost:   96
c ---[ 521]---> BDD-cost:   88
c ---[ 520]---> BDD-cost:   73
c ---[ 519]---> BDD-cost:   96
c ---[ 518]---> BDD-cost:   97
c ---[ 517]---> BDD-cost:   97
c ---[ 516]---> BDD-cost:   97
c ---[ 515]---> BDD-cost:   97
c ---[ 514]---> BDD-cost:   97
c ---[ 513]---> BDD-cost:   93
c ---[ 512]---> BDD-cost:   93
c ---[ 511]---> BDD-cost:   93
c ---[ 510]---> BDD-cost:   92
c ---[ 509]---> BDD-cost:   92
c ---[ 508]---> BDD-cost:   93
c ---[ 507]---> BDD-cost:   93
c ---[ 506]---> BDD-cost:   85
c ---[ 505]---> BDD-cost:   85
c ---[ 504]---> BDD-cost:   85
c ---[ 503]---> BDD-cost:   77
c ---[ 502]---> BDD-cost:   63
c ---[ 501]---> BDD-cost:  101
c ---[ 500]---> BDD-cost:  101
c ---[ 499]---> BDD-cost:   97
c ---[ 498]---> BDD-cost:   97
c ---[ 497]---> BDD-cost:   97
c ---[ 496]---> BDD-cost:   97
c ---[ 495]---> BDD-cost:   97
c ---[ 494]---> BDD-cost:   97
c ---[ 493]---> BDD-cost:   97
c ---[ 492]---> BDD-cost:   97
c ---[ 491]---> BDD-cost:   96
c ---[ 490]---> BDD-cost:   92
c ---[ 489]---> BDD-cost:   93
c ---[ 488]---> BDD-cost:   93
c ---[ 487]---> BDD-cost:   93
c ---[ 486]---> BDD-cost:   93
c ---[ 485]---> BDD-cost:   85
c ---[ 484]---> BDD-cost:   85
c ---[ 483]---> BDD-cost:   77
c ---[ 482]---> BDD-cost:  101
c ---[ 481]---> BDD-cost:  101
c ---[ 480]---> BDD-cost:  101
c ---[ 479]---> BDD-cost:  101
c ---[ 478]---> BDD-cost:  101
c ---[ 477]---> BDD-cost:  101
c ---[ 476]---> BDD-cost:  101
c ---[ 475]---> BDD-cost:  101
c ---[ 474]---> BDD-cost:   97
c ---[ 473]---> BDD-cost:   97
c ---[ 472]---> BDD-cost:   97
c ---[ 471]---> BDD-cost:   97
c ---[ 470]---> BDD-cost:   97
c ---[ 469]---> BDD-cost:   97
c ---[ 468]---> BDD-cost:   93
c ---[ 467]---> BDD-cost:   93
c ---[ 466]---> BDD-cost:   93
c ---[ 465]---> BDD-cost:   93
c ---[ 464]---> BDD-cost:   47
c ---[ 463]---> BDD-cost:   17
c ---[ 462]---> BDD-cost:   29
c ---[ 461]---> BDD-cost:   27
c ---[ 460]---> BDD-cost:   28
c ---[ 459]---> BDD-cost:   28
c ---[ 458]---> BDD-cost:   28
c ---[ 457]---> BDD-cost:   29
c ---[ 456]---> BDD-cost:   29
c ---[ 455]---> BDD-cost:   29
c ---[ 454]---> BDD-cost:   27
c ---[ 453]---> BDD-cost:   29
c ---[ 452]---> BDD-cost:   29
c ---[ 451]---> BDD-cost:   25
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:   22
c ---[ 448]---> BDD-cost:   27
c ---[ 447]---> BDD-cost:   27
c ---[ 446]---> BDD-cost:   21
c ---[ 445]---> BDD-cost:   25
c ---[ 444]---> BDD-cost:   25
c ---[ 443]---> BDD-cost:   22
c ---[ 442]---> BDD-cost:   21
c ---[ 441]---> BDD-cost:   20
c ---[ 440]---> BDD-cost:   17
c ---[ 439]---> BDD-cost:   16
c ---[ 438]---> BDD-cost:   21
c ---[ 437]---> BDD-cost:   26
c ---[ 436]---> BDD-cost:   26
c ---[ 435]---> BDD-cost:   24
c ---[ 434]---> BDD-cost:   27
c ---[ 433]---> BDD-cost:   24
c ---[ 432]---> BDD-cost:   24
c ---[ 431]---> BDD-cost:   26
c ---[ 430]---> BDD-cost:   24
c ---[ 429]---> BDD-cost:   21
c ---[ 428]---> BDD-cost:   25
c ---[ 427]---> BDD-cost:   23
c ---[ 426]---> BDD-cost:   25
c ---[ 425]---> BDD-cost:   23
c ---[ 424]---> BDD-cost:   20
c ---[ 423]---> BDD-cost:   23
c ---[ 422]---> BDD-cost:   22
c ---[ 421]---> BDD-cost:   21
c ---[ 420]---> BDD-cost:   21
c ---[ 419]---> BDD-cost:   21
c ---[ 418]---> BDD-cost:   19
c ---[ 417]---> BDD-cost:   19
c ---[ 416]---> BDD-cost:   15
c ---[ 415]---> BDD-cost:   17
c ---[ 414]---> BDD-cost:   27
c ---[ 413]---> BDD-cost:   29
c ---[ 412]---> BDD-cost:   29
c ---[ 411]---> BDD-cost:   29
c ---[ 410]---> BDD-cost:   27
c ---[ 409]---> BDD-cost:   28
c ---[ 408]---> BDD-cost:   27
c ---[ 407]---> BDD-cost:   27
c ---[ 406]---> BDD-cost:   26
c ---[ 405]---> BDD-cost:   27
c ---[ 404]---> BDD-cost:   27
c ---[ 403]---> BDD-cost:   27
c ---[ 402]---> BDD-cost:   27
c ---[ 401]---> BDD-cost:   25
c ---[ 400]---> BDD-cost:   25
c ---[ 399]---> BDD-cost:   22
c ---[ 398]---> BDD-cost:   25
c ---[ 397]---> BDD-cost:   22
c ---[ 396]---> BDD-cost:   19
c ---[ 395]---> BDD-cost:   23
c ---[ 394]---> BDD-cost:   20
c ---[ 393]---> BDD-cost:   20
c ---[ 392]---> BDD-cost:   17
c ---[ 391]---> BDD-cost:   18
c ---[ 390]---> BDD-cost:   30
c ---[ 389]---> BDD-cost:   31
c ---[ 388]---> BDD-cost:   27
c ---[ 387]---> BDD-cost:   31
c ---[ 386]---> BDD-cost:   30
c ---[ 385]---> BDD-cost:   31
c ---[ 384]---> BDD-cost:   27
c ---[ 383]---> BDD-cost:   29
c ---[ 382]---> BDD-cost:   29
c ---[ 381]---> BDD-cost:   29
c ---[ 380]---> BDD-cost:   28
c ---[ 379]---> BDD-cost:   27
c ---[ 378]---> BDD-cost:   28
c ---[ 377]---> BDD-cost:   27
c ---[ 376]---> BDD-cost:   26
c ---[ 375]---> BDD-cost:   26
c ---[ 374]---> BDD-cost:   25
c ---[ 373]---> BDD-cost:   25
c ---[ 372]---> BDD-cost:   24
c ---[ 371]---> BDD-cost:   25
c ---[ 370]---> BDD-cost:   21
c ---[ 369]---> BDD-cost:   20
c ---[ 368]---> BDD-cost:   18
c ---[ 367]---> BDD-cost:   18
c ---[ 366]---> BDD-cost:   31
c ---[ 365]---> BDD-cost:   30
c ---[ 364]---> BDD-cost:   29
c ---[ 363]---> BDD-cost:   30
c ---[ 362]---> BDD-cost:   31
c ---[ 361]---> BDD-cost:   31
c ---[ 360]---> BDD-cost:   29
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   28
c ---[ 357]---> BDD-cost:   29
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   25
c ---[ 352]---> BDD-cost:   27
c ---[ 351]---> BDD-cost:   25
c ---[ 350]---> BDD-cost:   26
c ---[ 349]---> BDD-cost:   24
c ---[ 348]---> BDD-cost:   24
c ---[ 347]---> BDD-cost:   25
c ---[ 346]---> BDD-cost:   23
c ---[ 345]---> BDD-cost:   21
c ---[ 344]---> BDD-cost:   18
c ---[ 342]---> BDD-cost:   27
c ---[ 341]---> BDD-cost:   29
c ---[ 340]---> BDD-cost:   29
c ---[ 339]---> BDD-cost:   29
c ---[ 338]---> BDD-cost:   29
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   29
c ---[ 335]---> BDD-cost:   29
c ---[ 334]---> BDD-cost:   24
c ---[ 333]---> BDD-cost:   29
c ---[ 332]---> BDD-cost:   26
c ---[ 331]---> BDD-cost:   29
c ---[ 330]---> BDD-cost:   26
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   27
c ---[ 327]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:   25
c ---[ 325]---> BDD-cost:   25
c ---[ 324]---> BDD-cost:   25
c ---[ 323]---> BDD-cost:   21
c ---[ 322]---> BDD-cost:   23
c ---[ 321]---> BDD-cost:   21
c ---[ 320]---> BDD-cost:   18
c ---[ 318]---> BDD-cost:   30
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   31
c ---[ 315]---> BDD-cost:   30
c ---[ 314]---> BDD-cost:   30
c ---[ 313]---> BDD-cost:   31
c ---[ 312]---> BDD-cost:   31
c ---[ 311]---> BDD-cost:   30
c ---[ 310]---> BDD-cost:   31
c ---[ 309]---> BDD-cost:   30
c ---[ 308]---> BDD-cost:   31
c ---[ 307]---> BDD-cost:   29
c ---[ 306]---> BDD-cost:   29
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   29
c ---[ 303]---> BDD-cost:   28
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   26
c ---[ 299]---> BDD-cost:   24
c ---[ 298]---> BDD-cost:   24
c ---[ 297]---> BDD-cost:   20
c ---[ 296]---> BDD-cost:   21
c ---[ 295]---> BDD-cost:   18
c ---[ 294]---> BDD-cost:   31
c ---[ 293]---> BDD-cost:   30
c ---[ 292]---> BDD-cost:   29
c ---[ 291]---> BDD-cost:   30
c ---[ 290]---> BDD-cost:   31
c ---[ 289]---> BDD-cost:   31
c ---[ 288]---> BDD-cost:   29
c ---[ 287]---> BDD-cost:   29
c ---[ 286]---> BDD-cost:   28
c ---[ 285]---> BDD-cost:   29
c ---[ 284]---> BDD-cost:   28
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   28
c ---[ 281]---> BDD-cost:   25
c ---[ 280]---> BDD-cost:   27
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   24
c ---[ 276]---> BDD-cost:   24
c ---[ 275]---> BDD-cost:   25
c ---[ 274]---> BDD-cost:   23
c ---[ 273]---> BDD-cost:   21
c ---[ 272]---> BDD-cost:   18
c ---[ 271]---> BDD-cost:   19
c ---[ 270]---> BDD-cost:   33
c ---[ 269]---> BDD-cost:   33
c ---[ 268]---> BDD-cost:   33
c ---[ 267]---> BDD-cost:   31
c ---[ 266]---> BDD-cost:   27
c ---[ 265]---> BDD-cost:   31
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   30
c ---[ 262]---> BDD-cost:   30
c ---[ 261]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:   30
c ---[ 259]---> BDD-cost:   31
c ---[ 258]---> BDD-cost:   27
c ---[ 257]---> BDD-cost:   29
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   29
c ---[ 254]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   27
c ---[ 252]---> BDD-cost:   27
c ---[ 251]---> BDD-cost:   25
c ---[ 250]---> BDD-cost:   23
c ---[ 249]---> BDD-cost:   22
c ---[ 248]---> BDD-cost:   18
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   32
c ---[ 245]---> BDD-cost:   33
c ---[ 244]---> BDD-cost:   31
c ---[ 243]---> BDD-cost:   33
c ---[ 242]---> BDD-cost:   33
c ---[ 241]---> BDD-cost:   33
c ---[ 240]---> BDD-cost:   32
c ---[ 239]---> BDD-cost:   33
c ---[ 238]---> BDD-cost:   31
c ---[ 237]---> BDD-cost:   31
c ---[ 236]---> BDD-cost:   31
c ---[ 235]---> BDD-cost:   30
c ---[ 234]---> BDD-cost:   31
c ---[ 233]---> BDD-cost:   31
c ---[ 232]---> BDD-cost:   26
c ---[ 231]---> BDD-cost:   29
c ---[ 230]---> BDD-cost:   26
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   27
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   25
c ---[ 225]---> BDD-cost:   25
c ---[ 224]---> BDD-cost:   23
c ---[ 223]---> Sorter-cost:  711     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 220]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 218]---> Sorter-cost:  889     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 216]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 212]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost: 1096     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 210]---> Sorter-cost: 1074     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 208]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost:  974     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 206]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 190]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost: 1182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost: 1214     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> Sorter-cost: 1177     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 1419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost: 1403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 1422     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost: 1422     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 1422     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 1400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1446     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 1405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1379     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost: 1366     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1346     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 1346     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 1347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost: 1523     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost: 1580     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 157]---> Sorter-cost: 1788     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:    5
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:    4
c ---[ 150]---> BDD-cost:   16
c ---[ 149]---> BDD-cost:    6
c ---[ 148]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  434     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost:  461     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  537     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost:  648     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  841     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 1427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1536     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 1577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1516     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:    7
c ---[ 133]---> BDD-cost:    4
c ---[ 132]---> BDD-cost:    7
c ---[ 131]---> BDD-cost:    7
c ---[ 130]---> BDD-cost:    5
c ---[ 129]---> BDD-cost:    7
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:    6
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:    6
c ---[ 123]---> BDD-cost:    7
c ---[ 122]---> BDD-cost:    5
c ---[ 121]---> BDD-cost:    7
c ---[ 120]---> BDD-cost:    7
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> Sorter-cost:  518     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost:  543     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost:  486     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> BDD-cost:  118
c ---[ 114]---> BDD-cost:  119
c ---[ 113]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:  124
c ---[ 111]---> BDD-cost:  134
c ---[ 110]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1545     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 1468     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1606     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1553     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1512     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    6
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:    3
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    6
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:  127
c ---[  91]---> BDD-cost:  134
c ---[  90]---> BDD-cost:  115
c ---[  89]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> Sorter-cost: 1007     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost:  693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  84]---> Sorter-cost: 1577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  82]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:   19
c ---[  79]---> BDD-cost:   11
c ---[  78]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost:  490     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> Sorter-cost: 1126     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  74]---> Sorter-cost: 1165     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  73]---> Sorter-cost:  164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1615     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost: 1574     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:   22
c ---[  67]---> BDD-cost:    8
c ---[  66]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   39
c ---[  63]---> BDD-cost:    1
c ---[  62]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost:  533     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> BDD-cost:    8
c ---[  59]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:   23
c ---[  52]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> BDD-cost:  127
c ---[  50]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:   11
c ---[  46]---> Sorter-cost:  876     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   19
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:   48
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:    4
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:  123
c ---[  37]---> BDD-cost:    8
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   55
c ---[  34]---> BDD-cost:    6
c ---[  33]---> Sorter-cost: 1081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:   22
c ---[  29]---> BDD-cost:   15
c ---[  28]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   39
c ---[  25]---> BDD-cost:   48
c ---[  24]---> BDD-cost:   35
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:    8
c ---[  21]---> BDD-cost:  127
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:  109
c ---[  17]---> BDD-cost:  139
c ---[  16]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   46
c ---[  13]---> BDD-cost:   45
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   16
c ---[   9]---> Sorter-cost:  953     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  986     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  940     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  963     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost: 1152     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost: 1096     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost: 1412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost: 1350     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  999288  2398467 |  333096       0        0     nan |  0.000 % |
c |       100 |  999163  2398190 |  366405      75      255     3.4 |  3.274 % |
c |       250 |  999087  2398022 |  403046     215      725     3.4 |  3.280 % |
c |       475 |  998818  2397424 |  443350     397     1333     3.4 |  3.304 % |
c |       812 |  998623  2396989 |  487685     712     2348     3.3 |  3.321 % |
c |      1318 |  998072  2395770 |  536454    1124     3770     3.4 |  3.371 % |
c |      2077 |  997271  2393977 |  590099    1773     6000     3.4 |  3.438 % |
c |      3217 |  996216  2391631 |  649109    2743     9941     3.6 |  3.531 % |
c |      4926 |  994242  2387223 |  714020    4170    15590     3.7 |  3.701 % |
c |      7488 |  991641  2381420 |  785422    6367    24661     3.9 |  3.923 % |
c |     11332 |  988497  2374409 |  863965    9810    43487     4.4 |  4.191 % |
c |     17098 |  984375  2365167 |  950361   15027    77872     5.2 |  4.540 % |
c |     25747 |  979569  2354431 | 1045397   23041   120996     5.3 |  4.950 % |
c |     38721 |  973695  2341307 | 1149937   35234   224926     6.4 |  5.451 % |
c |     58183 |  969673  2332312 | 1264931   54181   440503     8.1 |  5.793 % |
#### 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.86 0.95 0.92 2/54 25129
Raw data (stat): 25129 (runsolver) R 25128 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481819818 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.88 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28632 0 0 0 932 66 0 0 25 0 1 0 481819818 128757760 27250 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31435 27250 603 41 0 31394 0
vsize: 125740
[startup+20.0014 s]
Raw data (loadavg): 0.90 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28639 0 0 0 1931 67 0 0 25 0 1 0 481819818 128892928 27257 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31468 27257 603 41 0 31427 0
vsize: 125872
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28712 0 0 0 2931 67 0 0 25 0 1 0 481819818 129028096 27330 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31501 27330 603 41 0 31460 0
vsize: 126004
[startup+40.0011 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28728 0 0 0 3931 67 0 0 25 0 1 0 481819818 129028096 27346 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31501 27346 603 41 0 31460 0
vsize: 126004
[startup+50.0009 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28762 0 0 0 4930 68 0 0 25 0 1 0 481819818 129163264 27380 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31534 27380 603 41 0 31493 0
vsize: 126136
[startup+60.0017 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28780 0 0 0 5930 68 0 0 25 0 1 0 481819818 129298432 27398 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31567 27398 603 41 0 31526 0
vsize: 126268
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28809 0 0 0 6930 69 0 0 25 0 1 0 481819818 129298432 27427 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31567 27427 603 41 0 31526 0
vsize: 126268
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28835 0 0 0 7929 69 0 0 25 0 1 0 481819818 129433600 27453 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31600 27453 603 41 0 31559 0
vsize: 126400
[startup+90.0021 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28858 0 0 0 8929 69 0 0 25 0 1 0 481819818 129433600 27476 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31600 27476 603 41 0 31559 0
vsize: 126400
[startup+100.002 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28864 0 0 0 9929 69 0 0 25 0 1 0 481819818 129433600 27482 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31600 27482 603 41 0 31559 0
vsize: 126400
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28872 0 0 0 10930 69 0 0 25 0 1 0 481819818 129433600 27490 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31600 27490 603 41 0 31559 0
vsize: 126400
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28899 0 0 0 11930 69 0 0 25 0 1 0 481819818 129568768 27517 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31633 27517 603 41 0 31592 0
vsize: 126532
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28907 0 0 0 12930 69 0 0 25 0 1 0 481819818 129568768 27525 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31633 27525 603 41 0 31592 0
vsize: 126532
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28917 0 0 0 13930 69 0 0 25 0 1 0 481819818 129568768 27535 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31633 27535 603 41 0 31592 0
vsize: 126532
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28946 0 0 0 14930 70 0 0 25 0 1 0 481819818 129703936 27564 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31666 27564 603 41 0 31625 0
vsize: 126664
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28949 0 0 0 15930 70 0 0 25 0 1 0 481819818 129703936 27567 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31666 27567 603 41 0 31625 0
vsize: 126664
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28954 0 0 0 16930 70 0 0 25 0 1 0 481819818 129703936 27572 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31666 27572 603 41 0 31625 0
vsize: 126664
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28976 0 0 0 17930 70 0 0 25 0 1 0 481819818 129703936 27594 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31666 27594 603 41 0 31625 0
vsize: 126664
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28986 0 0 0 18931 70 0 0 25 0 1 0 481819818 129839104 27604 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31699 27604 603 41 0 31658 0
vsize: 126796
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28996 0 0 0 19931 70 0 0 25 0 1 0 481819818 129839104 27614 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31699 27614 603 41 0 31658 0
vsize: 126796
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 28999 0 0 0 20931 70 0 0 25 0 1 0 481819818 129839104 27617 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31699 27617 603 41 0 31658 0
vsize: 126796
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29013 0 0 0 21931 70 0 0 25 0 1 0 481819818 129839104 27631 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31699 27631 603 41 0 31658 0
vsize: 126796
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29018 0 0 0 22931 70 0 0 25 0 1 0 481819818 129839104 27636 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31699 27636 603 41 0 31658 0
vsize: 126796
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29037 0 0 0 23931 70 0 0 25 0 1 0 481819818 129974272 27655 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31732 27655 603 41 0 31691 0
vsize: 126928
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29050 0 0 0 24931 70 0 0 25 0 1 0 481819818 129974272 27668 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31732 27668 603 41 0 31691 0
vsize: 126928
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29061 0 0 0 25931 70 0 0 25 0 1 0 481819818 129974272 27679 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31732 27679 603 41 0 31691 0
vsize: 126928
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29068 0 0 0 26932 70 0 0 25 0 1 0 481819818 130109440 27686 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31765 27686 603 41 0 31724 0
vsize: 127060
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29070 0 0 0 27932 70 0 0 25 0 1 0 481819818 130109440 27688 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31765 27688 603 41 0 31724 0
vsize: 127060
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29100 0 0 0 28931 70 0 0 25 0 1 0 481819818 130109440 27718 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31765 27718 603 41 0 31724 0
vsize: 127060
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29106 0 0 0 29931 70 0 0 25 0 1 0 481819818 130109440 27724 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31765 27724 603 41 0 31724 0
vsize: 127060
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29110 0 0 0 30932 70 0 0 25 0 1 0 481819818 130109440 27728 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31765 27728 603 41 0 31724 0
vsize: 127060
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29126 0 0 0 31932 70 0 0 25 0 1 0 481819818 130244608 27744 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31798 27744 603 41 0 31757 0
vsize: 127192
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29137 0 0 0 32932 70 0 0 25 0 1 0 481819818 130244608 27755 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31798 27755 603 41 0 31757 0
vsize: 127192
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29149 0 0 0 33932 70 0 0 25 0 1 0 481819818 130244608 27767 4294967295 134512640 134672761 3221224544 3221223712 134564736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31798 27767 603 41 0 31757 0
vsize: 127192
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29153 0 0 0 34932 70 0 0 25 0 1 0 481819818 130244608 27771 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31798 27771 603 41 0 31757 0
vsize: 127192
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29159 0 0 0 35932 70 0 0 25 0 1 0 481819818 130379776 27777 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31831 27777 603 41 0 31790 0
vsize: 127324
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29185 0 0 0 36932 70 0 0 25 0 1 0 481819818 130379776 27803 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31831 27803 603 41 0 31790 0
vsize: 127324
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29187 0 0 0 37933 70 0 0 25 0 1 0 481819818 130379776 27805 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31831 27805 603 41 0 31790 0
vsize: 127324
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29191 0 0 0 38933 70 0 0 25 0 1 0 481819818 130379776 27809 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31831 27809 603 41 0 31790 0
vsize: 127324
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29196 0 0 0 39933 70 0 0 25 0 1 0 481819818 130379776 27814 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31831 27814 603 41 0 31790 0
vsize: 127324
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29203 0 0 0 40932 71 0 0 25 0 1 0 481819818 130514944 27821 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31864 27821 603 41 0 31823 0
vsize: 127456
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29207 0 0 0 41933 71 0 0 25 0 1 0 481819818 130514944 27825 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31864 27825 603 41 0 31823 0
vsize: 127456
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29213 0 0 0 42933 71 0 0 25 0 1 0 481819818 130514944 27831 4294967295 134512640 134672761 3221224544 3221223716 134556604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31864 27831 603 41 0 31823 0
vsize: 127456
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29233 0 0 0 43934 71 0 0 25 0 1 0 481819818 130719744 27851 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27851 603 41 0 31873 0
vsize: 127656
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29233 0 0 0 44934 71 0 0 25 0 1 0 481819818 130719744 27851 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27851 603 41 0 31873 0
vsize: 127656
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29233 0 0 0 45934 71 0 0 25 0 1 0 481819818 130719744 27851 4294967295 134512640 134672761 3221224544 3221223760 134561950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27851 603 41 0 31873 0
vsize: 127656
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29247 0 0 0 46934 71 0 0 25 0 1 0 481819818 130719744 27865 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27865 603 41 0 31873 0
vsize: 127656
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29261 0 0 0 47934 71 0 0 25 0 1 0 481819818 130719744 27879 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27879 603 41 0 31873 0
vsize: 127656
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29266 0 0 0 48934 71 0 0 25 0 1 0 481819818 130719744 27884 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27884 603 41 0 31873 0
vsize: 127656
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29271 0 0 0 49934 71 0 0 25 0 1 0 481819818 130719744 27889 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27889 603 41 0 31873 0
vsize: 127656
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29277 0 0 0 50934 71 0 0 25 0 1 0 481819818 130719744 27895 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31914 27895 603 41 0 31873 0
vsize: 127656
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29294 0 0 0 51935 71 0 0 25 0 1 0 481819818 130854912 27912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31947 27912 603 41 0 31906 0
vsize: 127788
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29306 0 0 0 52935 71 0 0 25 0 1 0 481819818 130854912 27924 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31947 27924 603 41 0 31906 0
vsize: 127788
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29309 0 0 0 53935 71 0 0 25 0 1 0 481819818 130854912 27927 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31947 27927 603 41 0 31906 0
vsize: 127788
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29316 0 0 0 54935 71 0 0 25 0 1 0 481819818 130854912 27934 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31947 27934 603 41 0 31906 0
vsize: 127788
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29325 0 0 0 55935 71 0 0 25 0 1 0 481819818 130854912 27943 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31947 27943 603 41 0 31906 0
vsize: 127788
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29331 0 0 0 56935 71 0 0 25 0 1 0 481819818 130990080 27949 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31980 27949 603 41 0 31939 0
vsize: 127920
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29342 0 0 0 57935 71 0 0 25 0 1 0 481819818 130990080 27960 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31980 27960 603 41 0 31939 0
vsize: 127920
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29348 0 0 0 58935 71 0 0 25 0 1 0 481819818 130990080 27966 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31980 27966 603 41 0 31939 0
vsize: 127920
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29357 0 0 0 59935 71 0 0 25 0 1 0 481819818 130990080 27975 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31980 27975 603 41 0 31939 0
vsize: 127920
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29362 0 0 0 60936 71 0 0 25 0 1 0 481819818 130990080 27980 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31980 27980 603 41 0 31939 0
vsize: 127920
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29365 0 0 0 61936 71 0 0 25 0 1 0 481819818 130990080 27983 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31980 27983 603 41 0 31939 0
vsize: 127920
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29369 0 0 0 62936 71 0 0 25 0 1 0 481819818 131125248 27987 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32013 27987 603 41 0 31972 0
vsize: 128052
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29373 0 0 0 63936 71 0 0 25 0 1 0 481819818 131125248 27991 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32013 27991 603 41 0 31972 0
vsize: 128052
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29379 0 0 0 64936 71 0 0 25 0 1 0 481819818 131125248 27997 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32013 27997 603 41 0 31972 0
vsize: 128052
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29388 0 0 0 65936 71 0 0 25 0 1 0 481819818 131125248 28006 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32013 28006 603 41 0 31972 0
vsize: 128052
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29396 0 0 0 66936 71 0 0 25 0 1 0 481819818 131125248 28014 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32013 28014 603 41 0 31972 0
vsize: 128052
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29405 0 0 0 67936 71 0 0 25 0 1 0 481819818 131125248 28023 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32013 28023 603 41 0 31972 0
vsize: 128052
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29411 0 0 0 68937 71 0 0 25 0 1 0 481819818 131260416 28029 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32046 28029 603 41 0 32005 0
vsize: 128184
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29425 0 0 0 69937 71 0 0 25 0 1 0 481819818 131260416 28043 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32046 28043 603 41 0 32005 0
vsize: 128184
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29443 0 0 0 70937 71 0 0 25 0 1 0 481819818 131395584 28061 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32079 28061 603 41 0 32038 0
vsize: 128316
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29449 0 0 0 71937 71 0 0 25 0 1 0 481819818 131395584 28067 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32079 28067 603 41 0 32038 0
vsize: 128316
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29456 0 0 0 72937 71 0 0 25 0 1 0 481819818 131395584 28074 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32079 28074 603 41 0 32038 0
vsize: 128316
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29522 0 0 0 73937 71 0 0 25 0 1 0 481819818 131788800 28140 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32175 28140 603 41 0 32134 0
vsize: 128700
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29523 0 0 0 74937 71 0 0 25 0 1 0 481819818 131788800 28141 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32175 28141 603 41 0 32134 0
vsize: 128700
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29526 0 0 0 75938 71 0 0 25 0 1 0 481819818 131788800 28144 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32175 28144 603 41 0 32134 0
vsize: 128700
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29536 0 0 0 76937 71 0 0 25 0 1 0 481819818 131788800 28154 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32175 28154 603 41 0 32134 0
vsize: 128700
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29554 0 0 0 77937 71 0 0 25 0 1 0 481819818 131923968 28172 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32208 28172 603 41 0 32167 0
vsize: 128832
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29563 0 0 0 78937 72 0 0 25 0 1 0 481819818 131923968 28181 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32208 28181 603 41 0 32167 0
vsize: 128832
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29575 0 0 0 79938 72 0 0 25 0 1 0 481819818 131923968 28193 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32208 28193 603 41 0 32167 0
vsize: 128832
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29580 0 0 0 80938 72 0 0 25 0 1 0 481819818 132059136 28198 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32241 28198 603 41 0 32200 0
vsize: 128964
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29590 0 0 0 81938 72 0 0 25 0 1 0 481819818 132059136 28208 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32241 28208 603 41 0 32200 0
vsize: 128964
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29618 0 0 0 82938 72 0 0 25 0 1 0 481819818 132194304 28236 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32274 28236 603 41 0 32233 0
vsize: 129096
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29628 0 0 0 83938 72 0 0 25 0 1 0 481819818 132194304 28246 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32274 28246 603 41 0 32233 0
vsize: 129096
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29640 0 0 0 84939 72 0 0 25 0 1 0 481819818 132194304 28258 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32274 28258 603 41 0 32233 0
vsize: 129096
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29654 0 0 0 85938 72 0 0 25 0 1 0 481819818 132325376 28272 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32306 28272 603 41 0 32265 0
vsize: 129224
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29666 0 0 0 86939 72 0 0 25 0 1 0 481819818 132325376 28284 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32306 28284 603 41 0 32265 0
vsize: 129224
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29672 0 0 0 87939 72 0 0 25 0 1 0 481819818 132325376 28290 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32306 28290 603 41 0 32265 0
vsize: 129224
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29680 0 0 0 88939 72 0 0 25 0 1 0 481819818 132325376 28298 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32306 28298 603 41 0 32265 0
vsize: 129224
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29687 0 0 0 89939 72 0 0 25 0 1 0 481819818 132460544 28305 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32339 28305 603 41 0 32298 0
vsize: 129356
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29705 0 0 0 90939 72 0 0 25 0 1 0 481819818 132460544 28323 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32339 28323 603 41 0 32298 0
vsize: 129356
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29713 0 0 0 91939 72 0 0 25 0 1 0 481819818 132460544 28331 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32339 28331 603 41 0 32298 0
vsize: 129356
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29718 0 0 0 92940 72 0 0 25 0 1 0 481819818 132460544 28336 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32339 28336 603 41 0 32298 0
vsize: 129356
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29733 0 0 0 93940 72 0 0 25 0 1 0 481819818 132595712 28351 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32372 28351 603 41 0 32331 0
vsize: 129488
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29744 0 0 0 94940 72 0 0 25 0 1 0 481819818 132595712 28362 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32372 28362 603 41 0 32331 0
vsize: 129488
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29810 0 0 0 95940 72 0 0 25 0 1 0 481819818 132866048 28428 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32438 28428 603 41 0 32397 0
vsize: 129752
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29826 0 0 0 96940 72 0 0 25 0 1 0 481819818 132997120 28444 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32470 28444 603 41 0 32429 0
vsize: 129880
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29933 0 0 0 97939 72 0 0 25 0 1 0 481819818 133394432 28551 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32567 28551 603 41 0 32526 0
vsize: 130268
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29942 0 0 0 98940 72 0 0 25 0 1 0 481819818 133394432 28560 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32567 28560 603 41 0 32526 0
vsize: 130268
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29954 0 0 0 99940 72 0 0 25 0 1 0 481819818 133394432 28572 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32567 28572 603 41 0 32526 0
vsize: 130268
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29960 0 0 0 100940 73 0 0 25 0 1 0 481819818 133529600 28578 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32600 28578 603 41 0 32559 0
vsize: 130400
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29976 0 0 0 101940 73 0 0 25 0 1 0 481819818 133529600 28594 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32600 28594 603 41 0 32559 0
vsize: 130400
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29981 0 0 0 102940 73 0 0 25 0 1 0 481819818 133529600 28599 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32600 28599 603 41 0 32559 0
vsize: 130400
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 29994 0 0 0 103940 73 0 0 25 0 1 0 481819818 133529600 28612 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32600 28612 603 41 0 32559 0
vsize: 130400
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30012 0 0 0 104940 73 0 0 25 0 1 0 481819818 133664768 28630 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32633 28630 603 41 0 32592 0
vsize: 130532
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30027 0 0 0 105941 73 0 0 25 0 1 0 481819818 133664768 28645 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32633 28645 603 41 0 32592 0
vsize: 130532
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30034 0 0 0 106941 73 0 0 25 0 1 0 481819818 133664768 28652 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32633 28652 603 41 0 32592 0
vsize: 130532
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30050 0 0 0 107941 73 0 0 25 0 1 0 481819818 133799936 28668 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32666 28668 603 41 0 32625 0
vsize: 130664
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30070 0 0 0 108941 73 0 0 25 0 1 0 481819818 133935104 28688 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32699 28688 603 41 0 32658 0
vsize: 130796
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30085 0 0 0 109941 73 0 0 25 0 1 0 481819818 133935104 28703 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32699 28703 603 41 0 32658 0
vsize: 130796
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30100 0 0 0 110941 73 0 0 25 0 1 0 481819818 133935104 28718 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32699 28718 603 41 0 32658 0
vsize: 130796
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30116 0 0 0 111941 73 0 0 25 0 1 0 481819818 134066176 28734 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32731 28734 603 41 0 32690 0
vsize: 130924
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30160 0 0 0 112941 73 0 0 25 0 1 0 481819818 134459392 28778 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32827 28778 603 41 0 32786 0
vsize: 131308
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30166 0 0 0 113942 73 0 0 25 0 1 0 481819818 134459392 28784 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32827 28784 603 41 0 32786 0
vsize: 131308
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30188 0 0 0 114942 73 0 0 25 0 1 0 481819818 134594560 28806 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32860 28806 603 41 0 32819 0
vsize: 131440
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30318 0 0 0 115941 74 0 0 25 0 1 0 481819818 135122944 28936 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32989 28936 603 41 0 32948 0
vsize: 131956
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30330 0 0 0 116941 75 0 0 25 0 1 0 481819818 135122944 28948 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32989 28948 603 41 0 32948 0
vsize: 131956
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30356 0 0 0 117941 75 0 0 25 0 1 0 481819818 135254016 28974 4294967295 134512640 134672761 3221224544 3221223744 134557959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33021 28974 603 41 0 32980 0
vsize: 132084
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30370 0 0 0 118941 75 0 0 25 0 1 0 481819818 135254016 28988 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33021 28988 603 41 0 32980 0
vsize: 132084
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25129
Raw data (stat): 25129 (minisat+) R 25128 29151 29150 0 -1 0 30386 0 0 0 119941 75 0 0 25 0 1 0 481819818 135389184 29004 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33054 29004 603 41 0 33013 0
vsize: 132216
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 25129
Raw data (stat): 25129 (minisat+) Z 25128 29151 29150 0 -1 12 30388 0 0 0 119941 80 0 0 25 0 1 0 481819818 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.23
CPU user time (s): 1199.42
CPU system time (s): 0.809876
CPU usage (%): 100.013
Max. virtual memory (Kb): 132216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####