PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 22:48:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13740 boxname=wulflinc10 idbench=1057 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-p0548.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 13740
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        734304 kB
Buffers:         19856 kB
Cached:         259080 kB
SwapCached:          0 kB
Active:          43428 kB
Inactive:       238020 kB
HighTotal:      131008 kB
HighFree:          868 kB
LowTotal:       903652 kB
LowFree:        733436 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13276 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:08:55 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 13740 7 1200.26 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]---> BDD-cost:142726
c ---[  79]---> BDD-cost: 1478
c ---[  78]---> BDD-cost: 1140
c ---[  77]---> BDD-cost: 2534
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  444846  1328425 |  148282       0        0     nan |  0.000 % |
c |       101 |  441209  1318476 |  163110      98     5432    55.4 |  0.424 % |
c |       251 |  441209  1318476 |  179421     248    21498    86.7 |  0.424 % |
c |       476 |  441209  1318476 |  197363     473    28197    59.6 |  0.424 % |
c |       813 |  438913  1313060 |  217099     798    37190    46.6 |  1.091 % |
c ==============================================================================
c [1mFound solution: 47049[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:108445     Base: 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       838 |  736455  2007125 |  245485     807    37347    46.3 |  1.091 % |
c |       938 |  736455  2007125 |  270033     907    38571    42.5 |  1.054 % |
c |      1090 |  736455  2007125 |  297036    1059    39109    36.9 |  1.054 % |
c |      1315 |  736455  2007125 |  326740    1284    41364    32.2 |  1.054 % |
c |      1654 |  736439  2007089 |  359414    1622    43195    26.6 |  1.056 % |
c |      2160 |  736028  2005916 |  395356    2119    93991    44.4 |  1.113 % |
c |      2920 |  735716  2004989 |  434891    2873   145416    50.6 |  1.155 % |
c |      4059 |  735701  2004944 |  478380    4010   168919    42.1 |  1.157 % |
c |      5767 |  735701  2004944 |  526218    5718   198094    34.6 |  1.157 % |
c |      8330 |  735614  2004683 |  578840    8278   442134    53.4 |  1.168 % |
c |     12175 |  720208  1958823 |  636724   11694   979186    83.7 |  3.194 % |
c |     17943 |  719276  1956027 |  700397   17400  2513961   144.5 |  3.317 % |
c |     26593 |  711392  1932375 |  770437   25708  4843896   188.4 |  4.337 % |
c |     39571 |  699563  1896888 |  847480   37844  6277713   165.9 |  5.897 % |
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_bit0 -C1324_bit0 -C1325_bit0 -C1326_bit0 -C1327_bit0 C1328_bit0 -C1329_bit0 -C1330_bit0 C1331_bit0 -C1332_bit0 C1333_bit0 C1334_bit0 C1335_bit0 -C1336_bit0 C1337_bit0 -C1338_bit0 -C1339_bit0 -C1340_bit0 C1342_bit0 -C1343_bit0 -C1344_bit0 -C1345_bit0 C1346_bit0 -C1347_bit0 -C1348_bit0 -C1349_bit0 C1351_bit0 -C1352_bit0 C1353_bit0 -C1354_bit0 C1355_bit0 -C1356_bit0 -C1357_bit0 -C1358_bit0 C1359_bit0 -C1361_bit0 -C1362_bit0 -C1363_bit0 -C1364_bit0 -C1365_bit0 C1366_bit0 C1367_bit0 -C1368_bit0 -C1369_bit0 -C1370_bit0 -C1371_bit0 C1374_bit0 -C1375_bit0 C1376_bit0 C1377_bit0 -C1378_bit0 C1379_bit0 -C1380_bit0 C1381_bit0 -C1382_bit0 -C1383_bit0 -C1384_bit0 -C1387_bit0 -C1388_bit0 C1389_bit0 C1390_bit0 C1391_bit0 -C1392_bit0 C1393_bit0 -C1394_bit0 -C1395_bit0 -C1396_bit0 C1399_bit0 C1400_bit0 C1401_bit0 C1402_bit0 C1403_bit0 -C1404_bit0 -C1405_bit0 C1406_bit0 -C1407_bit0 -C1408_bit0 -C1409_bit0 C1412_bit0 -C1413_bit0 -C1414_bit0 C1415_bit0 -C1416_bit0 -C1417_bit0 C1418_bit0 -C1419_bit0 -C1420_bit0 -C1421_bit0 -C14#### 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.93 0.98 0.99 2/54 6229
Raw data (stat): 6229 (runsolver) R 6228 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490590922 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.94 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 14009 0 0 0 967 31 0 0 25 0 1 0 490590922 65110016 13069 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15896 13069 603 41 0 15855 0
vsize: 63584
[startup+20.0008 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 22716 0 0 0 1948 50 0 0 25 0 1 0 490590922 91877376 21446 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22431 21446 603 41 0 22390 0
vsize: 89724
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 22777 0 0 0 2948 51 0 0 25 0 1 0 490590922 92057600 21507 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22475 21507 603 41 0 22434 0
vsize: 89900
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 22830 0 0 0 3947 51 0 0 25 0 1 0 490590922 92327936 21560 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22541 21560 603 41 0 22500 0
vsize: 90164
[startup+50.0026 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 22897 0 0 0 4947 51 0 0 25 0 1 0 490590922 92594176 21627 4294967295 134512640 134672761 3221224544 3221223680 134560650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22606 21627 603 41 0 22565 0
vsize: 90424
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 22937 0 0 0 5947 51 0 0 25 0 1 0 490590922 92729344 21667 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22639 21667 603 41 0 22598 0
vsize: 90556
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23011 0 0 0 6947 52 0 0 25 0 1 0 490590922 93061120 21741 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22720 21741 603 41 0 22679 0
vsize: 90880
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23090 0 0 0 7946 53 0 0 25 0 1 0 490590922 93454336 21820 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22816 21820 603 41 0 22775 0
vsize: 91264
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23126 0 0 0 8946 53 0 0 25 0 1 0 490590922 93585408 21856 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22848 21856 603 41 0 22807 0
vsize: 91392
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23183 0 0 0 9946 53 0 0 25 0 1 0 490590922 93921280 21913 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22930 21913 603 41 0 22889 0
vsize: 91720
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23215 0 0 0 10946 53 0 0 25 0 1 0 490590922 94081024 21945 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22969 21945 603 41 0 22928 0
vsize: 91876
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23239 0 0 0 11946 54 0 0 25 0 1 0 490590922 94081024 21969 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22969 21969 603 41 0 22928 0
vsize: 91876
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23248 0 0 0 12946 54 0 0 25 0 1 0 490590922 94216192 21978 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 21978 603 41 0 22961 0
vsize: 92008
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23253 0 0 0 13946 54 0 0 25 0 1 0 490590922 94216192 21983 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 21983 603 41 0 22961 0
vsize: 92008
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23262 0 0 0 14946 54 0 0 25 0 1 0 490590922 94216192 21992 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 21992 603 41 0 22961 0
vsize: 92008
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23266 0 0 0 15946 54 0 0 25 0 1 0 490590922 94216192 21996 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 21996 603 41 0 22961 0
vsize: 92008
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23267 0 0 0 16946 55 0 0 25 0 1 0 490590922 94216192 21997 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 21997 603 41 0 22961 0
vsize: 92008
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23268 0 0 0 17946 55 0 0 25 0 1 0 490590922 94216192 21998 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 21998 603 41 0 22961 0
vsize: 92008
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23273 0 0 0 18946 55 0 0 25 0 1 0 490590922 94216192 22003 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 22003 603 41 0 22961 0
vsize: 92008
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23276 0 0 0 19946 55 0 0 25 0 1 0 490590922 94351360 22006 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22006 603 41 0 22994 0
vsize: 92140
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23279 0 0 0 20945 56 0 0 25 0 1 0 490590922 94351360 22009 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22009 603 41 0 22994 0
vsize: 92140
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23283 0 0 0 21945 56 0 0 25 0 1 0 490590922 94351360 22013 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22013 603 41 0 22994 0
vsize: 92140
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23284 0 0 0 22946 56 0 0 25 0 1 0 490590922 94351360 22014 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22014 603 41 0 22994 0
vsize: 92140
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23286 0 0 0 23945 56 0 0 25 0 1 0 490590922 94351360 22016 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22016 603 41 0 22994 0
vsize: 92140
[startup+250.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23289 0 0 0 24946 56 0 0 25 0 1 0 490590922 94351360 22019 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22019 603 41 0 22994 0
vsize: 92140
[startup+260.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23290 0 0 0 25946 56 0 0 25 0 1 0 490590922 94351360 22020 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22020 603 41 0 22994 0
vsize: 92140
[startup+270.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23292 0 0 0 26946 57 0 0 25 0 1 0 490590922 94351360 22022 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22022 603 41 0 22994 0
vsize: 92140
[startup+280.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23293 0 0 0 27945 57 0 0 25 0 1 0 490590922 94351360 22023 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22023 603 41 0 22994 0
vsize: 92140
[startup+290.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23296 0 0 0 28945 57 0 0 25 0 1 0 490590922 94351360 22026 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22026 603 41 0 22994 0
vsize: 92140
[startup+300.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23298 0 0 0 29945 57 0 0 25 0 1 0 490590922 94351360 22028 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22028 603 41 0 22994 0
vsize: 92140
[startup+310.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23301 0 0 0 30945 57 0 0 25 0 1 0 490590922 94351360 22031 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22031 603 41 0 22994 0
vsize: 92140
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23302 0 0 0 31945 58 0 0 25 0 1 0 490590922 94351360 22032 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22032 603 41 0 22994 0
vsize: 92140
[startup+330.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23304 0 0 0 32945 58 0 0 25 0 1 0 490590922 94351360 22034 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22034 603 41 0 22994 0
vsize: 92140
[startup+340.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23308 0 0 0 33945 58 0 0 25 0 1 0 490590922 94351360 22038 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 22038 603 41 0 22994 0
vsize: 92140
[startup+350.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23309 0 0 0 34945 59 0 0 25 0 1 0 490590922 94486528 22039 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23068 22039 603 41 0 23027 0
vsize: 92272
[startup+360.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23310 0 0 0 35945 59 0 0 25 0 1 0 490590922 94486528 22040 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 22040 603 41 0 23027 0
vsize: 92272
[startup+370.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23314 0 0 0 36945 59 0 0 25 0 1 0 490590922 94486528 22044 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 22044 603 41 0 23027 0
vsize: 92272
[startup+380.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23316 0 0 0 37945 59 0 0 25 0 1 0 490590922 94486528 22046 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 22046 603 41 0 23027 0
vsize: 92272
[startup+390.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23318 0 0 0 38945 59 0 0 25 0 1 0 490590922 94486528 22048 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 22048 603 41 0 23027 0
vsize: 92272
[startup+400.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23321 0 0 0 39945 59 0 0 25 0 1 0 490590922 94486528 22051 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 22051 603 41 0 23027 0
vsize: 92272
[startup+410.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23322 0 0 0 40945 59 0 0 25 0 1 0 490590922 94486528 22052 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 22052 603 41 0 23027 0
vsize: 92272
[startup+420.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23327 0 0 0 41946 59 0 0 25 0 1 0 490590922 94486528 22057 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 22057 603 41 0 23027 0
vsize: 92272
[startup+430.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23350 0 0 0 42946 59 0 0 25 0 1 0 490590922 94621696 22080 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23101 22080 603 41 0 23060 0
vsize: 92404
[startup+440.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23429 0 0 0 43946 59 0 0 25 0 1 0 490590922 94887936 22159 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23166 22159 603 41 0 23125 0
vsize: 92664
[startup+450.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23459 0 0 0 44946 59 0 0 25 0 1 0 490590922 95019008 22189 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23198 22189 603 41 0 23157 0
vsize: 92792
[startup+460.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23496 0 0 0 45946 59 0 0 25 0 1 0 490590922 95154176 22226 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23231 22226 603 41 0 23190 0
vsize: 92924
[startup+470.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23500 0 0 0 46946 59 0 0 25 0 1 0 490590922 95154176 22230 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23231 22230 603 41 0 23190 0
vsize: 92924
[startup+480.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23503 0 0 0 47946 59 0 0 25 0 1 0 490590922 95154176 22233 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23231 22233 603 41 0 23190 0
vsize: 92924
[startup+490.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23509 0 0 0 48947 59 0 0 25 0 1 0 490590922 95289344 22239 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23264 22239 603 41 0 23223 0
vsize: 93056
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23513 0 0 0 49947 59 0 0 25 0 1 0 490590922 95289344 22243 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23264 22243 603 41 0 23223 0
vsize: 93056
[startup+510.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23519 0 0 0 50947 59 0 0 25 0 1 0 490590922 95289344 22249 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23264 22249 603 41 0 23223 0
vsize: 93056
[startup+520.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23526 0 0 0 51947 60 0 0 25 0 1 0 490590922 95289344 22256 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23264 22256 603 41 0 23223 0
vsize: 93056
[startup+530.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23540 0 0 0 52947 60 0 0 25 0 1 0 490590922 95408128 22270 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23293 22270 603 41 0 23252 0
vsize: 93172
[startup+540.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23552 0 0 0 53947 60 0 0 25 0 1 0 490590922 95408128 22282 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23293 22282 603 41 0 23252 0
vsize: 93172
[startup+550.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23590 0 0 0 54947 60 0 0 25 0 1 0 490590922 95543296 22320 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23326 22320 603 41 0 23285 0
vsize: 93304
[startup+560.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23598 0 0 0 55947 60 0 0 25 0 1 0 490590922 95543296 22328 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23326 22328 603 41 0 23285 0
vsize: 93304
[startup+570.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23606 0 0 0 56947 60 0 0 25 0 1 0 490590922 95666176 22336 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23356 22336 603 41 0 23315 0
vsize: 93424
[startup+580.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23629 0 0 0 57948 60 0 0 25 0 1 0 490590922 95666176 22359 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23356 22359 603 41 0 23315 0
vsize: 93424
[startup+590.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23714 0 0 0 58948 60 0 0 25 0 1 0 490590922 96071680 22444 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23455 22444 603 41 0 23414 0
vsize: 93820
[startup+600.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23790 0 0 0 59948 60 0 0 25 0 1 0 490590922 96342016 22520 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23521 22520 603 41 0 23480 0
vsize: 94084
[startup+610.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23811 0 0 0 60947 60 0 0 25 0 1 0 490590922 96477184 22541 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23554 22541 603 41 0 23513 0
vsize: 94216
[startup+620.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 23894 0 0 0 61947 61 0 0 25 0 1 0 490590922 96747520 22624 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23620 22624 603 41 0 23579 0
vsize: 94480
[startup+630.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 24064 0 0 0 62947 61 0 0 25 0 1 0 490590922 97538048 22794 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23813 22794 603 41 0 23772 0
vsize: 95252
[startup+640.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 24199 0 0 0 63946 62 0 0 25 0 1 0 490590922 98078720 22929 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23945 22929 603 41 0 23904 0
vsize: 95780
[startup+650.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 24371 0 0 0 64946 63 0 0 25 0 1 0 490590922 98750464 23101 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24109 23101 603 41 0 24068 0
vsize: 96436
[startup+660.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 24518 0 0 0 65945 63 0 0 25 0 1 0 490590922 99282944 23248 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24239 23248 603 41 0 24198 0
vsize: 96956
[startup+670.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6229
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 24651 0 0 0 66945 63 0 0 25 0 1 0 490590922 99958784 23381 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24404 23381 603 41 0 24363 0
vsize: 97616
[startup+680.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6282
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 24790 0 0 0 67945 64 0 0 25 0 1 0 490590922 100478976 23520 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24531 23520 603 41 0 24490 0
vsize: 98124
[startup+690.002 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6282
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 24942 0 0 0 68944 65 0 0 25 0 1 0 490590922 101146624 23672 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24694 23672 603 41 0 24653 0
vsize: 98776
[startup+700.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6282
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 25111 0 0 0 69944 65 0 0 25 0 1 0 490590922 101810176 23841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24856 23841 603 41 0 24815 0
vsize: 99424
[startup+710.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6282
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 25270 0 0 0 70943 66 0 0 25 0 1 0 490590922 102453248 24000 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25013 24000 603 41 0 24972 0
vsize: 100052
[startup+720.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6282
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 25277 0 0 0 71943 66 0 0 25 0 1 0 490590922 102453248 24007 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25013 24007 603 41 0 24972 0
vsize: 100052
[startup+730.002 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6282
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 25332 0 0 0 72942 67 0 0 25 0 1 0 490590922 102723584 24062 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25079 24062 603 41 0 25038 0
vsize: 100316
[startup+740.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 25473 0 0 0 73941 68 0 0 25 0 1 0 490590922 103354368 24203 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24203 603 41 0 25192 0
vsize: 100932
[startup+750.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 25655 0 0 0 74941 69 0 0 25 0 1 0 490590922 103993344 24385 4294967295 134512640 134672761 3221224544 3221223648 134559859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25389 24385 603 41 0 25348 0
vsize: 101556
[startup+760.002 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 25843 0 0 0 75940 70 0 0 25 0 1 0 490590922 104779776 24573 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25581 24573 603 41 0 25540 0
vsize: 102324
[startup+770.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 26049 0 0 0 76940 70 0 0 25 0 1 0 490590922 105705472 24779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25807 24779 603 41 0 25766 0
vsize: 103228
[startup+780.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 26219 0 0 0 77940 71 0 0 25 0 1 0 490590922 106344448 24949 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25963 24949 603 41 0 25922 0
vsize: 103852
[startup+790.003 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 26416 0 0 0 78939 72 0 0 25 0 1 0 490590922 107139072 25146 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26157 25146 603 41 0 26116 0
vsize: 104628
[startup+800.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 26642 0 0 0 79938 73 0 0 25 0 1 0 490590922 108101632 25372 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26392 25372 603 41 0 26351 0
vsize: 105568
[startup+810.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 26821 0 0 0 80937 74 0 0 25 0 1 0 490590922 108769280 25551 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26555 25551 603 41 0 26514 0
vsize: 106220
[startup+820.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 26979 0 0 0 81938 75 0 0 25 0 1 0 490590922 109408256 25709 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26711 25709 603 41 0 26670 0
vsize: 106844
[startup+830.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27141 0 0 0 82937 75 0 0 25 0 1 0 490590922 110104576 25871 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26881 25871 603 41 0 26840 0
vsize: 107524
[startup+840.016 s]
Raw data (loadavg): 1.07 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27300 0 0 0 83937 76 0 0 25 0 1 0 490590922 110735360 26030 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27035 26030 603 41 0 26994 0
vsize: 108140
[startup+850.017 s]
Raw data (loadavg): 1.06 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27436 0 0 0 84936 76 0 0 25 0 1 0 490590922 111411200 26166 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27200 26166 603 41 0 27159 0
vsize: 108800
[startup+860.019 s]
Raw data (loadavg): 1.05 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27460 0 0 0 85937 77 0 0 25 0 1 0 490590922 111411200 26190 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27200 26190 603 41 0 27159 0
vsize: 108800
[startup+870.02 s]
Raw data (loadavg): 1.04 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27528 0 0 0 86937 77 0 0 25 0 1 0 490590922 111677440 26258 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27265 26258 603 41 0 27224 0
vsize: 109060
[startup+880.019 s]
Raw data (loadavg): 1.04 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27595 0 0 0 87936 78 0 0 25 0 1 0 490590922 111943680 26325 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27330 26325 603 41 0 27289 0
vsize: 109320
[startup+890.019 s]
Raw data (loadavg): 1.03 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27600 0 0 0 88936 78 0 0 25 0 1 0 490590922 111943680 26330 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27330 26330 603 41 0 27289 0
vsize: 109320
[startup+900.019 s]
Raw data (loadavg): 1.03 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27627 0 0 0 89936 78 0 0 25 0 1 0 490590922 112082944 26357 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27364 26357 603 41 0 27323 0
vsize: 109456
[startup+910.019 s]
Raw data (loadavg): 1.02 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27703 0 0 0 90936 79 0 0 25 0 1 0 490590922 112349184 26433 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27429 26433 603 41 0 27388 0
vsize: 109716
[startup+920.02 s]
Raw data (loadavg): 1.02 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27716 0 0 0 91936 79 0 0 25 0 1 0 490590922 112492544 26446 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27464 26446 603 41 0 27423 0
vsize: 109856
[startup+930.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27727 0 0 0 92936 79 0 0 25 0 1 0 490590922 112492544 26457 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27464 26457 603 41 0 27423 0
vsize: 109856
[startup+940.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27741 0 0 0 93935 80 0 0 25 0 1 0 490590922 112611328 26471 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27493 26471 603 41 0 27452 0
vsize: 109972
[startup+950.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27760 0 0 0 94936 80 0 0 25 0 1 0 490590922 112611328 26490 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27493 26490 603 41 0 27452 0
vsize: 109972
[startup+960.021 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27799 0 0 0 95936 80 0 0 25 0 1 0 490590922 112742400 26529 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27525 26529 603 41 0 27484 0
vsize: 110100
[startup+970.021 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27812 0 0 0 96936 80 0 0 25 0 1 0 490590922 112873472 26542 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27557 26542 603 41 0 27516 0
vsize: 110228
[startup+980.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27829 0 0 0 97936 80 0 0 25 0 1 0 490590922 112873472 26559 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27557 26559 603 41 0 27516 0
vsize: 110228
[startup+990.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27842 0 0 0 98936 80 0 0 25 0 1 0 490590922 112992256 26572 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27586 26572 603 41 0 27545 0
vsize: 110344
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27853 0 0 0 99937 80 0 0 25 0 1 0 490590922 112992256 26583 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27586 26583 603 41 0 27545 0
vsize: 110344
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6284
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27859 0 0 0 100937 80 0 0 25 0 1 0 490590922 112992256 26589 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27586 26589 603 41 0 27545 0
vsize: 110344
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27891 0 0 0 101937 80 0 0 25 0 1 0 490590922 113127424 26621 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27619 26621 603 41 0 27578 0
vsize: 110476
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27900 0 0 0 102937 80 0 0 25 0 1 0 490590922 113246208 26630 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27648 26630 603 41 0 27607 0
vsize: 110592
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27908 0 0 0 103937 80 0 0 25 0 1 0 490590922 113246208 26638 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27648 26638 603 41 0 27607 0
vsize: 110592
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 27919 0 0 0 104937 80 0 0 25 0 1 0 490590922 113246208 26649 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27648 26649 603 41 0 27607 0
vsize: 110592
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28009 0 0 0 105937 80 0 0 25 0 1 0 490590922 113647616 26739 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27746 26739 603 41 0 27705 0
vsize: 110984
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28032 0 0 0 106937 80 0 0 25 0 1 0 490590922 113778688 26762 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27778 26762 603 41 0 27737 0
vsize: 111112
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28056 0 0 0 107937 80 0 0 25 0 1 0 490590922 113778688 26786 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27778 26786 603 41 0 27737 0
vsize: 111112
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28072 0 0 0 108938 80 0 0 25 0 1 0 490590922 113909760 26802 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27810 26802 603 41 0 27769 0
vsize: 111240
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28103 0 0 0 109938 81 0 0 25 0 1 0 490590922 114044928 26833 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27843 26833 603 41 0 27802 0
vsize: 111372
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28122 0 0 0 110938 81 0 0 25 0 1 0 490590922 114044928 26852 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27843 26852 603 41 0 27802 0
vsize: 111372
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28123 0 0 0 111938 81 0 0 25 0 1 0 490590922 114176000 26853 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27875 26853 603 41 0 27834 0
vsize: 111500
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28180 0 0 0 112938 81 0 0 25 0 1 0 490590922 114438144 26910 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27939 26910 603 41 0 27898 0
vsize: 111756
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28245 0 0 0 113938 81 0 0 25 0 1 0 490590922 114692096 26975 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28001 26975 603 41 0 27960 0
vsize: 112004
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28263 0 0 0 114939 81 0 0 25 0 1 0 490590922 114827264 26993 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28034 26993 603 41 0 27993 0
vsize: 112136
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28291 0 0 0 115939 81 0 0 25 0 1 0 490590922 114962432 27021 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28067 27021 603 41 0 28026 0
vsize: 112268
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28411 0 0 0 116939 81 0 0 25 0 1 0 490590922 115363840 27141 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28165 27141 603 41 0 28124 0
vsize: 112660
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28588 0 0 0 117938 81 0 0 25 0 1 0 490590922 116174848 27318 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28363 27318 603 41 0 28322 0
vsize: 113452
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 28862 0 0 0 118938 82 0 0 25 0 1 0 490590922 117248000 27592 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28625 27592 603 41 0 28584 0
vsize: 114500
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 6286
Raw data (stat): 6229 (minisat+) R 6228 25347 25346 0 -1 0 29010 0 0 0 119937 83 0 0 25 0 1 0 490590922 117899264 27740 4294967295 134512640 134672761 3221224544 3221223680 134560650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28784 27740 603 41 0 28743 0
vsize: 115136
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 1.00 1/54 6286
Raw data (stat): 6229 (minisat+) Z 6228 25347 25346 0 -1 12 29013 0 0 0 119937 88 0 0 25 0 1 0 490590922 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.08
CPU time (s): 1200.26
CPU user time (s): 1199.38
CPU system time (s): 0.884865
CPU usage (%): 100.015
Max. virtual memory (Kb): 115136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####