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/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-grow15.opb
MD5SUM18d2e7037e36eb0868942f66e3c0ecc5
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 1335
Biggest coefficient in the objective function 3758096384
Number of bits for the biggest coefficient in the objective function 32
Sum of the numbers in the objective function 154618822482
Number of bits of the sum of numbers in the objective function 38
Biggest number in a constraint 878188741787648
Number of bits of the biggest number in a constraint 50
Biggest sum of numbers in a constraint 4550739094651140
Number of bits of the biggest sum of numbers53
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1236.3
Number of variables17130
Total number of constraints900
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 constraints900
Minimum length of a constraint22
Maximum length of a constraint491

Trace number 2680

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        920100 kB
Buffers:         17728 kB
Cached:          69248 kB
SwapCached:        812 kB
Active:          34772 kB
Inactive:        54804 kB
HighTotal:      131008 kB
HighFree:        58716 kB
LowTotal:       903652 kB
LowFree:        861384 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            19196 kB
Committed_AS:    64332 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 21:00:32 (client local time) WITH STATUS 0 IN 1209.7 SECONDS
stats: 2834 7 1209.7 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1250] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1409]---> BDD-cost:   23
c ---[1408]---> BDD-cost:   27
c ---[1406]---> BDD-cost:   26
c ---[1403]---> BDD-cost:   25
c ---[1402]---> BDD-cost:   25
c ---[1400]---> BDD-cost:   27
c ---[1399]---> BDD-cost:   28
c ---[1398]---> BDD-cost:   22
c ---[1397]---> BDD-cost:   24
c ---[1395]---> BDD-cost:   25
c ---[1394]---> BDD-cost:   24
c ---[1393]---> BDD-cost:   30
c ---[1392]---> BDD-cost:   23
c ---[1391]---> BDD-cost:   27
c ---[1389]---> BDD-cost:   26
c ---[1386]---> BDD-cost:   25
c ---[1385]---> BDD-cost:   25
c ---[1383]---> BDD-cost:   27
c ---[1382]---> BDD-cost:   28
c ---[1381]---> BDD-cost:   22
c ---[1380]---> BDD-cost:   24
c ---[1378]---> BDD-cost:   25
c ---[1377]---> BDD-cost:   24
c ---[1376]---> BDD-cost:   30
c ---[1375]---> BDD-cost:   23
c ---[1374]---> BDD-cost:   27
c ---[1372]---> BDD-cost:   26
c ---[1369]---> BDD-cost:   25
c ---[1368]---> BDD-cost:   25
c ---[1366]---> BDD-cost:   27
c ---[1365]---> BDD-cost:   28
c ---[1364]---> BDD-cost:   22
c ---[1363]---> BDD-cost:   24
c ---[1361]---> BDD-cost:   25
c ---[1360]---> BDD-cost:   24
c ---[1359]---> BDD-cost:   30
c ---[1358]---> BDD-cost:   23
c ---[1357]---> BDD-cost:   27
c ---[1355]---> BDD-cost:   26
c ---[1352]---> BDD-cost:   25
c ---[1351]---> BDD-cost:   25
c ---[1349]---> BDD-cost:   27
c ---[1348]---> BDD-cost:   28
c ---[1347]---> BDD-cost:   22
c ---[1346]---> BDD-cost:   24
c ---[1344]---> BDD-cost:   25
c ---[1343]---> BDD-cost:   24
c ---[1342]---> BDD-cost:   30
c ---[1341]---> BDD-cost:   23
c ---[1340]---> BDD-cost:   27
c ---[1338]---> BDD-cost:   26
c ---[1335]---> BDD-cost:   25
c ---[1334]---> BDD-cost:   25
c ---[1332]---> BDD-cost:   27
c ---[1331]---> BDD-cost:   28
c ---[1330]---> BDD-cost:   22
c ---[1329]---> BDD-cost:   24
c ---[1327]---> BDD-cost:   25
c ---[1326]---> BDD-cost:   24
c ---[1325]---> BDD-cost:   30
c ---[1324]---> BDD-cost:   23
c ---[1323]---> BDD-cost:   27
c ---[1321]---> BDD-cost:   26
c ---[1318]---> BDD-cost:   25
c ---[1317]---> BDD-cost:   25
c ---[1315]---> BDD-cost:   27
c ---[1314]---> BDD-cost:   28
c ---[1313]---> BDD-cost:   22
c ---[1312]---> BDD-cost:   24
c ---[1310]---> BDD-cost:   25
c ---[1309]---> BDD-cost:   24
c ---[1308]---> BDD-cost:   30
c ---[1307]---> BDD-cost:   23
c ---[1306]---> BDD-cost:   27
c ---[1304]---> BDD-cost:   26
c ---[1301]---> BDD-cost:   25
c ---[1300]---> BDD-cost:   25
c ---[1298]---> BDD-cost:   27
c ---[1297]---> BDD-cost:   28
c ---[1296]---> BDD-cost:   22
c ---[1295]---> BDD-cost:   24
c ---[1293]---> BDD-cost:   25
c ---[1292]---> BDD-cost:   24
c ---[1291]---> BDD-cost:   30
c ---[1290]---> BDD-cost:   23
c ---[1289]---> BDD-cost:   27
c ---[1287]---> BDD-cost:   26
c ---[1284]---> BDD-cost:   25
c ---[1283]---> BDD-cost:   25
c ---[1281]---> BDD-cost:   27
c ---[1280]---> BDD-cost:   28
c ---[1279]---> BDD-cost:   22
c ---[1278]---> BDD-cost:   24
c ---[1276]---> BDD-cost:   25
c ---[1275]---> BDD-cost:   24
c ---[1274]---> BDD-cost:   30
c ---[1273]---> BDD-cost:   23
c ---[1272]---> BDD-cost:   27
c ---[1270]---> BDD-cost:   26
c ---[1267]---> BDD-cost:   25
c ---[1266]---> BDD-cost:   25
c ---[1264]---> BDD-cost:   27
c ---[1263]---> BDD-cost:   28
c ---[1262]---> BDD-cost:   22
c ---[1261]---> BDD-cost:   24
c ---[1259]---> BDD-cost:   25
c ---[1258]---> BDD-cost:   24
c ---[1257]---> BDD-cost:   30
c ---[1256]---> BDD-cost:   23
c ---[1255]---> BDD-cost:   27
c ---[1253]---> BDD-cost:   26
c ---[1250]---> BDD-cost:   25
c ---[1249]---> BDD-cost:   25
c ---[1247]---> BDD-cost:   27
c ---[1246]---> BDD-cost:   28
c ---[1245]---> BDD-cost:   22
c ---[1244]---> BDD-cost:   24
c ---[1242]---> BDD-cost:   25
c ---[1241]---> BDD-cost:   24
c ---[1240]---> BDD-cost:   30
c ---[1239]---> BDD-cost:   23
c ---[1238]---> BDD-cost:   27
c ---[1236]---> BDD-cost:   26
c ---[1233]---> BDD-cost:   25
c ---[1232]---> BDD-cost:   25
c ---[1230]---> BDD-cost:   27
c ---[1229]---> BDD-cost:   28
c ---[1228]---> BDD-cost:   22
c ---[1227]---> BDD-cost:   24
c ---[1225]---> BDD-cost:   25
c ---[1224]---> BDD-cost:   24
c ---[1223]---> BDD-cost:   30
c ---[1222]---> BDD-cost:   23
c ---[1221]---> BDD-cost:   27
c ---[1219]---> BDD-cost:   26
c ---[1216]---> BDD-cost:   25
c ---[1215]---> BDD-cost:   25
c ---[1213]---> BDD-cost:   27
c ---[1212]---> BDD-cost:   28
c ---[1211]---> BDD-cost:   22
c ---[1210]---> BDD-cost:   24
c ---[1208]---> BDD-cost:   25
c ---[1207]---> BDD-cost:   24
c ---[1206]---> BDD-cost:   30
c ---[1205]---> BDD-cost:   23
c ---[1204]---> BDD-cost:   27
c ---[1202]---> BDD-cost:   26
c ---[1199]---> BDD-cost:   25
c ---[1198]---> BDD-cost:   25
c ---[1196]---> BDD-cost:   27
c ---[1195]---> BDD-cost:   28
c ---[1194]---> BDD-cost:   22
c ---[1193]---> BDD-cost:   24
c ---[1191]---> BDD-cost:   25
c ---[1190]---> BDD-cost:   24
c ---[1189]---> BDD-cost:   30
c ---[1188]---> BDD-cost:   23
c ---[1187]---> BDD-cost:   27
c ---[1185]---> BDD-cost:   26
c ---[1182]---> BDD-cost:   25
c ---[1181]---> BDD-cost:   25
c ---[1179]---> BDD-cost:   27
c ---[1178]---> BDD-cost:   28
c ---[1177]---> BDD-cost:   22
c ---[1176]---> BDD-cost:   24
c ---[1174]---> BDD-cost:   25
c ---[1173]---> BDD-cost:   24
c ---[1172]---> BDD-cost:   30
c ---[1171]---> BDD-cost:   23
c ---[1170]---> BDD-cost:   27
c ---[1168]---> BDD-cost:   26
c ---[1165]---> BDD-cost:   25
c ---[1164]---> BDD-cost:   25
c ---[1162]---> BDD-cost:   27
c ---[1161]---> BDD-cost:   28
c ---[1160]---> BDD-cost:   22
c ---[1159]---> BDD-cost:   24
c ---[1157]---> BDD-cost:   25
c ---[1156]---> BDD-cost:   24
c ---[1155]---> BDD-cost:   30
c ---[1154]---> BDD-cost:   29
c ---[1151]---> BDD-cost:   29
c ---[1148]---> BDD-cost:   29
c ---[1145]---> BDD-cost:   29
c ---[1142]---> BDD-cost:   29
c ---[1139]---> BDD-cost:   29
c ---[1136]---> BDD-cost:   29
c ---[1133]---> BDD-cost:   29
c ---[1130]---> BDD-cost:   29
c ---[1127]---> BDD-cost:   29
c ---[1124]---> BDD-cost:   29
c ---[1121]---> BDD-cost:   29
c ---[1118]---> BDD-cost:   29
c ---[1115]---> BDD-cost:   29
c ---[1112]---> BDD-cost:   29
c ---[1109]---> BDD-cost:   22
c ---[1108]---> BDD-cost:   26
c ---[1106]---> BDD-cost:   25
c ---[1103]---> BDD-cost:   24
c ---[1102]---> BDD-cost:   24
c ---[1100]---> BDD-cost:   26
c ---[1099]---> BDD-cost:   27
c ---[1098]---> BDD-cost:   21
c ---[1097]---> BDD-cost:   23
c ---[1095]---> BDD-cost:   24
c ---[1094]---> BDD-cost:   23
c ---[1093]---> BDD-cost:   29
c ---[1092]---> BDD-cost:   22
c ---[1091]---> BDD-cost:   26
c ---[1089]---> BDD-cost:   25
c ---[1086]---> BDD-cost:   24
c ---[1085]---> BDD-cost:   24
c ---[1083]---> BDD-cost:   26
c ---[1082]---> BDD-cost:   27
c ---[1081]---> BDD-cost:   21
c ---[1080]---> BDD-cost:   23
c ---[1078]---> BDD-cost:   24
c ---[1077]---> BDD-cost:   23
c ---[1076]---> BDD-cost:   29
c ---[1075]---> BDD-cost:   22
c ---[1074]---> BDD-cost:   26
c ---[1072]---> BDD-cost:   25
c ---[1069]---> BDD-cost:   24
c ---[1068]---> BDD-cost:   24
c ---[1066]---> BDD-cost:   26
c ---[1065]---> BDD-cost:   27
c ---[1064]---> BDD-cost:   21
c ---[1063]---> BDD-cost:   23
c ---[1061]---> BDD-cost:   24
c ---[1060]---> BDD-cost:   23
c ---[1059]---> BDD-cost:   29
c ---[1058]---> BDD-cost:   22
c ---[1057]---> BDD-cost:   26
c ---[1055]---> BDD-cost:   25
c ---[1052]---> BDD-cost:   24
c ---[1051]---> BDD-cost:   24
c ---[1049]---> BDD-cost:   26
c ---[1048]---> BDD-cost:   27
c ---[1047]---> BDD-cost:   21
c ---[1046]---> BDD-cost:   23
c ---[1044]---> BDD-cost:   24
c ---[1043]---> BDD-cost:   23
c ---[1042]---> BDD-cost:   29
c ---[1041]---> BDD-cost:   22
c ---[1040]---> BDD-cost:   26
c ---[1038]---> BDD-cost:   25
c ---[1035]---> BDD-cost:   24
c ---[1034]---> BDD-cost:   24
c ---[1032]---> BDD-cost:   26
c ---[1031]---> BDD-cost:   27
c ---[1030]---> BDD-cost:   21
c ---[1029]---> BDD-cost:   23
c ---[1027]---> BDD-cost:   24
c ---[1026]---> BDD-cost:   23
c ---[1025]---> BDD-cost:   29
c ---[1024]---> BDD-cost:   22
c ---[1023]---> BDD-cost:   26
c ---[1021]---> BDD-cost:   25
c ---[1018]---> BDD-cost:   24
c ---[1017]---> BDD-cost:   24
c ---[1015]---> BDD-cost:   26
c ---[1014]---> BDD-cost:   27
c ---[1013]---> BDD-cost:   21
c ---[1012]---> BDD-cost:   23
c ---[1010]---> BDD-cost:   24
c ---[1009]---> BDD-cost:   23
c ---[1008]---> BDD-cost:   29
c ---[1007]---> BDD-cost:   22
c ---[1006]---> BDD-cost:   26
c ---[1004]---> BDD-cost:   25
c ---[1001]---> BDD-cost:   24
c ---[1000]---> BDD-cost:   24
c ---[ 998]---> BDD-cost:   26
c ---[ 997]---> BDD-cost:   27
c ---[ 996]---> BDD-cost:   21
c ---[ 995]---> BDD-cost:   23
c ---[ 993]---> BDD-cost:   24
c ---[ 992]---> BDD-cost:   23
c ---[ 991]---> BDD-cost:   29
c ---[ 990]---> BDD-cost:   22
c ---[ 989]---> BDD-cost:   26
c ---[ 987]---> BDD-cost:   25
c ---[ 984]---> BDD-cost:   24
c ---[ 983]---> BDD-cost:   24
c ---[ 981]---> BDD-cost:   26
c ---[ 980]---> BDD-cost:   27
c ---[ 979]---> BDD-cost:   21
c ---[ 978]---> BDD-cost:   23
c ---[ 976]---> BDD-cost:   24
c ---[ 975]---> BDD-cost:   23
c ---[ 974]---> BDD-cost:   29
c ---[ 973]---> BDD-cost:   22
c ---[ 972]---> BDD-cost:   26
c ---[ 970]---> BDD-cost:   25
c ---[ 967]---> BDD-cost:   24
c ---[ 966]---> BDD-cost:   24
c ---[ 964]---> BDD-cost:   26
c ---[ 963]---> BDD-cost:   27
c ---[ 962]---> BDD-cost:   21
c ---[ 961]---> BDD-cost:   23
c ---[ 959]---> BDD-cost:   24
c ---[ 958]---> BDD-cost:   23
c ---[ 957]---> BDD-cost:   29
c ---[ 956]---> BDD-cost:   22
c ---[ 955]---> BDD-cost:   26
c ---[ 953]---> BDD-cost:   25
c ---[ 950]---> BDD-cost:   24
c ---[ 949]---> BDD-cost:   24
c ---[ 947]---> BDD-cost:   26
c ---[ 946]---> BDD-cost:   27
c ---[ 945]---> BDD-cost:   21
c ---[ 944]---> BDD-cost:   23
c ---[ 942]---> BDD-cost:   24
c ---[ 941]---> BDD-cost:   23
c ---[ 940]---> BDD-cost:   29
c ---[ 939]---> BDD-cost:   22
c ---[ 938]---> BDD-cost:   26
c ---[ 936]---> BDD-cost:   25
c ---[ 933]---> BDD-cost:   24
c ---[ 932]---> BDD-cost:   24
c ---[ 930]---> BDD-cost:   26
c ---[ 929]---> BDD-cost:   27
c ---[ 928]---> BDD-cost:   21
c ---[ 927]---> BDD-cost:   23
c ---[ 925]---> BDD-cost:   24
c ---[ 924]---> BDD-cost:   23
c ---[ 923]---> BDD-cost:   29
c ---[ 922]---> BDD-cost:   22
c ---[ 921]---> BDD-cost:   26
c ---[ 919]---> BDD-cost:   25
c ---[ 916]---> BDD-cost:   24
c ---[ 915]---> BDD-cost:   24
c ---[ 913]---> BDD-cost:   26
c ---[ 912]---> BDD-cost:   27
c ---[ 911]---> BDD-cost:   21
c ---[ 910]---> BDD-cost:   23
c ---[ 908]---> BDD-cost:   24
c ---[ 907]---> BDD-cost:   23
c ---[ 906]---> BDD-cost:   29
c ---[ 905]---> BDD-cost:   22
c ---[ 904]---> BDD-cost:   26
c ---[ 902]---> BDD-cost:   25
c ---[ 899]---> BDD-cost:   24
c ---[ 898]---> BDD-cost:   24
c ---[ 896]---> BDD-cost:   26
c ---[ 895]---> BDD-cost:   27
c ---[ 894]---> BDD-cost:   21
c ---[ 893]---> BDD-cost:   23
c ---[ 891]---> BDD-cost:   24
c ---[ 890]---> BDD-cost:   23
c ---[ 889]---> BDD-cost:   29
c ---[ 888]---> BDD-cost:   22
c ---[ 887]---> BDD-cost:   26
c ---[ 885]---> BDD-cost:   25
c ---[ 882]---> BDD-cost:   24
c ---[ 881]---> BDD-cost:   24
c ---[ 879]---> BDD-cost:   26
c ---[ 878]---> BDD-cost:   27
c ---[ 877]---> BDD-cost:   21
c ---[ 876]---> BDD-cost:   23
c ---[ 874]---> BDD-cost:   24
c ---[ 873]---> BDD-cost:   23
c ---[ 872]---> BDD-cost:   29
c ---[ 871]---> BDD-cost:   22
c ---[ 870]---> BDD-cost:   26
c ---[ 868]---> BDD-cost:   25
c ---[ 865]---> BDD-cost:   24
c ---[ 864]---> BDD-cost:   24
c ---[ 862]---> BDD-cost:   26
c ---[ 861]---> BDD-cost:   27
c ---[ 860]---> BDD-cost:   21
c ---[ 859]---> BDD-cost:   23
c ---[ 857]---> BDD-cost:   24
c ---[ 856]---> BDD-cost:   2

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/32059/stat): 32059 (minisat+_script) R 32058 32059 20602 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1721477930 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/32059/statm): 174 3 169 147 0 27 0
[pid=32059] 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=32060
New process pid=32061
New process pid=32062
execve syscall for /bin/sed executable
One traced child (pid=32061) 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=32062) exited with status: 0
One traced child (pid=32060) exited with status: 0
New process pid=32063
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-grow15.opb
One traced child (pid=32063) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=32064
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-grow15.opb

[startup+10.0031 s]
Raw data (loadavg): 0.95 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 3168 0 0 0 937 18 0 0 25 0 1 0 1721477955 14204928 3144 4294967295 134512640 135167914 3221224448 3221223296 134569948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32064/statm): 3468 3144 162 162 0 3306 0
[pid=32064] vsize: 13872
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 16000

[startup+20.0038 s]
Raw data (loadavg): 0.95 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 1910 30 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221216704 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 19.58
Current children cumulated vsize (Kb) 24624

[startup+30.0054 s]
Raw data (loadavg): 0.96 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 2910 30 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221216876 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 29.58
Current children cumulated vsize (Kb) 24624

[startup+40.0061 s]
Raw data (loadavg): 0.97 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 3910 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221216624 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 39.59
Current children cumulated vsize (Kb) 24624

[startup+50.0068 s]
Raw data (loadavg): 0.97 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 4910 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217036 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 49.59
Current children cumulated vsize (Kb) 24624

[startup+60.0075 s]
Raw data (loadavg): 0.98 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 5910 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217208 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 59.59
Current children cumulated vsize (Kb) 24624

[startup+70.0081 s]
Raw data (loadavg): 0.98 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 6910 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217696 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 24624

[startup+80.0088 s]
Raw data (loadavg): 0.98 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 7910 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217792 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 79.59
Current children cumulated vsize (Kb) 24624

[startup+90.0095 s]
Raw data (loadavg): 0.98 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 8911 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217904 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 24624

[startup+100.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 9911 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217404 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 99.6
Current children cumulated vsize (Kb) 24624

[startup+110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 10911 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217600 134629069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 109.6
Current children cumulated vsize (Kb) 24624

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 11911 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217904 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 119.6
Current children cumulated vsize (Kb) 24624

[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 12911 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217216 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 129.6
Current children cumulated vsize (Kb) 24624

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 13912 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217568 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 24624

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 14912 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217840 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 24624

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 15912 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217680 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 24624

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 16912 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217328 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 169.61
Current children cumulated vsize (Kb) 24624

[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 17913 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218208 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 24624

[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 18913 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218116 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 24624

[startup+200.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 19913 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218320 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 24624

[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 20913 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218284 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 209.62
Current children cumulated vsize (Kb) 24624

[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 21913 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217536 134720484 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 219.62
Current children cumulated vsize (Kb) 24624

[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 22914 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217856 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 229.63
Current children cumulated vsize (Kb) 24624

[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 23914 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218208 134696310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 239.63
Current children cumulated vsize (Kb) 24624

[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 24914 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218064 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 249.63
Current children cumulated vsize (Kb) 24624

[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 25914 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218236 134722208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 24624

[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 26915 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221216496 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 269.64
Current children cumulated vsize (Kb) 24624

[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 27915 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217760 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 24624

[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 28915 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218144 134629454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 289.64
Current children cumulated vsize (Kb) 24624

[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 29915 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218828 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 299.64
Current children cumulated vsize (Kb) 24624

[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 30915 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218796 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 309.64
Current children cumulated vsize (Kb) 24624

[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 31916 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218208 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 319.65
Current children cumulated vsize (Kb) 24624

[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 32916 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218688 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 329.65
Current children cumulated vsize (Kb) 24624

[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 33916 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217328 134844694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 339.65
Current children cumulated vsize (Kb) 24624

[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 34916 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217872 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 349.65
Current children cumulated vsize (Kb) 24624

[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 35917 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218560 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 359.66
Current children cumulated vsize (Kb) 24624

[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 36917 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218240 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 369.66
Current children cumulated vsize (Kb) 24624

[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 37917 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218496 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 379.66
Current children cumulated vsize (Kb) 24624

[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 38917 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217792 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 389.66
Current children cumulated vsize (Kb) 24624

[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 39917 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218560 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 399.66
Current children cumulated vsize (Kb) 24624

[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 40918 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218628 134522308 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 409.67
Current children cumulated vsize (Kb) 24624

[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 41918 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217692 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 419.67
Current children cumulated vsize (Kb) 24624

[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 42918 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218208 134696395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 429.67
Current children cumulated vsize (Kb) 24624

[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 43919 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218976 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 439.68
Current children cumulated vsize (Kb) 24624

[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 44919 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218752 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 449.68
Current children cumulated vsize (Kb) 24624

[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 45919 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218456 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 459.68
Current children cumulated vsize (Kb) 24624

[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 46919 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218416 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 469.68
Current children cumulated vsize (Kb) 24624

[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 47920 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218476 134693762 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 479.69
Current children cumulated vsize (Kb) 24624

[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 48920 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219168 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 489.69
Current children cumulated vsize (Kb) 24624

[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 49920 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218768 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 499.69
Current children cumulated vsize (Kb) 24624

[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 50920 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217232 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 509.69
Current children cumulated vsize (Kb) 24624

[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 51920 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218272 134694545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 519.69
Current children cumulated vsize (Kb) 24624

[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 52921 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219008 134629290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 529.7
Current children cumulated vsize (Kb) 24624

[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 53921 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218304 134629123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 539.7
Current children cumulated vsize (Kb) 24624

[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 54921 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219156 134522308 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 549.7
Current children cumulated vsize (Kb) 24624

[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 55921 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218632 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 559.7
Current children cumulated vsize (Kb) 24624

[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 56922 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218624 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 569.71
Current children cumulated vsize (Kb) 24624

[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 57922 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219052 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 579.71
Current children cumulated vsize (Kb) 24624

[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 58922 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218924 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 589.71
Current children cumulated vsize (Kb) 24624

[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 59922 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219008 134629259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 599.71
Current children cumulated vsize (Kb) 24624

[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 60923 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217168 134723288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 609.72
Current children cumulated vsize (Kb) 24624

[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 61923 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218572 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 619.72
Current children cumulated vsize (Kb) 24624

[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 62923 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218800 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 629.72
Current children cumulated vsize (Kb) 24624

[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 63923 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218472 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 639.72
Current children cumulated vsize (Kb) 24624

[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 64923 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218612 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 649.72
Current children cumulated vsize (Kb) 24624

[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 65924 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219264 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 659.73
Current children cumulated vsize (Kb) 24624

[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 66924 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219168 134522206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 669.73
Current children cumulated vsize (Kb) 24624

[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 67924 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218592 134695278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 679.73
Current children cumulated vsize (Kb) 24624

[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 68924 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218960 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 689.73
Current children cumulated vsize (Kb) 24624

[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 69925 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218992 134694338 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 699.74
Current children cumulated vsize (Kb) 24624

[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 70925 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219040 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 709.74
Current children cumulated vsize (Kb) 24624

[startup+720.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 71925 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218288 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 719.74
Current children cumulated vsize (Kb) 24624

[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 72925 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218784 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 729.74
Current children cumulated vsize (Kb) 24624

[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 73926 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218992 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 739.75
Current children cumulated vsize (Kb) 24624

[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 74926 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218968 134695249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 749.75
Current children cumulated vsize (Kb) 24624

[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 75926 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219340 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 759.75
Current children cumulated vsize (Kb) 24624

[startup+770.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 76926 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219856 134843081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 769.75
Current children cumulated vsize (Kb) 24624

[startup+780.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 77927 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219344 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 779.76
Current children cumulated vsize (Kb) 24624

[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 78927 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218804 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 789.76
Current children cumulated vsize (Kb) 24624

[startup+800.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 79927 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219088 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 799.76
Current children cumulated vsize (Kb) 24624

[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 80927 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219460 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 809.76
Current children cumulated vsize (Kb) 24624

[startup+820.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 81927 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219340 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 819.76
Current children cumulated vsize (Kb) 24624

[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 82928 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221217792 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 829.77
Current children cumulated vsize (Kb) 24624

[startup+840.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 83928 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218608 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 839.77
Current children cumulated vsize (Kb) 24624

[startup+850.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 84928 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219152 134843015 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 849.77
Current children cumulated vsize (Kb) 24624

[startup+860.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 85928 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219168 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 859.77
Current children cumulated vsize (Kb) 24624

[startup+870.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 86928 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218816 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 869.77
Current children cumulated vsize (Kb) 24624

[startup+880.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 87929 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219440 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 879.78
Current children cumulated vsize (Kb) 24624

[startup+890.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 88929 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219264 134843068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 889.78
Current children cumulated vsize (Kb) 24624

[startup+900.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 89929 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219472 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 899.78
Current children cumulated vsize (Kb) 24624

[startup+910.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 90930 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219148 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 909.79
Current children cumulated vsize (Kb) 24624

[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 91930 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219004 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 919.79
Current children cumulated vsize (Kb) 24624

[startup+930.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 92930 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219712 134630858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 929.79
Current children cumulated vsize (Kb) 24624

[startup+940.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 93930 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219648 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 939.79
Current children cumulated vsize (Kb) 24624

[startup+950.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 94930 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219616 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 949.79
Current children cumulated vsize (Kb) 24624

[startup+960.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 95931 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218912 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 959.8
Current children cumulated vsize (Kb) 24624

[startup+970.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 96931 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219456 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 969.8
Current children cumulated vsize (Kb) 24624

[startup+980.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 97931 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219632 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 979.8
Current children cumulated vsize (Kb) 24624

[startup+990.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 98931 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218988 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 989.8
Current children cumulated vsize (Kb) 24624

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 99932 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219872 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 999.81
Current children cumulated vsize (Kb) 24624

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 100932 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219720 134629086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1009.81
Current children cumulated vsize (Kb) 24624

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 101932 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219648 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1019.81
Current children cumulated vsize (Kb) 24624

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 102932 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221220400 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1029.81
Current children cumulated vsize (Kb) 24624

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 103933 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219648 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1039.82
Current children cumulated vsize (Kb) 24624

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 104933 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219700 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1049.82
Current children cumulated vsize (Kb) 24624

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 105933 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221220424 134629360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1059.82
Current children cumulated vsize (Kb) 24624

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 106933 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221220204 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1069.82
Current children cumulated vsize (Kb) 24624

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 107934 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219440 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1079.83
Current children cumulated vsize (Kb) 24624

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 108934 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219200 134629161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1089.83
Current children cumulated vsize (Kb) 24624

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 109934 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221218816 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1099.83
Current children cumulated vsize (Kb) 24624

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 110934 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219440 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1109.83
Current children cumulated vsize (Kb) 24624

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 111935 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219440 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1119.84
Current children cumulated vsize (Kb) 24624

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 112935 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219436 134718504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1129.84
Current children cumulated vsize (Kb) 24624

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 113935 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219852 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1139.84
Current children cumulated vsize (Kb) 24624

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 114935 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219880 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1149.84
Current children cumulated vsize (Kb) 24624

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 115936 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219800 134693629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1159.85
Current children cumulated vsize (Kb) 24624

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 116936 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219364 134629364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1169.85
Current children cumulated vsize (Kb) 24624

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 117936 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219832 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1179.85
Current children cumulated vsize (Kb) 24624

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 118937 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219884 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1189.86
Current children cumulated vsize (Kb) 24624

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 119937 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219616 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1199.86
Current children cumulated vsize (Kb) 24624

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 120937 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221219968 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1209.86
Current children cumulated vsize (Kb) 24624



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 32064
Raw data (/proc/32059/stat): 32059 (minisat+_script) S 32058 32059 20602 0 -1 0 314 986 0 0 0 0 14 4 17 0 1 0 1721477930 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32059/statm): 532 234 485 147 0 385 0
[pid=32059] vsize: 2128
Raw data (/proc/32064/stat): 32064 (minisat+_bignum) R 32059 32059 20602 0 -1 0 6052 0 0 0 120937 31 0 0 25 0 1 0 1721477955 23035904 5307 4294967295 134512640 135167914 3221224448 3221220032 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32064/statm): 5624 5307 162 162 0 5462 0
[pid=32064] vsize: 22496
Current children cumulated CPU time (s) 1209.86
Current children cumulated vsize (Kb) 24624

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

Child status: 0
Real time (s): 1210.09
CPU time (s): 1209.7
CPU user time (s): 1209.38
CPU system time (s): 0.32395
CPU usage (%): 99.9681
Max. virtual memory (cumulated for all children) (Kb): 24624

Verifier Data

ERROR: no interpretation found !