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 14500

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        679616 kB
Buffers:         31560 kB
Cached:         289368 kB
SwapCached:        508 kB
Active:          56348 kB
Inactive:       266800 kB
HighTotal:      131008 kB
HighFree:         4172 kB
LowTotal:       903652 kB
LowFree:        675444 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            26260 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:24:27 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 19934 7 1200.32 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 |  915400  2172318 |  305133       0        0     nan |  0.000 % |
c |       100 |  915172  2171811 |  335646      59      159     2.7 |  3.284 % |
c |       251 |  915115  2171683 |  369210     206      710     3.4 |  3.287 % |
c |       476 |  914854  2171104 |  406132     385     1364     3.5 |  3.310 % |
c |       813 |  914521  2170366 |  446745     668     2371     3.5 |  3.340 % |
c |      1319 |  914029  2169269 |  491419    1109     3847     3.5 |  3.383 % |
c |      2079 |  913372  2167800 |  540561    1784     6750     3.8 |  3.439 % |
c |      3218 |  911844  2164402 |  594617    2705    10508     3.9 |  3.573 % |
c |      4926 |  910038  2160371 |  654079    4148    16933     4.1 |  3.726 % |
c |      7488 |  907935  2155692 |  719487    6413    33497     5.2 |  3.910 % |
c |     11333 |  904344  2147713 |  791436    9763    50920     5.2 |  4.220 % |
c |     17099 |  900626  2139415 |  870580   15056    80695     5.4 |  4.540 % |
c |     25748 |  893610  2123764 |  957638   22806   126337     5.5 |  5.141 % |
c |     38722 |  885934  2106645 | 1053401   34792   205766     5.9 |  5.799 % |
c |     58185 |  881284  2096233 | 1158742   53643   409642     7.6 |  6.195 % |
#### 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.82 0.94 0.91 2/54 22199
Raw data (stat): 22199 (runsolver) R 22198 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540612901 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.85 0.94 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28232 0 0 0 929 69 0 0 25 0 1 0 540612901 128229376 26850 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31306 26850 603 41 0 31265 0
vsize: 125224
[startup+20.0019 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28252 0 0 0 1929 70 0 0 25 0 1 0 540612901 128229376 26870 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31306 26870 603 41 0 31265 0
vsize: 125224
[startup+30.0017 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28311 0 0 0 2929 70 0 0 25 0 1 0 540612901 128364544 26929 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31339 26929 603 41 0 31298 0
vsize: 125356
[startup+40.0023 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28365 0 0 0 3928 70 0 0 25 0 1 0 540612901 128634880 26983 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31405 26983 603 41 0 31364 0
vsize: 125620
[startup+50.0029 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28421 0 0 0 4929 70 0 0 25 0 1 0 540612901 128770048 27039 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31438 27039 603 41 0 31397 0
vsize: 125752
[startup+60.0035 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28443 0 0 0 5929 70 0 0 25 0 1 0 540612901 128770048 27061 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31438 27061 603 41 0 31397 0
vsize: 125752
[startup+70.004 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28461 0 0 0 6929 71 0 0 25 0 1 0 540612901 128905216 27079 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31471 27079 603 41 0 31430 0
vsize: 125884
[startup+80.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28470 0 0 0 7929 71 0 0 25 0 1 0 540612901 128905216 27088 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31471 27088 603 41 0 31430 0
vsize: 125884
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28491 0 0 0 8929 71 0 0 25 0 1 0 540612901 128905216 27109 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31471 27109 603 41 0 31430 0
vsize: 125884
[startup+100.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28500 0 0 0 9929 71 0 0 25 0 1 0 540612901 129040384 27118 4294967295 134512640 134672761 3221224624 3221223840 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31504 27118 603 41 0 31463 0
vsize: 126016
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22199
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28538 0 0 0 10929 71 0 0 25 0 1 0 540612901 129040384 27156 4294967295 134512640 134672761 3221224624 3221223840 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31504 27156 603 41 0 31463 0
vsize: 126016
[startup+120.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28570 0 0 0 11929 71 0 0 25 0 1 0 540612901 129175552 27188 4294967295 134512640 134672761 3221224624 3221223748 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31537 27188 603 41 0 31496 0
vsize: 126148
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28579 0 0 0 12929 71 0 0 25 0 1 0 540612901 129175552 27197 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31537 27197 603 41 0 31496 0
vsize: 126148
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28591 0 0 0 13929 72 0 0 25 0 1 0 540612901 129318912 27209 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31572 27209 603 41 0 31531 0
vsize: 126288
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28618 0 0 0 14929 72 0 0 25 0 1 0 540612901 129318912 27236 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31572 27236 603 41 0 31531 0
vsize: 126288
[startup+160.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28626 0 0 0 15929 72 0 0 25 0 1 0 540612901 129318912 27244 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31572 27244 603 41 0 31531 0
vsize: 126288
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28646 0 0 0 16929 72 0 0 25 0 1 0 540612901 129454080 27264 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31605 27264 603 41 0 31564 0
vsize: 126420
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28657 0 0 0 17930 72 0 0 25 0 1 0 540612901 129454080 27275 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31605 27275 603 41 0 31564 0
vsize: 126420
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28669 0 0 0 18929 72 0 0 25 0 1 0 540612901 129454080 27287 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31605 27287 603 41 0 31564 0
vsize: 126420
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28672 0 0 0 19930 72 0 0 25 0 1 0 540612901 129454080 27290 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31605 27290 603 41 0 31564 0
vsize: 126420
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28690 0 0 0 20930 72 0 0 25 0 1 0 540612901 129589248 27308 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31638 27308 603 41 0 31597 0
vsize: 126552
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28695 0 0 0 21930 72 0 0 25 0 1 0 540612901 129589248 27313 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31638 27313 603 41 0 31597 0
vsize: 126552
[startup+230.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28699 0 0 0 22931 72 0 0 25 0 1 0 540612901 129589248 27317 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31638 27317 603 41 0 31597 0
vsize: 126552
[startup+240.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28703 0 0 0 23931 72 0 0 25 0 1 0 540612901 129589248 27321 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31638 27321 603 41 0 31597 0
vsize: 126552
[startup+250.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28710 0 0 0 24931 72 0 0 25 0 1 0 540612901 129589248 27328 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31638 27328 603 41 0 31597 0
vsize: 126552
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28733 0 0 0 25931 72 0 0 25 0 1 0 540612901 129724416 27351 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31671 27351 603 41 0 31630 0
vsize: 126684
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28755 0 0 0 26931 73 0 0 25 0 1 0 540612901 129724416 27373 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31671 27373 603 41 0 31630 0
vsize: 126684
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28765 0 0 0 27931 73 0 0 25 0 1 0 540612901 129859584 27383 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31704 27383 603 41 0 31663 0
vsize: 126816
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28773 0 0 0 28932 73 0 0 25 0 1 0 540612901 129859584 27391 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31704 27391 603 41 0 31663 0
vsize: 126816
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28781 0 0 0 29931 73 0 0 25 0 1 0 540612901 129859584 27399 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31704 27399 603 41 0 31663 0
vsize: 126816
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28787 0 0 0 30931 73 0 0 25 0 1 0 540612901 129859584 27405 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31704 27405 603 41 0 31663 0
vsize: 126816
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28804 0 0 0 31932 73 0 0 25 0 1 0 540612901 129859584 27422 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31704 27422 603 41 0 31663 0
vsize: 126816
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28808 0 0 0 32932 73 0 0 25 0 1 0 540612901 129994752 27426 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31737 27426 603 41 0 31696 0
vsize: 126948
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28825 0 0 0 33932 73 0 0 25 0 1 0 540612901 129994752 27443 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31737 27443 603 41 0 31696 0
vsize: 126948
[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28831 0 0 0 34933 73 0 0 25 0 1 0 540612901 129994752 27449 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31737 27449 603 41 0 31696 0
vsize: 126948
[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28855 0 0 0 35933 73 0 0 25 0 1 0 540612901 129994752 27473 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31737 27473 603 41 0 31696 0
vsize: 126948
[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28865 0 0 0 36933 73 0 0 25 0 1 0 540612901 130129920 27483 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31770 27483 603 41 0 31729 0
vsize: 127080
[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28868 0 0 0 37933 73 0 0 25 0 1 0 540612901 130129920 27486 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31770 27486 603 41 0 31729 0
vsize: 127080
[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28874 0 0 0 38933 73 0 0 25 0 1 0 540612901 130129920 27492 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31770 27492 603 41 0 31729 0
vsize: 127080
[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28884 0 0 0 39933 73 0 0 25 0 1 0 540612901 130129920 27502 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31770 27502 603 41 0 31729 0
vsize: 127080
[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28894 0 0 0 40934 73 0 0 25 0 1 0 540612901 130260992 27512 4294967295 134512640 134672761 3221224624 3221223776 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31802 27512 603 41 0 31761 0
vsize: 127208
[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28899 0 0 0 41934 73 0 0 25 0 1 0 540612901 130260992 27517 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31802 27517 603 41 0 31761 0
vsize: 127208
[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28917 0 0 0 42934 73 0 0 25 0 1 0 540612901 130260992 27535 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31802 27535 603 41 0 31761 0
vsize: 127208
[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28920 0 0 0 43934 74 0 0 25 0 1 0 540612901 130260992 27538 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31802 27538 603 41 0 31761 0
vsize: 127208
[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28937 0 0 0 44934 74 0 0 25 0 1 0 540612901 130473984 27555 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31854 27555 603 41 0 31813 0
vsize: 127416
[startup+460.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28938 0 0 0 45934 74 0 0 25 0 1 0 540612901 130473984 27556 4294967295 134512640 134672761 3221224624 3221223796 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31854 27556 603 41 0 31813 0
vsize: 127416
[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28944 0 0 0 46934 74 0 0 25 0 1 0 540612901 130473984 27562 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31854 27562 603 41 0 31813 0
vsize: 127416
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28954 0 0 0 47935 74 0 0 25 0 1 0 540612901 130473984 27572 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31854 27572 603 41 0 31813 0
vsize: 127416
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28964 0 0 0 48935 74 0 0 25 0 1 0 540612901 130473984 27582 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31854 27582 603 41 0 31813 0
vsize: 127416
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28974 0 0 0 49935 74 0 0 25 0 1 0 540612901 130473984 27592 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31854 27592 603 41 0 31813 0
vsize: 127416
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28975 0 0 0 50935 74 0 0 25 0 1 0 540612901 130473984 27593 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31854 27593 603 41 0 31813 0
vsize: 127416
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28982 0 0 0 51935 74 0 0 25 0 1 0 540612901 130609152 27600 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27600 603 41 0 31846 0
vsize: 127548
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28984 0 0 0 52935 74 0 0 25 0 1 0 540612901 130609152 27602 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27602 603 41 0 31846 0
vsize: 127548
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28988 0 0 0 53936 74 0 0 25 0 1 0 540612901 130609152 27606 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27606 603 41 0 31846 0
vsize: 127548
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28994 0 0 0 54936 74 0 0 25 0 1 0 540612901 130609152 27612 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27612 603 41 0 31846 0
vsize: 127548
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 28995 0 0 0 55936 74 0 0 25 0 1 0 540612901 130609152 27613 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27613 603 41 0 31846 0
vsize: 127548
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29001 0 0 0 56936 74 0 0 25 0 1 0 540612901 130609152 27619 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27619 603 41 0 31846 0
vsize: 127548
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29003 0 0 0 57936 75 0 0 25 0 1 0 540612901 130609152 27621 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27621 603 41 0 31846 0
vsize: 127548
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29006 0 0 0 58936 75 0 0 25 0 1 0 540612901 130609152 27624 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27624 603 41 0 31846 0
vsize: 127548
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29009 0 0 0 59936 75 0 0 25 0 1 0 540612901 130609152 27627 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31887 27627 603 41 0 31846 0
vsize: 127548
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29039 0 0 0 60936 75 0 0 25 0 1 0 540612901 130744320 27657 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31920 27657 603 41 0 31879 0
vsize: 127680
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29041 0 0 0 61936 75 0 0 25 0 1 0 540612901 130744320 27659 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31920 27659 603 41 0 31879 0
vsize: 127680
[startup+630.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29046 0 0 0 62936 75 0 0 25 0 1 0 540612901 130744320 27664 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31920 27664 603 41 0 31879 0
vsize: 127680
[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29054 0 0 0 63936 75 0 0 25 0 1 0 540612901 130744320 27672 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31920 27672 603 41 0 31879 0
vsize: 127680
[startup+650.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29062 0 0 0 64936 75 0 0 25 0 1 0 540612901 130744320 27680 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31920 27680 603 41 0 31879 0
vsize: 127680
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29067 0 0 0 65936 75 0 0 25 0 1 0 540612901 130744320 27685 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31920 27685 603 41 0 31879 0
vsize: 127680
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29073 0 0 0 66937 75 0 0 25 0 1 0 540612901 130879488 27691 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31953 27691 603 41 0 31912 0
vsize: 127812
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29077 0 0 0 67937 75 0 0 25 0 1 0 540612901 130879488 27695 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31953 27695 603 41 0 31912 0
vsize: 127812
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29085 0 0 0 68937 75 0 0 25 0 1 0 540612901 130879488 27703 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31953 27703 603 41 0 31912 0
vsize: 127812
[startup+700.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29090 0 0 0 69938 75 0 0 25 0 1 0 540612901 130879488 27708 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31953 27708 603 41 0 31912 0
vsize: 127812
[startup+710.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29098 0 0 0 70939 75 0 0 25 0 1 0 540612901 130879488 27716 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31953 27716 603 41 0 31912 0
vsize: 127812
[startup+720.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29105 0 0 0 71939 75 0 0 25 0 1 0 540612901 130879488 27723 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31953 27723 603 41 0 31912 0
vsize: 127812
[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29109 0 0 0 72939 75 0 0 25 0 1 0 540612901 131014656 27727 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31986 27727 603 41 0 31945 0
vsize: 127944
[startup+740.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29113 0 0 0 73941 76 0 0 25 0 1 0 540612901 131014656 27731 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31986 27731 603 41 0 31945 0
vsize: 127944
[startup+750.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29116 0 0 0 74941 76 0 0 25 0 1 0 540612901 131014656 27734 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31986 27734 603 41 0 31945 0
vsize: 127944
[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29121 0 0 0 75941 76 0 0 25 0 1 0 540612901 131014656 27739 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31986 27739 603 41 0 31945 0
vsize: 127944
[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29133 0 0 0 76942 76 0 0 25 0 1 0 540612901 131014656 27751 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31986 27751 603 41 0 31945 0
vsize: 127944
[startup+780.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29138 0 0 0 77942 76 0 0 25 0 1 0 540612901 131014656 27756 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31986 27756 603 41 0 31945 0
vsize: 127944
[startup+790.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29144 0 0 0 78942 76 0 0 25 0 1 0 540612901 131149824 27762 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32019 27762 603 41 0 31978 0
vsize: 128076
[startup+800.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29152 0 0 0 79943 76 0 0 25 0 1 0 540612901 131149824 27770 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32019 27770 603 41 0 31978 0
vsize: 128076
[startup+810.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29160 0 0 0 80943 76 0 0 25 0 1 0 540612901 131149824 27778 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32019 27778 603 41 0 31978 0
vsize: 128076
[startup+820.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29167 0 0 0 81943 76 0 0 25 0 1 0 540612901 131149824 27785 4294967295 134512640 134672761 3221224624 3221223760 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32019 27785 603 41 0 31978 0
vsize: 128076
[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29173 0 0 0 82943 76 0 0 25 0 1 0 540612901 131149824 27791 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32019 27791 603 41 0 31978 0
vsize: 128076
[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29208 0 0 0 83943 76 0 0 25 0 1 0 540612901 131411968 27826 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32083 27826 603 41 0 32042 0
vsize: 128332
[startup+850.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29208 0 0 0 84943 76 0 0 25 0 1 0 540612901 131411968 27826 4294967295 134512640 134672761 3221224624 3221223780 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32083 27826 603 41 0 32042 0
vsize: 128332
[startup+860.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29209 0 0 0 85944 76 0 0 25 0 1 0 540612901 131411968 27827 4294967295 134512640 134672761 3221224624 3221223792 134561259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32083 27827 603 41 0 32042 0
vsize: 128332
[startup+870.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29209 0 0 0 86944 76 0 0 25 0 1 0 540612901 131411968 27827 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32083 27827 603 41 0 32042 0
vsize: 128332
[startup+880.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29214 0 0 0 87944 76 0 0 25 0 1 0 540612901 131411968 27832 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32083 27832 603 41 0 32042 0
vsize: 128332
[startup+890.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29217 0 0 0 88944 76 0 0 25 0 1 0 540612901 131547136 27835 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32116 27835 603 41 0 32075 0
vsize: 128464
[startup+900.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29228 0 0 0 89944 76 0 0 25 0 1 0 540612901 131547136 27846 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32116 27846 603 41 0 32075 0
vsize: 128464
[startup+910.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29235 0 0 0 90944 76 0 0 25 0 1 0 540612901 131547136 27853 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32116 27853 603 41 0 32075 0
vsize: 128464
[startup+920.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29249 0 0 0 91944 76 0 0 25 0 1 0 540612901 131547136 27867 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32116 27867 603 41 0 32075 0
vsize: 128464
[startup+930.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29259 0 0 0 92944 77 0 0 25 0 1 0 540612901 131682304 27877 4294967295 134512640 134672761 3221224624 3221223796 134556661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32149 27877 603 41 0 32108 0
vsize: 128596
[startup+940.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29265 0 0 0 93944 77 0 0 25 0 1 0 540612901 131682304 27883 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32149 27883 603 41 0 32108 0
vsize: 128596
[startup+950.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29272 0 0 0 94945 77 0 0 25 0 1 0 540612901 131682304 27890 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32149 27890 603 41 0 32108 0
vsize: 128596
[startup+960.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29280 0 0 0 95945 77 0 0 25 0 1 0 540612901 131682304 27898 4294967295 134512640 134672761 3221224624 3221223792 134564755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32149 27898 603 41 0 32108 0
vsize: 128596
[startup+970.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29356 0 0 0 96945 77 0 0 25 0 1 0 540612901 132087808 27974 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32248 27974 603 41 0 32207 0
vsize: 128992
[startup+980.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29389 0 0 0 97945 77 0 0 25 0 1 0 540612901 132087808 28007 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32248 28007 603 41 0 32207 0
vsize: 128992
[startup+990.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29402 0 0 0 98945 77 0 0 25 0 1 0 540612901 132218880 28020 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32280 28020 603 41 0 32239 0
vsize: 129120
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29452 0 0 0 99944 78 0 0 25 0 1 0 540612901 132354048 28070 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32313 28070 603 41 0 32272 0
vsize: 129252
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29460 0 0 0 100944 78 0 0 25 0 1 0 540612901 132489216 28078 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32346 28078 603 41 0 32305 0
vsize: 129384
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29470 0 0 0 101945 78 0 0 25 0 1 0 540612901 132489216 28088 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32346 28088 603 41 0 32305 0
vsize: 129384
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29482 0 0 0 102945 78 0 0 25 0 1 0 540612901 132489216 28100 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32346 28100 603 41 0 32305 0
vsize: 129384
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29493 0 0 0 103945 78 0 0 25 0 1 0 540612901 132624384 28111 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32379 28111 603 41 0 32338 0
vsize: 129516
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29509 0 0 0 104945 78 0 0 25 0 1 0 540612901 132624384 28127 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32379 28127 603 41 0 32338 0
vsize: 129516
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29522 0 0 0 105945 78 0 0 25 0 1 0 540612901 132624384 28140 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32379 28140 603 41 0 32338 0
vsize: 129516
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29529 0 0 0 106945 78 0 0 25 0 1 0 540612901 132759552 28147 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32412 28147 603 41 0 32371 0
vsize: 129648
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29535 0 0 0 107945 78 0 0 25 0 1 0 540612901 132759552 28153 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32412 28153 603 41 0 32371 0
vsize: 129648
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29544 0 0 0 108946 78 0 0 25 0 1 0 540612901 132759552 28162 4294967295 134512640 134672761 3221224624 3221223796 134556669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32412 28162 603 41 0 32371 0
vsize: 129648
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29555 0 0 0 109946 78 0 0 25 0 1 0 540612901 132759552 28173 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32412 28173 603 41 0 32371 0
vsize: 129648
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29563 0 0 0 110945 78 0 0 25 0 1 0 540612901 132759552 28181 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32412 28181 603 41 0 32371 0
vsize: 129648
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29569 0 0 0 111944 79 0 0 25 0 1 0 540612901 132894720 28187 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32445 28187 603 41 0 32404 0
vsize: 129780
[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29578 0 0 0 112945 79 0 0 25 0 1 0 540612901 132894720 28196 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32445 28196 603 41 0 32404 0
vsize: 129780
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29587 0 0 0 113945 79 0 0 25 0 1 0 540612901 132894720 28205 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32445 28205 603 41 0 32404 0
vsize: 129780
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29612 0 0 0 114945 79 0 0 25 0 1 0 540612901 133029888 28230 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32478 28230 603 41 0 32437 0
vsize: 129912
[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29632 0 0 0 115945 79 0 0 25 0 1 0 540612901 133029888 28250 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32478 28250 603 41 0 32437 0
vsize: 129912
[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29647 0 0 0 116944 80 0 0 25 0 1 0 540612901 133165056 28265 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32511 28265 603 41 0 32470 0
vsize: 130044
[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29754 0 0 0 117944 80 0 0 25 0 1 0 540612901 133566464 28372 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32609 28372 603 41 0 32568 0
vsize: 130436
[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29778 0 0 0 118945 80 0 0 25 0 1 0 540612901 133701632 28396 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32642 28396 603 41 0 32601 0
vsize: 130568
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22201
Raw data (stat): 22199 (minisat+) R 22198 28546 28545 0 -1 0 29794 0 0 0 119945 80 0 0 25 0 1 0 540612901 133701632 28412 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32642 28412 603 41 0 32601 0
vsize: 130568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22201
Raw data (stat): 22199 (minisat+) Z 22198 28546 28545 0 -1 12 29796 0 0 0 119945 86 0 0 25 0 1 0 540612901 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.32
CPU user time (s): 1199.45
CPU system time (s): 0.865868
CPU usage (%): 100.014
Max. virtual memory (Kb): 130568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####