[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.pdtravdeep
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b18s.aig
[runlim] start:			Thu Sep 17 12:29:54 2015
[runlim] main pid:		8647
[runlim] sample:		8.4 time, 10.6 real, 132.4 MB
[runlim] sample:		18.4 time, 20.6 real, 161.7 MB
[runlim] sample:		28.4 time, 30.6 real, 182.8 MB
[runlim] sample:		38.4 time, 40.6 real, 209.1 MB
[runlim] sample:		48.4 time, 50.6 real, 209.6 MB
[runlim] sample:		58.4 time, 60.6 real, 209.6 MB
[runlim] sample:		68.4 time, 70.6 real, 209.6 MB
[runlim] sample:		78.4 time, 80.6 real, 268.7 MB
[runlim] sample:		88.4 time, 90.6 real, 268.7 MB
[runlim] sample:		98.4 time, 100.6 real, 268.7 MB
[runlim] sample:		108.7 time, 110.6 real, 803.1 MB
[runlim] sample:		118.7 time, 120.6 real, 1094.6 MB
[runlim] sample:		128.7 time, 130.6 real, 1361.4 MB
[runlim] sample:		138.6 time, 140.6 real, 1519.3 MB
[runlim] sample:		148.6 time, 150.6 real, 1869.3 MB
[runlim] sample:		158.6 time, 160.6 real, 2026.9 MB
[runlim] sample:		168.6 time, 170.6 real, 2258.4 MB
[runlim] sample:		178.6 time, 180.6 real, 2378.4 MB
[runlim] sample:		188.6 time, 190.6 real, 2543.8 MB
[runlim] sample:		198.6 time, 200.6 real, 2613.7 MB
[runlim] sample:		208.6 time, 210.6 real, 3165.8 MB
[runlim] sample:		218.6 time, 220.6 real, 3275.1 MB
[runlim] sample:		228.5 time, 230.6 real, 3398.6 MB
[runlim] sample:		238.5 time, 240.6 real, 3519.1 MB
[runlim] sample:		248.5 time, 250.6 real, 3721.7 MB
[runlim] sample:		258.5 time, 260.6 real, 3806.1 MB
[runlim] sample:		267.8 time, 270.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 280.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 290.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 300.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 310.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 320.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 330.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 340.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 350.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 360.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 370.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 380.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 390.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 400.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 410.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 420.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 430.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 440.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 450.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 460.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 470.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 480.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 490.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 500.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 510.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 520.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 530.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 540.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 550.6 real, 3905.0 MB
[runlim] sample:		267.8 time, 560.6 real, 3905.0 MB
[runlim] sample:		268.5 time, 570.6 real, 3907.0 MB
[runlim] sample:		278.5 time, 580.6 real, 4048.3 MB
[runlim] sample:		288.5 time, 590.6 real, 4123.1 MB
[runlim] sample:		298.5 time, 600.6 real, 4234.2 MB
[runlim] sample:		308.4 time, 610.6 real, 4339.7 MB
[runlim] sample:		318.4 time, 620.6 real, 4440.4 MB
[runlim] sample:		328.4 time, 630.6 real, 5355.4 MB
[runlim] sample:		338.4 time, 640.6 real, 5474.1 MB
[runlim] sample:		348.4 time, 650.6 real, 5551.7 MB
[runlim] sample:		358.4 time, 660.6 real, 5583.7 MB
[runlim] sample:		368.4 time, 670.6 real, 5671.9 MB
[runlim] sample:		378.4 time, 680.6 real, 5781.5 MB
[runlim] sample:		388.4 time, 690.6 real, 5891.0 MB
[runlim] sample:		398.3 time, 700.6 real, 6032.0 MB
[runlim] sample:		408.3 time, 710.6 real, 6114.4 MB
[runlim] sample:		418.3 time, 720.6 real, 6200.5 MB
[runlim] sample:		428.3 time, 730.6 real, 6303.7 MB
[runlim] sample:		438.3 time, 740.6 real, 6399.6 MB
[runlim] sample:		448.3 time, 750.6 real, 6487.8 MB
[runlim] sample:		458.3 time, 760.6 real, 6506.2 MB
[runlim] sample:		468.3 time, 770.6 real, 6623.1 MB
[runlim] sample:		478.2 time, 780.6 real, 6714.1 MB
[runlim] sample:		488.2 time, 790.6 real, 6821.3 MB
[runlim] sample:		498.2 time, 800.6 real, 6915.6 MB
[runlim] sample:		508.2 time, 810.6 real, 6962.6 MB
[runlim] end:			Thu Sep 17 12:43:25 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		5
[runlim] real:			811.51 seconds
[runlim] time:			508.99 seconds
[runlim] space:			7019.7 MB
[runlim] samples:		8108
