[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/hwmcc14/single/oski1rub00i.aig
[runlim] start:			Thu Sep 17 02:50:46 2015
[runlim] main pid:		569
[runlim] sample:		9.4 time, 10.3 real, 294.1 MB
[runlim] sample:		19.4 time, 20.3 real, 294.1 MB
[runlim] sample:		29.4 time, 30.3 real, 294.1 MB
[runlim] sample:		46.8 time, 40.3 real, 1604.9 MB
[runlim] sample:		76.7 time, 50.3 real, 2181.6 MB
[runlim] sample:		106.4 time, 60.3 real, 2408.5 MB
[runlim] sample:		136.1 time, 70.3 real, 2448.6 MB
[runlim] sample:		166.1 time, 80.3 real, 2574.1 MB
[runlim] sample:		195.8 time, 90.3 real, 2615.5 MB
[runlim] sample:		225.5 time, 100.3 real, 2673.9 MB
[runlim] sample:		255.4 time, 110.3 real, 2712.1 MB
[runlim] sample:		285.4 time, 120.3 real, 2754.5 MB
[runlim] sample:		315.4 time, 130.3 real, 2799.7 MB
[runlim] sample:		345.1 time, 140.3 real, 2858.9 MB
[runlim] sample:		375.1 time, 150.3 real, 2930.5 MB
[runlim] sample:		405.0 time, 160.3 real, 2991.8 MB
[runlim] sample:		434.7 time, 170.3 real, 3067.7 MB
[runlim] sample:		464.6 time, 180.3 real, 3145.8 MB
[runlim] sample:		494.5 time, 190.3 real, 3214.1 MB
[runlim] sample:		524.3 time, 200.3 real, 3246.1 MB
[runlim] sample:		554.1 time, 210.3 real, 3298.1 MB
[runlim] sample:		583.8 time, 220.3 real, 3356.1 MB
[runlim] sample:		613.7 time, 230.3 real, 3412.9 MB
[runlim] sample:		643.6 time, 240.3 real, 3455.7 MB
[runlim] sample:		673.6 time, 250.3 real, 3529.5 MB
[runlim] sample:		703.5 time, 260.3 real, 3569.5 MB
[runlim] sample:		733.3 time, 270.3 real, 3635.7 MB
[runlim] sample:		763.2 time, 280.3 real, 3693.7 MB
[runlim] sample:		793.2 time, 290.3 real, 3763.7 MB
[runlim] sample:		823.1 time, 300.3 real, 3815.9 MB
[runlim] sample:		852.8 time, 310.3 real, 3881.0 MB
[runlim] sample:		882.5 time, 320.3 real, 3968.9 MB
[runlim] sample:		912.1 time, 330.3 real, 4053.3 MB
[runlim] sample:		941.8 time, 340.3 real, 4121.5 MB
[runlim] sample:		971.5 time, 350.3 real, 4203.5 MB
[runlim] sample:		1001.2 time, 360.3 real, 4269.7 MB
[runlim] sample:		1031.0 time, 370.3 real, 4337.5 MB
[runlim] sample:		1061.0 time, 380.3 real, 4407.5 MB
[runlim] sample:		1090.9 time, 390.3 real, 4499.0 MB
[runlim] sample:		1120.9 time, 400.3 real, 4562.2 MB
[runlim] sample:		1150.5 time, 410.3 real, 4642.6 MB
[runlim] sample:		1180.4 time, 420.3 real, 4736.6 MB
[runlim] sample:		1210.2 time, 430.3 real, 4810.6 MB
[runlim] sample:		1239.9 time, 440.3 real, 4888.6 MB
[runlim] sample:		1269.6 time, 450.3 real, 4962.6 MB
[runlim] sample:		1299.2 time, 460.3 real, 5032.8 MB
[runlim] sample:		1328.9 time, 470.3 real, 5122.8 MB
[runlim] sample:		1358.6 time, 480.3 real, 5150.8 MB
[runlim] sample:		1388.5 time, 490.3 real, 5184.8 MB
[runlim] sample:		1418.5 time, 500.3 real, 5216.5 MB
[runlim] sample:		1448.4 time, 510.3 real, 5266.5 MB
[runlim] sample:		1478.4 time, 520.3 real, 5310.5 MB
[runlim] sample:		1508.3 time, 530.3 real, 5334.5 MB
[runlim] sample:		1538.3 time, 540.3 real, 5386.5 MB
[runlim] sample:		1568.2 time, 550.3 real, 5427.8 MB
[runlim] sample:		1598.1 time, 560.3 real, 5485.8 MB
[runlim] sample:		1628.1 time, 570.3 real, 5540.1 MB
[runlim] sample:		1657.9 time, 580.3 real, 5588.1 MB
[runlim] sample:		1687.8 time, 590.3 real, 5623.4 MB
[runlim] sample:		1717.7 time, 600.3 real, 5661.4 MB
[runlim] sample:		1747.6 time, 610.3 real, 5705.4 MB
[runlim] sample:		1777.5 time, 620.3 real, 5780.6 MB
[runlim] sample:		1807.4 time, 630.3 real, 5836.6 MB
[runlim] sample:		1837.2 time, 640.3 real, 5901.8 MB
[runlim] sample:		1867.0 time, 650.3 real, 5951.8 MB
[runlim] sample:		1896.8 time, 660.3 real, 5997.9 MB
[runlim] sample:		1926.5 time, 670.3 real, 6067.5 MB
[runlim] sample:		1956.3 time, 680.3 real, 6165.5 MB
[runlim] sample:		1986.1 time, 690.3 real, 6213.5 MB
[runlim] sample:		2016.0 time, 700.3 real, 6260.5 MB
[runlim] sample:		2045.9 time, 710.3 real, 6305.2 MB
[runlim] sample:		2075.9 time, 720.3 real, 6371.2 MB
[runlim] sample:		2105.8 time, 730.3 real, 6429.2 MB
[runlim] sample:		2135.8 time, 740.3 real, 6477.5 MB
[runlim] sample:		2165.7 time, 750.3 real, 6523.5 MB
[runlim] sample:		2195.7 time, 760.3 real, 6605.2 MB
[runlim] sample:		2225.7 time, 770.3 real, 6675.5 MB
[runlim] sample:		2255.6 time, 780.3 real, 6751.8 MB
[runlim] sample:		2285.2 time, 790.3 real, 6796.4 MB
[runlim] sample:		2314.9 time, 800.3 real, 6858.5 MB
[runlim] sample:		2344.6 time, 810.3 real, 6915.0 MB
[runlim] sample:		2374.5 time, 820.3 real, 6959.7 MB
[runlim] end:			Thu Sep 17 03:04:35 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		8
[runlim] real:			829.91 seconds
[runlim] time:			2402.85 seconds
[runlim] space:			7000.9 MB
[runlim] samples:		8296
