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/miplib3/normalized-mps-v2-20-10-qiu.opb
MD5SUMe35e3cb279fca9040eb6914414619c36
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 4546

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        891184 kB
Buffers:         36412 kB
Cached:          81728 kB
SwapCached:        792 kB
Active:          70804 kB
Inactive:        49984 kB
HighTotal:      131008 kB
HighFree:        49588 kB
LowTotal:       903652 kB
LowFree:        841596 kB
SwapTotal:     2097136 kB
SwapFree:      2095876 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5756 kB
Slab:            17040 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:27:55 (client local time) WITH STATUS 0 IN 1206.3 SECONDS
stats: 3002 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/14015/stat): 14015 (minisat+_script) R 14014 14015 27660 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1780140583 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14015/statm): 174 3 169 147 0 27 0
[pid=14015] 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=14016
New process pid=14017
New process pid=14018
execve syscall for /bin/sed executable
One traced child (pid=14017) 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=14018) exited with status: 0
One traced child (pid=14016) exited with status: 0
New process pid=14019
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-qiu.opb

[startup+10.0032 s]
Raw data (loadavg): 0.94 0.99 0.90 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 5805 0 0 0 943 28 0 0 25 0 1 0 1780140588 23187456 5193 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 5661 5193 145 145 0 5516 0
[pid=14019] vsize: 22644
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 24768

[startup+20.005 s]
Raw data (loadavg): 0.95 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 6964 0 0 0 1925 35 0 0 25 0 1 0 1780140588 27942912 6352 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 6822 6352 145 145 0 6677 0
[pid=14019] vsize: 27288
Current children cumulated CPU time (s) 19.61
Current children cumulated vsize (Kb) 29412

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.99 0.91 3/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 8125 0 0 0 2908 42 0 0 25 0 1 0 1780140588 32788480 7513 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 8005 7513 145 145 0 7860 0
[pid=14019] vsize: 32020
Current children cumulated CPU time (s) 29.51
Current children cumulated vsize (Kb) 34144

[startup+40.0066 s]
Raw data (loadavg): 0.96 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 9148 0 0 0 3891 50 0 0 25 0 1 0 1780140588 36933632 8536 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 9017 8536 145 145 0 8872 0
[pid=14019] vsize: 36068
Current children cumulated CPU time (s) 39.42
Current children cumulated vsize (Kb) 38192

[startup+50.0074 s]
Raw data (loadavg): 0.97 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 9890 0 0 0 4877 56 0 0 25 0 1 0 1780140588 39956480 9278 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 9755 9278 145 145 0 9610 0
[pid=14019] vsize: 39020
Current children cumulated CPU time (s) 49.34
Current children cumulated vsize (Kb) 41144

[startup+60.0082 s]
Raw data (loadavg): 0.97 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 10709 0 0 0 5864 61 0 0 25 0 1 0 1780140588 43282432 10097 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 10567 10097 145 145 0 10422 0
[pid=14019] vsize: 42268
Current children cumulated CPU time (s) 59.26
Current children cumulated vsize (Kb) 44392

[startup+70.01 s]
Raw data (loadavg): 0.98 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 11668 0 0 0 6847 68 0 0 25 0 1 0 1780140588 47452160 11056 4294967295 134512640 135094434 3221224448 3221223040 134557191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 11585 11056 145 145 0 11440 0
[pid=14019] vsize: 46340
Current children cumulated CPU time (s) 69.16
Current children cumulated vsize (Kb) 48464

[startup+80.0107 s]
Raw data (loadavg): 0.98 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 12444 0 0 0 7834 74 0 0 25 0 1 0 1780140588 50614272 11832 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 12357 11832 145 145 0 12212 0
[pid=14019] vsize: 49428
Current children cumulated CPU time (s) 79.09
Current children cumulated vsize (Kb) 51552

[startup+90.0115 s]
Raw data (loadavg): 0.98 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 13165 0 0 0 8822 79 0 0 25 0 1 0 1780140588 53563392 12553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 13077 12553 145 145 0 12932 0
[pid=14019] vsize: 52308
Current children cumulated CPU time (s) 89.02
Current children cumulated vsize (Kb) 54432

[startup+100.012 s]
Raw data (loadavg): 0.98 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 13827 0 0 0 9812 83 0 0 25 0 1 0 1780140588 56295424 13215 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 13744 13215 145 145 0 13599 0
[pid=14019] vsize: 54976
Current children cumulated CPU time (s) 98.96
Current children cumulated vsize (Kb) 57100

[startup+110.013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 14437 0 0 0 10800 88 0 0 25 0 1 0 1780140588 58773504 13825 4294967295 134512640 135094434 3221224448 3221223104 134561460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 14349 13825 145 145 0 14204 0
[pid=14019] vsize: 57396
Current children cumulated CPU time (s) 108.89
Current children cumulated vsize (Kb) 59520

[startup+120.015 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 14965 0 0 0 11792 92 0 0 25 0 1 0 1780140588 60911616 14353 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 14871 14353 145 145 0 14726 0
[pid=14019] vsize: 59484
Current children cumulated CPU time (s) 118.85
Current children cumulated vsize (Kb) 61608

[startup+130.016 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 15353 0 0 0 12785 94 0 0 25 0 1 0 1780140588 62529536 14741 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 15266 14741 145 145 0 15121 0
[pid=14019] vsize: 61064
Current children cumulated CPU time (s) 128.8
Current children cumulated vsize (Kb) 63188

[startup+140.016 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 15712 0 0 0 13778 98 0 0 25 0 1 0 1780140588 63991808 15100 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 15623 15100 145 145 0 15478 0
[pid=14019] vsize: 62492
Current children cumulated CPU time (s) 138.77
Current children cumulated vsize (Kb) 64616

[startup+150.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 16044 0 0 0 14773 100 0 0 25 0 1 0 1780140588 65347584 15432 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 15954 15432 145 145 0 15809 0
[pid=14019] vsize: 63816
Current children cumulated CPU time (s) 148.74
Current children cumulated vsize (Kb) 65940

[startup+160.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 16277 0 0 0 15770 101 0 0 25 0 1 0 1780140588 66301952 15665 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 16187 15665 145 145 0 16042 0
[pid=14019] vsize: 64748
Current children cumulated CPU time (s) 158.72
Current children cumulated vsize (Kb) 66872

[startup+170.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 16556 0 0 0 16765 104 0 0 25 0 1 0 1780140588 67575808 15944 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 16498 15944 145 145 0 16353 0
[pid=14019] vsize: 65992
Current children cumulated CPU time (s) 168.7
Current children cumulated vsize (Kb) 68116

[startup+180.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 16942 0 0 0 17759 108 0 0 25 0 1 0 1780140588 69689344 16330 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 17014 16330 145 145 0 16869 0
[pid=14019] vsize: 68056
Current children cumulated CPU time (s) 178.68
Current children cumulated vsize (Kb) 70180

[startup+190.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 17743 0 0 0 18747 113 0 0 25 0 1 0 1780140588 72933376 17131 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 17806 17131 145 145 0 17661 0
[pid=14019] vsize: 71224
Current children cumulated CPU time (s) 188.61
Current children cumulated vsize (Kb) 73348

[startup+200.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 18344 0 0 0 19736 117 0 0 25 0 1 0 1780140588 75407360 17732 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 18410 17732 145 145 0 18265 0
[pid=14019] vsize: 73640
Current children cumulated CPU time (s) 198.54
Current children cumulated vsize (Kb) 75764

[startup+210.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 18891 0 0 0 20725 122 0 0 25 0 1 0 1780140588 77615104 18279 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 18949 18279 145 145 0 18804 0
[pid=14019] vsize: 75796
Current children cumulated CPU time (s) 208.48
Current children cumulated vsize (Kb) 77920

[startup+220.025 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 19381 0 0 0 21717 126 0 0 25 0 1 0 1780140588 79638528 18769 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 19443 18769 145 145 0 19298 0
[pid=14019] vsize: 77772
Current children cumulated CPU time (s) 218.44
Current children cumulated vsize (Kb) 79896

[startup+230.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 19825 0 0 0 22710 128 0 0 25 0 1 0 1780140588 81473536 19213 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 19891 19213 145 145 0 19746 0
[pid=14019] vsize: 79564
Current children cumulated CPU time (s) 228.39
Current children cumulated vsize (Kb) 81688

[startup+240.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 20256 0 0 0 23703 131 0 0 25 0 1 0 1780140588 83263488 19644 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 20328 19644 145 145 0 20183 0
[pid=14019] vsize: 81312
Current children cumulated CPU time (s) 238.35
Current children cumulated vsize (Kb) 83436

[startup+250.027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 20644 0 0 0 24696 134 0 0 25 0 1 0 1780140588 84955136 20032 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 20741 20032 145 145 0 20596 0
[pid=14019] vsize: 82964
Current children cumulated CPU time (s) 248.31
Current children cumulated vsize (Kb) 85088

[startup+260.028 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 21007 0 0 0 25689 138 0 0 25 0 1 0 1780140588 86470656 20395 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 21111 20395 145 145 0 20966 0
[pid=14019] vsize: 84444
Current children cumulated CPU time (s) 258.28
Current children cumulated vsize (Kb) 86568

[startup+270.029 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 21321 0 0 0 26685 140 0 0 25 0 1 0 1780140588 87781376 20709 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 21431 20709 145 145 0 21286 0
[pid=14019] vsize: 85724
Current children cumulated CPU time (s) 268.26
Current children cumulated vsize (Kb) 87848

[startup+280.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 21687 0 0 0 27681 142 0 0 25 0 1 0 1780140588 89309184 21075 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 21804 21075 145 145 0 21659 0
[pid=14019] vsize: 87216
Current children cumulated CPU time (s) 278.24
Current children cumulated vsize (Kb) 89340

[startup+290.031 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 22074 0 0 0 28673 145 0 0 25 0 1 0 1780140588 90873856 21462 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 22186 21462 145 145 0 22041 0
[pid=14019] vsize: 88744
Current children cumulated CPU time (s) 288.19
Current children cumulated vsize (Kb) 90868

[startup+300.032 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 22437 0 0 0 29667 148 0 0 25 0 1 0 1780140588 92352512 21825 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 22547 21825 145 145 0 22402 0
[pid=14019] vsize: 90188
Current children cumulated CPU time (s) 298.16
Current children cumulated vsize (Kb) 92312

[startup+310.033 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 22738 0 0 0 30660 151 0 0 25 0 1 0 1780140588 93581312 22126 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 22847 22126 145 145 0 22702 0
[pid=14019] vsize: 91388
Current children cumulated CPU time (s) 308.12
Current children cumulated vsize (Kb) 93512

[startup+320.034 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 23026 0 0 0 31655 154 0 0 25 0 1 0 1780140588 94773248 22414 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 23138 22414 145 145 0 22993 0
[pid=14019] vsize: 92552
Current children cumulated CPU time (s) 318.1
Current children cumulated vsize (Kb) 94676

[startup+330.034 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 23338 0 0 0 32649 156 0 0 25 0 1 0 1780140588 96034816 22726 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 23446 22726 145 145 0 23301 0
[pid=14019] vsize: 93784
Current children cumulated CPU time (s) 328.06
Current children cumulated vsize (Kb) 95908

[startup+340.036 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 23689 0 0 0 33643 158 0 0 25 0 1 0 1780140588 97431552 23077 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 23787 23077 145 145 0 23642 0
[pid=14019] vsize: 95148
Current children cumulated CPU time (s) 338.02
Current children cumulated vsize (Kb) 97272

[startup+350.037 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 23985 0 0 0 34638 161 0 0 25 0 1 0 1780140588 98648064 23373 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 24084 23373 145 145 0 23939 0
[pid=14019] vsize: 96336
Current children cumulated CPU time (s) 348
Current children cumulated vsize (Kb) 98460

[startup+360.038 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 24052 0 0 0 35636 162 0 0 25 0 1 0 1780140588 98922496 23440 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 24151 23440 145 145 0 24006 0
[pid=14019] vsize: 96604
Current children cumulated CPU time (s) 357.99
Current children cumulated vsize (Kb) 98728

[startup+370.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 24722 0 0 0 36626 166 0 0 25 0 1 0 1780140588 101617664 24110 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 24809 24110 145 145 0 24664 0
[pid=14019] vsize: 99236
Current children cumulated CPU time (s) 367.93
Current children cumulated vsize (Kb) 101360

[startup+380.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 25580 0 0 0 37612 172 0 0 25 0 1 0 1780140588 105111552 24968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 25662 24968 145 145 0 25517 0
[pid=14019] vsize: 102648
Current children cumulated CPU time (s) 377.85
Current children cumulated vsize (Kb) 104772

[startup+390.042 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 26168 0 0 0 38602 176 0 0 25 0 1 0 1780140588 107520000 25556 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 26250 25556 145 145 0 26105 0
[pid=14019] vsize: 105000
Current children cumulated CPU time (s) 387.79
Current children cumulated vsize (Kb) 107124

[startup+400.044 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 26705 0 0 0 39592 181 0 0 25 0 1 0 1780140588 109752320 26093 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 26795 26093 145 145 0 26650 0
[pid=14019] vsize: 107180
Current children cumulated CPU time (s) 397.74
Current children cumulated vsize (Kb) 109304

[startup+410.045 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 27156 0 0 0 40584 184 0 0 25 0 1 0 1780140588 111620096 26544 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 27251 26544 145 145 0 27106 0
[pid=14019] vsize: 109004
Current children cumulated CPU time (s) 407.69
Current children cumulated vsize (Kb) 111128

[startup+420.046 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 27651 0 0 0 41576 188 0 0 25 0 1 0 1780140588 113659904 27039 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 27749 27039 145 145 0 27604 0
[pid=14019] vsize: 110996
Current children cumulated CPU time (s) 417.65
Current children cumulated vsize (Kb) 113120

[startup+430.046 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 28156 0 0 0 42567 192 0 0 25 0 1 0 1780140588 115703808 27544 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 28248 27544 145 145 0 28103 0
[pid=14019] vsize: 112992
Current children cumulated CPU time (s) 427.6
Current children cumulated vsize (Kb) 115116

[startup+440.047 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 28605 0 0 0 43559 195 0 0 25 0 1 0 1780140588 117534720 27993 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 28695 27993 145 145 0 28550 0
[pid=14019] vsize: 114780
Current children cumulated CPU time (s) 437.55
Current children cumulated vsize (Kb) 116904

[startup+450.048 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 29065 0 0 0 44552 198 0 0 25 0 1 0 1780140588 119386112 28453 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 29147 28453 145 145 0 29002 0
[pid=14019] vsize: 116588
Current children cumulated CPU time (s) 447.51
Current children cumulated vsize (Kb) 118712

[startup+460.049 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 29530 0 0 0 45546 201 0 0 25 0 1 0 1780140588 121356288 28918 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 29628 28918 145 145 0 29483 0
[pid=14019] vsize: 118512
Current children cumulated CPU time (s) 457.48
Current children cumulated vsize (Kb) 120636

[startup+470.05 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 30181 0 0 0 46535 205 0 0 25 0 1 0 1780140588 125046784 29569 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 30529 29569 145 145 0 30384 0
[pid=14019] vsize: 122116
Current children cumulated CPU time (s) 467.41
Current children cumulated vsize (Kb) 124240

[startup+480.05 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 30847 0 0 0 47525 210 0 0 25 0 1 0 1780140588 127750144 30235 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 31189 30235 145 145 0 31044 0
[pid=14019] vsize: 124756
Current children cumulated CPU time (s) 477.36
Current children cumulated vsize (Kb) 126880

[startup+490.052 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31701 0 0 0 48511 216 0 0 25 0 1 0 1780140588 131215360 31089 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32035 31089 145 145 0 31890 0
[pid=14019] vsize: 128140
Current children cumulated CPU time (s) 487.28
Current children cumulated vsize (Kb) 130264

[startup+500.053 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 49505 218 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 497.24
Current children cumulated vsize (Kb) 131336

[startup+510.054 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 50505 218 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 507.24
Current children cumulated vsize (Kb) 131336

[startup+520.056 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 51505 218 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 517.24
Current children cumulated vsize (Kb) 131336

[startup+530.056 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 52505 219 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223120 134556499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 527.25
Current children cumulated vsize (Kb) 131336

[startup+540.057 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 53505 219 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223176 134538517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 537.25
Current children cumulated vsize (Kb) 131336

[startup+550.058 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 54504 220 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 547.25
Current children cumulated vsize (Kb) 131336

[startup+560.059 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 55504 220 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 557.25
Current children cumulated vsize (Kb) 131336

[startup+570.059 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 56504 220 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223040 134557256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 567.25
Current children cumulated vsize (Kb) 131336

[startup+580.06 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 57503 221 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223168 134538574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 577.25
Current children cumulated vsize (Kb) 131336

[startup+590.062 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 58502 222 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 587.25
Current children cumulated vsize (Kb) 131336

[startup+600.063 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 59502 223 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 597.26
Current children cumulated vsize (Kb) 131336

[startup+610.064 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 60501 223 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 607.25
Current children cumulated vsize (Kb) 131336

[startup+620.064 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 61501 223 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 617.25
Current children cumulated vsize (Kb) 131336

[startup+630.065 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 62501 224 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 627.26
Current children cumulated vsize (Kb) 131336

[startup+640.067 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 63500 224 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 637.25
Current children cumulated vsize (Kb) 131336

[startup+650.068 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 64500 225 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 647.26
Current children cumulated vsize (Kb) 131336

[startup+660.069 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 65500 225 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 657.26
Current children cumulated vsize (Kb) 131336

[startup+670.07 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 66499 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 667.26
Current children cumulated vsize (Kb) 131336

[startup+680.071 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 67499 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 677.26
Current children cumulated vsize (Kb) 131336

[startup+690.072 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 68499 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 687.26
Current children cumulated vsize (Kb) 131336

[startup+700.074 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 69499 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 697.26
Current children cumulated vsize (Kb) 131336

[startup+710.073 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 70499 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 707.26
Current children cumulated vsize (Kb) 131336

[startup+720.074 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 71500 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 717.27
Current children cumulated vsize (Kb) 131336

[startup+730.075 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 72500 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 727.27
Current children cumulated vsize (Kb) 131336

[startup+740.076 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 73500 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 737.27
Current children cumulated vsize (Kb) 131336

[startup+750.077 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 74500 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 747.27
Current children cumulated vsize (Kb) 131336

[startup+760.077 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 75501 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 757.28
Current children cumulated vsize (Kb) 131336

[startup+770.078 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 76501 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 767.28
Current children cumulated vsize (Kb) 131336

[startup+780.079 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 77501 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 777.28
Current children cumulated vsize (Kb) 131336

[startup+790.08 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 78501 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 787.28
Current children cumulated vsize (Kb) 131336

[startup+800.081 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 79501 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 797.28
Current children cumulated vsize (Kb) 131336

[startup+810.08 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 80502 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 807.29
Current children cumulated vsize (Kb) 131336

[startup+820.082 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 81502 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 817.29
Current children cumulated vsize (Kb) 131336

[startup+830.083 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 82502 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 827.29
Current children cumulated vsize (Kb) 131336

[startup+840.085 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 83503 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 837.3
Current children cumulated vsize (Kb) 131336

[startup+850.086 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 84503 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 847.3
Current children cumulated vsize (Kb) 131336

[startup+860.085 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 85503 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 857.3
Current children cumulated vsize (Kb) 131336

[startup+870.086 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 86503 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 867.3
Current children cumulated vsize (Kb) 131336

[startup+880.087 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 87503 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 877.3
Current children cumulated vsize (Kb) 131336

[startup+890.088 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 88504 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 887.31
Current children cumulated vsize (Kb) 131336

[startup+900.088 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 89504 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 897.31
Current children cumulated vsize (Kb) 131336

[startup+910.089 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 90504 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 907.31
Current children cumulated vsize (Kb) 131336

[startup+920.09 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 91504 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 917.31
Current children cumulated vsize (Kb) 131336

[startup+930.091 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 31971 0 0 0 92505 226 0 0 25 0 1 0 1780140588 132313088 31359 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32303 31359 145 145 0 32158 0
[pid=14019] vsize: 129212
Current children cumulated CPU time (s) 927.32
Current children cumulated vsize (Kb) 131336

[startup+940.093 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 32236 0 0 0 93501 228 0 0 25 0 1 0 1780140588 133459968 31624 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32583 31624 145 145 0 32438 0
[pid=14019] vsize: 130332
Current children cumulated CPU time (s) 937.3
Current children cumulated vsize (Kb) 132456

[startup+950.093 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 32525 0 0 0 94495 231 0 0 25 0 1 0 1780140588 134647808 31913 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 32873 31913 145 145 0 32728 0
[pid=14019] vsize: 131492
Current children cumulated CPU time (s) 947.27
Current children cumulated vsize (Kb) 133616

[startup+960.093 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 32852 0 0 0 95490 233 0 0 25 0 1 0 1780140588 135987200 32240 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 33200 32240 145 145 0 33055 0
[pid=14019] vsize: 132800
Current children cumulated CPU time (s) 957.24
Current children cumulated vsize (Kb) 134924

[startup+970.094 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 33163 0 0 0 96486 235 0 0 25 0 1 0 1780140588 137265152 32551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 33512 32551 145 145 0 33367 0
[pid=14019] vsize: 134048
Current children cumulated CPU time (s) 967.22
Current children cumulated vsize (Kb) 136172

[startup+980.095 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 33482 0 0 0 97480 238 0 0 25 0 1 0 1780140588 138567680 32870 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 33830 32870 145 145 0 33685 0
[pid=14019] vsize: 135320
Current children cumulated CPU time (s) 977.19
Current children cumulated vsize (Kb) 137444

[startup+990.096 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 33779 0 0 0 98476 240 0 0 25 0 1 0 1780140588 139784192 33167 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 34127 33167 145 145 0 33982 0
[pid=14019] vsize: 136508
Current children cumulated CPU time (s) 987.17
Current children cumulated vsize (Kb) 138632

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 34068 0 0 0 99470 242 0 0 25 0 1 0 1780140588 140967936 33456 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 34416 33456 145 145 0 34271 0
[pid=14019] vsize: 137664
Current children cumulated CPU time (s) 997.13
Current children cumulated vsize (Kb) 139788

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 34366 0 0 0 100463 244 0 0 25 0 1 0 1780140588 142192640 33754 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 34715 33754 145 145 0 34570 0
[pid=14019] vsize: 138860
Current children cumulated CPU time (s) 1007.08
Current children cumulated vsize (Kb) 140984

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 34657 0 0 0 101458 246 0 0 25 0 1 0 1780140588 143417344 34045 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 35014 34045 145 145 0 34869 0
[pid=14019] vsize: 140056
Current children cumulated CPU time (s) 1017.05
Current children cumulated vsize (Kb) 142180

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) T 14015 14015 27660 0 -1 0 34983 0 0 0 102453 249 0 0 25 0 1 0 1780140588 144842752 34371 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14019/statm): 35362 34371 145 145 0 35217 0
[pid=14019] vsize: 141448
Current children cumulated CPU time (s) 1027.03
Current children cumulated vsize (Kb) 143572

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 35258 0 0 0 103448 251 0 0 25 0 1 0 1780140588 145993728 34646 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 35643 34646 145 145 0 35498 0
[pid=14019] vsize: 142572
Current children cumulated CPU time (s) 1037
Current children cumulated vsize (Kb) 144696

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 35551 0 0 0 104443 253 0 0 25 0 1 0 1780140588 147218432 34939 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 35942 34939 145 145 0 35797 0
[pid=14019] vsize: 143768
Current children cumulated CPU time (s) 1046.97
Current children cumulated vsize (Kb) 145892

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 35851 0 0 0 105438 255 0 0 25 0 1 0 1780140588 148471808 35239 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 36248 35239 145 145 0 36103 0
[pid=14019] vsize: 144992
Current children cumulated CPU time (s) 1056.94
Current children cumulated vsize (Kb) 147116

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 36163 0 0 0 106433 257 0 0 25 0 1 0 1780140588 149749760 35551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 36560 35551 145 145 0 36415 0
[pid=14019] vsize: 146240
Current children cumulated CPU time (s) 1066.91
Current children cumulated vsize (Kb) 148364

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 36453 0 0 0 107427 260 0 0 25 0 1 0 1780140588 150933504 35841 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 36849 35841 145 145 0 36704 0
[pid=14019] vsize: 147396
Current children cumulated CPU time (s) 1076.88
Current children cumulated vsize (Kb) 149520

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 36775 0 0 0 108422 262 0 0 25 0 1 0 1780140588 152313856 36163 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 37186 36163 145 145 0 37041 0
[pid=14019] vsize: 148744
Current children cumulated CPU time (s) 1086.85
Current children cumulated vsize (Kb) 150868

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 37069 0 0 0 109416 265 0 0 25 0 1 0 1780140588 153522176 36457 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 37481 36457 145 145 0 37336 0
[pid=14019] vsize: 149924
Current children cumulated CPU time (s) 1096.82
Current children cumulated vsize (Kb) 152048

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 37368 0 0 0 110410 267 0 0 25 0 1 0 1780140588 154730496 36756 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 37776 36756 145 145 0 37631 0
[pid=14019] vsize: 151104
Current children cumulated CPU time (s) 1106.78
Current children cumulated vsize (Kb) 153228

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 37692 0 0 0 111404 269 0 0 25 0 1 0 1780140588 156057600 37080 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 38100 37080 145 145 0 37955 0
[pid=14019] vsize: 152400
Current children cumulated CPU time (s) 1116.74
Current children cumulated vsize (Kb) 154524

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 38275 0 0 0 112395 273 0 0 25 0 1 0 1780140588 158445568 37663 4294967295 134512640 135094434 3221224448 3221223072 134557577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 38683 37663 145 145 0 38538 0
[pid=14019] vsize: 154732
Current children cumulated CPU time (s) 1126.69
Current children cumulated vsize (Kb) 156856

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 39098 0 0 0 113382 280 0 0 25 0 1 0 1780140588 161820672 38486 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 39507 38486 145 145 0 39362 0
[pid=14019] vsize: 158028
Current children cumulated CPU time (s) 1136.63
Current children cumulated vsize (Kb) 160152

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 39821 0 0 0 114369 285 0 0 25 0 1 0 1780140588 164786176 39209 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 40231 39209 145 145 0 40086 0
[pid=14019] vsize: 160924
Current children cumulated CPU time (s) 1146.55
Current children cumulated vsize (Kb) 163048

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 40473 0 0 0 115359 290 0 0 25 0 1 0 1780140588 167460864 39861 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 40884 39861 145 145 0 40739 0
[pid=14019] vsize: 163536
Current children cumulated CPU time (s) 1156.5
Current children cumulated vsize (Kb) 165660

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 41116 0 0 0 116348 295 0 0 17 0 1 0 1780140588 170094592 40504 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14019/statm): 41527 40504 145 145 0 41382 0
[pid=14019] vsize: 166108
Current children cumulated CPU time (s) 1166.44
Current children cumulated vsize (Kb) 168232

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 41746 0 0 0 117336 300 0 0 25 0 1 0 1780140588 172691456 41134 4294967295 134512640 135094434 3221224448 3221223088 134562095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 42161 41134 145 145 0 42016 0
[pid=14019] vsize: 168644
Current children cumulated CPU time (s) 1176.37
Current children cumulated vsize (Kb) 170768

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) T 14015 14015 27660 0 -1 0 42354 0 0 0 118327 304 0 0 25 0 1 0 1780140588 175198208 41742 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14019/statm): 42773 41742 145 145 0 42628 0
[pid=14019] vsize: 171092
Current children cumulated CPU time (s) 1186.32
Current children cumulated vsize (Kb) 173216

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 42865 0 0 0 119319 307 0 0 25 0 1 0 1780140588 177328128 42253 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 43293 42253 145 145 0 43148 0
[pid=14019] vsize: 173172
Current children cumulated CPU time (s) 1196.27
Current children cumulated vsize (Kb) 175296

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 43346 0 0 0 120311 311 0 0 25 0 1 0 1780140588 179306496 42734 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 43776 42734 145 145 0 43631 0
[pid=14019] vsize: 175104
Current children cumulated CPU time (s) 1206.23
Current children cumulated vsize (Kb) 177228



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.99 0.91 2/57 14019
Raw data (/proc/14015/stat): 14015 (minisat+_script) S 14014 14015 27660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1780140583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14015/statm): 531 226 485 147 0 384 0
[pid=14015] vsize: 2124
Raw data (/proc/14019/stat): 14019 (minisat+_64-bit) R 14015 14015 27660 0 -1 0 43346 0 0 0 120311 311 0 0 25 0 1 0 1780140588 179306496 42734 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14019/statm): 43776 42734 145 145 0 43631 0
[pid=14019] vsize: 175104
Current children cumulated CPU time (s) 1206.23
Current children cumulated vsize (Kb) 177228

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1206.3
CPU user time (s): 1203.11
CPU system time (s): 3.19351
CPU usage (%): 99.6783
Max. virtual memory (cumulated for all children) (Kb): 177228

Verifier Data

ERROR: no interpretation found !