[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/oski15a14b24s.aig
[runlim] start:			Thu Sep 17 09:11:18 2015
[runlim] main pid:		3010
[runlim] sample:		18.2 time, 10.3 real, 255.7 MB
[runlim] sample:		38.2 time, 20.3 real, 292.6 MB
[runlim] sample:		58.1 time, 30.3 real, 314.9 MB
[runlim] sample:		78.1 time, 40.3 real, 341.1 MB
[runlim] sample:		98.1 time, 50.3 real, 346.7 MB
[runlim] sample:		118.1 time, 60.3 real, 358.0 MB
[runlim] sample:		138.1 time, 70.3 real, 366.4 MB
[runlim] sample:		79.5 time, 80.3 real, 267.8 MB
[runlim] sample:		89.5 time, 90.3 real, 267.8 MB
[runlim] sample:		99.5 time, 100.3 real, 267.8 MB
[runlim] sample:		109.5 time, 110.3 real, 267.8 MB
[runlim] sample:		143.5 time, 120.3 real, 2180.5 MB
[runlim] sample:		183.1 time, 130.3 real, 2255.3 MB
[runlim] sample:		222.7 time, 140.3 real, 2282.4 MB
[runlim] sample:		262.3 time, 150.3 real, 2387.1 MB
[runlim] sample:		301.9 time, 160.3 real, 2500.0 MB
[runlim] sample:		341.5 time, 170.3 real, 2508.8 MB
[runlim] sample:		381.1 time, 180.3 real, 2547.5 MB
[runlim] sample:		420.7 time, 190.3 real, 2582.9 MB
[runlim] sample:		460.3 time, 200.3 real, 2584.9 MB
[runlim] sample:		499.9 time, 210.3 real, 2649.7 MB
[runlim] sample:		539.5 time, 220.3 real, 2619.6 MB
[runlim] sample:		579.1 time, 230.3 real, 2681.7 MB
[runlim] sample:		618.7 time, 240.3 real, 2667.7 MB
[runlim] sample:		658.3 time, 250.3 real, 2676.6 MB
[runlim] sample:		697.9 time, 260.3 real, 2679.2 MB
[runlim] sample:		737.5 time, 270.3 real, 2804.3 MB
[runlim] sample:		777.1 time, 280.3 real, 2769.6 MB
[runlim] sample:		816.6 time, 290.3 real, 2790.3 MB
[runlim] sample:		856.2 time, 300.3 real, 2874.2 MB
[runlim] sample:		895.8 time, 310.3 real, 2907.9 MB
[runlim] sample:		935.5 time, 320.3 real, 2919.1 MB
[runlim] sample:		975.0 time, 330.3 real, 2919.5 MB
[runlim] sample:		1014.6 time, 340.3 real, 2918.2 MB
[runlim] sample:		1054.2 time, 350.3 real, 2907.3 MB
[runlim] sample:		1093.8 time, 360.3 real, 2926.3 MB
[runlim] sample:		1133.4 time, 370.3 real, 2928.3 MB
[runlim] sample:		1173.0 time, 380.3 real, 2929.3 MB
[runlim] sample:		1212.6 time, 390.3 real, 2931.3 MB
[runlim] sample:		1252.2 time, 400.3 real, 2932.4 MB
[runlim] sample:		1291.8 time, 410.3 real, 2922.6 MB
[runlim] sample:		1331.4 time, 420.3 real, 2926.9 MB
[runlim] sample:		1371.0 time, 430.3 real, 2925.2 MB
[runlim] sample:		1410.5 time, 440.3 real, 2925.3 MB
[runlim] sample:		1450.1 time, 450.3 real, 2928.1 MB
[runlim] sample:		1489.7 time, 460.3 real, 2928.7 MB
[runlim] sample:		1529.3 time, 470.3 real, 3037.3 MB
[runlim] sample:		1568.9 time, 480.3 real, 3041.1 MB
[runlim] sample:		1608.4 time, 490.3 real, 3011.6 MB
[runlim] sample:		1648.0 time, 500.3 real, 3013.5 MB
[runlim] sample:		1687.6 time, 510.3 real, 3013.5 MB
[runlim] sample:		1727.2 time, 520.3 real, 3015.8 MB
[runlim] sample:		1766.8 time, 530.3 real, 3024.3 MB
[runlim] sample:		1806.4 time, 540.3 real, 3026.1 MB
[runlim] sample:		1846.0 time, 550.3 real, 3028.1 MB
[runlim] sample:		1885.6 time, 560.3 real, 3032.3 MB
[runlim] sample:		1925.2 time, 570.3 real, 3033.1 MB
[runlim] sample:		1964.8 time, 580.3 real, 3036.6 MB
[runlim] sample:		2004.4 time, 590.3 real, 3039.3 MB
[runlim] sample:		2044.0 time, 600.3 real, 3039.3 MB
[runlim] sample:		2083.6 time, 610.3 real, 3225.4 MB
[runlim] sample:		2123.2 time, 620.3 real, 3349.0 MB
[runlim] sample:		2162.8 time, 630.3 real, 3469.1 MB
[runlim] sample:		2202.4 time, 640.3 real, 3540.2 MB
[runlim] sample:		2242.1 time, 650.3 real, 3756.4 MB
[runlim] sample:		2281.7 time, 660.3 real, 3791.0 MB
[runlim] sample:		2321.3 time, 670.3 real, 3813.1 MB
[runlim] sample:		2360.9 time, 680.3 real, 3814.2 MB
[runlim] sample:		2400.5 time, 690.3 real, 3815.2 MB
[runlim] sample:		2440.1 time, 700.3 real, 3828.7 MB
[runlim] sample:		2479.7 time, 710.3 real, 3829.9 MB
[runlim] sample:		2519.3 time, 720.3 real, 3831.8 MB
[runlim] sample:		2558.9 time, 730.3 real, 3834.5 MB
[runlim] sample:		2598.6 time, 740.3 real, 3835.0 MB
[runlim] sample:		2638.2 time, 750.3 real, 3837.8 MB
[runlim] sample:		2677.7 time, 760.3 real, 3841.0 MB
[runlim] sample:		2717.3 time, 770.3 real, 3843.0 MB
[runlim] sample:		2756.9 time, 780.3 real, 3859.2 MB
[runlim] sample:		2796.5 time, 790.3 real, 3864.2 MB
[runlim] sample:		2836.1 time, 800.3 real, 3886.8 MB
[runlim] sample:		2875.7 time, 810.3 real, 3876.3 MB
[runlim] sample:		2915.3 time, 820.3 real, 3893.8 MB
[runlim] sample:		2954.9 time, 830.3 real, 3944.0 MB
[runlim] sample:		2994.5 time, 840.3 real, 3944.0 MB
[runlim] end:			Thu Sep 17 09:25:24 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		734
[runlim] real:			846.99 seconds
[runlim] time:			3020.34 seconds
[runlim] space:			3950.9 MB
[runlim] samples:		8466
