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-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-grow15.opb
MD5SUM997a6069ce24fed97967c5999a31ff05
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 1200
Biggest coefficient in the objective function 469762048
Number of bits for the biggest coefficient in the objective function 29
Sum of the numbers in the objective function 19327352658
Number of bits of the sum of numbers in the objective function 35
Biggest number in a constraint 109773592723456
Number of bits of the biggest number in a constraint 47
Biggest sum of numbers in a constraint 511403730649348
Number of bits of the biggest sum of numbers49
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1262.28
Number of variables14880
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 constraint19
Maximum length of a constraint416

Trace number 6068

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        922476 kB
Buffers:         13064 kB
Cached:          69476 kB
SwapCached:        692 kB
Active:          26068 kB
Inactive:        58996 kB
HighTotal:      131008 kB
HighFree:        59304 kB
LowTotal:       903652 kB
LowFree:        863172 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            21372 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:22:26 (client local time) WITH STATUS 0 IN 1209.77 SECONDS
stats: 3218 7 1209.77 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): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1381]---> BDD-cost:   20
c ---[1380]---> BDD-cost:   24
c ---[1378]---> BDD-cost:   23
c ---[1374]---> BDD-cost:   22
c ---[1372]---> BDD-cost:   24
c ---[1371]---> BDD-cost:   25
c ---[1370]---> BDD-cost:   19
c ---[1369]---> BDD-cost:   21
c ---[1367]---> BDD-cost:   22
c ---[1366]---> BDD-cost:   21
c ---[1365]---> BDD-cost:   27
c ---[1364]---> BDD-cost:   20
c ---[1363]---> BDD-cost:   24
c ---[1361]---> BDD-cost:   23
c ---[1358]---> BDD-cost:   22
c ---[1357]---> BDD-cost:   22
c ---[1355]---> BDD-cost:   24
c ---[1354]---> BDD-cost:   25
c ---[1353]---> BDD-cost:   19
c ---[1352]---> BDD-cost:   21
c ---[1350]---> BDD-cost:   22
c ---[1349]---> BDD-cost:   21
c ---[1348]---> BDD-cost:   27
c ---[1347]---> BDD-cost:   20
c ---[1346]---> BDD-cost:   24
c ---[1344]---> BDD-cost:   23
c ---[1341]---> BDD-cost:   22
c ---[1340]---> BDD-cost:   22
c ---[1338]---> BDD-cost:   24
c ---[1337]---> BDD-cost:   25
c ---[1336]---> BDD-cost:   19
c ---[1335]---> BDD-cost:   21
c ---[1333]---> BDD-cost:   22
c ---[1332]---> BDD-cost:   21
c ---[1331]---> BDD-cost:   27
c ---[1330]---> BDD-cost:   20
c ---[1329]---> BDD-cost:   24
c ---[1327]---> BDD-cost:   23
c ---[1324]---> BDD-cost:   22
c ---[1323]---> BDD-cost:   22
c ---[1321]---> BDD-cost:   24
c ---[1320]---> BDD-cost:   25
c ---[1319]---> BDD-cost:   19
c ---[1318]---> BDD-cost:   21
c ---[1316]---> BDD-cost:   22
c ---[1315]---> BDD-cost:   21
c ---[1314]---> BDD-cost:   27
c ---[1313]---> BDD-cost:   20
c ---[1312]---> BDD-cost:   24
c ---[1310]---> BDD-cost:   23
c ---[1307]---> BDD-cost:   22
c ---[1306]---> BDD-cost:   22
c ---[1304]---> BDD-cost:   24
c ---[1303]---> BDD-cost:   25
c ---[1302]---> BDD-cost:   19
c ---[1301]---> BDD-cost:   21
c ---[1299]---> BDD-cost:   22
c ---[1298]---> BDD-cost:   21
c ---[1297]---> BDD-cost:   27
c ---[1296]---> BDD-cost:   20
c ---[1295]---> BDD-cost:   24
c ---[1293]---> BDD-cost:   23
c ---[1290]---> BDD-cost:   22
c ---[1289]---> BDD-cost:   22
c ---[1287]---> BDD-cost:   24
c ---[1286]---> BDD-cost:   25
c ---[1285]---> BDD-cost:   19
c ---[1284]---> BDD-cost:   21
c ---[1282]---> BDD-cost:   22
c ---[1281]---> BDD-cost:   21
c ---[1280]---> BDD-cost:   27
c ---[1279]---> BDD-cost:   20
c ---[1278]---> BDD-cost:   24
c ---[1276]---> BDD-cost:   23
c ---[1273]---> BDD-cost:   22
c ---[1272]---> BDD-cost:   22
c ---[1270]---> BDD-cost:   24
c ---[1269]---> BDD-cost:   25
c ---[1268]---> BDD-cost:   19
c ---[1267]---> BDD-cost:   21
c ---[1265]---> BDD-cost:   22
c ---[1264]---> BDD-cost:   21
c ---[1263]---> BDD-cost:   27
c ---[1262]---> BDD-cost:   20
c ---[1261]---> BDD-cost:   24
c ---[1259]---> BDD-cost:   23
c ---[1256]---> BDD-cost:   22
c ---[1255]---> BDD-cost:   22
c ---[1253]---> BDD-cost:   24
c ---[1252]---> BDD-cost:   25
c ---[1251]---> BDD-cost:   19
c ---[1250]---> BDD-cost:   21
c ---[1248]---> BDD-cost:   22
c ---[1247]---> BDD-cost:   21
c ---[1246]---> BDD-cost:   27
c ---[1245]---> BDD-cost:   20
c ---[1244]---> BDD-cost:   24
c ---[1242]---> BDD-cost:   23
c ---[1239]---> BDD-cost:   22
c ---[1238]---> BDD-cost:   22
c ---[1236]---> BDD-cost:   24
c ---[1235]---> BDD-cost:   25
c ---[1234]---> BDD-cost:   19
c ---[1233]---> BDD-cost:   21
c ---[1231]---> BDD-cost:   22
c ---[1230]---> BDD-cost:   21
c ---[1229]---> BDD-cost:   27
c ---[1228]---> BDD-cost:   20
c ---[1227]---> BDD-cost:   24
c ---[1225]---> BDD-cost:   23
c ---[1222]---> BDD-cost:   22
c ---[1221]---> BDD-cost:   22
c ---[1219]---> BDD-cost:   24
c ---[1218]---> BDD-cost:   25
c ---[1217]---> BDD-cost:   19
c ---[1216]---> BDD-cost:   21
c ---[1214]---> BDD-cost:   22
c ---[1213]---> BDD-cost:   21
c ---[1212]---> BDD-cost:   27
c ---[1211]---> BDD-cost:   20
c ---[1210]---> BDD-cost:   24
c ---[1208]---> BDD-cost:   23
c ---[1205]---> BDD-cost:   22
c ---[1204]---> BDD-cost:   22
c ---[1202]---> BDD-cost:   24
c ---[1201]---> BDD-cost:   25
c ---[1200]---> BDD-cost:   19
c ---[1199]---> BDD-cost:   21
c ---[1197]---> BDD-cost:   22
c ---[1196]---> BDD-cost:   21
c ---[1195]---> BDD-cost:   27
c ---[1194]---> BDD-cost:   20
c ---[1193]---> BDD-cost:   24
c ---[1191]---> BDD-cost:   23
c ---[1188]---> BDD-cost:   22
c ---[1187]---> BDD-cost:   22
c ---[1185]---> BDD-cost:   24
c ---[1184]---> BDD-cost:   25
c ---[1183]---> BDD-cost:   19
c ---[1182]---> BDD-cost:   21
c ---[1180]---> BDD-cost:   22
c ---[1179]---> BDD-cost:   21
c ---[1178]---> BDD-cost:   27
c ---[1177]---> BDD-cost:   20
c ---[1176]---> BDD-cost:   24
c ---[1174]---> BDD-cost:   23
c ---[1171]---> BDD-cost:   22
c ---[1170]---> BDD-cost:   22
c ---[1168]---> BDD-cost:   24
c ---[1167]---> BDD-cost:   25
c ---[1166]---> BDD-cost:   19
c ---[1165]---> BDD-cost:   21
c ---[1163]---> BDD-cost:   22
c ---[1162]---> BDD-cost:   21
c ---[1161]---> BDD-cost:   27
c ---[1160]---> BDD-cost:   20
c ---[1159]---> BDD-cost:   24
c ---[1157]---> BDD-cost:   23
c ---[1154]---> BDD-cost:   22
c ---[1153]---> BDD-cost:   22
c ---[1151]---> BDD-cost:   24
c ---[1150]---> BDD-cost:   25
c ---[1149]---> BDD-cost:   19
c ---[1148]---> BDD-cost:   21
c ---[1146]---> BDD-cost:   22
c ---[1145]---> BDD-cost:   21
c ---[1144]---> BDD-cost:   27
c ---[1143]---> BDD-cost:   20
c ---[1142]---> BDD-cost:   24
c ---[1140]---> BDD-cost:   23
c ---[1137]---> BDD-cost:   22
c ---[1136]---> BDD-cost:   22
c ---[1134]---> BDD-cost:   24
c ---[1133]---> BDD-cost:   25
c ---[1132]---> BDD-cost:   19
c ---[1131]---> BDD-cost:   21
c ---[1129]---> BDD-cost:   22
c ---[1128]---> BDD-cost:   21
c ---[1127]---> BDD-cost:   27
c ---[1105]---> BDD-cost:   26
c ---[1102]---> BDD-cost:   26
c ---[1099]---> BDD-cost:   26
c ---[1096]---> BDD-cost:   26
c ---[1093]---> BDD-cost:   26
c ---[1090]---> BDD-cost:   26
c ---[1087]---> BDD-cost:   26
c ---[1084]---> BDD-cost:   26
c ---[1081]---> BDD-cost:   19
c ---[1080]---> BDD-cost:   23
c ---[1078]---> BDD-cost:   22
c ---[1075]---> BDD-cost:   21
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   23
c ---[1071]---> BDD-cost:   24
c ---[1070]---> BDD-cost:   18
c ---[1069]---> BDD-cost:   20
c ---[1067]---> BDD-cost:   21
c ---[1066]---> BDD-cost:   20
c ---[1065]---> BDD-cost:   26
c ---[1064]---> BDD-cost:   19
c ---[1063]---> BDD-cost:   23
c ---[1061]---> BDD-cost:   22
c ---[1058]---> BDD-cost:   21
c ---[1057]---> BDD-cost:   21
c ---[1055]---> BDD-cost:   23
c ---[1054]---> BDD-cost:   24
c ---[1053]---> BDD-cost:   18
c ---[1052]---> BDD-cost:   20
c ---[1050]---> BDD-cost:   21
c ---[1049]---> BDD-cost:   20
c ---[1048]---> BDD-cost:   26
c ---[1047]---> BDD-cost:   19
c ---[1046]---> BDD-cost:   23
c ---[1044]---> BDD-cost:   22
c ---[1041]---> BDD-cost:   21
c ---[1040]---> BDD-cost:   21
c ---[1038]---> BDD-cost:   23
c ---[1037]---> BDD-cost:   24
c ---[1036]---> BDD-cost:   18
c ---[1035]---> BDD-cost:   20
c ---[1033]---> BDD-cost:   21
c ---[1032]---> BDD-cost:   20
c ---[1031]---> BDD-cost:   26
c ---[1030]---> BDD-cost:   19
c ---[1029]---> BDD-cost:   23
c ---[1027]---> BDD-cost:   22
c ---[1024]---> BDD-cost:   21
c ---[1023]---> BDD-cost:   21
c ---[1021]---> BDD-cost:   23
c ---[1020]---> BDD-cost:   24
c ---[1019]---> BDD-cost:   18
c ---[1018]---> BDD-cost:   20
c ---[1016]---> BDD-cost:   21
c ---[1015]---> BDD-cost:   20
c ---[1014]---> BDD-cost:   26
c ---[1013]---> BDD-cost:   19
c ---[1012]---> BDD-cost:   23
c ---[1010]---> BDD-cost:   22
c ---[1007]---> BDD-cost:   21
c ---[1006]---> BDD-cost:   21
c ---[1004]---> BDD-cost:   23
c ---[1003]---> BDD-cost:   24
c ---[1002]---> BDD-cost:   18
c ---[1001]---> BDD-cost:   20
c ---[ 999]---> BDD-cost:   21
c ---[ 998]---> BDD-cost:   20
c ---[ 997]---> BDD-cost:   26
c ---[ 996]---> BDD-cost:   19
c ---[ 995]---> BDD-cost:   23
c ---[ 993]---> BDD-cost:   22
c ---[ 990]---> BDD-cost:   21
c ---[ 989]---> BDD-cost:   21
c ---[ 987]---> BDD-cost:   23
c ---[ 986]---> BDD-cost:   24
c ---[ 985]---> BDD-cost:   18
c ---[ 984]---> BDD-cost:   20
c ---[ 982]---> BDD-cost:   21
c ---[ 981]---> BDD-cost:   20
c ---[ 980]---> BDD-cost:   26
c ---[ 979]---> BDD-cost:   19
c ---[ 978]---> BDD-cost:   23
c ---[ 976]---> BDD-cost:   22
c ---[ 973]---> BDD-cost:   21
c ---[ 972]---> BDD-cost:   21
c ---[ 970]---> BDD-cost:   23
c ---[ 969]---> BDD-cost:   24
c ---[ 968]---> BDD-cost:   18
c ---[ 967]---> BDD-cost:   20
c ---[ 965]---> BDD-cost:   21
c ---[ 964]---> BDD-cost:   20
c ---[ 963]---> BDD-cost:   26
c ---[ 962]---> BDD-cost:   19
c ---[ 961]---> BDD-cost:   23
c ---[ 959]---> BDD-cost:   22
c ---[ 956]---> BDD-cost:   21
c ---[ 955]---> BDD-cost:   21
c ---[ 953]---> BDD-cost:   23
c ---[ 952]---> BDD-cost:   24
c ---[ 951]---> BDD-cost:   18
c ---[ 950]---> BDD-cost:   20
c ---[ 948]---> BDD-cost:   21
c ---[ 947]---> BDD-cost:   20
c ---[ 946]---> BDD-cost:   26
c ---[ 945]---> BDD-cost:   19
c ---[ 944]---> BDD-cost:   23
c ---[ 942]---> BDD-cost:   22
c ---[ 939]---> BDD-cost:   21
c ---[ 938]---> BDD-cost:   21
c ---[ 936]---> BDD-cost:   23
c ---[ 935]---> BDD-cost:   24
c ---[ 934]---> BDD-cost:   18
c ---[ 933]---> BDD-cost:   20
c ---[ 931]---> BDD-cost:   21
c ---[ 930]---> BDD-cost:   20
c ---[ 929]---> BDD-cost:   26
c ---[ 928]---> BDD-cost:   19
c ---[ 927]---> BDD-cost:   23
c ---[ 925]---> BDD-cost:   22
c ---[ 922]---> BDD-cost:   21
c ---[ 921]---> BDD-cost:   21
c ---[ 919]---> BDD-cost:   23
c ---[ 918]---> BDD-cost:   24
c ---[ 917]---> BDD-cost:   18
c ---[ 916]---> BDD-cost:   20
c ---[ 914]---> BDD-cost:   21
c ---[ 913]---> BDD-cost:   20
c ---[ 912]---> BDD-cost:   26
c ---[ 911]---> BDD-cost:   19
c ---[ 910]---> BDD-cost:   23
c ---[ 908]---> BDD-cost:   22
c ---[ 905]---> BDD-cost:   21
c ---[ 904]---> BDD-cost:   21
c ---[ 902]---> BDD-cost:   23
c ---[ 901]---> BDD-cost:   24
c ---[ 900]---> BDD-cost:   18
c ---[ 899]---> BDD-cost:   20
c ---[ 897]---> BDD-cost:   21
c ---[ 896]---> BDD-cost:   20
c ---[ 895]---> BDD-cost:   26
c ---[ 894]---> BDD-cost:   19
c ---[ 893]---> BDD-cost:   23
c ---[ 891]---> BDD-cost:   22
c ---[ 888]---> BDD-cost:   21
c ---[ 887]---> BDD-cost:   21
c ---[ 885]---> BDD-cost:   23
c ---[ 884]---> BDD-cost:   24
c ---[ 883]---> BDD-cost:   18
c ---[ 882]---> BDD-cost:   20
c ---[ 880]---> BDD-cost:   21
c ---[ 879]---> BDD-cost:   20
c ---[ 878]---> BDD-cost:   26
c ---[ 877]---> BDD-cost:   19
c ---[ 876]---> BDD-cost:   23
c ---[ 874]---> BDD-cost:   22
c ---[ 871]---> BDD-cost:   21
c ---[ 870]---> BDD-cost:   21
c ---[ 868]---> BDD-cost:   23
c ---[ 867]---> BDD-cost:   24
c ---[ 866]---> BDD-cost:   18
c ---[ 865]---> BDD-cost:   20
c ---[ 863]---> BDD-cost:   21
c ---[ 862]---> BDD-cost:   20
c ---[ 861]---> BDD-cost:   26
c ---[ 860]---> BDD-cost:   19
c ---[ 859]---> BDD-cost:   23
c ---[ 857]---> BDD-cost:   22
c ---[ 854]---> BDD-cost:   21
c ---[ 853]---> BDD-cost:   21
c ---[ 851]---> BDD-cost:   23
c ---[ 850]---> BDD-cost:   24
c ---[ 849]---> BDD-cost:   18
c ---[ 848]---> BDD-cost:   20
c ---[ 846]---> BDD-cost:   21
c ---[ 845]---> BDD-cost:   20
c ---[ 844]---> BDD-cost:   26
c ---[ 843]---> BDD-cost:   19
c ---[ 842]---> BDD-cost:   23
c ---[ 840]---> BDD-cost:   22
c ---[ 837]---> BDD-cost:   21
c ---[ 836]---> BDD-cost:   21
c ---[ 834]---> BDD-cost:   23
c ---[ 833]---> BDD-cost:   24
c ---[ 832]---> BDD-cost:   18
c ---[ 831]---> BDD-cost:   20
c ---[ 829]---> BDD-cost:   21
c ---[ 828]---> BDD-cost:   20
c ---[ 827]---> BDD-cost:   26
c ---[ 808]---> BDD-cost:   25
c ---[ 805]---> BDD-cost:   25
c ---[ 802]---> BDD-cost:   25
c ---[ 799]---> BDD-cost:   25
c ---[ 796]---> BDD-cost:   25
c ---[ 793]---> BDD-cost:   25
c ---[ 790]---> BDD-cost:   25
c ---[ 787]---> BDD-cost:

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/27615/stat): 27615 (minisat+_script) R 27614 27615 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855125300 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27615/statm): 174 3 169 147 0 27 0
[pid=27615] 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=27616
New process pid=27617
New process pid=27618
execve syscall for /bin/sed executable
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
One traced child (pid=27617) exited with status: 0
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=27618) exited with status: 0
One traced child (pid=27616) exited with status: 0
New process pid=27619
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-grow15.opb
One traced child (pid=27619) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=27620
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-grow15.opb

[startup+10.0045 s]
Raw data (loadavg): 0.90 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 3092 0 0 0 939 18 0 0 25 0 1 0 1855125324 13086720 3075 4294967295 134512640 135167914 3221224448 3221223024 134845634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27620/statm): 3195 3075 162 162 0 3033 0
[pid=27620] vsize: 12780
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 14908

[startup+20.0054 s]
Raw data (loadavg): 0.91 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 1918 28 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218240 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 21220

[startup+30.0082 s]
Raw data (loadavg): 0.92 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 2918 29 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218848 134629445 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 29.63
Current children cumulated vsize (Kb) 21220

[startup+40.009 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 3918 29 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221217888 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 21220

[startup+50.0098 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 4918 29 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218972 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 49.63
Current children cumulated vsize (Kb) 21220

[startup+60.0106 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 5918 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218816 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 59.64
Current children cumulated vsize (Kb) 21220

[startup+70.0115 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 6918 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218144 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 21220

[startup+80.0123 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 7918 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218384 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 21220

[startup+90.0131 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 8918 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219264 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 89.64
Current children cumulated vsize (Kb) 21220

[startup+100.013 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 9918 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219180 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 99.64
Current children cumulated vsize (Kb) 21220

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 10919 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219000 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 109.65
Current children cumulated vsize (Kb) 21220

[startup+120.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 11919 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218912 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 119.65
Current children cumulated vsize (Kb) 21220

[startup+130.015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 12919 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219636 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 129.65
Current children cumulated vsize (Kb) 21220

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 13919 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219296 134695263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 139.65
Current children cumulated vsize (Kb) 21220

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 14919 30 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219100 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 149.65
Current children cumulated vsize (Kb) 21220

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 15919 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219072 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 159.66
Current children cumulated vsize (Kb) 21220

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 16919 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219264 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 169.66
Current children cumulated vsize (Kb) 21220

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 17920 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219200 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 179.67
Current children cumulated vsize (Kb) 21220

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 18920 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219804 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 189.67
Current children cumulated vsize (Kb) 21220

[startup+200.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 19920 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219160 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 199.67
Current children cumulated vsize (Kb) 21220

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 20920 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220048 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 209.67
Current children cumulated vsize (Kb) 21220

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 21920 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219264 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 219.67
Current children cumulated vsize (Kb) 21220

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 22921 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219296 134720508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 229.68
Current children cumulated vsize (Kb) 21220

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 23921 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219276 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 239.68
Current children cumulated vsize (Kb) 21220

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 24921 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220048 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 249.68
Current children cumulated vsize (Kb) 21220

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 25921 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219952 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 259.68
Current children cumulated vsize (Kb) 21220

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 26921 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220048 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 269.68
Current children cumulated vsize (Kb) 21220

[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 27922 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219888 134629358 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 279.69
Current children cumulated vsize (Kb) 21220

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 28922 31 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221218748 134723265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 289.69
Current children cumulated vsize (Kb) 21220

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 29922 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220192 134522331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 299.7
Current children cumulated vsize (Kb) 21220

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 30922 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219616 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 309.7
Current children cumulated vsize (Kb) 21220

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 31922 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219820 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 319.7
Current children cumulated vsize (Kb) 21220

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 32922 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219520 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 329.7
Current children cumulated vsize (Kb) 21220

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 33923 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219856 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 339.71
Current children cumulated vsize (Kb) 21220

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 34923 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220008 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 349.71
Current children cumulated vsize (Kb) 21220

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 35923 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219456 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 359.71
Current children cumulated vsize (Kb) 21220

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 36923 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219904 134631215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 369.71
Current children cumulated vsize (Kb) 21220

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 37924 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219712 134629080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 379.72
Current children cumulated vsize (Kb) 21220

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 38924 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219852 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 389.72
Current children cumulated vsize (Kb) 21220

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 39924 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219880 134693737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 399.72
Current children cumulated vsize (Kb) 21220

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 40924 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 409.72
Current children cumulated vsize (Kb) 21220

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 41925 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220144 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 419.73
Current children cumulated vsize (Kb) 21220

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 42924 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220304 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 429.72
Current children cumulated vsize (Kb) 21220

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 43925 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220384 134843015 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 439.73
Current children cumulated vsize (Kb) 21220

[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 44925 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219904 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 449.73
Current children cumulated vsize (Kb) 21220

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 45925 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220144 134696697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 459.73
Current children cumulated vsize (Kb) 21220

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 46925 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219856 134849071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 469.73
Current children cumulated vsize (Kb) 21220

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 47926 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220320 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 479.74
Current children cumulated vsize (Kb) 21220

[startup+490.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 48926 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220200 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 489.74
Current children cumulated vsize (Kb) 21220

[startup+500.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 49926 32 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220144 134696310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 499.74
Current children cumulated vsize (Kb) 21220

[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 50926 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219984 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 509.75
Current children cumulated vsize (Kb) 21220

[startup+520.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 51927 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219664 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 519.76
Current children cumulated vsize (Kb) 21220

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 52927 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220000 134693573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 529.76
Current children cumulated vsize (Kb) 21220

[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 53927 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220012 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 539.76
Current children cumulated vsize (Kb) 21220

[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 54927 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220244 134629267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 549.76
Current children cumulated vsize (Kb) 21220

[startup+560.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 55927 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220544 134522331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 559.76
Current children cumulated vsize (Kb) 21220

[startup+570.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 56928 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220848 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 569.77
Current children cumulated vsize (Kb) 21220

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 57928 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219880 134694481 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 579.77
Current children cumulated vsize (Kb) 21220

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 58928 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220396 134696406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 589.77
Current children cumulated vsize (Kb) 21220

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 59928 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220256 134630843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 599.77
Current children cumulated vsize (Kb) 21220

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 60928 33 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220856 134693615 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 609.77
Current children cumulated vsize (Kb) 21220

[startup+620.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 61927 34 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219692 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 619.77
Current children cumulated vsize (Kb) 21220

[startup+630.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 62927 34 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219776 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 629.77
Current children cumulated vsize (Kb) 21220

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 63927 35 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220320 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 639.78
Current children cumulated vsize (Kb) 21220

[startup+650.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 64927 35 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220236 134694551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 649.78
Current children cumulated vsize (Kb) 21220

[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 65927 35 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220732 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 659.78
Current children cumulated vsize (Kb) 21220

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 66927 35 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220768 134629345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 669.78
Current children cumulated vsize (Kb) 21220

[startup+680.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 67927 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220320 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 679.79
Current children cumulated vsize (Kb) 21220

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 68927 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220496 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 689.79
Current children cumulated vsize (Kb) 21220

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 69927 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220532 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 699.79
Current children cumulated vsize (Kb) 21220

[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 70928 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220892 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 709.8
Current children cumulated vsize (Kb) 21220

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 71928 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220960 134631184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 719.8
Current children cumulated vsize (Kb) 21220

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 72928 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 729.8
Current children cumulated vsize (Kb) 21220

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 73928 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220240 134629270 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 739.8
Current children cumulated vsize (Kb) 21220

[startup+750.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 74928 36 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220356 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 749.8
Current children cumulated vsize (Kb) 21220

[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 75928 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219884 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 759.81
Current children cumulated vsize (Kb) 21220

[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 76929 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220056 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 769.82
Current children cumulated vsize (Kb) 21220

[startup+780.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 77929 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220380 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 779.82
Current children cumulated vsize (Kb) 21220

[startup+790.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 78929 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219792 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 789.82
Current children cumulated vsize (Kb) 21220

[startup+800.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 79929 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220352 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 799.82
Current children cumulated vsize (Kb) 21220

[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 80929 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220672 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 809.82
Current children cumulated vsize (Kb) 21220

[startup+820.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 81929 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220588 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 819.82
Current children cumulated vsize (Kb) 21220

[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 82930 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220144 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 829.83
Current children cumulated vsize (Kb) 21220

[startup+840.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 83930 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220744 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 839.83
Current children cumulated vsize (Kb) 21220

[startup+850.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 84930 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220400 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 849.83
Current children cumulated vsize (Kb) 21220

[startup+860.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 85930 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220924 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 859.83
Current children cumulated vsize (Kb) 21220

[startup+870.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 86930 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220552 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 869.83
Current children cumulated vsize (Kb) 21220

[startup+880.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 87931 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221112 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 879.84
Current children cumulated vsize (Kb) 21220

[startup+890.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 88931 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220512 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 889.84
Current children cumulated vsize (Kb) 21220

[startup+900.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 89931 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220936 134696561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 899.84
Current children cumulated vsize (Kb) 21220

[startup+910.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 90931 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221219792 134696714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 909.84
Current children cumulated vsize (Kb) 21220

[startup+920.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 91931 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220880 134849595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 919.84
Current children cumulated vsize (Kb) 21220

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 92931 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220672 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 929.84
Current children cumulated vsize (Kb) 21220

[startup+940.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 93932 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220912 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 939.85
Current children cumulated vsize (Kb) 21220

[startup+950.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 94932 37 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221436 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 949.85
Current children cumulated vsize (Kb) 21220

[startup+960.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 95932 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221136 134629126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 959.86
Current children cumulated vsize (Kb) 21220

[startup+970.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 96932 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220368 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 969.86
Current children cumulated vsize (Kb) 21220

[startup+980.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 97932 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221020 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 979.86
Current children cumulated vsize (Kb) 21220

[startup+990.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 98933 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220584 134696409 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 989.87
Current children cumulated vsize (Kb) 21220

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 99933 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220508 134723246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 999.87
Current children cumulated vsize (Kb) 21220

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 100933 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221376 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1009.87
Current children cumulated vsize (Kb) 21220

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 101933 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220944 134629167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1019.87
Current children cumulated vsize (Kb) 21220

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 102933 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221312 134629307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1029.87
Current children cumulated vsize (Kb) 21220

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 103933 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220512 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1039.87
Current children cumulated vsize (Kb) 21220

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 104934 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220544 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1049.88
Current children cumulated vsize (Kb) 21220

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 105934 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220908 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1059.88
Current children cumulated vsize (Kb) 21220

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 106934 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221116 134693792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1069.88
Current children cumulated vsize (Kb) 21220

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 107934 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221296 134629096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1079.88
Current children cumulated vsize (Kb) 21220

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 108935 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221076 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1089.89
Current children cumulated vsize (Kb) 21220

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 109935 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220196 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1099.89
Current children cumulated vsize (Kb) 21220

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 110935 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220320 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1109.89
Current children cumulated vsize (Kb) 21220

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 111935 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221084 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1119.89
Current children cumulated vsize (Kb) 21220

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 112935 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220860 134723285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1129.89
Current children cumulated vsize (Kb) 21220

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 113935 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221200 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1139.89
Current children cumulated vsize (Kb) 21220

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 114936 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221196 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1149.9
Current children cumulated vsize (Kb) 21220

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 115936 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221220432 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1159.9
Current children cumulated vsize (Kb) 21220

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 116936 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221428 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1169.9
Current children cumulated vsize (Kb) 21220

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 117936 38 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221296 134629153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1179.9
Current children cumulated vsize (Kb) 21220

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 118936 39 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221224 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1189.91
Current children cumulated vsize (Kb) 21220

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 119936 39 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221376 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1199.91
Current children cumulated vsize (Kb) 21220

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 120937 39 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221264 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1209.92
Current children cumulated vsize (Kb) 21220



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27620
Raw data (/proc/27615/stat): 27615 (minisat+_script) S 27614 27615 28974 0 -1 0 314 930 0 0 0 1 12 3 17 0 1 0 1855125300 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27615/statm): 532 234 485 147 0 385 0
[pid=27615] vsize: 2128
Raw data (/proc/27620/stat): 27620 (minisat+_bignum) R 27615 27615 28974 0 -1 0 5373 0 0 0 120937 39 0 0 25 0 1 0 1855125324 19550208 4648 4294967295 134512640 135167914 3221224448 3221221228 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27620/statm): 4773 4648 162 162 0 4611 0
[pid=27620] vsize: 19092
Current children cumulated CPU time (s) 1209.92
Current children cumulated vsize (Kb) 21220

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

Child status: 0
Real time (s): 1210.11
CPU time (s): 1209.77
CPU user time (s): 1209.37
CPU system time (s): 0.399939
CPU usage (%): 99.9719
Max. virtual memory (cumulated for all children) (Kb): 21220

Verifier Data

ERROR: no interpretation found !