[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/avy/single.avy
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/intel045.aig
[runlim] start:			Sat Sep 19 23:42:30 2015
[runlim] main pid:		18901
[runlim] sample:		35.5 time, 10.3 real, 243.5 MB
[runlim] sample:		75.1 time, 20.3 real, 314.5 MB
[runlim] sample:		114.7 time, 30.3 real, 331.2 MB
[runlim] sample:		154.3 time, 40.3 real, 363.4 MB
[runlim] sample:		193.9 time, 50.3 real, 415.5 MB
[runlim] sample:		233.5 time, 60.3 real, 449.8 MB
[runlim] sample:		273.1 time, 70.3 real, 483.7 MB
[runlim] sample:		312.8 time, 80.3 real, 539.6 MB
[runlim] sample:		352.4 time, 90.3 real, 537.4 MB
[runlim] sample:		392.0 time, 100.3 real, 590.8 MB
[runlim] sample:		431.7 time, 110.3 real, 592.6 MB
[runlim] sample:		471.2 time, 120.3 real, 626.6 MB
[runlim] sample:		510.8 time, 130.3 real, 716.2 MB
[runlim] sample:		550.5 time, 140.3 real, 703.5 MB
[runlim] sample:		590.1 time, 150.3 real, 776.3 MB
[runlim] sample:		629.7 time, 160.3 real, 748.4 MB
[runlim] sample:		669.3 time, 170.3 real, 806.7 MB
[runlim] sample:		708.9 time, 180.3 real, 843.1 MB
[runlim] sample:		748.5 time, 190.3 real, 852.1 MB
[runlim] sample:		788.1 time, 200.3 real, 928.4 MB
[runlim] sample:		827.6 time, 210.3 real, 882.1 MB
[runlim] sample:		867.2 time, 220.3 real, 907.8 MB
[runlim] end:			Sat Sep 19 23:46:19 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		9146
[runlim] real:			229.83 seconds
[runlim] time:			904.07 seconds
[runlim] space:			1025.6 MB
[runlim] samples:		2295
