[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/oski15/submission/single/oski15a01b02s.aig
[runlim] start:			Thu Sep 17 22:23:14 2015
[runlim] main pid:		2620
[runlim] sample:		9.3 time, 10.3 real, 443.4 MB
[runlim] sample:		19.3 time, 20.3 real, 443.4 MB
[runlim] sample:		29.3 time, 30.3 real, 443.4 MB
[runlim] sample:		39.3 time, 40.3 real, 670.3 MB
[runlim] sample:		50.5 time, 50.3 real, 1385.6 MB
[runlim] sample:		60.5 time, 60.3 real, 1904.1 MB
[runlim] sample:		70.5 time, 70.3 real, 2233.9 MB
[runlim] sample:		80.5 time, 80.3 real, 2502.5 MB
[runlim] sample:		90.5 time, 90.3 real, 2570.1 MB
[runlim] sample:		100.4 time, 100.3 real, 2570.1 MB
[runlim] sample:		110.4 time, 110.3 real, 2570.1 MB
[runlim] sample:		120.4 time, 120.3 real, 2574.1 MB
[runlim] sample:		130.4 time, 130.3 real, 2578.1 MB
[runlim] sample:		140.4 time, 140.3 real, 2586.1 MB
[runlim] sample:		150.4 time, 150.3 real, 2598.1 MB
[runlim] sample:		160.3 time, 160.3 real, 2604.1 MB
[runlim] sample:		170.3 time, 170.3 real, 2616.3 MB
[runlim] sample:		180.3 time, 180.3 real, 2648.5 MB
[runlim] sample:		190.3 time, 190.3 real, 2877.4 MB
[runlim] sample:		200.3 time, 200.3 real, 2879.4 MB
[runlim] sample:		210.3 time, 210.3 real, 2885.4 MB
[runlim] sample:		220.3 time, 220.3 real, 2891.4 MB
[runlim] sample:		230.2 time, 230.3 real, 2909.4 MB
[runlim] sample:		240.2 time, 240.3 real, 2911.4 MB
[runlim] sample:		250.2 time, 250.3 real, 2913.4 MB
[runlim] sample:		260.2 time, 260.3 real, 2915.4 MB
[runlim] sample:		270.2 time, 270.3 real, 2919.4 MB
[runlim] sample:		280.2 time, 280.3 real, 2935.4 MB
[runlim] sample:		290.2 time, 290.3 real, 2941.3 MB
[runlim] sample:		300.1 time, 300.3 real, 2949.3 MB
[runlim] sample:		310.1 time, 310.3 real, 2959.3 MB
[runlim] sample:		320.1 time, 320.3 real, 2967.3 MB
[runlim] sample:		330.1 time, 330.3 real, 2985.3 MB
[runlim] sample:		340.1 time, 340.3 real, 3041.4 MB
[runlim] sample:		363.4 time, 350.3 real, 4046.0 MB
[runlim] sample:		393.2 time, 360.3 real, 4493.3 MB
[runlim] sample:		423.2 time, 370.3 real, 4509.7 MB
[runlim] sample:		453.2 time, 380.3 real, 4537.2 MB
[runlim] sample:		483.1 time, 390.3 real, 4602.2 MB
[runlim] sample:		513.1 time, 400.3 real, 4622.4 MB
[runlim] sample:		543.1 time, 410.3 real, 4640.4 MB
[runlim] sample:		573.0 time, 420.3 real, 4658.6 MB
[runlim] sample:		603.0 time, 430.3 real, 4688.7 MB
[runlim] sample:		633.0 time, 440.3 real, 4724.7 MB
[runlim] sample:		663.0 time, 450.3 real, 4764.7 MB
[runlim] sample:		693.0 time, 460.3 real, 4799.0 MB
[runlim] sample:		722.9 time, 470.3 real, 4871.0 MB
[runlim] sample:		752.9 time, 480.3 real, 4973.0 MB
[runlim] sample:		782.9 time, 490.3 real, 5041.3 MB
[runlim] sample:		812.8 time, 500.3 real, 5115.3 MB
[runlim] sample:		842.8 time, 510.3 real, 5185.4 MB
[runlim] sample:		872.8 time, 520.3 real, 5271.5 MB
[runlim] sample:		902.8 time, 530.3 real, 5335.5 MB
[runlim] sample:		932.7 time, 540.3 real, 5389.5 MB
[runlim] sample:		962.7 time, 550.3 real, 5425.5 MB
[runlim] sample:		992.7 time, 560.3 real, 5471.5 MB
[runlim] sample:		1022.6 time, 570.3 real, 5521.5 MB
[runlim] sample:		1052.6 time, 580.3 real, 5559.7 MB
[runlim] sample:		1082.6 time, 590.3 real, 5619.7 MB
[runlim] sample:		1112.6 time, 600.3 real, 5676.1 MB
[runlim] sample:		1142.5 time, 610.3 real, 5730.1 MB
[runlim] sample:		1172.5 time, 620.3 real, 5824.3 MB
[runlim] sample:		1202.5 time, 630.3 real, 5884.4 MB
[runlim] sample:		1232.5 time, 640.3 real, 5930.5 MB
[runlim] sample:		1262.4 time, 650.3 real, 5972.5 MB
[runlim] sample:		1292.4 time, 660.3 real, 6026.5 MB
[runlim] sample:		1322.4 time, 670.3 real, 6098.7 MB
[runlim] sample:		1352.3 time, 680.3 real, 6150.8 MB
[runlim] sample:		1382.3 time, 690.3 real, 6200.9 MB
[runlim] sample:		1412.3 time, 700.3 real, 6243.1 MB
[runlim] sample:		1442.3 time, 710.3 real, 6289.1 MB
[runlim] sample:		1472.2 time, 720.3 real, 6361.1 MB
[runlim] sample:		1502.2 time, 730.3 real, 6433.2 MB
[runlim] sample:		1532.2 time, 740.3 real, 6491.3 MB
[runlim] sample:		1562.2 time, 750.3 real, 6503.4 MB
[runlim] sample:		1592.1 time, 760.3 real, 6515.5 MB
[runlim] sample:		1622.1 time, 770.3 real, 6523.6 MB
[runlim] sample:		1652.1 time, 780.3 real, 6525.7 MB
[runlim] sample:		1682.0 time, 790.3 real, 6537.7 MB
[runlim] sample:		1712.0 time, 800.3 real, 6549.8 MB
[runlim] sample:		1742.0 time, 810.3 real, 6567.9 MB
[runlim] sample:		1772.0 time, 820.3 real, 6584.0 MB
[runlim] sample:		1802.0 time, 830.3 real, 6602.1 MB
[runlim] sample:		1831.9 time, 840.3 real, 6610.2 MB
[runlim] sample:		1861.9 time, 850.3 real, 6620.2 MB
[runlim] sample:		1891.6 time, 860.3 real, 6646.3 MB
[runlim] sample:		1921.3 time, 870.3 real, 6656.4 MB
[runlim] sample:		1951.3 time, 880.3 real, 6670.5 MB
[runlim] sample:		1981.3 time, 890.3 real, 6696.6 MB
[runlim] sample:		2011.3 time, 900.3 real, 6718.6 MB
[runlim] sample:		2041.2 time, 910.3 real, 6743.8 MB
[runlim] sample:		2071.2 time, 920.3 real, 6811.0 MB
[runlim] sample:		2101.2 time, 930.3 real, 6885.0 MB
[runlim] sample:		2131.2 time, 940.3 real, 6929.0 MB
[runlim] sample:		2161.1 time, 950.3 real, 6967.0 MB
[runlim] sample:		2191.1 time, 960.3 real, 6997.3 MB
[runlim] end:			Thu Sep 17 22:39:16 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		12
[runlim] real:			962.36 seconds
[runlim] time:			2196.71 seconds
[runlim] space:			7001.3 MB
[runlim] samples:		9620
