[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.abcsimple
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/pdtswvqis10x6p2.aig
[runlim] start:			Sat Sep 19 19:10:06 2015
[runlim] main pid:		7596
[runlim] sample:		10.2 time, 10.3 real, 434.3 MB
[runlim] sample:		49.8 time, 20.3 real, 479.4 MB
[runlim] sample:		89.4 time, 30.3 real, 495.7 MB
[runlim] sample:		129.0 time, 40.3 real, 551.8 MB
[runlim] sample:		168.5 time, 50.3 real, 590.5 MB
[runlim] sample:		208.1 time, 60.3 real, 604.1 MB
[runlim] sample:		247.7 time, 70.3 real, 603.1 MB
[runlim] sample:		287.3 time, 80.3 real, 625.3 MB
[runlim] sample:		326.9 time, 90.3 real, 647.3 MB
[runlim] sample:		366.4 time, 100.3 real, 670.2 MB
[runlim] sample:		406.0 time, 110.3 real, 677.2 MB
[runlim] sample:		445.6 time, 120.3 real, 695.8 MB
[runlim] sample:		485.1 time, 130.3 real, 729.7 MB
[runlim] sample:		524.7 time, 140.3 real, 749.7 MB
[runlim] sample:		564.3 time, 150.3 real, 759.6 MB
[runlim] sample:		603.9 time, 160.3 real, 766.0 MB
[runlim] sample:		643.5 time, 170.3 real, 771.6 MB
[runlim] sample:		683.0 time, 180.3 real, 777.5 MB
[runlim] sample:		722.6 time, 190.3 real, 811.3 MB
[runlim] sample:		762.1 time, 200.3 real, 782.7 MB
[runlim] sample:		801.7 time, 210.3 real, 786.8 MB
[runlim] sample:		841.3 time, 220.3 real, 794.8 MB
[runlim] sample:		880.9 time, 230.3 real, 798.9 MB
[runlim] sample:		920.4 time, 240.3 real, 804.4 MB
[runlim] sample:		960.0 time, 250.3 real, 809.7 MB
[runlim] sample:		999.6 time, 260.3 real, 813.3 MB
[runlim] sample:		1039.2 time, 270.3 real, 815.2 MB
[runlim] sample:		1078.7 time, 280.3 real, 850.6 MB
[runlim] sample:		1118.3 time, 290.3 real, 858.4 MB
[runlim] sample:		1157.9 time, 300.3 real, 865.9 MB
[runlim] sample:		1197.5 time, 310.3 real, 874.6 MB
[runlim] sample:		1237.1 time, 320.3 real, 879.3 MB
[runlim] sample:		1276.6 time, 330.3 real, 839.0 MB
[runlim] sample:		1316.2 time, 340.3 real, 841.3 MB
[runlim] sample:		1355.8 time, 350.3 real, 847.8 MB
[runlim] sample:		1395.4 time, 360.3 real, 852.8 MB
[runlim] sample:		1435.0 time, 370.3 real, 861.1 MB
[runlim] sample:		1474.5 time, 380.3 real, 867.3 MB
[runlim] sample:		1514.1 time, 390.3 real, 868.6 MB
[runlim] sample:		1553.7 time, 400.3 real, 907.2 MB
[runlim] sample:		1593.3 time, 410.3 real, 920.6 MB
[runlim] sample:		1632.9 time, 420.3 real, 926.8 MB
[runlim] sample:		1672.5 time, 430.3 real, 930.1 MB
[runlim] sample:		1712.0 time, 440.3 real, 933.9 MB
[runlim] sample:		1751.6 time, 450.3 real, 937.3 MB
[runlim] sample:		1791.2 time, 460.3 real, 942.6 MB
[runlim] sample:		1830.7 time, 470.3 real, 946.0 MB
[runlim] sample:		1870.3 time, 480.3 real, 950.0 MB
[runlim] sample:		1909.9 time, 490.3 real, 952.5 MB
[runlim] sample:		1949.5 time, 500.3 real, 955.8 MB
[runlim] sample:		1989.0 time, 510.3 real, 962.7 MB
[runlim] sample:		2028.6 time, 520.3 real, 970.0 MB
[runlim] sample:		2068.2 time, 530.3 real, 976.1 MB
[runlim] sample:		2107.7 time, 540.3 real, 981.2 MB
[runlim] sample:		2147.3 time, 550.3 real, 985.5 MB
[runlim] sample:		2186.9 time, 560.3 real, 919.0 MB
[runlim] sample:		2226.5 time, 570.3 real, 925.7 MB
[runlim] sample:		2266.1 time, 580.3 real, 927.0 MB
[runlim] sample:		2305.6 time, 590.3 real, 927.8 MB
[runlim] sample:		2345.2 time, 600.3 real, 930.8 MB
[runlim] sample:		2384.8 time, 610.3 real, 931.7 MB
[runlim] sample:		2424.3 time, 620.3 real, 932.8 MB
[runlim] sample:		2463.9 time, 630.3 real, 933.8 MB
[runlim] sample:		2503.5 time, 640.3 real, 969.1 MB
[runlim] sample:		2543.1 time, 650.3 real, 972.7 MB
[runlim] sample:		2582.6 time, 660.3 real, 978.7 MB
[runlim] sample:		2622.2 time, 670.3 real, 981.3 MB
[runlim] sample:		2661.8 time, 680.3 real, 984.0 MB
[runlim] sample:		2701.4 time, 690.3 real, 986.8 MB
[runlim] sample:		2740.9 time, 700.3 real, 991.6 MB
[runlim] sample:		2780.5 time, 710.3 real, 994.3 MB
[runlim] sample:		2820.1 time, 720.3 real, 1001.2 MB
[runlim] sample:		2859.7 time, 730.3 real, 1004.5 MB
[runlim] sample:		2899.3 time, 740.3 real, 1007.8 MB
[runlim] sample:		2938.9 time, 750.3 real, 1013.6 MB
[runlim] sample:		2978.5 time, 760.3 real, 1016.1 MB
[runlim] sample:		3018.0 time, 770.3 real, 1019.6 MB
[runlim] sample:		3057.6 time, 780.3 real, 1022.4 MB
[runlim] sample:		3097.2 time, 790.3 real, 1030.1 MB
[runlim] sample:		3136.7 time, 800.3 real, 1034.2 MB
[runlim] sample:		3176.3 time, 810.3 real, 1040.5 MB
[runlim] sample:		3215.9 time, 820.3 real, 1044.0 MB
[runlim] sample:		3255.4 time, 830.3 real, 1052.6 MB
[runlim] sample:		3295.0 time, 840.3 real, 1055.7 MB
[runlim] sample:		3334.6 time, 850.3 real, 979.1 MB
[runlim] sample:		3374.2 time, 860.3 real, 983.3 MB
[runlim] sample:		3413.8 time, 870.3 real, 1003.4 MB
[runlim] sample:		3453.4 time, 880.3 real, 1010.0 MB
[runlim] sample:		3493.0 time, 890.3 real, 1015.3 MB
[runlim] sample:		3532.6 time, 900.3 real, 1019.4 MB
[runlim] sample:		3572.1 time, 910.3 real, 1055.2 MB
[runlim] sample:		3611.7 time, 920.3 real, 1061.3 MB
[runlim] sample:		3651.3 time, 930.3 real, 1072.4 MB
[runlim] sample:		3690.9 time, 940.3 real, 1075.5 MB
[runlim] sample:		3730.5 time, 950.3 real, 1078.5 MB
[runlim] sample:		3770.1 time, 960.3 real, 1081.0 MB
[runlim] sample:		3809.7 time, 970.3 real, 1119.5 MB
[runlim] sample:		3849.3 time, 980.3 real, 1066.5 MB
[runlim] sample:		3888.8 time, 990.3 real, 1072.0 MB
[runlim] sample:		3928.4 time, 1000.3 real, 1081.7 MB
[runlim] sample:		3968.0 time, 1010.3 real, 1086.5 MB
[runlim] sample:		4007.6 time, 1020.3 real, 1093.2 MB
[runlim] sample:		4047.2 time, 1030.3 real, 1098.8 MB
[runlim] sample:		4086.8 time, 1040.3 real, 1105.9 MB
[runlim] sample:		4126.4 time, 1050.3 real, 1111.0 MB
[runlim] sample:		4166.0 time, 1060.3 real, 1122.6 MB
[runlim] sample:		4205.5 time, 1070.3 real, 1135.6 MB
[runlim] sample:		4245.1 time, 1080.3 real, 1140.2 MB
[runlim] sample:		4284.7 time, 1090.3 real, 1145.8 MB
[runlim] sample:		4324.3 time, 1100.3 real, 1150.4 MB
[runlim] sample:		4363.9 time, 1110.3 real, 1155.5 MB
[runlim] end:			Sat Sep 19 19:28:44 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		145257
[runlim] real:			1118.80 seconds
[runlim] time:			4397.12 seconds
[runlim] space:			1157.8 MB
[runlim] samples:		11185
