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 14058

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        746348 kB
Buffers:         33560 kB
Cached:         230192 kB
SwapCached:       2060 kB
Active:         100832 kB
Inactive:       167720 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        746096 kB
SwapTotal:     2097136 kB
SwapFree:      2094988 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14092 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:09:23 (client local time) WITH STATUS 0 IN 1200.41 SECONDS
stats: 19734 7 1200.41 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 | 3023302  9827827 | 1007767       0        0     nan |  0.000 % |
c |       103 | 3023282  9827767 | 1108543      94     2279    24.2 |  1.956 % |
c |       255 | 3023282  9827767 | 1219398     246     5103    20.7 |  1.956 % |
c |       480 | 3023235  9827618 | 1341337     465     9083    19.5 |  1.957 % |
c |       818 | 3023104  9827225 | 1475471     775    14506    18.7 |  1.960 % |
c |      1324 | 3023076  9827141 | 1623018    1271    30056    23.6 |  1.961 % |
c |      2083 | 3022989  9826880 | 1785320    1983    75289    38.0 |  1.964 % |
c |      3224 | 3022979  9826850 | 1963852    3118   110622    35.5 |  1.965 % |
c |      4932 | 3022576  9825541 | 2160238    3566    89260    25.0 |  1.977 % |
c |      7495 | 3022376  9824887 | 2376261    6065   218296    36.0 |  1.983 % |
c |     11339 | 3021424  9821676 | 2613888    9576   673648    70.3 |  2.013 % |
c |     17105 | 3020720  9819396 | 2875276   15073  1169707    77.6 |  2.037 % |
c |     25755 | 3018663  9812649 | 3162804   22944  1526637    66.5 |  2.097 % |
c |     38732 | 3016902  9806862 | 3479085   35152  2163025    61.5 |  2.156 % |
c |     58194 | 3013450  9795439 | 3826993   51517  2940294    57.1 |  2.266 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.92 2/54 25219
Raw data (stat): 25219 (runsolver) R 25218 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481941024 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+10.0007 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 9272 0 0 0 973 26 0 0 25 0 1 0 481941024 37273600 7994 4294967295 134512640 134672761 3221224544 3221176268 1075755419 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9142 8001 603 41 0 9101 0
vsize: 36400
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 10310 0 0 0 1970 29 0 0 25 0 1 0 481941024 39960576 9032 4294967295 134512640 134672761 3221224544 3221221264 134522444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9756 9032 603 41 0 9715 0
vsize: 39024
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 39293 0 0 0 2900 98 0 0 25 0 1 0 481941024 176517120 38000 4294967295 134512640 134672761 3221224544 3221219848 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43095 38002 603 41 0 43054 0
vsize: 172380
[startup+40.0004 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 57134 0 0 0 3854 144 0 0 25 0 1 0 481941024 275058688 55841 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67153 55841 603 41 0 67112 0
vsize: 268612
[startup+50.0009 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 57428 0 0 0 4853 146 0 0 25 0 1 0 481941024 276000768 56135 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67383 56135 603 41 0 67342 0
vsize: 269532
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 57710 0 0 0 5852 147 0 0 25 0 1 0 481941024 277082112 56417 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67647 56417 603 41 0 67606 0
vsize: 270588
[startup+70.0005 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58175 0 0 0 6850 149 0 0 25 0 1 0 481941024 278568960 56882 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68010 56882 603 41 0 67969 0
vsize: 272040
[startup+80.0014 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58274 0 0 0 7850 149 0 0 25 0 1 0 481941024 278970368 56981 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68108 56981 603 41 0 68067 0
vsize: 272432
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58288 0 0 0 8850 149 0 0 25 0 1 0 481941024 279105536 56995 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68141 56995 603 41 0 68100 0
vsize: 272564
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58288 0 0 0 9850 150 0 0 25 0 1 0 481941024 279105536 56995 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68141 56995 603 41 0 68100 0
vsize: 272564
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58288 0 0 0 10850 150 0 0 25 0 1 0 481941024 279105536 56995 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68141 56995 603 41 0 68100 0
vsize: 272564
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58288 0 0 0 11849 150 0 0 25 0 1 0 481941024 279105536 56995 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68141 56995 603 41 0 68100 0
vsize: 272564
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58360 0 0 0 12849 151 0 0 25 0 1 0 481941024 279396352 57067 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68212 57067 603 41 0 68171 0
vsize: 272848
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58475 0 0 0 13849 151 0 0 25 0 1 0 481941024 279666688 57182 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68278 57182 603 41 0 68237 0
vsize: 273112
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58510 0 0 0 14848 152 0 0 25 0 1 0 481941024 279797760 57217 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68310 57217 603 41 0 68269 0
vsize: 273240
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58519 0 0 0 15848 152 0 0 25 0 1 0 481941024 279932928 57226 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68343 57226 603 41 0 68302 0
vsize: 273372
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58566 0 0 0 16847 153 0 0 25 0 1 0 481941024 280068096 57273 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68376 57273 603 41 0 68335 0
vsize: 273504
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58596 0 0 0 17847 153 0 0 25 0 1 0 481941024 280203264 57303 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68409 57303 603 41 0 68368 0
vsize: 273636
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 58599 0 0 0 18847 154 0 0 25 0 1 0 481941024 280203264 57306 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68409 57306 603 41 0 68368 0
vsize: 273636
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59095 0 0 0 19845 156 0 0 25 0 1 0 481941024 282226688 57802 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68903 57802 603 41 0 68862 0
vsize: 275612
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59395 0 0 0 20845 156 0 0 25 0 1 0 481941024 283443200 58102 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69200 58102 603 41 0 69159 0
vsize: 276800
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59547 0 0 0 21844 157 0 0 25 0 1 0 481941024 283992064 58254 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69334 58254 603 41 0 69293 0
vsize: 277336
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59547 0 0 0 22844 157 0 0 25 0 1 0 481941024 283992064 58254 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69334 58254 603 41 0 69293 0
vsize: 277336
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59564 0 0 0 23844 157 0 0 25 0 1 0 481941024 284127232 58271 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69367 58271 603 41 0 69326 0
vsize: 277468
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59593 0 0 0 24844 158 0 0 25 0 1 0 481941024 284262400 58300 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69400 58300 603 41 0 69359 0
vsize: 277600
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59615 0 0 0 25844 158 0 0 25 0 1 0 481941024 284262400 58322 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69400 58322 603 41 0 69359 0
vsize: 277600
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59646 0 0 0 26844 158 0 0 25 0 1 0 481941024 284397568 58353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69433 58353 603 41 0 69392 0
vsize: 277732
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59667 0 0 0 27844 159 0 0 25 0 1 0 481941024 284532736 58374 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69466 58374 603 41 0 69425 0
vsize: 277864
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59669 0 0 0 28844 159 0 0 25 0 1 0 481941024 284532736 58376 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69466 58376 603 41 0 69425 0
vsize: 277864
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59703 0 0 0 29843 159 0 0 25 0 1 0 481941024 284663808 58410 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69498 58410 603 41 0 69457 0
vsize: 277992
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59778 0 0 0 30843 160 0 0 25 0 1 0 481941024 285114368 58485 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69608 58485 603 41 0 69567 0
vsize: 278432
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59851 0 0 0 31843 160 0 0 25 0 1 0 481941024 285380608 58558 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69673 58558 603 41 0 69632 0
vsize: 278692
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59854 0 0 0 32842 161 0 0 25 0 1 0 481941024 285380608 58561 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69673 58561 603 41 0 69632 0
vsize: 278692
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 59962 0 0 0 33842 162 0 0 25 0 1 0 481941024 285786112 58669 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69772 58669 603 41 0 69731 0
vsize: 279088
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60017 0 0 0 34841 162 0 0 25 0 1 0 481941024 286056448 58724 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 58724 603 41 0 69797 0
vsize: 279352
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60021 0 0 0 35841 162 0 0 25 0 1 0 481941024 286056448 58728 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 58728 603 41 0 69797 0
vsize: 279352
[startup+370.109 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60033 0 0 0 36851 163 0 0 25 0 1 0 481941024 286056448 58740 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 58740 603 41 0 69797 0
vsize: 279352
[startup+380.109 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60035 0 0 0 37851 163 0 0 25 0 1 0 481941024 286056448 58742 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 58742 603 41 0 69797 0
vsize: 279352
[startup+390.116 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60040 0 0 0 38852 163 0 0 25 0 1 0 481941024 286056448 58747 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 58747 603 41 0 69797 0
vsize: 279352
[startup+400.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60055 0 0 0 39852 163 0 0 25 0 1 0 481941024 286191616 58762 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 58762 603 41 0 69830 0
vsize: 279484
[startup+410.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60064 0 0 0 40852 163 0 0 25 0 1 0 481941024 286191616 58771 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 58771 603 41 0 69830 0
vsize: 279484
[startup+420.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60072 0 0 0 41852 163 0 0 25 0 1 0 481941024 286191616 58779 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 58779 603 41 0 69830 0
vsize: 279484
[startup+430.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60094 0 0 0 42852 163 0 0 25 0 1 0 481941024 286322688 58801 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69903 58801 603 41 0 69862 0
vsize: 279612
[startup+440.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60104 0 0 0 43852 163 0 0 25 0 1 0 481941024 286322688 58811 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69903 58811 603 41 0 69862 0
vsize: 279612
[startup+450.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60114 0 0 0 44853 163 0 0 25 0 1 0 481941024 286457856 58821 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69936 58821 603 41 0 69895 0
vsize: 279744
[startup+460.118 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60117 0 0 0 45853 163 0 0 25 0 1 0 481941024 286457856 58824 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69936 58824 603 41 0 69895 0
vsize: 279744
[startup+470.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60123 0 0 0 46853 163 0 0 25 0 1 0 481941024 286457856 58830 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69936 58830 603 41 0 69895 0
vsize: 279744
[startup+480.119 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60159 0 0 0 47853 164 0 0 25 0 1 0 481941024 286593024 58866 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69969 58866 603 41 0 69928 0
vsize: 279876
[startup+490.118 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60170 0 0 0 48852 164 0 0 25 0 1 0 481941024 286593024 58877 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69969 58877 603 41 0 69928 0
vsize: 279876
[startup+500.119 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60194 0 0 0 49850 165 0 0 25 0 1 0 481941024 286728192 58901 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70002 58901 603 41 0 69961 0
vsize: 280008
[startup+510.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60197 0 0 0 50850 165 0 0 25 0 1 0 481941024 286728192 58904 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70002 58904 603 41 0 69961 0
vsize: 280008
[startup+520.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60245 0 0 0 51850 165 0 0 25 0 1 0 481941024 286863360 58952 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70035 58952 603 41 0 69994 0
vsize: 280140
[startup+530.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60268 0 0 0 52850 165 0 0 25 0 1 0 481941024 286998528 58975 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70068 58975 603 41 0 70027 0
vsize: 280272
[startup+540.128 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60271 0 0 0 53851 165 0 0 25 0 1 0 481941024 286998528 58978 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70068 58978 603 41 0 70027 0
vsize: 280272
[startup+550.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60272 0 0 0 54850 166 0 0 25 0 1 0 481941024 286998528 58979 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70068 58979 603 41 0 70027 0
vsize: 280272
[startup+560.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60296 0 0 0 55850 167 0 0 25 0 1 0 481941024 287133696 59003 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70101 59003 603 41 0 70060 0
vsize: 280404
[startup+570.136 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60347 0 0 0 56850 167 0 0 25 0 1 0 481941024 287404032 59054 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70167 59054 603 41 0 70126 0
vsize: 280668
[startup+580.143 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60370 0 0 0 57850 168 0 0 25 0 1 0 481941024 287404032 59077 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70167 59077 603 41 0 70126 0
vsize: 280668
[startup+590.143 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60375 0 0 0 58850 168 0 0 25 0 1 0 481941024 287404032 59082 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70167 59082 603 41 0 70126 0
vsize: 280668
[startup+600.144 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60398 0 0 0 59850 168 0 0 25 0 1 0 481941024 287539200 59105 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70200 59105 603 41 0 70159 0
vsize: 280800
[startup+610.144 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60500 0 0 0 60849 169 0 0 25 0 1 0 481941024 287940608 59207 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70298 59207 603 41 0 70257 0
vsize: 281192
[startup+620.144 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60515 0 0 0 61849 169 0 0 25 0 1 0 481941024 288075776 59222 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70331 59222 603 41 0 70290 0
vsize: 281324
[startup+630.144 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60515 0 0 0 62849 170 0 0 25 0 1 0 481941024 288075776 59222 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70331 59222 603 41 0 70290 0
vsize: 281324
[startup+640.144 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25219
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60528 0 0 0 63849 170 0 0 25 0 1 0 481941024 288075776 59235 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70331 59235 603 41 0 70290 0
vsize: 281324
[startup+650.144 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 25272
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60595 0 0 0 64843 175 0 0 25 0 1 0 481941024 288342016 59302 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70396 59302 603 41 0 70355 0
vsize: 281584
[startup+660.145 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 25272
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60622 0 0 0 65843 175 0 0 25 0 1 0 481941024 288477184 59329 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70429 59329 603 41 0 70388 0
vsize: 281716
[startup+670.145 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 25272
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60858 0 0 0 66843 175 0 0 25 0 1 0 481941024 289550336 59565 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70691 59565 603 41 0 70650 0
vsize: 282764
[startup+680.145 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 25272
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60960 0 0 0 67843 176 0 0 25 0 1 0 481941024 289955840 59667 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70790 59667 603 41 0 70749 0
vsize: 283160
[startup+690.145 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 25272
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 60992 0 0 0 68843 176 0 0 25 0 1 0 481941024 290086912 59699 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70822 59699 603 41 0 70781 0
vsize: 283288
[startup+700.147 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 25272
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61014 0 0 0 69843 176 0 0 25 0 1 0 481941024 290222080 59721 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70855 59721 603 41 0 70814 0
vsize: 283420
[startup+710.147 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 25272
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61052 0 0 0 70843 176 0 0 25 0 1 0 481941024 290357248 59759 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70888 59759 603 41 0 70847 0
vsize: 283552
[startup+720.147 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61074 0 0 0 71843 176 0 0 25 0 1 0 481941024 290357248 59781 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70888 59781 603 41 0 70847 0
vsize: 283552
[startup+730.148 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61114 0 0 0 72843 176 0 0 25 0 1 0 481941024 290627584 59821 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70954 59821 603 41 0 70913 0
vsize: 283816
[startup+740.147 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61137 0 0 0 73843 176 0 0 25 0 1 0 481941024 290627584 59844 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70954 59844 603 41 0 70913 0
vsize: 283816
[startup+750.149 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61164 0 0 0 74843 176 0 0 25 0 1 0 481941024 290762752 59871 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70987 59871 603 41 0 70946 0
vsize: 283948
[startup+760.149 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61198 0 0 0 75843 177 0 0 25 0 1 0 481941024 290897920 59905 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71020 59905 603 41 0 70979 0
vsize: 284080
[startup+770.149 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61276 0 0 0 76843 177 0 0 25 0 1 0 481941024 291164160 59983 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71085 59983 603 41 0 71044 0
vsize: 284340
[startup+780.149 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61296 0 0 0 77843 177 0 0 25 0 1 0 481941024 291299328 60003 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71118 60003 603 41 0 71077 0
vsize: 284472
[startup+790.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61297 0 0 0 78844 177 0 0 25 0 1 0 481941024 291299328 60004 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71118 60004 603 41 0 71077 0
vsize: 284472
[startup+800.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61316 0 0 0 79844 177 0 0 25 0 1 0 481941024 291434496 60023 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71151 60023 603 41 0 71110 0
vsize: 284604
[startup+810.151 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61346 0 0 0 80844 177 0 0 25 0 1 0 481941024 291569664 60053 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71184 60053 603 41 0 71143 0
vsize: 284736
[startup+820.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61394 0 0 0 81844 177 0 0 25 0 1 0 481941024 291700736 60101 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71216 60101 603 41 0 71175 0
vsize: 284864
[startup+830.151 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61394 0 0 0 82844 177 0 0 25 0 1 0 481941024 291700736 60101 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71216 60101 603 41 0 71175 0
vsize: 284864
[startup+840.151 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61394 0 0 0 83844 177 0 0 25 0 1 0 481941024 291700736 60101 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71216 60101 603 41 0 71175 0
vsize: 284864
[startup+850.152 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61404 0 0 0 84845 177 0 0 25 0 1 0 481941024 291700736 60111 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71216 60111 603 41 0 71175 0
vsize: 284864
[startup+860.152 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61406 0 0 0 85845 177 0 0 25 0 1 0 481941024 291700736 60113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71216 60113 603 41 0 71175 0
vsize: 284864
[startup+870.153 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61435 0 0 0 86845 177 0 0 25 0 1 0 481941024 291835904 60142 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71249 60142 603 41 0 71208 0
vsize: 284996
[startup+880.153 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61451 0 0 0 87845 177 0 0 25 0 1 0 481941024 291971072 60158 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71282 60158 603 41 0 71241 0
vsize: 285128
[startup+890.153 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61555 0 0 0 88845 177 0 0 25 0 1 0 481941024 292380672 60262 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71382 60262 603 41 0 71341 0
vsize: 285528
[startup+900.154 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61608 0 0 0 89845 177 0 0 25 0 1 0 481941024 292515840 60315 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71415 60315 603 41 0 71374 0
vsize: 285660
[startup+910.153 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61650 0 0 0 90845 178 0 0 25 0 1 0 481941024 292782080 60357 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71480 60357 603 41 0 71439 0
vsize: 285920
[startup+920.153 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61796 0 0 0 91845 178 0 0 25 0 1 0 481941024 293310464 60503 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71609 60503 603 41 0 71568 0
vsize: 286436
[startup+930.154 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61804 0 0 0 92845 178 0 0 25 0 1 0 481941024 293310464 60511 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71609 60511 603 41 0 71568 0
vsize: 286436
[startup+940.154 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61890 0 0 0 93845 178 0 0 25 0 1 0 481941024 293576704 60597 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71674 60597 603 41 0 71633 0
vsize: 286696
[startup+950.155 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61923 0 0 0 94845 179 0 0 25 0 1 0 481941024 293711872 60630 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71707 60630 603 41 0 71666 0
vsize: 286828
[startup+960.155 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61954 0 0 0 95845 179 0 0 25 0 1 0 481941024 293842944 60661 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71739 60661 603 41 0 71698 0
vsize: 286956
[startup+970.155 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 61995 0 0 0 96845 179 0 0 25 0 1 0 481941024 293978112 60702 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71772 60702 603 41 0 71731 0
vsize: 287088
[startup+980.155 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62011 0 0 0 97845 179 0 0 25 0 1 0 481941024 294113280 60718 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71805 60718 603 41 0 71764 0
vsize: 287220
[startup+990.155 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62022 0 0 0 98845 179 0 0 25 0 1 0 481941024 294113280 60729 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71805 60729 603 41 0 71764 0
vsize: 287220
[startup+1000.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25274
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62029 0 0 0 99846 179 0 0 25 0 1 0 481941024 294113280 60736 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71805 60736 603 41 0 71764 0
vsize: 287220
[startup+1010.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62053 0 0 0 100846 179 0 0 25 0 1 0 481941024 294248448 60760 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71838 60760 603 41 0 71797 0
vsize: 287352
[startup+1020.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62082 0 0 0 101846 179 0 0 25 0 1 0 481941024 294383616 60789 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71871 60789 603 41 0 71830 0
vsize: 287484
[startup+1030.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62084 0 0 0 102846 179 0 0 25 0 1 0 481941024 294383616 60791 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71871 60791 603 41 0 71830 0
vsize: 287484
[startup+1040.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62249 0 0 0 103845 180 0 0 25 0 1 0 481941024 295059456 60956 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72036 60956 603 41 0 71995 0
vsize: 288144
[startup+1050.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62325 0 0 0 104845 180 0 0 25 0 1 0 481941024 295194624 61032 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72069 61032 603 41 0 72028 0
vsize: 288276
[startup+1060.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62326 0 0 0 105845 180 0 0 25 0 1 0 481941024 295194624 61033 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72069 61033 603 41 0 72028 0
vsize: 288276
[startup+1070.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62328 0 0 0 106846 180 0 0 25 0 1 0 481941024 295329792 61035 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72102 61035 603 41 0 72061 0
vsize: 288408
[startup+1080.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62328 0 0 0 107846 180 0 0 25 0 1 0 481941024 295329792 61035 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72102 61035 603 41 0 72061 0
vsize: 288408
[startup+1090.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62461 0 0 0 108846 180 0 0 25 0 1 0 481941024 295735296 61168 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72201 61168 603 41 0 72160 0
vsize: 288804
[startup+1100.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62462 0 0 0 109846 180 0 0 25 0 1 0 481941024 295735296 61169 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72201 61169 603 41 0 72160 0
vsize: 288804
[startup+1110.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62534 0 0 0 110846 180 0 0 25 0 1 0 481941024 296005632 61241 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72267 61241 603 41 0 72226 0
vsize: 289068
[startup+1120.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62537 0 0 0 111846 180 0 0 25 0 1 0 481941024 296005632 61244 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72267 61244 603 41 0 72226 0
vsize: 289068
[startup+1130.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62542 0 0 0 112846 180 0 0 25 0 1 0 481941024 296005632 61249 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72267 61249 603 41 0 72226 0
vsize: 289068
[startup+1140.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62543 0 0 0 113846 180 0 0 25 0 1 0 481941024 296005632 61250 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72267 61250 603 41 0 72226 0
vsize: 289068
[startup+1150.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62549 0 0 0 114847 180 0 0 25 0 1 0 481941024 296005632 61256 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72267 61256 603 41 0 72226 0
vsize: 289068
[startup+1160.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62550 0 0 0 115847 180 0 0 25 0 1 0 481941024 296005632 61257 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72267 61257 603 41 0 72226 0
vsize: 289068
[startup+1170.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62553 0 0 0 116847 180 0 0 25 0 1 0 481941024 296140800 61260 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72300 61260 603 41 0 72259 0
vsize: 289200
[startup+1180.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62557 0 0 0 117847 180 0 0 25 0 1 0 481941024 296140800 61264 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72300 61264 603 41 0 72259 0
vsize: 289200
[startup+1190.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62567 0 0 0 118847 180 0 0 25 0 1 0 481941024 296140800 61274 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72300 61274 603 41 0 72259 0
vsize: 289200
[startup+1200.16 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25276
Raw data (stat): 25219 (minisat+) R 25218 29151 29150 0 -1 0 62571 0 0 0 119848 180 0 0 25 0 1 0 481941024 296140800 61278 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72300 61278 603 41 0 72259 0
vsize: 289200
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.29 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 25276
Raw data (stat): 25219 (minisat+) Z 25218 29151 29150 0 -1 12 62573 0 0 0 119848 192 0 0 25 0 1 0 481941024 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.29
CPU time (s): 1200.41
CPU user time (s): 1198.48
CPU system time (s): 1.92971
CPU usage (%): 100.01
Max. virtual memory (Kb): 289200
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####