[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/all/selection/random/oski2b2i.aig
[runlim] start:			Mon Sep 21 02:36:02 2015
[runlim] main pid:		17378
[runlim] sample:		9.4 time, 10.3 real, 319.6 MB
[runlim] sample:		19.4 time, 20.3 real, 319.6 MB
[runlim] sample:		29.4 time, 30.3 real, 319.6 MB
[runlim] sample:		45.6 time, 40.3 real, 1559.7 MB
[runlim] sample:		75.6 time, 50.3 real, 2142.6 MB
[runlim] sample:		105.6 time, 60.3 real, 2556.7 MB
[runlim] sample:		135.6 time, 70.3 real, 2672.7 MB
[runlim] sample:		165.6 time, 80.3 real, 3012.4 MB
[runlim] sample:		195.6 time, 90.3 real, 3159.6 MB
[runlim] sample:		225.6 time, 100.3 real, 3351.3 MB
[runlim] sample:		255.6 time, 110.3 real, 3428.5 MB
[runlim] sample:		285.6 time, 120.3 real, 3596.6 MB
[runlim] sample:		315.6 time, 130.3 real, 3984.2 MB
[runlim] sample:		345.6 time, 140.3 real, 4222.2 MB
[runlim] sample:		375.6 time, 150.3 real, 4331.5 MB
[runlim] sample:		405.6 time, 160.3 real, 4486.6 MB
[runlim] sample:		435.6 time, 170.3 real, 4560.9 MB
[runlim] sample:		465.6 time, 180.3 real, 4730.5 MB
[runlim] sample:		495.6 time, 190.3 real, 4823.9 MB
[runlim] sample:		525.5 time, 200.3 real, 4939.4 MB
[runlim] sample:		555.5 time, 210.3 real, 5002.7 MB
[runlim] sample:		585.5 time, 220.3 real, 5158.4 MB
[runlim] sample:		615.5 time, 230.3 real, 5318.3 MB
[runlim] sample:		645.5 time, 240.3 real, 5390.1 MB
[runlim] sample:		675.5 time, 250.3 real, 5500.8 MB
[runlim] sample:		705.5 time, 260.3 real, 6084.6 MB
[runlim] sample:		735.5 time, 270.3 real, 6566.3 MB
[runlim] sample:		765.5 time, 280.3 real, 6677.7 MB
[runlim] sample:		795.5 time, 290.3 real, 6841.2 MB
[runlim] sample:		825.5 time, 300.3 real, 6832.5 MB
[runlim] sample:		855.5 time, 310.3 real, 6943.3 MB
[runlim] end:			Mon Sep 21 02:41:16 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		9
[runlim] real:			314.47 seconds
[runlim] time:			867.21 seconds
[runlim] space:			7000.8 MB
[runlim] samples:		3141
