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/miplib3/normalized-mps-v2-20-10-p0548.opb
MD5SUM	10547c6c0f11ab5df74fcaff6ba6d160
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	1230.87
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 16284

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 06:46:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13739 boxname=wulflinc29 idbench=1057 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-p0548.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 13739
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        740540 kB
Buffers:         24240 kB
Cached:         241992 kB
SwapCached:        464 kB
Active:          53416 kB
Inactive:       215040 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        740288 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20016 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:06:25 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 13739 7 1200.23 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.81866 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.91 0.95 0.91 2/54 24754
Raw data (stat): 24754 (runsolver) R 24753 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543025438 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 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 4258 0 0 0 988 10 0 0 25 0 1 0 543025438 17641472 3655 4294967295 134512640 134672761 3221224544 3221223640 134616254 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.0003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 4506 0 0 0 1986 11 0 0 25 0 1 0 543025438 18710528 3903 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4568 3903 603 41 0 4527 0
vsize: 18272
[startup+30.0005 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 4994 0 0 0 2984 12 0 0 25 0 1 0 543025438 20844544 4391 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4391 603 41 0 5048 0
vsize: 20356
[startup+40.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 5472 0 0 0 3983 14 0 0 25 0 1 0 543025438 22695936 4869 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5541 4869 603 41 0 5500 0
vsize: 22164
[startup+50.0003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 5827 0 0 0 4982 15 0 0 25 0 1 0 543025438 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615758 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.0009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 5827 0 0 0 5982 15 0 0 25 0 1 0 543025438 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615632 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.0009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 5827 0 0 0 6983 15 0 0 25 0 1 0 543025438 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615608 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.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 6235 0 0 0 7982 16 0 0 25 0 1 0 543025438 25759744 5585 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6289 5585 603 41 0 6248 0
vsize: 25156
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 6600 0 0 0 8980 18 0 0 25 0 1 0 543025438 27213824 5950 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6644 5950 603 41 0 6603 0
vsize: 26576
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 6959 0 0 0 9980 18 0 0 25 0 1 0 543025438 28676096 6309 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7001 6309 603 41 0 6960 0
vsize: 28004
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7208 0 0 0 10979 19 0 0 25 0 1 0 543025438 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615916 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7208 0 0 0 11980 19 0 0 25 0 1 0 543025438 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7208 0 0 0 12980 19 0 0 25 0 1 0 543025438 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615663 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7208 0 0 0 13980 19 0 0 25 0 1 0 543025438 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7209 0 0 0 14980 19 0 0 25 0 1 0 543025438 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7209 0 0 0 15980 19 0 0 25 0 1 0 543025438 29532160 6535 4294967295 134512640 134672761 3221224544 3221223720 134553585 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7361 0 0 0 16980 20 0 0 25 0 1 0 543025438 30195712 6687 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6687 603 41 0 7331 0
vsize: 29488
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7581 0 0 0 17979 20 0 0 25 0 1 0 543025438 31121408 6907 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7598 6907 603 41 0 7557 0
vsize: 30392
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7864 0 0 0 18978 22 0 0 25 0 1 0 543025438 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7864 0 0 0 19978 22 0 0 25 0 1 0 543025438 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7864 0 0 0 20978 22 0 0 25 0 1 0 543025438 32026624 7129 4294967295 134512640 134672761 3221224544 3221223584 134614348 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7864 0 0 0 21978 22 0 0 25 0 1 0 543025438 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+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7864 0 0 0 22979 22 0 0 25 0 1 0 543025438 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7865 0 0 0 23979 22 0 0 25 0 1 0 543025438 32026624 7130 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7130 603 41 0 7778 0
vsize: 31276
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7866 0 0 0 24979 22 0 0 25 0 1 0 543025438 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+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7866 0 0 0 25979 22 0 0 25 0 1 0 543025438 32026624 7131 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7868 0 0 0 26979 23 0 0 25 0 1 0 543025438 32026624 7133 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7133 603 41 0 7778 0
vsize: 31276
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7871 0 0 0 27979 23 0 0 25 0 1 0 543025438 32288768 7136 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7883 7136 603 41 0 7842 0
vsize: 31532
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 28979 23 0 0 25 0 1 0 543025438 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+300.007 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 29979 23 0 0 25 0 1 0 543025438 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+310.008 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 30979 23 0 0 25 0 1 0 543025438 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615804 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.009 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 31979 23 0 0 25 0 1 0 543025438 32419840 7176 4294967295 134512640 134672761 3221224544 3221223584 134612478 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.009 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 32979 23 0 0 25 0 1 0 543025438 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+340.009 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 33980 23 0 0 25 0 1 0 543025438 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615937 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.03 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 34980 23 0 0 25 0 1 0 543025438 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615693 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.02 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 35980 23 0 0 25 0 1 0 543025438 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615632 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.02 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7978 0 0 0 36980 23 0 0 25 0 1 0 543025438 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.01 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 7979 0 0 0 37980 23 0 0 25 0 1 0 543025438 32419840 7177 4294967295 134512640 134672761 3221224544 3221223584 134614228 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.01 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8151 0 0 0 38980 24 0 0 25 0 1 0 543025438 33230848 7349 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8113 7349 603 41 0 8072 0
vsize: 32452
[startup+400.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8489 0 0 0 39979 25 0 0 25 0 1 0 543025438 34631680 7655 4294967295 134512640 134672761 3221224544 3221223600 134644281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8455 7655 603 41 0 8414 0
vsize: 33820
[startup+410.012 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8496 0 0 0 40980 25 0 0 25 0 1 0 543025438 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+420.012 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8496 0 0 0 41980 25 0 0 25 0 1 0 543025438 34107392 7589 4294967295 134512640 134672761 3221224544 3221223728 134616005 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.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8497 0 0 0 42980 25 0 0 25 0 1 0 543025438 34107392 7590 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 7590 603 41 0 8286 0
vsize: 33308
[startup+440.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8519 0 0 0 43980 25 0 0 25 0 1 0 543025438 34287616 7612 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8371 7612 603 41 0 8330 0
vsize: 33484
[startup+450.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8542 0 0 0 44980 25 0 0 25 0 1 0 543025438 34451456 7635 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7635 603 41 0 8370 0
vsize: 33644
[startup+460.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8546 0 0 0 45980 25 0 0 25 0 1 0 543025438 34451456 7639 4294967295 134512640 134672761 3221224544 3221223584 134614223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7639 603 41 0 8370 0
vsize: 33644
[startup+470.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8553 0 0 0 46980 25 0 0 25 0 1 0 543025438 34451456 7646 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7646 603 41 0 8370 0
vsize: 33644
[startup+480.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8572 0 0 0 47980 26 0 0 25 0 1 0 543025438 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+490.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8573 0 0 0 48980 26 0 0 25 0 1 0 543025438 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+500.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8609 0 0 0 49980 26 0 0 25 0 1 0 543025438 34779136 7702 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8491 7702 603 41 0 8450 0
vsize: 33964
[startup+510.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 8773 0 0 0 50980 27 0 0 25 0 1 0 543025438 35418112 7866 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8647 7866 603 41 0 8606 0
vsize: 34588
[startup+520.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9003 0 0 0 51979 27 0 0 25 0 1 0 543025438 36347904 8096 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8096 603 41 0 8833 0
vsize: 35496
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9178 0 0 0 52978 28 0 0 25 0 1 0 543025438 37195776 8271 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9081 8271 603 41 0 9040 0
vsize: 36324
[startup+540.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9371 0 0 0 53978 29 0 0 25 0 1 0 543025438 37982208 8464 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9273 8464 603 41 0 9232 0
vsize: 37092
[startup+550.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9558 0 0 0 54977 30 0 0 25 0 1 0 543025438 38776832 8651 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9467 8651 603 41 0 9426 0
vsize: 37868
[startup+560.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9800 0 0 0 55976 31 0 0 25 0 1 0 543025438 39747584 8861 4294967295 134512640 134672761 3221224544 3221223600 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 8861 603 41 0 9663 0
vsize: 38816
[startup+570.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9800 0 0 0 56976 31 0 0 25 0 1 0 543025438 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+580.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9800 0 0 0 57977 31 0 0 25 0 1 0 543025438 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615627 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.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9800 0 0 0 58977 31 0 0 25 0 1 0 543025438 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9800 0 0 0 59977 31 0 0 25 0 1 0 543025438 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+610.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9800 0 0 0 60977 31 0 0 25 0 1 0 543025438 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615665 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.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9800 0 0 0 61977 31 0 0 25 0 1 0 543025438 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615671 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9801 0 0 0 62978 31 0 0 25 0 1 0 543025438 39223296 8789 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8789 603 41 0 9535 0
vsize: 38304
[startup+640.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9801 0 0 0 63978 31 0 0 25 0 1 0 543025438 39223296 8789 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8789 603 41 0 9535 0
vsize: 38304
[startup+650.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9803 0 0 0 64978 31 0 0 25 0 1 0 543025438 39223296 8791 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8791 603 41 0 9535 0
vsize: 38304
[startup+660.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9805 0 0 0 65978 31 0 0 25 0 1 0 543025438 39223296 8793 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8793 603 41 0 9535 0
vsize: 38304
[startup+670.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9808 0 0 0 66978 32 0 0 25 0 1 0 543025438 39223296 8796 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8796 603 41 0 9535 0
vsize: 38304
[startup+680.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9811 0 0 0 67978 32 0 0 25 0 1 0 543025438 39223296 8799 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 8799 603 41 0 9535 0
vsize: 38304
[startup+690.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9930 0 0 0 68978 32 0 0 25 0 1 0 543025438 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8838 603 41 0 9567 0
vsize: 38432
[startup+700.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9930 0 0 0 69978 32 0 0 25 0 1 0 543025438 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 8838 603 41 0 9567 0
vsize: 38432
[startup+710.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9930 0 0 0 70979 32 0 0 25 0 1 0 543025438 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.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9931 0 0 0 71979 32 0 0 25 0 1 0 543025438 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+730.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9931 0 0 0 72979 32 0 0 25 0 1 0 543025438 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+740.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9931 0 0 0 73979 32 0 0 25 0 1 0 543025438 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615720 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.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9931 0 0 0 74979 32 0 0 25 0 1 0 543025438 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9931 0 0 0 75979 32 0 0 25 0 1 0 543025438 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.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9954 0 0 0 76979 32 0 0 25 0 1 0 543025438 39550976 8862 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8862 603 41 0 9615 0
vsize: 38624
[startup+780.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9955 0 0 0 77980 32 0 0 25 0 1 0 543025438 39550976 8863 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8863 603 41 0 9615 0
vsize: 38624
[startup+790.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9967 0 0 0 78980 32 0 0 25 0 1 0 543025438 39550976 8875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8875 603 41 0 9615 0
vsize: 38624
[startup+800.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9969 0 0 0 79980 32 0 0 25 0 1 0 543025438 39550976 8877 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8877 603 41 0 9615 0
vsize: 38624
[startup+810.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9970 0 0 0 80980 32 0 0 25 0 1 0 543025438 39550976 8878 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8878 603 41 0 9615 0
vsize: 38624
[startup+820.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24754
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 9983 0 0 0 81980 32 0 0 25 0 1 0 543025438 39747584 8891 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 8891 603 41 0 9663 0
vsize: 38816
[startup+830.022 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 24807
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10002 0 0 0 82978 34 0 0 25 0 1 0 543025438 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 8910 603 41 0 9663 0
vsize: 38816
[startup+840.023 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 24807
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10002 0 0 0 83978 34 0 0 25 0 1 0 543025438 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 8910 603 41 0 9663 0
vsize: 38816
[startup+850.023 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 24807
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10052 0 0 0 84978 34 0 0 25 0 1 0 543025438 40009728 8960 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9768 8960 603 41 0 9727 0
vsize: 39072
[startup+860.023 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 24807
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10168 0 0 0 85979 34 0 0 25 0 1 0 543025438 40796160 9076 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9960 9076 603 41 0 9919 0
vsize: 39840
[startup+870.023 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 24807
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10168 0 0 0 86979 34 0 0 25 0 1 0 543025438 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8996 603 41 0 9791 0
vsize: 39328
[startup+880.024 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 24807
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10168 0 0 0 87979 34 0 0 25 0 1 0 543025438 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8996 603 41 0 9791 0
vsize: 39328
[startup+890.023 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24807
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10168 0 0 0 88979 34 0 0 25 0 1 0 543025438 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8996 603 41 0 9791 0
vsize: 39328
[startup+900.023 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10169 0 0 0 89979 34 0 0 25 0 1 0 543025438 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+910.024 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10169 0 0 0 90979 34 0 0 25 0 1 0 543025438 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+920.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10169 0 0 0 91979 34 0 0 25 0 1 0 543025438 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+930.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10169 0 0 0 92980 34 0 0 25 0 1 0 543025438 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+940.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10169 0 0 0 93980 34 0 0 25 0 1 0 543025438 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+950.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10244 0 0 0 94980 34 0 0 25 0 1 0 543025438 40665088 9072 4294967295 134512640 134672761 3221224544 3221223560 134603109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9928 9072 603 41 0 9887 0
vsize: 39712
[startup+960.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 10656 0 0 0 95979 36 0 0 25 0 1 0 543025438 42266624 9484 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10319 9484 603 41 0 10278 0
vsize: 41276
[startup+970.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 11053 0 0 0 96978 37 0 0 25 0 1 0 543025438 43991040 9881 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10740 9881 603 41 0 10699 0
vsize: 42960
[startup+980.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 11456 0 0 0 97977 38 0 0 25 0 1 0 543025438 45629440 10284 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11140 10284 603 41 0 11099 0
vsize: 44560
[startup+990.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 11855 0 0 0 98976 39 0 0 25 0 1 0 543025438 47218688 10683 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11528 10683 603 41 0 11487 0
vsize: 46112
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 99975 40 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223480 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 100975 40 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 101976 40 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 102976 40 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 103975 40 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 104976 40 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 105976 40 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12170 0 0 0 106975 41 0 0 25 0 1 0 543025438 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12171 0 0 0 107976 41 0 0 25 0 1 0 543025438 48349184 10910 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11804 10910 603 41 0 11763 0
vsize: 47216
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12275 0 0 0 108976 41 0 0 25 0 1 0 543025438 48943104 11014 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11949 11014 603 41 0 11908 0
vsize: 47796
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 12722 0 0 0 109975 42 0 0 25 0 1 0 543025438 50782208 11461 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12398 11461 603 41 0 12357 0
vsize: 49592
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 13055 0 0 0 110974 43 0 0 25 0 1 0 543025438 52109312 11794 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12722 11794 603 41 0 12681 0
vsize: 50888
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 13313 0 0 0 111973 44 0 0 25 0 1 0 543025438 53170176 12052 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12981 12052 603 41 0 12940 0
vsize: 51924
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 13595 0 0 0 112973 45 0 0 25 0 1 0 543025438 54353920 12334 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13270 12334 603 41 0 13229 0
vsize: 53080
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 13865 0 0 0 113972 46 0 0 25 0 1 0 543025438 55418880 12604 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13530 12604 603 41 0 13489 0
vsize: 54120
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 14125 0 0 0 114971 47 0 0 25 0 1 0 543025438 56487936 12864 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 12864 603 41 0 13750 0
vsize: 55164
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 14403 0 0 0 115971 47 0 0 25 0 1 0 543025438 57679872 13142 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14082 13142 603 41 0 14041 0
vsize: 56328
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24809
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 14680 0 0 0 116970 48 0 0 25 0 1 0 543025438 58859520 13419 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13419 603 41 0 14329 0
vsize: 57480
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24811
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 14923 0 0 0 117970 48 0 0 25 0 1 0 543025438 59785216 13662 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14596 13662 603 41 0 14555 0
vsize: 58384
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24811
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 15173 0 0 0 118970 49 0 0 25 0 1 0 543025438 60858368 13912 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14858 13912 603 41 0 14817 0
vsize: 59432
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24811
Raw data (stat): 24754 (minisat+) R 24753 27222 27221 0 -1 0 15381 0 0 0 119969 50 0 0 25 0 1 0 543025438 61865984 14120 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15104 14120 603 41 0 15063 0
vsize: 60416
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 24811
Raw data (stat): 24754 (minisat+) Z 24753 27222 27221 0 -1 12 15382 0 0 0 119969 53 0 0 24 0 1 0 543025438 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.08
CPU time (s): 1200.23
CPU user time (s): 1199.69
CPU system time (s): 0.530919
CPU usage (%): 100.013
Max. virtual memory (Kb): 60416
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####