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 14617

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 00:24:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19732 boxname=wulflinc30 idbench=1518 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0633214154e8bab02f648560b9bfa54f  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-neos6.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-neos6.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-neos6.opb
IDLAUNCH: 19732
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        706432 kB
Buffers:         20364 kB
Cached:         272580 kB
SwapCached:          0 kB
Active:         200644 kB
Inactive:        95204 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        706180 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6900 kB
Slab:            26736 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:44:18 (client local time) WITH STATUS 0 IN 1200.43 SECONDS
stats: 19732 7 1200.43 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 2327175  7928649 |  698152       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/524613          
c   -- var.elim.:  2000/524613          
c   -- var.elim.:  3000/524613          
c   -- var.elim.:  4000/524613          
c   -- var.elim.:  5000/524613          
c   -- var.elim.:  6000/524613          
c   -- var.elim.:  7000/524613          
c   -- var.elim.:  8000/524613          
c   -- var.elim.:  9000/524613          
c   -- var.elim.:  10000/524613          
c   -- var.elim.:  11000/524613          
c   -- var.elim.:  12000/524613          
c   -- var.elim.:  13000/524613          
c   -- var.elim.:  14000/524613          
c   -- var.elim.:  15000/524613          
c   -- var.elim.:  16000/524613          
c   -- var.elim.:  17000/524613          
c   -- var.elim.:  18000/524613          
c   -- var.elim.:  1900#### 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.72 0.90 0.89 2/54 9231
Raw data (stat): 9231 (runsolver) R 9230 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540732510 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99984 s]
Raw data (loadavg): 0.76 0.90 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 9473 0 0 0 971 27 0 0 25 0 1 0 540732510 38584320 8195 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9420 8195 603 41 0 9379 0
vsize: 37680
[startup+19.9999 s]
Raw data (loadavg): 0.80 0.90 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 10502 0 0 0 1968 31 0 0 25 0 1 0 540732510 41271296 9224 4294967295 134512640 134672761 3221224544 3221220880 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10076 9224 603 41 0 10035 0
vsize: 40304
[startup+30.0004 s]
Raw data (loadavg): 0.83 0.91 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 46392 0 0 0 2877 122 0 0 25 0 1 0 540732510 218423296 45114 4294967295 134512640 134672761 3221224544 3221217656 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53326 45115 603 41 0 53285 0
vsize: 213304
[startup+40.0001 s]
Raw data (loadavg): 0.85 0.91 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 90367 0 0 0 3772 227 0 0 25 0 1 0 540732510 449097728 89089 4294967295 134512640 134672761 3221224544 3221223088 134621202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109643 89089 603 41 0 109602 0
vsize: 438572
[startup+50.0009 s]
Raw data (loadavg): 0.87 0.91 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 90367 0 0 0 4772 227 0 0 25 0 1 0 540732510 449097728 89089 4294967295 134512640 134672761 3221224544 3221223088 134621396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109643 89089 603 41 0 109602 0
vsize: 438572
[startup+60.0008 s]
Raw data (loadavg): 0.89 0.91 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 95046 0 0 0 5759 241 0 0 25 0 1 0 540732510 457023488 90499 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111578 90499 603 41 0 111537 0
vsize: 446312
[startup+70.0005 s]
Raw data (loadavg): 0.91 0.92 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 96488 0 0 0 6750 249 0 0 25 0 1 0 540732510 463364096 91941 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113126 91941 603 41 0 113085 0
vsize: 452504
[startup+80.0014 s]
Raw data (loadavg): 0.92 0.92 0.89 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 97454 0 0 0 7745 255 0 0 25 0 1 0 540732510 467857408 92907 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114223 92907 603 41 0 114182 0
vsize: 456892
[startup+90.0012 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 98082 0 0 0 8741 259 0 0 25 0 1 0 540732510 470659072 93535 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114907 93535 603 41 0 114866 0
vsize: 459628
[startup+100.002 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 98596 0 0 0 9736 263 0 0 25 0 1 0 540732510 472842240 94049 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115440 94049 603 41 0 115399 0
vsize: 461760
[startup+110.003 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 99295 0 0 0 10732 267 0 0 25 0 1 0 540732510 476004352 94748 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116212 94748 603 41 0 116171 0
vsize: 464848
[startup+120.003 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 99633 0 0 0 11729 270 0 0 25 0 1 0 540732510 477351936 95086 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116541 95086 603 41 0 116500 0
vsize: 466164
[startup+130.002 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 100158 0 0 0 12727 272 0 0 25 0 1 0 540732510 479809536 95611 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117141 95611 603 41 0 117100 0
vsize: 468564
[startup+140.002 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 100706 0 0 0 13723 276 0 0 25 0 1 0 540732510 482394112 96159 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117772 96159 603 41 0 117731 0
vsize: 471088
[startup+150.003 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 101499 0 0 0 14719 280 0 0 25 0 1 0 540732510 485879808 96952 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118623 96952 603 41 0 118582 0
vsize: 474492
[startup+160.003 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 102017 0 0 0 15716 284 0 0 25 0 1 0 540732510 488226816 97470 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119196 97470 603 41 0 119155 0
vsize: 476784
[startup+170.003 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 102539 0 0 0 16713 287 0 0 25 0 1 0 540732510 490799104 97992 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 119824 97992 603 41 0 119783 0
vsize: 479296
[startup+180.003 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 103035 0 0 0 17709 290 0 0 25 0 1 0 540732510 492924928 98488 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120343 98488 603 41 0 120302 0
vsize: 481372
[startup+190.003 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 103439 0 0 0 18705 292 0 0 25 0 1 0 540732510 494993408 98892 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120848 98892 603 41 0 120807 0
vsize: 483392
[startup+200.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 104022 0 0 0 19701 296 0 0 25 0 1 0 540732510 497852416 99475 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121546 99475 603 41 0 121505 0
vsize: 486184
[startup+210.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 104283 0 0 0 20699 299 0 0 25 0 1 0 540732510 499175424 99736 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121869 99736 603 41 0 121828 0
vsize: 487476
[startup+220.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 104675 0 0 0 21697 301 0 0 25 0 1 0 540732510 501071872 100128 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 122332 100128 603 41 0 122291 0
vsize: 489328
[startup+230.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 105041 0 0 0 22696 303 0 0 25 0 1 0 540732510 502755328 100494 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 122743 100494 603 41 0 122702 0
vsize: 490972
[startup+240.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 105345 0 0 0 23695 304 0 0 25 0 1 0 540732510 504033280 100798 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123055 100798 603 41 0 123014 0
vsize: 492220
[startup+250.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 105762 0 0 0 24691 306 0 0 25 0 1 0 540732510 506003456 101215 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123536 101215 603 41 0 123495 0
vsize: 494144
[startup+260.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 105949 0 0 0 25691 307 0 0 25 0 1 0 540732510 506675200 101402 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123700 101402 603 41 0 123659 0
vsize: 494800
[startup+270.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 106256 0 0 0 26688 309 0 0 25 0 1 0 540732510 508203008 101709 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124073 101709 603 41 0 124032 0
vsize: 496292
[startup+280.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 106587 0 0 0 27686 311 0 0 25 0 1 0 540732510 509829120 102040 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124470 102040 603 41 0 124429 0
vsize: 497880
[startup+290.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 106903 0 0 0 28684 313 0 0 25 0 1 0 540732510 511442944 102356 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124864 102356 603 41 0 124823 0
vsize: 499456
[startup+300.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 107234 0 0 0 29683 314 0 0 25 0 1 0 540732510 513048576 102687 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125256 102687 603 41 0 125215 0
vsize: 501024
[startup+310.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 107406 0 0 0 30681 316 0 0 25 0 1 0 540732510 513708032 102859 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125417 102859 603 41 0 125376 0
vsize: 501668
[startup+320.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 107712 0 0 0 31679 318 0 0 25 0 1 0 540732510 515338240 103165 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125815 103165 603 41 0 125774 0
vsize: 503260
[startup+330.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 107970 0 0 0 32678 320 0 0 25 0 1 0 540732510 516485120 103423 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126095 103423 603 41 0 126054 0
vsize: 504380
[startup+340.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 108182 0 0 0 33676 321 0 0 25 0 1 0 540732510 517328896 103635 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126301 103635 603 41 0 126260 0
vsize: 505204
[startup+350.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 108409 0 0 0 34675 323 0 0 25 0 1 0 540732510 518492160 103862 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126585 103862 603 41 0 126544 0
vsize: 506340
[startup+360.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 108695 0 0 0 35672 325 0 0 25 0 1 0 540732510 519966720 104148 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126945 104148 603 41 0 126904 0
vsize: 507780
[startup+370.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 108887 0 0 0 36671 326 0 0 25 0 1 0 540732510 520798208 104340 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127148 104340 603 41 0 127107 0
vsize: 508592
[startup+380.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 110298 0 0 0 37663 334 0 0 25 0 1 0 540732510 526876672 105751 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128632 105751 603 41 0 128591 0
vsize: 514528
[startup+390.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 111192 0 0 0 38659 339 0 0 25 0 1 0 540732510 530976768 106645 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129633 106645 603 41 0 129592 0
vsize: 518532
[startup+400.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 111917 0 0 0 39655 343 0 0 25 0 1 0 540732510 534163456 107370 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130411 107370 603 41 0 130370 0
vsize: 521644
[startup+410.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 112552 0 0 0 40652 346 0 0 25 0 1 0 540732510 536965120 108005 4294967295 134512640 134672761 3221224544 3221222896 134604066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131095 108005 603 41 0 131054 0
vsize: 524380
[startup+420.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 112941 0 0 0 41648 350 0 0 25 0 1 0 540732510 538603520 108394 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131495 108394 603 41 0 131454 0
vsize: 525980
[startup+430.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 113439 0 0 0 42644 354 0 0 25 0 1 0 540732510 540762112 108892 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132022 108892 603 41 0 131981 0
vsize: 528088
[startup+440.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 113878 0 0 0 43642 356 0 0 25 0 1 0 540732510 542924800 109331 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132550 109331 603 41 0 132509 0
vsize: 530200
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 114410 0 0 0 44638 360 0 0 25 0 1 0 540732510 545525760 109863 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133185 109863 603 41 0 133144 0
vsize: 532740
[startup+460.009 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 114738 0 0 0 45635 362 0 0 25 0 1 0 540732510 547229696 110191 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133601 110191 603 41 0 133560 0
vsize: 534404
[startup+470.009 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 115247 0 0 0 46633 364 0 0 25 0 1 0 540732510 549195776 110700 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134081 110700 603 41 0 134040 0
vsize: 536324
[startup+480.009 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 115549 0 0 0 47632 365 0 0 25 0 1 0 540732510 550649856 111002 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134436 111002 603 41 0 134395 0
vsize: 537744
[startup+490.009 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 115897 0 0 0 48630 367 0 0 25 0 1 0 540732510 552521728 111350 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134893 111350 603 41 0 134852 0
vsize: 539572
[startup+500.01 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 116423 0 0 0 49628 370 0 0 25 0 1 0 540732510 555229184 111876 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135554 111876 603 41 0 135513 0
vsize: 542216
[startup+510.01 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 116772 0 0 0 50625 372 0 0 25 0 1 0 540732510 556847104 112225 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135949 112225 603 41 0 135908 0
vsize: 543796
[startup+520.01 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 117409 0 0 0 51623 375 0 0 25 0 1 0 540732510 559685632 112862 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136642 112862 603 41 0 136601 0
vsize: 546568
[startup+530.011 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 117913 0 0 0 52620 378 0 0 25 0 1 0 540732510 561856512 113366 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137172 113366 603 41 0 137131 0
vsize: 548688
[startup+540.014 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 118329 0 0 0 53619 380 0 0 25 0 1 0 540732510 563937280 113782 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137680 113782 603 41 0 137639 0
vsize: 550720
[startup+550.014 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 118933 0 0 0 54613 383 0 0 25 0 1 0 540732510 566681600 114386 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138350 114386 603 41 0 138309 0
vsize: 553400
[startup+560.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 119188 0 0 0 55612 385 0 0 25 0 1 0 540732510 567873536 114641 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138641 114641 603 41 0 138600 0
vsize: 554564
[startup+570.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 119660 0 0 0 56609 388 0 0 25 0 1 0 540732510 569708544 115113 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139089 115113 603 41 0 139048 0
vsize: 556356
[startup+580.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 120124 0 0 0 57608 389 0 0 25 0 1 0 540732510 572010496 115577 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139651 115577 603 41 0 139610 0
vsize: 558604
[startup+590.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 120368 0 0 0 58606 391 0 0 25 0 1 0 540732510 573091840 115821 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139915 115821 603 41 0 139874 0
vsize: 559660
[startup+600.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 120894 0 0 0 59604 394 0 0 25 0 1 0 540732510 575856640 116347 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140590 116347 603 41 0 140549 0
vsize: 562360
[startup+610.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 121112 0 0 0 60602 396 0 0 25 0 1 0 540732510 576811008 116565 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140823 116565 603 41 0 140782 0
vsize: 563292
[startup+620.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 121503 0 0 0 61601 398 0 0 25 0 1 0 540732510 578678784 116956 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141279 116956 603 41 0 141238 0
vsize: 565116
[startup+630.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 121822 0 0 0 62599 400 0 0 25 0 1 0 540732510 579944448 117275 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141588 117275 603 41 0 141547 0
vsize: 566352
[startup+640.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 122033 0 0 0 63598 401 0 0 25 0 1 0 540732510 580915200 117486 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141825 117486 603 41 0 141784 0
vsize: 567300
[startup+650.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 122468 0 0 0 64596 404 0 0 25 0 1 0 540732510 582889472 117921 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142307 117921 603 41 0 142266 0
vsize: 569228
[startup+660.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 122695 0 0 0 65595 405 0 0 25 0 1 0 540732510 583958528 118148 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142568 118148 603 41 0 142527 0
vsize: 570272
[startup+670.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 123064 0 0 0 66592 408 0 0 25 0 1 0 540732510 585732096 118517 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143001 118517 603 41 0 142960 0
vsize: 572004
[startup+680.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 123355 0 0 0 67590 410 0 0 25 0 1 0 540732510 587354112 118808 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143397 118808 603 41 0 143356 0
vsize: 573588
[startup+690.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 123567 0 0 0 68589 411 0 0 25 0 1 0 540732510 588185600 119020 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143600 119020 603 41 0 143559 0
vsize: 574400
[startup+700.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 123846 0 0 0 69588 412 0 0 25 0 1 0 540732510 589553664 119299 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143934 119299 603 41 0 143893 0
vsize: 575736
[startup+710.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 124164 0 0 0 70586 414 0 0 25 0 1 0 540732510 591101952 119617 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144312 119617 603 41 0 144271 0
vsize: 577248
[startup+720.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 124347 0 0 0 71585 416 0 0 25 0 1 0 540732510 592072704 119800 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144549 119800 603 41 0 144508 0
vsize: 578196
[startup+730.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 124588 0 0 0 72584 417 0 0 25 0 1 0 540732510 593141760 120041 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144810 120041 603 41 0 144769 0
vsize: 579240
[startup+740.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 124862 0 0 0 73582 419 0 0 25 0 1 0 540732510 594448384 120315 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145129 120315 603 41 0 145088 0
vsize: 580516
[startup+750.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 125309 0 0 0 74579 422 0 0 25 0 1 0 540732510 596434944 120762 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145614 120762 603 41 0 145573 0
vsize: 582456
[startup+760.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 126724 0 0 0 75571 430 0 0 25 0 1 0 540732510 602660864 122177 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147134 122177 603 41 0 147093 0
vsize: 588536
[startup+770.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 127510 0 0 0 76565 437 0 0 25 0 1 0 540732510 606412800 122963 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148050 122963 603 41 0 148009 0
vsize: 592200
[startup+780.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 128181 0 0 0 77562 440 0 0 25 0 1 0 540732510 609529856 123634 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148811 123634 603 41 0 148770 0
vsize: 595244
[startup+790.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 128875 0 0 0 78559 443 0 0 25 0 1 0 540732510 612532224 124328 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149544 124328 603 41 0 149503 0
vsize: 598176
[startup+800.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 129385 0 0 0 79555 448 0 0 25 0 1 0 540732510 614850560 124838 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150110 124838 603 41 0 150069 0
vsize: 600440
[startup+810.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 130475 0 0 0 80549 454 0 0 25 0 1 0 540732510 619343872 125928 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151207 125928 603 41 0 151166 0
vsize: 604828
[startup+820.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 131416 0 0 0 81544 458 0 0 25 0 1 0 540732510 623570944 126869 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152239 126869 603 41 0 152198 0
vsize: 608956
[startup+830.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 132116 0 0 0 82541 462 0 0 25 0 1 0 540732510 626532352 127569 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152962 127569 603 41 0 152921 0
vsize: 611848
[startup+840.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 132898 0 0 0 83537 466 0 0 25 0 1 0 540732510 630140928 128351 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153843 128351 603 41 0 153802 0
vsize: 615372
[startup+850.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 133315 0 0 0 84535 468 0 0 25 0 1 0 540732510 632242176 128768 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154356 128768 603 41 0 154315 0
vsize: 617424
[startup+860.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 133785 0 0 0 85531 472 0 0 25 0 1 0 540732510 634556416 129238 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154921 129238 603 41 0 154880 0
vsize: 619684
[startup+870.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 134234 0 0 0 86529 474 0 0 25 0 1 0 540732510 636485632 129687 4294967295 134512640 134672761 3221224544 3221222896 134604052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155392 129687 603 41 0 155351 0
vsize: 621568
[startup+880.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 134572 0 0 0 87527 476 0 0 25 0 1 0 540732510 637874176 130025 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155731 130025 603 41 0 155690 0
vsize: 622924
[startup+890.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 134885 0 0 0 88524 479 0 0 25 0 1 0 540732510 639078400 130338 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156025 130338 603 41 0 155984 0
vsize: 624100
[startup+900.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 135339 0 0 0 89522 481 0 0 25 0 1 0 540732510 641597440 130792 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156640 130792 603 41 0 156599 0
vsize: 626560
[startup+910.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 135585 0 0 0 90520 483 0 0 25 0 1 0 540732510 642875392 131038 4294967295 134512640 134672761 3221224544 3221222896 134605453 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156952 131038 603 41 0 156911 0
vsize: 627808
[startup+920.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 135895 0 0 0 91519 485 0 0 25 0 1 0 540732510 644280320 131348 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157295 131348 603 41 0 157254 0
vsize: 629180
[startup+930.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 136816 0 0 0 92514 490 0 0 25 0 1 0 540732510 648323072 132269 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158282 132269 603 41 0 158241 0
vsize: 633128
[startup+940.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 137835 0 0 0 93507 497 0 0 25 0 1 0 540732510 652840960 133288 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159385 133288 603 41 0 159344 0
vsize: 637540
[startup+950.032 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 138635 0 0 0 94503 501 0 0 25 0 1 0 540732510 656441344 134088 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160264 134088 603 41 0 160223 0
vsize: 641056
[startup+960.033 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 139261 0 0 0 95500 505 0 0 25 0 1 0 540732510 659288064 134714 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160959 134714 603 41 0 160918 0
vsize: 643836
[startup+970.033 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 139914 0 0 0 96496 508 0 0 25 0 1 0 540732510 662200320 135367 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161670 135367 603 41 0 161629 0
vsize: 646680
[startup+980.032 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 140360 0 0 0 97494 511 0 0 25 0 1 0 540732510 664092672 135813 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162132 135813 603 41 0 162091 0
vsize: 648528
[startup+990.032 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 140759 0 0 0 98492 513 0 0 25 0 1 0 540732510 665767936 136212 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162541 136212 603 41 0 162500 0
vsize: 650164
[startup+1000.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 141315 0 0 0 99489 516 0 0 25 0 1 0 540732510 668708864 136768 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 163259 136768 603 41 0 163218 0
vsize: 653036
[startup+1010.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 141719 0 0 0 100487 519 0 0 25 0 1 0 540732510 670412800 137172 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 163675 137172 603 41 0 163634 0
vsize: 654700
[startup+1020.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 142052 0 0 0 101485 520 0 0 25 0 1 0 540732510 672083968 137505 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 164083 137505 603 41 0 164042 0
vsize: 656332
[startup+1030.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 142559 0 0 0 102482 523 0 0 25 0 1 0 540732510 674390016 138012 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 164646 138012 603 41 0 164605 0
vsize: 658584
[startup+1040.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 142843 0 0 0 103481 524 0 0 25 0 1 0 540732510 675852288 138296 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165003 138296 603 41 0 164962 0
vsize: 660012
[startup+1050.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 143298 0 0 0 104479 526 0 0 25 0 1 0 540732510 677986304 138751 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165524 138751 603 41 0 165483 0
vsize: 662096
[startup+1060.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 143779 0 0 0 105477 529 0 0 25 0 1 0 540732510 680357888 139232 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166103 139232 603 41 0 166062 0
vsize: 664412
[startup+1070.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 143955 0 0 0 106475 530 0 0 25 0 1 0 540732510 681029632 139408 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166267 139408 603 41 0 166226 0
vsize: 665068
[startup+1080.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 144253 0 0 0 107474 532 0 0 25 0 1 0 540732510 682455040 139706 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166615 139706 603 41 0 166574 0
vsize: 666460
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 144697 0 0 0 108472 534 0 0 25 0 1 0 540732510 684519424 140150 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167119 140150 603 41 0 167078 0
vsize: 668476
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 145126 0 0 0 109469 536 0 0 25 0 1 0 540732510 686637056 140579 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167636 140579 603 41 0 167595 0
vsize: 670544
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 145310 0 0 0 110468 537 0 0 25 0 1 0 540732510 687423488 140763 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167828 140763 603 41 0 167787 0
vsize: 671312
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 145632 0 0 0 111466 538 0 0 25 0 1 0 540732510 688812032 141085 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168167 141085 603 41 0 168126 0
vsize: 672668
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 146010 0 0 0 112465 540 0 0 25 0 1 0 540732510 690409472 141463 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168557 141463 603 41 0 168516 0
vsize: 674228
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 146233 0 0 0 113464 542 0 0 25 0 1 0 540732510 691294208 141686 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168773 141686 603 41 0 168732 0
vsize: 675092
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 146393 0 0 0 114461 545 0 0 25 0 1 0 540732510 692015104 141846 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168949 141846 603 41 0 168908 0
vsize: 675796
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 146740 0 0 0 115459 547 0 0 25 0 1 0 540732510 693571584 142193 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169329 142193 603 41 0 169288 0
vsize: 677316
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 147158 0 0 0 116457 549 0 0 25 0 1 0 540732510 695537664 142611 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169809 142611 603 41 0 169768 0
vsize: 679236
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 147515 0 0 0 117456 551 0 0 25 0 1 0 540732510 697360384 142968 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170254 142968 603 41 0 170213 0
vsize: 681016
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 147639 0 0 0 118455 552 0 0 25 0 1 0 540732510 697982976 143092 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170406 143092 603 41 0 170365 0
vsize: 681624
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9231
Raw data (stat): 9231 (minisat+) R 9230 11931 11930 0 -1 0 147919 0 0 0 119453 554 0 0 25 0 1 0 540732510 699203584 143372 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170704 143372 603 41 0 170663 0
vsize: 682816
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.4 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 9231
Raw data (stat): 9231 (minisat+) Z 9230 11931 11930 0 -1 12 147919 0 0 0 119453 590 0 0 25 0 1 0 540732510 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.4
CPU time (s): 1200.43
CPU user time (s): 1194.53
CPU system time (s): 5.9001
CPU usage (%): 100.003
Max. virtual memory (Kb): 682816
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####