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 31306

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        505460 kB
Buffers:         38188 kB
Cached:         469052 kB
SwapCached:        584 kB
Active:          25292 kB
Inactive:       484028 kB
HighTotal:      131008 kB
HighFree:        20440 kB
LowTotal:       903652 kB
LowFree:        485020 kB
SwapTotal:     2097136 kB
SwapFree:      2095648 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14044 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:20:30 (client local time) WITH STATUS 152 IN 1229.95 SECONDS
stats: 22702 7 1229.95 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1259 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................
c ---[1258]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1257]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1256]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1255]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1254]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1253]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1252]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1251]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1250]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1249]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1248]---> BDD-cost:  173
c ---[1247]---> BDD-cost:  353
c ---[1246]---> BDD-cost:  533
c ---[1245]---> BDD-cost:  678
c ---[1244]---> BDD-cost:  893
c ---[1243]---> BDD-cost:  984
c ---[1242]---> BDD-cost: 1182
c ---[1241]---> Adder-cost: 899   maxlim: 5   bits: 4/3
c ---[1240]---> Adder-cost: 879   maxlim: 5   bits: 4/3
c ---[1239]---> Adder-cost: 937   maxlim: 5   bits: 4/3
c ---[1238]---> BDD-cost: 2467
c ---[1237]---> BDD-cost: 2502
c ---[1236]---> BDD-cost: 2722
c ---[1235]---> BDD-cost: 2778
c ---[1234]---> BDD-cost: 2922
c ---[1233]---> Adder-cost: 1354   maxlim: 5   bits: 4/3
c ---[1232]---> Adder-cost: 1267   maxlim: 5   bits: 4/3
c ---[1231]---> Adder-cost: 1200   maxlim: 5   bits: 4/3
c ---[1230]---> Adder-cost: 1201   maxlim: 5   bits: 4/3
c ---[1229]---> BDD-cost: 2262
c ---[1228]---> BDD-cost: 2213
c ---[1227]---> BDD-cost: 2115
c ---[1226]---> BDD-cost: 2063
c ---[1225]---> BDD-cost: 1917
c ---[1224]---> BDD-cost: 1853
c ---[1223]---> BDD-cost: 1680
c ---[1222]---> BDD-cost: 1572
c ---[1221]---> BDD-cost: 1395
c ---[1220]---> BDD-cost: 1242
c ---[1219]---> BDD-cost: 1044
c ---[1218]---> BDD-cost:  891
c ---[1217]---> BDD-cost:  699
c ---[1216]---> BDD-cost:  533
c ---[1215]---> BDD-cost:  233
c ---[1214]---> BDD-cost:  117
c ---[1213]---> BDD-cost:  173
c ---[1212]---> BDD-cost:  353
c ---[1211]---> BDD-cost:  533
c ---[1210]---> BDD-cost:  663
c ---[1209]---> BDD-cost:  893
c ---[1208]---> BDD-cost: 1005
c ---[1207]---> BDD-cost: 1253
c ---[1206]---> BDD-cost: 1854
c ---[1205]---> BDD-cost: 1994
c ---[1204]---> BDD-cost: 2242
c ---[1203]---> BDD-cost: 2426
c ---[1202]---> BDD-cost: 2494
c ---[1201]---> BDD-cost: 2730
c ---[1200]---> BDD-cost: 2064
c ---[1199]---> BDD-cost: 2208
c ---[1198]---> Adder-cost: 1424   maxlim: 5   bits: 4/3
c ---[1197]---> Adder-cost: 1267   maxlim: 5   bits: 4/3
c ---[1196]---> Adder-cost: 1230   maxlim: 5   bits: 4/3
c ---[1195]---> Adder-cost: 1161   maxlim: 5   bits: 4/3
c ---[1194]---> BDD-cost: 2273
c ---[1193]---> BDD-cost: 2202
c ---[1192]---> BDD-cost: 2103
c ---[1191]---> BDD-cost: 2052
c ---[1190]---> BDD-cost: 1920
c ---[1189]---> BDD-cost: 1842
c ---[1188]---> BDD-cost: 1722
c ---[1187]---> BDD-cost: 1578
c ---[1186]---> BDD-cost: 1407
c ---[1185]---> BDD-cost: 1248
c ---[1184]---> BDD-cost: 1053
c ---[1183]---> BDD-cost:  893
c ---[1182]---> BDD-cost:  705
c ---[1181]---> BDD-cost:  533
c ---[1180]---> BDD-cost:  237
c ---[1179]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  173
c ---[1177]---> BDD-cost:  353
c ---[1176]---> BDD-cost:  533
c ---[1175]---> BDD-cost:  713
c ---[1174]---> BDD-cost:  879
c ---[1173]---> BDD-cost: 1073
c ---[1172]---> BDD-cost: 1149
c ---[1171]---> BDD-cost: 1821
c ---[1170]---> BDD-cost: 1515
c ---[1169]---> BDD-cost: 1647
c ---[1168]---> BDD-cost: 1821
c ---[1167]---> BDD-cost: 1973
c ---[1166]---> Adder-cost: 1291   maxlim: 5   bits: 4/3
c ---[1165]---> Adder-cost: 1201   maxlim: 5   bits: 4/3
c ---[1164]---> Adder-cost: 1163   maxlim: 5   bits: 4/3
c ---[1163]---> Adder-cost: 1208   maxlim: 5   bits: 4/3
c ---[1162]---> Adder-cost: 1153   maxlim: 5   bits: 4/3
c ---[1161]---> Adder-cost: 1148   maxlim: 5   bits: 4/3
c ---[1160]---> Adder-cost: 1157   maxlim: 5   bits: 4/3
c ---[1159]---> Adder-cost: 1136   maxlim: 5   bits: 4/3
c ---[1158]---> Adder-cost: 1095   maxlim: 4   bits: 4/3
c ---[1157]---> BDD-cost: 2153
c ---[1156]---> BDD-cost: 2019
c ---[1155]---> BDD-cost: 1973
c ---[1154]---> BDD-cost: 1800
c ---[1153]---> BDD-cost: 1731
c ---[1152]---> BDD-cost: 1557
c ---[1151]---> BDD-cost: 1428
c ---[1150]---> BDD-cost: 1221
c ---[1149]---> BDD-cost: 1068
c ---[1148]---> BDD-cost:  876
c ---[1147]---> BDD-cost:  713
c ---[1146]---> BDD-cost:  522
c ---[1145]---> BDD-cost:  237
c ---[1144]---> BDD-cost:  115
c ---[1143]---> BDD-cost:  173
c ---[1142]---> BDD-cost:  353
c ---[1141]---> BDD-cost:  492
c ---[1140]---> BDD-cost:  690
c ---[1139]---> BDD-cost:  834
c ---[1138]---> BDD-cost: 1050
c ---[1137]---> BDD-cost: 1230
c ---[1136]---> BDD-cost: 1902
c ---[1135]---> BDD-cost: 2078
c ---[1134]---> BDD-cost: 2166
c ---[1133]---> BDD-cost: 2438
c ---[1132]---> BDD-cost: 2558
c ---[1131]---> BDD-cost: 2718
c ---[1130]---> BDD-cost: 2061
c ---[1129]---> BDD-cost: 2190
c ---[1128]---> BDD-cost: 2273
c ---[1127]---> BDD-cost: 2250
c ---[1126]---> BDD-cost: 2333
c ---[1125]---> BDD-cost: 2256
c ---[1124]---> BDD-cost: 2273
c ---[1123]---> BDD-cost: 2208
c ---[1122]---> BDD-cost: 2153
c ---[1121]---> BDD-cost: 2043
c ---[1120]---> BDD-cost: 1973
c ---[1119]---> BDD-cost: 1836
c ---[1118]---> BDD-cost: 1733
c ---[1117]---> BDD-cost: 1583
c ---[1116]---> BDD-cost: 1386
c ---[1115]---> BDD-cost: 1245
c ---[1114]---> BDD-cost: 1038
c ---[1113]---> BDD-cost:  893
c ---[1112]---> BDD-cost:  699
c ---[1111]---> BDD-cost:  533
c ---[1110]---> BDD-cost:  233
c ---[1109]---> BDD-cost:  117
c ---[1108]---> BDD-cost:  173
c ---[1107]---> BDD-cost:  353
c ---[1106]---> BDD-cost:  533
c ---[1105]---> BDD-cost:  663
c ---[1104]---> BDD-cost:  893
c ---[1103]---> BDD-cost: 1005
c ---[1102]---> BDD-cost: 1185
c ---[1101]---> BDD-cost: 1857
c ---[1100]---> BDD-cost: 2107
c ---[1099]---> BDD-cost: 2242
c ---[1098]---> BDD-cost: 2467
c ---[1097]---> BDD-cost: 2518
c ---[1096]---> BDD-cost: 2698
c ---[1095]---> BDD-cost: 2076
c ---[1094]---> BDD-cost: 2175
c ---[1093]---> Adder-cost: 1424   maxlim: 5   bits: 4/3
c ---[1092]---> Adder-cost: 1299   maxlim: 5   bits: 4/3
c ---[1091]---> Adder-cost: 1204   maxlim: 5   bits: 4/3
c ---[1090]---> Adder-cost: 1165   maxlim: 5   bits: 4/3
c ---[1089]---> BDD-cost: 2262
c ---[1088]---> BDD-cost: 2213
c ---[1087]---> BDD-cost: 2133
c ---[1086]---> BDD-cost: 2063
c ---[1085]---> BDD-cost: 1941
c ---[1084]---> BDD-cost: 1848
c ---[1083]---> BDD-cost: 1728
c ---[1082]---> BDD-cost: 1572
c ---[1081]---> BDD-cost: 1407
c ---[1080]---> BDD-cost: 1242
c ---[1079]---> BDD-cost: 1053
c ---[1078]---> BDD-cost:  893
c ---[1077]---> BDD-cost:  705
c ---[1076]---> BDD-cost:  533
c ---[1075]---> BDD-cost:  237
c ---[1074]---> BDD-cost:  117
c ---[1024]---> Adder-cost: 156   maxlim: 1055615   bits: 22/21
c ---[1022]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[1020]---> Adder-cost: 334   maxlim: 1070975   bits: 22/21
c ---[1018]---> Adder-cost: 398   maxlim: 1078655   bits: 22/21
c ---[1016]---> Adder-cost: 462   maxlim: 1086335   bits: 22/21
c ---[1014]---> Adder-cost: 510   maxlim: 1093887   bits: 22/21
c ---[1012]---> Adder-cost: 548   maxlim: 1101567   bits: 22/21
c ---[1010]---> Adder-cost: 616   maxlim: 1109247   bits: 22/21
c ---[1008]---> Adder-cost: 758   maxlim: 1115647   bits: 22/21
c ---[1006]---> Adder-cost: 818   maxlim: 1122047   bits: 22/21
c ---[1004]---> Adder-cost: 874   maxlim: 1127423   bits: 22/21
c ---[1002]---> Adder-cost: 964   maxlim: 1132543   bits: 22/21
c ---[1000]---> Adder-cost: 1024   maxlim: 1136383   bits: 22/21
c ---[ 998]---> Adder-cost: 1096   maxlim: 1140223   bits: 22/21
c ---[ 996]---> Adder-cost: 1070   maxlim: 1142783   bits: 22/21
c ---[ 994]---> Adder-cost: 1140   maxlim: 1145087   bits: 22/21
c ---[ 992]---> Adder-cost: 1110   maxlim: 1146367   bits: 22/21
c ---[ 990]---> Adder-cost: 1136   maxlim: 1147647   bits: 22/21
c ---[ 988]---> Adder-cost: 1212   maxlim: 1146367   bits: 22/21
c ---[ 986]---> Adder-cost: 1128   maxlim: 1145471   bits: 22/21
c ---[ 984]---> Adder-cost: 1208   maxlim: 1142911   bits: 22/21
c ---[ 982]---> Adder-cost: 1196   maxlim: 1140351   bits: 22/21
c ---[ 980]---> Adder-cost: 1144   maxlim: 1136511   bits: 22/21
c ---[ 978]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 976]---> Adder-cost: 1060   maxlim: 1127295   bits: 22/21
c ---[ 974]---> Adder-cost: 976   maxlim: 1122175   bits: 22/21
c ---[ 972]---> Adder-cost: 952   maxlim: 1116031   bits: 22/21
c ---[ 970]---> Adder-cost: 848   maxlim: 1109631   bits: 22/21
c ---[ 968]---> Adder-cost: 756   maxlim: 1101951   bits: 22/21
c ---[ 966]---> Adder-cost: 636   maxlim: 1094271   bits: 22/21
c ---[ 964]---> Adder-cost: 570   maxlim: 1086591   bits: 22/21
c ---[ 962]---> Adder-cost: 486   maxlim: 1078527   bits: 22/21
c ---[ 960]---> Adder-cost: 380   maxlim: 1070847   bits: 22/21
c ---[ 958]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 956]---> Adder-cost: 168   maxlim: 1055999   bits: 22/21
c ---[ 954]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 952]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 950]---> Adder-cost: 348   maxlim: 1070975   bits: 22/21
c ---[ 948]---> Adder-cost: 416   maxlim: 1078655   bits: 22/21
c ---[ 946]---> Adder-cost: 488   maxlim: 1086335   bits: 22/21
c ---[ 944]---> Adder-cost: 544   maxlim: 1094143   bits: 22/21
c ---[ 942]---> Adder-cost: 594   maxlim: 1101823   bits: 22/21
c ---[ 940]---> Adder-cost: 648   maxlim: 1109503   bits: 22/21
c ---[ 938]---> Adder-cost: 928   maxlim: 1115903   bits: 22/21
c ---[ 936]---> Adder-cost: 1026   maxlim: 1122303   bits: 22/21
c ---[ 934]---> Adder-cost: 942   maxlim: 1127423   bits: 22/21
c ---[ 932]---> Adder-cost: 984   maxlim: 1132543   bits: 22/21
c ---[ 930]---> Adder-cost: 1080   maxlim: 1136383   bits: 22/21
c ---[ 928]---> Adder-cost: 1104   maxlim: 1140351   bits: 22/21
c ---[ 926]---> Adder-cost: 1096   maxlim: 1142911   bits: 22/21
c ---[ 924]---> Adder-cost: 1100   maxlim: 1145087   bits: 22/21
c ---[ 922]---> Adder-cost: 1150   maxlim: 1146367   bits: 22/21
c ---[ 920]---> Adder-cost: 1174   maxlim: 1147647   bits: 22/21
c ---[ 918]---> Adder-cost: 1164   maxlim: 1146367   bits: 22/21
c ---[ 916]---> Adder-cost: 1184   maxlim: 1145471   bits: 22/21
c ---[ 914]---> Adder-cost: 1186   maxlim: 1142911   bits: 22/21
c ---[ 912]---> Adder-cost: 1202   maxlim: 1140351   bits: 22/21
c ---[ 910]---> Adder-cost: 1160   maxlim: 1136511   bits: 22/21
c ---[ 908]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 906]---> Adder-cost: 1054   maxlim: 1127295   bits: 22/21
c ---[ 904]---> Adder-cost: 982   maxlim: 1122175   bits: 22/21
c ---[ 902]---> Adder-cost: 940   maxlim: 1116031   bits: 22/21
c ---[ 900]---> Adder-cost: 848   maxlim: 1109631   bits: 22/21
c ---[ 898]---> Adder-cost: 758   maxlim: 1101951   bits: 22/21
c ---[ 896]---> Adder-cost: 638   maxlim: 1094271   bits: 22/21
c ---[ 894]---> Adder-cost: 586   maxlim: 1086591   bits: 22/21
c ---[ 892]---> Adder-cost: 506   maxlim: 1078527   bits: 22/21
c ---[ 890]---> Adder-cost: 374   maxlim: 1070847   bits: 22/21
c ---[ 888]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 886]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 884]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 882]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 880]---> Adder-cost: 348   maxlim: 1070975   bits: 22/21
c ---[ 878]---> Adder-cost: 406   maxlim: 1078655   bits: 22/21
c ---[ 876]---> Adder-cost: 478   maxlim: 1086335   bits: 22/21
c ---[ 874]---> Adder-cost: 550   maxlim: 1094015   bits: 22/21
c ---[ 872]---> Adder-cost: 566   maxlim: 1101823   bits: 22/21
c ---[ 870]---> Adder-cost: 646   maxlim: 1109503   bits: 22/21
c ---[ 868]---> Adder-cost: 868   maxlim: 1116031   bits: 22/21
c ---[ 866]---> Adder-cost: 890   maxlim: 1122431   bits: 22/21
c ---[ 864]---> Adder-cost: 882   maxlim: 1127551   bits: 22/21
c ---[ 862]---> Adder-cost: 944   maxlim: 1132671   bits: 22/21
c ---[ 860]---> Adder-cost: 982   maxlim: 1136127   bits: 22/21
c ---[ 858]---> Adder-cost: 998   maxlim: 1139967   bits: 22/21
c ---[ 856]---> Adder-cost: 1036   maxlim: 1142527   bits: 22/21
c ---[ 854]---> Adder-cost: 1050   maxlim: 1145087   bits: 22/21
c ---[ 852]---> Adder-cost: 1086   maxlim: 1146367   bits: 22/21
c ---[ 850]---> Adder-cost: 1106   maxlim: 1147647   bits: 22/21
c ---[ 848]---> Adder-cost: 1126   maxlim: 1146367   bits: 22/21
c ---[ 846]---> Adder-cost: 1116   maxlim: 1145087   bits: 22/21
c ---[ 844]---> Adder-cost: 1140   maxlim: 1142655   bits: 22/21
c ---[ 842]---> Adder-cost: 1106   maxlim: 1140095   bits: 22/21
c ---[ 840]---> Adder-cost: 1120   maxlim: 1136255   bits: 22/21
c ---[ 838]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 836]---> Adder-cost: 1052   maxlim: 1127295   bits: 22/21
c ---[ 834]---> Adder-cost: 1012   maxlim: 1122175   bits: 22/21
c ---[ 832]---> Adder-cost: 920   maxlim: 1116031   bits: 22/21
c ---[ 830]---> Adder-cost: 846   maxlim: 1109631   bits: 22/21
c ---[ 828]---> Adder-cost: 762   maxlim: 1101951   bits: 22/21
c ---[ 826]---> Adder-cost: 690   maxlim: 1094271   bits: 22/21
c ---[ 824]---> Adder-cost: 586   maxlim: 1086591   bits: 22/21
c ---[ 822]---> Adder-cost: 476   maxlim: 1078527   bits: 22/21
c ---[ 820]---> Adder-cost: 388   maxlim: 1070847   bits: 22/21
c ---[ 818]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 816]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 814]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 812]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 810]---> Adder-cost: 350   maxlim: 1070975   bits: 22/21
c ---[ 808]---> Adder-cost: 422   maxlim: 1078655   bits: 22/21
c ---[ 806]---> Adder-cost: 486   maxlim: 1086335   bits: 22/21
c ---[ 804]---> Adder-cost: 570   maxlim: 1094143   bits: 22/21
c ---[ 802]---> Adder-cost: 624   maxlim: 1101823   bits: 22/21
c ---[ 800]---> Adder-cost: 658   maxlim: 1109503   bits: 22/21
c ---[ 798]---> Adder-cost: 1000   maxlim: 1115903   bits: 22/21
c ---[ 796]---> Adder-cost: 966   maxlim: 1122303   bits: 22/21
c ---[ 794]---> Adder-cost: 1084   maxlim: 1127423   bits: 22/21
c ---[ 792]---> Adder-cost: 1088   maxlim: 1132543   bits: 22/21
c ---[ 790]---> Adder-cost: 1150   maxlim: 1136383   bits: 22/21
c ---[ 788]---> Adder-cost: 1158   maxlim: 1140351   bits: 22/21
c ---[ 786]---> Adder-cost: 1236   maxlim: 1142911   bits: 22/21
c ---[ 784]---> Adder-cost: 1334   maxlim: 1145471   bits: 22/21
c ---[ 782]---> Adder-cost: 1220   maxlim: 1146751   bits: 22/21
c ---[ 780]---> Adder-cost: 1358   maxlim: 1148031   bits: 22/21
c ---[ 778]---> Adder-cost: 1294   maxlim: 1146751   bits: 22/21
c ---[ 776]---> Adder-cost: 1270   maxlim: 1145471   bits: 22/21
c ---[ 774]---> Adder-cost: 1242   maxlim: 1142911   bits: 22/21
c ---[ 772]---> Adder-cost: 1226   maxlim: 1140351   bits: 22/21
c ---[ 770]---> Adder-cost: 1148   maxlim: 1136511   bits: 22/21
c ---[ 768]---> Adder-cost: 1122   maxlim: 1132415   bits: 22/21
c ---[ 766]---> Adder-cost: 1064   maxlim: 1127295   bits: 22/21
c ---[ 764]---> Adder-cost: 1038   maxlim: 1122175   bits: 22/21
c ---[ 762]---> Adder-cost: 932   maxlim: 1116031   bits: 22/21
c ---[ 760]---> Adder-cost: 858   maxlim: 1109631   bits: 22/21
c ---[ 758]---> Adder-cost: 754   maxlim: 1101951   bits: 22/21
c ---[ 756]---> Adder-cost: 642   maxlim: 1094271   bits: 22/21
c ---[ 754]---> Adder-cost: 560   maxlim: 1086591   bits: 22/21
c ---[ 752]---> Adder-cost: 494   maxlim: 1078527   bits: 22/21
c ---[ 750]---> Adder-cost: 378   maxlim: 1070847   bits: 22/21
c ---[ 748]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 746]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 744]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 742]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 740]---> Adder-cost: 352   maxlim: 1070975   bits: 22/21
c ---[ 738]---> Adder-cost: 416   maxlim: 1078655   bits: 22/21
c ---[ 736]---> Adder-cost: 490   maxlim: 1086335   bits: 22/21
c ---[ 734]---> Adder-cost: 550   maxlim: 1094015   bits: 22/21
c ---[ 732]---> Adder-cost: 628   maxlim: 1101695   bits: 22/21
c ---[ 730]---> Adder-cost: 658   maxlim: 1109503   bits: 22/21
c ---[ 728]---> Adder-cost: 942   maxlim: 1115903   bits: 22/21
c ---[ 726]---> Adder-cost: 968   maxlim: 1122303   bits: 22/21
c ---[ 724]---> Adder-cost: 948   maxlim: 1127423   bits: 22/21
c ---[ 722]---> Adder-cost: 1004   maxlim: 1132543   bits: 22/21
c ---[ 720]---> Adder-cost: 1086   maxlim: 1136383   bits: 22/21
c ---[ 718]---> Adder-cost: 1088   maxlim: 1140351   bits: 22/21
c ---[ 716]---> Adder-cost: 1110   maxlim: 1142911   bits: 22/21
c ---[ 714]---> Adder-cost: 1072   maxlim: 1145087   bits: 22/21
c ---[ 712]---> Adder-cost: 1192   maxlim: 1146367   bits: 22/21
c ---[ 710]---> Adder-cost: 1182   maxlim: 1147647   bits: 22/21
c ---[ 708]---> Adder-cost: 1200   maxlim: 1146367   bits: 22/21
c ---[ 706]---> Adder-cost: 1182   maxlim: 1145471   bits: 22/21
c ---[ 704]---> Adder-cost: 1194   maxlim: 1142911   bits: 22/21
c ---[ 702]---> Adder-cost: 1212   maxlim: 1140351   bits: 22/21
c ---[ 700]---> Adder-cost: 1120   maxlim: 1136511   bits: 22/21
c ---[ 698]---> Adder-cost: 1120   maxlim: 1132415   bits: 22/21
c ---[ 696]---> Adder-cost: 1082   maxlim: 1127295   bits: 22/21
c ---[ 694]---> Adder-cost: 984   maxlim: 1122175   bits: 22/21
c ---[ 692]---> Adder-cost: 960   maxlim: 1116031   bits: 22/21
c ---[ 690]---> Adder-cost: 834   maxlim: 1109631   bits: 22/21
c ---[ 688]---> Adder-cost: 774   maxlim: 1101951   bits: 22/21
c ---[ 686]---> Adder-cost: 658   maxlim: 1094271   bits: 22/21
c ---[ 684]---> Adder-cost: 566   maxlim: 1086591   bits: 22/21
c ---[ 682]---> Adder-cost: 486   maxlim: 1078527   bits: 22/21
c ---[ 680]---> Adder-cost: 386   maxlim: 1070847   bits: 22/21
c ---[ 678]---> Adder-cost: 290   maxlim: 1063679   bits: 22/21
c ---[ 676]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 674]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 672]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 670]---> Adder-cost: 416   maxlim: 1071359   bits: 22/21
c ---[ 668]---> Adder-cost: 404   maxlim: 1079039   bits: 22/21
c ---[ 666]---> Adder-cost: 456   maxlim: 1086719   bits: 22/21
c ---[ 664]---> Adder-cost: 542   maxlim: 1094399   bits: 22/21
c ---[ 662]---> Adder-cost: 598   maxlim: 1102079   bits: 22/21
c ---[ 660]---> Adder-cost: 826   maxlim: 1108479   bits: 22/21
c ---[ 658]---> Adder-cost: 794   maxlim: 1113599   bits: 22/21
c ---[ 656]---> Adder-cost: 916   maxlim: 1117439   bits: 22/21
c ---[ 654]---> Adder-cost: 914   maxlim: 1119999   bits: 22/21
c ---[ 652]---> Adder-cost: 968   maxlim: 1121279   bits: 22/21
c ---[ 650]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 648]---> Adder-cost: 884   maxlim: 1119999   bits: 22/21
c ---[ 646]---> Adder-cost: 878   maxlim: 1117439   bits: 22/21
c ---[ 644]---> Adder-cost: 876   maxlim: 1113599   bits: 22/21
c ---[ 642]---> Adder-cost: 834   maxlim: 1108479   bits: 22/21
c ---[ 640]---> Adder-cost: 752   maxlim: 1102079   bits: 22/21
c ---[ 638]---> Adder-cost: 656   maxlim: 1094399   bits: 22/21
c ---[ 636]---> Adder-cost: 574   maxlim: 1086719   bits: 22/21
c ---[ 634]---> Adder-cost: 496   maxlim: 1079039   bits: 22/21
c ---[ 632]---> Adder-cost: 394   maxlim: 1071359   bits: 22/21
c ---[ 630]---> Adder-cost: 286   maxlim: 1063679   bits: 22/21
c ---[ 628]---> Adder-cost: 168   maxlim: 1055999   bits: 22/21
c ---[ 626]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 624]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 622]---> Adder-cost: 348   maxlim: 1071359   bits: 22/21
c ---[ 620]---> Adder-cost: 424   maxlim: 1079039   bits: 22/21
c ---[ 618]---> Adder-cost: 490   maxlim: 1086719   bits: 22/21
c ---[ 616]---> Adder-cost: 544   maxlim: 1094399   bits: 22/21
c ---[ 614]---> Adder-cost: 620   maxlim: 1102079   bits: 22/21
c ---[ 612]---> Adder-cost: 930   maxlim: 1108479   bits: 22/21
c ---[ 610]---> Adder-cost: 908   maxlim: 1113599   bits: 22/21
c ---[ 608]---> Adder-cost: 924   maxlim: 1117439   bits: 22/21
c ---[ 606]---> Adder-cost: 894   maxlim: 1119999   bits: 22/21
c ---[ 604]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 602]---> Adder-cost: 952   maxlim: 1121151   bits: 22/21
c ---[ 600]---> Adder-cost: 886   maxlim: 1119871   bits: 22/21
c ---[ 598]---> Adder-cost: 894   maxlim: 1117311   bits: 22/21
c ---[ 596]---> Adder-cost: 860   maxlim: 1113471   bits: 22/21
c ---[ 594]---> Adder-cost: 812   maxlim: 1108351   bits: 22/21
c ---[ 592]---> Adder-cost: 766   maxlim: 1101951   bits: 22/21
c ---[ 590]---> Adder-cost: 658   maxlim: 1094271   bits: 22/21
c ---[ 588]---> Adder-cost: 580   maxlim: 1086591   bits: 22/21
c ---[ 586]---> Adder-cost: 488   maxlim: 1078911   bits: 22/21
c ---[ 584]---> Adder-cost: 368   maxlim: 1071231   bits: 22/21
c ---[ 582]---> Adder-cost: 282   maxlim: 1063551   bits: 22/21
c ---[ 580]---> Adder-cost: 170   maxlim: 1055871   bits: 22/21
c ---[ 579]---> BDD-cost:   21
c ---[ 578]---> BDD-cost:   33
c ---[ 577]---> BDD-cost:   45
c ---[ 576]---> BDD-cost:   57
c ---[ 575]---> BDD-cost:   69
c ---[ 574]---> BDD-cost:   81
c ---[ 573]---> BDD-cost:   93
c ---[ 572]---> BDD-cost:   95
c ---[ 571]---> BDD-cost:  117
c ---[ 570]---> BDD-cost:   21
c ---[ 569]---> BDD-cost:   33
c ---[ 568]---> BDD-cost:   45
c ---[ 567]---> BDD-cost:   57
c ---[ 566]---> BDD-cost:   69
c ---[ 565]---> BDD-cost:   81
c ---[ 564]---> BDD-cost:   93
c ---[ 563]---> BDD-cost:  105
c ---[ 562]---> BDD-cost:  117
c ---[ 561]---> BDD-cost:   21
c ---[ 560]---> BDD-cost:   33
c ---[ 559]---> BDD-cost:   45
c ---[ 558]---> BDD-cost:   57
c ---[ 557]---> BDD-cost:   69
c ---[ 556]---> BDD-cost:   81
c ---[ 555]---> BDD-cost:   93
c ---[ 554]---> BDD-cost:  105
c ---[ 553]---> BDD-cost:  117
c ---[ 552]---> BDD-cost:    9
c ---[ 551]---> BDD-cost:    9
c ---[ 550]---> BDD-cost:    9
c ---[ 549]---> BDD-cost:    9
c ---[ 548]---> BDD-cost:    9
c ---[ 547]---> BDD-cost:   21
c ---[ 546]---> BDD-cost:   33
c ---[ 545]---> BDD-cost:   45
c ---[ 544]---> BDD-cost:   47
c ---[ 543]---> BDD-cost:   21
c ---[ 542]---> BDD-cost:   33
c ---[ 541]---> BDD-cost:   45
c ---[ 540]---> BDD-cost:   57
c ---[ 539]---> BDD-cost:   69
c ---[ 538]---> BDD-cost:   81
c ---[ 537]---> BDD-cost:   93
c ---[ 536]---> BDD-cost:  105
c ---[ 535]---> BDD-cost:  117
c ---[ 534]---> BDD-cost:    9
c ---[ 533]---> BDD-cost:    9
c ---[ 532]---> BDD-cost:    9
c ---[ 531]---> BDD-cost:   21
c ---[ 530]---> BDD-cost:   33
c ---[ 529]---> BDD-cost:   45
c ---[ 528]---> BDD-cost:   47
c ---[ 527]---> BDD-cost:   61
c ---[ 526]---> BDD-cost:   81
c ---[ 525]---> BDD-cost:   83
c ---[ 524]---> BDD-cost:  105
c ---[ 523]---> BDD-cost:  107
c ---[ 522]---> BDD-cost:   21
c ---[ 521]---> BDD-cost:   33
c ---[ 520]---> BDD-cost:   45
c ---[ 519]---> BDD-cost:   57
c ---[ 518]---> BDD-cost:   69
c ---[ 517]---> BDD-cost:   81
c ---[ 516]---> BDD-cost:   47
c ---[ 515]---> BDD-cost:   59
c ---[ 514]---> BDD-cost:   71
c ---[ 513]---> BDD-cost:   21
c ---[ 512]---> BDD-cost:   33
c ---[ 511]---> BDD-cost:   45
c ---[ 510]---> BDD-cost:   57
c ---[ 509]---> BDD-cost:   69
c ---[ 508]---> BDD-cost:   81
c ---[ 507]---> BDD-cost:   93
c ---[ 506]---> BDD-cost:  105
c ---[ 505]---> BDD-cost:  117
c ---[ 504]---> BDD-cost:    9
c ---[ 503]---> BDD-cost:    9
c ---[ 502]---> BDD-cost:    9
c ---[ 501]---> BDD-cost:    9
c ---[ 500]---> BDD-cost:    9
c ---[ 499]---> BDD-cost:   21
c ---[ 498]---> BDD-cost:   33
c ---[ 497]---> BDD-cost:   45
c ---[ 496]---> BDD-cost:   57
c ---[ 495]---> BDD-cost:   21
c ---[ 494]---> BDD-cost:   33
c ---[ 493]---> BDD-cost:   23
c ---[ 492]---> BDD-cost:   35
c ---[ 491]---> BDD-cost:   69
c ---[ 490]---> BDD-cost:   81
c ---[ 489]---> BDD-cost:   71
c ---[ 488]---> BDD-cost:   83
c ---[ 487]---> BDD-cost:   71
c ---[ 486]---> BDD-cost:    9
c ---[ 485]---> BDD-cost:    9
c ---[ 484]---> BDD-cost:    9
c ---[ 483]---> BDD-cost:   21
c ---[ 482]---> BDD-cost:   33
c ---[ 481]---> BDD-cost:   45
c ---[ 480]---> BDD-cost:   57
c ---[ 479]---> BDD-cost:   69
c ---[ 478]---> BDD-cost:   81
c ---[ 477]---> BDD-cost:   93
c ---[ 476]---> BDD-cost:  105
c ---[ 475]---> BDD-cost:  117
c ---[ 474]---> BDD-cost:   21
c ---[ 473]---> BDD-cost:   33
c ---[ 472]---> BDD-cost:   45
c ---[ 471]---> BDD-cost:   57
c ---[ 470]---> BDD-cost:   69
c ---[ 469]---> BDD-cost:   81
c ---[ 468]---> BDD-cost:   93
c ---[ 467]---> BDD-cost:  105
c ---[ 466]---> BDD-cost:  117
c ---[ 465]---> BDD-cost:   21
c ---[ 464]---> BDD-cost:   33
c ---[ 463]---> BDD-cost:   45
c ---[ 462]---> BDD-cost:   57
c ---[ 461]---> BDD-cost:   69
c ---[ 460]---> BDD-cost:   81
c ---[ 459]---> BDD-cost:   93
c ---[ 458]---> BDD-cost:  105
c ---[ 457]---> BDD-cost:  117
c ---[ 456]---> BDD-cost:    9
c ---[ 455]---> BDD-cost:    9
c ---[ 454]---> BDD-cost:    9
c ---[ 453]---> BDD-cost:    9
c ---[ 452]---> BDD-cost:    9
c ---[ 451]---> BDD-cost:   21
c ---[ 450]---> BDD-cost:   33
c ---[ 449]---> BDD-cost:   45
c ---[ 448]---> BDD-cost:   57
c ---[ 447]---> BDD-cost:   21
c ---[ 446]---> BDD-cost:   33
c ---[ 445]---> BDD-cost:   35
c ---[ 444]---> BDD-cost:   47
c ---[ 443]---> BDD-cost:   59
c ---[ 442]---> BDD-cost:   71
c ---[ 441]---> BDD-cost:   83
c ---[ 440]---> BDD-cost:   95
c ---[ 439]---> BDD-cost:  107
c ---[ 438]---> BDD-cost:    9
c ---[ 437]---> BDD-cost:    9
c ---[ 436]---> BDD-cost:    9
c ---[ 435]---> BDD-cost:   21
c ---[ 434]---> BDD-cost:   33
c ---[ 433]---> BDD-cost:   45
c ---[ 432]---> BDD-cost:   47
c ---[ 431]---> BDD-cost:   69
c ---[ 430]---> BDD-cost:   81
c ---[ 429]---> BDD-cost:   93
c ---[ 428]---> BDD-cost:   95
c ---[ 427]---> BDD-cost:  117
c ---[ 426]---> BDD-cost:   21
c ---[ 425]---> BDD-cost:   33
c ---[ 424]---> BDD-cost:   45
c ---[ 423]---> BDD-cost:   57
c ---[ 422]---> BDD-cost:   69
c ---[ 421]---> BDD-cost:   81
c ---[ 420]---> BDD-cost:   93
c ---[ 419]---> BDD-cost:  101
c ---[ 418]---> BDD-cost:   95
c ---[ 417]---> BDD-cost:   21
c ---[ 416]---> BDD-cost:   33
c ---[ 415]---> BDD-cost:   45
c ---[ 414]---> BDD-cost:   57
c ---[ 413]---> BDD-cost:   69
c ---[ 412]---> BDD-cost:   81
c ---[ 411]---> BDD-cost:   93
c ---[ 410]---> BDD-cost:  105
c ---[ 409]---> BDD-cost:  117
c ---[ 408]---> BDD-cost:    9
c ---[ 407]---> BDD-cost:    9
c ---[ 406]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:   21
c ---[ 402]---> BDD-cost:   33
c ---[ 401]---> BDD-cost:   45
c ---[ 400]---> BDD-cost:   57
c ---[ 399]---> BDD-cost:   21
c ---[ 398]---> BDD-cost:   33
c ---[ 397]---> BDD-cost:   45
c ---[ 396]---> BDD-cost:   57
c ---[ 395]---> BDD-cost:   69
c ---[ 394]---> BDD-cost:   81
c ---[ 393]---> BDD-cost:   71
c ---[ 392]---> BDD-cost:   83
c ---[ 391]---> BDD-cost:   71
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:   21
c ---[ 386]---> BDD-cost:   33
c ---[ 385]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:   57
c ---[ 383]---> BDD-cost:   59
c ---[ 382]---> BDD-cost:   81
c ---[ 381]---> BDD-cost:   83
c ---[ 380]---> BDD-cost:  105
c ---[ 379]---> BDD-cost:  107
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:   33
c ---[ 376]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   57
c ---[ 374]---> BDD-cost:   69
c ---[ 373]---> BDD-cost:   81
c ---[ 372]---> BDD-cost:   93
c ---[ 371]---> BDD-cost:  105
c ---[ 370]---> BDD-cost:  117
c ---[ 369]---> BDD-cost:   21
c ---[ 368]---> BDD-cost:   33
c ---[ 367]---> BDD-cost:   45
c ---[ 366]---> BDD-cost:   57
c ---[ 365]---> BDD-cost:   69
c ---[ 364]---> BDD-cost:   81
c ---[ 363]---> BDD-cost:   93
c ---[ 362]---> BDD-cost:  105
c ---[ 361]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:   21
c ---[ 354]---> BDD-cost:   33
c ---[ 353]---> BDD-cost:   45
c ---[ 352]---> BDD-cost:   57
c ---[ 351]---> BDD-cost:   11
c ---[ 350]---> BDD-cost:   11
c ---[ 349]---> BDD-cost:   23
c ---[ 348]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   47
c ---[ 346]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   71
c ---[ 344]---> BDD-cost:   59
c ---[ 343]---> BDD-cost:   95
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:   21
c ---[ 338]---> BDD-cost:   33
c ---[ 337]---> BDD-cost:   45
c ---[ 336]---> BDD-cost:   47
c ---[ 335]---> BDD-cost:   69
c ---[ 334]---> BDD-cost:   81
c ---[ 333]---> BDD-cost:   93
c ---[ 332]---> BDD-cost:   95
c ---[ 331]---> BDD-cost:  117
c ---[ 330]---> BDD-cost:   21
c ---[ 329]---> BDD-cost:   33
c ---[ 328]---> BDD-cost:   45
c ---[ 327]---> BDD-cost:   57
c ---[ 326]---> BDD-cost:   69
c ---[ 325]---> BDD-cost:   81
c ---[ 324]---> BDD-cost:   93
c ---[ 323]---> BDD-cost:  105
c ---[ 322]---> BDD-cost:   95
c ---[ 321]---> BDD-cost:   21
c ---[ 320]---> BDD-cost:   33
c ---[ 319]---> BDD-cost:   45
c ---[ 318]---> BDD-cost:   57
c ---[ 317]---> BDD-cost:   69
c ---[ 316]---> BDD-cost:   71
c ---[ 315]---> BDD-cost:   83
c ---[ 314]---> BDD-cost:   95
c ---[ 313]---> BDD-cost:   83
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:   21
c ---[ 306]---> BDD-cost:   33
c ---[ 305]---> BDD-cost:   45
c ---[ 304]---> BDD-cost:   57
c ---[ 303]---> BDD-cost:   21
c ---[ 302]---> BDD-cost:   33
c ---[ 301]---> BDD-cost:   45
c ---[ 300]---> BDD-cost:   57
c ---[ 299]---> BDD-cost:   69
c ---[ 298]---> BDD-cost:   81
c ---[ 297]---> BDD-cost:   71
c ---[ 296]---> BDD-cost:   83
c ---[ 295]---> BDD-cost:   71
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:   11
c ---[ 290]---> BDD-cost:   23
c ---[ 289]---> BDD-cost:   45
c ---[ 288]---> BDD-cost:   47
c ---[ 287]---> BDD-cost:   69
c ---[ 286]---> BDD-cost:   71
c ---[ 285]---> BDD-cost:   93
c ---[ 284]---> BDD-cost:   95
c ---[ 283]---> BDD-cost:  117
c ---[ 282]---> BDD-cost:   21
c ---[ 281]---> BDD-cost:   33
c ---[ 280]---> BDD-cost:   45
c ---[ 279]---> BDD-cost:   57
c ---[ 278]---> BDD-cost:   69
c ---[ 277]---> BDD-cost:   81
c ---[ 276]---> BDD-cost:   93
c ---[ 275]---> BDD-cost:  105
c ---[ 274]---> BDD-cost:  117
c ---[ 273]---> BDD-cost:   21
c ---[ 272]---> BDD-cost:   33
c ---[ 271]---> BDD-cost:   45
c ---[ 270]---> BDD-cost:   57
c ---[ 269]---> BDD-cost:   69
c ---[ 268]---> BDD-cost:   81
c ---[ 267]---> BDD-cost:   93
c ---[ 266]---> BDD-cost:  105
c ---[ 265]---> BDD-cost:  117
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:   21
c ---[ 258]---> BDD-cost:   33
c ---[ 257]---> BDD-cost:   45
c ---[ 256]---> BDD-cost:   57
c ---[ 255]---> BDD-cost:   21
c ---[ 254]---> BDD-cost:   33
c ---[ 253]---> BDD-cost:   23
c ---[ 252]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   47
c ---[ 250]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   71
c ---[ 248]---> BDD-cost:   59
c ---[ 247]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   21
c ---[ 242]---> BDD-cost:   33
c ---[ 241]---> BDD-cost:   45
c ---[ 240]---> BDD-cost:   57
c ---[ 239]---> BDD-cost:   69
c ---[ 238]---> BDD-cost:   81
c ---[ 237]---> BDD-cost:   93
c ---[ 236]---> BDD-cost:   95
c ---[ 235]---> BDD-cost:  117
c ---[ 234]---> BDD-cost:   21
c ---[ 233]---> BDD-cost:   33
c ---[ 232]---> BDD-cost:   45
c ---[ 231]---> BDD-cost:   57
c ---[ 230]---> BDD-cost:   69
c ---[ 229]---> BDD-cost:   81
c ---[ 228]---> BDD-cost:   93
c ---[ 227]---> BDD-cost:  105
c ---[ 226]---> BDD-cost:  117
c ---[ 225]---> BDD-cost:   21
c ---[ 224]---> BDD-cost:   33
c ---[ 223]---> BDD-cost:   45
c ---[ 222]---> BDD-cost:   57
c ---[ 221]---> BDD-cost:   69
c ---[ 220]---> BDD-cost:   81
c ---[ 219]---> BDD-cost:   71
c ---[ 218]---> BDD-cost:  105
c ---[ 217]---> BDD-cost:   95
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:   21
c ---[ 210]---> BDD-cost:   33
c ---[ 209]---> BDD-cost:   45
c ---[ 208]---> BDD-cost:   43
c ---[ 207]---> BDD-cost:   21
c ---[ 206]---> BDD-cost:   33
c ---[ 205]---> BDD-cost:   45
c ---[ 204]---> BDD-cost:   57
c ---[ 203]---> BDD-cost:   69
c ---[ 202]---> BDD-cost:   81
c ---[ 201]---> BDD-cost:   71
c ---[ 200]---> BDD-cost:   83
c ---[ 199]---> BDD-cost:   71
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   33
c ---[ 193]---> BDD-cost:   45
c ---[ 192]---> BDD-cost:   47
c ---[ 191]---> BDD-cost:   69
c ---[ 190]---> BDD-cost:   71
c ---[ 189]---> BDD-cost:   93
c ---[ 188]---> BDD-cost:   95
c ---[ 187]---> BDD-cost:  117
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   29
c ---[ 183]---> BDD-cost:   29
c ---[ 182]---> BDD-cost:   29
c ---[ 181]---> BDD-cost:   41
c ---[ 180]---> BDD-cost:   53
c ---[ 179]---> BDD-cost:   65
c ---[ 178]---> BDD-cost:   77
c ---[ 177]---> BDD-cost:   21
c ---[ 176]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:   45
c ---[ 174]---> BDD-cost:   57
c ---[ 173]---> BDD-cost:   59
c ---[ 172]---> BDD-cost:   81
c ---[ 171]---> BDD-cost:   83
c ---[ 170]---> BDD-cost:  105
c ---[ 169]---> BDD-cost:  107
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:   21
c ---[ 162]---> BDD-cost:   33
c ---[ 161]---> BDD-cost:   45
c ---[ 160]---> BDD-cost:   57
c ---[ 159]---> BDD-cost:   21
c ---[ 158]---> BDD-cost:   33
c ---[ 157]---> BDD-cost:   23
c ---[ 156]---> BDD-cost:   35
c ---[ 155]---> BDD-cost:   47
c ---[ 154]---> BDD-cost:   81
c ---[ 153]---> BDD-cost:   83
c ---[ 152]---> BDD-cost:   95
c ---[ 151]---> BDD-cost:  107
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:   21
c ---[ 146]---> BDD-cost:   33
c ---[ 145]---> BDD-cost:   45
c ---[ 144]---> BDD-cost:   47
c ---[ 143]---> BDD-cost:   69
c ---[ 142]---> BDD-cost:   71
c ---[ 141]---> BDD-cost:   93
c ---[ 140]---> BDD-cost:   95
c ---[ 139]---> BDD-cost:  107
c ---[ 138]---> BDD-cost:   21
c ---[ 137]---> BDD-cost:   33
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   35
c ---[ 132]---> BDD-cost:   47
c ---[ 131]---> BDD-cost:   59
c ---[ 130]---> BDD-cost:   71
c ---[ 129]---> BDD-cost:   21
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   45
c ---[ 126]---> BDD-cost:   47
c ---[ 125]---> BDD-cost:   69
c ---[ 124]---> BDD-cost:   71
c ---[ 123]---> BDD-cost:   93
c ---[ 122]---> BDD-cost:   95
c ---[ 121]---> BDD-cost:  117
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:   21
c ---[ 114]---> BDD-cost:   33
c ---[ 113]---> BDD-cost:   45
c ---[ 112]---> BDD-cost:   57
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   33
c ---[ 109]---> BDD-cost:   25
c ---[ 108]---> BDD-cost:   35
c ---[ 107]---> BDD-cost:   59
c ---[ 106]---> BDD-cost:   71
c ---[ 105]---> BDD-cost:   83
c ---[ 104]---> BDD-cost:   95
c ---[ 103]---> BDD-cost:   83
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:  273
c ---[  98]---> BDD-cost:  273
c ---[  97]---> BDD-cost:  273
c ---[  96]---> BDD-cost:  273
c ---[  95]---> BDD-cost:  269
c ---[  94]---> BDD-cost:  141
c ---[  93]---> BDD-cost:  141
c ---[  92]---> BDD-cost:  271
c ---[  91]---> BDD-cost:  273
c ---[  90]---> BDD-cost:  269
c ---[  89]---> BDD-cost:  273
c ---[  88]---> BDD-cost:  263
c ---[  87]---> BDD-cost:  141
c ---[  86]---> BDD-cost:  141
c ---[  85]---> BDD-cost:  273
c ---[  84]---> BDD-cost:  263
c ---[  83]---> BDD-cost:  265
c ---[  82]---> BDD-cost:  273
c ---[  81]---> BDD-cost:  273
c ---[  80]---> BDD-cost:  141
c ---[  79]---> BDD-cost:  141
c ---[  78]---> BDD-cost:  263
c ---[  77]---> BDD-cost:  273
c ---[  76]---> BDD-cost:  273
c ---[  75]---> BDD-cost:  239
c ---[  74]---> BDD-cost:  263
c ---[  73]---> BDD-cost:  141
c ---[  72]---> BDD-cost:  141
c ---[  71]---> BDD-cost:  269
c ---[  70]---> BDD-cost:  227
c ---[  69]---> BDD-cost:  263
c ---[  68]---> BDD-cost:  267
c ---[  67]---> BDD-cost:  263
c ---[  66]---> BDD-cost:  141
c ---[  65]---> BDD-cost:  141
c ---[  64]---> BDD-cost:  239
c ---[  63]---> BDD-cost:  265
c ---[  62]---> BDD-cost:  251
c ---[  61]---> BDD-cost:  273
c ---[  60]---> BDD-cost:  273
c ---[  59]---> BDD-cost:  141
c ---[  58]---> BDD-cost:  141
c ---[  57]---> BDD-cost:  273
c ---[  56]---> BDD-cost:  273
c ---[  55]---> BDD-cost:  273
c ---[  54]---> BDD-cost:  273
c ---[  53]---> BDD-cost:  251
c ---[  52]---> BDD-cost:  141
c ---[  51]---> BDD-cost:  141
c ---[  50]---> BDD-cost:  263
c ---[  49]---> BDD-cost:  273
c ---[  48]---> BDD-cost:  273
c ---[  47]---> BDD-cost:  273
c ---[  46]---> BDD-cost:  273
c ---[  45]---> BDD-cost:  115
c ---[  44]---> BDD-cost:  141
c ---[  43]---> BDD-cost:  263
c ---[  42]---> BDD-cost:  263
c ---[  41]---> BDD-cost:  273
c ---[  40]---> BDD-cost:  233
c ---[  39]---> BDD-cost:  273
c ---[  38]---> BDD-cost:  141
c ---[  37]---> BDD-cost:  141
c ---[  36]---> BDD-cost:  261
c ---[  35]---> BDD-cost:  239
c ---[  34]---> BDD-cost:  263
c ---[  33]---> BDD-cost:  273
c ---[  32]---> BDD-cost:  263
c ---[  31]---> BDD-cost:  141
c ---[  30]---> BDD-cost:  141
c ---[  29]---> Adder-cost: 1446   maxlim: 828   bits: 10/10
c ---[  28]---> Adder-cost: 1416   maxlim: 828   bits: 10/10
c ---[  27]---> Adder-cost: 1412   maxlim: 828   bits: 10/10
c ---[  26]---> Adder-cost: 1448   maxlim: 828   bits: 10/10
c ---[  25]---> Adder-cost: 1428   maxlim: 828   bits: 10/10
c ---[  24]---> Adder-cost: 1438   maxlim: 828   bits: 10/10
c ---[  23]---> Adder-cost: 1438   maxlim: 828   bits: 10/10
c ---[  22]---> Adder-cost: 1388   maxlim: 828   bits: 10/10
c ---[  21]---> Adder-cost: 1470   maxlim: 828   bits: 10/10
c ---[  20]---> Adder-cost: 1388   maxlim: 828   bits: 10/10
c ---[  19]---> BDD-cost: 1307
c ---[  18]---> BDD-cost: 1302
c ---[  17]---> BDD-cost: 1303
c ---[  16]---> BDD-cost: 1305
c ---[  15]---> BDD-cost: 1302
c ---[  14]---> BDD-cost: 1299
c ---[  13]---> BDD-cost: 1307
c ---[  12]---> BDD-cost: 1307
c ---[  11]---> BDD-cost: 1305
c ---[  10]---> BDD-cost: 1307
c ---[   9]---> BDD-cost:  721
c ---[   8]---> BDD-cost:  716
c ---[   7]---> BDD-cost:  716
c ---[   6]---> BDD-cost:  721
c ---[   5]---> BDD-cost:  717
c ---[   4]---> BDD-cost:  731
c ---[   3]---> BDD-cost:  675
c ---[   2]---> BDD-cost:  714
c ---[   1]---> BDD-cost:  723
c ---[   0]---> BDD-cost:  731
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2307742  7817718 |  769247       0        0     nan |  0.000 % |
c |       102 | 2307715  7817623 |  846171     100      538     5.4 |  1.956 % |
c |       264 | 2307712  7817614 |  930788     257    11092    43.2 |  1.956 % |
c |       490 | 2307703  7817587 | 1023867     474    15162    32.0 |  1.957 % |
c |       828 | 2307703  7817587 | 1126254     812    28025    34.5 |  1.957 % |
c |      1335 | 2307635  7817347 | 1238879    1306    63664    48.7 |  1.957 % |
c |      2094 | 2307635  7817347 | 1362767    2065    92386    44.7 |  1.957 % |
c |      3234 | 2307451  7816689 | 1499044    3185   179837    56.5 |  1.959 % |
c |      4943 | 2307299  7816151 | 1648949    4839   319898    66.1 |  1.961 % |
c |      7507 | 2306792  7814328 | 1813844    7361   559199    76.0 |  1.965 % |
c |     11351 | 2306394  7812896 | 1995228   11168   872187    78.1 |  1.969 % |
c |     17117 | 2306106  7811868 | 2194751   16900  1534364    90.8 |  1.971 % |
c |     25767 | 2305918  7811204 | 2414226   25531  2567240   100.6 |  1.973 % |
c |     38742 | 2305589  7810019 | 2655649   38464  4263347   110.8 |  1.977 % |
c |     58203 | 2304913  7807599 | 2921214   57819  6790674   117.4 |  1.983 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 25549 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 25545
Raw data (stat): 25545 (runsolver) R 25544 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784807987 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 25602
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0017 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 25602
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0022 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 25602
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0035 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 25602
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0043 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 25602
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0046 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 25602
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0049 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 25602
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0075 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25604
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.06 s]
Raw data (loadavg): 0.99 0.98 0.92 3/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.79 s]
Raw data (loadavg): 0.99 0.98 0.92 1/53 25606
Raw data (stat): 25545 (minisat+_script) S 25544 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784807987 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.79
CPU time (s): 1229.95
CPU user time (s): 1227.9
CPU system time (s): 2.04669
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####