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/milp/normalized-mps-v2-13-7-neos6.opb
MD5SUM	0633214154e8bab02f648560b9bfa54f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	4460
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	233832225
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	233832225
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.18697
Number of variables	17260
Total number of constraints	9376
Number of constraints which are clauses	48
Number of constraints which are cardinality constraints (but not clauses)	9095
Number of constraints which are nor clauses,nor cardinality constraints	233
Minimum length of a constraint	1
Maximum length of a constraint	834
Trace number 14060

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        896828 kB
Buffers:          9592 kB
Cached:          93928 kB
SwapCached:        248 kB
Active:          13132 kB
Inactive:        92536 kB
HighTotal:      131008 kB
HighFree:        81732 kB
LowTotal:       903652 kB
LowFree:        815096 kB
SwapTotal:     2097892 kB
SwapFree:      2096924 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            26372 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:09:28 (client local time) WITH STATUS 0 IN 1200.65 SECONDS
stats: 19726 7 1200.65 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1259 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................
c ---[1258]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1257]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1256]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1255]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1254]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1253]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1252]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1251]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1250]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1249]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1248]---> BDD-cost:  173
c ---[1247]---> BDD-cost:  353
c ---[1246]---> BDD-cost:  533
c ---[1245]---> BDD-cost:  678
c ---[1244]---> BDD-cost:  893
c ---[1243]---> BDD-cost:  984
c ---[1242]---> BDD-cost: 1182
c ---[1241]---> Adder-cost: 899   maxlim: 5   bits: 4/3
c ---[1240]---> Adder-cost: 879   maxlim: 5   bits: 4/3
c ---[1239]---> Adder-cost: 937   maxlim: 5   bits: 4/3
c ---[1238]---> BDD-cost: 2467
c ---[1237]---> BDD-cost: 2502
c ---[1236]---> BDD-cost: 2722
c ---[1235]---> BDD-cost: 2778
c ---[1234]---> BDD-cost: 2922
c ---[1233]---> Adder-cost: 1354   maxlim: 5   bits: 4/3
c ---[1232]---> Adder-cost: 1267   maxlim: 5   bits: 4/3
c ---[1231]---> Adder-cost: 1200   maxlim: 5   bits: 4/3
c ---[1230]---> Adder-cost: 1201   maxlim: 5   bits: 4/3
c ---[1229]---> BDD-cost: 2262
c ---[1228]---> BDD-cost: 2213
c ---[1227]---> BDD-cost: 2115
c ---[1226]---> BDD-cost: 2063
c ---[1225]---> BDD-cost: 1917
c ---[1224]---> BDD-cost: 1853
c ---[1223]---> BDD-cost: 1680
c ---[1222]---> BDD-cost: 1572
c ---[1221]---> BDD-cost: 1395
c ---[1220]---> BDD-cost: 1242
c ---[1219]---> BDD-cost: 1044
c ---[1218]---> BDD-cost:  891
c ---[1217]---> BDD-cost:  699
c ---[1216]---> BDD-cost:  533
c ---[1215]---> BDD-cost:  233
c ---[1214]---> BDD-cost:  117
c ---[1213]---> BDD-cost:  173
c ---[1212]---> BDD-cost:  353
c ---[1211]---> BDD-cost:  533
c ---[1210]---> BDD-cost:  663
c ---[1209]---> BDD-cost:  893
c ---[1208]---> BDD-cost: 1005
c ---[1207]---> BDD-cost: 1253
c ---[1206]---> BDD-cost: 1854
c ---[1205]---> BDD-cost: 1994
c ---[1204]---> BDD-cost: 2242
c ---[1203]---> BDD-cost: 2426
c ---[1202]---> BDD-cost: 2494
c ---[1201]---> BDD-cost: 2730
c ---[1200]---> BDD-cost: 2064
c ---[1199]---> BDD-cost: 2208
c ---[1198]---> Adder-cost: 1424   maxlim: 5   bits: 4/3
c ---[1197]---> Adder-cost: 1267   maxlim: 5   bits: 4/3
c ---[1196]---> Adder-cost: 1230   maxlim: 5   bits: 4/3
c ---[1195]---> Adder-cost: 1161   maxlim: 5   bits: 4/3
c ---[1194]---> BDD-cost: 2273
c ---[1193]---> BDD-cost: 2202
c ---[1192]---> BDD-cost: 2103
c ---[1191]---> BDD-cost: 2052
c ---[1190]---> BDD-cost: 1920
c ---[1189]---> BDD-cost: 1842
c ---[1188]---> BDD-cost: 1722
c ---[1187]---> BDD-cost: 1578
c ---[1186]---> BDD-cost: 1407
c ---[1185]---> BDD-cost: 1248
c ---[1184]---> BDD-cost: 1053
c ---[1183]---> BDD-cost:  893
c ---[1182]---> BDD-cost:  705
c ---[1181]---> BDD-cost:  533
c ---[1180]---> BDD-cost:  237
c ---[1179]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  173
c ---[1177]---> BDD-cost:  353
c ---[1176]---> BDD-cost:  533
c ---[1175]---> BDD-cost:  713
c ---[1174]---> BDD-cost:  879
c ---[1173]---> BDD-cost: 1073
c ---[1172]---> BDD-cost: 1149
c ---[1171]---> BDD-cost: 1821
c ---[1170]---> BDD-cost: 1515
c ---[1169]---> BDD-cost: 1647
c ---[1168]---> BDD-cost: 1821
c ---[1167]---> BDD-cost: 1973
c ---[1166]---> Adder-cost: 1291   maxlim: 5   bits: 4/3
c ---[1165]---> Adder-cost: 1201   maxlim: 5   bits: 4/3
c ---[1164]---> Adder-cost: 1163   maxlim: 5   bits: 4/3
c ---[1163]---> Adder-cost: 1208   maxlim: 5   bits: 4/3
c ---[1162]---> Adder-cost: 1153   maxlim: 5   bits: 4/3
c ---[1161]---> Adder-cost: 1148   maxlim: 5   bits: 4/3
c ---[1160]---> Adder-cost: 1157   maxlim: 5   bits: 4/3
c ---[1159]---> Adder-cost: 1136   maxlim: 5   bits: 4/3
c ---[1158]---> Adder-cost: 1095   maxlim: 4   bits: 4/3
c ---[1157]---> BDD-cost: 2153
c ---[1156]---> BDD-cost: 2019
c ---[1155]---> BDD-cost: 1973
c ---[1154]---> BDD-cost: 1800
c ---[1153]---> BDD-cost: 1731
c ---[1152]---> BDD-cost: 1557
c ---[1151]---> BDD-cost: 1428
c ---[1150]---> BDD-cost: 1221
c ---[1149]---> BDD-cost: 1068
c ---[1148]---> BDD-cost:  876
c ---[1147]---> BDD-cost:  713
c ---[1146]---> BDD-cost:  522
c ---[1145]---> BDD-cost:  237
c ---[1144]---> BDD-cost:  115
c ---[1143]---> BDD-cost:  173
c ---[1142]---> BDD-cost:  353
c ---[1141]---> BDD-cost:  492
c ---[1140]---> BDD-cost:  690
c ---[1139]---> BDD-cost:  834
c ---[1138]---> BDD-cost: 1050
c ---[1137]---> BDD-cost: 1230
c ---[1136]---> BDD-cost: 1902
c ---[1135]---> BDD-cost: 2078
c ---[1134]---> BDD-cost: 2166
c ---[1133]---> BDD-cost: 2438
c ---[1132]---> BDD-cost: 2558
c ---[1131]---> BDD-cost: 2718
c ---[1130]---> BDD-cost: 2061
c ---[1129]---> BDD-cost: 2190
c ---[1128]---> BDD-cost: 2273
c ---[1127]---> BDD-cost: 2250
c ---[1126]---> BDD-cost: 2333
c ---[1125]---> BDD-cost: 2256
c ---[1124]---> BDD-cost: 2273
c ---[1123]---> BDD-cost: 2208
c ---[1122]---> BDD-cost: 2153
c ---[1121]---> BDD-cost: 2043
c ---[1120]---> BDD-cost: 1973
c ---[1119]---> BDD-cost: 1836
c ---[1118]---> BDD-cost: 1733
c ---[1117]---> BDD-cost: 1583
c ---[1116]---> BDD-cost: 1386
c ---[1115]---> BDD-cost: 1245
c ---[1114]---> BDD-cost: 1038
c ---[1113]---> BDD-cost:  893
c ---[1112]---> BDD-cost:  699
c ---[1111]---> BDD-cost:  533
c ---[1110]---> BDD-cost:  233
c ---[1109]---> BDD-cost:  117
c ---[1108]---> BDD-cost:  173
c ---[1107]---> BDD-cost:  353
c ---[1106]---> BDD-cost:  533
c ---[1105]---> BDD-cost:  663
c ---[1104]---> BDD-cost:  893
c ---[1103]---> BDD-cost: 1005
c ---[1102]---> BDD-cost: 1185
c ---[1101]---> BDD-cost: 1857
c ---[1100]---> BDD-cost: 2107
c ---[1099]---> BDD-cost: 2242
c ---[1098]---> BDD-cost: 2467
c ---[1097]---> BDD-cost: 2518
c ---[1096]---> BDD-cost: 2698
c ---[1095]---> BDD-cost: 2076
c ---[1094]---> BDD-cost: 2175
c ---[1093]---> Adder-cost: 1424   maxlim: 5   bits: 4/3
c ---[1092]---> Adder-cost: 1299   maxlim: 5   bits: 4/3
c ---[1091]---> Adder-cost: 1204   maxlim: 5   bits: 4/3
c ---[1090]---> Adder-cost: 1165   maxlim: 5   bits: 4/3
c ---[1089]---> BDD-cost: 2262
c ---[1088]---> BDD-cost: 2213
c ---[1087]---> BDD-cost: 2133
c ---[1086]---> BDD-cost: 2063
c ---[1085]---> BDD-cost: 1941
c ---[1084]---> BDD-cost: 1848
c ---[1083]---> BDD-cost: 1728
c ---[1082]---> BDD-cost: 1572
c ---[1081]---> BDD-cost: 1407
c ---[1080]---> BDD-cost: 1242
c ---[1079]---> BDD-cost: 1053
c ---[1078]---> BDD-cost:  893
c ---[1077]---> BDD-cost:  705
c ---[1076]---> BDD-cost:  533
c ---[1075]---> BDD-cost:  237
c ---[1074]---> BDD-cost:  117
c ---[1024]---> Adder-cost: 156   maxlim: 1055615   bits: 22/21
c ---[1022]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[1020]---> Adder-cost: 334   maxlim: 1070975   bits: 22/21
c ---[1018]---> Adder-cost: 398   maxlim: 1078655   bits: 22/21
c ---[1016]---> Adder-cost: 462   maxlim: 1086335   bits: 22/21
c ---[1014]---> Adder-cost: 510   maxlim: 1093887   bits: 22/21
c ---[1012]---> Adder-cost: 548   maxlim: 1101567   bits: 22/21
c ---[1010]---> Adder-cost: 616   maxlim: 1109247   bits: 22/21
c ---[1008]---> Adder-cost: 758   maxlim: 1115647   bits: 22/21
c ---[1006]---> Adder-cost: 818   maxlim: 1122047   bits: 22/21
c ---[1004]---> Adder-cost: 874   maxlim: 1127423   bits: 22/21
c ---[1002]---> Adder-cost: 964   maxlim: 1132543   bits: 22/21
c ---[1000]---> Adder-cost: 1024   maxlim: 1136383   bits: 22/21
c ---[ 998]---> Adder-cost: 1096   maxlim: 1140223   bits: 22/21
c ---[ 996]---> Adder-cost: 1070   maxlim: 1142783   bits: 22/21
c ---[ 994]---> Adder-cost: 1140   maxlim: 1145087   bits: 22/21
c ---[ 992]---> Adder-cost: 1110   maxlim: 1146367   bits: 22/21
c ---[ 990]---> Adder-cost: 1136   maxlim: 1147647   bits: 22/21
c ---[ 988]---> Adder-cost: 1212   maxlim: 1146367   bits: 22/21
c ---[ 986]---> Adder-cost: 1128   maxlim: 1145471   bits: 22/21
c ---[ 984]---> Adder-cost: 1208   maxlim: 1142911   bits: 22/21
c ---[ 982]---> Adder-cost: 1196   maxlim: 1140351   bits: 22/21
c ---[ 980]---> Adder-cost: 1144   maxlim: 1136511   bits: 22/21
c ---[ 978]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 976]---> Adder-cost: 1060   maxlim: 1127295   bits: 22/21
c ---[ 974]---> Adder-cost: 976   maxlim: 1122175   bits: 22/21
c ---[ 972]---> Adder-cost: 952   maxlim: 1116031   bits: 22/21
c ---[ 970]---> Adder-cost: 848   maxlim: 1109631   bits: 22/21
c ---[ 968]---> Adder-cost: 756   maxlim: 1101951   bits: 22/21
c ---[ 966]---> Adder-cost: 636   maxlim: 1094271   bits: 22/21
c ---[ 964]---> Adder-cost: 570   maxlim: 1086591   bits: 22/21
c ---[ 962]---> Adder-cost: 486   maxlim: 1078527   bits: 22/21
c ---[ 960]---> Adder-cost: 380   maxlim: 1070847   bits: 22/21
c ---[ 958]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 956]---> Adder-cost: 168   maxlim: 1055999   bits: 22/21
c ---[ 954]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 952]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 950]---> Adder-cost: 348   maxlim: 1070975   bits: 22/21
c ---[ 948]---> Adder-cost: 416   maxlim: 1078655   bits: 22/21
c ---[ 946]---> Adder-cost: 488   maxlim: 1086335   bits: 22/21
c ---[ 944]---> Adder-cost: 544   maxlim: 1094143   bits: 22/21
c ---[ 942]---> Adder-cost: 594   maxlim: 1101823   bits: 22/21
c ---[ 940]---> Adder-cost: 648   maxlim: 1109503   bits: 22/21
c ---[ 938]---> Adder-cost: 928   maxlim: 1115903   bits: 22/21
c ---[ 936]---> Adder-cost: 1026   maxlim: 1122303   bits: 22/21
c ---[ 934]---> Adder-cost: 942   maxlim: 1127423   bits: 22/21
c ---[ 932]---> Adder-cost: 984   maxlim: 1132543   bits: 22/21
c ---[ 930]---> Adder-cost: 1080   maxlim: 1136383   bits: 22/21
c ---[ 928]---> Adder-cost: 1104   maxlim: 1140351   bits: 22/21
c ---[ 926]---> Adder-cost: 1096   maxlim: 1142911   bits: 22/21
c ---[ 924]---> Adder-cost: 1100   maxlim: 1145087   bits: 22/21
c ---[ 922]---> Adder-cost: 1150   maxlim: 1146367   bits: 22/21
c ---[ 920]---> Adder-cost: 1174   maxlim: 1147647   bits: 22/21
c ---[ 918]---> Adder-cost: 1164   maxlim: 1146367   bits: 22/21
c ---[ 916]---> Adder-cost: 1184   maxlim: 1145471   bits: 22/21
c ---[ 914]---> Adder-cost: 1186   maxlim: 1142911   bits: 22/21
c ---[ 912]---> Adder-cost: 1202   maxlim: 1140351   bits: 22/21
c ---[ 910]---> Adder-cost: 1160   maxlim: 1136511   bits: 22/21
c ---[ 908]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 906]---> Adder-cost: 1054   maxlim: 1127295   bits: 22/21
c ---[ 904]---> Adder-cost: 982   maxlim: 1122175   bits: 22/21
c ---[ 902]---> Adder-cost: 940   maxlim: 1116031   bits: 22/21
c ---[ 900]---> Adder-cost: 848   maxlim: 1109631   bits: 22/21
c ---[ 898]---> Adder-cost: 758   maxlim: 1101951   bits: 22/21
c ---[ 896]---> Adder-cost: 638   maxlim: 1094271   bits: 22/21
c ---[ 894]---> Adder-cost: 586   maxlim: 1086591   bits: 22/21
c ---[ 892]---> Adder-cost: 506   maxlim: 1078527   bits: 22/21
c ---[ 890]---> Adder-cost: 374   maxlim: 1070847   bits: 22/21
c ---[ 888]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 886]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 884]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 882]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 880]---> Adder-cost: 348   maxlim: 1070975   bits: 22/21
c ---[ 878]---> Adder-cost: 406   maxlim: 1078655   bits: 22/21
c ---[ 876]---> Adder-cost: 478   maxlim: 1086335   bits: 22/21
c ---[ 874]---> Adder-cost: 550   maxlim: 1094015   bits: 22/21
c ---[ 872]---> Adder-cost: 566   maxlim: 1101823   bits: 22/21
c ---[ 870]---> Adder-cost: 646   maxlim: 1109503   bits: 22/21
c ---[ 868]---> Adder-cost: 868   maxlim: 1116031   bits: 22/21
c ---[ 866]---> Adder-cost: 890   maxlim: 1122431   bits: 22/21
c ---[ 864]---> Adder-cost: 882   maxlim: 1127551   bits: 22/21
c ---[ 862]---> Adder-cost: 944   maxlim: 1132671   bits: 22/21
c ---[ 860]---> Adder-cost: 982   maxlim: 1136127   bits: 22/21
c ---[ 858]---> Adder-cost: 998   maxlim: 1139967   bits: 22/21
c ---[ 856]---> Adder-cost: 1036   maxlim: 1142527   bits: 22/21
c ---[ 854]---> Adder-cost: 1050   maxlim: 1145087   bits: 22/21
c ---[ 852]---> Adder-cost: 1086   maxlim: 1146367   bits: 22/21
c ---[ 850]---> Adder-cost: 1106   maxlim: 1147647   bits: 22/21
c ---[ 848]---> Adder-cost: 1126   maxlim: 1146367   bits: 22/21
c ---[ 846]---> Adder-cost: 1116   maxlim: 1145087   bits: 22/21
c ---[ 844]---> Adder-cost: 1140   maxlim: 1142655   bits: 22/21
c ---[ 842]---> Adder-cost: 1106   maxlim: 1140095   bits: 22/21
c ---[ 840]---> Adder-cost: 1120   maxlim: 1136255   bits: 22/21
c ---[ 838]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 836]---> Adder-cost: 1052   maxlim: 1127295   bits: 22/21
c ---[ 834]---> Adder-cost: 1012   maxlim: 1122175   bits: 22/21
c ---[ 832]---> Adder-cost: 920   maxlim: 1116031   bits: 22/21
c ---[ 830]---> Adder-cost: 846   maxlim: 1109631   bits: 22/21
c ---[ 828]---> Adder-cost: 762   maxlim: 1101951   bits: 22/21
c ---[ 826]---> Adder-cost: 690   maxlim: 1094271   bits: 22/21
c ---[ 824]---> Adder-cost: 586   maxlim: 1086591   bits: 22/21
c ---[ 822]---> Adder-cost: 476   maxlim: 1078527   bits: 22/21
c ---[ 820]---> Adder-cost: 388   maxlim: 1070847   bits: 22/21
c ---[ 818]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 816]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 814]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 812]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 810]---> Adder-cost: 350   maxlim: 1070975   bits: 22/21
c ---[ 808]---> Adder-cost: 422   maxlim: 1078655   bits: 22/21
c ---[ 806]---> Adder-cost: 486   maxlim: 1086335   bits: 22/21
c ---[ 804]---> Adder-cost: 570   maxlim: 1094143   bits: 22/21
c ---[ 802]---> Adder-cost: 624   maxlim: 1101823   bits: 22/21
c ---[ 800]---> Adder-cost: 658   maxlim: 1109503   bits: 22/21
c ---[ 798]---> Adder-cost: 1000   maxlim: 1115903   bits: 22/21
c ---[ 796]---> Adder-cost: 966   maxlim: 1122303   bits: 22/21
c ---[ 794]---> Adder-cost: 1084   maxlim: 1127423   bits: 22/21
c ---[ 792]---> Adder-cost: 1088   maxlim: 1132543   bits: 22/21
c ---[ 790]---> Adder-cost: 1150   maxlim: 1136383   bits: 22/21
c ---[ 788]---> Adder-cost: 1158   maxlim: 1140351   bits: 22/21
c ---[ 786]---> Adder-cost: 1236   maxlim: 1142911   bits: 22/21
c ---[ 784]---> Adder-cost: 1334   maxlim: 1145471   bits: 22/21
c ---[ 782]---> Adder-cost: 1220   maxlim: 1146751   bits: 22/21
c ---[ 780]---> Adder-cost: 1358   maxlim: 1148031   bits: 22/21
c ---[ 778]---> Adder-cost: 1294   maxlim: 1146751   bits: 22/21
c ---[ 776]---> Adder-cost: 1270   maxlim: 1145471   bits: 22/21
c ---[ 774]---> Adder-cost: 1242   maxlim: 1142911   bits: 22/21
c ---[ 772]---> Adder-cost: 1226   maxlim: 1140351   bits: 22/21
c ---[ 770]---> Adder-cost: 1148   maxlim: 1136511   bits: 22/21
c ---[ 768]---> Adder-cost: 1122   maxlim: 1132415   bits: 22/21
c ---[ 766]---> Adder-cost: 1064   maxlim: 1127295   bits: 22/21
c ---[ 764]---> Adder-cost: 1038   maxlim: 1122175   bits: 22/21
c ---[ 762]---> Adder-cost: 932   maxlim: 1116031   bits: 22/21
c ---[ 760]---> Adder-cost: 858   maxlim: 1109631   bits: 22/21
c ---[ 758]---> Adder-cost: 754   maxlim: 1101951   bits: 22/21
c ---[ 756]---> Adder-cost: 642   maxlim: 1094271   bits: 22/21
c ---[ 754]---> Adder-cost: 560   maxlim: 1086591   bits: 22/21
c ---[ 752]---> Adder-cost: 494   maxlim: 1078527   bits: 22/21
c ---[ 750]---> Adder-cost: 378   maxlim: 1070847   bits: 22/21
c ---[ 748]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 746]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 744]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 742]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 740]---> Adder-cost: 352   maxlim: 1070975   bits: 22/21
c ---[ 738]---> Adder-cost: 416   maxlim: 1078655   bits: 22/21
c ---[ 736]---> Adder-cost: 490   maxlim: 1086335   bits: 22/21
c ---[ 734]---> Adder-cost: 550   maxlim: 1094015   bits: 22/21
c ---[ 732]---> Adder-cost: 628   maxlim: 1101695   bits: 22/21
c ---[ 730]---> Adder-cost: 658   maxlim: 1109503   bits: 22/21
c ---[ 728]---> Adder-cost: 942   maxlim: 1115903   bits: 22/21
c ---[ 726]---> Adder-cost: 968   maxlim: 1122303   bits: 22/21
c ---[ 724]---> Adder-cost: 948   maxlim: 1127423   bits: 22/21
c ---[ 722]---> Adder-cost: 1004   maxlim: 1132543   bits: 22/21
c ---[ 720]---> Adder-cost: 1086   maxlim: 1136383   bits: 22/21
c ---[ 718]---> Adder-cost: 1088   maxlim: 1140351   bits: 22/21
c ---[ 716]---> Adder-cost: 1110   maxlim: 1142911   bits: 22/21
c ---[ 714]---> Adder-cost: 1072   maxlim: 1145087   bits: 22/21
c ---[ 712]---> Adder-cost: 1192   maxlim: 1146367   bits: 22/21
c ---[ 710]---> Adder-cost: 1182   maxlim: 1147647   bits: 22/21
c ---[ 708]---> Adder-cost: 1200   maxlim: 1146367   bits: 22/21
c ---[ 706]---> Adder-cost: 1182   maxlim: 1145471   bits: 22/21
c ---[ 704]---> Adder-cost: 1194   maxlim: 1142911   bits: 22/21
c ---[ 702]---> Adder-cost: 1212   maxlim: 1140351   bits: 22/21
c ---[ 700]---> Adder-cost: 1120   maxlim: 1136511   bits: 22/21
c ---[ 698]---> Adder-cost: 1120   maxlim: 1132415   bits: 22/21
c ---[ 696]---> Adder-cost: 1082   maxlim: 1127295   bits: 22/21
c ---[ 694]---> Adder-cost: 984   maxlim: 1122175   bits: 22/21
c ---[ 692]---> Adder-cost: 960   maxlim: 1116031   bits: 22/21
c ---[ 690]---> Adder-cost: 834   maxlim: 1109631   bits: 22/21
c ---[ 688]---> Adder-cost: 774   maxlim: 1101951   bits: 22/21
c ---[ 686]---> Adder-cost: 658   maxlim: 1094271   bits: 22/21
c ---[ 684]---> Adder-cost: 566   maxlim: 1086591   bits: 22/21
c ---[ 682]---> Adder-cost: 486   maxlim: 1078527   bits: 22/21
c ---[ 680]---> Adder-cost: 386   maxlim: 1070847   bits: 22/21
c ---[ 678]---> Adder-cost: 290   maxlim: 1063679   bits: 22/21
c ---[ 676]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 674]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 672]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 670]---> Adder-cost: 416   maxlim: 1071359   bits: 22/21
c ---[ 668]---> Adder-cost: 404   maxlim: 1079039   bits: 22/21
c ---[ 666]---> Adder-cost: 456   maxlim: 1086719   bits: 22/21
c ---[ 664]---> Adder-cost: 542   maxlim: 1094399   bits: 22/21
c ---[ 662]---> Adder-cost: 598   maxlim: 1102079   bits: 22/21
c ---[ 660]---> Adder-cost: 826   maxlim: 1108479   bits: 22/21
c ---[ 658]---> Adder-cost: 794   maxlim: 1113599   bits: 22/21
c ---[ 656]---> Adder-cost: 916   maxlim: 1117439   bits: 22/21
c ---[ 654]---> Adder-cost: 914   maxlim: 1119999   bits: 22/21
c ---[ 652]---> Adder-cost: 968   maxlim: 1121279   bits: 22/21
c ---[ 650]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 648]---> Adder-cost: 884   maxlim: 1119999   bits: 22/21
c ---[ 646]---> Adder-cost: 878   maxlim: 1117439   bits: 22/21
c ---[ 644]---> Adder-cost: 876   maxlim: 1113599   bits: 22/21
c ---[ 642]---> Adder-cost: 834   maxlim: 1108479   bits: 22/21
c ---[ 640]---> Adder-cost: 752   maxlim: 1102079   bits: 22/21
c ---[ 638]---> Adder-cost: 656   maxlim: 1094399   bits: 22/21
c ---[ 636]---> Adder-cost: 574   maxlim: 1086719   bits: 22/21
c ---[ 634]---> Adder-cost: 496   maxlim: 1079039   bits: 22/21
c ---[ 632]---> Adder-cost: 394   maxlim: 1071359   bits: 22/21
c ---[ 630]---> Adder-cost: 286   maxlim: 1063679   bits: 22/21
c ---[ 628]---> Adder-cost: 168   maxlim: 1055999   bits: 22/21
c ---[ 626]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 624]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 622]---> Adder-cost: 348   maxlim: 1071359   bits: 22/21
c ---[ 620]---> Adder-cost: 424   maxlim: 1079039   bits: 22/21
c ---[ 618]---> Adder-cost: 490   maxlim: 1086719   bits: 22/21
c ---[ 616]---> Adder-cost: 544   maxlim: 1094399   bits: 22/21
c ---[ 614]---> Adder-cost: 620   maxlim: 1102079   bits: 22/21
c ---[ 612]---> Adder-cost: 930   maxlim: 1108479   bits: 22/21
c ---[ 610]---> Adder-cost: 908   maxlim: 1113599   bits: 22/21
c ---[ 608]---> Adder-cost: 924   maxlim: 1117439   bits: 22/21
c ---[ 606]---> Adder-cost: 894   maxlim: 1119999   bits: 22/21
c ---[ 604]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 602]---> Adder-cost: 952   maxlim: 1121151   bits: 22/21
c ---[ 600]---> Adder-cost: 886   maxlim: 1119871   bits: 22/21
c ---[ 598]---> Adder-cost: 894   maxlim: 1117311   bits: 22/21
c ---[ 596]---> Adder-cost: 860   maxlim: 1113471   bits: 22/21
c ---[ 594]---> Adder-cost: 812   maxlim: 1108351   bits: 22/21
c ---[ 592]---> Adder-cost: 766   maxlim: 1101951   bits: 22/21
c ---[ 590]---> Adder-cost: 658   maxlim: 1094271   bits: 22/21
c ---[ 588]---> Adder-cost: 580   maxlim: 1086591   bits: 22/21
c ---[ 586]---> Adder-cost: 488   maxlim: 1078911   bits: 22/21
c ---[ 584]---> Adder-cost: 368   maxlim: 1071231   bits: 22/21
c ---[ 582]---> Adder-cost: 282   maxlim: 1063551   bits: 22/21
c ---[ 580]---> Adder-cost: 170   maxlim: 1055871   bits: 22/21
c ---[ 579]---> BDD-cost:   21
c ---[ 578]---> BDD-cost:   33
c ---[ 577]---> BDD-cost:   45
c ---[ 576]---> BDD-cost:   57
c ---[ 575]---> BDD-cost:   69
c ---[ 574]---> BDD-cost:   81
c ---[ 573]---> BDD-cost:   93
c ---[ 572]---> BDD-cost:   95
c ---[ 571]---> BDD-cost:  117
c ---[ 570]---> BDD-cost:   21
c ---[ 569]---> BDD-cost:   33
c ---[ 568]---> BDD-cost:   45
c ---[ 567]---> BDD-cost:   57
c ---[ 566]---> BDD-cost:   69
c ---[ 565]---> BDD-cost:   81
c ---[ 564]---> BDD-cost:   93
c ---[ 563]---> BDD-cost:  105
c ---[ 562]---> BDD-cost:  117
c ---[ 561]---> BDD-cost:   21
c ---[ 560]---> BDD-cost:   33
c ---[ 559]---> BDD-cost:   45
c ---[ 558]---> BDD-cost:   57
c ---[ 557]---> BDD-cost:   69
c ---[ 556]---> BDD-cost:   81
c ---[ 555]---> BDD-cost:   93
c ---[ 554]---> BDD-cost:  105
c ---[ 553]---> BDD-cost:  117
c ---[ 552]---> BDD-cost:    9
c ---[ 551]---> BDD-cost:    9
c ---[ 550]---> BDD-cost:    9
c ---[ 549]---> BDD-cost:    9
c ---[ 548]---> BDD-cost:    9
c ---[ 547]---> BDD-cost:   21
c ---[ 546]---> BDD-cost:   33
c ---[ 545]---> BDD-cost:   45
c ---[ 544]---> BDD-cost:   47
c ---[ 543]---> BDD-cost:   21
c ---[ 542]---> BDD-cost:   33
c ---[ 541]---> BDD-cost:   45
c ---[ 540]---> BDD-cost:   57
c ---[ 539]---> BDD-cost:   69
c ---[ 538]---> BDD-cost:   81
c ---[ 537]---> BDD-cost:   93
c ---[ 536]---> BDD-cost:  105
c ---[ 535]---> BDD-cost:  117
c ---[ 534]---> BDD-cost:    9
c ---[ 533]---> BDD-cost:    9
c ---[ 532]---> BDD-cost:    9
c ---[ 531]---> BDD-cost:   21
c ---[ 530]---> BDD-cost:   33
c ---[ 529]---> BDD-cost:   45
c ---[ 528]---> BDD-cost:   47
c ---[ 527]---> BDD-cost:   61
c ---[ 526]---> BDD-cost:   81
c ---[ 525]---> BDD-cost:   83
c ---[ 524]---> BDD-cost:  105
c ---[ 523]---> BDD-cost:  107
c ---[ 522]---> BDD-cost:   21
c ---[ 521]---> BDD-cost:   33
c ---[ 520]---> BDD-cost:   45
c ---[ 519]---> BDD-cost:   57
c ---[ 518]---> BDD-cost:   69
c ---[ 517]---> BDD-cost:   81
c ---[ 516]---> BDD-cost:   47
c ---[ 515]---> BDD-cost:   59
c ---[ 514]---> BDD-cost:   71
c ---[ 513]---> BDD-cost:   21
c ---[ 512]---> BDD-cost:   33
c ---[ 511]---> BDD-cost:   45
c ---[ 510]---> BDD-cost:   57
c ---[ 509]---> BDD-cost:   69
c ---[ 508]---> BDD-cost:   81
c ---[ 507]---> BDD-cost:   93
c ---[ 506]---> BDD-cost:  105
c ---[ 505]---> BDD-cost:  117
c ---[ 504]---> BDD-cost:    9
c ---[ 503]---> BDD-cost:    9
c ---[ 502]---> BDD-cost:    9
c ---[ 501]---> BDD-cost:    9
c ---[ 500]---> BDD-cost:    9
c ---[ 499]---> BDD-cost:   21
c ---[ 498]---> BDD-cost:   33
c ---[ 497]---> BDD-cost:   45
c ---[ 496]---> BDD-cost:   57
c ---[ 495]---> BDD-cost:   21
c ---[ 494]---> BDD-cost:   33
c ---[ 493]---> BDD-cost:   23
c ---[ 492]---> BDD-cost:   35
c ---[ 491]---> BDD-cost:   69
c ---[ 490]---> BDD-cost:   81
c ---[ 489]---> BDD-cost:   71
c ---[ 488]---> BDD-cost:   83
c ---[ 487]---> BDD-cost:   71
c ---[ 486]---> BDD-cost:    9
c ---[ 485]---> BDD-cost:    9
c ---[ 484]---> BDD-cost:    9
c ---[ 483]---> BDD-cost:   21
c ---[ 482]---> BDD-cost:   33
c ---[ 481]---> BDD-cost:   45
c ---[ 480]---> BDD-cost:   57
c ---[ 479]---> BDD-cost:   69
c ---[ 478]---> BDD-cost:   81
c ---[ 477]---> BDD-cost:   93
c ---[ 476]---> BDD-cost:  105
c ---[ 475]---> BDD-cost:  117
c ---[ 474]---> BDD-cost:   21
c ---[ 473]---> BDD-cost:   33
c ---[ 472]---> BDD-cost:   45
c ---[ 471]---> BDD-cost:   57
c ---[ 470]---> BDD-cost:   69
c ---[ 469]---> BDD-cost:   81
c ---[ 468]---> BDD-cost:   93
c ---[ 467]---> BDD-cost:  105
c ---[ 466]---> BDD-cost:  117
c ---[ 465]---> BDD-cost:   21
c ---[ 464]---> BDD-cost:   33
c ---[ 463]---> BDD-cost:   45
c ---[ 462]---> BDD-cost:   57
c ---[ 461]---> BDD-cost:   69
c ---[ 460]---> BDD-cost:   81
c ---[ 459]---> BDD-cost:   93
c ---[ 458]---> BDD-cost:  105
c ---[ 457]---> BDD-cost:  117
c ---[ 456]---> BDD-cost:    9
c ---[ 455]---> BDD-cost:    9
c ---[ 454]---> BDD-cost:    9
c ---[ 453]---> BDD-cost:    9
c ---[ 452]---> BDD-cost:    9
c ---[ 451]---> BDD-cost:   21
c ---[ 450]---> BDD-cost:   33
c ---[ 449]---> BDD-cost:   45
c ---[ 448]---> BDD-cost:   57
c ---[ 447]---> BDD-cost:   21
c ---[ 446]---> BDD-cost:   33
c ---[ 445]---> BDD-cost:   35
c ---[ 444]---> BDD-cost:   47
c ---[ 443]---> BDD-cost:   59
c ---[ 442]---> BDD-cost:   71
c ---[ 441]---> BDD-cost:   83
c ---[ 440]---> BDD-cost:   95
c ---[ 439]---> BDD-cost:  107
c ---[ 438]---> BDD-cost:    9
c ---[ 437]---> BDD-cost:    9
c ---[ 436]---> BDD-cost:    9
c ---[ 435]---> BDD-cost:   21
c ---[ 434]---> BDD-cost:   33
c ---[ 433]---> BDD-cost:   45
c ---[ 432]---> BDD-cost:   47
c ---[ 431]---> BDD-cost:   69
c ---[ 430]---> BDD-cost:   81
c ---[ 429]---> BDD-cost:   93
c ---[ 428]---> BDD-cost:   95
c ---[ 427]---> BDD-cost:  117
c ---[ 426]---> BDD-cost:   21
c ---[ 425]---> BDD-cost:   33
c ---[ 424]---> BDD-cost:   45
c ---[ 423]---> BDD-cost:   57
c ---[ 422]---> BDD-cost:   69
c ---[ 421]---> BDD-cost:   81
c ---[ 420]---> BDD-cost:   93
c ---[ 419]---> BDD-cost:  101
c ---[ 418]---> BDD-cost:   95
c ---[ 417]---> BDD-cost:   21
c ---[ 416]---> BDD-cost:   33
c ---[ 415]---> BDD-cost:   45
c ---[ 414]---> BDD-cost:   57
c ---[ 413]---> BDD-cost:   69
c ---[ 412]---> BDD-cost:   81
c ---[ 411]---> BDD-cost:   93
c ---[ 410]---> BDD-cost:  105
c ---[ 409]---> BDD-cost:  117
c ---[ 408]---> BDD-cost:    9
c ---[ 407]---> BDD-cost:    9
c ---[ 406]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:   21
c ---[ 402]---> BDD-cost:   33
c ---[ 401]---> BDD-cost:   45
c ---[ 400]---> BDD-cost:   57
c ---[ 399]---> BDD-cost:   21
c ---[ 398]---> BDD-cost:   33
c ---[ 397]---> BDD-cost:   45
c ---[ 396]---> BDD-cost:   57
c ---[ 395]---> BDD-cost:   69
c ---[ 394]---> BDD-cost:   81
c ---[ 393]---> BDD-cost:   71
c ---[ 392]---> BDD-cost:   83
c ---[ 391]---> BDD-cost:   71
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:   21
c ---[ 386]---> BDD-cost:   33
c ---[ 385]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:   57
c ---[ 383]---> BDD-cost:   59
c ---[ 382]---> BDD-cost:   81
c ---[ 381]---> BDD-cost:   83
c ---[ 380]---> BDD-cost:  105
c ---[ 379]---> BDD-cost:  107
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:   33
c ---[ 376]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   57
c ---[ 374]---> BDD-cost:   69
c ---[ 373]---> BDD-cost:   81
c ---[ 372]---> BDD-cost:   93
c ---[ 371]---> BDD-cost:  105
c ---[ 370]---> BDD-cost:  117
c ---[ 369]---> BDD-cost:   21
c ---[ 368]---> BDD-cost:   33
c ---[ 367]---> BDD-cost:   45
c ---[ 366]---> BDD-cost:   57
c ---[ 365]---> BDD-cost:   69
c ---[ 364]---> BDD-cost:   81
c ---[ 363]---> BDD-cost:   93
c ---[ 362]---> BDD-cost:  105
c ---[ 361]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:   21
c ---[ 354]---> BDD-cost:   33
c ---[ 353]---> BDD-cost:   45
c ---[ 352]---> BDD-cost:   57
c ---[ 351]---> BDD-cost:   11
c ---[ 350]---> BDD-cost:   11
c ---[ 349]---> BDD-cost:   23
c ---[ 348]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   47
c ---[ 346]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   71
c ---[ 344]---> BDD-cost:   59
c ---[ 343]---> BDD-cost:   95
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:   21
c ---[ 338]---> BDD-cost:   33
c ---[ 337]---> BDD-cost:   45
c ---[ 336]---> BDD-cost:   47
c ---[ 335]---> BDD-cost:   69
c ---[ 334]---> BDD-cost:   81
c ---[ 333]---> BDD-cost:   93
c ---[ 332]---> BDD-cost:   95
c ---[ 331]---> BDD-cost:  117
c ---[ 330]---> BDD-cost:   21
c ---[ 329]---> BDD-cost:   33
c ---[ 328]---> BDD-cost:   45
c ---[ 327]---> BDD-cost:   57
c ---[ 326]---> BDD-cost:   69
c ---[ 325]---> BDD-cost:   81
c ---[ 324]---> BDD-cost:   93
c ---[ 323]---> BDD-cost:  105
c ---[ 322]---> BDD-cost:   95
c ---[ 321]---> BDD-cost:   21
c ---[ 320]---> BDD-cost:   33
c ---[ 319]---> BDD-cost:   45
c ---[ 318]---> BDD-cost:   57
c ---[ 317]---> BDD-cost:   69
c ---[ 316]---> BDD-cost:   71
c ---[ 315]---> BDD-cost:   83
c ---[ 314]---> BDD-cost:   95
c ---[ 313]---> BDD-cost:   83
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:   21
c ---[ 306]---> BDD-cost:   33
c ---[ 305]---> BDD-cost:   45
c ---[ 304]---> BDD-cost:   57
c ---[ 303]---> BDD-cost:   21
c ---[ 302]---> BDD-cost:   33
c ---[ 301]---> BDD-cost:   45
c ---[ 300]---> BDD-cost:   57
c ---[ 299]---> BDD-cost:   69
c ---[ 298]---> BDD-cost:   81
c ---[ 297]---> BDD-cost:   71
c ---[ 296]---> BDD-cost:   83
c ---[ 295]---> BDD-cost:   71
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:   11
c ---[ 290]---> BDD-cost:   23
c ---[ 289]---> BDD-cost:   45
c ---[ 288]---> BDD-cost:   47
c ---[ 287]---> BDD-cost:   69
c ---[ 286]---> BDD-cost:   71
c ---[ 285]---> BDD-cost:   93
c ---[ 284]---> BDD-cost:   95
c ---[ 283]---> BDD-cost:  117
c ---[ 282]---> BDD-cost:   21
c ---[ 281]---> BDD-cost:   33
c ---[ 280]---> BDD-cost:   45
c ---[ 279]---> BDD-cost:   57
c ---[ 278]---> BDD-cost:   69
c ---[ 277]---> BDD-cost:   81
c ---[ 276]---> BDD-cost:   93
c ---[ 275]---> BDD-cost:  105
c ---[ 274]---> BDD-cost:  117
c ---[ 273]---> BDD-cost:   21
c ---[ 272]---> BDD-cost:   33
c ---[ 271]---> BDD-cost:   45
c ---[ 270]---> BDD-cost:   57
c ---[ 269]---> BDD-cost:   69
c ---[ 268]---> BDD-cost:   81
c ---[ 267]---> BDD-cost:   93
c ---[ 266]---> BDD-cost:  105
c ---[ 265]---> BDD-cost:  117
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:   21
c ---[ 258]---> BDD-cost:   33
c ---[ 257]---> BDD-cost:   45
c ---[ 256]---> BDD-cost:   57
c ---[ 255]---> BDD-cost:   21
c ---[ 254]---> BDD-cost:   33
c ---[ 253]---> BDD-cost:   23
c ---[ 252]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   47
c ---[ 250]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   71
c ---[ 248]---> BDD-cost:   59
c ---[ 247]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   21
c ---[ 242]---> BDD-cost:   33
c ---[ 241]---> BDD-cost:   45
c ---[ 240]---> BDD-cost:   57
c ---[ 239]---> BDD-cost:   69
c ---[ 238]---> BDD-cost:   81
c ---[ 237]---> BDD-cost:   93
c ---[ 236]---> BDD-cost:   95
c ---[ 235]---> BDD-cost:  117
c ---[ 234]---> BDD-cost:   21
c ---[ 233]---> BDD-cost:   33
c ---[ 232]---> BDD-cost:   45
c ---[ 231]---> BDD-cost:   57
c ---[ 230]---> BDD-cost:   69
c ---[ 229]---> BDD-cost:   81
c ---[ 228]---> BDD-cost:   93
c ---[ 227]---> BDD-cost:  105
c ---[ 226]---> BDD-cost:  117
c ---[ 225]---> BDD-cost:   21
c ---[ 224]---> BDD-cost:   33
c ---[ 223]---> BDD-cost:   45
c ---[ 222]---> BDD-cost:   57
c ---[ 221]---> BDD-cost:   69
c ---[ 220]---> BDD-cost:   81
c ---[ 219]---> BDD-cost:   71
c ---[ 218]---> BDD-cost:  105
c ---[ 217]---> BDD-cost:   95
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:   21
c ---[ 210]---> BDD-cost:   33
c ---[ 209]---> BDD-cost:   45
c ---[ 208]---> BDD-cost:   43
c ---[ 207]---> BDD-cost:   21
c ---[ 206]---> BDD-cost:   33
c ---[ 205]---> BDD-cost:   45
c ---[ 204]---> BDD-cost:   57
c ---[ 203]---> BDD-cost:   69
c ---[ 202]---> BDD-cost:   81
c ---[ 201]---> BDD-cost:   71
c ---[ 200]---> BDD-cost:   83
c ---[ 199]---> BDD-cost:   71
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   33
c ---[ 193]---> BDD-cost:   45
c ---[ 192]---> BDD-cost:   47
c ---[ 191]---> BDD-cost:   69
c ---[ 190]---> BDD-cost:   71
c ---[ 189]---> BDD-cost:   93
c ---[ 188]---> BDD-cost:   95
c ---[ 187]---> BDD-cost:  117
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   29
c ---[ 183]---> BDD-cost:   29
c ---[ 182]---> BDD-cost:   29
c ---[ 181]---> BDD-cost:   41
c ---[ 180]---> BDD-cost:   53
c ---[ 179]---> BDD-cost:   65
c ---[ 178]---> BDD-cost:   77
c ---[ 177]---> BDD-cost:   21
c ---[ 176]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:   45
c ---[ 174]---> BDD-cost:   57
c ---[ 173]---> BDD-cost:   59
c ---[ 172]---> BDD-cost:   81
c ---[ 171]---> BDD-cost:   83
c ---[ 170]---> BDD-cost:  105
c ---[ 169]---> BDD-cost:  107
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:   21
c ---[ 162]---> BDD-cost:   33
c ---[ 161]---> BDD-cost:   45
c ---[ 160]---> BDD-cost:   57
c ---[ 159]---> BDD-cost:   21
c ---[ 158]---> BDD-cost:   33
c ---[ 157]---> BDD-cost:   23
c ---[ 156]---> BDD-cost:   35
c ---[ 155]---> BDD-cost:   47
c ---[ 154]---> BDD-cost:   81
c ---[ 153]---> BDD-cost:   83
c ---[ 152]---> BDD-cost:   95
c ---[ 151]---> BDD-cost:  107
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:   21
c ---[ 146]---> BDD-cost:   33
c ---[ 145]---> BDD-cost:   45
c ---[ 144]---> BDD-cost:   47
c ---[ 143]---> BDD-cost:   69
c ---[ 142]---> BDD-cost:   71
c ---[ 141]---> BDD-cost:   93
c ---[ 140]---> BDD-cost:   95
c ---[ 139]---> BDD-cost:  107
c ---[ 138]---> BDD-cost:   21
c ---[ 137]---> BDD-cost:   33
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   35
c ---[ 132]---> BDD-cost:   47
c ---[ 131]---> BDD-cost:   59
c ---[ 130]---> BDD-cost:   71
c ---[ 129]---> BDD-cost:   21
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   45
c ---[ 126]---> BDD-cost:   47
c ---[ 125]---> BDD-cost:   69
c ---[ 124]---> BDD-cost:   71
c ---[ 123]---> BDD-cost:   93
c ---[ 122]---> BDD-cost:   95
c ---[ 121]---> BDD-cost:  117
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:   21
c ---[ 114]---> BDD-cost:   33
c ---[ 113]---> BDD-cost:   45
c ---[ 112]---> BDD-cost:   57
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   33
c ---[ 109]---> BDD-cost:   25
c ---[ 108]---> BDD-cost:   35
c ---[ 107]---> BDD-cost:   59
c ---[ 106]---> BDD-cost:   71
c ---[ 105]---> BDD-cost:   83
c ---[ 104]---> BDD-cost:   95
c ---[ 103]---> BDD-cost:   83
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:  273
c ---[  98]---> BDD-cost:  273
c ---[  97]---> BDD-cost:  273
c ---[  96]---> BDD-cost:  273
c ---[  95]---> BDD-cost:  269
c ---[  94]---> BDD-cost:  141
c ---[  93]---> BDD-cost:  141
c ---[  92]---> BDD-cost:  271
c ---[  91]---> BDD-cost:  273
c ---[  90]---> BDD-cost:  269
c ---[  89]---> BDD-cost:  273
c ---[  88]---> BDD-cost:  263
c ---[  87]---> BDD-cost:  141
c ---[  86]---> BDD-cost:  141
c ---[  85]---> BDD-cost:  273
c ---[  84]---> BDD-cost:  263
c ---[  83]---> BDD-cost:  265
c ---[  82]---> BDD-cost:  273
c ---[  81]---> BDD-cost:  273
c ---[  80]---> BDD-cost:  141
c ---[  79]---> BDD-cost:  141
c ---[  78]---> BDD-cost:  263
c ---[  77]---> BDD-cost:  273
c ---[  76]---> BDD-cost:  273
c ---[  75]---> BDD-cost:  239
c ---[  74]---> BDD-cost:  263
c ---[  73]---> BDD-cost:  141
c ---[  72]---> BDD-cost:  141
c ---[  71]---> BDD-cost:  269
c ---[  70]---> BDD-cost:  227
c ---[  69]---> BDD-cost:  263
c ---[  68]---> BDD-cost:  267
c ---[  67]---> BDD-cost:  263
c ---[  66]---> BDD-cost:  141
c ---[  65]---> BDD-cost:  141
c ---[  64]---> BDD-cost:  239
c ---[  63]---> BDD-cost:  265
c ---[  62]---> BDD-cost:  251
c ---[  61]---> BDD-cost:  273
c ---[  60]---> BDD-cost:  273
c ---[  59]---> BDD-cost:  141
c ---[  58]---> BDD-cost:  141
c ---[  57]---> BDD-cost:  273
c ---[  56]---> BDD-cost:  273
c ---[  55]---> BDD-cost:  273
c ---[  54]---> BDD-cost:  273
c ---[  53]---> BDD-cost:  251
c ---[  52]---> BDD-cost:  141
c ---[  51]---> BDD-cost:  141
c ---[  50]---> BDD-cost:  263
c ---[  49]---> BDD-cost:  273
c ---[  48]---> BDD-cost:  273
c ---[  47]---> BDD-cost:  273
c ---[  46]---> BDD-cost:  273
c ---[  45]---> BDD-cost:  115
c ---[  44]---> BDD-cost:  141
c ---[  43]---> BDD-cost:  263
c ---[  42]---> BDD-cost:  263
c ---[  41]---> BDD-cost:  273
c ---[  40]---> BDD-cost:  233
c ---[  39]---> BDD-cost:  273
c ---[  38]---> BDD-cost:  141
c ---[  37]---> BDD-cost:  141
c ---[  36]---> BDD-cost:  261
c ---[  35]---> BDD-cost:  239
c ---[  34]---> BDD-cost:  263
c ---[  33]---> BDD-cost:  273
c ---[  32]---> BDD-cost:  263
c ---[  31]---> BDD-cost:  141
c ---[  30]---> BDD-cost:  141
c ---[  29]---> Adder-cost: 1446   maxlim: 828   bits: 10/10
c ---[  28]---> Adder-cost: 1416   maxlim: 828   bits: 10/10
c ---[  27]---> Adder-cost: 1412   maxlim: 828   bits: 10/10
c ---[  26]---> Adder-cost: 1448   maxlim: 828   bits: 10/10
c ---[  25]---> Adder-cost: 1428   maxlim: 828   bits: 10/10
c ---[  24]---> Adder-cost: 1438   maxlim: 828   bits: 10/10
c ---[  23]---> Adder-cost: 1438   maxlim: 828   bits: 10/10
c ---[  22]---> Adder-cost: 1388   maxlim: 828   bits: 10/10
c ---[  21]---> Adder-cost: 1470   maxlim: 828   bits: 10/10
c ---[  20]---> Adder-cost: 1388   maxlim: 828   bits: 10/10
c ---[  19]---> BDD-cost: 1307
c ---[  18]---> BDD-cost: 1302
c ---[  17]---> BDD-cost: 1303
c ---[  16]---> BDD-cost: 1305
c ---[  15]---> BDD-cost: 1302
c ---[  14]---> BDD-cost: 1299
c ---[  13]---> BDD-cost: 1307
c ---[  12]---> BDD-cost: 1307
c ---[  11]---> BDD-cost: 1305
c ---[  10]---> BDD-cost: 1307
c ---[   9]---> BDD-cost:  721
c ---[   8]---> BDD-cost:  716
c ---[   7]---> BDD-cost:  716
c ---[   6]---> BDD-cost:  721
c ---[   5]---> BDD-cost:  717
c ---[   4]---> BDD-cost:  731
c ---[   3]---> BDD-cost:  675
c ---[   2]---> BDD-cost:  714
c ---[   1]---> BDD-cost:  723
c ---[   0]---> BDD-cost:  731
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2307742  7817718 |  769247       0        0     nan |  0.000 % |
c |       102 | 2307715  7817623 |  846171     100      538     5.4 |  1.956 % |
c |       264 | 2307712  7817614 |  930788     257    11092    43.2 |  1.956 % |
c |       490 | 2307703  7817587 | 1023867     474    15162    32.0 |  1.957 % |
c |       828 | 2307703  7817587 | 1126254     812    28025    34.5 |  1.957 % |
c |      1335 | 2307635  7817347 | 1238879    1306    63664    48.7 |  1.957 % |
c |      2094 | 2307635  7817347 | 1362767    2065    92386    44.7 |  1.957 % |
c |      3234 | 2307451  7816689 | 1499044    3185   179837    56.5 |  1.959 % |
c |      4943 | 2307299  7816151 | 1648949    4839   319898    66.1 |  1.961 % |
c |      7507 | 2306792  7814328 | 1813844    7361   559199    76.0 |  1.965 % |
c |     11351 | 2306394  7812896 | 1995228   11168   872187    78.1 |  1.969 % |
c |     17117 | 2306106  7811868 | 2194751   16900  1534364    90.8 |  1.971 % |
c |     25767 | 2305918  7811204 | 2414226   25531  2567240   100.6 |  1.973 % |
c |     38742 | 2305589  7810019 | 2655649   38464  4263347   110.8 |  1.977 % |
c |     58203 | 2304913  7807599 | 2921214   57819  6790674   117.4 |  1.983 % |
#### 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): 1.23 1.07 0.98 2/54 16430
Raw data (stat): 16430 (runsolver) R 16429 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540163385 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.99995 s]
Raw data (loadavg): 1.20 1.07 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 9262 0 0 0 969 29 0 0 25 0 1 0 540163385 37269504 7984 4294967295 134512640 134672761 3221224624 3221221424 134523837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9099 7984 603 41 0 9058 0
vsize: 36396
[startup+20.0005 s]
Raw data (loadavg): 1.17 1.07 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 10291 0 0 0 1966 32 0 0 25 0 1 0 540163385 39956480 9013 4294967295 134512640 134672761 3221224624 3221223616 134597195 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9013 603 41 0 9714 0
vsize: 39020
[startup+30.0009 s]
Raw data (loadavg): 1.14 1.06 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 38736 0 0 0 2900 98 0 0 25 0 1 0 540163385 172777472 37443 4294967295 134512640 134672761 3221224624 3221217272 134543013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42182 37443 603 41 0 42141 0
vsize: 168728
[startup+40.0013 s]
Raw data (loadavg): 1.12 1.06 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 52733 0 0 0 3865 133 0 0 25 0 1 0 540163385 261828608 51440 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63923 51440 603 41 0 63882 0
vsize: 255692
[startup+50.0021 s]
Raw data (loadavg): 1.10 1.06 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 52880 0 0 0 4865 134 0 0 25 0 1 0 540163385 262500352 51587 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64087 51587 603 41 0 64046 0
vsize: 256348
[startup+60.0023 s]
Raw data (loadavg): 1.08 1.06 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 52963 0 0 0 5864 135 0 0 25 0 1 0 540163385 262770688 51670 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64153 51670 603 41 0 64112 0
vsize: 256612
[startup+70.0027 s]
Raw data (loadavg): 1.07 1.05 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53004 0 0 0 6864 135 0 0 25 0 1 0 540163385 262901760 51711 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64185 51711 603 41 0 64144 0
vsize: 256740
[startup+80.0035 s]
Raw data (loadavg): 1.06 1.05 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53041 0 0 0 7864 135 0 0 25 0 1 0 540163385 263172096 51748 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64251 51748 603 41 0 64210 0
vsize: 257004
[startup+90.0037 s]
Raw data (loadavg): 1.05 1.05 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53084 0 0 0 8864 135 0 0 25 0 1 0 540163385 263307264 51791 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64284 51791 603 41 0 64243 0
vsize: 257136
[startup+100.004 s]
Raw data (loadavg): 1.04 1.05 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53154 0 0 0 9863 136 0 0 25 0 1 0 540163385 263577600 51861 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64350 51861 603 41 0 64309 0
vsize: 257400
[startup+110.005 s]
Raw data (loadavg): 1.04 1.05 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53220 0 0 0 10863 137 0 0 25 0 1 0 540163385 263847936 51927 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64416 51927 603 41 0 64375 0
vsize: 257664
[startup+120.006 s]
Raw data (loadavg): 1.03 1.04 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53267 0 0 0 11863 137 0 0 25 0 1 0 540163385 263983104 51974 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64449 51974 603 41 0 64408 0
vsize: 257796
[startup+130.007 s]
Raw data (loadavg): 1.02 1.04 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53321 0 0 0 12862 138 0 0 25 0 1 0 540163385 264249344 52028 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64514 52028 603 41 0 64473 0
vsize: 258056
[startup+140.006 s]
Raw data (loadavg): 1.02 1.04 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53401 0 0 0 13861 138 0 0 25 0 1 0 540163385 264519680 52108 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64580 52108 603 41 0 64539 0
vsize: 258320
[startup+150.008 s]
Raw data (loadavg): 1.02 1.04 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53482 0 0 0 14861 139 0 0 25 0 1 0 540163385 264921088 52189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64678 52189 603 41 0 64637 0
vsize: 258712
[startup+160.008 s]
Raw data (loadavg): 1.01 1.04 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53552 0 0 0 15861 139 0 0 25 0 1 0 540163385 265187328 52259 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64743 52259 603 41 0 64702 0
vsize: 258972
[startup+170.009 s]
Raw data (loadavg): 1.01 1.04 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53598 0 0 0 16860 140 0 0 25 0 1 0 540163385 265457664 52305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64809 52305 603 41 0 64768 0
vsize: 259236
[startup+180.01 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53716 0 0 0 17860 141 0 0 25 0 1 0 540163385 265863168 52423 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64908 52423 603 41 0 64867 0
vsize: 259632
[startup+190.01 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53835 0 0 0 18859 142 0 0 25 0 1 0 540163385 266399744 52542 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65039 52542 603 41 0 64998 0
vsize: 260156
[startup+200.01 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53905 0 0 0 19858 143 0 0 25 0 1 0 540163385 266665984 52612 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65104 52612 603 41 0 65063 0
vsize: 260416
[startup+210.011 s]
Raw data (loadavg): 1.00 1.03 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 53998 0 0 0 20858 143 0 0 25 0 1 0 540163385 267071488 52705 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65203 52705 603 41 0 65162 0
vsize: 260812
[startup+220.012 s]
Raw data (loadavg): 1.00 1.03 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54046 0 0 0 21858 144 0 0 25 0 1 0 540163385 267206656 52753 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65236 52753 603 41 0 65195 0
vsize: 260944
[startup+230.012 s]
Raw data (loadavg): 1.00 1.03 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54086 0 0 0 22857 145 0 0 25 0 1 0 540163385 267337728 52793 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65268 52793 603 41 0 65227 0
vsize: 261072
[startup+240.012 s]
Raw data (loadavg): 1.00 1.03 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54135 0 0 0 23857 145 0 0 25 0 1 0 540163385 267603968 52842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65333 52842 603 41 0 65292 0
vsize: 261332
[startup+250.013 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54186 0 0 0 24856 146 0 0 25 0 1 0 540163385 267739136 52893 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65366 52893 603 41 0 65325 0
vsize: 261464
[startup+260.013 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54272 0 0 0 25855 147 0 0 25 0 1 0 540163385 268144640 52979 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65465 52979 603 41 0 65424 0
vsize: 261860
[startup+270.014 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54394 0 0 0 26855 147 0 0 25 0 1 0 540163385 268677120 53101 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65595 53101 603 41 0 65554 0
vsize: 262380
[startup+280.015 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54502 0 0 0 27854 148 0 0 25 0 1 0 540163385 269156352 53209 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65712 53209 603 41 0 65671 0
vsize: 262848
[startup+290.015 s]
Raw data (loadavg): 1.00 1.02 0.98 3/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54594 0 0 0 28853 149 0 0 25 0 1 0 540163385 269553664 53301 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65809 53301 603 41 0 65768 0
vsize: 263236
[startup+300.02 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54680 0 0 0 29854 149 0 0 25 0 1 0 540163385 269824000 53387 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65875 53387 603 41 0 65834 0
vsize: 263500
[startup+310.021 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54749 0 0 0 30854 150 0 0 25 0 1 0 540163385 270090240 53456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65940 53456 603 41 0 65899 0
vsize: 263760
[startup+320.024 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54858 0 0 0 31854 150 0 0 25 0 1 0 540163385 270622720 53565 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66070 53565 603 41 0 66029 0
vsize: 264280
[startup+330.028 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 54954 0 0 0 32854 150 0 0 25 0 1 0 540163385 271028224 53661 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66169 53661 603 41 0 66128 0
vsize: 264676
[startup+340.028 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55101 0 0 0 33853 151 0 0 25 0 1 0 540163385 271560704 53808 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66299 53808 603 41 0 66258 0
vsize: 265196
[startup+350.029 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55293 0 0 0 34853 152 0 0 25 0 1 0 540163385 272363520 54000 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66495 54000 603 41 0 66454 0
vsize: 265980
[startup+360.029 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55348 0 0 0 35852 152 0 0 25 0 1 0 540163385 272629760 54055 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66560 54055 603 41 0 66519 0
vsize: 266240
[startup+370.04 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55404 0 0 0 36853 152 0 0 25 0 1 0 540163385 272760832 54111 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66592 54111 603 41 0 66551 0
vsize: 266368
[startup+380.04 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55473 0 0 0 37853 153 0 0 25 0 1 0 540163385 273162240 54180 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66690 54180 603 41 0 66649 0
vsize: 266760
[startup+390.04 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55576 0 0 0 38852 153 0 0 25 0 1 0 540163385 273559552 54283 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66787 54283 603 41 0 66746 0
vsize: 267148
[startup+400.041 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55665 0 0 0 39852 154 0 0 25 0 1 0 540163385 273825792 54372 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66852 54372 603 41 0 66811 0
vsize: 267408
[startup+410.04 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55744 0 0 0 40852 154 0 0 25 0 1 0 540163385 274223104 54451 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66949 54451 603 41 0 66908 0
vsize: 267796
[startup+420.041 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55870 0 0 0 41851 155 0 0 25 0 1 0 540163385 274755584 54577 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67079 54577 603 41 0 67038 0
vsize: 268316
[startup+430.042 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 55952 0 0 0 42850 156 0 0 25 0 1 0 540163385 275025920 54659 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67145 54659 603 41 0 67104 0
vsize: 268580
[startup+440.045 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56043 0 0 0 43851 156 0 0 25 0 1 0 540163385 275431424 54750 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67244 54750 603 41 0 67203 0
vsize: 268976
[startup+450.046 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56117 0 0 0 44850 157 0 0 25 0 1 0 540163385 275697664 54824 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67309 54824 603 41 0 67268 0
vsize: 269236
[startup+460.046 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56206 0 0 0 45850 157 0 0 25 0 1 0 540163385 276103168 54913 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67408 54913 603 41 0 67367 0
vsize: 269632
[startup+470.047 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56282 0 0 0 46849 158 0 0 25 0 1 0 540163385 276369408 54989 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67473 54989 603 41 0 67432 0
vsize: 269892
[startup+480.047 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56377 0 0 0 47849 159 0 0 25 0 1 0 540163385 276770816 55084 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67571 55084 603 41 0 67530 0
vsize: 270284
[startup+490.047 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56445 0 0 0 48848 159 0 0 25 0 1 0 540163385 277032960 55152 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67635 55152 603 41 0 67594 0
vsize: 270540
[startup+500.048 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56498 0 0 0 49848 160 0 0 25 0 1 0 540163385 277299200 55205 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67700 55205 603 41 0 67659 0
vsize: 270800
[startup+510.048 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56580 0 0 0 50848 160 0 0 25 0 1 0 540163385 277561344 55287 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67764 55287 603 41 0 67723 0
vsize: 271056
[startup+520.048 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56652 0 0 0 51847 160 0 0 25 0 1 0 540163385 277962752 55359 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67862 55359 603 41 0 67821 0
vsize: 271448
[startup+530.049 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56735 0 0 0 52847 161 0 0 25 0 1 0 540163385 278360064 55442 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67959 55442 603 41 0 67918 0
vsize: 271836
[startup+540.05 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56834 0 0 0 53847 161 0 0 25 0 1 0 540163385 278757376 55541 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68056 55541 603 41 0 68015 0
vsize: 272224
[startup+550.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56925 0 0 0 54848 162 0 0 25 0 1 0 540163385 279154688 55632 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68153 55632 603 41 0 68112 0
vsize: 272612
[startup+560.378 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 56989 0 0 0 55879 162 0 0 25 0 1 0 540163385 279425024 55696 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68219 55696 603 41 0 68178 0
vsize: 272876
[startup+570.378 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57074 0 0 0 56878 164 0 0 25 0 1 0 540163385 279691264 55781 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68284 55781 603 41 0 68243 0
vsize: 273136
[startup+580.378 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57131 0 0 0 57878 164 0 0 25 0 1 0 540163385 279953408 55838 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68348 55838 603 41 0 68307 0
vsize: 273392
[startup+590.378 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57260 0 0 0 58877 164 0 0 25 0 1 0 540163385 280485888 55967 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68478 55967 603 41 0 68437 0
vsize: 273912
[startup+600.378 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57393 0 0 0 59877 165 0 0 25 0 1 0 540163385 281022464 56100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68609 56100 603 41 0 68568 0
vsize: 274436
[startup+610.379 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57529 0 0 0 60876 166 0 0 25 0 1 0 540163385 281554944 56236 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68739 56236 603 41 0 68698 0
vsize: 274956
[startup+620.379 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57646 0 0 0 61875 167 0 0 25 0 1 0 540163385 282091520 56353 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68870 56353 603 41 0 68829 0
vsize: 275480
[startup+630.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16430
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57768 0 0 0 62874 168 0 0 25 0 1 0 540163385 282619904 56475 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68999 56475 603 41 0 68958 0
vsize: 275996
[startup+640.38 s]
Raw data (loadavg): 1.00 1.00 0.98 3/57 16465
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57862 0 0 0 63867 174 0 0 25 0 1 0 540163385 283013120 56569 4294967295 134512640 134672761 3221224624 3221223728 134560316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69095 56569 603 41 0 69054 0
vsize: 276380
[startup+650.382 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16483
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 57946 0 0 0 64859 182 0 0 25 0 1 0 540163385 283279360 56653 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69160 56653 603 41 0 69119 0
vsize: 276640
[startup+660.381 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16483
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58044 0 0 0 65859 183 0 0 25 0 1 0 540163385 283684864 56751 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69259 56751 603 41 0 69218 0
vsize: 277036
[startup+670.383 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16483
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58132 0 0 0 66858 184 0 0 25 0 1 0 540163385 284078080 56839 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69355 56839 603 41 0 69314 0
vsize: 277420
[startup+680.383 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16483
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58222 0 0 0 67858 185 0 0 25 0 1 0 540163385 284479488 56929 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69453 56929 603 41 0 69412 0
vsize: 277812
[startup+690.383 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16483
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58311 0 0 0 68857 186 0 0 25 0 1 0 540163385 284745728 57018 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69518 57018 603 41 0 69477 0
vsize: 278072
[startup+700.384 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16483
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58401 0 0 0 69856 186 0 0 25 0 1 0 540163385 285151232 57108 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69617 57108 603 41 0 69576 0
vsize: 278468
[startup+710.383 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16483
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58454 0 0 0 70856 187 0 0 25 0 1 0 540163385 285421568 57161 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69683 57161 603 41 0 69642 0
vsize: 278732
[startup+720.384 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58478 0 0 0 71856 187 0 0 25 0 1 0 540163385 285421568 57185 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69683 57185 603 41 0 69642 0
vsize: 278732
[startup+730.385 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58504 0 0 0 72855 188 0 0 25 0 1 0 540163385 285556736 57211 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69716 57211 603 41 0 69675 0
vsize: 278864
[startup+740.385 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58529 0 0 0 73855 189 0 0 25 0 1 0 540163385 285687808 57236 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69748 57236 603 41 0 69707 0
vsize: 278992
[startup+750.386 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58595 0 0 0 74855 189 0 0 25 0 1 0 540163385 285958144 57302 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69814 57302 603 41 0 69773 0
vsize: 279256
[startup+760.385 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58791 0 0 0 75853 191 0 0 25 0 1 0 540163385 286629888 57498 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69978 57498 603 41 0 69937 0
vsize: 279912
[startup+770.386 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58844 0 0 0 76853 191 0 0 25 0 1 0 540163385 286896128 57551 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70043 57551 603 41 0 70002 0
vsize: 280172
[startup+780.386 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 58952 0 0 0 77852 192 0 0 25 0 1 0 540163385 287289344 57659 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70139 57659 603 41 0 70098 0
vsize: 280556
[startup+790.386 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59048 0 0 0 78852 192 0 0 25 0 1 0 540163385 287694848 57755 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70238 57755 603 41 0 70197 0
vsize: 280952
[startup+800.386 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59177 0 0 0 79852 193 0 0 25 0 1 0 540163385 288235520 57884 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70370 57884 603 41 0 70329 0
vsize: 281480
[startup+810.386 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59304 0 0 0 80851 194 0 0 25 0 1 0 540163385 288763904 58011 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70499 58011 603 41 0 70458 0
vsize: 281996
[startup+820.387 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59429 0 0 0 81850 195 0 0 25 0 1 0 540163385 289169408 58136 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70598 58136 603 41 0 70557 0
vsize: 282392
[startup+830.388 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59513 0 0 0 82850 195 0 0 25 0 1 0 540163385 289570816 58220 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70696 58220 603 41 0 70655 0
vsize: 282784
[startup+840.388 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59574 0 0 0 83850 196 0 0 25 0 1 0 540163385 289841152 58281 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70762 58281 603 41 0 70721 0
vsize: 283048
[startup+850.389 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59649 0 0 0 84850 196 0 0 25 0 1 0 540163385 290111488 58356 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70828 58356 603 41 0 70787 0
vsize: 283312
[startup+860.389 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59744 0 0 0 85849 197 0 0 25 0 1 0 540163385 290516992 58451 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70927 58451 603 41 0 70886 0
vsize: 283708
[startup+870.39 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59853 0 0 0 86849 197 0 0 25 0 1 0 540163385 290910208 58560 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71023 58560 603 41 0 70982 0
vsize: 284092
[startup+880.391 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 59958 0 0 0 87848 198 0 0 25 0 1 0 540163385 291450880 58665 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71155 58665 603 41 0 71114 0
vsize: 284620
[startup+890.39 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60058 0 0 0 88847 199 0 0 25 0 1 0 540163385 291848192 58765 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71252 58765 603 41 0 71211 0
vsize: 285008
[startup+900.391 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60086 0 0 0 89847 200 0 0 25 0 1 0 540163385 291848192 58793 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71252 58793 603 41 0 71211 0
vsize: 285008
[startup+910.392 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60128 0 0 0 90847 200 0 0 25 0 1 0 540163385 292118528 58835 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71318 58835 603 41 0 71277 0
vsize: 285272
[startup+920.392 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60219 0 0 0 91846 201 0 0 25 0 1 0 540163385 292384768 58926 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71383 58926 603 41 0 71342 0
vsize: 285532
[startup+930.392 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60327 0 0 0 92845 202 0 0 25 0 1 0 540163385 292909056 59034 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71511 59034 603 41 0 71470 0
vsize: 286044
[startup+940.393 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60383 0 0 0 93845 203 0 0 25 0 1 0 540163385 293179392 59090 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71577 59090 603 41 0 71536 0
vsize: 286308
[startup+950.393 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60465 0 0 0 94845 203 0 0 25 0 1 0 540163385 293449728 59172 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71643 59172 603 41 0 71602 0
vsize: 286572
[startup+960.393 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60502 0 0 0 95844 204 0 0 25 0 1 0 540163385 293584896 59209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 59209 603 41 0 71635 0
vsize: 286704
[startup+970.394 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60535 0 0 0 96844 204 0 0 25 0 1 0 540163385 293715968 59242 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71708 59242 603 41 0 71667 0
vsize: 286832
[startup+980.395 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60584 0 0 0 97844 205 0 0 25 0 1 0 540163385 293982208 59291 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71773 59291 603 41 0 71732 0
vsize: 287092
[startup+990.395 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16485
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60617 0 0 0 98843 205 0 0 25 0 1 0 540163385 294117376 59324 4294967295 134512640 134672761 3221224624 3221223840 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71806 59324 603 41 0 71765 0
vsize: 287224
[startup+1000.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60651 0 0 0 99843 206 0 0 25 0 1 0 540163385 294252544 59358 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71839 59358 603 41 0 71798 0
vsize: 287356
[startup+1010.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60706 0 0 0 100843 206 0 0 25 0 1 0 540163385 294387712 59413 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71872 59413 603 41 0 71831 0
vsize: 287488
[startup+1020.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60746 0 0 0 101842 207 0 0 25 0 1 0 540163385 294522880 59453 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71905 59453 603 41 0 71864 0
vsize: 287620
[startup+1030.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60790 0 0 0 102842 207 0 0 25 0 1 0 540163385 294789120 59497 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71970 59497 603 41 0 71929 0
vsize: 287880
[startup+1040.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60841 0 0 0 103842 208 0 0 25 0 1 0 540163385 294924288 59548 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72003 59548 603 41 0 71962 0
vsize: 288012
[startup+1050.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60883 0 0 0 104842 208 0 0 25 0 1 0 540163385 295194624 59590 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72069 59590 603 41 0 72028 0
vsize: 288276
[startup+1060.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 60940 0 0 0 105842 208 0 0 25 0 1 0 540163385 295329792 59647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72102 59647 603 41 0 72061 0
vsize: 288408
[startup+1070.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61001 0 0 0 106841 209 0 0 25 0 1 0 540163385 295600128 59708 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72168 59708 603 41 0 72127 0
vsize: 288672
[startup+1080.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61045 0 0 0 107841 209 0 0 25 0 1 0 540163385 295731200 59752 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72200 59752 603 41 0 72159 0
vsize: 288800
[startup+1090.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61099 0 0 0 108841 210 0 0 25 0 1 0 540163385 296001536 59806 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72266 59806 603 41 0 72225 0
vsize: 289064
[startup+1100.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61140 0 0 0 109841 210 0 0 25 0 1 0 540163385 296394752 59847 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72362 59847 603 41 0 72321 0
vsize: 289448
[startup+1110.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61198 0 0 0 110841 210 0 0 25 0 1 0 540163385 296665088 59905 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72428 59905 603 41 0 72387 0
vsize: 289712
[startup+1120.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61253 0 0 0 111841 210 0 0 25 0 1 0 540163385 296935424 59960 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72494 59960 603 41 0 72453 0
vsize: 289976
[startup+1130.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61314 0 0 0 112841 210 0 0 25 0 1 0 540163385 297205760 60021 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72560 60021 603 41 0 72519 0
vsize: 290240
[startup+1140.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61393 0 0 0 113841 211 0 0 25 0 1 0 540163385 297472000 60100 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72625 60100 603 41 0 72584 0
vsize: 290500
[startup+1150.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61449 0 0 0 114841 211 0 0 25 0 1 0 540163385 297742336 60156 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72691 60156 603 41 0 72650 0
vsize: 290764
[startup+1160.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61527 0 0 0 115841 211 0 0 25 0 1 0 540163385 298004480 60234 4294967295 134512640 134672761 3221224624 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72755 60234 603 41 0 72714 0
vsize: 291020
[startup+1170.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61574 0 0 0 116841 211 0 0 25 0 1 0 540163385 298139648 60281 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72788 60281 603 41 0 72747 0
vsize: 291152
[startup+1180.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61627 0 0 0 117841 211 0 0 25 0 1 0 540163385 298409984 60334 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72854 60334 603 41 0 72813 0
vsize: 291416
[startup+1190.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61732 0 0 0 118841 211 0 0 25 0 1 0 540163385 298811392 60439 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72952 60439 603 41 0 72911 0
vsize: 291808
[startup+1200.4 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 16487
Raw data (stat): 16430 (minisat+) R 16429 27222 27221 0 -1 0 61859 0 0 0 119841 212 0 0 25 0 1 0 540163385 299339776 60566 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73081 60566 603 41 0 73040 0
vsize: 292324
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.52 s]
Raw data (loadavg): 1.00 1.00 0.98 1/54 16487
Raw data (stat): 16430 (minisat+) Z 16429 27222 27221 0 -1 12 61861 0 0 0 119841 223 0 0 25 0 1 0 540163385 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.52
CPU time (s): 1200.65
CPU user time (s): 1198.42
CPU system time (s): 2.23666
CPU usage (%): 100.011
Max. virtual memory (Kb): 292324
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####