PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0548.opb
MD5SUM	6f47095f2d417d23ced995954e641689
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	14938
Optimality of the best value was proved	NO
Number of terms in the objective function	416
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	96797
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	96797
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1236.51
Number of variables	548
Total number of constraints	724
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	550
Number of constraints which are nor clauses,nor cardinality constraints	134
Minimum length of a constraint	1
Maximum length of a constraint	143
Trace number 22049

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-22 01:59:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12166 boxname=wulflinc3 idbench=936 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f47095f2d417d23ced995954e641689  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-p0548.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 12166
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        488604 kB
Buffers:         34608 kB
Cached:         488788 kB
SwapCached:          0 kB
Active:          53768 kB
Inactive:       472456 kB
HighTotal:      131008 kB
HighFree:        24416 kB
LowTotal:       903652 kB
LowFree:        464188 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            14032 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:19:53 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 12166 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssss.s..ssss........................................
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   46
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:   48
c ---[ 159]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:   75
c ---[ 156]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   54
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:  105
c ---[ 151]---> BDD-cost:  104
c ---[ 150]---> BDD-cost:  120
c ---[ 149]---> BDD-cost:   79
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:  115
c ---[ 146]---> BDD-cost:  107
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   55
c ---[ 143]---> BDD-cost:   87
c ---[ 142]---> BDD-cost:   54
c ---[ 141]---> BDD-cost:  164
c ---[ 140]---> BDD-cost:  151
c ---[ 139]---> BDD-cost:   31
c ---[ 138]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   28
c ---[ 135]---> BDD-cost:   77
c ---[ 134]---> BDD-cost:  153
c ---[ 133]---> BDD-cost:  109
c ---[ 131]---> BDD-cost:  137
c ---[ 130]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:   56
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:    7
c ---[ 126]---> BDD-cost:   32
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   19
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   24
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:   29
c ---[ 112]---> BDD-cost:    6
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   29
c ---[ 109]---> BDD-cost:   51
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:   35
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   29
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   49
c ---[  99]---> BDD-cost:   60
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   68
c ---[  92]---> BDD-cost:   78
c ---[  91]---> BDD-cost:   47
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   68
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   12
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> BDD-cost:   37
c ---[  75]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   49
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    7
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    2
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   19075    57625 |    5722       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5315          
c   -- var.elim.:  2000/5315          
c   -- var.elim.:  3000/5315          
c   -- var.elim.:  4000/5315          
c   -- var.elim.:  5000/5315          
c   -- var.elim.:  5315/5315          
c   -- var.elim.:  1000/2378          
c   -- var.elim.:  2000/2378          
c   -- var.elim.:  2378/2378          
c   -- var.elim.:  397/397          
c   -- var.elim.:  34/34          
c   -- var.elim.:  7/7          
c   -- var.elim.:  7/7          
c   -- var.elim.:  6/6          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  772/772          
c   -- var.elim.:  370/370          
c   -- var.elim.:  22/22          
c   -- subsuming                       
c   -- var.elim.:  212/212          
c   -- var.elim.:  107/107          
c   -- var.elim.:  33/33          
c |         0 |   16772    55641 |      --       0       --      -- |     --   | -2299/-1794
c |         0 |   16772    55641 |    6708       0        0     nan |  0.000 % |
c |       100 |   16772    55641 |    7379     100     1128    11.3 |  4.070 % |
c |       250 |   16772    55641 |    8117     250     2964    11.9 |  4.070 % |
c |       475 |   16762    55601 |    8924     473     5972    12.6 |  4.097 % |
c |       813 |   16704    55366 |    9782     803    13123    16.3 |  4.203 % |
c |      1319 |   16646    55139 |   10723    1302    21332    16.4 |  4.310 % |
c |      2078 |   16631    55084 |   11785    2059    42441    20.6 |  4.363 % |
c |      3217 |   16631    55084 |   12963    3198    75788    23.7 |  4.363 % |
c |      4925 |   16631    55084 |   14260    4906   121329    24.7 |  4.363 % |
c |      7487 |   16631    55084 |   15686    7468   222551    29.8 |  4.363 % |
c |     11331 |   16631    55084 |   17254   11312   366479    32.4 |  4.363 % |
c |     17097 |   16631    55084 |   18980   17078   565290    33.1 |  4.363 % |
c ==============================================================================
c (current CPU-time: 8.67068 s)
c ==============================================================================
c [1mFound solution: 46347[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2918   maxlim: 49601   bits: 17/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     18063 |   36977   127739 |   11093   18044   583588    32.3 |  4.363 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3778          
c   -- var.elim.:  2000/3778          
c   -- var.elim.:  3000/3778          
c   -- var.elim.:  3778/3778          
c   -- var.elim.:  272/272          
c   -- var.elim.:  27/27          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  87/87          
c   -- var.elim.:  37/37          
c   -- var.elim.:  22/22          
c   -- var.elim.:  6/6          
c |     18063 |   36706   126773 |      --   18044       --      -- |     --   | -271/-960
c |     18063 |   36706   126773 |   14682   15934   477392    30.0 |  4.363 % |
c |     18163 |   36706   126773 |   16150   10723   318740    29.7 |  2.567 % |
c |     18314 |   36706   126773 |   17765   10874   321541    29.6 |  2.567 % |
c |     18539 |   36706   126773 |   19542   11099   327521    29.5 |  2.567 % |
c |     18876 |   36706   126773 |   21496   11436   334307    29.2 |  2.567 % |
c |     19382 |   36706   126773 |   23646   11942   347336    29.1 |  2.567 % |
c |     20142 |   36706   126773 |   26010   12702   366930    28.9 |  2.567 % |
c |     21282 |   36706   126773 |   28611   13842   404089    29.2 |  2.567 % |
c |     22991 |   36706   126773 |   31473   15551   456549    29.4 |  2.567 % |
c |     25554 |   36706   126773 |   34620   18114   558182    30.8 |  2.567 % |
c |     29398 |   36706   126773 |   38082   21958   674029    30.7 |  2.567 % |
c |     35166 |   36706   126773 |   41890   27726   855722    30.9 |  2.567 % |
c |     43815 |   36694   126732 |   46064   36374  1190177    32.7 |  2.582 % |
c |     56789 |   36694   126732 |   50671   16501   752094    45.6 |  2.582 % |
c |     76250 |   36694   126732 |   55738   35962  1548495    43.1 |  2.582 % |
c |    105442 |   36694   126732 |   61311   23721  1455072    61.3 |  2.582 % |
c |    149232 |   36694   126732 |   67443   22474   917126    40.8 |  2.582 % |
c |    214919 |   36694   126732 |   74187   36925  1147205    31.1 |  2.582 % |
c |    313446 |   36694   126732 |   81606   20838  1001239    48.0 |  2.582 % |
c |    461235 |   36694   126732 |   89766   42295  1668197    39.4 |  2.582 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1001_bit0 -C1002_bit0 C1003_bit0 C1004_bit0 -C1005_bit0 -C1008_bit0 -C1010_bit0 -C1011_bit0 C1012_bit0 -C1013_bit0 -C1014_bit0 -C1015_bit0 -C1016_bit0 C1019_bit0 C1021_bit0 C1022_bit0 -C1023_bit0 C1024_bit0 C1025_bit0 -C1026_bit0 -C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 -C1034_bit0 -C1035_bit0 -C1038_bit0 -C1040_bit0 -C1041_bit0 -C1042_bit0 -C1043_bit0 -C1044_bit0 -C1045_bit0 -C1046_bit0 C1049_bit0 C1051_bit0 -C1052_bit0 -C1053_bit0 -C1054_bit0 -C1055_bit0 -C1058_bit0 -C1060_bit0 -C1061_bit0 C1062_bit0 C1063_bit0 -C1064_bit0 -C1066_bit0 -C1067_bit0 -C1068_bit0 -C1069_bit0 -C1070_bit0 -C1072_bit0 -C1073_bit0 -C1074_bit0 -C1075_bit0 -C1076_bit0 -C1077_bit0 -C1079_bit0 -C1080_bit0 -C1081_bit0 -C1082_bit0 -C1083_bit0 -C1084_bit0 -C1087_bit0 -C1089_bit0 C1090_bit0 -C1091_bit0 -C1092_bit0 -C1093_bit0 C1094_bit0 C1095_bit0 C1098_bit0 -C1100_bit0 -C1101_bit0 -C1102_bit0 -C1103_bit0 -C1104_bit0 -C1105_bit0 -C1108_bit0 -C1109_bit0 -C1110_bit0 -C1111_bit0 C1112_bit0 C1113_bit0 -C1114_bit0 -C1117_bit0 -C1119_bit0 C1120_bit0 C1121_bit0 -C1122_bit0 -C1123_bit0 -C1124_bit0 -C1125_bit0 C1128_bit0 C1130_bit0 -C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1137_bit0 -C1139_bit0 -C1140_bit0 -C1141_bit0 -C1142_bit0 -C1143_bit0 -C1145_bit0 -C1146_bit0 -C1147_bit0 -C1148_bit0 -C1149_bit0 -C1151_bit0 -C1152_bit0 -C1153_bit0 -C1154_bit0 -C1155_bit0 -C1156_bit0 -C1158_bit0 -C1159_bit0 C1160_bit0 -C1161_bit0 C1162_bit0 C1163_bit0 -C1164_bit0 -C1167_bit0 -C1168_bit0 -C1169_bit0 -C1170_bit0 -C1171_bit0 -C1172_bit0 -C1173_bit0 -C1174_bit0 -C1175_bit0 -C1176_bit0 -C1179_bit0 -C1180_bit0 -C1181_bit0 -C1182_bit0 -C1183_bit0 C1184_bit0 -C1185_bit0 -C1186_bit0 C1187_bit0 C1188_bit0 -C1191_bit0 C1192_bit0 C1193_bit0 C1194_bit0 -C1195_bit0 -C1196_bit0 -C1197_bit0 -C1198_bit0 -C1199_bit0 -C1200_bit0 C1201_bit0 C1202_bit0 -C1205_bit0 -C1206_bit0 -C1207_bit0 -C1208_bit0 -C1209_bit0 -C1210_bit0 -C1211_bit0 -C1212_bit0 -C1213_bit0 -C1214_bit0 -C1215_bit0 -C1216_bit0 -C1217_bit0 C1218_bit0 -C1219_bit0 -C1220_bit0 -C1221_bit0 C1224_bit0 C1225_bit0 C1226_bit0 -C1227_bit0 C1228_bit0 -C1229_bit0 -C1230_bit0 -C1231_bit0 C1232_bit0 C1233_bit0 C1236_bit0 C1237_bit0 C1238_bit0 -C1239_bit0 C1240_bit0 -C1241_bit0 -C1242_bit0 -C1243_bit0 -C1244_bit0 -C1245_bit0 -C1246_bit0 -C1249_bit0 -C1250_bit0 -C1251_bit0 -C1252_bit0 -C1253_bit0 -C1254_bit0 -C1255_bit0 -C1256_bit0 -C1257_bit0 -C1258_bit0 -C1259_bit0 -C1262_bit0 -C1263_bit0 -C1264_bit0 -C1265_bit0 -C1266_bit0 C1267_bit0 -C1268_bit0 -C1269_bit0 -C1270_bit0 C1271_bit0 C1272_bit0 -C1273_bit0 C1276_bit0 -C1277_bit0 -C1278_bit0 C1279_bit0 C1280_bit0 -C1281_bit0 -C1282_bit0 -C1283_bit0 -C1284_bit0 -C1285_bit0 -C1286_bit0 -C1289_bit0 -C1290_bit0 -C1291_bit0 -C1292_bit0 C1293_bit0 C1294_bit0 -C1295_bit0 -C1296_bit0 -C1297_bit0 -C1298_bit0 -C1299_bit0 -C1300_bit0 C1303_bit0 C1304_bit0 C1305_bit0 -C1306_bit0 C1307_bit0 C1308_bit0 C1309_bit0 C1310_bit0 -C1311_bit0 C1312_bit0 C1313_bit0 -C1314_bit0 C1316_bit0 -C1317_bit0 C1318_bit0 C1319_bit0 -C1320_bit0 -C1321_bit0 -C1322_bit0 -C1323_#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.72 0.88 0.89 2/54 25252
Raw data (stat): 25252 (runsolver) R 25251 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491724299 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.76 0.89 0.89 2/54 25252
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 4258 0 0 0 987 11 0 0 25 0 1 0 491724299 17641472 3655 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4307 3655 603 41 0 4266 0
vsize: 17228
[startup+20.0036 s]
Raw data (loadavg): 0.87 0.91 0.90 2/54 25305
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 4510 0 0 0 1984 14 0 0 25 0 1 0 491724299 18710528 3907 4294967295 134512640 134672761 3221224544 3221223680 134614715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4568 3907 603 41 0 4527 0
vsize: 18272
[startup+30.0044 s]
Raw data (loadavg): 0.89 0.91 0.90 2/54 25305
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 4992 0 0 0 2981 17 0 0 25 0 1 0 491724299 20844544 4389 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4389 603 41 0 5048 0
vsize: 20356
[startup+40.0042 s]
Raw data (loadavg): 0.91 0.91 0.90 2/54 25305
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 5452 0 0 0 3980 19 0 0 25 0 1 0 491724299 22695936 4849 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5541 4849 603 41 0 5500 0
vsize: 22164
[startup+50.004 s]
Raw data (loadavg): 0.92 0.91 0.90 2/54 25305
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 5827 0 0 0 4978 20 0 0 25 0 1 0 491724299 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5177 603 41 0 5826 0
vsize: 23468
[startup+60.0039 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 25305
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 5827 0 0 0 5978 20 0 0 25 0 1 0 491724299 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5177 603 41 0 5826 0
vsize: 23468
[startup+70.0037 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 25305
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 5827 0 0 0 6978 21 0 0 25 0 1 0 491724299 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5177 603 41 0 5826 0
vsize: 23468
[startup+80.0046 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 6188 0 0 0 7977 22 0 0 25 0 1 0 491724299 25628672 5538 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6257 5538 603 41 0 6216 0
vsize: 25028
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 6545 0 0 0 8976 24 0 0 25 0 1 0 491724299 27082752 5895 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 5895 603 41 0 6571 0
vsize: 26448
[startup+100.004 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 6898 0 0 0 9974 25 0 0 25 0 1 0 491724299 28540928 6248 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6968 6248 603 41 0 6927 0
vsize: 27872
[startup+110.005 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7208 0 0 0 10974 26 0 0 25 0 1 0 491724299 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+120.005 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7208 0 0 0 11974 26 0 0 25 0 1 0 491724299 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+130.006 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7208 0 0 0 12973 27 0 0 25 0 1 0 491724299 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+140.006 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7208 0 0 0 13973 27 0 0 25 0 1 0 491724299 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+150.006 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7209 0 0 0 14973 27 0 0 25 0 1 0 491724299 29532160 6535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7210 6535 603 41 0 7169 0
vsize: 28840
[startup+160.006 s]
Raw data (loadavg): 1.06 0.95 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7209 0 0 0 15973 28 0 0 25 0 1 0 491724299 29532160 6535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7210 6535 603 41 0 7169 0
vsize: 28840
[startup+170.006 s]
Raw data (loadavg): 1.05 0.95 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7284 0 0 0 16973 28 0 0 25 0 1 0 491724299 29925376 6610 4294967295 134512640 134672761 3221224544 3221223728 134615649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7306 6610 603 41 0 7265 0
vsize: 29224
[startup+180.006 s]
Raw data (loadavg): 1.04 0.95 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7492 0 0 0 17972 29 0 0 25 0 1 0 491724299 30724096 6818 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7501 6818 603 41 0 7460 0
vsize: 30004
[startup+190.007 s]
Raw data (loadavg): 1.03 0.95 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7729 0 0 0 18972 30 0 0 25 0 1 0 491724299 31809536 7055 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7766 7055 603 41 0 7725 0
vsize: 31064
[startup+200.007 s]
Raw data (loadavg): 1.03 0.95 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7864 0 0 0 19971 30 0 0 25 0 1 0 491724299 32026624 7129 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+210.007 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7864 0 0 0 20971 30 0 0 25 0 1 0 491724299 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+220.007 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7864 0 0 0 21971 31 0 0 25 0 1 0 491724299 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+230.007 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7864 0 0 0 22971 31 0 0 25 0 1 0 491724299 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+240.007 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7864 0 0 0 23971 31 0 0 25 0 1 0 491724299 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+250.007 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7865 0 0 0 24971 31 0 0 25 0 1 0 491724299 32026624 7130 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7130 603 41 0 7778 0
vsize: 31276
[startup+260.008 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7866 0 0 0 25971 32 0 0 25 0 1 0 491724299 32026624 7131 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7131 603 41 0 7778 0
vsize: 31276
[startup+270.008 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7866 0 0 0 26970 32 0 0 25 0 1 0 491724299 32026624 7131 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7131 603 41 0 7778 0
vsize: 31276
[startup+280.008 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7869 0 0 0 27970 32 0 0 25 0 1 0 491724299 32026624 7134 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7134 603 41 0 7778 0
vsize: 31276
[startup+290.009 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7971 0 0 0 28970 33 0 0 25 0 1 0 491724299 32944128 7236 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8043 7236 603 41 0 8002 0
vsize: 32172
[startup+300.009 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 29970 33 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+310.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 30970 33 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+320.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 31970 34 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+330.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 32969 34 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+340.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 33969 34 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+350.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 34969 35 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+360.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 35969 35 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+370.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7978 0 0 0 36969 35 0 0 25 0 1 0 491724299 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+380.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7979 0 0 0 37969 36 0 0 25 0 1 0 491724299 32419840 7177 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7177 603 41 0 7874 0
vsize: 31660
[startup+390.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25307
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 7980 0 0 0 38969 36 0 0 25 0 1 0 491724299 32419840 7178 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7178 603 41 0 7874 0
vsize: 31660
[startup+400.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8187 0 0 0 39968 37 0 0 25 0 1 0 491724299 33361920 7385 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8145 7385 603 41 0 8104 0
vsize: 32580
[startup+410.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8495 0 0 0 40966 39 0 0 25 0 1 0 491724299 34107392 7588 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 7588 603 41 0 8286 0
vsize: 33308
[startup+420.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8496 0 0 0 41966 39 0 0 25 0 1 0 491724299 34107392 7589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 7589 603 41 0 8286 0
vsize: 33308
[startup+430.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8496 0 0 0 42966 39 0 0 25 0 1 0 491724299 34107392 7589 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 7589 603 41 0 8286 0
vsize: 33308
[startup+440.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8497 0 0 0 43966 40 0 0 25 0 1 0 491724299 34107392 7590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 7590 603 41 0 8286 0
vsize: 33308
[startup+450.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8521 0 0 0 44966 40 0 0 25 0 1 0 491724299 34287616 7614 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8371 7614 603 41 0 8330 0
vsize: 33484
[startup+460.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8542 0 0 0 45965 41 0 0 25 0 1 0 491724299 34451456 7635 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7635 603 41 0 8370 0
vsize: 33644
[startup+470.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8546 0 0 0 46965 41 0 0 25 0 1 0 491724299 34451456 7639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7639 603 41 0 8370 0
vsize: 33644
[startup+480.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8553 0 0 0 47965 41 0 0 25 0 1 0 491724299 34451456 7646 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7646 603 41 0 8370 0
vsize: 33644
[startup+490.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8572 0 0 0 48965 41 0 0 25 0 1 0 491724299 34615296 7665 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8451 7665 603 41 0 8410 0
vsize: 33804
[startup+500.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8573 0 0 0 49965 42 0 0 25 0 1 0 491724299 34615296 7666 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8451 7666 603 41 0 8410 0
vsize: 33804
[startup+510.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8609 0 0 0 50965 42 0 0 25 0 1 0 491724299 34779136 7702 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8491 7702 603 41 0 8450 0
vsize: 33964
[startup+520.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8761 0 0 0 51965 42 0 0 25 0 1 0 491724299 35418112 7854 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8647 7854 603 41 0 8606 0
vsize: 34588
[startup+530.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 8987 0 0 0 52964 43 0 0 25 0 1 0 491724299 36347904 8080 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8080 603 41 0 8833 0
vsize: 35496
[startup+540.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9159 0 0 0 53963 44 0 0 25 0 1 0 491724299 37064704 8252 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8252 603 41 0 9008 0
vsize: 36196
[startup+550.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9350 0 0 0 54963 45 0 0 25 0 1 0 491724299 37851136 8443 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9241 8443 603 41 0 9200 0
vsize: 36964
[startup+560.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9543 0 0 0 55962 46 0 0 25 0 1 0 491724299 38645760 8636 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9435 8636 603 41 0 9394 0
vsize: 37740
[startup+570.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 56961 47 0 0 25 0 1 0 491724299 39747584 8861 4294967295 134512640 134672761 3221224544 3221223524 1075351233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 8861 603 41 0 9663 0
vsize: 38816
[startup+580.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 57961 47 0 0 25 0 1 0 491724299 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+590.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 58961 47 0 0 25 0 1 0 491724299 39223296 8788 4294967295 134512640 134672761 3221224544 3221223680 134614661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+600.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 59961 47 0 0 25 0 1 0 491724299 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+610.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 60961 48 0 0 25 0 1 0 491724299 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+620.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 61961 48 0 0 25 0 1 0 491724299 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+630.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 62961 48 0 0 25 0 1 0 491724299 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+640.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9800 0 0 0 63961 48 0 0 25 0 1 0 491724299 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+650.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9801 0 0 0 64961 49 0 0 25 0 1 0 491724299 39223296 8789 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8789 603 41 0 9535 0
vsize: 38304
[startup+660.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9803 0 0 0 65961 49 0 0 25 0 1 0 491724299 39223296 8791 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8791 603 41 0 9535 0
vsize: 38304
[startup+670.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9803 0 0 0 66961 49 0 0 25 0 1 0 491724299 39223296 8791 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8791 603 41 0 9535 0
vsize: 38304
[startup+680.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9807 0 0 0 67960 50 0 0 25 0 1 0 491724299 39223296 8795 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8795 603 41 0 9535 0
vsize: 38304
[startup+690.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9810 0 0 0 68960 50 0 0 25 0 1 0 491724299 39223296 8798 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8798 603 41 0 9535 0
vsize: 38304
[startup+700.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9924 0 0 0 69960 50 0 0 25 0 1 0 491724299 39878656 8912 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9736 8912 603 41 0 9695 0
vsize: 38944
[startup+710.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9930 0 0 0 70960 51 0 0 25 0 1 0 491724299 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8838 603 41 0 9567 0
vsize: 38432
[startup+720.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9930 0 0 0 71960 51 0 0 25 0 1 0 491724299 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8838 603 41 0 9567 0
vsize: 38432
[startup+730.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9930 0 0 0 72960 51 0 0 25 0 1 0 491724299 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8838 603 41 0 9567 0
vsize: 38432
[startup+740.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9931 0 0 0 73959 52 0 0 25 0 1 0 491724299 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+750.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9931 0 0 0 74959 52 0 0 25 0 1 0 491724299 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+760.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9931 0 0 0 75959 52 0 0 25 0 1 0 491724299 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+770.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9931 0 0 0 76959 53 0 0 25 0 1 0 491724299 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+780.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9942 0 0 0 77959 53 0 0 25 0 1 0 491724299 39550976 8850 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8850 603 41 0 9615 0
vsize: 38624
[startup+790.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9955 0 0 0 78959 53 0 0 25 0 1 0 491724299 39550976 8863 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8863 603 41 0 9615 0
vsize: 38624
[startup+800.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9956 0 0 0 79958 54 0 0 25 0 1 0 491724299 39550976 8864 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8864 603 41 0 9615 0
vsize: 38624
[startup+810.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9967 0 0 0 80957 54 0 0 25 0 1 0 491724299 39550976 8875 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8875 603 41 0 9615 0
vsize: 38624
[startup+820.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9970 0 0 0 81958 54 0 0 25 0 1 0 491724299 39550976 8878 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8878 603 41 0 9615 0
vsize: 38624
[startup+830.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 9970 0 0 0 82958 54 0 0 25 0 1 0 491724299 39550976 8878 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8878 603 41 0 9615 0
vsize: 38624
[startup+840.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10002 0 0 0 83958 54 0 0 25 0 1 0 491724299 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9704 8910 603 41 0 9663 0
vsize: 38816
[startup+850.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10002 0 0 0 84958 54 0 0 25 0 1 0 491724299 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9704 8910 603 41 0 9663 0
vsize: 38816
[startup+860.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10023 0 0 0 85958 54 0 0 25 0 1 0 491724299 40009728 8931 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9768 8931 603 41 0 9727 0
vsize: 39072
[startup+870.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10055 0 0 0 86959 54 0 0 25 0 1 0 491724299 40009728 8963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9768 8963 603 41 0 9727 0
vsize: 39072
[startup+880.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10168 0 0 0 87959 55 0 0 25 0 1 0 491724299 40796160 9076 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9960 9076 603 41 0 9919 0
vsize: 39840
[startup+890.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10168 0 0 0 88959 55 0 0 25 0 1 0 491724299 40271872 8996 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8996 603 41 0 9791 0
vsize: 39328
[startup+900.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10168 0 0 0 89959 55 0 0 25 0 1 0 491724299 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8996 603 41 0 9791 0
vsize: 39328
[startup+910.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10168 0 0 0 90959 55 0 0 25 0 1 0 491724299 40271872 8996 4294967295 134512640 134672761 3221224544 3221223584 134614340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8996 603 41 0 9791 0
vsize: 39328
[startup+920.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10169 0 0 0 91959 55 0 0 25 0 1 0 491724299 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+930.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10169 0 0 0 92959 55 0 0 25 0 1 0 491724299 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+940.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10169 0 0 0 93960 55 0 0 25 0 1 0 491724299 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+950.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10169 0 0 0 94960 55 0 0 25 0 1 0 491724299 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+960.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10169 0 0 0 95960 55 0 0 25 0 1 0 491724299 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+970.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10413 0 0 0 96959 55 0 0 25 0 1 0 491724299 41336832 9241 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9241 603 41 0 10051 0
vsize: 40368
[startup+980.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 10830 0 0 0 97959 56 0 0 25 0 1 0 491724299 43057152 9658 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10512 9658 603 41 0 10471 0
vsize: 42048
[startup+990.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 11196 0 0 0 98958 57 0 0 25 0 1 0 491724299 44515328 10024 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10024 603 41 0 10827 0
vsize: 43472
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 11598 0 0 0 99957 59 0 0 25 0 1 0 491724299 46161920 10426 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11270 10426 603 41 0 11229 0
vsize: 45080
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 11999 0 0 0 100956 60 0 0 25 0 1 0 491724299 47882240 10827 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11690 10827 603 41 0 11649 0
vsize: 46760
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 101955 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 102955 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 103955 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 104955 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 105956 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 106956 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 107956 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12170 0 0 0 108956 60 0 0 25 0 1 0 491724299 48349184 10909 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12189 0 0 0 109956 60 0 0 25 0 1 0 491724299 48545792 10928 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11852 10928 603 41 0 11811 0
vsize: 47408
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12457 0 0 0 110956 61 0 0 25 0 1 0 491724299 49598464 11196 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12109 11196 603 41 0 12068 0
vsize: 48436
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 12854 0 0 0 111954 62 0 0 25 0 1 0 491724299 51318784 11593 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12529 11593 603 41 0 12488 0
vsize: 50116
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 13159 0 0 0 112954 63 0 0 25 0 1 0 491724299 52506624 11898 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12819 11898 603 41 0 12778 0
vsize: 51276
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 13402 0 0 0 113953 64 0 0 25 0 1 0 491724299 53563392 12141 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13077 12141 603 41 0 13036 0
vsize: 52308
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 13702 0 0 0 114952 66 0 0 25 0 1 0 491724299 54747136 12441 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13366 12441 603 41 0 13325 0
vsize: 53464
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 13976 0 0 0 115951 67 0 0 25 0 1 0 491724299 55820288 12715 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13628 12715 603 41 0 13587 0
vsize: 54512
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 14224 0 0 0 116951 67 0 0 25 0 1 0 491724299 56885248 12963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13888 12963 603 41 0 13847 0
vsize: 55552
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 14506 0 0 0 117950 68 0 0 25 0 1 0 491724299 58073088 13245 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14178 13245 603 41 0 14137 0
vsize: 56712
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 14778 0 0 0 118949 69 0 0 25 0 1 0 491724299 59260928 13517 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14468 13517 603 41 0 14427 0
vsize: 57872
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25309
Raw data (stat): 25252 (minisat+) R 25251 10720 10719 0 -1 0 15018 0 0 0 119947 70 0 0 25 0 1 0 491724299 60198912 13757 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14697 13757 603 41 0 14656 0
vsize: 58788
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 25309
Raw data (stat): 25252 (minisat+) Z 25251 10720 10719 0 -1 12 15019 0 0 0 119947 73 0 0 25 0 1 0 491724299 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.48
CPU system time (s): 0.735888
CPU usage (%): 100.013
Max. virtual memory (Kb): 58788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####