[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/abc/single.abcsuprove
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/intel044.aig
[runlim] start:			Sat Sep 19 23:29:30 2015
[runlim] main pid:		6443
[runlim] sample:		21.0 time, 10.3 real, 416.8 MB
[runlim] sample:		11.3 time, 20.3 real, 566.9 MB
[runlim] sample:		34.1 time, 30.3 real, 441.0 MB
[runlim] sample:		73.7 time, 40.3 real, 462.5 MB
[runlim] sample:		113.3 time, 50.3 real, 475.4 MB
[runlim] sample:		152.9 time, 60.3 real, 476.1 MB
[runlim] sample:		192.5 time, 70.3 real, 506.2 MB
[runlim] sample:		34.0 time, 80.3 real, 412.5 MB
[runlim] sample:		73.6 time, 90.3 real, 438.9 MB
[runlim] sample:		113.3 time, 100.3 real, 453.1 MB
[runlim] sample:		152.9 time, 110.3 real, 474.9 MB
[runlim] sample:		192.5 time, 120.3 real, 496.7 MB
[runlim] sample:		232.1 time, 130.3 real, 516.4 MB
[runlim] sample:		271.8 time, 140.3 real, 543.8 MB
[runlim] sample:		311.4 time, 150.3 real, 560.8 MB
[runlim] sample:		351.0 time, 160.3 real, 543.3 MB
[runlim] sample:		390.6 time, 170.3 real, 565.7 MB
[runlim] sample:		430.3 time, 180.3 real, 602.9 MB
[runlim] sample:		469.9 time, 190.3 real, 620.3 MB
[runlim] sample:		509.5 time, 200.3 real, 646.1 MB
[runlim] sample:		549.1 time, 210.3 real, 620.2 MB
[runlim] sample:		588.8 time, 220.3 real, 646.8 MB
[runlim] sample:		628.4 time, 230.3 real, 723.1 MB
[runlim] sample:		668.0 time, 240.3 real, 749.1 MB
[runlim] sample:		707.6 time, 250.3 real, 776.3 MB
[runlim] sample:		747.2 time, 260.3 real, 746.6 MB
[runlim] sample:		786.8 time, 270.3 real, 761.4 MB
[runlim] sample:		826.4 time, 280.3 real, 723.8 MB
[runlim] sample:		866.0 time, 290.3 real, 731.8 MB
[runlim] end:			Sat Sep 19 23:34:21 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		35019
[runlim] real:			291.15 seconds
[runlim] time:			868.79 seconds
[runlim] space:			776.7 MB
[runlim] samples:		2908
