[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/6s392r.aig
[runlim] start:			Wed Sep 16 11:01:50 2015
[runlim] main pid:		26512
[runlim] sample:		11.1 time, 10.3 real, 1910.5 MB
[runlim] sample:		18.7 time, 20.3 real, 1267.0 MB
[runlim] sample:		28.7 time, 30.3 real, 1452.2 MB
[runlim] sample:		38.7 time, 40.3 real, 1383.5 MB
[runlim] sample:		48.7 time, 50.3 real, 1383.5 MB
[runlim] sample:		58.7 time, 60.3 real, 1383.5 MB
[runlim] sample:		68.7 time, 70.3 real, 1394.1 MB
[runlim] sample:		88.5 time, 80.3 real, 2855.2 MB
[runlim] sample:		108.5 time, 90.3 real, 3282.4 MB
[runlim] sample:		128.5 time, 100.3 real, 3047.5 MB
[runlim] sample:		148.4 time, 110.3 real, 3257.4 MB
[runlim] sample:		168.4 time, 120.3 real, 3491.4 MB
[runlim] sample:		185.1 time, 130.3 real, 3634.3 MB
[runlim] sample:		204.1 time, 140.3 real, 3759.8 MB
[runlim] sample:		219.1 time, 150.3 real, 3972.8 MB
[runlim] sample:		236.4 time, 160.3 real, 4165.5 MB
[runlim] sample:		255.7 time, 170.3 real, 4389.4 MB
[runlim] sample:		274.8 time, 180.3 real, 4423.4 MB
[runlim] sample:		288.7 time, 190.3 real, 4548.9 MB
[runlim] sample:		308.7 time, 200.3 real, 4689.0 MB
[runlim] sample:		328.6 time, 210.3 real, 4715.0 MB
[runlim] sample:		345.0 time, 220.3 real, 4880.4 MB
[runlim] sample:		357.7 time, 230.3 real, 4964.4 MB
[runlim] sample:		377.7 time, 240.3 real, 5060.8 MB
[runlim] sample:		394.4 time, 250.3 real, 5207.1 MB
[runlim] sample:		414.4 time, 260.3 real, 5036.9 MB
[runlim] sample:		434.3 time, 270.3 real, 5276.2 MB
[runlim] sample:		454.3 time, 280.3 real, 5438.4 MB
[runlim] sample:		472.8 time, 290.3 real, 6100.8 MB
[runlim] sample:		485.6 time, 300.3 real, 5676.0 MB
[runlim] sample:		495.6 time, 310.3 real, 5846.4 MB
[runlim] sample:		505.6 time, 320.3 real, 6307.5 MB
[runlim] sample:		515.6 time, 330.3 real, 6061.0 MB
[runlim] sample:		525.5 time, 340.3 real, 6061.0 MB
[runlim] sample:		535.5 time, 350.3 real, 6061.0 MB
[runlim] sample:		545.5 time, 360.3 real, 6091.0 MB
[runlim] sample:		555.5 time, 370.3 real, 6045.4 MB
[runlim] sample:		566.3 time, 380.3 real, 0.0 MB
[runlim] end:			Wed Sep 16 11:08:10 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		42
[runlim] real:			380.63 seconds
[runlim] time:			566.51 seconds
[runlim] space:			7033.6 MB
[runlim] samples:		3802
