[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/oski15a01b72s.aig
[runlim] start:			Fri Sep 18 07:15:26 2015
[runlim] main pid:		954
[runlim] sample:		9.5 time, 10.2 real, 472.4 MB
[runlim] sample:		19.5 time, 20.2 real, 472.4 MB
[runlim] sample:		29.5 time, 30.2 real, 472.4 MB
[runlim] sample:		39.5 time, 40.2 real, 674.4 MB
[runlim] sample:		50.6 time, 50.2 real, 1384.8 MB
[runlim] sample:		60.6 time, 60.2 real, 1717.5 MB
[runlim] sample:		70.6 time, 70.2 real, 2077.7 MB
[runlim] sample:		80.6 time, 80.2 real, 2084.7 MB
[runlim] sample:		90.6 time, 90.2 real, 2096.7 MB
[runlim] sample:		100.6 time, 100.2 real, 2118.7 MB
[runlim] sample:		110.6 time, 110.2 real, 2099.9 MB
[runlim] sample:		120.5 time, 120.2 real, 2107.7 MB
[runlim] sample:		130.5 time, 130.2 real, 2125.7 MB
[runlim] sample:		140.5 time, 140.2 real, 2159.7 MB
[runlim] sample:		150.5 time, 150.2 real, 2149.3 MB
[runlim] sample:		160.5 time, 160.2 real, 2149.3 MB
[runlim] sample:		170.5 time, 170.2 real, 2149.3 MB
[runlim] sample:		180.5 time, 180.2 real, 2149.3 MB
[runlim] sample:		190.4 time, 190.2 real, 2157.1 MB
[runlim] sample:		200.4 time, 200.2 real, 2167.1 MB
[runlim] sample:		210.4 time, 210.2 real, 2179.1 MB
[runlim] sample:		220.4 time, 220.2 real, 2185.3 MB
[runlim] sample:		230.4 time, 230.2 real, 2203.3 MB
[runlim] sample:		240.4 time, 240.2 real, 2223.3 MB
[runlim] sample:		250.4 time, 250.2 real, 2261.2 MB
[runlim] sample:		260.4 time, 260.2 real, 2301.2 MB
[runlim] sample:		270.3 time, 270.2 real, 2539.7 MB
[runlim] sample:		280.3 time, 280.2 real, 2848.3 MB
[runlim] sample:		290.3 time, 290.2 real, 2850.3 MB
[runlim] sample:		300.3 time, 300.2 real, 2856.7 MB
[runlim] sample:		310.3 time, 310.2 real, 2858.7 MB
[runlim] sample:		320.3 time, 320.2 real, 2866.7 MB
[runlim] sample:		330.2 time, 330.2 real, 2872.7 MB
[runlim] sample:		340.2 time, 340.2 real, 2876.7 MB
[runlim] sample:		363.9 time, 350.2 real, 3874.6 MB
[runlim] sample:		393.8 time, 360.2 real, 4324.5 MB
[runlim] sample:		423.8 time, 370.2 real, 4336.8 MB
[runlim] sample:		453.8 time, 380.2 real, 4364.6 MB
[runlim] sample:		483.7 time, 390.2 real, 4385.6 MB
[runlim] sample:		513.7 time, 400.2 real, 4403.6 MB
[runlim] sample:		543.7 time, 410.2 real, 4439.7 MB
[runlim] sample:		573.6 time, 420.2 real, 4477.7 MB
[runlim] sample:		603.6 time, 430.2 real, 4524.0 MB
[runlim] sample:		633.6 time, 440.2 real, 4624.1 MB
[runlim] sample:		663.5 time, 450.2 real, 4455.9 MB
[runlim] sample:		693.5 time, 460.2 real, 4461.9 MB
[runlim] sample:		723.5 time, 470.2 real, 4463.9 MB
[runlim] sample:		753.5 time, 480.2 real, 4463.9 MB
[runlim] sample:		783.5 time, 490.2 real, 4473.9 MB
[runlim] sample:		813.4 time, 500.2 real, 4475.9 MB
[runlim] sample:		843.4 time, 510.2 real, 4479.9 MB
[runlim] sample:		873.4 time, 520.2 real, 4483.9 MB
[runlim] sample:		903.3 time, 530.2 real, 4491.9 MB
[runlim] sample:		933.3 time, 540.2 real, 4497.9 MB
[runlim] sample:		963.3 time, 550.2 real, 4506.4 MB
[runlim] sample:		993.2 time, 560.2 real, 4523.1 MB
[runlim] sample:		1023.2 time, 570.2 real, 4525.1 MB
[runlim] sample:		1053.2 time, 580.2 real, 4531.3 MB
[runlim] sample:		1083.2 time, 590.2 real, 4547.4 MB
[runlim] sample:		1113.1 time, 600.2 real, 4565.5 MB
[runlim] sample:		1143.1 time, 610.2 real, 4588.1 MB
[runlim] sample:		1173.1 time, 620.2 real, 4627.8 MB
[runlim] sample:		1203.0 time, 630.2 real, 4648.3 MB
[runlim] sample:		1233.0 time, 640.2 real, 4706.5 MB
[runlim] sample:		1263.0 time, 650.2 real, 4732.4 MB
[runlim] sample:		1293.0 time, 660.2 real, 4772.5 MB
[runlim] sample:		1322.9 time, 670.2 real, 4814.5 MB
[runlim] sample:		1352.9 time, 680.2 real, 4852.6 MB
[runlim] sample:		1382.9 time, 690.2 real, 4896.7 MB
[runlim] sample:		1412.8 time, 700.2 real, 4946.6 MB
[runlim] sample:		1442.8 time, 710.2 real, 5064.8 MB
[runlim] sample:		1472.8 time, 720.2 real, 5076.9 MB
[runlim] sample:		1502.8 time, 730.2 real, 5076.9 MB
[runlim] sample:		1532.7 time, 740.2 real, 5079.1 MB
[runlim] sample:		1562.7 time, 750.2 real, 5081.1 MB
[runlim] sample:		1592.7 time, 760.2 real, 5085.2 MB
[runlim] sample:		1622.7 time, 770.2 real, 5085.2 MB
[runlim] sample:		1652.6 time, 780.2 real, 5091.3 MB
[runlim] sample:		1682.6 time, 790.2 real, 5093.5 MB
[runlim] sample:		1712.6 time, 800.2 real, 5100.9 MB
[runlim] sample:		1742.5 time, 810.2 real, 5108.9 MB
[runlim] sample:		1772.5 time, 820.2 real, 5114.9 MB
[runlim] sample:		1802.5 time, 830.2 real, 5119.0 MB
[runlim] sample:		1832.5 time, 840.2 real, 5129.1 MB
[runlim] sample:		1862.4 time, 850.2 real, 5135.2 MB
[runlim] sample:		1892.4 time, 860.2 real, 5141.2 MB
[runlim] sample:		1922.4 time, 870.2 real, 5147.3 MB
[runlim] sample:		1952.3 time, 880.2 real, 5157.5 MB
[runlim] sample:		1982.3 time, 890.2 real, 5163.5 MB
[runlim] sample:		2012.3 time, 900.2 real, 5167.7 MB
[runlim] sample:		2042.2 time, 910.2 real, 5179.8 MB
[runlim] sample:		2072.2 time, 920.2 real, 5191.8 MB
[runlim] sample:		2102.2 time, 930.2 real, 5206.0 MB
[runlim] sample:		2132.2 time, 940.2 real, 5230.0 MB
[runlim] sample:		2162.1 time, 950.2 real, 5258.1 MB
[runlim] sample:		2192.1 time, 960.2 real, 5274.2 MB
[runlim] sample:		2222.1 time, 970.2 real, 5306.2 MB
[runlim] sample:		2252.0 time, 980.2 real, 5338.3 MB
[runlim] sample:		2282.0 time, 990.2 real, 5372.4 MB
[runlim] sample:		2312.0 time, 1000.2 real, 5396.5 MB
[runlim] sample:		2341.9 time, 1010.2 real, 5418.6 MB
[runlim] sample:		2371.9 time, 1020.2 real, 5446.1 MB
[runlim] sample:		2401.9 time, 1030.2 real, 5486.1 MB
[runlim] sample:		2431.9 time, 1040.2 real, 5538.2 MB
[runlim] sample:		2461.8 time, 1050.2 real, 5574.4 MB
[runlim] sample:		2491.6 time, 1060.2 real, 5624.5 MB
[runlim] sample:		2521.6 time, 1070.2 real, 5680.5 MB
[runlim] sample:		2551.6 time, 1080.2 real, 5752.6 MB
[runlim] sample:		2581.6 time, 1090.2 real, 5860.7 MB
[runlim] end:			Fri Sep 18 07:33:41 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		11
[runlim] real:			1095.54 seconds
[runlim] time:			2596.82 seconds
[runlim] space:			7061.2 MB
[runlim] samples:		10953
