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/miplib3/normalized-mps-v2-13-7-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	1244.18
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 18199

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 13:53:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18731 boxname=wulflinc5 idbench=1441 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-p0548.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 18731
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        581460 kB
Buffers:         22060 kB
Cached:         408732 kB
SwapCached:        328 kB
Active:          58708 kB
Inactive:       374584 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        581208 kB
SwapTotal:     2097136 kB
SwapFree:      2096444 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            14232 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:13:41 (client local time) WITH STATUS 10 IN 1200.33 SECONDS
stats: 18731 7 1200.33 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.70568 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.64 0.88 0.92 1/54 23598
Raw data (stat): 23598 (runsolver) R 23597 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487371307 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.69 0.88 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 4258 0 0 0 987 11 0 0 25 0 1 0 487371307 17641472 3655 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4307 3655 603 41 0 4266 0
vsize: 17228
[startup+19.9997 s]
Raw data (loadavg): 0.74 0.89 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 4513 0 0 0 1985 12 0 0 25 0 1 0 487371307 18710528 3910 4294967295 134512640 134672761 3221224544 3221223728 134615758 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.0008 s]
Raw data (loadavg): 0.78 0.89 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 5002 0 0 0 2984 14 0 0 25 0 1 0 487371307 20844544 4399 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5089 4399 603 41 0 5048 0
vsize: 20356
[startup+40.0005 s]
Raw data (loadavg): 0.81 0.89 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 5486 0 0 0 3982 15 0 0 25 0 1 0 487371307 22831104 4883 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5574 4883 603 41 0 5533 0
vsize: 22296
[startup+50.001 s]
Raw data (loadavg): 0.84 0.89 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 5827 0 0 0 4981 17 0 0 25 0 1 0 487371307 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+60.0007 s]
Raw data (loadavg): 0.87 0.90 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 5827 0 0 0 5981 17 0 0 25 0 1 0 487371307 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615671 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.0007 s]
Raw data (loadavg): 0.89 0.90 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 5827 0 0 0 6982 17 0 0 25 0 1 0 487371307 24031232 5177 4294967295 134512640 134672761 3221224544 3221223728 134615736 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.0012 s]
Raw data (loadavg): 0.90 0.90 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 6253 0 0 0 7981 18 0 0 25 0 1 0 487371307 25890816 5603 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6321 5603 603 41 0 6280 0
vsize: 25284
[startup+90.0013 s]
Raw data (loadavg): 0.92 0.91 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 6612 0 0 0 8980 19 0 0 25 0 1 0 487371307 27344896 5962 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5962 603 41 0 6635 0
vsize: 26704
[startup+100.002 s]
Raw data (loadavg): 0.93 0.91 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 6973 0 0 0 9979 20 0 0 25 0 1 0 487371307 28807168 6323 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7033 6323 603 41 0 6992 0
vsize: 28132
[startup+110.002 s]
Raw data (loadavg): 0.94 0.91 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7208 0 0 0 10979 20 0 0 25 0 1 0 487371307 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615671 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.002 s]
Raw data (loadavg): 0.95 0.91 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7208 0 0 0 11979 20 0 0 25 0 1 0 487371307 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615564 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.002 s]
Raw data (loadavg): 0.96 0.92 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7208 0 0 0 12979 20 0 0 25 0 1 0 487371307 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134616011 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.002 s]
Raw data (loadavg): 0.96 0.92 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7208 0 0 0 13979 20 0 0 25 0 1 0 487371307 29532160 6534 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.003 s]
Raw data (loadavg): 0.97 0.92 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7209 0 0 0 14980 20 0 0 25 0 1 0 487371307 29532160 6535 4294967295 134512640 134672761 3221224544 3221223728 134615804 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.002 s]
Raw data (loadavg): 0.97 0.92 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7209 0 0 0 15980 20 0 0 25 0 1 0 487371307 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+170.002 s]
Raw data (loadavg): 0.98 0.92 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7374 0 0 0 16979 21 0 0 25 0 1 0 487371307 30330880 6700 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7405 6701 603 41 0 7364 0
vsize: 29620
[startup+180.002 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7600 0 0 0 17978 22 0 0 25 0 1 0 487371307 31252480 6926 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7630 6926 603 41 0 7589 0
vsize: 30520
[startup+190.002 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7864 0 0 0 18977 23 0 0 25 0 1 0 487371307 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7129 603 41 0 7778 0
vsize: 31276
[startup+200.002 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7864 0 0 0 19977 23 0 0 25 0 1 0 487371307 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615689 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.002 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7864 0 0 0 20978 23 0 0 25 0 1 0 487371307 32026624 7129 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.002 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7864 0 0 0 21978 23 0 0 25 0 1 0 487371307 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+230.002 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7864 0 0 0 22978 23 0 0 25 0 1 0 487371307 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+240.002 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7865 0 0 0 23978 23 0 0 25 0 1 0 487371307 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.003 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7866 0 0 0 24978 23 0 0 25 0 1 0 487371307 32026624 7131 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7131 603 41 0 7778 0
vsize: 31276
[startup+260.004 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7866 0 0 0 25979 23 0 0 25 0 1 0 487371307 32026624 7131 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.004 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7868 0 0 0 26979 23 0 0 25 0 1 0 487371307 32026624 7133 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7133 603 41 0 7778 0
vsize: 31276
[startup+280.004 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7871 0 0 0 27979 23 0 0 25 0 1 0 487371307 32288768 7136 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7883 7136 603 41 0 7842 0
vsize: 31532
[startup+290.005 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 28979 24 0 0 25 0 1 0 487371307 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615732 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.006 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 29979 24 0 0 25 0 1 0 487371307 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+310.006 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 30979 24 0 0 25 0 1 0 487371307 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.005 s]
Raw data (loadavg): 0.99 0.95 0.92 3/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 31979 24 0 0 25 0 1 0 487371307 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+330.006 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 32980 24 0 0 25 0 1 0 487371307 32419840 7176 4294967295 134512640 134672761 3221224544 3221223728 134615807 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.006 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 33980 24 0 0 25 0 1 0 487371307 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+350.006 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 34980 24 0 0 25 0 1 0 487371307 32419840 7176 4294967295 134512640 134672761 3221224544 3221223744 134610686 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.007 s]
Raw data (loadavg): 0.99 0.95 0.92 3/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7978 0 0 0 35980 24 0 0 25 0 1 0 487371307 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.007 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7979 0 0 0 36980 24 0 0 25 0 1 0 487371307 32419840 7177 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7177 603 41 0 7874 0
vsize: 31660
[startup+380.008 s]
Raw data (loadavg): 0.99 0.95 0.92 3/54 23598
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 7980 0 0 0 37980 24 0 0 25 0 1 0 487371307 32419840 7178 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7178 603 41 0 7874 0
vsize: 31660
[startup+390.009 s]
Raw data (loadavg): 0.99 0.95 0.92 3/59 23650
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8170 0 0 0 38980 24 0 0 25 0 1 0 487371307 33230848 7368 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8113 7368 603 41 0 8072 0
vsize: 32452
[startup+400.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23651
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8495 0 0 0 39980 25 0 0 25 0 1 0 487371307 34107392 7588 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7588 603 41 0 8286 0
vsize: 33308
[startup+410.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23651
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8496 0 0 0 40980 25 0 0 25 0 1 0 487371307 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): 0.99 0.96 0.92 2/54 23651
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8496 0 0 0 41980 25 0 0 25 0 1 0 487371307 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+430.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23651
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8497 0 0 0 42980 25 0 0 25 0 1 0 487371307 34107392 7590 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7590 603 41 0 8286 0
vsize: 33308
[startup+440.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23651
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8521 0 0 0 43980 25 0 0 25 0 1 0 487371307 34287616 7614 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8371 7614 603 41 0 8330 0
vsize: 33484
[startup+450.012 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23651
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8543 0 0 0 44981 25 0 0 25 0 1 0 487371307 34451456 7636 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7636 603 41 0 8370 0
vsize: 33644
[startup+460.013 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8546 0 0 0 45981 25 0 0 25 0 1 0 487371307 34451456 7639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7639 603 41 0 8370 0
vsize: 33644
[startup+470.013 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8553 0 0 0 46981 25 0 0 25 0 1 0 487371307 34451456 7646 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7646 603 41 0 8370 0
vsize: 33644
[startup+480.013 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8572 0 0 0 47981 25 0 0 25 0 1 0 487371307 34615296 7665 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8451 7665 603 41 0 8410 0
vsize: 33804
[startup+490.013 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8573 0 0 0 48981 25 0 0 25 0 1 0 487371307 34615296 7666 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8609 0 0 0 49982 25 0 0 25 0 1 0 487371307 34779136 7702 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8491 7702 603 41 0 8450 0
vsize: 33964
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 8805 0 0 0 50981 26 0 0 25 0 1 0 487371307 35549184 7898 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8679 7898 603 41 0 8638 0
vsize: 34716
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9022 0 0 0 51981 26 0 0 25 0 1 0 487371307 36478976 8115 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8906 8115 603 41 0 8865 0
vsize: 35624
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9207 0 0 0 52981 26 0 0 25 0 1 0 487371307 37326848 8300 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9113 8300 603 41 0 9072 0
vsize: 36452
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9405 0 0 0 53981 26 0 0 25 0 1 0 487371307 38113280 8498 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9305 8498 603 41 0 9264 0
vsize: 37220
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9588 0 0 0 54981 26 0 0 25 0 1 0 487371307 38776832 8681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9467 8681 603 41 0 9426 0
vsize: 37868
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9800 0 0 0 55980 27 0 0 25 0 1 0 487371307 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+570.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9800 0 0 0 56980 27 0 0 25 0 1 0 487371307 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+580.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9800 0 0 0 57980 27 0 0 25 0 1 0 487371307 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9800 0 0 0 58981 27 0 0 25 0 1 0 487371307 39223296 8788 4294967295 134512640 134672761 3221224544 3221223728 134615601 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9800 0 0 0 59981 27 0 0 25 0 1 0 487371307 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9800 0 0 0 60981 27 0 0 25 0 1 0 487371307 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+620.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9800 0 0 0 61981 27 0 0 25 0 1 0 487371307 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9801 0 0 0 62981 27 0 0 25 0 1 0 487371307 39223296 8789 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8789 603 41 0 9535 0
vsize: 38304
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9802 0 0 0 63982 27 0 0 25 0 1 0 487371307 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+650.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9803 0 0 0 64982 27 0 0 25 0 1 0 487371307 39223296 8791 4294967295 134512640 134672761 3221224544 3221223568 134612944 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8791 603 41 0 9535 0
vsize: 38304
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9805 0 0 0 65982 27 0 0 25 0 1 0 487371307 39223296 8793 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8793 603 41 0 9535 0
vsize: 38304
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9809 0 0 0 66982 27 0 0 25 0 1 0 487371307 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+680.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9812 0 0 0 67982 27 0 0 25 0 1 0 487371307 39223296 8800 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9576 8800 603 41 0 9535 0
vsize: 38304
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9930 0 0 0 68983 27 0 0 25 0 1 0 487371307 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+700.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9930 0 0 0 69983 27 0 0 25 0 1 0 487371307 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.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23653
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9930 0 0 0 70983 27 0 0 25 0 1 0 487371307 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.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9931 0 0 0 71983 27 0 0 25 0 1 0 487371307 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8839 603 41 0 9567 0
vsize: 38432
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9931 0 0 0 72983 27 0 0 25 0 1 0 487371307 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9931 0 0 0 73983 27 0 0 25 0 1 0 487371307 39354368 8839 4294967295 134512640 134672761 3221224544 3221223728 134615686 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.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9931 0 0 0 74984 27 0 0 25 0 1 0 487371307 39354368 8839 4294967295 134512640 134672761 3221224544 3221223584 134612636 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.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9932 0 0 0 75984 27 0 0 25 0 1 0 487371307 39354368 8840 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8840 603 41 0 9567 0
vsize: 38432
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9954 0 0 0 76984 27 0 0 25 0 1 0 487371307 39550976 8862 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8862 603 41 0 9615 0
vsize: 38624
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9955 0 0 0 77984 27 0 0 25 0 1 0 487371307 39550976 8863 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8863 603 41 0 9615 0
vsize: 38624
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9967 0 0 0 78984 27 0 0 25 0 1 0 487371307 39550976 8875 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8875 603 41 0 9615 0
vsize: 38624
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9969 0 0 0 79985 27 0 0 25 0 1 0 487371307 39550976 8877 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8877 603 41 0 9615 0
vsize: 38624
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9970 0 0 0 80985 27 0 0 25 0 1 0 487371307 39550976 8878 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9656 8878 603 41 0 9615 0
vsize: 38624
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 9985 0 0 0 81985 27 0 0 25 0 1 0 487371307 39747584 8893 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9704 8893 603 41 0 9663 0
vsize: 38816
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10002 0 0 0 82985 27 0 0 25 0 1 0 487371307 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9704 8910 603 41 0 9663 0
vsize: 38816
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10002 0 0 0 83985 27 0 0 25 0 1 0 487371307 39747584 8910 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10054 0 0 0 84985 28 0 0 25 0 1 0 487371307 40009728 8962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9768 8962 603 41 0 9727 0
vsize: 39072
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10168 0 0 0 85985 28 0 0 25 0 1 0 487371307 40796160 9076 4294967295 134512640 134672761 3221224544 3221223600 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9960 9076 603 41 0 9919 0
vsize: 39840
[startup+870.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10168 0 0 0 86996 28 0 0 25 0 1 0 487371307 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134615773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8996 603 41 0 9791 0
vsize: 39328
[startup+880.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10168 0 0 0 87996 28 0 0 25 0 1 0 487371307 40271872 8996 4294967295 134512640 134672761 3221224544 3221223728 134616017 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.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10168 0 0 0 88996 28 0 0 25 0 1 0 487371307 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+900.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10169 0 0 0 89996 28 0 0 25 0 1 0 487371307 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+910.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10169 0 0 0 90996 28 0 0 25 0 1 0 487371307 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+920.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10169 0 0 0 91997 28 0 0 25 0 1 0 487371307 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615929 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.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10169 0 0 0 92997 28 0 0 25 0 1 0 487371307 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+940.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10169 0 0 0 93997 28 0 0 25 0 1 0 487371307 40271872 8997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9832 8997 603 41 0 9791 0
vsize: 39328
[startup+950.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10367 0 0 0 94996 29 0 0 25 0 1 0 487371307 41201664 9195 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10059 9195 603 41 0 10018 0
vsize: 40236
[startup+960.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 10788 0 0 0 95994 31 0 0 25 0 1 0 487371307 42926080 9616 4294967295 134512640 134672761 3221224544 3221223680 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10480 9616 603 41 0 10439 0
vsize: 41920
[startup+970.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 11154 0 0 0 96994 32 0 0 25 0 1 0 487371307 44384256 9982 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10836 9982 603 41 0 10795 0
vsize: 43344
[startup+980.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 11564 0 0 0 97993 32 0 0 25 0 1 0 487371307 46026752 10392 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11237 10392 603 41 0 11196 0
vsize: 44948
[startup+990.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 11966 0 0 0 98992 34 0 0 25 0 1 0 487371307 47751168 10794 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11658 10794 603 41 0 11617 0
vsize: 46632
[startup+1000.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 99992 34 0 0 25 0 1 0 487371307 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1010.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 100992 34 0 0 25 0 1 0 487371307 48349184 10909 4294967295 134512640 134672761 3221224544 3221223584 134614228 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.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 101992 34 0 0 25 0 1 0 487371307 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10909 603 41 0 11763 0
vsize: 47216
[startup+1030.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 102992 34 0 0 25 0 1 0 487371307 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615579 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.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 103992 34 0 0 25 0 1 0 487371307 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615523 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.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 104993 34 0 0 25 0 1 0 487371307 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+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 105993 34 0 0 25 0 1 0 487371307 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+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12170 0 0 0 106993 34 0 0 25 0 1 0 487371307 48349184 10909 4294967295 134512640 134672761 3221224544 3221223728 134615739 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.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12180 0 0 0 107993 34 0 0 25 0 1 0 487371307 48545792 10919 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11852 10919 603 41 0 11811 0
vsize: 47408
[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12436 0 0 0 108993 34 0 0 25 0 1 0 487371307 49598464 11175 4294967295 134512640 134672761 3221224544 3221223728 134615622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12109 11175 603 41 0 12068 0
vsize: 48436
[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 12845 0 0 0 109992 35 0 0 25 0 1 0 487371307 51183616 11584 4294967295 134512640 134672761 3221224544 3221223584 134612507 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12496 11584 603 41 0 12455 0
vsize: 49984
[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 13151 0 0 0 110992 36 0 0 25 0 1 0 487371307 52506624 11890 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12819 11890 603 41 0 12778 0
vsize: 51276
[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 13397 0 0 0 111991 36 0 0 25 0 1 0 487371307 53563392 12136 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13077 12136 603 41 0 13036 0
vsize: 52308
[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 13694 0 0 0 112991 37 0 0 25 0 1 0 487371307 54747136 12433 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13366 12433 603 41 0 13325 0
vsize: 53464
[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 13973 0 0 0 113990 38 0 0 25 0 1 0 487371307 55820288 12712 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13628 12712 603 41 0 13587 0
vsize: 54512
[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 14216 0 0 0 114990 39 0 0 25 0 1 0 487371307 56885248 12955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13888 12955 603 41 0 13847 0
vsize: 55552
[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 14499 0 0 0 115989 40 0 0 25 0 1 0 487371307 58073088 13238 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14178 13238 603 41 0 14137 0
vsize: 56712
[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 14774 0 0 0 116988 40 0 0 25 0 1 0 487371307 59260928 13513 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14468 13513 603 41 0 14427 0
vsize: 57872
[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 15017 0 0 0 117988 41 0 0 25 0 1 0 487371307 60198912 13756 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14697 13756 603 41 0 14656 0
vsize: 58788
[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 15261 0 0 0 118987 42 0 0 25 0 1 0 487371307 61284352 14000 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14962 14000 603 41 0 14921 0
vsize: 59848
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23655
Raw data (stat): 23598 (minisat+) R 23597 24215 24214 0 -1 0 15463 0 0 0 119986 43 0 0 25 0 1 0 487371307 62132224 14202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15169 14202 603 41 0 15128 0
vsize: 60676
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 23655
Raw data (stat): 23598 (minisat+) Z 23597 24215 24214 0 -1 12 15464 0 0 0 119986 45 0 0 25 0 1 0 487371307 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.15
CPU time (s): 1200.33
CPU user time (s): 1199.87
CPU system time (s): 0.45993
CPU usage (%): 100.015
Max. virtual memory (Kb): 60676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####