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-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos6.opb
MD5SUM	6975fcd4cac18749e2635ee3bd162046
Bench Category	optimization, big integers (OPTBIGINT)
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	6690
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	239444426529
Number of bits of the sum of numbers in the objective function	38
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	239444426529
Number of bits of the biggest sum of numbers	38
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.223965
Number of variables	21720
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	840
Trace number 30920

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-25 20:49:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22317 boxname=wulflinc4 idbench=1133 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  6975fcd4cac18749e2635ee3bd162046  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-neos6.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-neos6.opb
IDLAUNCH: 22317
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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		: 451.169
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:        865016 kB
Buffers:         28628 kB
Cached:         120064 kB
SwapCached:        500 kB
Active:          34380 kB
Inactive:       116672 kB
HighTotal:      131008 kB
HighFree:        18032 kB
LowTotal:       903652 kB
LowFree:        846984 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5784 kB
Slab:            12812 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:10:25 (client local time) WITH STATUS 152 IN 1229.96 SECONDS
stats: 22317 7 1229.96 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]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Adder-cost: 308   maxlim: 1073859583   bits: 32/31
c ---[1020]---> Adder-cost: 368   maxlim: 1073921023   bits: 32/31
c ---[1018]---> Adder-cost: 432   maxlim: 1073982463   bits: 32/31
c ---[1016]---> Adder-cost: 496   maxlim: 1074043903   bits: 32/31
c ---[1014]---> Adder-cost: 544   maxlim: 1074104319   bits: 32/31
c ---[1012]---> Adder-cost: 582   maxlim: 1074165759   bits: 32/31
c ---[1010]---> Adder-cost: 650   maxlim: 1074227199   bits: 32/31
c ---[1008]---> Adder-cost: 792   maxlim: 1074278399   bits: 32/31
c ---[1006]---> Adder-cost: 852   maxlim: 1074329599   bits: 32/31
c ---[1004]---> Adder-cost: 908   maxlim: 1074372607   bits: 32/31
c ---[1002]---> Adder-cost: 998   maxlim: 1074413567   bits: 32/31
c ---[1000]---> Adder-cost: 1058   maxlim: 1074444287   bits: 32/31
c ---[ 998]---> Adder-cost: 1130   maxlim: 1074475007   bits: 32/31
c ---[ 996]---> Adder-cost: 1104   maxlim: 1074495487   bits: 32/31
c ---[ 994]---> Adder-cost: 1174   maxlim: 1074513919   bits: 32/31
c ---[ 992]---> Adder-cost: 1144   maxlim: 1074524159   bits: 32/31
c ---[ 990]---> Adder-cost: 1170   maxlim: 1074534399   bits: 32/31
c ---[ 988]---> Adder-cost: 1246   maxlim: 1074524159   bits: 32/31
c ---[ 986]---> Adder-cost: 1162   maxlim: 1074516991   bits: 32/31
c ---[ 984]---> Adder-cost: 1242   maxlim: 1074496511   bits: 32/31
c ---[ 982]---> Adder-cost: 1230   maxlim: 1074476031   bits: 32/31
c ---[ 980]---> Adder-cost: 1178   maxlim: 1074445311   bits: 32/31
c ---[ 978]---> Adder-cost: 1144   maxlim: 1074412543   bits: 32/31
c ---[ 976]---> Adder-cost: 1094   maxlim: 1074371583   bits: 32/31
c ---[ 974]---> Adder-cost: 1010   maxlim: 1074330623   bits: 32/31
c ---[ 972]---> Adder-cost: 986   maxlim: 1074281471   bits: 32/31
c ---[ 970]---> Adder-cost: 882   maxlim: 1074230271   bits: 32/31
c ---[ 968]---> Adder-cost: 790   maxlim: 1074168831   bits: 32/31
c ---[ 966]---> Adder-cost: 670   maxlim: 1074107391   bits: 32/31
c ---[ 964]---> Adder-cost: 604   maxlim: 1074045951   bits: 32/31
c ---[ 962]---> Adder-cost: 520   maxlim: 1073981439   bits: 32/31
c ---[ 960]---> Adder-cost: 414   maxlim: 1073919999   bits: 32/31
c ---[ 958]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 956]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 950]---> Adder-cost: 382   maxlim: 1073921023   bits: 32/31
c ---[ 948]---> Adder-cost: 450   maxlim: 1073982463   bits: 32/31
c ---[ 946]---> Adder-cost: 522   maxlim: 1074043903   bits: 32/31
c ---[ 944]---> Adder-cost: 578   maxlim: 1074106367   bits: 32/31
c ---[ 942]---> Adder-cost: 628   maxlim: 1074167807   bits: 32/31
c ---[ 940]---> Adder-cost: 682   maxlim: 1074229247   bits: 32/31
c ---[ 938]---> Adder-cost: 962   maxlim: 1074280447   bits: 32/31
c ---[ 936]---> Adder-cost: 1060   maxlim: 1074331647   bits: 32/31
c ---[ 934]---> Adder-cost: 976   maxlim: 1074372607   bits: 32/31
c ---[ 932]---> Adder-cost: 1018   maxlim: 1074413567   bits: 32/31
c ---[ 930]---> Adder-cost: 1114   maxlim: 1074444287   bits: 32/31
c ---[ 928]---> Adder-cost: 1138   maxlim: 1074476031   bits: 32/31
c ---[ 926]---> Adder-cost: 1130   maxlim: 1074496511   bits: 32/31
c ---[ 924]---> Adder-cost: 1134   maxlim: 1074513919   bits: 32/31
c ---[ 922]---> Adder-cost: 1184   maxlim: 1074524159   bits: 32/31
c ---[ 920]---> Adder-cost: 1208   maxlim: 1074534399   bits: 32/31
c ---[ 918]---> Adder-cost: 1198   maxlim: 1074524159   bits: 32/31
c ---[ 916]---> Adder-cost: 1218   maxlim: 1074516991   bits: 32/31
c ---[ 914]---> Adder-cost: 1220   maxlim: 1074496511   bits: 32/31
c ---[ 912]---> Adder-cost: 1236   maxlim: 1074476031   bits: 32/31
c ---[ 910]---> Adder-cost: 1194   maxlim: 1074445311   bits: 32/31
c ---[ 908]---> Adder-cost: 1144   maxlim: 1074412543   bits: 32/31
c ---[ 906]---> Adder-cost: 1088   maxlim: 1074371583   bits: 32/31
c ---[ 904]---> Adder-cost: 1016   maxlim: 1074330623   bits: 32/31
c ---[ 902]---> Adder-cost: 974   maxlim: 1074281471   bits: 32/31
c ---[ 900]---> Adder-cost: 882   maxlim: 1074230271   bits: 32/31
c ---[ 898]---> Adder-cost: 792   maxlim: 1074168831   bits: 32/31
c ---[ 896]---> Adder-cost: 672   maxlim: 1074107391   bits: 32/31
c ---[ 894]---> Adder-cost: 620   maxlim: 1074045951   bits: 32/31
c ---[ 892]---> Adder-cost: 540   maxlim: 1073981439   bits: 32/31
c ---[ 890]---> Adder-cost: 408   maxlim: 1073919999   bits: 32/31
c ---[ 888]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 886]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 884]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 880]---> Adder-cost: 382   maxlim: 1073921023   bits: 32/31
c ---[ 878]---> Adder-cost: 440   maxlim: 1073982463   bits: 32/31
c ---[ 876]---> Adder-cost: 512   maxlim: 1074043903   bits: 32/31
c ---[ 874]---> Adder-cost: 584   maxlim: 1074105343   bits: 32/31
c ---[ 872]---> Adder-cost: 600   maxlim: 1074167807   bits: 32/31
c ---[ 870]---> Adder-cost: 680   maxlim: 1074229247   bits: 32/31
c ---[ 868]---> Adder-cost: 902   maxlim: 1074281471   bits: 32/31
c ---[ 866]---> Adder-cost: 924   maxlim: 1074332671   bits: 32/31
c ---[ 864]---> Adder-cost: 916   maxlim: 1074373631   bits: 32/31
c ---[ 862]---> Adder-cost: 978   maxlim: 1074414591   bits: 32/31
c ---[ 860]---> Adder-cost: 1016   maxlim: 1074442239   bits: 32/31
c ---[ 858]---> Adder-cost: 1032   maxlim: 1074472959   bits: 32/31
c ---[ 856]---> Adder-cost: 1070   maxlim: 1074493439   bits: 32/31
c ---[ 854]---> Adder-cost: 1084   maxlim: 1074513919   bits: 32/31
c ---[ 852]---> Adder-cost: 1120   maxlim: 1074524159   bits: 32/31
c ---[ 850]---> Adder-cost: 1140   maxlim: 1074534399   bits: 32/31
c ---[ 848]---> Adder-cost: 1160   maxlim: 1074524159   bits: 32/31
c ---[ 846]---> Adder-cost: 1150   maxlim: 1074513919   bits: 32/31
c ---[ 844]---> Adder-cost: 1174   maxlim: 1074494463   bits: 32/31
c ---[ 842]---> Adder-cost: 1140   maxlim: 1074473983   bits: 32/31
c ---[ 840]---> Adder-cost: 1154   maxlim: 1074443263   bits: 32/31
c ---[ 838]---> Adder-cost: 1144   maxlim: 1074412543   bits: 32/31
c ---[ 836]---> Adder-cost: 1086   maxlim: 1074371583   bits: 32/31
c ---[ 834]---> Adder-cost: 1046   maxlim: 1074330623   bits: 32/31
c ---[ 832]---> Adder-cost: 954   maxlim: 1074281471   bits: 32/31
c ---[ 830]---> Adder-cost: 880   maxlim: 1074230271   bits: 32/31
c ---[ 828]---> Adder-cost: 796   maxlim: 1074168831   bits: 32/31
c ---[ 826]---> Adder-cost: 724   maxlim: 1074107391   bits: 32/31
c ---[ 824]---> Adder-cost: 620   maxlim: 1074045951   bits: 32/31
c ---[ 822]---> Adder-cost: 510   maxlim: 1073981439   bits: 32/31
c ---[ 820]---> Adder-cost: 422   maxlim: 1073919999   bits: 32/31
c ---[ 818]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 816]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 814]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 810]---> Adder-cost: 384   maxlim: 1073921023   bits: 32/31
c ---[ 808]---> Adder-cost: 456   maxlim: 1073982463   bits: 32/31
c ---[ 806]---> Adder-cost: 520   maxlim: 1074043903   bits: 32/31
c ---[ 804]---> Adder-cost: 604   maxlim: 1074106367   bits: 32/31
c ---[ 802]---> Adder-cost: 658   maxlim: 1074167807   bits: 32/31
c ---[ 800]---> Adder-cost: 692   maxlim: 1074229247   bits: 32/31
c ---[ 798]---> Adder-cost: 1034   maxlim: 1074280447   bits: 32/31
c ---[ 796]---> Adder-cost: 1000   maxlim: 1074331647   bits: 32/31
c ---[ 794]---> Adder-cost: 1118   maxlim: 1074372607   bits: 32/31
c ---[ 792]---> Adder-cost: 1122   maxlim: 1074413567   bits: 32/31
c ---[ 790]---> Adder-cost: 1184   maxlim: 1074444287   bits: 32/31
c ---[ 788]---> Adder-cost: 1192   maxlim: 1074476031   bits: 32/31
c ---[ 786]---> Adder-cost: 1270   maxlim: 1074496511   bits: 32/31
c ---[ 784]---> Adder-cost: 1368   maxlim: 1074516991   bits: 32/31
c ---[ 782]---> Adder-cost: 1254   maxlim: 1074527231   bits: 32/31
c ---[ 780]---> Adder-cost: 1392   maxlim: 1074537471   bits: 32/31
c ---[ 778]---> Adder-cost: 1328   maxlim: 1074527231   bits: 32/31
c ---[ 776]---> Adder-cost: 1304   maxlim: 1074516991   bits: 32/31
c ---[ 774]---> Adder-cost: 1276   maxlim: 1074496511   bits: 32/31
c ---[ 772]---> Adder-cost: 1260   maxlim: 1074476031   bits: 32/31
c ---[ 770]---> Adder-cost: 1182   maxlim: 1074445311   bits: 32/31
c ---[ 768]---> Adder-cost: 1156   maxlim: 1074412543   bits: 32/31
c ---[ 766]---> Adder-cost: 1098   maxlim: 1074371583   bits: 32/31
c ---[ 764]---> Adder-cost: 1072   maxlim: 1074330623   bits: 32/31
c ---[ 762]---> Adder-cost: 966   maxlim: 1074281471   bits: 32/31
c ---[ 760]---> Adder-cost: 892   maxlim: 1074230271   bits: 32/31
c ---[ 758]---> Adder-cost: 788   maxlim: 1074168831   bits: 32/31
c ---[ 756]---> Adder-cost: 676   maxlim: 1074107391   bits: 32/31
c ---[ 754]---> Adder-cost: 594   maxlim: 1074045951   bits: 32/31
c ---[ 752]---> Adder-cost: 528   maxlim: 1073981439   bits: 32/31
c ---[ 750]---> Adder-cost: 412   maxlim: 1073919999   bits: 32/31
c ---[ 748]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 746]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 740]---> Adder-cost: 386   maxlim: 1073921023   bits: 32/31
c ---[ 738]---> Adder-cost: 450   maxlim: 1073982463   bits: 32/31
c ---[ 736]---> Adder-cost: 524   maxlim: 1074043903   bits: 32/31
c ---[ 734]---> Adder-cost: 584   maxlim: 1074105343   bits: 32/31
c ---[ 732]---> Adder-cost: 662   maxlim: 1074166783   bits: 32/31
c ---[ 730]---> Adder-cost: 692   maxlim: 1074229247   bits: 32/31
c ---[ 728]---> Adder-cost: 976   maxlim: 1074280447   bits: 32/31
c ---[ 726]---> Adder-cost: 1002   maxlim: 1074331647   bits: 32/31
c ---[ 724]---> Adder-cost: 982   maxlim: 1074372607   bits: 32/31
c ---[ 722]---> Adder-cost: 1038   maxlim: 1074413567   bits: 32/31
c ---[ 720]---> Adder-cost: 1120   maxlim: 1074444287   bits: 32/31
c ---[ 718]---> Adder-cost: 1122   maxlim: 1074476031   bits: 32/31
c ---[ 716]---> Adder-cost: 1144   maxlim: 1074496511   bits: 32/31
c ---[ 714]---> Adder-cost: 1106   maxlim: 1074513919   bits: 32/31
c ---[ 712]---> Adder-cost: 1226   maxlim: 1074524159   bits: 32/31
c ---[ 710]---> Adder-cost: 1216   maxlim: 1074534399   bits: 32/31
c ---[ 708]---> Adder-cost: 1234   maxlim: 1074524159   bits: 32/31
c ---[ 706]---> Adder-cost: 1216   maxlim: 1074516991   bits: 32/31
c ---[ 704]---> Adder-cost: 1228   maxlim: 1074496511   bits: 32/31
c ---[ 702]---> Adder-cost: 1246   maxlim: 1074476031   bits: 32/31
c ---[ 700]---> Adder-cost: 1154   maxlim: 1074445311   bits: 32/31
c ---[ 698]---> Adder-cost: 1154   maxlim: 1074412543   bits: 32/31
c ---[ 696]---> Adder-cost: 1116   maxlim: 1074371583   bits: 32/31
c ---[ 694]---> Adder-cost: 1018   maxlim: 1074330623   bits: 32/31
c ---[ 692]---> Adder-cost: 994   maxlim: 1074281471   bits: 32/31
c ---[ 690]---> Adder-cost: 868   maxlim: 1074230271   bits: 32/31
c ---[ 688]---> Adder-cost: 808   maxlim: 1074168831   bits: 32/31
c ---[ 686]---> Adder-cost: 692   maxlim: 1074107391   bits: 32/31
c ---[ 684]---> Adder-cost: 600   maxlim: 1074045951   bits: 32/31
c ---[ 682]---> Adder-cost: 520   maxlim: 1073981439   bits: 32/31
c ---[ 680]---> Adder-cost: 420   maxlim: 1073919999   bits: 32/31
c ---[ 678]---> Adder-cost: 324   maxlim: 1073862655   bits: 32/31
c ---[ 676]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Adder-cost: 328   maxlim: 1073862655   bits: 32/31
c ---[ 670]---> Adder-cost: 450   maxlim: 1073924095   bits: 32/31
c ---[ 668]---> Adder-cost: 438   maxlim: 1073985535   bits: 32/31
c ---[ 666]---> Adder-cost: 490   maxlim: 1074046975   bits: 32/31
c ---[ 664]---> Adder-cost: 576   maxlim: 1074108415   bits: 32/31
c ---[ 662]---> Adder-cost: 632   maxlim: 1074169855   bits: 32/31
c ---[ 660]---> Adder-cost: 860   maxlim: 1074221055   bits: 32/31
c ---[ 658]---> Adder-cost: 828   maxlim: 1074262015   bits: 32/31
c ---[ 656]---> Adder-cost: 950   maxlim: 1074292735   bits: 32/31
c ---[ 654]---> Adder-cost: 948   maxlim: 1074313215   bits: 32/31
c ---[ 652]---> Adder-cost: 1002   maxlim: 1074323455   bits: 32/31
c ---[ 650]---> Adder-cost: 978   maxlim: 1074323455   bits: 32/31
c ---[ 648]---> Adder-cost: 918   maxlim: 1074313215   bits: 32/31
c ---[ 646]---> Adder-cost: 912   maxlim: 1074292735   bits: 32/31
c ---[ 644]---> Adder-cost: 910   maxlim: 1074262015   bits: 32/31
c ---[ 642]---> Adder-cost: 868   maxlim: 1074221055   bits: 32/31
c ---[ 640]---> Adder-cost: 786   maxlim: 1074169855   bits: 32/31
c ---[ 638]---> Adder-cost: 690   maxlim: 1074108415   bits: 32/31
c ---[ 636]---> Adder-cost: 608   maxlim: 1074046975   bits: 32/31
c ---[ 634]---> Adder-cost: 530   maxlim: 1073985535   bits: 32/31
c ---[ 632]---> Adder-cost: 428   maxlim: 1073924095   bits: 32/31
c ---[ 630]---> Adder-cost: 320   maxlim: 1073862655   bits: 32/31
c ---[ 628]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Adder-cost: 328   maxlim: 1073862655   bits: 32/31
c ---[ 622]---> Adder-cost: 382   maxlim: 1073924095   bits: 32/31
c ---[ 620]---> Adder-cost: 458   maxlim: 1073985535   bits: 32/31
c ---[ 618]---> Adder-cost: 524   maxlim: 1074046975   bits: 32/31
c ---[ 616]---> Adder-cost: 578   maxlim: 1074108415   bits: 32/31
c ---[ 614]---> Adder-cost: 654   maxlim: 1074169855   bits: 32/31
c ---[ 612]---> Adder-cost: 964   maxlim: 1074221055   bits: 32/31
c ---[ 610]---> Adder-cost: 942   maxlim: 1074262015   bits: 32/31
c ---[ 608]---> Adder-cost: 958   maxlim: 1074292735   bits: 32/31
c ---[ 606]---> Adder-cost: 928   maxlim: 1074313215   bits: 32/31
c ---[ 604]---> Adder-cost: 978   maxlim: 1074323455   bits: 32/31
c ---[ 602]---> Adder-cost: 986   maxlim: 1074322431   bits: 32/31
c ---[ 600]---> Adder-cost: 920   maxlim: 1074312191   bits: 32/31
c ---[ 598]---> Adder-cost: 928   maxlim: 1074291711   bits: 32/31
c ---[ 596]---> Adder-cost: 894   maxlim: 1074260991   bits: 32/31
c ---[ 594]---> Adder-cost: 846   maxlim: 1074220031   bits: 32/31
c ---[ 592]---> Adder-cost: 800   maxlim: 1074168831   bits: 32/31
c ---[ 590]---> Adder-cost: 692   maxlim: 1074107391   bits: 32/31
c ---[ 588]---> Adder-cost: 614   maxlim: 1074045951   bits: 32/31
c ---[ 586]---> Adder-cost: 522   maxlim: 1073984511   bits: 32/31
c ---[ 584]---> Adder-cost: 402   maxlim: 1073923071   bits: 32/31
c ---[ 582]---> Adder-cost: 316   maxlim: 1073861631   bits: 32/31
c ---[ 580]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 | 2411357  8078600 |  803785       0        0     nan |  0.000 % |
c |       100 | 2411357  8078600 |  884163     100      950     9.5 |  2.852 % |
c |       250 | 2411343  8078558 |  972579     242     3399    14.0 |  2.852 % |
c |       475 | 2411343  8078558 | 1069837     467    15737    33.7 |  2.852 % |
c |       813 | 2411343  8078558 | 1176821     805    29179    36.2 |  2.852 % |
c |      1319 | 2411312  8078465 | 1294503    1281    60674    47.4 |  2.853 % |
c |      2078 | 2411291  8078414 | 1423954    2037   196368    96.4 |  2.854 % |
c |      3218 | 2411270  8078355 | 1566349    3176   407748   128.4 |  2.855 % |
c |      4927 | 2411209  8078210 | 1722984    4880   864118   177.1 |  2.858 % |
c |      7490 | 2410919  8077192 | 1895282    7407  1028001   138.8 |  2.861 % |
c |     11347 | 2410624  8076163 | 2084811   11215  1321257   117.8 |  2.865 % |
c |     17113 | 2410313  8075056 | 2293292   16948  2198764   129.7 |  2.868 % |
c |     25763 | 2409688  8073126 | 2522621   25529  3920391   153.6 |  2.882 % |
c |     38737 | 2409418  8072170 | 2774883   38458  6228731   162.0 |  2.885 % |
c |     58199 | 2408903  8070389 | 3052372   57828 10556214   182.5 |  2.893 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  5253 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.89 0.97 0.96 2/54 5249
Raw data (stat): 5249 (runsolver) R 5248 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783660014 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+9.99999 s]
Raw data (loadavg): 0.91 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0007 s]
Raw data (loadavg): 0.92 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0005 s]
Raw data (loadavg): 0.93 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0016 s]
Raw data (loadavg): 0.94 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0023 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0021 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0019 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0018 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.0017 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.002 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.002 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.003 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.003 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5253
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 5256
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.038 s]
Raw data (loadavg): 1.07 0.99 0.96 2/55 5306
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.038 s]
Raw data (loadavg): 1.06 0.99 0.96 2/55 5306
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.038 s]
Raw data (loadavg): 1.05 0.99 0.96 2/55 5306
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.038 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 5306
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.038 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 5306
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.039 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 5306
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.04 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 5306
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.041 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.042 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.042 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.044 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.044 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.045 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.046 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.046 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.047 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.048 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.048 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.063 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.063 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.064 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.064 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.065 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.065 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.065 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.066 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.066 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.067 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5308
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.069 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.071 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.072 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.072 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.072 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.81 s]
Raw data (loadavg): 1.00 0.99 0.96 1/53 5310
Raw data (stat): 5249 (minisat+_script) S 5248 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783660014 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.81
CPU time (s): 1229.96
CPU user time (s): 1227.72
CPU system time (s): 2.24566
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####