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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ar98.opb
MD5SUM	181a05258ae35e5f3b5b834240f1847a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	83886080000000
Number of bits of the biggest number in a constraint	47
Biggest sum of numbers in a constraint	572975239517507
Number of bits of the biggest sum of numbers	50
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.23881
Number of variables	20024
Total number of constraints	17064
Number of constraints which are clauses	1
Number of constraints which are cardinality constraints (but not clauses)	16718
Number of constraints which are nor clauses,nor cardinality constraints	345
Minimum length of a constraint	1
Maximum length of a constraint	15837
Trace number 30957

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-25 20:59:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22335 boxname=wulflinc27 idbench=1151 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  181a05258ae35e5f3b5b834240f1847a  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-blp-ar98.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-blp-ar98.opb
IDLAUNCH: 22335
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        667144 kB
Buffers:         33200 kB
Cached:         312396 kB
SwapCached:        592 kB
Active:          40676 kB
Inactive:       307008 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        666892 kB
SwapTotal:     2097892 kB
SwapFree:      2096444 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5152 kB
Slab:            14156 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:23:32 (client local time) WITH STATUS 134 IN 1433.67 SECONDS
stats: 22335 7 1433.67 134
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 32096] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1473 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss.
c ---[1475]---> BDD-cost:   12
c ---[1474]---> BDD-cost:   12
c ---[1473]---> BDD-cost:   12
c ---[1472]---> BDD-cost:   13
c ---[1470]---> BDD-cost:   13
c ---[1469]---> BDD-cost:   12
c ---[1468]---> BDD-cost:   13
c ---[1467]---> BDD-cost:   12
c ---[1466]---> BDD-cost:   13
c ---[1465]---> BDD-cost:   13
c ---[1464]---> BDD-cost:   12
c ---[1463]---> BDD-cost:   13
c ---[1462]---> BDD-cost:   13
c ---[1461]---> BDD-cost:   12
c ---[1460]---> BDD-cost:   13
c ---[1459]---> BDD-cost:   13
c ---[1458]---> BDD-cost:   13
c ---[1457]---> BDD-cost:   13
c ---[1456]---> BDD-cost:   13
c ---[1455]---> BDD-cost:   12
c ---[1454]---> BDD-cost:   11
c ---[1453]---> BDD-cost:   12
c ---[1452]---> BDD-cost:   13
c ---[1451]---> BDD-cost:   13
c ---[1450]---> BDD-cost:   13
c ---[1449]---> BDD-cost:   13
c ---[1448]---> BDD-cost:   12
c ---[1447]---> BDD-cost:   13
c ---[1446]---> BDD-cost:   13
c ---[1445]---> BDD-cost:   13
c ---[1444]---> BDD-cost:   13
c ---[1443]---> BDD-cost:   13
c ---[1442]---> BDD-cost:   13
c ---[1441]---> BDD-cost:   13
c ---[1440]---> BDD-cost:   13
c ---[1439]---> BDD-cost:   13
c ---[1438]---> BDD-cost:   13
c ---[1437]---> BDD-cost:   13
c ---[1436]---> BDD-cost:   12
c ---[1435]---> BDD-cost:   13
c ---[1434]---> BDD-cost:   13
c ---[1433]---> BDD-cost:   13
c ---[1432]---> BDD-cost:   13
c ---[1431]---> BDD-cost:   13
c ---[1430]---> BDD-cost:   13
c ---[1429]---> BDD-cost:   13
c ---[1428]---> BDD-cost:   13
c ---[1427]---> BDD-cost:   12
c ---[1426]---> BDD-cost:   13
c ---[1425]---> BDD-cost:   13
c ---[1424]---> BDD-cost:   13
c ---[1423]---> BDD-cost:   12
c ---[1422]---> BDD-cost:   12
c ---[1421]---> BDD-cost:   13
c ---[1420]---> BDD-cost:   13
c ---[1419]---> BDD-cost:   13
c ---[1418]---> BDD-cost:   13
c ---[1417]---> BDD-cost:   13
c ---[1416]---> BDD-cost:   13
c ---[1415]---> BDD-cost:   13
c ---[1414]---> BDD-cost:   13
c ---[1413]---> BDD-cost:   13
c ---[1412]---> BDD-cost:   13
c ---[1411]---> BDD-cost:   13
c ---[1410]---> BDD-cost:   12
c ---[1409]---> BDD-cost:   13
c ---[1408]---> BDD-cost:   13
c ---[1407]---> BDD-cost:   13
c ---[1406]---> BDD-cost:   13
c ---[1405]---> BDD-cost:   13
c ---[1404]---> BDD-cost:   12
c ---[1403]---> BDD-cost:   12
c ---[1402]---> BDD-cost:   13
c ---[1401]---> BDD-cost:   13
c ---[1400]---> BDD-cost:   13
c ---[1399]---> BDD-cost:   12
c ---[1398]---> BDD-cost:   13
c ---[1397]---> BDD-cost:   13
c ---[1396]---> BDD-cost:   13
c ---[1395]---> BDD-cost:   13
c ---[1394]---> BDD-cost:   13
c ---[1393]---> BDD-cost:   12
c ---[1392]---> BDD-cost:   13
c ---[1391]---> BDD-cost:   13
c ---[1390]---> BDD-cost:   13
c ---[1389]---> BDD-cost:   13
c ---[1388]---> BDD-cost:   13
c ---[1387]---> BDD-cost:   13
c ---[1386]---> BDD-cost:   13
c ---[1385]---> BDD-cost:   13
c ---[1384]---> BDD-cost:   13
c ---[1383]---> BDD-cost:   13
c ---[1381]---> BDD-cost:   13
c ---[1380]---> BDD-cost:   13
c ---[1379]---> BDD-cost:   13
c ---[1378]---> BDD-cost:   13
c ---[1377]---> BDD-cost:   13
c ---[1376]---> BDD-cost:   12
c ---[1375]---> BDD-cost:   13
c ---[1374]---> BDD-cost:   13
c ---[1373]---> BDD-cost:   12
c ---[1372]---> BDD-cost:   12
c ---[1371]---> BDD-cost:   12
c ---[1370]---> BDD-cost:   13
c ---[1369]---> BDD-cost:   13
c ---[1368]---> BDD-cost:   13
c ---[1367]---> BDD-cost:   13
c ---[1366]---> BDD-cost:   13
c ---[1365]---> BDD-cost:   12
c ---[1364]---> BDD-cost:   12
c ---[1362]---> BDD-cost:   13
c ---[1361]---> BDD-cost:   13
c ---[1360]---> BDD-cost:   13
c ---[1359]---> BDD-cost:   13
c ---[1358]---> BDD-cost:   13
c ---[1357]---> BDD-cost:   13
c ---[1356]---> BDD-cost:   13
c ---[1355]---> BDD-cost:   13
c ---[1354]---> BDD-cost:   13
c ---[1353]---> BDD-cost:   11
c ---[1352]---> BDD-cost:   13
c ---[1351]---> BDD-cost:   13
c ---[1350]---> BDD-cost:   12
c ---[1349]---> BDD-cost:   13
c ---[1348]---> BDD-cost:   13
c ---[1347]---> BDD-cost:   13
c ---[1346]---> BDD-cost:   13
c ---[1344]---> Adder-cost: 4370   maxlim: 4711424   bits: 23/23
c ---[1342]---> Adder-cost: 3378   maxlim: 4420608   bits: 23/23
c ---[1340]---> Adder-cost: 3212   maxlim: 3318784   bits: 22/22
c ---[1338]---> Adder-cost: 3118   maxlim: 3374080   bits: 22/22
c ---[1336]---> Adder-cost: 2686   maxlim: 2925568   bits: 22/22
c ---[1334]---> Adder-cost: 1564   maxlim: 1969152   bits: 21/21
c ---[1332]---> Adder-cost: 756   maxlim: 929792   bits: 20/20
c ---[1330]---> Adder-cost: 704   maxlim: 756736   bits: 20/20
c ---[1328]---> Adder-cost: 1236   maxlim: 1556480   bits: 21/21
c ---[1326]---> Adder-cost: 2132   maxlim: 2252800   bits: 22/22
c ---[1324]---> Adder-cost: 1340   maxlim: 1588224   bits: 21/21
c ---[1322]---> Adder-cost: 3828   maxlim: 4342784   bits: 23/23
c ---[1320]---> Adder-cost: 1388   maxlim: 1639424   bits: 21/21
c ---[1318]---> Adder-cost: 782   maxlim: 794624   bits: 20/20
c ---[1316]---> Adder-cost: 562   maxlim: 758784   bits: 20/20
c ---[1314]---> Adder-cost: 330   maxlim: 414720   bits: 19/19
c ---[1312]---> Adder-cost: 176   maxlim: 212992   bits: 18/18
c ---[1310]---> Adder-cost: 232   maxlim: 228352   bits: 18/18
c ---[1308]---> Adder-cost: 522   maxlim: 563200   bits: 20/20
c ---[1306]---> Adder-cost: 924   maxlim: 1088512   bits: 21/21
c ---[1304]---> Adder-cost: 4884   maxlim: 7817216   bits: 23/23
c ---[1302]---> Adder-cost: 3826   maxlim: 6107136   bits: 23/23
c ---[1300]---> Adder-cost: 776   maxlim: 4420608   bits: 23/23
c ---[1298]---> Adder-cost: 2220   maxlim: 3396608   bits: 22/22
c ---[1296]---> Adder-cost: 452   maxlim: 452608   bits: 19/19
c ---[1294]---> Adder-cost: 524   maxlim: 532480   bits: 20/20
c ---[1292]---> Adder-cost: 1474   maxlim: 2452480   bits: 22/22
c ---[1290]---> Adder-cost: 1944   maxlim: 3654656   bits: 22/22
c ---[1288]---> Adder-cost: 362   maxlim: 369664   bits: 19/19
c ---[1286]---> Sorter-cost: 1180     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1284]---> Adder-cost: 1814   maxlim: 2660352   bits: 22/22
c ---[1282]---> Adder-cost: 1258   maxlim: 2051072   bits: 21/21
c ---[1280]---> Adder-cost: 498   maxlim: 541696   bits: 20/20
c ---[1278]---> Adder-cost: 712   maxlim: 857088   bits: 20/20
c ---[1276]---> Adder-cost: 810   maxlim: 1186816   bits: 21/21
c ---[1274]---> Adder-cost: 250   maxlim: 271360   bits: 19/19
c ---[1272]---> Adder-cost: 210   maxlim: 271360   bits: 19/19
c ---[1270]---> Adder-cost: 342   maxlim: 493568   bits: 19/19
c ---[1268]---> Adder-cost: 476   maxlim: 559104   bits: 20/20
c ---[1266]---> Adder-cost: 1820   maxlim: 1997824   bits: 21/21
c ---[1264]---> Adder-cost: 2086   maxlim: 2534400   bits: 22/22
c ---[1262]---> BDD-cost:   79
c ---[1260]---> Adder-cost: 224   maxlim: 318464   bits: 19/19
c ---[1258]---> Adder-cost: 258   maxlim: 433152   bits: 19/19
c ---[1256]---> Adder-cost: 896   maxlim: 1175552   bits: 21/21
c ---[1254]---> Adder-cost: 1424   maxlim: 1523712   bits: 21/21
c ---[1252]---> Adder-cost: 3020   maxlim: 3462144   bits: 22/22
c ---[1250]---> Adder-cost: 1796   maxlim: 2198528   bits: 22/22
c ---[1248]---> Adder-cost: 4044   maxlim: 5436416   bits: 23/23
c ---[1246]---> Adder-cost: 192   maxlim: 269312   bits: 19/19
c ---[1244]---> Adder-cost: 228   maxlim: 289792   bits: 19/19
c ---[1242]---> Adder-cost: 334   maxlim: 496640   bits: 19/19
c ---[1240]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1238]---> Adder-cost: 656   maxlim: 825344   bits: 20/20
c ---[1236]---> Adder-cost: 270   maxlim: 825344   bits: 20/20
c ---[1234]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1232]---> Adder-cost: 1774   maxlim: 2400256   bits: 22/22
c ---[1230]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1228]---> Adder-cost: 380   maxlim: 538624   bits: 20/20
c ---[1226]---> Adder-cost: 142   maxlim: 188416   bits: 18/18
c ---[1224]---> Adder-cost: 464   maxlim: 786432   bits: 20/20
c ---[1222]---> Adder-cost: 152   maxlim: 148480   bits: 18/18
c ---[1220]---> Adder-cost: 466   maxlim: 531456   bits: 20/20
c ---[1218]---> Adder-cost: 2418   maxlim: 3253248   bits: 22/22
c ---[1216]---> Adder-cost: 1274   maxlim: 1677312   bits: 21/21
c ---[1214]---> Adder-cost: 4864   maxlim: 6126592   bits: 23/23
c ---[1212]---> Adder-cost: 1392   maxlim: 1899520   bits: 21/21
c ---[1210]---> Adder-cost: 3074   maxlim: 4076544   bits: 22/22
c ---[1208]---> Adder-cost: 4114   maxlim: 6376448   bits: 23/23
c ---[1206]---> Adder-cost: 1758   maxlim: 2183168   bits: 22/22
c ---[1204]---> Adder-cost: 2902   maxlim: 3851264   bits: 22/22
c ---[1202]---> Adder-cost: 1576   maxlim: 2208768   bits: 22/22
c ---[1200]---> Adder-cost: 3600   maxlim: 5413888   bits: 23/23
c ---[1198]---> Adder-cost: 232   maxlim: 271360   bits: 19/19
c ---[1196]---> Adder-cost: 156   maxlim: 174080   bits: 18/18
c ---[1194]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1192]---> Adder-cost: 1542   maxlim: 2054144   bits: 21/21
c ---[1190]---> Adder-cost: 1494   maxlim: 2045952   bits: 21/21
c ---[1188]---> Adder-cost: 758   maxlim: 1026048   bits: 20/20
c ---[1186]---> Adder-cost: 1014   maxlim: 1204224   bits: 21/21
c ---[1184]---> Adder-cost: 1460   maxlim: 2139136   bits: 22/22
c ---[1182]---> Adder-cost: 542   maxlim: 750   bits: 10/10
c ---[1180]---> Adder-cost: 860   maxlim: 1327104   bits: 21/21
c ---[1178]---> Adder-cost: 600   maxlim: 952320   bits: 20/20
c ---[1176]---> Sorter-cost: 1393     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1174]---> Adder-cost: 656   maxlim: 883712   bits: 20/20
c ---[1172]---> Adder-cost: 562   maxlim: 715776   bits: 20/20
c ---[1170]---> Adder-cost: 272   maxlim: 371712   bits: 19/19
c ---[1168]---> Adder-cost: 1440   maxlim: 1993728   bits: 21/21
c ---[1166]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost: 1051     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1162]---> Adder-cost: 246   maxlim: 434176   bits: 19/19
c ---[1160]---> Adder-cost: 608   maxlim: 1158144   bits: 21/21
c ---[1158]---> Adder-cost: 1120   maxlim: 2419712   bits: 22/22
c ---[1156]---> Adder-cost: 360   maxlim: 365568   bits: 19/19
c ---[1154]---> Adder-cost: 490   maxlim: 513024   bits: 20/19
c ---[1152]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1150]---> Sorter-cost: 1721     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1148]---> Sorter-cost: 1430     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Adder-cost: 832   maxlim: 963584   bits: 20/20
c ---[1144]---> Adder-cost: 1850   maxlim: 3003392   bits: 22/22
c ---[1142]---> Adder-cost: 1194   maxlim: 2665472   bits: 22/22
c ---[1140]---> Adder-cost: 206   maxlim: 242688   bits: 18/18
c ---[1138]---> Adder-cost: 254   maxlim: 491   bits: 9/9
c ---[1136]---> Adder-cost: 758   maxlim: 1467392   bits: 21/21
c ---[1134]---> Adder-cost: 120   maxlim: 178176   bits: 18/18
c ---[1132]---> Adder-cost: 192   maxlim: 324608   bits: 19/19
c ---[1130]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1128]---> Adder-cost: 1596   maxlim: 2703360   bits: 22/22
c ---[1126]---> Adder-cost: 856   maxlim: 1112064   bits: 21/21
c ---[1124]---> Adder-cost: 294   maxlim: 335872   bits: 19/19
c ---[1122]---> Adder-cost: 332   maxlim: 421888   bits: 19/19
c ---[1120]---> Adder-cost: 1674   maxlim: 2615296   bits: 22/22
c ---[1118]---> Adder-cost: 1610   maxlim: 2498560   bits: 22/22
c ---[1116]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1114]---> Adder-cost: 172   maxlim: 182272   bits: 18/18
c ---[1112]---> Adder-cost: 130   maxlim: 123904   bits: 18/17
c ---[1110]---> Adder-cost: 1116   maxlim: 1618944   bits: 21/21
c ---[1108]---> Adder-cost: 908   maxlim: 1317888   bits: 21/21
c ---[1106]---> Sorter-cost:  201     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Adder-cost: 444   maxlim: 544768   bits: 20/20
c ---[1102]---> BDD-cost:   53
c ---[1100]---> Adder-cost: 298   maxlim: 356352   bits: 19/19
c ---[1098]---> Adder-cost: 260   maxlim: 367616   bits: 19/19
c ---[1096]---> Adder-cost: 2140  GNU MP: Cannot allocate memory (size=4)
 maxlim: 3369   bits: 12/12
c ---[1094]---> Adder-cost: 1600   maxlim: 3086336   bits: 22/22
c ---[1092]---> Sorter-cost:  195     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1090]---> Sorter-cost: 1371     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1088]---> Adder-cost: 3128   maxlim: 4966   bits: 13/13
c ---[1086]---> Adder-cost: 3234   maxlim: 5427200   bits: 23/23
c ---[1084]---> Adder-cost: 690   maxlim: 1234944   bits: 21/21
c ---[1082]---> Adder-cost: 472   maxlim: 669696   bits: 20/20
c ---[1080]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1078]---> Adder-cost: 274   maxlim: 331776   bits: 19/19
c ---[1076]---> /oldhome/oroussel/solvers/minisat+_script: line 16: 21549 Aborted                 $XDIR/minisat+_bignum_static* "$@"
#### 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): 1.01 0.99 0.99 2/54 21489
Raw data (stat): 21489 (runsolver) R 21488 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841942126 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 21493
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+19.9998 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 21493
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0001 s]
Raw data (loadavg): 1.01 0.99 0.99 2/56 21494
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0005 s]
Raw data (loadavg): 1.23 1.04 1.00 2/55 21546
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0013 s]
Raw data (loadavg): 1.19 1.03 1.00 2/55 21546
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0012 s]
Raw data (loadavg): 1.16 1.03 1.00 2/55 21546
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.001 s]
Raw data (loadavg): 1.14 1.03 1.00 2/55 21546
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0017 s]
Raw data (loadavg): 1.11 1.03 1.00 2/55 21546
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0015 s]
Raw data (loadavg): 1.10 1.03 1.00 2/55 21546
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 1.08 1.03 1.00 2/55 21546
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 1.07 1.03 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.002 s]
Raw data (loadavg): 1.06 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 1.05 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 1.04 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.002 s]
Raw data (loadavg): 1.03 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 1.03 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.003 s]
Raw data (loadavg): 1.02 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.003 s]
Raw data (loadavg): 1.02 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.003 s]
Raw data (loadavg): 1.02 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.003 s]
Raw data (loadavg): 1.01 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.002 s]
Raw data (loadavg): 1.01 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.002 s]
Raw data (loadavg): 1.01 1.02 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.002 s]
Raw data (loadavg): 1.01 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.002 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.002 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.001 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.001 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.001 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.001 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.002 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.002 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21548
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841942126 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.002 s]
Raw data (loadavg): 1.00 1.01 1.00 2/55 21549
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+330.001 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21549
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+340.001 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21549
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+350.001 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21549
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+360.002 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21549
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+370.002 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21549
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+380.001 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+390.001 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+400.002 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+410.002 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+420.002 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+430.002 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+440.002 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+450.003 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+460.004 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+470.004 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+480.005 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+490.004 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+500.005 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+510.005 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+520.005 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+530.006 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+540.005 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+550.006 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+560.006 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+570.006 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+580.006 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+590.007 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+600.007 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+610.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+620.007 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+630.007 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+640.007 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+650.007 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+660.007 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+670.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+680.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+690.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+700.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+710.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+720.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+730.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+740.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+750.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+760.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+770.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+780.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+790.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+800.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+810.011 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+820.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+830.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+840.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+850.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+860.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+870.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+880.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+890.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+900.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+910.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+920.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+930.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+940.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+950.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+960.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+970.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+980.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+990.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1130.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1140.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1160.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1170.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1190.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1210.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1220.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1230.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1240.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1250.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1260.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1270.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1280.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1290.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1300.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1310.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1320.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1330.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1340.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1350.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1360.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1370.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1380.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1390.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1400.14 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1410.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1420.13 s]
Raw data (loadavg): 1.00 1.00 1.00 1/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1430.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1438.35 s]
Raw data (loadavg): 1.00 1.00 1.00 1/53 21551
Raw data (stat): 21489 (minisat+_script) S 21488 3394 3393 0 -1 0 300 3165 0 0 0 0 31794 23 19 0 1 0 841942126 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 134
Real time (s): 1438.35
CPU time (s): 1433.67
CPU user time (s): 1425.69
CPU system time (s): 7.97979
CPU usage (%): 99.6747
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####