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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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	15249
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.38
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 19012

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        812108 kB
Buffers:         25736 kB
Cached:         175520 kB
SwapCached:        364 kB
Active:          31992 kB
Inactive:       171800 kB
HighTotal:      131008 kB
HighFree:        91448 kB
LowTotal:       903652 kB
LowFree:        720660 kB
SwapTotal:     2097136 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6400 kB
Slab:            13184 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:46:14 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 17158 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.78366 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.84 0.95 0.98 2/54 10874
Raw data (stat): 10874 (runsolver) R 10873 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488641998 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99951 s]
Raw data (loadavg): 0.87 0.95 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 4258 0 0 0 987 11 0 0 25 0 1 0 488641998 17641472 3655 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.001 s]
Raw data (loadavg): 0.89 0.95 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 4513 0 0 0 1985 12 0 0 25 0 1 0 488641998 18710528 3910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4568 3910 603 41 0 4527 0
vsize: 18272
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.95 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 4998 0 0 0 2984 14 0 0 25 0 1 0 488641998 20844544 4395 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5089 4395 603 41 0 5048 0
vsize: 20356
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.95 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 5474 0 0 0 3983 15 0 0 25 0 1 0 488641998 22695936 4871 4294967295 134512640 134672761 3221224544 3221223680 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5541 4871 603 41 0 5500 0
vsize: 22164
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 5827 0 0 0 4983 16 0 0 25 0 1 0 488641998 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5867 5177 603 41 0 5826 0
vsize: 23468
[startup+60.0021 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 5827 0 0 0 5983 16 0 0 25 0 1 0 488641998 24031232 5177 4294967295 134512640 134672761 3221224544 3221223680 134614733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5867 5177 603 41 0 5826 0
vsize: 23468
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 5827 0 0 0 6983 16 0 0 25 0 1 0 488641998 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5867 5177 603 41 0 5826 0
vsize: 23468
[startup+80.0032 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 6225 0 0 0 7982 17 0 0 25 0 1 0 488641998 25759744 5575 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6289 5575 603 41 0 6248 0
vsize: 25156
[startup+90.0027 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 6585 0 0 0 8981 18 0 0 25 0 1 0 488641998 27213824 5935 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6644 5935 603 41 0 6603 0
vsize: 26576
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 6940 0 0 0 9980 19 0 0 25 0 1 0 488641998 28676096 6290 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7001 6290 603 41 0 6960 0
vsize: 28004
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7208 0 0 0 10979 20 0 0 25 0 1 0 488641998 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+120.004 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7208 0 0 0 11979 20 0 0 25 0 1 0 488641998 29532160 6534 4294967295 134512640 134672761 3221224544 3221221856 1075044273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+130.005 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7208 0 0 0 12980 20 0 0 25 0 1 0 488641998 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7208 0 0 0 13980 20 0 0 25 0 1 0 488641998 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7210 6534 603 41 0 7169 0
vsize: 28840
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7209 0 0 0 14980 20 0 0 25 0 1 0 488641998 29532160 6535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7210 6535 603 41 0 7169 0
vsize: 28840
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7209 0 0 0 15980 20 0 0 25 0 1 0 488641998 29532160 6535 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7210 6535 603 41 0 7169 0
vsize: 28840
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7332 0 0 0 16980 21 0 0 25 0 1 0 488641998 30060544 6658 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6658 603 41 0 7298 0
vsize: 29356
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7547 0 0 0 17980 21 0 0 25 0 1 0 488641998 30990336 6873 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7566 6873 603 41 0 7525 0
vsize: 30264
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7861 0 0 0 18979 22 0 0 25 0 1 0 488641998 32288768 7187 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7883 7187 603 41 0 7842 0
vsize: 31532
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7864 0 0 0 19979 22 0 0 25 0 1 0 488641998 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7864 0 0 0 20980 22 0 0 25 0 1 0 488641998 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7864 0 0 0 21980 22 0 0 25 0 1 0 488641998 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7864 0 0 0 22980 22 0 0 25 0 1 0 488641998 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7865 0 0 0 23980 22 0 0 25 0 1 0 488641998 32026624 7130 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7130 603 41 0 7778 0
vsize: 31276
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7865 0 0 0 24980 22 0 0 25 0 1 0 488641998 32026624 7130 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7130 603 41 0 7778 0
vsize: 31276
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7866 0 0 0 25981 22 0 0 25 0 1 0 488641998 32026624 7131 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7131 603 41 0 7778 0
vsize: 31276
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7867 0 0 0 26981 22 0 0 25 0 1 0 488641998 32026624 7132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7132 603 41 0 7778 0
vsize: 31276
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7870 0 0 0 27981 22 0 0 25 0 1 0 488641998 32288768 7135 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7883 7135 603 41 0 7842 0
vsize: 31532
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 28981 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+300.009 s]
Raw data (loadavg): 1.07 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 29981 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+310.008 s]
Raw data (loadavg): 1.06 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 30981 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7176 603 41 0 7874 0
vsize: 31660
[startup+320.009 s]
Raw data (loadavg): 1.05 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 31981 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 32982 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 33982 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 34982 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 35982 22 0 0 25 0 1 0 488641998 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7978 0 0 0 36981 22 0 0 25 0 1 0 488641998 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.02 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 7979 0 0 0 37981 22 0 0 25 0 1 0 488641998 32419840 7177 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7177 603 41 0 7874 0
vsize: 31660
[startup+390.01 s]
Raw data (loadavg): 1.01 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8078 0 0 0 38981 22 0 0 25 0 1 0 488641998 32964608 7276 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8048 7276 603 41 0 8007 0
vsize: 32192
[startup+400.01 s]
Raw data (loadavg): 1.01 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8287 0 0 0 39981 23 0 0 25 0 1 0 488641998 33779712 7485 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8247 7485 603 41 0 8206 0
vsize: 32988
[startup+410.01 s]
Raw data (loadavg): 1.01 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8496 0 0 0 40981 23 0 0 25 0 1 0 488641998 34107392 7589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7589 603 41 0 8286 0
vsize: 33308
[startup+420.011 s]
Raw data (loadavg): 1.01 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8496 0 0 0 41981 23 0 0 25 0 1 0 488641998 34107392 7589 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8496 0 0 0 42981 23 0 0 25 0 1 0 488641998 34107392 7589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7589 603 41 0 8286 0
vsize: 33308
[startup+440.012 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8506 0 0 0 43982 23 0 0 25 0 1 0 488641998 34287616 7599 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8371 7599 603 41 0 8330 0
vsize: 33484
[startup+450.012 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8523 0 0 0 44982 23 0 0 25 0 1 0 488641998 34287616 7616 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8371 7616 603 41 0 8330 0
vsize: 33484
[startup+460.012 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8545 0 0 0 45982 23 0 0 25 0 1 0 488641998 34451456 7638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7638 603 41 0 8370 0
vsize: 33644
[startup+470.012 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8546 0 0 0 46982 23 0 0 25 0 1 0 488641998 34451456 7639 4294967295 134512640 134672761 3221224544 3221223584 134612838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7639 603 41 0 8370 0
vsize: 33644
[startup+480.012 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8571 0 0 0 47982 23 0 0 25 0 1 0 488641998 34615296 7664 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8451 7664 603 41 0 8410 0
vsize: 33804
[startup+490.012 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8573 0 0 0 48982 23 0 0 25 0 1 0 488641998 34615296 7666 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8604 0 0 0 49983 23 0 0 25 0 1 0 488641998 34779136 7697 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8491 7697 603 41 0 8450 0
vsize: 33964
[startup+510.014 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8653 0 0 0 50982 24 0 0 25 0 1 0 488641998 34967552 7746 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8537 7746 603 41 0 8496 0
vsize: 34148
[startup+520.013 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 8888 0 0 0 51982 24 0 0 25 0 1 0 488641998 35946496 7981 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8776 7981 603 41 0 8735 0
vsize: 35104
[startup+530.015 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9074 0 0 0 52982 24 0 0 25 0 1 0 488641998 36610048 8167 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8938 8167 603 41 0 8897 0
vsize: 35752
[startup+540.014 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9259 0 0 0 53982 25 0 0 25 0 1 0 488641998 37457920 8352 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9145 8352 603 41 0 9104 0
vsize: 36580
[startup+550.014 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9458 0 0 0 54982 25 0 0 25 0 1 0 488641998 38244352 8551 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9337 8551 603 41 0 9296 0
vsize: 37348
[startup+560.014 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9628 0 0 0 55981 26 0 0 25 0 1 0 488641998 39088128 8721 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9543 8721 603 41 0 9502 0
vsize: 38172
[startup+570.016 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9800 0 0 0 56981 26 0 0 25 0 1 0 488641998 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+580.016 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9800 0 0 0 57981 26 0 0 25 0 1 0 488641998 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9800 0 0 0 58981 26 0 0 25 0 1 0 488641998 39223296 8788 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9800 0 0 0 59981 26 0 0 25 0 1 0 488641998 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+610.016 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9800 0 0 0 60982 26 0 0 25 0 1 0 488641998 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9800 0 0 0 61982 26 0 0 25 0 1 0 488641998 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+630.017 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9800 0 0 0 62982 26 0 0 25 0 1 0 488641998 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8788 603 41 0 9535 0
vsize: 38304
[startup+640.017 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9801 0 0 0 63982 26 0 0 25 0 1 0 488641998 39223296 8789 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8789 603 41 0 9535 0
vsize: 38304
[startup+650.017 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9802 0 0 0 64982 26 0 0 25 0 1 0 488641998 39223296 8790 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8790 603 41 0 9535 0
vsize: 38304
[startup+660.018 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9803 0 0 0 65982 26 0 0 25 0 1 0 488641998 39223296 8791 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8791 603 41 0 9535 0
vsize: 38304
[startup+670.017 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9806 0 0 0 66983 26 0 0 25 0 1 0 488641998 39223296 8794 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8794 603 41 0 9535 0
vsize: 38304
[startup+680.018 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9809 0 0 0 67983 26 0 0 25 0 1 0 488641998 39223296 8797 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8797 603 41 0 9535 0
vsize: 38304
[startup+690.018 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9812 0 0 0 68983 26 0 0 25 0 1 0 488641998 39223296 8800 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8800 603 41 0 9535 0
vsize: 38304
[startup+700.018 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9930 0 0 0 69983 27 0 0 25 0 1 0 488641998 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8838 603 41 0 9567 0
vsize: 38432
[startup+710.018 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9930 0 0 0 70983 27 0 0 25 0 1 0 488641998 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 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.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9930 0 0 0 71983 27 0 0 25 0 1 0 488641998 39354368 8838 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8838 603 41 0 9567 0
vsize: 38432
[startup+730.019 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9931 0 0 0 72984 27 0 0 25 0 1 0 488641998 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+740.019 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9931 0 0 0 73984 27 0 0 25 0 1 0 488641998 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9931 0 0 0 74984 27 0 0 25 0 1 0 488641998 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+760.019 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9931 0 0 0 75984 27 0 0 25 0 1 0 488641998 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+770.019 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9931 0 0 0 76984 27 0 0 25 0 1 0 488641998 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+780.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9954 0 0 0 77984 27 0 0 25 0 1 0 488641998 39550976 8862 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8862 603 41 0 9615 0
vsize: 38624
[startup+790.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9955 0 0 0 78984 27 0 0 25 0 1 0 488641998 39550976 8863 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8863 603 41 0 9615 0
vsize: 38624
[startup+800.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9967 0 0 0 79985 27 0 0 25 0 1 0 488641998 39550976 8875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8875 603 41 0 9615 0
vsize: 38624
[startup+810.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9969 0 0 0 80985 27 0 0 25 0 1 0 488641998 39550976 8877 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8877 603 41 0 9615 0
vsize: 38624
[startup+820.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9970 0 0 0 81985 27 0 0 25 0 1 0 488641998 39550976 8878 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 9984 0 0 0 82985 27 0 0 25 0 1 0 488641998 39747584 8892 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9704 8892 603 41 0 9663 0
vsize: 38816
[startup+840.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10002 0 0 0 83985 27 0 0 25 0 1 0 488641998 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615758 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.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10002 0 0 0 84985 27 0 0 25 0 1 0 488641998 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.02 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10053 0 0 0 85985 27 0 0 25 0 1 0 488641998 40009728 8961 4294967295 134512640 134672761 3221224544 3221223728 134615622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9768 8961 603 41 0 9727 0
vsize: 39072
[startup+870.022 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10168 0 0 0 86986 27 0 0 25 0 1 0 488641998 40796160 9076 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9960 9076 603 41 0 9919 0
vsize: 39840
[startup+880.021 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10168 0 0 0 87986 27 0 0 25 0 1 0 488641998 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+890.022 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10168 0 0 0 88986 27 0 0 25 0 1 0 488641998 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134615830 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.023 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10168 0 0 0 89986 27 0 0 25 0 1 0 488641998 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.022 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10169 0 0 0 90986 27 0 0 25 0 1 0 488641998 40271872 8997 4294967295 134512640 134672761 3221224544 3221223584 134612486 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+920.024 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10169 0 0 0 91986 27 0 0 25 0 1 0 488641998 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.025 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10169 0 0 0 92987 27 0 0 25 0 1 0 488641998 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615571 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.025 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10169 0 0 0 93987 27 0 0 25 0 1 0 488641998 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615671 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.025 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10169 0 0 0 94987 27 0 0 25 0 1 0 488641998 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615564 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.025 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10244 0 0 0 95987 27 0 0 25 0 1 0 488641998 40665088 9072 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9928 9072 603 41 0 9887 0
vsize: 39712
[startup+970.025 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 10650 0 0 0 96986 29 0 0 25 0 1 0 488641998 42266624 9478 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10319 9478 603 41 0 10278 0
vsize: 41276
[startup+980.026 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 11045 0 0 0 97985 30 0 0 25 0 1 0 488641998 43991040 9873 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10740 9873 603 41 0 10699 0
vsize: 42960
[startup+990.025 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 11443 0 0 0 98984 31 0 0 25 0 1 0 488641998 45629440 10271 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11140 10271 603 41 0 11099 0
vsize: 44560
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 11823 0 0 0 99983 32 0 0 25 0 1 0 488641998 47087616 10651 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11496 10651 603 41 0 11455 0
vsize: 45984
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 100982 33 0 0 25 0 1 0 488641998 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+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 101982 33 0 0 25 0 1 0 488641998 48349184 10909 4294967295 134512640 134672761 3221224544 3221223584 134613748 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.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 102983 33 0 0 25 0 1 0 488641998 48349184 10909 4294967295 134512640 134672761 3221224544 3221223584 134613818 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.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 103983 33 0 0 25 0 1 0 488641998 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+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 104983 33 0 0 25 0 1 0 488641998 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 105983 33 0 0 25 0 1 0 488641998 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615804 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.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 106983 33 0 0 25 0 1 0 488641998 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+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 107984 33 0 0 25 0 1 0 488641998 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.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12170 0 0 0 108984 33 0 0 25 0 1 0 488641998 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+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12210 0 0 0 109983 33 0 0 25 0 1 0 488641998 48676864 10949 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11884 10949 603 41 0 11843 0
vsize: 47536
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 12650 0 0 0 110982 35 0 0 25 0 1 0 488641998 50384896 11389 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12301 11389 603 41 0 12260 0
vsize: 49204
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 13003 0 0 0 111981 37 0 0 25 0 1 0 488641998 51843072 11742 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12657 11742 603 41 0 12616 0
vsize: 50628
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 13264 0 0 0 112981 37 0 0 25 0 1 0 488641998 53039104 12003 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12003 603 41 0 12908 0
vsize: 51796
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 13517 0 0 0 113980 38 0 0 25 0 1 0 488641998 53960704 12256 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13174 12256 603 41 0 13133 0
vsize: 52696
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 13803 0 0 0 114980 38 0 0 25 0 1 0 488641998 55148544 12542 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13464 12542 603 41 0 13423 0
vsize: 53856
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 14073 0 0 0 115979 39 0 0 25 0 1 0 488641998 56352768 12812 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13758 12812 603 41 0 13717 0
vsize: 55032
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 14334 0 0 0 116978 40 0 0 25 0 1 0 488641998 57413632 13073 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13073 603 41 0 13976 0
vsize: 56068
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 14610 0 0 0 117978 41 0 0 25 0 1 0 488641998 58466304 13349 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14274 13349 603 41 0 14233 0
vsize: 57096
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 14867 0 0 0 118977 42 0 0 25 0 1 0 488641998 59523072 13606 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14532 13606 603 41 0 14491 0
vsize: 58128
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.98 2/54 10874
Raw data (stat): 10874 (minisat+) R 10873 5897 5896 0 -1 0 15102 0 0 0 119976 43 0 0 25 0 1 0 488641998 60592128 13841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14793 13841 603 41 0 14752 0
vsize: 59172
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.98 1/54 10874
Raw data (stat): 10874 (minisat+) Z 10873 5897 5896 0 -1 12 15103 0 0 0 119977 45 0 0 25 0 1 0 488641998 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.07
CPU time (s): 1200.23
CPU user time (s): 1199.77
CPU system time (s): 0.45993
CPU usage (%): 100.014
Max. virtual memory (Kb): 59172
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####