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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-qiu.opb
MD5SUMd644054326940d86bc7f3576874ac5a9
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 7968
Biggest coefficient in the objective function 9098351345664
Number of bits for the biggest coefficient in the objective function 44
Sum of the numbers in the objective function 4803935111035752
Number of bits of the sum of numbers in the objective function 53
Biggest number in a constraint 9098351345664
Number of bits of the biggest number in a constraint 44
Biggest sum of numbers in a constraint 4803935111035752
Number of bits of the biggest sum of numbers53
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables23808
Total number of constraints1192
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1192
Minimum length of a constraint31
Maximum length of a constraint5940

Trace number 3883

Launcher Data

LAUNCH ON wulflinc26 THE 2005-09-19 03:24:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2881 boxname=wulflinc26 idbench=537 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d644054326940d86bc7f3576874ac5a9  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-qiu.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-qiu.opb
IDLAUNCH: 2881
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        887668 kB
Buffers:         37952 kB
Cached:          80044 kB
SwapCached:        868 kB
Active:          71224 kB
Inactive:        49456 kB
HighTotal:      131008 kB
HighFree:        48188 kB
LowTotal:       903652 kB
LowFree:        839480 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            20600 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:44:38 (client local time) WITH STATUS 0 IN 1206.3 SECONDS
stats: 2881 7 1206.3 0

Solver Data

c Parsing PB file...
c Converting 1324 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1322]---> BDD-cost:    0
c ---[1320]---> BDD-cost:    0
c ---[1318]---> BDD-cost:    0
c ---[1317]---> BDD-cost:   17
c ---[1316]---> BDD-cost:   17
c ---[1315]---> BDD-cost:   17
c ---[1314]---> BDD-cost:   17
c ---[1313]---> BDD-cost:   17
c ---[1312]---> BDD-cost:   17
c ---[1311]---> BDD-cost:   17
c ---[1310]---> BDD-cost:   17
c ---[1309]---> BDD-cost:   17
c ---[1308]---> BDD-cost:   18
c ---[1306]---> BDD-cost:    0
c ---[1305]---> BDD-cost:   18
c ---[1304]---> BDD-cost:   18
c ---[1303]---> BDD-cost:   18
c ---[1302]---> BDD-cost:   18
c ---[1301]---> BDD-cost:   18
c ---[1300]---> BDD-cost:   18
c ---[1299]---> BDD-cost:   18
c ---[1298]---> BDD-cost:   25
c ---[1297]---> BDD-cost:   25
c ---[1296]---> BDD-cost:   25
c ---[1294]---> BDD-cost:    0
c ---[1293]---> BDD-cost:   25
c ---[1292]---> BDD-cost:   25
c ---[1291]---> BDD-cost:   25
c ---[1290]---> BDD-cost:   25
c ---[1289]---> BDD-cost:   25
c ---[1288]---> BDD-cost:   17
c ---[1287]---> BDD-cost:   17
c ---[1286]---> BDD-cost:   17
c ---[1285]---> BDD-cost:   17
c ---[1284]---> BDD-cost:   17
c ---[1282]---> BDD-cost:    0
c ---[1281]---> BDD-cost:   17
c ---[1280]---> BDD-cost:   17
c ---[1279]---> BDD-cost:   17
c ---[1278]---> BDD-cost:   17
c ---[1277]---> BDD-cost:   17
c ---[1276]---> BDD-cost:   17
c ---[1275]---> BDD-cost:   17
c ---[1274]---> BDD-cost:   17
c ---[1273]---> BDD-cost:   17
c ---[1272]---> BDD-cost:   17
c ---[1270]---> BDD-cost:    0
c ---[1269]---> BDD-cost:   17
c ---[1268]---> BDD-cost:   23
c ---[1267]---> BDD-cost:   23
c ---[1266]---> BDD-cost:   23
c ---[1265]---> BDD-cost:   23
c ---[1264]---> BDD-cost:   23
c ---[1263]---> BDD-cost:   23
c ---[1262]---> BDD-cost:   23
c ---[1261]---> BDD-cost:   23
c ---[1260]---> BDD-cost:   17
c ---[1258]---> BDD-cost:    0
c ---[1257]---> BDD-cost:   17
c ---[1256]---> BDD-cost:   17
c ---[1255]---> BDD-cost:   17
c ---[1254]---> BDD-cost:   17
c ---[1253]---> BDD-cost:   17
c ---[1252]---> BDD-cost:   17
c ---[1251]---> BDD-cost:   17
c ---[1250]---> BDD-cost:   19
c ---[1249]---> BDD-cost:   19
c ---[1248]---> BDD-cost:   19
c ---[1246]---> BDD-cost:    0
c ---[1245]---> BDD-cost:   19
c ---[1244]---> BDD-cost:   19
c ---[1243]---> BDD-cost:   19
c ---[1242]---> BDD-cost:   19
c ---[1241]---> BDD-cost:   19
c ---[1240]---> BDD-cost:   17
c ---[1239]---> BDD-cost:   17
c ---[1238]---> BDD-cost:   17
c ---[1237]---> BDD-cost:   17
c ---[1236]---> BDD-cost:   17
c ---[1234]---> BDD-cost:    0
c ---[1233]---> BDD-cost:   17
c ---[1232]---> BDD-cost:   17
c ---[1231]---> BDD-cost:   17
c ---[1230]---> BDD-cost:   17
c ---[1229]---> BDD-cost:   17
c ---[1228]---> BDD-cost:   17
c ---[1227]---> BDD-cost:   17
c ---[1226]---> BDD-cost:   17
c ---[1225]---> BDD-cost:   17
c ---[1224]---> BDD-cost:   17
c ---[1222]---> BDD-cost:    0
c ---[1221]---> BDD-cost:   17
c ---[1220]---> BDD-cost:   17
c ---[1219]---> BDD-cost:   17
c ---[1218]---> BDD-cost:   17
c ---[1217]---> BDD-cost:   17
c ---[1216]---> BDD-cost:   17
c ---[1215]---> BDD-cost:   17
c ---[1214]---> BDD-cost:   17
c ---[1213]---> BDD-cost:   17
c ---[1212]---> BDD-cost:   23
c ---[1210]---> BDD-cost:    0
c ---[1209]---> BDD-cost:   23
c ---[1208]---> BDD-cost:   23
c ---[1207]---> BDD-cost:   23
c ---[1206]---> BDD-cost:   23
c ---[1205]---> BDD-cost:   23
c ---[1204]---> BDD-cost:   23
c ---[1203]---> BDD-cost:   23
c ---[1202]---> BDD-cost:   18
c ---[1201]---> BDD-cost:   18
c ---[1200]---> BDD-cost:   18
c ---[1198]---> BDD-cost:    0
c ---[1196]---> BDD-cost:    0
c ---[1195]---> BDD-cost:   18
c ---[1194]---> BDD-cost:   18
c ---[1193]---> BDD-cost:   18
c ---[1192]---> BDD-cost:   18
c ---[1191]---> BDD-cost:   18
c ---[1190]---> BDD-cost:   17
c ---[1189]---> BDD-cost:   17
c ---[1188]---> BDD-cost:   17
c ---[1187]---> BDD-cost:   17
c ---[1186]---> BDD-cost:   17
c ---[1184]---> BDD-cost:    0
c ---[1183]---> BDD-cost:   17
c ---[1182]---> BDD-cost:   17
c ---[1181]---> BDD-cost:   17
c ---[1180]---> BDD-cost:   17
c ---[1179]---> BDD-cost:   17
c ---[1178]---> BDD-cost:   17
c ---[1177]---> BDD-cost:   17
c ---[1176]---> BDD-cost:   17
c ---[1175]---> BDD-cost:   17
c ---[1174]---> BDD-cost:   17
c ---[1172]---> BDD-cost:    0
c ---[1171]---> BDD-cost:   17
c ---[1170]---> BDD-cost:   23
c ---[1169]---> BDD-cost:   23
c ---[1168]---> BDD-cost:   23
c ---[1167]---> BDD-cost:   23
c ---[1166]---> BDD-cost:   23
c ---[1165]---> BDD-cost:   23
c ---[1164]---> BDD-cost:   23
c ---[1163]---> BDD-cost:   23
c ---[1162]---> BDD-cost:   17
c ---[1160]---> BDD-cost:    0
c ---[1159]---> BDD-cost:   17
c ---[1158]---> BDD-cost:   17
c ---[1157]---> BDD-cost:   17
c ---[1156]---> BDD-cost:   17
c ---[1155]---> BDD-cost:   17
c ---[1154]---> BDD-cost:   17
c ---[1153]---> BDD-cost:   17
c ---[1152]---> BDD-cost:   19
c ---[1151]---> BDD-cost:   19
c ---[1150]---> BDD-cost:   19
c ---[1148]---> BDD-cost:    0
c ---[1147]---> BDD-cost:   19
c ---[1146]---> BDD-cost:   19
c ---[1145]---> BDD-cost:   19
c ---[1144]---> BDD-cost:   19
c ---[1143]---> BDD-cost:   19
c ---[1142]---> BDD-cost:   17
c ---[1141]---> BDD-cost:   17
c ---[1140]---> BDD-cost:   17
c ---[1139]---> BDD-cost:   17
c ---[1138]---> BDD-cost:   17
c ---[1136]---> BDD-cost:    0
c ---[1135]---> BDD-cost:   17
c ---[1134]---> BDD-cost:   17
c ---[1133]---> BDD-cost:   17
c ---[1132]---> BDD-cost:   17
c ---[1131]---> BDD-cost:   17
c ---[1130]---> BDD-cost:   17
c ---[1129]---> BDD-cost:   17
c ---[1128]---> BDD-cost:   17
c ---[1127]---> BDD-cost:   17
c ---[1126]---> BDD-cost:   17
c ---[1124]---> BDD-cost:    0
c ---[1123]---> BDD-cost:   17
c ---[1122]---> BDD-cost:   17
c ---[1121]---> BDD-cost:   17
c ---[1120]---> BDD-cost:   17
c ---[1119]---> BDD-cost:   17
c ---[1118]---> BDD-cost:   17
c ---[1117]---> BDD-cost:   17
c ---[1116]---> BDD-cost:   17
c ---[1115]---> BDD-cost:   17
c ---[1114]---> BDD-cost:   23
c ---[1112]---> BDD-cost:    0
c ---[1111]---> BDD-cost:   23
c ---[1110]---> BDD-cost:   23
c ---[1109]---> BDD-cost:   23
c ---[1108]---> BDD-cost:   23
c ---[1107]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   23
c ---[1105]---> BDD-cost:   23
c ---[1104]---> BDD-cost:   18
c ---[1103]---> BDD-cost:   18
c ---[1102]---> BDD-cost:   18
c ---[1100]---> BDD-cost:    0
c ---[1099]---> BDD-cost:   18
c ---[1098]---> BDD-cost:   18
c ---[1097]---> BDD-cost:   18
c ---[1096]---> BDD-cost:   18
c ---[1095]---> BDD-cost:   18
c ---[1094]---> BDD-cost:   17
c ---[1093]---> BDD-cost:   17
c ---[1092]---> BDD-cost:   17
c ---[1091]---> BDD-cost:   17
c ---[1090]---> BDD-cost:   17
c ---[1088]---> BDD-cost:    0
c ---[1087]---> BDD-cost:   17
c ---[1086]---> BDD-cost:   17
c ---[1085]---> BDD-cost:   17
c ---[1083]---> BDD-cost:    0
c ---[1081]---> BDD-cost:    0
c ---[1079]---> BDD-cost:    0
c ---[1077]---> BDD-cost:    0
c ---[1075]---> BDD-cost:    0
c ---[1073]---> BDD-cost:    0
c ---[1071]---> BDD-cost:    0
c ---[1069]---> BDD-cost:    0
c ---[1067]---> BDD-cost:    0
c ---[1065]---> BDD-cost:    0
c ---[1063]---> BDD-cost:    0
c ---[1061]---> BDD-cost:    0
c ---[1059]---> BDD-cost:    0
c ---[1057]---> BDD-cost:    0
c ---[1055]---> BDD-cost:    0
c ---[1054]---> BDD-cost:   25
c ---[1053]---> BDD-cost:   25
c ---[1052]---> BDD-cost:   25
c ---[1051]---> BDD-cost:   25
c ---[1050]---> BDD-cost:   25
c ---[1049]---> BDD-cost:   25
c ---[1048]---> BDD-cost:   25
c ---[1046]---> BDD-cost:    0
c ---[1045]---> BDD-cost:   25
c ---[1044]---> BDD-cost:   34
c ---[1043]---> BDD-cost:   34
c ---[1042]---> BDD-cost:   34
c ---[1041]---> BDD-cost:   34
c ---[1040]---> BDD-cost:   34
c ---[1039]---> BDD-cost:   34
c ---[1038]---> BDD-cost:   34
c ---[1037]---> BDD-cost:   34
c ---[1036]---> BDD-cost:   34
c ---[1034]---> BDD-cost:    0
c ---[1033]---> BDD-cost:   34
c ---[1032]---> BDD-cost:   34
c ---[1031]---> BDD-cost:   34
c ---[1030]---> BDD-cost:   34
c ---[1029]---> BDD-cost:   34
c ---[1028]---> BDD-cost:   34
c ---[1027]---> BDD-cost:   34
c ---[1026]---> BDD-cost:   25
c ---[1025]---> BDD-cost:   25
c ---[1024]---> BDD-cost:   25
c ---[1022]---> BDD-cost:    0
c ---[1021]---> BDD-cost:   25
c ---[1020]---> BDD-cost:   25
c ---[1019]---> BDD-cost:   25
c ---[1018]---> BDD-cost:   25
c ---[1017]---> BDD-cost:   25
c ---[1016]---> BDD-cost:   28
c ---[1015]---> BDD-cost:   28
c ---[1014]---> BDD-cost:   28
c ---[1013]---> BDD-cost:   28
c ---[1012]---> BDD-cost:   28
c ---[1010]---> BDD-cost:    0
c ---[1009]---> BDD-cost:   28
c ---[1008]---> BDD-cost:   28
c ---[1007]---> BDD-cost:   28
c ---[1006]---> BDD-cost:   37
c ---[1005]---> BDD-cost:   37
c ---[1004]---> BDD-cost:   37
c ---[1003]---> BDD-cost:   37
c ---[1002]---> BDD-cost:   37
c ---[1001]---> BDD-cost:   37
c ---[1000]---> BDD-cost:   37
c ---[ 998]---> BDD-cost:    0
c ---[ 997]---> BDD-cost:   37
c ---[ 996]---> BDD-cost:   28
c ---[ 995]---> BDD-cost:   28
c ---[ 994]---> BDD-cost:   28
c ---[ 993]---> BDD-cost:   28
c ---[ 992]---> BDD-cost:   28
c ---[ 991]---> BDD-cost:   28
c ---[ 990]---> BDD-cost:   28
c ---[ 989]---> BDD-cost:   28
c ---[ 988]---> BDD-cost:   34
c ---[ 986]---> BDD-cost:    0
c ---[ 985]---> BDD-cost:   34
c ---[ 984]---> BDD-cost:   34
c ---[ 983]---> BDD-cost:   34
c ---[ 982]---> BDD-cost:   34
c ---[ 981]---> BDD-cost:   34
c ---[ 980]---> BDD-cost:   34
c ---[ 979]---> BDD-cost:   34
c ---[ 978]---> BDD-cost:   43
c ---[ 977]---> BDD-cost:   43
c ---[ 976]---> BDD-cost:   43
c ---[ 974]---> BDD-cost:    0
c ---[ 972]---> BDD-cost:    0
c ---[ 971]---> BDD-cost:   43
c ---[ 970]---> BDD-cost:   43
c ---[ 969]---> BDD-cost:   43
c ---[ 968]---> BDD-cost:   43
c ---[ 967]---> BDD-cost:   43
c ---[ 966]---> BDD-cost:   34
c ---[ 965]---> BDD-cost:   34
c ---[ 964]---> BDD-cost:   34
c ---[ 963]---> BDD-cost:   34
c ---[ 962]---> BDD-cost:   34
c ---[ 960]---> BDD-cost:    0
c ---[ 959]---> BDD-cost:   34
c ---[ 958]---> BDD-cost:   34
c ---[ 957]---> BDD-cost:   34
c ---[ 956]---> BDD-cost:   25
c ---[ 955]---> BDD-cost:   25
c ---[ 954]---> BDD-cost:   25
c ---[ 953]---> BDD-cost:   25
c ---[ 952]---> BDD-cost:   25
c ---[ 951]---> BDD-cost:   25
c ---[ 950]---> BDD-cost:   25
c ---[ 948]---> BDD-cost:    0
c ---[ 947]---> BDD-cost:   25
c ---[ 946]---> BDD-cost:   25
c ---[ 945]---> BDD-cost:   25
c ---[ 944]---> BDD-cost:   25
c ---[ 943]---> BDD-cost:   25
c ---[ 942]---> BDD-cost:   25
c ---[ 941]---> BDD-cost:   25
c ---[ 940]---> BDD-cost:   25
c ---[ 939]---> BDD-cost:   25
c ---[ 938]---> BDD-cost:   34
c ---[ 936]---> BDD-cost:    0
c ---[ 935]---> BDD-cost:   34
c ---[ 934]---> BDD-cost:   34
c ---[ 933]---> BDD-cost:   34
c ---[ 932]---> BDD-cost:   34
c ---[ 931]---> BDD-cost:   34
c ---[ 930]---> BDD-cost:   34
c ---[ 929]---> BDD-cost:   34
c ---[ 928]---> BDD-cost:   25
c ---[ 927]---> BDD-cost:   25
c ---[ 926]---> BDD-cost:   25
c ---[ 924]---> BDD-cost:    0
c ---[ 923]---> BDD-cost:   25
c ---[ 922]---> BDD-cost:   25
c ---[ 921]---> BDD-cost:   25
c ---[ 920]---> BDD-cost:   25
c ---[ 919]---> BDD-cost:   25
c ---[ 918]---> BDD-cost:   28
c ---[ 917]---> BDD-cost:   28
c ---[ 916]---> BDD-cost:   28
c ---[ 915]---> BDD-cost:   28
c ---[ 914]---> BDD-cost:   28
c ---[ 912]---> BDD-cost:    0
c ---[ 911]---> BDD-cost:   28
c ---[ 910]---> BDD-cost:   28
c ---[ 909]---> BDD-cost:   28
c ---[ 908]---> BDD-cost:   25
c ---[ 907]---> BDD-cost:   25
c ---[ 906]---> BDD-cost:   25
c ---[ 905]---> BDD-cost:   25
c ---[ 904]---> BDD-cost:   25
c ---[ 903]---> BDD-cost:   25
c ---[ 902]---> BDD-cost:   25
c ---[ 900]---> BDD-cost:    0
c ---[ 899]---> BDD-cost:   25
c ---[ 898]---> BDD-cost:   25
c ---[ 897]---> BDD-cost:   25
c ---[ 896]---> BDD-cost:   25
c ---[ 895]---> BDD-cost:   25
c ---[ 894]---> BDD-cost:   25
c ---[ 893]---> BDD-cost:   25
c ---[ 892]---> BDD-cost:   25
c ---[ 891]---> BDD-cost:   25
c ---[ 890]---> BDD-cost:   34
c ---[ 888]---> BDD-cost:    0
c ---[ 887]---> BDD-cost:   34
c ---[ 886]---> BDD-cost:   34
c ---[ 885]---> BDD-cost:   34
c ---[ 884]---> BDD-cost:   34
c ---[ 883]---> BDD-cost:   34
c ---[ 882]---> BDD-cost:   34
c ---[ 881]---> BDD-cost:   34
c ---[ 880]---> BDD-cost:   25
c ---[ 879]---> BDD-cost:   25
c ---[ 878]---> BDD-cost:   25
c ---[ 876]---> BDD-cost:    0
c ---[ 875]---> BDD-cost:   25
c ---[ 874]---> BDD-cost:   25
c ---[ 873]---> BDD-cost:   25
c ---[ 872]---> BDD-cost:   25
c ---[ 871]---> BDD-cost:   25
c ---[ 870]---> BDD-cost:   31
c ---[ 869]---> BDD-cost:   31
c ---[ 868]---> BDD-cost:   31
c ---[ 867]---> BDD-cost:   31
c ---[ 866]---> BDD-cost:   31
c ---[ 864]---> BDD-cost:    0
c ---[ 863]---> BDD-cost:   31
c ---[ 862]---> BDD-cost:   31
c ---[ 861]---> BDD-cost:   31
c ---[ 860]---> BDD-cost:   25
c ---[ 859]---> BDD-cost:   25
c ---[ 858]---> BDD-cost:   25
c ---[ 857]---> BDD-cost:   25
c ---[ 856]---> BDD-cost:   25
c ---[ 855]---> BDD-cost:   25
c ---[ 854]---> BDD-cost:   25
c ---[ 852]---> BDD-cost:    0
c ---[ 850]---> BDD-cost:    0
c ---[ 849]---> BDD-cost:   25
c ---[ 848]---> BDD-cost:   25
c ---[ 847]---> BDD-cost:   25
c ---[ 846]---> BDD-cost:   25
c ---[ 845]---> BDD-cost:   25
c ---[ 844]---> BDD-cost:   25
c ---[ 843]---> BDD-cost:   25
c ---[ 842]---> BDD-cost:   25
c ---[ 841]---> BDD-cost:   25
c ---[ 840]---> BDD-cost:   25
c ---[ 838]---> BDD-cost:    0
c ---[ 837]---> BDD-cost:   25
c ---[ 836]---> BDD-cost:   25
c ---[ 835]---> BDD-cost:   25
c ---[ 834]---> BDD-cost:   25
c ---[ 833]---> BDD-cost:   25
c ---[ 832]---> BDD-cost:   25
c ---[ 831]---> BDD-cost:   25
c ---[ 830]---> BDD-cost:   34
c ---[ 829]---> BDD-cost:   34
c ---[ 828]---> BDD-cost:   34
c ---[ 826]---> BDD-cost:    0
c ---[ 825]---> BDD-cost:   34
c ---[ 824]---> BDD-cost:   34
c ---[ 823]---> BDD-cost:   34
c ---[ 822]---> BDD-cost:   34
c ---[ 821]---> BDD-cost:   34
c ---[ 820]---> BDD-cost:   25
c ---[ 819]---> BDD-cost:   25
c ---[ 818]---> BDD-cost:   25
c ---[ 817]---> BDD-cost:   25
c ---[ 816]---> BDD-cost:   25
c ---[ 814]---> BDD-cost:    0
c ---[ 813]---> BDD-cost:   25
c ---[ 812]---> BDD-cost:   25
c ---[ 811]---> BDD-cost:   25
c ---[ 810]---> BDD-cost:   31
c ---[ 809]---> BDD-cost:   31
c ---[ 808]---> BDD-cost:   31
c ---[ 807]---> BDD-cost:   31
c ---[ 806]---> BDD-cost:   31
c ---[ 805]---> BDD-cost:   31
c ---[ 804]---> BDD-cost:   31
c ---[ 802]---> BDD-cost:    0
c ---[ 801]---> BDD-cost:   31
c ---[ 800]---> BDD-cost:   25
c ---[ 799]---> BDD-cost:   25
c ---[ 798]---> BDD-cost:   25
c ---[ 797]---> BDD-cost:   25
c ---[ 796]---> BDD-cost:   25
c ---[ 795]---> BDD-cost:   25
c ---[ 794]---> BDD-cost:   25
c ---[ 793]---> BDD-cost:   25
c ---[ 792]---> BDD-cost:   25
c ---[ 790]---> BDD-cost:    0
c ---[ 789]---> BDD-cost:   25
c ---[ 788]---> BDD-cost:   25
c ---[ 787]---> BDD-cost:   25
c ---[ 786]---> BDD-cost:   25
c ---[ 785]---> BDD-cost:   25
c ---[ 784]---> BDD-cost:   25
c ---[ 783]---> BDD-cost:   25
c ---[ 782]---> BDD-cost:   34
c ---[ 781]---> BDD-cost:   34
c ---[ 780]---> BDD-cost:   34
c ---[ 778]---> BDD-cost:    0
c ---[ 777]---> BDD-cost:   34
c ---[ 776]---> BDD-cost:   34
c ---[ 775]---> BDD-cost:   34
c ---[ 774]---> BDD-cost:   34
c ---[ 773]---> BDD-cost:   34
c ---[ 772]---> BDD-cost:   34
c ---[ 771]---> BDD-cost:   34
c ---[ 770]---> BDD-cost:   34
c ---[ 769]---> BDD-cost:   34
c ---[ 768]---> BDD-cost:   34
c ---[ 766]---> BDD-cost:    0
c ---[ 765]---> BDD-cost:   34
c ---[ 764]---> BDD-cost:   34
c ---[ 763]---> BDD-cost:   34
c ---[ 762]---> BDD-cost:   25
c ---[ 761]---> BDD-cost:   25
c ---[ 760]---> BDD-cost:   25
c ---[ 759]---> BDD-cost:   25
c ---[ 758]---> BDD-cost:   25
c ---[ 757]---> BDD-cost:   25
c ---[ 756]---> BDD-cost:   25
c ---[ 754]---> BDD-cost:    0
c ---[ 753]---> BDD-cost:   25
c ---[ 752]---> BDD-cost:   34
c ---[ 751]---> BDD-cost:   34
c ---[ 750]---> BDD-cost:   34
c ---[ 749]---> BDD-cost:   34
c ---[ 748]---> BDD-cost:   34
c ---[ 747]---> BDD-cost:   34
c ---[ 746]---> BDD-cost:   34
c ---[ 745]---> BDD-cost:   34
c ---[ 744]---> BDD-cost:   43
c ---[ 742]---> BDD-cost:    0
c ---[ 741]---> BDD-cost:   43
c ---[ 740]---> BDD-cost:   43
c ---[ 739]---> BDD-cost:   43
c ---[ 738]---> BDD-cost:   43
c ---[ 737]---> BDD-cost:   43
c ---[ 736]---> BDD-cost:   43
c ---[ 735]---> BDD-cost:   43
c ---[ 734]---> BDD-cost:   34
c ---[ 733]---> BDD-cost:   34
c ---[ 732]---> BDD-cost:   34
c ---[ 730]---> BDD-cost:    0
c ---[ 728]---> BDD-cost:    0
c ---[ 727]---> BDD-cost:   34
c ---[ 726]---> BDD-cost:   34
c ---[ 725]---> BDD-cost:   34
c ---[ 724]---> BDD-cost:   34
c ---[ 723]---> BDD-cost:   34
c ---[ 722]---> BDD-cost:   34
c ---[ 721]---> BDD-cost:   34
c ---[ 720]---> BDD-cost:   34
c ---[ 719]---> BDD-cost:   34
c ---[ 718]---> BDD-cost:   34
c ---[ 716]---> BDD-cost:    0
c ---[ 715]---> BDD-cost:   34
c ---[ 714]---> BDD-cost:   34
c ---[ 713]---> BDD-cost:   34
c ---[ 712]---> BDD-cost:   34
c ---[ 711]---> BDD-cost:   34
c ---[ 710]---> BDD-cost:   34
c ---[ 709]---> BDD-cost:   34
c ---[ 708]---> BDD-cost:   34
c ---[ 707]---> BDD-cost:   34
c ---[ 706]---> BDD-cost:   34
c ---[ 704]---> BDD-cost:    0
c ---[ 703]---> BDD-cost:   34
c ---[ 702]---> BDD-cost:   25
c ---[ 701]---> BDD-cost:   25
c ---[ 700]---> BDD-cost:   25
c ---[ 699]---> BDD-cost:   25
c ---[ 698]---> BDD-cost:   25
c ---[ 697]---> BDD-cost:   25
c ---[ 696]---> BDD-cost:   25
c ---[ 695]---> BDD-cost:   25
c ---[ 694]---> BDD-cost:   28
c ---[ 692]---> BDD-cost:    0
c ---[ 691]---> BDD-cost:   28
c ---[ 690]---> BDD-cost:   28
c ---[ 689]---> BDD-cost:   28
c ---[ 688]---> BDD-cost:   28
c ---[ 687]---> BDD-cost:   28
c ---[ 686]---> BDD-cost:   28
c ---[ 685]---> BDD-cost:   28
c ---[ 684]---> BDD-cost:   37
c ---[ 683]---> BDD-cost:   37
c ---[ 682]---> BDD-cost:   37
c ---[ 680]---> BDD-cost:    0
c ---[ 679]---> BDD-cost:   37
c ---[ 678]---> BDD-cost:   37
c ---[ 677]---> BDD-cost:   37
c ---[ 676]---> BDD-cost:   37
c ---[ 675]---> BDD-cost:   37
c ---[ 674]---> BDD-cost:   31
c ---[ 673]---> BDD-cost:   31
c ---[ 672]---> BDD-cost:   31
c ---[ 671]---> BDD-cost:   31
c ---[ 670]---> BDD-cost:   31
c ---[ 668]---> BDD-cost:    0
c ---[ 667]---> BDD-cost:   31
c ---[ 666]---> BDD-cost:   31
c ---[ 665]---> BDD-cost:   31
c ---[ 664]---> BDD-cost:   37
c ---[ 663]---> BDD-cost:   37
c ---[ 662]---> BDD-cost:   37
c ---[ 661]---> BDD-cost:   37
c ---[ 660]---> BDD-cost:   37
c ---[ 659]---> BDD-cost:   37
c ---[ 658]---> BDD-cost:   37
c ---[ 656]---> BDD-cost:    0
c ---[ 655]---> BDD-cost:   37
c ---[ 654]---> BDD-cost:   25
c ---[ 653]---> BDD-cost:   25
c ---[ 652]---> BDD-cost:   25
c ---[ 651]---> BDD-cost:   25
c ---[ 650]---> BDD-cost:   25
c ---[ 649]---> BDD-cost:   25
c ---[ 648]---> BDD-cost:   25
c ---[ 647]---> BDD-cost:   25
c ---[ 646]---> BDD-cost:   25
c ---[ 644]---> BDD-cost:    0
c ---[ 643]---> BDD-cost:   25
c ---[ 642]---> BDD-cost:   25
c ---[ 641]---> BDD-cost:   25
c ---[ 640]---> BDD-cost:   25
c ---[ 639]---> BDD-cost:   25
c ---[ 638]---> BDD-cost:   25
c ---[ 637]---> BDD-cost:   25
c ---[ 636]---> BDD-cost:   28
c ---[ 635]---> BDD-cost:   28
c ---[ 634]---> BDD-cost:   28
c ---[ 632]---> BDD-cost:    0
c ---[ 631]---> BDD-cost:   28
c ---[ 630]---> BDD-cost:   28
c ---[ 629]---> BDD-cost:   28
c ---[ 628]---> BDD-cost:   28
c ---[ 627]---> BDD-cost:   28
c ---[ 626]---> BDD-cost:   37
c ---[ 625]---> BDD-cost:   37
c ---[ 624]---> BDD-cost:   37
c ---[ 623]---> BDD-cost:   37
c ---[ 622]---> BDD-cost:   37
c ---[ 620]---> BDD-cost:    0
c ---[ 619]---> BDD-cost:   37
c ---[ 618]---> BDD-cost:   37
c ---[ 617]---> BDD-cost:   37
c ---[ 616]---> BDD-cost:   25
c ---[ 615]---> BDD-cost:   25
c ---[ 614]---> BDD-cost:   25
c ---[ 613]---> BDD-cost:   25
c ---[ 612]---> BDD-cost:   25
c ---[ 611]---> BDD-cost:   25
c ---[ 610]---> BDD-cost:   25
c ---[ 608]---> BDD-cost:    0
c ---[ 606]---> BDD-cost:    0
c ---[ 605]---> BDD-cost:   25
c ---[ 604]---> BDD-cost:   25
c ---[ 603]---> BDD-cost:   25
c ---[ 602]---> BDD-cost:   25
c ---[ 601]---> BDD-cost:   25
c ---[ 600]---> BDD-cost:   25
c ---[ 599]---> BDD-cost:   25
c ---[ 598]---> BDD-cost:   25
c ---[ 597]---> BDD-cost:   25
c ---[ 596]---> BDD-cost:   34
c ---[ 594]---> BDD-cost:    0
c ---[ 593]---> BDD-cost:   34
c ---[ 592]---> BDD-cost:   34
c ---[ 591]---> BDD-cost:   34
c ---[ 590]---> BDD-cost:   34
c ---[ 589]---> BDD-cost:   34
c ---[ 588]---> BDD-cost:   34
c ---[ 587]---> BDD-cost:   34
c ---[ 586]---> BDD-cost:   25
c ---[ 585]---> BDD-cost:   25
c ---[ 584]---> BDD-cost:   25
c ---[ 582]---> BDD-cost:    0
c ---[ 581]---> BDD-cost:   25
c ---[ 580]---> BDD-cost:   25
c ---[ 579]---> BDD-cost:   25
c ---[ 578]---> BDD-cost:   25
c ---[ 577]---> BDD-cost:   25
c ---[ 576]---> BDD-cost:   31
c ---[ 575]---> BDD-cost:   31
c ---[ 574]---> BDD-cost:   31
c ---[ 573]---> BDD-cost:   31
c ---[ 572]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:    0
c ---[ 569]---> BDD-cost:   31
c ---[ 568]---> BDD-cost:   31
c ---[ 567]---> BDD-cost:   31
c ---[ 566]---> BDD-cost:   25
c ---[ 565]---> BDD-cost:   25
c ---[ 564]---> BDD-cost:   25
c ---[ 563]---> BDD-cost:   25
c ---[ 562]---> BDD-cost:   25
c ---[ 561]---> BDD-cost:   25
c ---[ 560]---> BDD-cost:   25
c ---[ 558]---> BDD-cost:    0
c ---[ 557]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:   25
c ---[ 555]---> BDD-cost:   25
c ---[ 554]---> BDD-cost:   25
c ---[ 553]---> BDD-cost:   25
c ---[ 552]---> BDD-cost:   25
c ---[ 551]---> BDD-cost:   25
c ---[ 550]---> BDD-cost:   25
c ---[ 549]---> BDD-cost:   25
c ---[ 548]---> BDD-cost:   25
c ---[ 546]---> BDD-cost:    0
c ---[ 545]---> BDD-cost:   25
c ---[ 544]---> BDD-cost:   25
c ---[ 543]---> BDD-cost:   25
c ---[ 542]---> BDD-cost:   25
c ---[ 541]---> BDD-cost:   25
c ---[ 540]---> BDD-cost:   25
c ---[ 539]---> BDD-cost:   25
c ---[ 538]---> BDD-cost:   34
c ---[ 537]---> BDD-cost:   34
c ---[ 536]---> BDD-cost:   34
c ---[ 534]---> BDD-cost:    0
c ---[ 533]---> BDD-cost:   34
c ---[ 532]---> BDD-cost:   34
c ---[ 531]---> BDD-cost:   34
c ---[ 530]---> BDD-cost:   34
c ---[ 529]---> BDD-cost:   34
c ---[ 528]---> BDD-cost:   28
c ---[ 527]---> BDD-cost:   28
c ---[ 526]---> BDD-cost:   28
c ---[ 525]---> BDD-cost:   28
c ---[ 524]---> BDD-cost:   28
c ---[ 522]---> BDD-cost:    0
c ---[ 521]---> BDD-cost:   28
c ---[ 520]---> BDD-cost:   28
c ---[ 519]---> BDD-cost:   28
c ---[ 518]---> BDD-cost:   25
c ---[ 517]---> BDD-cost:   25
c ---[ 516]---> BDD-cost:   25
c ---[ 515]---> BDD-cost:   25
c ---[ 514]---> BDD-cost:   25
c ---[ 513]---> BDD-cost:   25
c ---[ 512]---> BDD-cost:   25
c ---[ 510]---> BDD-cost:    0
c ---[ 509]---> BDD-cost:   25
c ---[ 508]---> BDD-cost:   25
c ---[ 507]---> BDD-cost:   25
c ---[ 506]---> BDD-cost:   25
c ---[ 505]---> BDD-cost:   25
c ---[ 504]---> BDD-cost:   25
c ---[ 503]---> BDD-cost:   25
c ---[ 502]---> BDD-cost:   25
c ---[ 501]---> BDD-cost:   25
c ---[ 500]---> BDD-cost:   34
c ---[ 498]---> BDD-cost:    0
c ---[ 497]---> BDD-cost:   34
c ---[ 496]---> BDD-cost:   34
c ---[ 495]---> BDD-cost:   34
c ---[ 494]---> BDD-cost:   34
c ---[ 493]---> BDD-cost:   34
c ---[ 492]---> BDD-cost:   34
c ---[ 491]---> BDD-cost:   34
c ---[ 490]---> BDD-cost:   25
c ---[ 489]---> BDD-cost:   25
c ---[ 488]---> BDD-cost:   25
c ---[ 486]---> BDD-cost:    0
c ---[ 484]---> BDD-cost:    0
c ---[ 483]---> BDD-cost:   25
c ---[ 482]---> BDD-cost:   25
c ---[ 481]---> BDD-cost:   25
c ---[ 480]---> BDD-cost:   25
c ---[ 479]---> BDD-cost:   25
c ---[ 478]---> BDD-cost:   28
c ---[ 477]---> BDD-cost:   28
c ---[ 476]---> BDD-cost:   28
c ---[ 475]---> BDD-cost:   28
c ---[ 474]---> BDD-cost:   28
c ---[ 472]---> BDD-cost:    0
c ---[ 471]---> BDD-cost:   28
c ---[ 470]---> BDD-cost:   28
c ---[ 469]---> BDD-cost:   28
c ---[ 468]---> BDD-cost:   25
c ---[ 467]---> BDD-cost:   25
c ---[ 466]---> BDD-cost:   25
c ---[ 465]---> BDD-cost:   25
c ---[ 464]---> BDD-cost:   25
c ---[ 463]---> BDD-cost:   25
c ---[ 462]---> BDD-cost:   25
c ---[ 460]---> BDD-cost:    0
c ---[ 459]---> BDD-cost:   25
c ---[ 458]---> BDD-cost:   25
c ---[ 457]---> BDD-cost:   25
c ---[ 456]---> BDD-cost:   25
c ---[ 455]---> BDD-cost:   25
c ---[ 454]---> BDD-cost:   25
c ---[ 453]---> BDD-cost:   25
c ---[ 452]---> BDD-cost:   25
c ---[ 451]---> BDD-cost:   25
c ---[ 450]---> BDD-cost:   25
c ---[ 448]---> BDD-cost:    0
c ---[ 447]---> BDD-cost:   25
c ---[ 446]---> BDD-cost:   25
c ---[ 445]---> BDD-cost:   25
c ---[ 444]---> BDD-cost:   25
c ---[ 443]---> BDD-cost:   25
c ---[ 442]---> BDD-cost:   25
c ---[ 441]---> BDD-cost:   25
c ---[ 440]---> BDD-cost:   34
c ---[ 439]---> BDD-cost:   34
c ---[ 438]---> BDD-cost:   34
c ---[ 436]---> BDD-cost:    0
c ---[ 435]---> BDD-cost:   34
c ---[ 434]---> BDD-cost:   34
c ---[ 433]---> BDD-cost:   34
c ---[ 432]---> BDD-cost:   34
c ---[ 431]---> BDD-cost:   34
c ---[ 430]---> BDD-cost:   28
c ---[ 429]---> BDD-cost:   28
c ---[ 428]---> BDD-cost:   28
c ---[ 427]---> BDD-cost:   28
c ---[ 426]---> BDD-cost:   28
c ---[ 424]---> BDD-cost:    0
c ---[ 423]---> BDD-cost:   28
c ---[ 422]---> BDD-cost:   28
c ---[ 421]---> BDD-cost:   28
c ---[ 420]---> BDD-cost:   25
c ---[ 419]---> BDD-cost:   25
c ---[ 418]---> BDD-cost:   25
c ---[ 417]---> BDD-cost:   25
c ---[ 416]---> BDD-cost:   25
c ---[ 415]---> BDD-cost:   25
c ---[ 414]---> BDD-cost:   25
c ---[ 412]---> BDD-cost:    0
c ---[ 411]---> BDD-cost:   25
c ---[ 410]---> Adder-cost: 4116   maxlim: 351099   bits: 20/19
c ---[ 409]---> Adder-cost: 4116   maxlim: 351099   bits: 20/19
c ---[ 408]---> Adder-cost: 4116   maxlim: 351099   bits: 20/19
c ---[ 407]---> Adder-cost: 4116   maxlim: 351099   bits: 20/19
c ---[ 406]---> BDD-cost:   17
c ---[ 405]---> BDD-cost:   17
c ---[ 404]---> BDD-cost:   17
c ---[ 403]---> BDD-cost:   17
c ---[ 402]---> BDD-cost:   17
c ---[ 400]---> BDD-cost:    0
c ---[ 399]---> BDD-cost:   17
c ---[ 398]---> BDD-cost:   17
c ---[ 397]---> BDD-cost:   17
c ---[ 396]---> BDD-cost:   21
c ---[ 395]---> BDD-cost:   21
c ---[ 394]---> BDD-cost:   21
c ---[ 393]---> BDD-cost:   21
c ---[ 392]---> BDD-cost:   21
c ---[ 391]---> BDD-cost:   21
c ---[ 390]---> BDD-cost:   21
c ---[ 388]---> BDD-cost:    0
c ---[ 387]---> BDD-cost:   21
c ---[ 386]---> BDD-cost:   22
c ---[ 385]---> BDD-cost:   22
c ---[ 384]---> BDD-cost:   22
c ---[ 383]---> BDD-cost:   22
c ---[ 382]---> BDD-cost:   22
c ---[ 381]---> BDD-cost:   22
c ---[ 380]---> BDD-cost:   22
c ---[ 379]---> BDD-cost:   22
c ---[ 378]---> BDD-cost:   17
c ---[ 376]---> BDD-cost:    0
c ---[ 375]---> BDD-cost:   17
c ---[ 374]---> BDD-cost:   17
c ---[ 373]---> BDD-cost:   17
c ---[ 372]---> BDD-cost:   17
c ---[ 371]---> BDD-cost:   17
c ---[ 370]---> BDD-cost:   17
c ---[ 369]---> BDD-cost:   17
c ---[ 368]---> BDD-cost:   18
c ---[ 367]---> BDD-cost:   18
c ---[ 366]---> BDD-cost:   18
c ---[ 364]---> BDD-cost:    0
c ---[ 362]---> BDD-cost:    0
c ---[ 361]---> BDD-cost:   18
c ---[ 360]---> BDD-cost:   18
c ---[ 359]---> BDD-cost:   18
c ---[ 358]---> BDD-cost:   18
c ---[ 357]---> BDD-cost:   18
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:   23
c ---[ 354]---> BDD-cost:   23
c ---[ 353]---> BDD-cost:   23
c ---[ 352]---> BDD-cost:   23
c ---[ 350]---> BDD-cost:    0
c ---[ 349]---> BDD-cost:   23
c ---[ 348]---> BDD-cost:   23
c ---[ 347]---> BDD-cost:   23
c ---[ 346]---> BDD-cost:   18
c ---[ 345]---> BDD-cost:   18
c ---[ 344]---> BDD-cost:   18
c ---[ 343]---> BDD-cost:   18
c ---[ 342]---> BDD-cost:   18
c ---[ 341]---> BDD-cost:   18
c ---[ 340]---> BDD-cost:   18
c ---[ 338]---> BDD-cost:    0
c ---[ 337]---> BDD-cost:   18
c ---[ 336]---> BDD-cost:   22
c ---[ 335]---> BDD-cost:   22
c ---[ 334]---> BDD-cost:   22
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   22
c ---[ 331]---> BDD-cost:   22
c ---[ 330]---> BDD-cost:   22
c ---[ 329]---> BDD-cost:   22
c ---[ 328]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:    0
c ---[ 325]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   27
c ---[ 322]---> BDD-cost:   27
c ---[ 321]---> BDD-cost:   27
c ---[ 320]---> BDD-cost:   27
c ---[ 319]---> BDD-cost:   27
c ---[ 318]---> BDD-cost:   19
c ---[ 317]---> BDD-cost:   19
c ---[ 316]---> BDD-cost:   19
c ---[ 314]---> BDD-cost:    0
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   19
c ---[ 311]---> BDD-cost:   19
c ---[ 310]---> BDD-cost:   19
c ---[ 309]---> BDD-cost:   19
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 305]---> BDD-cost:   17
c ---[ 304]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:    0
c ---[ 301]---> BDD-cost:   17
c ---[ 300]---> BDD-cost:   17
c ---[ 299]---> BDD-cost:   17
c ---[ 298]---> BDD-cost:   17
c ---[ 297]---> BDD-cost:   17
c ---[ 296]---> BDD-cost:   17
c ---[ 295]---> BDD-cost:   17
c ---[ 294]---> BDD-cost:   17
c ---[ 293]---> BDD-cost:   17
c ---[ 292]---> BDD-cost:   17
c ---[ 290]---> BDD-cost:    0
c ---[ 289]---> BDD-cost:   17
c ---[ 288]---> BDD-cost:   21
c ---[ 287]---> BDD-cost:   21
c ---[ 286]---> BDD-cost:   21
c ---[ 285]---> BDD-cost:   21
c ---[ 284]---> BDD-cost:   21
c ---[ 283]---> BDD-cost:   21
c ---[ 282]---> BDD-cost:   21
c ---[ 281]---> BDD-cost:   21
c ---[ 280]---> BDD-cost:   17
c ---[ 278]---> BDD-cost:    0
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   17
c ---[ 275]---> BDD-cost:   17
c ---[ 274]---> BDD-cost:   17
c ---[ 273]---> BDD-cost:   17
c ---[ 272]---> BDD-cost:   17
c ---[ 271]---> BDD-cost:   17
c ---[ 270]---> BDD-cost:   18
c ---[ 269]---> BDD-cost:   18
c ---[ 268]---> BDD-cost:   18
c ---[ 266]---> BDD-cost:    0
c ---[ 265]---> BDD-cost:   18
c ---[ 264]---> BDD-cost:   18
c ---[ 263]---> BDD-cost:   18
c ---[ 262]---> BDD-cost:   18
c ---[ 261]---> BDD-cost:   18
c ---[ 260]---> BDD-cost:   17
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   17
c ---[ 257]---> BDD-cost:   17
c ---[ 256]---> BDD-cost:   17
c ---[ 254]---> BDD-cost:    0
c ---[ 253]---> BDD-cost:   17
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:   17
c ---[ 250]---> BDD-cost:   17
c ---[ 249]---> BDD-cost:   17
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:   17
c ---[ 245]---> BDD-cost:   17
c ---[ 244]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:    0
c ---[ 240]---> BDD-cost:    0
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   22
c ---[ 237]---> BDD-cost:   22
c ---[ 236]---> BDD-cost:   22
c ---[ 235]---> BDD-cost:   22
c ---[ 234]---> BDD-cost:   22
c ---[ 233]---> BDD-cost:   22
c ---[ 232]---> BDD-cost:   22
c ---[ 231]---> BDD-cost:   22
c ---[ 230]---> BDD-cost:   17
c ---[ 228]---> BDD-cost:    0
c ---[ 227]---> BDD-cost:   17
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   17
c ---[ 221]---> BDD-cost:   17
c ---[ 220]---> BDD-cost:   18
c ---[ 219]---> BDD-cost:   18
c ---[ 218]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:    0
c ---[ 215]---> BDD-cost:   18
c ---[ 214]---> BDD-cost:   18
c ---[ 213]---> BDD-cost:   18
c ---[ 212]---> BDD-cost:   18
c ---[ 211]---> BDD-cost:   18
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   17
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   17
c ---[ 206]---> BDD-cost:   17
c ---[ 204]---> BDD-cost:    0
c ---[ 203]---> BDD-cost:   17
c ---[ 202]---> BDD-cost:   17
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   17
c ---[ 199]---> BDD-cost:   17
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   17
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   17
c ---[ 194]---> BDD-cost:   17
c ---[ 192]---> BDD-cost:    0
c ---[ 191]---> BDD-cost:   17
c ---[ 190]---> BDD-cost:   17
c ---[ 189]---> BDD-cost:   17
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   22
c ---[ 180]---> BDD-cost:    0
c ---[ 179]---> BDD-cost:   22
c ---[ 178]---> BDD-cost:   22
c ---[ 177]---> BDD-cost:   22
c ---[ 176]---> BDD-cost:   22
c ---[ 175]---> BDD-cost:   22
c ---[ 174]---> BDD-cost:   22
c ---[ 173]---> BDD-cost:   22
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   17
c ---[ 168]---> BDD-cost:    0
c ---[ 167]---> BDD-cost:   17
c ---[ 166]---> BDD-cost:   17
c ---[ 165]---> BDD-cost:   17
c ---[ 164]---> BDD-cost:   17
c ---[ 163]---> BDD-cost:   17
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   18
c ---[ 160]---> BDD-cost:   18
c ---[ 159]---> BDD-cost:   18
c ---[ 158]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:    0
c ---[ 155]---> BDD-cost:   18
c ---[ 154]---> BDD-cost:   18
c ---[ 153]---> BDD-cost:   18
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   17
c ---[ 147]---> BDD-cost:   17
c ---[ 146]---> BDD-cost:   17
c ---[ 144]---> BDD-cost:    0
c ---[ 143]---> BDD-cost:   17
c ---[ 142]---> BDD-cost:   17
c ---[ 141]---> BDD-cost:   17
c ---[ 140]---> BDD-cost:   17
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:   17
c ---[ 137]---> BDD-cost:   17
c ---[ 136]---> BDD-cost:   17
c ---[ 135]---> BDD-cost:   17
c ---[ 134]---> BDD-cost:   21
c ---[ 132]---> BDD-cost:    0
c ---[ 131]---> BDD-cost:   21
c ---[ 130]---> BDD-cost:   21
c ---[ 129]---> BDD-cost:   21
c ---[ 128]---> BDD-cost:   21
c ---[ 127]---> BDD-cost:   21
c ---[ 126]---> BDD-cost:   21
c ---[ 125]---> BDD-cost:   21
c ---[ 124]---> BDD-cost:   23
c ---[ 123]---> BDD-cost:   23
c ---[ 122]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:    0
c ---[ 118]---> BDD-cost:    0
c ---[ 117]---> BDD-cost:   23
c ---[ 116]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   23
c ---[ 114]---> BDD-cost:   23
c ---[ 113]---> BDD-cost:   23
c ---[ 112]---> BDD-cost:   17
c ---[ 111]---> BDD-cost:   17
c ---[ 110]---> BDD-cost:   17
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:    0
c ---[ 105]---> BDD-cost:   17
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   22
c ---[ 101]---> BDD-cost:   22
c ---[ 100]---> BDD-cost:   22
c ---[  99]---> BDD-cost:   22
c ---[  98]---> BDD-cost:   22
c ---[  97]---> BDD-cost:   22
c ---[  96]---> BDD-cost:   22
c ---[  94]---> BDD-cost:    0
c ---[  93]---> BDD-cost:   22
c ---[  92]---> BDD-cost:   29
c ---[  91]---> BDD-cost:   29
c ---[  90]---> BDD-cost:   29
c ---[  89]---> BDD-cost:   29
c ---[  88]---> BDD-cost:   29
c ---[  87]---> BDD-cost:   29
c ---[  86]---> BDD-cost:   29
c ---[  85]---> BDD-cost:   29
c ---[  84]---> BDD-cost:   21
c ---[  82]---> BDD-cost:    0
c ---[  81]---> BDD-cost:   21
c ---[  80]---> BDD-cost:   21
c ---[  79]---> BDD-cost:   21
c ---[  78]---> BDD-cost:   21
c ---[  77]---> BDD-cost:   21
c ---[  76]---> BDD-cost:   21
c ---[  75]---> BDD-cost:   21
c ---[  74]---> BDD-cost:   22
c ---[  73]---> BDD-cost:   22
c ---[  72]---> BDD-cost:   22
c ---[  70]---> BDD-cost:    0
c ---[  69]---> BDD-cost:   22
c ---[  68]---> BDD-cost:   22
c ---[  67]---> BDD-cost:   22
c ---[  66]---> BDD-cost:   22
c ---[  65]---> BDD-cost:   22
c ---[  64]---> BDD-cost:   22
c ---[  63]---> BDD-cost:   22
c ---[  62]---> BDD-cost:   22
c ---[  61]---> BDD-cost:   22
c ---[  60]---> BDD-cost:   22
c ---[  58]---> BDD-cost:    0
c ---[  57]---> BDD-cost:   22
c ---[  56]---> BDD-cost:   22
c ---[  55]---> BDD-cost:   22
c ---[  54]---> BDD-cost:   17
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   17
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   17
c ---[  46]---> BDD-cost:    0
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   18
c ---[  43]---> BDD-cost:   18
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   25
c ---[  34]---> BDD-cost:    0
c ---[  33]---> BDD-cost:   25
c ---[  32]---> BDD-cost:   25
c ---[  31]---> BDD-cost:   25
c ---[  30]---> BDD-cost:   25
c ---[  29]---> BDD-cost:   25
c ---[  28]---> BDD-cost:   25
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   19
c ---[  24]---> BDD-cost:   19
c ---[  22]---> BDD-cost:    0
c ---[  21]---> BDD-cost:   19
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:   19
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   25
c ---[  15]---> BDD-cost:   25
c ---[  14]---> BDD-cost:   25
c ---[  13]---> BDD-cost:   25
c ---[  12]---> BDD-cost:   25
c ---[  10]---> BDD-cost:    0
c ---[   9]---> BDD-cost:   25
c ---[   8]---> BDD-cost:   25
c ---[   7]---> BDD-cost:   25
c ---[   6]---> BDD-cost:   17
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  157736   520368 |   52578       0        0     nan |  0.000 % |
c |       100 |  157736   520368 |   57835     100      323     3.2 | 27.808 % |
c |       251 |  157736   520368 |   63619     251     1017     4.1 | 27.808 % |
c |       476 |  157736   520368 |   69981     476     1814     3.8 | 27.808 % |
c |       813 |  157736   520368 |   76979     813     3181     3.9 | 27.808 % |
c |      1319 |  157736   520368 |   84677    1319     6135     4.7 | 27.808 % |
c |      2080 |  157736   520368 |   93145    2080     9382     4.5 | 27.808 % |
c |      3219 |  157736   520368 |  102459    3219    16345     5.1 | 27.808 % |
c |      4927 |  157736   520368 |  112705    4927    37594     7.6 | 27.808 % |
c |      7489 |  157736   520368 |  123976    7489   175263    23.4 | 27.808 % |
c |     11334 |  157736   520368 |  136373   11334   308265    27.2 | 27.808 % |
c |     17102 |  157736   520368 |  150011   17102   693489    40.6 | 27.808 % |
c |     25754 |  157736   520368 |  165012   25754  1398546    54.3 | 27.808 % |
c |     38728 |  157736   520368 |  181513   38728  2590424    66.9 | 27.808 % |
c |     58189 |  157736   520368 |  199664   58189  4206048    72.3 | 27.808 % |
c |     87381 |  157736   520368 |  219631   87381  7955989    91.0 | 27.808 % |
c |    131170 |  157736   520368 |  241594  131170  9953635    75.9 | 27.808 % |
c |    196854 |  157736   520368 |  265753  196854 16345566    83.0 | 27.808 % |
c |    295382 |  157736   520368 |  292329   24277  2301501    94.8 | 27.808 % |
c |    443171 |  157736   520368 |  321562  172066 28152579   163.6 | 27.808 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/9013/stat): 9013 (minisat+_script) R 9012 9013 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846643793 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9013/statm): 174 3 169 147 0 27 0
[pid=9013] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=9014
New process pid=9015
New process pid=9016
execve syscall for /bin/sed executable
One traced child (pid=9015) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=9016) exited with status: 0
One traced child (pid=9014) exited with status: 0
New process pid=9017
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-qiu.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.96 0.87 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 5804 0 0 0 946 25 0 0 25 0 1 0 1846643797 23183360 5192 4294967295 134512640 135094434 3221224432 3221222912 134780674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 5660 5192 145 145 0 5515 0
[pid=9017] vsize: 22640
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 24764

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.96 0.87 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 6967 0 0 0 1927 32 0 0 25 0 1 0 1846643797 27955200 6355 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 6825 6355 145 145 0 6680 0
[pid=9017] vsize: 27300
Current children cumulated CPU time (s) 19.6
Current children cumulated vsize (Kb) 29424

[startup+30.0071 s]
Raw data (loadavg): 0.95 0.96 0.87 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 8122 0 0 0 2909 40 0 0 25 0 1 0 1846643797 32776192 7510 4294967295 134512640 135094434 3221224432 3221223040 134781858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 8002 7510 145 145 0 7857 0
[pid=9017] vsize: 32008
Current children cumulated CPU time (s) 29.5
Current children cumulated vsize (Kb) 34132

[startup+40.0078 s]
Raw data (loadavg): 0.96 0.96 0.87 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 9134 0 0 0 3893 47 0 0 25 0 1 0 1846643797 36876288 8522 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 9003 8522 145 145 0 8858 0
[pid=9017] vsize: 36012
Current children cumulated CPU time (s) 39.41
Current children cumulated vsize (Kb) 38136

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.96 0.87 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 9872 0 0 0 4882 51 0 0 25 0 1 0 1846643797 39882752 9260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 9737 9260 145 145 0 9592 0
[pid=9017] vsize: 38948
Current children cumulated CPU time (s) 49.34
Current children cumulated vsize (Kb) 41072

[startup+60.0092 s]
Raw data (loadavg): 0.97 0.96 0.87 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 10672 0 0 0 5870 56 0 0 25 0 1 0 1846643797 43130880 10060 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 10530 10060 145 145 0 10385 0
[pid=9017] vsize: 42120
Current children cumulated CPU time (s) 59.27
Current children cumulated vsize (Kb) 44244

[startup+70.0098 s]
Raw data (loadavg): 0.97 0.96 0.87 1/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) T 9013 9013 16528 0 -1 0 11627 0 0 0 6853 63 0 0 25 0 1 0 1846643797 47288320 11015 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9017/statm): 11545 11015 145 145 0 11400 0
[pid=9017] vsize: 46180
Current children cumulated CPU time (s) 69.17
Current children cumulated vsize (Kb) 48304

[startup+80.0115 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 12402 0 0 0 7841 68 0 0 25 0 1 0 1846643797 50446336 11790 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 12316 11790 145 145 0 12171 0
[pid=9017] vsize: 49264
Current children cumulated CPU time (s) 79.1
Current children cumulated vsize (Kb) 51388

[startup+90.0122 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 13118 0 0 0 8830 72 0 0 25 0 1 0 1846643797 53370880 12506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 13030 12506 145 145 0 12885 0
[pid=9017] vsize: 52120
Current children cumulated CPU time (s) 89.03
Current children cumulated vsize (Kb) 54244

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 13783 0 0 0 9817 78 0 0 25 0 1 0 1846643797 56115200 13171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 13700 13171 145 145 0 13555 0
[pid=9017] vsize: 54800
Current children cumulated CPU time (s) 98.96
Current children cumulated vsize (Kb) 56924

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 14380 0 0 0 10807 82 0 0 25 0 1 0 1846643797 58544128 13768 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 14293 13768 145 145 0 14148 0
[pid=9017] vsize: 57172
Current children cumulated CPU time (s) 108.9
Current children cumulated vsize (Kb) 59296

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 14922 0 0 0 11800 85 0 0 25 0 1 0 1846643797 60739584 14310 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 14829 14310 145 145 0 14684 0
[pid=9017] vsize: 59316
Current children cumulated CPU time (s) 118.86
Current children cumulated vsize (Kb) 61440

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 15317 0 0 0 12793 88 0 0 25 0 1 0 1846643797 62353408 14705 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 15223 14705 145 145 0 15078 0
[pid=9017] vsize: 60892
Current children cumulated CPU time (s) 128.82
Current children cumulated vsize (Kb) 63016

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 15680 0 0 0 13786 90 0 0 25 0 1 0 1846643797 63844352 15068 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 15587 15068 145 145 0 15442 0
[pid=9017] vsize: 62348
Current children cumulated CPU time (s) 138.77
Current children cumulated vsize (Kb) 64472

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 16006 0 0 0 14781 93 0 0 25 0 1 0 1846643797 65208320 15394 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 15920 15394 145 145 0 15775 0
[pid=9017] vsize: 63680
Current children cumulated CPU time (s) 148.75
Current children cumulated vsize (Kb) 65804

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 16251 0 0 0 15777 95 0 0 25 0 1 0 1846643797 66207744 15639 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 16164 15639 145 145 0 16019 0
[pid=9017] vsize: 64656
Current children cumulated CPU time (s) 158.73
Current children cumulated vsize (Kb) 66780

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 16519 0 0 0 16773 97 0 0 25 0 1 0 1846643797 67387392 15907 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 16452 15907 145 145 0 16307 0
[pid=9017] vsize: 65808
Current children cumulated CPU time (s) 168.71
Current children cumulated vsize (Kb) 67932

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 16807 0 0 0 17770 98 0 0 25 0 1 0 1846643797 69144576 16195 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 16881 16195 145 145 0 16736 0
[pid=9017] vsize: 67524
Current children cumulated CPU time (s) 178.69
Current children cumulated vsize (Kb) 69648

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 17602 0 0 0 18756 104 0 0 25 0 1 0 1846643797 72364032 16990 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 17667 16990 145 145 0 17522 0
[pid=9017] vsize: 70668
Current children cumulated CPU time (s) 188.61
Current children cumulated vsize (Kb) 72792

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 18258 0 0 0 19744 108 0 0 25 0 1 0 1846643797 75067392 17646 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 18327 17646 145 145 0 18182 0
[pid=9017] vsize: 73308
Current children cumulated CPU time (s) 198.53
Current children cumulated vsize (Kb) 75432

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 18781 0 0 0 20736 111 0 0 25 0 1 0 1846643797 77176832 18169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 18842 18169 145 145 0 18697 0
[pid=9017] vsize: 75368
Current children cumulated CPU time (s) 208.48
Current children cumulated vsize (Kb) 77492

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.89 1/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) T 9013 9013 16528 0 -1 0 19280 0 0 0 21727 115 0 0 25 0 1 0 1846643797 79212544 18668 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9017/statm): 19339 18668 145 145 0 19194 0
[pid=9017] vsize: 77356
Current children cumulated CPU time (s) 218.43
Current children cumulated vsize (Kb) 79480

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 19731 0 0 0 22720 119 0 0 25 0 1 0 1846643797 81080320 19119 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 19795 19119 145 145 0 19650 0
[pid=9017] vsize: 79180
Current children cumulated CPU time (s) 228.4
Current children cumulated vsize (Kb) 81304

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 20157 0 0 0 23713 122 0 0 25 0 1 0 1846643797 82862080 19545 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 20230 19545 145 145 0 20085 0
[pid=9017] vsize: 80920
Current children cumulated CPU time (s) 238.36
Current children cumulated vsize (Kb) 83044

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 20538 0 0 0 24708 124 0 0 25 0 1 0 1846643797 84537344 19926 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 20639 19926 145 145 0 20494 0
[pid=9017] vsize: 82556
Current children cumulated CPU time (s) 248.33
Current children cumulated vsize (Kb) 84680

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 20905 0 0 0 25702 127 0 0 25 0 1 0 1846643797 86040576 20293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 21006 20293 145 145 0 20861 0
[pid=9017] vsize: 84024
Current children cumulated CPU time (s) 258.3
Current children cumulated vsize (Kb) 86148

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 21243 0 0 0 26696 130 0 0 25 0 1 0 1846643797 87470080 20631 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 21355 20631 145 145 0 21210 0
[pid=9017] vsize: 85420
Current children cumulated CPU time (s) 268.27
Current children cumulated vsize (Kb) 87544

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 21580 0 0 0 27690 133 0 0 25 0 1 0 1846643797 88870912 20968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 21697 20968 145 145 0 21552 0
[pid=9017] vsize: 86788
Current children cumulated CPU time (s) 278.24
Current children cumulated vsize (Kb) 88912

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 21955 0 0 0 28684 136 0 0 25 0 1 0 1846643797 90386432 21343 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 22067 21343 145 145 0 21922 0
[pid=9017] vsize: 88268
Current children cumulated CPU time (s) 288.21
Current children cumulated vsize (Kb) 90392

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 22338 0 0 0 29677 138 0 0 25 0 1 0 1846643797 91955200 21726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 22450 21726 145 145 0 22305 0
[pid=9017] vsize: 89800
Current children cumulated CPU time (s) 298.16
Current children cumulated vsize (Kb) 91924

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 22662 0 0 0 30670 141 0 0 25 0 1 0 1846643797 93274112 22050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 22772 22050 145 145 0 22627 0
[pid=9017] vsize: 91088
Current children cumulated CPU time (s) 308.12
Current children cumulated vsize (Kb) 93212

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 22935 0 0 0 31666 143 0 0 25 0 1 0 1846643797 94412800 22323 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 23050 22323 145 145 0 22905 0
[pid=9017] vsize: 92200
Current children cumulated CPU time (s) 318.1
Current children cumulated vsize (Kb) 94324

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 23254 0 0 0 32660 146 0 0 25 0 1 0 1846643797 95703040 22642 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 23365 22642 145 145 0 23220 0
[pid=9017] vsize: 93460
Current children cumulated CPU time (s) 328.07
Current children cumulated vsize (Kb) 95584

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 23574 0 0 0 33656 147 0 0 25 0 1 0 1846643797 96972800 22962 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 23675 22962 145 145 0 23530 0
[pid=9017] vsize: 94700
Current children cumulated CPU time (s) 338.04
Current children cumulated vsize (Kb) 96824

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 23897 0 0 0 34650 150 0 0 25 0 1 0 1846643797 98267136 23285 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 23991 23285 145 145 0 23846 0
[pid=9017] vsize: 95964
Current children cumulated CPU time (s) 348.01
Current children cumulated vsize (Kb) 98088

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 24034 0 0 0 35647 151 0 0 25 0 1 0 1846643797 98840576 23422 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 24131 23422 145 145 0 23986 0
[pid=9017] vsize: 96524
Current children cumulated CPU time (s) 357.99
Current children cumulated vsize (Kb) 98648

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 24349 0 0 0 36643 153 0 0 25 0 1 0 1846643797 100102144 23737 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 24439 23737 145 145 0 24294 0
[pid=9017] vsize: 97756
Current children cumulated CPU time (s) 367.97
Current children cumulated vsize (Kb) 99880

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 25313 0 0 0 37627 159 0 0 25 0 1 0 1846643797 104022016 24701 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 25396 24701 145 145 0 25251 0
[pid=9017] vsize: 101584
Current children cumulated CPU time (s) 377.87
Current children cumulated vsize (Kb) 103708

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 25957 0 0 0 38618 164 0 0 25 0 1 0 1846643797 106659840 25345 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 26040 25345 145 145 0 25895 0
[pid=9017] vsize: 104160
Current children cumulated CPU time (s) 387.83
Current children cumulated vsize (Kb) 106284

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 26522 0 0 0 39608 169 0 0 25 0 1 0 1846643797 108986368 25910 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 26608 25910 145 145 0 26463 0
[pid=9017] vsize: 106432
Current children cumulated CPU time (s) 397.78
Current children cumulated vsize (Kb) 108556

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 26976 0 0 0 40600 172 0 0 25 0 1 0 1846643797 110891008 26364 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 27073 26364 145 145 0 26928 0
[pid=9017] vsize: 108292
Current children cumulated CPU time (s) 407.73
Current children cumulated vsize (Kb) 110416

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 27447 0 0 0 41592 175 0 0 25 0 1 0 1846643797 112836608 26835 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 27548 26835 145 145 0 27403 0
[pid=9017] vsize: 110192
Current children cumulated CPU time (s) 417.68
Current children cumulated vsize (Kb) 112316

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 27955 0 0 0 42583 179 0 0 25 0 1 0 1846643797 114884608 27343 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 28048 27343 145 145 0 27903 0
[pid=9017] vsize: 112192
Current children cumulated CPU time (s) 427.63
Current children cumulated vsize (Kb) 114316

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 28409 0 0 0 43576 182 0 0 25 0 1 0 1846643797 116744192 27797 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 28502 27797 145 145 0 28357 0
[pid=9017] vsize: 114008
Current children cumulated CPU time (s) 437.59
Current children cumulated vsize (Kb) 116132

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 28866 0 0 0 44567 185 0 0 25 0 1 0 1846643797 118571008 28254 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 28948 28254 145 145 0 28803 0
[pid=9017] vsize: 115792
Current children cumulated CPU time (s) 447.53
Current children cumulated vsize (Kb) 117916

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 29333 0 0 0 45559 189 0 0 25 0 1 0 1846643797 120520704 28721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 29424 28721 145 145 0 29279 0
[pid=9017] vsize: 117696
Current children cumulated CPU time (s) 457.49
Current children cumulated vsize (Kb) 119820

[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 29796 0 0 0 46552 193 0 0 25 0 1 0 1846643797 123494400 29184 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 30150 29184 145 145 0 30005 0
[pid=9017] vsize: 120600
Current children cumulated CPU time (s) 467.46
Current children cumulated vsize (Kb) 122724

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 30543 0 0 0 47540 197 0 0 25 0 1 0 1846643797 126509056 29931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 30886 29931 145 145 0 30741 0
[pid=9017] vsize: 123544
Current children cumulated CPU time (s) 477.38
Current children cumulated vsize (Kb) 125668

[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31139 0 0 0 48528 203 0 0 25 0 1 0 1846643797 128933888 30527 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 31478 30527 145 145 0 31333 0
[pid=9017] vsize: 125912
Current children cumulated CPU time (s) 487.32
Current children cumulated vsize (Kb) 128036

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 49515 208 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 497.24
Current children cumulated vsize (Kb) 131336

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 50515 208 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 507.24
Current children cumulated vsize (Kb) 131336

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 51515 208 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221222992 134550333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 517.24
Current children cumulated vsize (Kb) 131336

[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 52514 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221222976 134562092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 527.24
Current children cumulated vsize (Kb) 131336

[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 53514 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223104 134556545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 537.24
Current children cumulated vsize (Kb) 131336

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 54514 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 547.24
Current children cumulated vsize (Kb) 131336

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 55514 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 557.24
Current children cumulated vsize (Kb) 131336

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 56515 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 567.25
Current children cumulated vsize (Kb) 131336

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 57515 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223096 134555971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 577.25
Current children cumulated vsize (Kb) 131336

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 58515 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 587.25
Current children cumulated vsize (Kb) 131336

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 59515 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 597.25
Current children cumulated vsize (Kb) 131336

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 60515 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 607.25
Current children cumulated vsize (Kb) 131336

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 61516 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134558147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 617.26
Current children cumulated vsize (Kb) 131336

[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 62516 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223104 134555683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 627.26
Current children cumulated vsize (Kb) 131336

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 63516 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 637.26
Current children cumulated vsize (Kb) 131336

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 64516 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 647.26
Current children cumulated vsize (Kb) 131336

[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 65517 209 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 657.27
Current children cumulated vsize (Kb) 131336

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 66516 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 667.27
Current children cumulated vsize (Kb) 131336

[startup+680.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 67517 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221222856 134782680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 677.28
Current children cumulated vsize (Kb) 131336

[startup+690.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 68517 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 687.28
Current children cumulated vsize (Kb) 131336

[startup+700.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 69517 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 697.28
Current children cumulated vsize (Kb) 131336

[startup+710.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 70517 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 707.28
Current children cumulated vsize (Kb) 131336

[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 71518 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 717.29
Current children cumulated vsize (Kb) 131336

[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 72518 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 727.29
Current children cumulated vsize (Kb) 131336

[startup+740.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 73518 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 737.29
Current children cumulated vsize (Kb) 131336

[startup+750.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 74518 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 747.29
Current children cumulated vsize (Kb) 131336

[startup+760.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 75518 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 757.29
Current children cumulated vsize (Kb) 131336

[startup+770.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 76519 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 767.3
Current children cumulated vsize (Kb) 131336

[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 77519 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223068 134557058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 777.3
Current children cumulated vsize (Kb) 131336

[startup+790.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 78519 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 787.3
Current children cumulated vsize (Kb) 131336

[startup+800.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 79519 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 797.3
Current children cumulated vsize (Kb) 131336

[startup+810.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 80520 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 807.31
Current children cumulated vsize (Kb) 131336

[startup+820.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 81520 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 817.31
Current children cumulated vsize (Kb) 131336

[startup+830.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 82520 210 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 827.31
Current children cumulated vsize (Kb) 131336

[startup+840.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 83520 211 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 837.32
Current children cumulated vsize (Kb) 131336

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 84520 211 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 847.32
Current children cumulated vsize (Kb) 131336

[startup+860.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 85520 211 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 857.32
Current children cumulated vsize (Kb) 131336

[startup+870.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 86518 213 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 867.32
Current children cumulated vsize (Kb) 131336

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 87518 213 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 877.32
Current children cumulated vsize (Kb) 131336

[startup+890.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 88518 213 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 887.32
Current children cumulated vsize (Kb) 131336

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 89518 213 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 897.32
Current children cumulated vsize (Kb) 131336

[startup+910.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 90518 214 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 907.33
Current children cumulated vsize (Kb) 131336

[startup+920.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 91519 214 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 917.34
Current children cumulated vsize (Kb) 131336

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31971 0 0 0 92518 214 0 0 25 0 1 0 1846643797 132313088 31359 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32303 31359 145 145 0 32158 0
[pid=9017] vsize: 129212
Current children cumulated CPU time (s) 927.33
Current children cumulated vsize (Kb) 131336

[startup+940.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 31980 0 0 0 93519 214 0 0 25 0 1 0 1846643797 132349952 31368 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32312 31368 145 145 0 32167 0
[pid=9017] vsize: 129248
Current children cumulated CPU time (s) 937.34
Current children cumulated vsize (Kb) 131372

[startup+950.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 32265 0 0 0 94514 217 0 0 25 0 1 0 1846643797 133578752 31653 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32612 31653 145 145 0 32467 0
[pid=9017] vsize: 130448
Current children cumulated CPU time (s) 947.32
Current children cumulated vsize (Kb) 132572

[startup+960.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 32564 0 0 0 95510 218 0 0 25 0 1 0 1846643797 134803456 31952 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 32911 31952 145 145 0 32766 0
[pid=9017] vsize: 131644
Current children cumulated CPU time (s) 957.29
Current children cumulated vsize (Kb) 133768

[startup+970.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 32888 0 0 0 96505 219 0 0 25 0 1 0 1846643797 136134656 32276 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 33236 32276 145 145 0 33091 0
[pid=9017] vsize: 132944
Current children cumulated CPU time (s) 967.25
Current children cumulated vsize (Kb) 135068

[startup+980.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 33191 0 0 0 97499 222 0 0 25 0 1 0 1846643797 137379840 32579 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 33540 32579 145 145 0 33395 0
[pid=9017] vsize: 134160
Current children cumulated CPU time (s) 977.22
Current children cumulated vsize (Kb) 136284

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 33513 0 0 0 98493 225 0 0 25 0 1 0 1846643797 138694656 32901 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 33861 32901 145 145 0 33716 0
[pid=9017] vsize: 135444
Current children cumulated CPU time (s) 987.19
Current children cumulated vsize (Kb) 137568

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 33808 0 0 0 99488 227 0 0 25 0 1 0 1846643797 139902976 33196 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 34156 33196 145 145 0 34011 0
[pid=9017] vsize: 136624
Current children cumulated CPU time (s) 997.16
Current children cumulated vsize (Kb) 138748

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 34098 0 0 0 100482 229 0 0 25 0 1 0 1846643797 141090816 33486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 34446 33486 145 145 0 34301 0
[pid=9017] vsize: 137784
Current children cumulated CPU time (s) 1007.12
Current children cumulated vsize (Kb) 139908

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 34391 0 0 0 101478 231 0 0 25 0 1 0 1846643797 142307328 33779 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 34743 33779 145 145 0 34598 0
[pid=9017] vsize: 138972
Current children cumulated CPU time (s) 1017.1
Current children cumulated vsize (Kb) 141096

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 34706 0 0 0 102472 233 0 0 25 0 1 0 1846643797 143618048 34094 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 35063 34094 145 145 0 34918 0
[pid=9017] vsize: 140252
Current children cumulated CPU time (s) 1027.06
Current children cumulated vsize (Kb) 142376

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 35011 0 0 0 103467 235 0 0 25 0 1 0 1846643797 144969728 34399 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 35393 34399 145 145 0 35248 0
[pid=9017] vsize: 141572
Current children cumulated CPU time (s) 1037.03
Current children cumulated vsize (Kb) 143696

[startup+1050.08 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 35277 0 0 0 104463 237 0 0 25 0 1 0 1846643797 146079744 34665 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 35664 34665 145 145 0 35519 0
[pid=9017] vsize: 142656
Current children cumulated CPU time (s) 1047.01
Current children cumulated vsize (Kb) 144780

[startup+1060.08 s]
Raw data (loadavg): 1.14 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 35570 0 0 0 105458 240 0 0 25 0 1 0 1846643797 147296256 34958 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 35961 34958 145 145 0 35816 0
[pid=9017] vsize: 143844
Current children cumulated CPU time (s) 1056.99
Current children cumulated vsize (Kb) 145968

[startup+1070.08 s]
Raw data (loadavg): 1.11 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 35872 0 0 0 106453 241 0 0 25 0 1 0 1846643797 148557824 35260 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 36269 35260 145 145 0 36124 0
[pid=9017] vsize: 145076
Current children cumulated CPU time (s) 1066.95
Current children cumulated vsize (Kb) 147200

[startup+1080.08 s]
Raw data (loadavg): 1.10 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 36180 0 0 0 107448 244 0 0 25 0 1 0 1846643797 149819392 35568 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 36577 35568 145 145 0 36432 0
[pid=9017] vsize: 146308
Current children cumulated CPU time (s) 1076.93
Current children cumulated vsize (Kb) 148432

[startup+1090.08 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 36475 0 0 0 108442 247 0 0 25 0 1 0 1846643797 151023616 35863 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 36871 35863 145 145 0 36726 0
[pid=9017] vsize: 147484
Current children cumulated CPU time (s) 1086.9
Current children cumulated vsize (Kb) 149608

[startup+1100.08 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 36787 0 0 0 109437 249 0 0 25 0 1 0 1846643797 152363008 36175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 37198 36175 145 145 0 37053 0
[pid=9017] vsize: 148792
Current children cumulated CPU time (s) 1096.87
Current children cumulated vsize (Kb) 150916

[startup+1110.08 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 37083 0 0 0 110432 251 0 0 25 0 1 0 1846643797 153579520 36471 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 37495 36471 145 145 0 37350 0
[pid=9017] vsize: 149980
Current children cumulated CPU time (s) 1106.84
Current children cumulated vsize (Kb) 152104

[startup+1120.08 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 37381 0 0 0 111427 253 0 0 25 0 1 0 1846643797 154783744 36769 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 37789 36769 145 145 0 37644 0
[pid=9017] vsize: 151156
Current children cumulated CPU time (s) 1116.81
Current children cumulated vsize (Kb) 153280

[startup+1130.08 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 37706 0 0 0 112420 256 0 0 25 0 1 0 1846643797 156114944 37094 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 38114 37094 145 145 0 37969 0
[pid=9017] vsize: 152456
Current children cumulated CPU time (s) 1126.77
Current children cumulated vsize (Kb) 154580

[startup+1140.09 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 38304 0 0 0 113410 260 0 0 25 0 1 0 1846643797 158564352 37692 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 38712 37692 145 145 0 38567 0
[pid=9017] vsize: 154848
Current children cumulated CPU time (s) 1136.71
Current children cumulated vsize (Kb) 156972

[startup+1150.09 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 39146 0 0 0 114396 265 0 0 25 0 1 0 1846643797 162017280 38534 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 39555 38534 145 145 0 39410 0
[pid=9017] vsize: 158220
Current children cumulated CPU time (s) 1146.62
Current children cumulated vsize (Kb) 160344

[startup+1160.09 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 39865 0 0 0 115384 270 0 0 25 0 1 0 1846643797 164966400 39253 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 40275 39253 145 145 0 40130 0
[pid=9017] vsize: 161100
Current children cumulated CPU time (s) 1156.55
Current children cumulated vsize (Kb) 163224

[startup+1170.09 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 40525 0 0 0 116372 276 0 0 25 0 1 0 1846643797 167673856 39913 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 40936 39913 145 145 0 40791 0
[pid=9017] vsize: 163744
Current children cumulated CPU time (s) 1166.49
Current children cumulated vsize (Kb) 165868

[startup+1180.09 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 41170 0 0 0 117359 280 0 0 25 0 1 0 1846643797 170315776 40558 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9017/statm): 41581 40558 145 145 0 41436 0
[pid=9017] vsize: 166324
Current children cumulated CPU time (s) 1176.4
Current children cumulated vsize (Kb) 168448

[startup+1190.09 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 41792 0 0 0 118347 284 0 0 25 0 1 0 1846643797 172879872 41180 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 42207 41180 145 145 0 42062 0
[pid=9017] vsize: 168828
Current children cumulated CPU time (s) 1186.32
Current children cumulated vsize (Kb) 170952

[startup+1200.09 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 42404 0 0 0 119337 289 0 0 25 0 1 0 1846643797 175398912 41792 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 42822 41792 145 145 0 42677 0
[pid=9017] vsize: 171288
Current children cumulated CPU time (s) 1196.27
Current children cumulated vsize (Kb) 173412

[startup+1210.09 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 42903 0 0 0 120328 293 0 0 25 0 1 0 1846643797 177487872 42291 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 43332 42291 145 145 0 43187 0
[pid=9017] vsize: 173328
Current children cumulated CPU time (s) 1206.22
Current children cumulated vsize (Kb) 175452



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 9017
Raw data (/proc/9013/stat): 9013 (minisat+_script) S 9012 9013 16528 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1846643793 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9013/statm): 531 226 485 147 0 384 0
[pid=9013] vsize: 2124
Raw data (/proc/9017/stat): 9017 (minisat+_64-bit) R 9013 9013 16528 0 -1 0 42903 0 0 0 120328 293 0 0 25 0 1 0 1846643797 177487872 42291 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9017/statm): 43332 42291 145 145 0 43187 0
[pid=9017] vsize: 173328
Current children cumulated CPU time (s) 1206.22
Current children cumulated vsize (Kb) 175452

Sending SIGTERM to -9013
Sleeping 2 seconds
One traced child (pid=9013) ended because it received signal 15 (SIGTERM)
One traced child (pid=9017) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.17
CPU time (s): 1206.3
CPU user time (s): 1203.29
CPU system time (s): 3.01354
CPU usage (%): 99.6798
Max. virtual memory (cumulated for all children) (Kb): 175452

Verifier Data

ERROR: no interpretation found !