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 13965

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        446464 kB
Buffers:         35604 kB
Cached:         529200 kB
SwapCached:          4 kB
Active:         232484 kB
Inactive:       335116 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        446212 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14884 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:49:13 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 19940 7 1200.34 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  944399  2236028 |  283319       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/322928          
c   -- var.elim.:  2000/322928          
c   -- var.elim.:  3000/322928          
c   -- var.elim.:  4000/322928          
c   -- var.elim.:  5000/322928          
c   -- var.elim.:  6000/322928          
c   -- var.elim.:  7000/322928          
c   -- var.elim.:  8000/322928          
c   -- var.elim.:  9000/322928          
c   -- var.elim.:  10000/322928          
c   -- var.elim.:  11000/322928          
c   -- var.elim.:  12000/322928          
c   -- var.elim.:  13000/322928          
c   -- var.elim.:  14000/322928          
c   -- var.elim.:  15000/322928          
c   -- var.elim.:  16000/322928          
c   -- var.elim.:  17000/322928          
c   -- var.elim.:  18000/322928          
c   -- var.elim.:  19000/322928          
c   -- var.elim.:  20000/322928          
c   -- var.elim.:  21000/322928          
c   -- var.elim.:  22000/322928          
c   -- var.elim.:  23000/322928          
c   -- var.elim.:  24000/322928          
c   -- var.elim.:  25000/322928          
c   -- var.elim.:  26000/322928          
c   -- var.elim.:  27000/322928          
c   -- var.elim.:  28000/322928          
c   -- var.elim.:  29000/322928          
c   -- var.elim.:  30000/322928          
c   -- var.elim.:  31000/322928          
c   -- var.elim.:  32000/322928          
c   -- var.elim.:  33000/322928          
c   -- var.elim.:  34000/322928          
c   -- var.elim.:  35000/322928          
c   -- var.elim.:  36000/322928          
c   -- var.elim.:  37000/322928          
c   -- var.elim.:  38000/322928          
c   -- var.elim.:  39000/322928          
c   -- var.elim.:  40000/322928          
c   -- var.elim.:  41000/322928          
c   -- var.elim.:  42000/322928          
c   -- var.elim.:  43000/322928          
c   -- var.elim.:  44000/322928          
c   -- var.elim.:  45000/322928          
c   -- var.elim.:  46000/322928          
c   -- var.elim.:  47000/322928          
c   -- var.elim.:  48000/322928          
c   -- var.elim.:  49000/322928          
c   -- var.elim.:  50000/322928          
c   -- var.elim.:  51000/322928          
c   -- var.elim.:  52000/322928          
c   -- var.elim.:  53000/322928          
c   -- var.elim.:  54000/322928          
c   -- var.elim.:  55000/322928          
c   -- var.elim.:  56000/322928          
c   -- var.elim.:  57000/322928          
c   -- var.elim.:  58000/322928          
c   -- var.elim.:  59000/322928          
c   -- var.elim.:  60000/322928          
c   -- var.elim.:  61000/322928          
c   -- var.elim.:  62000/322928          
c   -- var.elim.:  63000/322928          
c   -- var.elim.:  64000/322928          
c   -- var.elim.:  65000/322928          
c   -- var.elim.:  66000/322928          
c   -- var.elim.:  67000/322928          
c   -- var.elim.:  68000/322928          
c   -- var.elim.:  69000/322928          
c   -- var.elim.:  70000/322928          
c   -- var.elim.:  71000/322928          
c   -- var.elim.:  72000/322928          
c   -- var.elim.:  73000/322928          
c   -- var.elim.:  74000/322928          
c   -- var.elim.:  75000/322928          
c   -- var.elim.:  76000/322928          
c   -- var.elim.:  77000/322928          
c   -- var.elim.:  78000/322928          
c   -- var.elim.:  79000/322928          
c   -- var.elim.:  80000/322928          
c   -- var.elim.:  81000/322928          
c   -- var.elim.:  82000/322928          
c   -- var.elim.:  83000/322928          
c   -- var.elim.:  84000/322928          
c   -- var.elim.:  85000/322928          
c   -- var.elim.:  86000/322928          
c   -- var.elim.:  87000/322928          
c   -- var.elim.:  88000/322928          
c   -- var.elim.:  89000/322928          
c   -- var.elim.:  90000/322928          
c   -- var.elim.:  91000/322928          
c   -- var.elim.:  92000/322928          
c   -- var.elim.:  93000/322928          
c   -- var.elim.:  94000/322928          
c   -- var.elim.:  95000/322928          
c   -- var.elim.:  96000/322928          
c   -- var.elim.:  97000/322928          
c   -- var.elim.:  98000/322928          
c   -- var.elim.:  99000/322928          
c   -- var.elim.:  100000/322928          
c   -- var.elim.:  101000/322928          
c   -- var.elim.:  102000/322928          
c   -- var.elim.:  103000/322928          
c   -- var.elim.:  104000/322928          
c   -- var.elim.:  105000/322928          
c   -- var.elim.:  106000/322928          
c   -- var.elim.:  107000/322928          
c   -- var.elim.:  108000/322928          
c   -- var.elim.:  109000/322928          
c   -- var.elim.:  110000/322928          
c   -- var.elim.:  111000/322928          
c   -- var.elim.:  112000/322928          
c   -- var.elim.:  113000/322928          
c   -- var.elim.:  114000/322928          
c   -- var.elim.:  115000/322928          
c   -- var.elim.:  116000/322928          
c   -- var.elim.:  117000/322928          
c   -- var.elim.:  118000/322928          
c   -- var.elim.:  119000/322928          
c   -- var.elim.:  120000/322928          
c   -- var.elim.:  121000/322928          
c   -- var.elim.:  122000/322928          
c   -- var.elim.:  123000/322928          
c   -- var.elim.:  124000/322928          
c   -- var.elim.:  125000/322928          
c   -- var.elim.:  126000/322928          
c   -- var.elim.:  127000/322928          
c   -- var.elim.:  128000/322928          
c   -- var.elim.:  129000/322928          
c   -- var.elim.:  130000/322928          
c   -- var.elim.:  131000/322928          
c   -- var.elim.:  132000/322928          
c   -- var.elim.:  133000/322928          
c   -- var.elim.:  134000/322928          
c   -- var.elim.:  135000/322928          
c   -- var.elim.:  136000/322928          
c   -- var.elim.:  137000/322928          
c   -- var.elim.:  138000/322928          
c   -- var.elim.:  139000/322928          
c   -- var.elim.:  140000/322928          
c   -- var.elim.:  141000/322928          
c   -- var.elim.:  142000/322928          
c   -- var.elim.:  143000/322928          
c   -- var.elim.:  144000/322928          
c   -- var.elim.:  145000/322928          
c   -- var.elim.:  146000/322928          
c   -- var.elim.:  147000/322928          
c   -- var.elim.:  148000/322928          
c   -- var.elim.:  149000/322928          
c   -- var.elim.:  150000/322928          
c   -- var.elim.:  151000/322928          
c   -- var.elim.:  152000/322928          
c   -- var.elim.:  153000/322928          
c   -- var.elim.:  154000/322928          
c   -- var.elim.:  155000/322928          
c   -- var.elim.:  156000/322928          
c   -- var.elim.:  157000/322928          
c   -- var.elim.:  158000/322928          
c   -- var.elim.:  159000/322928          
c   -- var.elim.:  160000/322928          
c   -- var.elim.:  161000/322928          
c   -- var.elim.:  162000/322928          
c   -- var.elim.:  163000/322928          
c   -- var.elim.:  164000/322928          
c   -- var.elim.:  165000/322928          
c   -- var.elim.:  166000/322928          
c   -- var.elim.:  167000/322928          
c   -- var.elim.:  168000/322928          
c   -- var.elim.:  169000/322928          
c   -- var.elim.:  170000/322928          
c   -- var.elim.:  171000/322928          
c   -- var.elim.:  172000/322928          
c   -- var.elim.:  173000/322928          
c   -- var.elim.:  174000/322928          
c   -- var.elim.:  175000/322928          
c   -- var.elim.:  176000/322928          
c   -- var.elim.:  177000/322928          
c   -- var.elim.:  178000/322928          
c   -- var.elim.:  179000/322928          
c   -- var.elim.:  180000/322928          
c   -- var.elim.:  181000/322928          
c   -- var.elim.:  182000/322928          
c   -- var.elim.:  183000/322928          
c   -- var.elim.:  184000/322928          
c   -- var.elim.:  185000/322928          
c   -- var.elim.:  186000/322928          
c   -- var.elim.:  187000/322928          
c   -- var.elim.:  188000/322928          
c   -- var.elim.:  189000/322928          
c   -- var.elim.:  190000/322928          
c   -- var.elim.:  191000/322928          
c   -- var.elim.:  192000/322928          
c   -- var.elim.:  193000/322928          
c   -- var.elim.:  194000/322928          
c   -- var.elim.:  195000/322928          
c   -- var.elim.:  196000/322928          
c   -- var.elim.:  197000/322928          
c   -- var.elim.:  198000/322928          
c   -- var.elim.:  199000/322928          
c   -- var.elim.:  200000/322928          
c   -- var.elim.:  201000/322928          
c   -- var.elim.:  202000/322928          
c   -- var.elim.:  203000/322928          
c   -- var.elim.:  204000/322928          
c   -- var.elim.:  205000/322928          
c   -- var.elim.:  206000/322928          
c   -- var.elim.:  207000/322928          
c   -- var.elim.:  208000/322928          
c   -- var.elim.:  209000/322928          
c   -- var.elim.:  210000/322928          
c   -- var.elim.:  211000/322928          
c   -- var.elim.:  212000/322928          
c   -- var.elim.:  213000/322928          
c   -- var.elim.:  214000/322928          
c   -- var.elim.:  215000/322928          
c   -- var.elim.:  216000/322928          
c   -- var.elim.:  217000/322928          
c   -- var.elim.:  218000/322928          
c   -- var.elim.:  219000/322928          
c   -- var.elim.:  220000/322928          
c   -- var.elim.:  221000/322928          
c   -- var.elim.:  222000/322928          
c   -- var.elim.:  223000/322928          
c   -- var.elim.:  224000/322928          
c   -- var.elim.:  225000/322928          
c   -- var.elim.:  226000/322928          
c   -- var.elim.:  227000/322928          
c   -- var.elim.:  228000/322928          
c   -- var.elim.:  229000/322928          
c   -- var.elim.:  230000/322928          
c   -- var.elim.:  231000/322928          
c   -- var.elim.:  232000/322928          
c   -- var.elim.:  233000/322928          
c   -- var.elim.:  234000/322928          
c   -- var.elim.:  235000/322928          
c   -- var.elim.:  236000/322928          
c   -- var.elim.:  237000/322928          
c   -- var.elim.:  238000/322928          
c   -- var.elim.:  239000/322928          
c   -- var.elim.:  240000/322928          
c   -- var.elim.:  241000/322928          
c   -- var.elim.:  242000/322928          
c   -- var.elim.:  243000/322928          
c   -- var.elim.:  244000/322928          
c   -- var.elim.:  245000/322928          
c   -- var.elim.:  246000/322928          
c   -- var.elim.:  247000/322928          
c   -- var.elim.:  248000/322928          
c   -- var.elim.:  249000/322928          
c   -- var.elim.:  250000/322928          
c   -- var.elim.:  251000/322928          
c   -- var.elim.:  252000/322928          
c   -- var.elim.:  253000/322928          
c   -- var.elim.:  254000/322928          
c   -- var.elim.:  255000/322928          
c   -- var.elim.:  256000/322928          
c   -- var.elim.:  257000/322928          
c   -- var.elim.:  258000/322928          
c   -- var.elim.:  259000/322928          
c   -- var.elim.:  260000/322928          
c   -- var.elim.:  261000/322928          
c   -- var.elim.:  262000/322928          
c   -- var.elim.:  263000/322928          
c   -- var.elim.:  264000/322928          
c   -- var.elim.:  265000/322928          
c   -- var.elim.:  266000/322928          
c   -- var.elim.:  267000/322928          
c   -- var.elim.:  268000/322928          
c   -- var.elim.:  269000/322928          
c   -- var.elim.:  270000/322928          
c   -- var.elim.:  271000/322928          
c   -- var.elim.:  272000/322928          
c   -- var.elim.:  273000/322928          
c   -- var.elim.:  274000/322928          
c   -- var.elim.:  275000/322928          
c   -- var.elim.:  276000/322928          
c   -- var.elim.:  277000/322928          
c   -- var.elim.:  278000/322928          
c   -- var.elim.:  279000/322928          
c   -- var.elim.:  280000/322928          
c   -- var.elim.:  281000/322928          
c   -- var.elim.:  282000/322928          
c   -- var.elim.:  283000/322928          
c   -- var.elim.:  284000/322928          
c   -- var.elim.:  285000/322928          
c   -- var.elim.:  286000/322928          
c   -- var.elim.:  287000/322928          
c   -- var.elim.:  288000/322928          
c   -- var.elim.:  289000/322928          
c   -- var.elim.:  290000/322928          
c   -- var.elim.:  291000/322928          
c   -- var.elim.:  292000/322928          
c   -- var.elim.:  293000/322928          
c   -- var.elim.:  294000/322928          
c   -- var.elim.:  295000/322928          
c   -- var.elim.:  296000/322928          
c   -- var.elim.:  297000/322928          
c   -- var.elim.:  298000/322928          
c   -- var.elim.:  299000/322928          
c   -- var.elim.:  300000/322928          
c   -- var.elim.:  301000/322928          
c   -- var.elim.:  302000/322928          
c   -- var.elim.:  303000/322928          
c   -- var.elim.:  304000/322928          
c   -- var.elim.:  305000/322928          
c   -- var.elim.:  306000/322928          
c   -- var.elim.:  307000/322928          
c   -- var.elim.:  308000/322928          
c   -- var.elim.:  309000/322928          
c   -- var.elim.:  310000/322928          
c   -- var.elim.:  311000/322928          
c   -- var.elim.:  312000/322928          
c   -- var.elim.:  313000/322928          
c   -- var.elim.:  314000/322928          
c   -- var.elim.:  315000/322928          
c   -- var.elim.:  316000/322928          
c   -- var.elim.:  317000/322928          
c   -- var.elim.:  318000/322928          
c   -- var.elim.:  319000/322928          
c   -- var.elim.:  320000/322928          
c   -- var.elim.:  321000/322928          
c   -- var.elim.:  322000/322928          
c   -- var.elim.:  322928/322928          
c   -- var.elim.:  1000/175009          
c   -- var.elim.:  2000/175009          
c   -- var.elim.:  3000/175009          
c   -- var.elim.:  4000/175009          
c   -- var.elim.:  5000/175009          
c   -- var.elim.:  6000/175009          
c   -- var.elim.:  7000/175009          
c   -- var.elim.:  8000/175009          
c   -- var.elim.:  9000/175009          
c   -- var.elim.:  10000/175009          
c   -- var.elim.:  11000/175009          
c   -- var.elim.:  12000/175009          
c   -- var.elim.:  13000/175009          
c   -- var.elim.:  14000/175009          
c   -- var.elim.:  15000/175009          
c   -- var.elim.:  16000/175009          
c   -- var.elim.:  17000/175009          
c   -- var.elim.:  18000/175009          
c   -- var.elim.:  19000/175009          
c   -- var.elim.:  20000/175009          
c   -- var.elim.:  21000/175009          
c   -- var.elim.:  22000/175009          
c   -- var.elim.:  23000/175009          
c   -- var.elim.:  24000/175009          
c   -- var.elim.:  25000/175009          
c   -- var.elim.:  26000/175009          
c   -- var.elim.:  27000/175009          
c   -- var.elim.:  28000/175009          
c   -- var.elim.:  29000/175009          
c   -- var.elim.:  30000/175009          
c   -- var.elim.:  31000/175009          
c   -- var.elim.:  32000/175009          
c   -- var.elim.:  33000/175009          
c   -- var.elim.:  34000/175009          
c   -- var.elim.:  35000/175009          
c   -- var.elim.:  36000/175009          
c   -- var.elim.:  37000/175009          
c   -- var.elim.:  38000/175009          
c   -- var.elim.:  39000/175009          
c   -- var.elim.:  40000/175009          
c   -- var.elim.:  41000/175009          
c   -- var.elim.:  42000/175009          
c   -- var.elim.:  43000/175009          
c   -- var.elim.:  44000/175009          
c   -- var.elim.:  45000/175009          
c   -- var.elim.:  46000/175009          
c   -- var.elim.:  47000/175009          
c   -- var.elim.:  48000/175009          
c   -- var.elim.:  49000/175009          
c   -- var.elim.:  50000/175009          
c   -- var.elim.:  51000/175009          
c   -- var.elim.:  52000/175009          
c   -- var.elim.:  53000/175009          
c   -- var.elim.:  54000/175009          
c   -- var.elim.:  55000/175009          
c   -- var.elim.:  56000/175009          
c   -- var.elim.:  57000/175009          
c   -- var.elim.:  58000/175009          
c   -- var.elim.:  59000/175009          
c   -- var.elim.:  60000/175009          
c   -- var.elim.:  61000/175009          
c   -- var.elim.:  62000/175009          
c   -- var.elim.:  63000/175009          
c   -- var.elim.:  64000/175009          
c   -- var.elim.:  65000/175009          
c   -- var.elim.:  66000/175009          
c   -- var.elim.:  67000/175009          
c   -- var.elim.:  68000/175009          
c   -- var.elim.:  69000/175009          
c   -- var.elim.:  70000/175009          
c   -- var.elim.:  71000/175009          
c   -- var.elim.:  72000/175009          
c   -- var.elim.:  73000/175009          
c   -- var.elim.:  74000/175009          
c   -- var.elim.:  75000/175009          
c   -- var.elim.:  76000/175009          
c   -- var.elim.:  77000/175009          
c   -- var.elim.:  78000/175009          
c   -- var.elim.:  79000/175009          
c   -- var.elim.:  80000/175009          
c   -- var.elim.:  81000/175009          
c   -- var.elim.:  82000/175009          
c   -- var.elim.:  83000/175009          
c   -- var.elim.:  84000/175009          
c   -- var.elim.:  85000/175009          
c   -- var.elim.:  86000/175009          
c   -- var.elim.:  87000/175009          
c   -- var.elim.:  88000/175009          
c   -- var.elim.:  89000/175009          
c   -- var.elim.:  90000/175009          
c   -- var.elim.:  91000/175009          
c   -- var.elim.:  92000/175009          
c   -- var.elim.:  93000/175009          
c   -- var.elim.:  94000/175009          
c   -- var.elim.:  95000/175009          
c   -- var.elim.:  96000/175009          
c   -- var.elim.:  97000/175009          
c   -- var.elim.:  98000/175009          
c   -- var.elim.:  99000/175009          
c   -- var.elim.:  100000/175009          
c   -- var.elim.:  101000/175009          
c   -- var.elim.:  102000/175009          
c   -- var.elim.:  103000/175009          
c   -- var.elim.:  104000/175009          
c   -- var.elim.:  105000/175009          
c   -- var.elim.:  106000/175009          
c   -- var.elim.:  107000/175009          
c   -- var.elim.:  108000/175009          
c   -- var.elim.:  109000/175009          
c   -- var.elim.:  110000/175009          
c   -- var.elim.:  111000/175009          
c   -- var.elim.:  112000/175009          
c   -- var.elim.:  113000/175009          
c   -- var.elim.:  114000/175009          
c   -- var.elim.:  115000/175009          
c   -- var.elim.:  116000/175009          
c   -- var.elim.:  117000/175009          
c   -- var.elim.:  118000/175009          
c   -- var.elim.:  119000/175009          
c   -- var.elim.:  120000/175009          
c   -- var.elim.:  121000/175009          
c   -- var.elim.:  122000/175009          
c   -- var.elim.:  123000/175009          
c   -- var.elim.:  124000/175009          
c   -- var.elim.:  125000/175009          
c   -- var.elim.:  126000/175009          
c   -- var.elim.:  127000/175009          
c   -- var.elim.:  128000/175009          
c   -- var.elim.:  129000/175009          
c   -- var.elim.:  130000/175009          
c   -- var.elim.:  131000/175009          
c   -- var.elim.:  132000/175009          
c   -- var.elim.:  133000/175009          
c   -- var.elim.:  134000/175009          
c   -- var.elim.:  135000/175009          
c   -- var.elim.:  136000/175009          
c   -- var.elim.:  137000/175009          
c   -- var.elim.:  138000/175009          
c   -- var.elim.:  139000/175009          
c   -- var.elim.:  140000/175009          
c   -- var.elim.:  141000/175009          
c   -- var.elim.:  142000/175009          
c   -- var.elim.:  143000/175009          
c   -- var.elim.:  144000/175009          
c   -- var.elim.:  145000/175009          
c   -- var.elim.:  146000/175009          
c   -- var.elim.:  147000/175009          
c   -- var.elim.:  148000/175009          
c   -- var.elim.:  149000/175009          
c   -- var.elim.:  150000/175009          
c   -- var.elim.:  151000/175009          
c   -- var.elim.:  152000/175009          
c   -- var.elim.:  153000/175009          
c   -- var.elim.:  154000/175009          
c   -- var.elim.:  155000/175009          
c   -- var.elim.:  156000/175009          
c   -- var.elim.:  157000/175009          
c   -- var.elim.:  158000/175009          
c   -- var.elim.:  159000/175009          
c   -- var.elim.:  160000/175009          
c   -- var.elim.:  161000/175009          
c   -- var.elim.:  162000/175009          
c   -- var.elim.:  163000/175009          
c   -- var.elim.:  164000/175009          
c   -- var.elim.:  165000/175009          
c   -- var.elim.:  166000/175009          
c   -- var.elim.:  167000/175009          
c   -- var.elim.:  168000/175009          
c   -- var.elim.:  169000/175009          
c   -- var.elim.:  170000/175009          
c   -- var.elim.:  171000/175009          
c   -- var.elim.:  172000/175009          
c   -- var.elim.:  173000/175009          
c   -- var.elim.:  174000/175009          
c   -- var.elim.:  175000/175009          
c   -- var.elim.:  175009/175009          
c   -- var.elim.:  1000/3102          
c   -- var.elim.:  2000/3102          
c   -- var.elim.:  3000/3102          
c   -- var.elim.:  3102/3102          
c   -- var.elim.:  1000/2131          
c   -- var.elim.:  2000/2131          
c   -- var.elim.:  2131/2131          
c   -- var.elim.:  1000/1936          
c   -- var.elim.:  1936/1936          
c   -- var.elim.:  1000/2216          
c   -- var.elim.:  2000/2216          
c   -- var.elim.:  2216/2216          
c   -- var.elim.:  1000/2001          
c   -- var.elim.:  2000/2001          
c   -- var.elim.:  2001/2001          
c   -- var.elim.:  1000/1935          
c   -- var.elim.:  1935/1935          
c   -- var.elim.:  1000/1131          
c   -- var.elim.:  1131/1131          
c   -- var.elim.:  559/559          
c   -- var.elim.:  274/274          
c   -- var.elim.:  116/116          
c   -- var.elim.:  35/35          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  1000/59595          
c   -- var.elim.:  2000/59595          
c   -- var.elim.:  3000/59595          
c   -- var.elim.:  4000/59595          
c   -- var.elim.:  5000/59595          
c   -- var.elim.:  6000/59595          
c   -- var.elim.:  7000/59595          
c   -- var.elim.:  8000/59595          
c   -- var.elim.:  9000/59595          
c   -- var.elim.:  10000/59595          
c   -- var.elim.:  11000/59595          
c   -- var.elim.:  12000/59595          
c   -- var.elim.:  13000/59595          
c   -- var.elim.:  14000/59595          
c   -- var.elim.:  15000/59595          
c   -- var.elim.:  16000/59595          
c   -- var.elim.:  17000/59595          
c   -- var.elim.:  18000/59595          
c   -- var.elim.:  19000/59595          
c   -- var.elim.:  20000/59595          
c   -- var.elim.:  21000/59595          
c   -- var.elim.:  22000/59595          
c   -- var.elim.:  23000/59595          
c   -- var.elim.:  24000/59595          
c   -- var.elim.:  25000/59595          
c   -- var.elim.:  26000/59595          
c   -- var.elim.:  27000/59595          
c   -- var.elim.:  28000/59595          
c   -- var.elim.:  29000/59595          
c   -- var.elim.:  30000/59595          
c   -- var.elim.:  31000/59595          
c   -- var.elim.:  32000/59595          
c   -- var.elim.:  33000/59595          
c   -- var.elim.:  34000/59595          
c   -- var.elim.:  35000/59595          
c   -- var.elim.:  36000/59595          
c   -- var.elim.:  37000/59595          
c   -- var.elim.:  38000/59595          
c   -- var.elim.:  39000/59595          
c   -- var.elim.:  40000/59595          
c   -- var.elim.:  41000/59595          
c   -- var.elim.:  42000/59595          
c   -- var.elim.:  43000/59595          
c   -- var.elim.:  44000/59595          
c   -- var.elim.:  45000/59595          
c   -- var.elim.:  46000/59595          
c   -- var.elim.:  47000/59595          
c   -- var.elim.:  48000/59595          
c   -- var.elim.:  49000/59595          
c   -- var.elim.:  50000/59595          
c   -- var.elim.:  51000/59595          
c   -- var.elim.:  52000/59595          
c   -- var.elim.:  53000/59595          
c   -- var.elim.:  54000/59595          
c   -- var.elim.:  55000/59595          
c   -- var.elim.:  56000/59595          
c   -- var.elim.:  57000/59595          
c   -- var.elim.:  58000/59595          
c   -- var.elim.:  59000/59595          
c   -- var.elim.:  59595/59595          
c   -- var.elim.:  1000/35108          
c   -- var.elim.:  2000/35108          
c   -- var.elim.:  3000/35108          
c   -- var.elim.:  4000/35108          
c   -- var.elim.:  5000/35108          
c   -- var.elim.:  6000/35108          
c   -- var.elim.:  7000/35108          
c   -- var.elim.:  8000/35108          
c   -- var.elim.:  9000/35108          
c   -- var.elim.:  10000/35108          
c   -- var.elim.:  11000/35108          
c   -- var.elim.:  12000/35108          
c   -- var.elim.:  13000/35108          
c   -- var.elim.:  14000/35108          
c   -- var.elim.:  15000/35108          
c   -- var.elim.:  16000/35108          
c   -- var.elim.:  17000/35108          
c   -- var.elim.:  18000/35108          
c   -- var.elim.:  19000/35108          
c   -- var.elim.:  20000/35108          
c   -- var.elim.:  21000/35108          
c   -- var.elim.:  22000/35108          
c   -- var.elim.:  23000/35108          
c   -- var.elim.:  24000/35108          
c   -- var.elim.:  25000/35108          
c   -- var.elim.:  26000/35108          
c   -- var.elim.:  27000/35108          
c   -- var.elim.:  28000/35108          
c   -- var.elim.:  29000/35108          
c   -- var.elim.:  30000/35108          
c   -- var.elim.:  31000/35108          
c   -- var.elim.:  32000/35108          
c   -- var.elim.:  33000/35108          
c   -- var.elim.:  34000/35108          
c   -- var.elim.:  35000/35108          
c   -- var.elim.:  35108/35108          
c   -- var.elim.:  1000/1809          
c   -- var.elim.:  1809/1809          
c   -- var.elim.:  835/835          
c   -- var.elim.:  813/813          
c   -- var.elim.:  162/162          
c   -- var.elim.:  24/24          
c   -- var.elim.:  148/148          
c   -- var.elim.:  150/150          
c   -- subsuming                       
c   -- var.elim.:  1000/14558          
c   -- var.elim.:  2000/14558          
c   -- var.elim.:  3000/14558          
c   -- var.elim.:  4000/14558          
c   -- var.elim.:  5000/14558          
c   -- var.elim.:  6000/14558          
c   -- var.elim.:  7000/14558          
c   -- var.elim.:  8000/14558          
c   -- var.elim.:  9000/14558          
c   -- var.elim.:  10000/14558          
c   -- var.elim.:  11000/14558          
c   -- var.elim.:  12000/14558          
c   -- var.elim.:  13000/14558          
c   -- var.elim.:  14000/14558          
c   -- var.elim.:  14558/14558          
c   -- var.elim.:  1000/3547          
c   -- var.elim.:  2000/3547          
c   -- var.elim.:  3000/3547          
c   -- var.elim.:  3547/3547          
c   -- var.elim.:  53/53          
c   -- subsuming                       
c   -- var.elim.:  1000/2589          
c   -- var.elim.:  2000/2589          
c   -- var.elim.:  2589/2589          
c   -- var.elim.:  1000/1471          
c   -- var.elim.:  1471/1471          
c   -- var.elim.:  108/108          
c   -- var.elim.:  24/24          
c   -- subsuming                       
c   -- var.elim.:  1000/1242          
c   -- var.elim.:  1242/1242          
c   -- var.elim.:  1000/1133          
c   -- var.elim.:  1133/1133          
c   -- var.elim.:  48/48          
c   -- subsuming                       
c   -- var.elim.:  1000/1116          
c   -- var.elim.:  1116/1116          
c   -- var.elim.:  1000/1144          
c   -- var.elim.:  1144/1144          
c   -- var.elim.:  36/36          
c   -- var.elim.:  68/68          
c   -- subsuming                       
c   -- var.elim.:  1000/1066          
c   -- var.elim.:  1066/1066          
c   -- var.elim.:  1000/1339          
c   -- var.elim.:  1339/1339          
c   -- subsuming                       
c   -- var.elim.:  1000/1249          
c   -- var.elim.:  1249/1249          
c   -- var.elim.:  1000/1015          
c   -- var.elim.:  1015/1015          
c   -- subsuming                       
c   -- var.elim.:  643/643          
c   -- var.elim.:  480/480          
c   -- subsuming                       
c   -- var.elim.:  192/192          
c   -- var.elim.:  96/96          
c |         0 |  738332  2242130 |      --       0       --      -- | #### 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.75 0.93 0.91 2/54 14903
Raw data (stat): 14903 (runsolver) R 14902 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481819922 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.79 0.93 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 45754 0 0 0 883 115 0 0 25 0 1 0 481819922 209395712 44375 4294967295 134512640 134672761 3221224544 3221203792 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51122 44376 603 41 0 51081 0
vsize: 204488
[startup+20.0016 s]
Raw data (loadavg): 0.82 0.94 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 51625 0 0 0 1859 140 0 0 25 0 1 0 481819922 228114432 48620 4294967295 134512640 134672761 3221224544 3221222936 1075280321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55692 48620 603 41 0 55651 0
vsize: 222768
[startup+30.0014 s]
Raw data (loadavg): 0.85 0.94 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 51666 0 0 0 2837 161 0 0 25 0 1 0 481819922 228638720 48661 4294967295 134512640 134672761 3221224544 3221222880 134633767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55820 48661 603 41 0 55779 0
vsize: 223280
[startup+40.0016 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 51851 0 0 0 3827 171 0 0 25 0 1 0 481819922 228392960 48530 4294967295 134512640 134672761 3221224544 3221223040 134637123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55760 48530 603 41 0 55719 0
vsize: 223040
[startup+50.002 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 52817 0 0 0 4823 175 0 0 25 0 1 0 481819922 232443904 49009 4294967295 134512640 134672761 3221224544 3221223136 134621336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56749 49009 603 41 0 56708 0
vsize: 226996
[startup+60.0028 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68332 0 0 0 5780 217 0 0 25 0 1 0 481819922 225640448 48156 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55088 48156 603 41 0 55047 0
vsize: 220352
[startup+70.0046 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68372 0 0 0 6780 218 0 0 25 0 1 0 481819922 225902592 48196 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55152 48196 603 41 0 55111 0
vsize: 220608
[startup+80.0044 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68388 0 0 0 7779 219 0 0 25 0 1 0 481819922 225902592 48212 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55152 48212 603 41 0 55111 0
vsize: 220608
[startup+90.0044 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68437 0 0 0 8779 219 0 0 25 0 1 0 481819922 226164736 48261 4294967295 134512640 134672761 3221224544 3221223744 134610528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48261 603 41 0 55175 0
vsize: 220864
[startup+100.004 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68447 0 0 0 9779 219 0 0 25 0 1 0 481819922 226164736 48271 4294967295 134512640 134672761 3221224544 3221223712 134564698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48271 603 41 0 55175 0
vsize: 220864
[startup+110.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68453 0 0 0 10780 219 0 0 25 0 1 0 481819922 226164736 48277 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48277 603 41 0 55175 0
vsize: 220864
[startup+120.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68458 0 0 0 11780 219 0 0 25 0 1 0 481819922 226164736 48282 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48282 603 41 0 55175 0
vsize: 220864
[startup+130.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68459 0 0 0 12780 219 0 0 25 0 1 0 481819922 226164736 48283 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48283 603 41 0 55175 0
vsize: 220864
[startup+140.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68460 0 0 0 13780 219 0 0 25 0 1 0 481819922 226164736 48284 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48284 603 41 0 55175 0
vsize: 220864
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68461 0 0 0 14780 219 0 0 25 0 1 0 481819922 226164736 48285 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48285 603 41 0 55175 0
vsize: 220864
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68463 0 0 0 15780 219 0 0 25 0 1 0 481819922 226164736 48287 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48287 603 41 0 55175 0
vsize: 220864
[startup+170.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68472 0 0 0 16780 219 0 0 25 0 1 0 481819922 226164736 48296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48296 603 41 0 55175 0
vsize: 220864
[startup+180.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68474 0 0 0 17781 219 0 0 25 0 1 0 481819922 226164736 48298 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48298 603 41 0 55175 0
vsize: 220864
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68474 0 0 0 18781 219 0 0 25 0 1 0 481819922 226164736 48298 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48298 603 41 0 55175 0
vsize: 220864
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68477 0 0 0 19781 219 0 0 25 0 1 0 481819922 226164736 48301 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48301 603 41 0 55175 0
vsize: 220864
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68483 0 0 0 20781 219 0 0 25 0 1 0 481819922 226164736 48307 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55216 48307 603 41 0 55175 0
vsize: 220864
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68518 0 0 0 21781 219 0 0 25 0 1 0 481819922 226426880 48342 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48342 603 41 0 55239 0
vsize: 221120
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68520 0 0 0 22781 219 0 0 25 0 1 0 481819922 226426880 48344 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48344 603 41 0 55239 0
vsize: 221120
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68523 0 0 0 23782 219 0 0 25 0 1 0 481819922 226426880 48347 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48347 603 41 0 55239 0
vsize: 221120
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68525 0 0 0 24782 219 0 0 25 0 1 0 481819922 226426880 48349 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48349 603 41 0 55239 0
vsize: 221120
[startup+260.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68527 0 0 0 25782 219 0 0 25 0 1 0 481819922 226426880 48351 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48351 603 41 0 55239 0
vsize: 221120
[startup+270.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68528 0 0 0 26782 219 0 0 25 0 1 0 481819922 226426880 48352 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48352 603 41 0 55239 0
vsize: 221120
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68530 0 0 0 27782 219 0 0 25 0 1 0 481819922 226426880 48354 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48354 603 41 0 55239 0
vsize: 221120
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68533 0 0 0 28782 219 0 0 25 0 1 0 481819922 226426880 48357 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48357 603 41 0 55239 0
vsize: 221120
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68535 0 0 0 29783 219 0 0 25 0 1 0 481819922 226426880 48359 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48359 603 41 0 55239 0
vsize: 221120
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68539 0 0 0 30783 219 0 0 25 0 1 0 481819922 226426880 48363 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48363 603 41 0 55239 0
vsize: 221120
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68541 0 0 0 31783 219 0 0 25 0 1 0 481819922 226426880 48365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48365 603 41 0 55239 0
vsize: 221120
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68543 0 0 0 32783 219 0 0 25 0 1 0 481819922 226426880 48367 4294967295 134512640 134672761 3221224544 3221223680 134614677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48367 603 41 0 55239 0
vsize: 221120
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68545 0 0 0 33783 219 0 0 25 0 1 0 481819922 226426880 48369 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48369 603 41 0 55239 0
vsize: 221120
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68547 0 0 0 34783 219 0 0 25 0 1 0 481819922 226426880 48371 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48371 603 41 0 55239 0
vsize: 221120
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68551 0 0 0 35784 219 0 0 25 0 1 0 481819922 226426880 48375 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55280 48375 603 41 0 55239 0
vsize: 221120
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68561 0 0 0 36784 219 0 0 25 0 1 0 481819922 226951168 48385 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55408 48385 603 41 0 55367 0
vsize: 221632
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68563 0 0 0 37784 219 0 0 25 0 1 0 481819922 226951168 48387 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55408 48387 603 41 0 55367 0
vsize: 221632
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68564 0 0 0 38784 219 0 0 25 0 1 0 481819922 226951168 48388 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55408 48388 603 41 0 55367 0
vsize: 221632
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68567 0 0 0 39784 219 0 0 25 0 1 0 481819922 226951168 48391 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55408 48391 603 41 0 55367 0
vsize: 221632
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68568 0 0 0 40785 219 0 0 25 0 1 0 481819922 226951168 48392 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55408 48392 603 41 0 55367 0
vsize: 221632
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68661 0 0 0 41784 220 0 0 25 0 1 0 481819922 227610624 48485 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55569 48485 603 41 0 55528 0
vsize: 222276
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68666 0 0 0 42784 220 0 0 25 0 1 0 481819922 227610624 48490 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55569 48490 603 41 0 55528 0
vsize: 222276
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68669 0 0 0 43784 220 0 0 25 0 1 0 481819922 227610624 48493 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55569 48493 603 41 0 55528 0
vsize: 222276
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68673 0 0 0 44784 220 0 0 25 0 1 0 481819922 227610624 48497 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55569 48497 603 41 0 55528 0
vsize: 222276
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68742 0 0 0 45784 220 0 0 25 0 1 0 481819922 228007936 48566 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55666 48566 603 41 0 55625 0
vsize: 222664
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68747 0 0 0 46784 220 0 0 25 0 1 0 481819922 228007936 48571 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55666 48571 603 41 0 55625 0
vsize: 222664
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68751 0 0 0 47784 220 0 0 25 0 1 0 481819922 228007936 48575 4294967295 134512640 134672761 3221224544 3221223688 134616366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55666 48575 603 41 0 55625 0
vsize: 222664
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68758 0 0 0 48785 220 0 0 25 0 1 0 481819922 228007936 48582 4294967295 134512640 134672761 3221224544 3221223680 134614825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55666 48582 603 41 0 55625 0
vsize: 222664
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68761 0 0 0 49785 220 0 0 25 0 1 0 481819922 228007936 48585 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55666 48585 603 41 0 55625 0
vsize: 222664
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68772 0 0 0 50785 220 0 0 25 0 1 0 481819922 228007936 48596 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55666 48596 603 41 0 55625 0
vsize: 222664
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68792 0 0 0 51785 220 0 0 25 0 1 0 481819922 228007936 48616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55666 48616 603 41 0 55625 0
vsize: 222664
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68839 0 0 0 52785 220 0 0 25 0 1 0 481819922 228278272 48663 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55732 48663 603 41 0 55691 0
vsize: 222928
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68900 0 0 0 53785 220 0 0 25 0 1 0 481819922 228413440 48724 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55765 48724 603 41 0 55724 0
vsize: 223060
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 68915 0 0 0 54785 220 0 0 25 0 1 0 481819922 228548608 48739 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55798 48739 603 41 0 55757 0
vsize: 223192
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69002 0 0 0 55785 220 0 0 25 0 1 0 481819922 228814848 48826 4294967295 134512640 134672761 3221224544 3221223536 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55863 48826 603 41 0 55822 0
vsize: 223452
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69013 0 0 0 56786 220 0 0 25 0 1 0 481819922 228950016 48837 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55896 48837 603 41 0 55855 0
vsize: 223584
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69035 0 0 0 57786 220 0 0 25 0 1 0 481819922 228950016 48859 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55896 48859 603 41 0 55855 0
vsize: 223584
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69258 0 0 0 58785 221 0 0 25 0 1 0 481819922 229871616 49082 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56121 49082 603 41 0 56080 0
vsize: 224484
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69270 0 0 0 59785 221 0 0 25 0 1 0 481819922 229871616 49094 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56121 49094 603 41 0 56080 0
vsize: 224484
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69286 0 0 0 60785 221 0 0 25 0 1 0 481819922 230006784 49110 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56154 49110 603 41 0 56113 0
vsize: 224616
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69300 0 0 0 61786 221 0 0 25 0 1 0 481819922 230006784 49124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56154 49124 603 41 0 56113 0
vsize: 224616
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69406 0 0 0 62786 221 0 0 25 0 1 0 481819922 230404096 49230 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56251 49230 603 41 0 56210 0
vsize: 225004
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69421 0 0 0 63786 221 0 0 25 0 1 0 481819922 230539264 49245 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56284 49245 603 41 0 56243 0
vsize: 225136
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69778 0 0 0 64784 223 0 0 25 0 1 0 481819922 232382464 49602 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56734 49602 603 41 0 56693 0
vsize: 226936
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 69922 0 0 0 65784 223 0 0 25 0 1 0 481819922 233046016 49746 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56896 49746 603 41 0 56855 0
vsize: 227584
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 70177 0 0 0 66783 224 0 0 25 0 1 0 481819922 234098688 50001 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57153 50001 603 41 0 57112 0
vsize: 228612
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 70406 0 0 0 67783 225 0 0 25 0 1 0 481819922 234897408 50230 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57348 50230 603 41 0 57307 0
vsize: 229392
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 70694 0 0 0 68783 225 0 0 25 0 1 0 481819922 236085248 50518 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57638 50518 603 41 0 57597 0
vsize: 230552
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 70774 0 0 0 69783 225 0 0 25 0 1 0 481819922 236486656 50598 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57736 50598 603 41 0 57695 0
vsize: 230944
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 71058 0 0 0 70782 226 0 0 25 0 1 0 481819922 237551616 50882 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57996 50882 603 41 0 57955 0
vsize: 231984
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 71119 0 0 0 71782 226 0 0 25 0 1 0 481819922 237821952 50943 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58062 50943 603 41 0 58021 0
vsize: 232248
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 71153 0 0 0 72782 227 0 0 25 0 1 0 481819922 237957120 50977 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58095 50977 603 41 0 58054 0
vsize: 232380
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 71660 0 0 0 73780 228 0 0 25 0 1 0 481819922 239935488 51484 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58578 51484 603 41 0 58537 0
vsize: 234312
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72049 0 0 0 74779 230 0 0 25 0 1 0 481819922 241524736 51873 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58966 51873 603 41 0 58925 0
vsize: 235864
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72366 0 0 0 75778 231 0 0 25 0 1 0 481819922 242851840 52190 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59290 52190 603 41 0 59249 0
vsize: 237160
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72421 0 0 0 76778 231 0 0 25 0 1 0 481819922 243122176 52245 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59356 52245 603 41 0 59315 0
vsize: 237424
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72566 0 0 0 77778 232 0 0 25 0 1 0 481819922 243650560 52390 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59485 52390 603 41 0 59444 0
vsize: 237940
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72665 0 0 0 78778 232 0 0 25 0 1 0 481819922 244051968 52489 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59583 52489 603 41 0 59542 0
vsize: 238332
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72769 0 0 0 79777 232 0 0 25 0 1 0 481819922 244449280 52593 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59680 52593 603 41 0 59639 0
vsize: 238720
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72803 0 0 0 80777 233 0 0 25 0 1 0 481819922 244580352 52627 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59712 52627 603 41 0 59671 0
vsize: 238848
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 72861 0 0 0 81778 233 0 0 25 0 1 0 481819922 244842496 52685 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59776 52685 603 41 0 59735 0
vsize: 239104
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73107 0 0 0 82777 234 0 0 25 0 1 0 481819922 245768192 52931 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60002 52931 603 41 0 59961 0
vsize: 240008
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73135 0 0 0 83777 234 0 0 25 0 1 0 481819922 245903360 52959 4294967295 134512640 134672761 3221224544 3221223688 134616339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60035 52959 603 41 0 59994 0
vsize: 240140
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73194 0 0 0 84777 234 0 0 25 0 1 0 481819922 246169600 53018 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60100 53018 603 41 0 60059 0
vsize: 240400
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73242 0 0 0 85777 234 0 0 25 0 1 0 481819922 246304768 53066 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60133 53066 603 41 0 60092 0
vsize: 240532
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73259 0 0 0 86777 234 0 0 25 0 1 0 481819922 246435840 53083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60165 53083 603 41 0 60124 0
vsize: 240660
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73275 0 0 0 87777 234 0 0 25 0 1 0 481819922 246435840 53099 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60165 53099 603 41 0 60124 0
vsize: 240660
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73291 0 0 0 88778 235 0 0 25 0 1 0 481819922 246435840 53115 4294967295 134512640 134672761 3221224544 3221223728 134615988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60165 53115 603 41 0 60124 0
vsize: 240660
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73306 0 0 0 89778 235 0 0 25 0 1 0 481819922 246571008 53130 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60198 53130 603 41 0 60157 0
vsize: 240792
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73373 0 0 0 90778 235 0 0 25 0 1 0 481819922 246837248 53197 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60263 53197 603 41 0 60222 0
vsize: 241052
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73389 0 0 0 91778 235 0 0 25 0 1 0 481819922 246837248 53213 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60263 53213 603 41 0 60222 0
vsize: 241052
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73413 0 0 0 92778 235 0 0 25 0 1 0 481819922 246972416 53237 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60296 53237 603 41 0 60255 0
vsize: 241184
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73428 0 0 0 93778 235 0 0 25 0 1 0 481819922 246972416 53252 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60296 53252 603 41 0 60255 0
vsize: 241184
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73447 0 0 0 94778 235 0 0 25 0 1 0 481819922 247107584 53271 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60329 53271 603 41 0 60288 0
vsize: 241316
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73467 0 0 0 95778 235 0 0 25 0 1 0 481819922 247107584 53291 4294967295 134512640 134672761 3221224544 3221223456 1075352369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60329 53291 603 41 0 60288 0
vsize: 241316
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73504 0 0 0 96778 235 0 0 25 0 1 0 481819922 247377920 53328 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60395 53328 603 41 0 60354 0
vsize: 241580
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73548 0 0 0 97778 235 0 0 25 0 1 0 481819922 247508992 53372 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60427 53372 603 41 0 60386 0
vsize: 241708
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73665 0 0 0 98778 236 0 0 25 0 1 0 481819922 247906304 53489 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60524 53489 603 41 0 60483 0
vsize: 242096
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73686 0 0 0 99779 236 0 0 25 0 1 0 481819922 248041472 53510 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60557 53510 603 41 0 60516 0
vsize: 242228
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73696 0 0 0 100779 236 0 0 25 0 1 0 481819922 248041472 53520 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60557 53520 603 41 0 60516 0
vsize: 242228
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73735 0 0 0 101780 236 0 0 25 0 1 0 481819922 248172544 53559 4294967295 134512640 134672761 3221224544 3221223696 134565094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60589 53559 603 41 0 60548 0
vsize: 242356
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73775 0 0 0 102780 236 0 0 25 0 1 0 481819922 248438784 53599 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60654 53599 603 41 0 60613 0
vsize: 242616
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73804 0 0 0 103780 236 0 0 25 0 1 0 481819922 248438784 53628 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60654 53628 603 41 0 60613 0
vsize: 242616
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73826 0 0 0 104780 236 0 0 25 0 1 0 481819922 248573952 53650 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60687 53650 603 41 0 60646 0
vsize: 242748
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 73884 0 0 0 105780 237 0 0 25 0 1 0 481819922 248844288 53708 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60753 53708 603 41 0 60712 0
vsize: 243012
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74295 0 0 0 106778 238 0 0 25 0 1 0 481819922 250425344 54119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61139 54119 603 41 0 61098 0
vsize: 244556
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74335 0 0 0 107778 239 0 0 25 0 1 0 481819922 250560512 54159 4294967295 134512640 134672761 3221224544 3221223808 134617922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61172 54159 603 41 0 61131 0
vsize: 244688
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74398 0 0 0 108778 239 0 0 25 0 1 0 481819922 250830848 54222 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61238 54222 603 41 0 61197 0
vsize: 244952
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74464 0 0 0 109779 239 0 0 25 0 1 0 481819922 251097088 54288 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61303 54288 603 41 0 61262 0
vsize: 245212
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74529 0 0 0 110779 239 0 0 25 0 1 0 481819922 251367424 54353 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61369 54353 603 41 0 61328 0
vsize: 245476
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74705 0 0 0 111779 239 0 0 25 0 1 0 481819922 253091840 54529 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61790 54529 603 41 0 61749 0
vsize: 247160
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74807 0 0 0 112778 239 0 0 25 0 1 0 481819922 253493248 54631 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61888 54631 603 41 0 61847 0
vsize: 247552
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74858 0 0 0 113778 240 0 0 25 0 1 0 481819922 253755392 54682 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61952 54682 603 41 0 61911 0
vsize: 247808
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74886 0 0 0 114779 240 0 0 25 0 1 0 481819922 253890560 54710 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61985 54710 603 41 0 61944 0
vsize: 247940
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 74945 0 0 0 115779 240 0 0 25 0 1 0 481819922 254025728 54769 4294967295 134512640 134672761 3221224544 3221223688 134616296 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62018 54769 603 41 0 61977 0
vsize: 248072
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 75339 0 0 0 116778 241 0 0 25 0 1 0 481819922 255627264 55163 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62409 55163 603 41 0 62368 0
vsize: 249636
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 75806 0 0 0 117777 242 0 0 25 0 1 0 481819922 257613824 55630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62894 55630 603 41 0 62853 0
vsize: 251576
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 75967 0 0 0 118777 242 0 0 25 0 1 0 481819922 258273280 55791 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63055 55791 603 41 0 63014 0
vsize: 252220
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14903
Raw data (stat): 14903 (minisat+) R 14902 25285 25284 0 -1 0 76012 0 0 0 119777 242 0 0 25 0 1 0 481819922 258408448 55836 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63088 55836 603 41 0 63047 0
vsize: 252352
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 14903
Raw data (stat): 14903 (minisat+) Z 14902 25285 25284 0 -1 12 76012 0 0 0 119777 256 0 0 25 0 1 0 481819922 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.19
CPU time (s): 1200.34
CPU user time (s): 1197.77
CPU system time (s): 2.56561
CPU usage (%): 100.013
Max. virtual memory (Kb): 252352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####