[runlim] version:		1.9
[runlim] time limit:		311040000 seconds
[runlim] real time limit:	3600 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/hwmcc15/solvers/pdtrav/single.pdtravthrd
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/6s48p1.aig
[runlim] start:			Fri Sep 18 20:32:18 2015
[runlim] main pid:		2865
[runlim] sample:		32.9 time, 10.5 real, 942.0 MB
[runlim] sample:		72.6 time, 20.5 real, 984.7 MB
[runlim] sample:		112.3 time, 30.5 real, 997.0 MB
[runlim] sample:		151.9 time, 40.5 real, 1010.8 MB
[runlim] sample:		191.5 time, 50.5 real, 1024.5 MB
[runlim] sample:		231.2 time, 60.5 real, 1036.4 MB
[runlim] sample:		270.8 time, 70.5 real, 1045.2 MB
[runlim] sample:		310.4 time, 80.5 real, 1054.6 MB
[runlim] sample:		350.0 time, 90.5 real, 1060.2 MB
[runlim] sample:		389.6 time, 100.5 real, 1107.3 MB
[runlim] sample:		429.3 time, 110.5 real, 1116.1 MB
[runlim] sample:		468.9 time, 120.5 real, 1205.7 MB
[runlim] sample:		508.5 time, 130.5 real, 1257.1 MB
[runlim] sample:		548.1 time, 140.5 real, 1433.3 MB
[runlim] sample:		587.8 time, 150.5 real, 1317.1 MB
[runlim] sample:		627.4 time, 160.5 real, 1390.3 MB
[runlim] sample:		667.0 time, 170.5 real, 1356.5 MB
[runlim] sample:		706.6 time, 180.5 real, 1354.3 MB
[runlim] sample:		746.3 time, 190.5 real, 1333.8 MB
[runlim] sample:		785.9 time, 200.5 real, 1352.4 MB
[runlim] sample:		825.5 time, 210.5 real, 1370.4 MB
[runlim] sample:		865.2 time, 220.5 real, 1385.0 MB
[runlim] sample:		904.8 time, 230.5 real, 1406.8 MB
[runlim] sample:		944.4 time, 240.5 real, 1423.2 MB
[runlim] sample:		984.1 time, 250.5 real, 1438.9 MB
[runlim] sample:		1023.7 time, 260.5 real, 1435.6 MB
[runlim] sample:		1063.4 time, 270.5 real, 1440.7 MB
[runlim] sample:		1103.0 time, 280.5 real, 1442.3 MB
[runlim] sample:		1142.6 time, 290.5 real, 1443.6 MB
[runlim] sample:		1182.2 time, 300.5 real, 1442.7 MB
[runlim] sample:		1221.9 time, 310.5 real, 1446.3 MB
[runlim] sample:		1261.5 time, 320.5 real, 1465.4 MB
[runlim] sample:		1301.1 time, 330.5 real, 1467.6 MB
[runlim] sample:		1340.8 time, 340.5 real, 1469.8 MB
[runlim] sample:		1380.4 time, 350.5 real, 1482.3 MB
[runlim] sample:		1420.0 time, 360.5 real, 1485.3 MB
[runlim] sample:		1459.7 time, 370.5 real, 1489.1 MB
[runlim] sample:		1499.3 time, 380.5 real, 1502.6 MB
[runlim] sample:		1538.9 time, 390.5 real, 1503.9 MB
[runlim] sample:		1578.6 time, 400.5 real, 1510.7 MB
[runlim] sample:		1618.2 time, 410.5 real, 1518.4 MB
[runlim] sample:		1657.8 time, 420.5 real, 1522.0 MB
[runlim] sample:		1697.4 time, 430.5 real, 1530.9 MB
[runlim] sample:		1737.0 time, 440.5 real, 1528.0 MB
[runlim] sample:		1776.7 time, 450.5 real, 1538.9 MB
[runlim] sample:		1816.3 time, 460.5 real, 1544.4 MB
[runlim] sample:		1855.9 time, 470.5 real, 1554.3 MB
[runlim] sample:		1895.5 time, 480.5 real, 1552.7 MB
[runlim] sample:		1935.2 time, 490.5 real, 1562.4 MB
[runlim] sample:		1974.8 time, 500.5 real, 1567.8 MB
[runlim] sample:		2014.4 time, 510.5 real, 1569.9 MB
[runlim] sample:		2054.0 time, 520.5 real, 1578.4 MB
[runlim] sample:		2093.7 time, 530.5 real, 1574.6 MB
[runlim] sample:		2133.3 time, 540.5 real, 1577.9 MB
[runlim] sample:		2172.9 time, 550.5 real, 1577.4 MB
[runlim] end:			Fri Sep 18 20:41:33 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		8
[runlim] real:			555.61 seconds
[runlim] time:			2192.83 seconds
[runlim] space:			1582.6 MB
[runlim] samples:		5551
