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 31324

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        845228 kB
Buffers:         31096 kB
Cached:         131892 kB
SwapCached:        756 kB
Active:          30240 kB
Inactive:       135112 kB
HighTotal:      131008 kB
HighFree:        63392 kB
LowTotal:       903652 kB
LowFree:        781836 kB
SwapTotal:     2097892 kB
SwapFree:      2096424 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5408 kB
Slab:            18412 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-26 00:29:21 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22718 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1171 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1224]---> Sorter-cost: 1119     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1222]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1221]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1220]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost: 1205     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1218]---> Sorter-cost:  643     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1211]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1210]---> Sorter-cost:  940     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1208]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Sorter-cost: 1094     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> BDD-cost:  131
c ---[1205]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1200]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1199]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1198]---> Sorter-cost: 1142     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1197]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1188]---> Sorter-cost: 1221     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1182]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1181]---> Sorter-cost:  949     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1180]---> Sorter-cost: 1205     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1178]---> Sorter-cost:  953     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1177]---> Sorter-cost:  484     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1176]---> Sorter-cost:  666     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1175]---> Sorter-cost: 1136     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1173]---> Sorter-cost: 1324     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1172]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1171]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1168]---> Sorter-cost: 1029     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1167]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1166]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1165]---> Sorter-cost: 1127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1163]---> Sorter-cost:  672     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost:  708     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1153]---> Sorter-cost: 1331     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1152]---> Sorter-cost: 1244     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1147]---> Sorter-cost:  985     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1145]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1143]---> Sorter-cost: 1186     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1142]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1140]---> Sorter-cost:  710     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1139]---> BDD-cost:  113
c ---[1136]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost:  666     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1129]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1125]---> BDD-cost:  163
c ---[1123]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1119]---> Sorter-cost: 1140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1117]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1115]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1113]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1111]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1109]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1107]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1105]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1103]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1101]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1099]---> Sorter-cost: 1125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1097]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1095]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1093]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1091]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1089]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1087]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1085]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1083]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1081]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1079]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1077]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1075]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1073]---> Sorter-cost: 1099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1071]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1069]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1067]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1065]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1063]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1061]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1059]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1057]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1055]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1053]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1051]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1049]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1047]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1045]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1043]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1041]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1039]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1037]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1035]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1033]---> Sorter-cost:  948     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1031]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1029]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1027]---> Sorter-cost: 1165     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1025]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1023]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1021]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1019]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1017]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1015]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1013]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1011]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1009]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1007]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1005]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1003]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1001]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 999]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 997]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 995]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 993]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 991]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 989]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 987]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 985]---> Sorter-cost:  967     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 983]---> Sorter-cost:  897     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 981]---> Sorter-cost:  742     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 979]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 977]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 975]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 973]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 971]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 969]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 967]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 965]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 963]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 961]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 959]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 957]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 955]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 953]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 951]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 949]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 947]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 945]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 943]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 941]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 939]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 937]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 935]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 933]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 931]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 929]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 927]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 925]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 923]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 921]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 919]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 917]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 915]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 913]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 911]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 909]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 907]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 905]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 903]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 901]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 899]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 897]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 895]---> Sorter-cost: 1018     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 893]---> Sorter-cost:  967     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 891]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 889]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 887]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 885]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 883]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 881]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 879]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 877]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 875]---> Sorter-cost: 1201     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 873]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 871]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 869]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 867]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 865]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 863]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 861]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 859]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 857]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 855]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 853]---> Sorter-cost: 1101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 851]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 849]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 847]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 845]---> Sorter-cost:  948     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 843]---> BDD-cost:   71
c ---[ 841]---> BDD-cost:   62
c ---[ 839]---> BDD-cost:   71
c ---[ 837]---> BDD-cost:   76
c ---[ 835]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 833]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 831]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 829]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 827]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 825]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 823]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 821]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 819]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 817]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 815]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 813]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 811]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 809]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 807]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 803]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 797]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 795]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 793]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 791]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 789]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 787]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 785]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 777]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 773]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 771]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 769]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 767]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 765]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 763]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 761]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 759]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 757]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 755]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 753]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 751]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 749]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 747]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 745]---> Sorter-cost:  382     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 743]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 741]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 739]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 737]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 735]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 733]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 731]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 729]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 727]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 725]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 723]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 721]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 719]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 717]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 715]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 713]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 711]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 709]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 707]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 705]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 703]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 701]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 699]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 697]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 695]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 693]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 691]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 689]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 685]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 683]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 681]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 679]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 677]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 675]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 673]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 671]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 669]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 667]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 665]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 663]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 657]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> BDD-cost:   73
c ---[ 651]---> BDD-cost:   97
c ---[ 650]---> BDD-cost:   97
c ---[ 649]---> BDD-cost:   97
c ---[ 648]---> BDD-cost:   97
c ---[ 647]---> BDD-cost:   97
c ---[ 646]---> BDD-cost:   97
c ---[ 645]---> BDD-cost:   97
c ---[ 644]---> BDD-cost:   97
c ---[ 643]---> BDD-cost:   97
c ---[ 642]---> BDD-cost:   97
c ---[ 641]---> BDD-cost:   97
c ---[ 640]---> BDD-cost:   93
c ---[ 639]---> BDD-cost:   93
c ---[ 638]---> BDD-cost:   93
c ---[ 637]---> BDD-cost:   93
c ---[ 636]---> BDD-cost:   93
c ---[ 635]---> BDD-cost:   89
c ---[ 634]---> BDD-cost:   89
c ---[ 633]---> BDD-cost:   89
c ---[ 632]---> BDD-cost:   69
c ---[ 631]---> BDD-cost:   93
c ---[ 630]---> BDD-cost:   93
c ---[ 629]---> BDD-cost:   93
c ---[ 628]---> BDD-cost:   93
c ---[ 627]---> BDD-cost:   93
c ---[ 626]---> BDD-cost:   93
c ---[ 625]---> BDD-cost:   93
c ---[ 624]---> BDD-cost:   93
c ---[ 623]---> BDD-cost:   89
c ---[ 622]---> BDD-cost:   89
c ---[ 621]---> BDD-cost:   89
c ---[ 620]---> BDD-cost:   89
c ---[ 619]---> BDD-cost:   89
c ---[ 618]---> BDD-cost:   89
c ---[ 617]---> BDD-cost:   78
c ---[ 616]---> BDD-cost:   73
c ---[ 615]---> BDD-cost:  100
c ---[ 614]---> BDD-cost:  100
c ---[ 613]---> BDD-cost:  100
c ---[ 612]---> BDD-cost:  100
c ---[ 611]---> BDD-cost:  100
c ---[ 610]---> BDD-cost:  100
c ---[ 609]---> BDD-cost:   96
c ---[ 608]---> BDD-cost:   96
c ---[ 607]---> BDD-cost:   96
c ---[ 606]---> BDD-cost:   96
c ---[ 605]---> BDD-cost:   96
c ---[ 604]---> BDD-cost:   96
c ---[ 603]---> BDD-cost:   96
c ---[ 602]---> BDD-cost:   88
c ---[ 601]---> BDD-cost:   88
c ---[ 600]---> BDD-cost:   88
c ---[ 599]---> BDD-cost:   77
c ---[ 598]---> BDD-cost:  104
c ---[ 597]---> BDD-cost:  104
c ---[ 596]---> BDD-cost:  104
c ---[ 595]---> BDD-cost:  103
c ---[ 594]---> BDD-cost:  104
c ---[ 593]---> BDD-cost:  104
c ---[ 592]---> BDD-cost:  100
c ---[ 591]---> BDD-cost:  100
c ---[ 590]---> BDD-cost:   99
c ---[ 589]---> BDD-cost:   99
c ---[ 588]---> BDD-cost:  100
c ---[ 587]---> BDD-cost:  100
c ---[ 586]---> BDD-cost:  100
c ---[ 585]---> BDD-cost:   96
c ---[ 584]---> BDD-cost:   96
c ---[ 583]---> BDD-cost:   96
c ---[ 582]---> BDD-cost:   96
c ---[ 581]---> BDD-cost:   88
c ---[ 580]---> BDD-cost:   88
c ---[ 579]---> BDD-cost:   77
c ---[ 578]---> BDD-cost:  107
c ---[ 577]---> BDD-cost:  107
c ---[ 576]---> BDD-cost:  107
c ---[ 575]---> BDD-cost:  107
c ---[ 574]---> BDD-cost:  107
c ---[ 573]---> BDD-cost:  107
c ---[ 572]---> BDD-cost:  103
c ---[ 571]---> BDD-cost:  103
c ---[ 570]---> BDD-cost:  103
c ---[ 569]---> BDD-cost:  103
c ---[ 568]---> BDD-cost:  103
c ---[ 567]---> BDD-cost:  103
c ---[ 566]---> BDD-cost:  103
c ---[ 565]---> BDD-cost:   95
c ---[ 564]---> BDD-cost:   95
c ---[ 563]---> BDD-cost:   95
c ---[ 562]---> BDD-cost:   73
c ---[ 561]---> BDD-cost:   97
c ---[ 560]---> BDD-cost:   97
c ---[ 559]---> BDD-cost:   97
c ---[ 558]---> BDD-cost:   97
c ---[ 557]---> BDD-cost:   97
c ---[ 556]---> BDD-cost:   97
c ---[ 555]---> BDD-cost:   97
c ---[ 554]---> BDD-cost:   97
c ---[ 553]---> BDD-cost:   97
c ---[ 552]---> BDD-cost:   97
c ---[ 551]---> BDD-cost:   97
c ---[ 550]---> BDD-cost:   97
c ---[ 549]---> BDD-cost:   93
c ---[ 548]---> BDD-cost:   93
c ---[ 547]---> BDD-cost:   93
c ---[ 546]---> BDD-cost:   92
c ---[ 545]---> BDD-cost:   88
c ---[ 544]---> BDD-cost:   88
c ---[ 543]---> BDD-cost:   89
c ---[ 542]---> BDD-cost:   78
c ---[ 541]---> BDD-cost:   77
c ---[ 540]---> BDD-cost:  104
c ---[ 539]---> BDD-cost:  104
c ---[ 538]---> BDD-cost:  104
c ---[ 537]---> BDD-cost:  104
c ---[ 536]---> BDD-cost:  104
c ---[ 535]---> BDD-cost:  104
c ---[ 534]---> BDD-cost:  104
c ---[ 533]---> BDD-cost:  104
c ---[ 532]---> BDD-cost:  104
c ---[ 531]---> BDD-cost:  104
c ---[ 530]---> BDD-cost:  104
c ---[ 529]---> BDD-cost:  100
c ---[ 528]---> BDD-cost:  100
c ---[ 527]---> BDD-cost:  100
c ---[ 526]---> BDD-cost:  100
c ---[ 525]---> BDD-cost:   99
c ---[ 524]---> BDD-cost:   95
c ---[ 523]---> BDD-cost:   95
c ---[ 522]---> BDD-cost:   96
c ---[ 521]---> BDD-cost:   88
c ---[ 520]---> BDD-cost:   73
c ---[ 519]---> BDD-cost:   96
c ---[ 518]---> BDD-cost:   97
c ---[ 517]---> BDD-cost:   97
c ---[ 516]---> BDD-cost:   97
c ---[ 515]---> BDD-cost:   97
c ---[ 514]---> BDD-cost:   97
c ---[ 513]---> BDD-cost:   93
c ---[ 512]---> BDD-cost:   93
c ---[ 511]---> BDD-cost:   93
c ---[ 510]---> BDD-cost:   92
c ---[ 509]---> BDD-cost:   92
c ---[ 508]---> BDD-cost:   93
c ---[ 507]---> BDD-cost:   93
c ---[ 506]---> BDD-cost:   85
c ---[ 505]---> BDD-cost:   85
c ---[ 504]---> BDD-cost:   85
c ---[ 503]---> BDD-cost:   77
c ---[ 502]---> BDD-cost:   63
c ---[ 501]---> BDD-cost:  101
c ---[ 500]---> BDD-cost:  101
c ---[ 499]---> BDD-cost:   97
c ---[ 498]---> BDD-cost:   97
c ---[ 497]---> BDD-cost:   97
c ---[ 496]---> BDD-cost:   97
c ---[ 495]---> BDD-cost:   97
c ---[ 494]---> BDD-cost:   97
c ---[ 493]---> BDD-cost:   97
c ---[ 492]---> BDD-cost:   97
c ---[ 491]---> BDD-cost:   96
c ---[ 490]---> BDD-cost:   92
c ---[ 489]---> BDD-cost:   93
c ---[ 488]---> BDD-cost:   93
c ---[ 487]---> BDD-cost:   93
c ---[ 486]---> BDD-cost:   93
c ---[ 485]---> BDD-cost:   85
c ---[ 484]---> BDD-cost:   85
c ---[ 483]---> BDD-cost:   77
c ---[ 482]---> BDD-cost:  101
c ---[ 481]---> BDD-cost:  101
c ---[ 480]---> BDD-cost:  101
c ---[ 479]---> BDD-cost:  101
c ---[ 478]---> BDD-cost:  101
c ---[ 477]---> BDD-cost:  101
c ---[ 476]---> BDD-cost:  101
c ---[ 475]---> BDD-cost:  101
c ---[ 474]---> BDD-cost:   97
c ---[ 473]---> BDD-cost:   97
c ---[ 472]---> BDD-cost:   97
c ---[ 471]---> BDD-cost:   97
c ---[ 470]---> BDD-cost:   97
c ---[ 469]---> BDD-cost:   97
c ---[ 468]---> BDD-cost:   93
c ---[ 467]---> BDD-cost:   93
c ---[ 466]---> BDD-cost:   93
c ---[ 465]---> BDD-cost:   93
c ---[ 464]---> BDD-cost:   47
c ---[ 463]---> BDD-cost:   17
c ---[ 462]---> BDD-cost:   29
c ---[ 461]---> BDD-cost:   27
c ---[ 460]---> BDD-cost:   28
c ---[ 459]---> BDD-cost:   28
c ---[ 458]---> BDD-cost:   28
c ---[ 457]---> BDD-cost:   29
c ---[ 456]---> BDD-cost:   29
c ---[ 455]---> BDD-cost:   29
c ---[ 454]---> BDD-cost:   27
c ---[ 453]---> BDD-cost:   29
c ---[ 452]---> BDD-cost:   29
c ---[ 451]---> BDD-cost:   25
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:   22
c ---[ 448]---> BDD-cost:   27
c ---[ 447]---> BDD-cost:   27
c ---[ 446]---> BDD-cost:   21
c ---[ 445]---> BDD-cost:   25
c ---[ 444]---> BDD-cost:   25
c ---[ 443]---> BDD-cost:   22
c ---[ 442]---> BDD-cost:   21
c ---[ 441]---> BDD-cost:   20
c ---[ 440]---> BDD-cost:   17
c ---[ 439]---> BDD-cost:   16
c ---[ 438]---> BDD-cost:   21
c ---[ 437]---> BDD-cost:   26
c ---[ 436]---> BDD-cost:   26
c ---[ 435]---> BDD-cost:   24
c ---[ 434]---> BDD-cost:   27
c ---[ 433]---> BDD-cost:   24
c ---[ 432]---> BDD-cost:   24
c ---[ 431]---> BDD-cost:   26
c ---[ 430]---> BDD-cost:   24
c ---[ 429]---> BDD-cost:   21
c ---[ 428]---> BDD-cost:   25
c ---[ 427]---> BDD-cost:   23
c ---[ 426]---> BDD-cost:   25
c ---[ 425]---> BDD-cost:   23
c ---[ 424]---> BDD-cost:   20
c ---[ 423]---> BDD-cost:   23
c ---[ 422]---> BDD-cost:   22
c ---[ 421]---> BDD-cost:   21
c ---[ 420]---> BDD-cost:   21
c ---[ 419]---> BDD-cost:   21
c ---[ 418]---> BDD-cost:   19
c ---[ 417]---> BDD-cost:   19
c ---[ 416]---> BDD-cost:   15
c ---[ 415]---> BDD-cost:   17
c ---[ 414]---> BDD-cost:   27
c ---[ 413]---> BDD-cost:   29
c ---[ 412]---> BDD-cost:   29
c ---[ 411]---> BDD-cost:   29
c ---[ 410]---> BDD-cost:   27
c ---[ 409]---> BDD-cost:   28
c ---[ 408]---> BDD-cost:   27
c ---[ 407]---> BDD-cost:   27
c ---[ 406]---> BDD-cost:   26
c ---[ 405]---> BDD-cost:   27
c ---[ 404]---> BDD-cost:   27
c ---[ 403]---> BDD-cost:   27
c ---[ 402]---> BDD-cost:   27
c ---[ 401]---> BDD-cost:   25
c ---[ 400]---> BDD-cost:   25
c ---[ 399]---> BDD-cost:   22
c ---[ 398]---> BDD-cost:   25
c ---[ 397]---> BDD-cost:   22
c ---[ 396]---> BDD-cost:   19
c ---[ 395]---> BDD-cost:   23
c ---[ 394]---> BDD-cost:   20
c ---[ 393]---> BDD-cost:   20
c ---[ 392]---> BDD-cost:   17
c ---[ 391]---> BDD-cost:   18
c ---[ 390]---> BDD-cost:   30
c ---[ 389]---> BDD-cost:   31
c ---[ 388]---> BDD-cost:   27
c ---[ 387]---> BDD-cost:   31
c ---[ 386]---> BDD-cost:   30
c ---[ 385]---> BDD-cost:   31
c ---[ 384]---> BDD-cost:   27
c ---[ 383]---> BDD-cost:   29
c ---[ 382]---> BDD-cost:   29
c ---[ 381]---> BDD-cost:   29
c ---[ 380]---> BDD-cost:   28
c ---[ 379]---> BDD-cost:   27
c ---[ 378]---> BDD-cost:   28
c ---[ 377]---> BDD-cost:   27
c ---[ 376]---> BDD-cost:   26
c ---[ 375]---> BDD-cost:   26
c ---[ 374]---> BDD-cost:   25
c ---[ 373]---> BDD-cost:   25
c ---[ 372]---> BDD-cost:   24
c ---[ 371]---> BDD-cost:   25
c ---[ 370]---> BDD-cost:   21
c ---[ 369]---> BDD-cost:   20
c ---[ 368]---> BDD-cost:   18
c ---[ 367]---> BDD-cost:   18
c ---[ 366]---> BDD-cost:   31
c ---[ 365]---> BDD-cost:   30
c ---[ 364]---> BDD-cost:   29
c ---[ 363]---> BDD-cost:   30
c ---[ 362]---> BDD-cost:   31
c ---[ 361]---> BDD-cost:   31
c ---[ 360]---> BDD-cost:   29
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   28
c ---[ 357]---> BDD-cost:   29
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   25
c ---[ 352]---> BDD-cost:   27
c ---[ 351]---> BDD-cost:   25
c ---[ 350]---> BDD-cost:   26
c ---[ 349]---> BDD-cost:   24
c ---[ 348]---> BDD-cost:   24
c ---[ 347]---> BDD-cost:   25
c ---[ 346]---> BDD-cost:   23
c ---[ 345]---> BDD-cost:   21
c ---[ 344]---> BDD-cost:   18
c ---[ 342]---> BDD-cost:   27
c ---[ 341]---> BDD-cost:   29
c ---[ 340]---> BDD-cost:   29
c ---[ 339]---> BDD-cost:   29
c ---[ 338]---> BDD-cost:   29
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   29
c ---[ 335]---> BDD-cost:   29
c ---[ 334]---> BDD-cost:   24
c ---[ 333]---> BDD-cost:   29
c ---[ 332]---> BDD-cost:   26
c ---[ 331]---> BDD-cost:   29
c ---[ 330]---> BDD-cost:   26
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   27
c ---[ 327]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:   25
c ---[ 325]---> BDD-cost:   25
c ---[ 324]---> BDD-cost:   25
c ---[ 323]---> BDD-cost:   21
c ---[ 322]---> BDD-cost:   23
c ---[ 321]---> BDD-cost:   21
c ---[ 320]---> BDD-cost:   18
c ---[ 318]---> BDD-cost:   30
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   31
c ---[ 315]---> BDD-cost:   30
c ---[ 314]---> BDD-cost:   30
c ---[ 313]---> BDD-cost:   31
c ---[ 312]---> BDD-cost:   31
c ---[ 311]---> BDD-cost:   30
c ---[ 310]---> BDD-cost:   31
c ---[ 309]---> BDD-cost:   30
c ---[ 308]---> BDD-cost:   31
c ---[ 307]---> BDD-cost:   29
c ---[ 306]---> BDD-cost:   29
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   29
c ---[ 303]---> BDD-cost:   28
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   26
c ---[ 299]---> BDD-cost:   24
c ---[ 298]---> BDD-cost:   24
c ---[ 297]---> BDD-cost:   20
c ---[ 296]---> BDD-cost:   21
c ---[ 295]---> BDD-cost:   18
c ---[ 294]---> BDD-cost:   31
c ---[ 293]---> BDD-cost:   30
c ---[ 292]---> BDD-cost:   29
c ---[ 291]---> BDD-cost:   30
c ---[ 290]---> BDD-cost:   31
c ---[ 289]---> BDD-cost:   31
c ---[ 288]---> BDD-cost:   29
c ---[ 287]---> BDD-cost:   29
c ---[ 286]---> BDD-cost:   28
c ---[ 285]---> BDD-cost:   29
c ---[ 284]---> BDD-cost:   28
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   28
c ---[ 281]---> BDD-cost:   25
c ---[ 280]---> BDD-cost:   27
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   24
c ---[ 276]---> BDD-cost:   24
c ---[ 275]---> BDD-cost:   25
c ---[ 274]---> BDD-cost:   23
c ---[ 273]---> BDD-cost:   21
c ---[ 272]---> BDD-cost:   18
c ---[ 271]---> BDD-cost:   19
c ---[ 270]---> BDD-cost:   33
c ---[ 269]---> BDD-cost:   33
c ---[ 268]---> BDD-cost:   33
c ---[ 267]---> BDD-cost:   31
c ---[ 266]---> BDD-cost:   27
c ---[ 265]---> BDD-cost:   31
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   30
c ---[ 262]---> BDD-cost:   30
c ---[ 261]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:   30
c ---[ 259]---> BDD-cost:   31
c ---[ 258]---> BDD-cost:   27
c ---[ 257]---> BDD-cost:   29
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   29
c ---[ 254]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   27
c ---[ 252]---> BDD-cost:   27
c ---[ 251]---> BDD-cost:   25
c ---[ 250]---> BDD-cost:   23
c ---[ 249]---> BDD-cost:   22
c ---[ 248]---> BDD-cost:   18
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   32
c ---[ 245]---> BDD-cost:   33
c ---[ 244]---> BDD-cost:   31
c ---[ 243]---> BDD-cost:   33
c ---[ 242]---> BDD-cost:   33
c ---[ 241]---> BDD-cost:   33
c ---[ 240]---> BDD-cost:   32
c ---[ 239]---> BDD-cost:   33
c ---[ 238]---> BDD-cost:   31
c ---[ 237]---> BDD-cost:   31
c ---[ 236]---> BDD-cost:   31
c ---[ 235]---> BDD-cost:   30
c ---[ 234]---> BDD-cost:   31
c ---[ 233]---> BDD-cost:   31
c ---[ 232]---> BDD-cost:   26
c ---[ 231]---> BDD-cost:   29
c ---[ 230]---> BDD-cost:   26
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   27
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   25
c ---[ 225]---> BDD-cost:   25
c ---[ 224]---> BDD-cost:   23
c ---[ 223]---> Sorter-cost:  711     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 220]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 218]---> Sorter-cost:  889     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 216]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 212]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost: 1096     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 210]---> Sorter-cost: 1074     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 208]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost:  974     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 206]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 190]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost: 1182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost: 1214     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> Sorter-cost: 1177     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 1419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost: 1403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 1422     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost: 1422     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 1422     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 1400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1446     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 1405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1379     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost: 1366     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1346     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 1346     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 1347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost: 1523     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost: 1580     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 157]---> Sorter-cost: 1788     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:    5
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:    4
c ---[ 150]---> BDD-cost:   16
c ---[ 149]---> BDD-cost:    6
c ---[ 148]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  434     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost:  461     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  537     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost:  648     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  841     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 1427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1536     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 1577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1516     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:    7
c ---[ 133]---> BDD-cost:    4
c ---[ 132]---> BDD-cost:    7
c ---[ 131]---> BDD-cost:    7
c ---[ 130]---> BDD-cost:    5
c ---[ 129]---> BDD-cost:    7
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:    6
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:    6
c ---[ 123]---> BDD-cost:    7
c ---[ 122]---> BDD-cost:    5
c ---[ 121]---> BDD-cost:    7
c ---[ 120]---> BDD-cost:    7
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> Sorter-cost:  518     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost:  543     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost:  486     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> BDD-cost:  118
c ---[ 114]---> BDD-cost:  119
c ---[ 113]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:  124
c ---[ 111]---> BDD-cost:  134
c ---[ 110]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1545     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 1468     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1606     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1553     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1512     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    6
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:    3
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    6
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:  127
c ---[  91]---> BDD-cost:  134
c ---[  90]---> BDD-cost:  115
c ---[  89]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> Sorter-cost: 1007     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost:  693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  84]---> Sorter-cost: 1577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  82]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:   19
c ---[  79]---> BDD-cost:   11
c ---[  78]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost:  490     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> Sorter-cost: 1126     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  74]---> Sorter-cost: 1165     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  73]---> Sorter-cost:  164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1615     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost: 1574     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:   22
c ---[  67]---> BDD-cost:    8
c ---[  66]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   39
c ---[  63]---> BDD-cost:    1
c ---[  62]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost:  533     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> BDD-cost:    8
c ---[  59]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:   23
c ---[  52]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> BDD-cost:  127
c ---[  50]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:   11
c ---[  46]---> Sorter-cost:  876     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   19
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:   48
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:    4
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:  123
c ---[  37]---> BDD-cost:    8
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   55
c ---[  34]---> BDD-cost:    6
c ---[  33]---> Sorter-cost: 1081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:   22
c ---[  29]---> BDD-cost:   15
c ---[  28]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   39
c ---[  25]---> BDD-cost:   48
c ---[  24]---> BDD-cost:   35
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:    8
c ---[  21]---> BDD-cost:  127
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:  109
c ---[  17]---> BDD-cost:  139
c ---[  16]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   46
c ---[  13]---> BDD-cost:   45
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   16
c ---[   9]---> Sorter-cost:  953     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  986     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  940     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  963     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost: 1152     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost: 1096     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost: 1412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost: 1350     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  915400  2172318 |  305133       0        0     nan |  0.000 % |
c |       100 |  915172  2171811 |  335646      59      159     2.7 |  3.284 % |
c |       251 |  915115  2171683 |  369210     206      710     3.4 |  3.287 % |
c |       476 |  914854  2171104 |  406132     385     1364     3.5 |  3.310 % |
c |       813 |  914521  2170366 |  446745     668     2371     3.5 |  3.340 % |
c |      1319 |  914029  2169269 |  491419    1109     3847     3.5 |  3.383 % |
c |      2079 |  913372  2167800 |  540561    1784     6750     3.8 |  3.439 % |
c |      3218 |  911844  2164402 |  594617    2705    10508     3.9 |  3.573 % |
c |      4926 |  910038  2160371 |  654079    4148    16933     4.1 |  3.726 % |
c |      7488 |  907935  2155692 |  719487    6413    33497     5.2 |  3.910 % |
c |     11332 |  904341  2147720 |  791436    9776    50159     5.1 |  4.223 % |
c |     17099 |  899942  2137878 |  870580   14969    76327     5.1 |  4.595 % |
c |     25748 |  894003  2124644 |  957638   22831   122985     5.4 |  5.108 % |
c |     38722 |  888546  2112457 | 1053401   35033   247391     7.1 |  5.574 % |
c |     58183 |  882840  2099697 | 1158742   53770   423172     7.9 |  6.058 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 28317 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.92 0.97 0.94 2/54 28313
Raw data (stat): 28313 (runsolver) R 28312 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 843076167 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9998 s]
Raw data (loadavg): 0.93 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.018 s]
Raw data (loadavg): 1.07 0.99 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.017 s]
Raw data (loadavg): 1.06 0.99 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.017 s]
Raw data (loadavg): 1.05 0.99 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.018 s]
Raw data (loadavg): 1.11 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.019 s]
Raw data (loadavg): 1.10 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.025 s]
Raw data (loadavg): 1.08 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.025 s]
Raw data (loadavg): 1.07 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.024 s]
Raw data (loadavg): 1.06 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.025 s]
Raw data (loadavg): 1.05 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.026 s]
Raw data (loadavg): 1.04 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.025 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.025 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.026 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.027 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.026 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.027 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.027 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.027 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.028 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.77 s]
Raw data (loadavg): 1.00 1.00 0.95 1/53 28317
Raw data (stat): 28313 (minisat+_script) S 28312 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843076167 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.77
CPU time (s): 1229.89
CPU user time (s): 1228.95
CPU system time (s): 0.938857
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####