[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/6s122.aig
[runlim] start:			Sat Sep 19 16:09:18 2015
[runlim] main pid:		10591
[runlim] sample:		19.3 time, 10.3 real, 496.8 MB
[runlim] sample:		59.0 time, 20.3 real, 519.9 MB
[runlim] sample:		98.6 time, 30.3 real, 556.2 MB
[runlim] sample:		8.1 time, 40.3 real, 581.3 MB
[runlim] sample:		34.5 time, 50.3 real, 610.1 MB
[runlim] sample:		74.2 time, 60.3 real, 739.9 MB
[runlim] sample:		80.6 time, 70.3 real, 681.9 MB
[runlim] sample:		94.8 time, 80.3 real, 693.2 MB
[runlim] sample:		107.4 time, 90.3 real, 344.7 MB
[runlim] sample:		146.9 time, 100.3 real, 725.5 MB
[runlim] sample:		186.5 time, 110.3 real, 787.6 MB
[runlim] sample:		226.1 time, 120.3 real, 813.2 MB
[runlim] sample:		265.8 time, 130.3 real, 840.6 MB
[runlim] sample:		305.4 time, 140.3 real, 865.8 MB
[runlim] sample:		345.0 time, 150.3 real, 891.1 MB
[runlim] sample:		384.7 time, 160.3 real, 916.3 MB
[runlim] sample:		424.2 time, 170.3 real, 936.1 MB
[runlim] sample:		463.9 time, 180.3 real, 963.9 MB
[runlim] sample:		503.5 time, 190.3 real, 988.7 MB
[runlim] sample:		543.1 time, 200.3 real, 1020.3 MB
[runlim] sample:		316.7 time, 210.3 real, 457.4 MB
[runlim] sample:		356.4 time, 220.3 real, 470.8 MB
[runlim] sample:		396.1 time, 230.3 real, 477.4 MB
[runlim] sample:		435.8 time, 240.3 real, 482.5 MB
[runlim] sample:		475.4 time, 250.3 real, 488.5 MB
[runlim] sample:		515.1 time, 260.3 real, 492.1 MB
[runlim] sample:		554.8 time, 270.3 real, 497.2 MB
[runlim] sample:		594.4 time, 280.3 real, 499.3 MB
[runlim] sample:		634.1 time, 290.3 real, 506.8 MB
[runlim] sample:		673.8 time, 300.3 real, 510.9 MB
[runlim] sample:		713.4 time, 310.3 real, 516.8 MB
[runlim] sample:		753.1 time, 320.3 real, 526.4 MB
[runlim] sample:		792.8 time, 330.3 real, 532.8 MB
[runlim] sample:		832.5 time, 340.3 real, 539.8 MB
[runlim] sample:		872.1 time, 350.3 real, 543.4 MB
[runlim] sample:		911.8 time, 360.3 real, 547.5 MB
[runlim] sample:		951.5 time, 370.3 real, 550.9 MB
[runlim] sample:		991.1 time, 380.3 real, 554.7 MB
[runlim] sample:		1030.8 time, 390.3 real, 558.3 MB
[runlim] sample:		1070.5 time, 400.3 real, 563.5 MB
[runlim] sample:		1110.2 time, 410.3 real, 566.9 MB
[runlim] sample:		1149.9 time, 420.3 real, 570.7 MB
[runlim] sample:		1189.5 time, 430.3 real, 573.5 MB
[runlim] sample:		1229.2 time, 440.3 real, 577.4 MB
[runlim] sample:		1268.9 time, 450.3 real, 581.5 MB
[runlim] sample:		1308.5 time, 460.3 real, 585.6 MB
[runlim] sample:		1348.2 time, 470.3 real, 586.7 MB
[runlim] sample:		1387.8 time, 480.3 real, 588.0 MB
[runlim] sample:		1427.5 time, 490.3 real, 595.1 MB
[runlim] sample:		1467.2 time, 500.3 real, 601.1 MB
[runlim] sample:		35.0 time, 510.3 real, 457.2 MB
[runlim] sample:		74.7 time, 520.3 real, 508.9 MB
[runlim] sample:		114.3 time, 530.3 real, 538.0 MB
[runlim] sample:		153.9 time, 540.3 real, 560.5 MB
[runlim] sample:		193.6 time, 550.3 real, 579.9 MB
[runlim] sample:		14.9 time, 560.3 real, 408.5 MB
[runlim] sample:		54.6 time, 570.3 real, 469.9 MB
[runlim] sample:		94.3 time, 580.3 real, 488.2 MB
[runlim] sample:		11.1 time, 590.3 real, 383.7 MB
[runlim] sample:		50.7 time, 600.3 real, 436.6 MB
[runlim] sample:		90.4 time, 610.3 real, 484.5 MB
[runlim] sample:		130.1 time, 620.3 real, 510.0 MB
[runlim] sample:		169.7 time, 630.3 real, 519.4 MB
[runlim] sample:		209.4 time, 640.3 real, 547.3 MB
[runlim] sample:		249.0 time, 650.3 real, 565.4 MB
[runlim] sample:		288.7 time, 660.3 real, 585.5 MB
[runlim] sample:		328.3 time, 670.3 real, 597.9 MB
[runlim] sample:		368.0 time, 680.3 real, 607.8 MB
[runlim] sample:		10.1 time, 690.3 real, 362.1 MB
[runlim] sample:		49.8 time, 700.3 real, 427.1 MB
[runlim] sample:		89.4 time, 710.3 real, 456.9 MB
[runlim] sample:		13.7 time, 720.3 real, 371.8 MB
[runlim] sample:		53.3 time, 730.3 real, 453.4 MB
[runlim] sample:		93.0 time, 740.3 real, 485.2 MB
[runlim] sample:		132.7 time, 750.3 real, 506.8 MB
[runlim] sample:		172.3 time, 760.3 real, 516.9 MB
[runlim] sample:		212.0 time, 770.3 real, 537.4 MB
[runlim] sample:		35.6 time, 780.3 real, 437.7 MB
[runlim] sample:		75.2 time, 790.3 real, 501.1 MB
[runlim] sample:		114.9 time, 800.3 real, 519.7 MB
[runlim] sample:		154.6 time, 810.3 real, 553.2 MB
[runlim] sample:		194.3 time, 820.3 real, 567.8 MB
[runlim] sample:		233.9 time, 830.3 real, 594.5 MB
[runlim] sample:		273.5 time, 840.3 real, 610.8 MB
[runlim] sample:		313.2 time, 850.3 real, 629.4 MB
[runlim] sample:		352.8 time, 860.3 real, 643.9 MB
[runlim] sample:		392.5 time, 870.3 real, 655.1 MB
[runlim] sample:		432.1 time, 880.3 real, 667.4 MB
[runlim] sample:		471.8 time, 890.3 real, 681.8 MB
[runlim] sample:		511.4 time, 900.3 real, 697.3 MB
[runlim] sample:		551.1 time, 910.3 real, 709.7 MB
[runlim] sample:		590.7 time, 920.3 real, 721.3 MB
[runlim] sample:		630.4 time, 930.3 real, 728.6 MB
[runlim] sample:		670.0 time, 940.3 real, 733.9 MB
[runlim] sample:		709.7 time, 950.3 real, 739.4 MB
[runlim] sample:		749.3 time, 960.3 real, 743.6 MB
[runlim] sample:		789.0 time, 970.3 real, 751.5 MB
[runlim] sample:		828.6 time, 980.3 real, 755.4 MB
[runlim] sample:		868.2 time, 990.3 real, 761.8 MB
[runlim] sample:		907.9 time, 1000.3 real, 766.4 MB
[runlim] sample:		947.6 time, 1010.3 real, 770.3 MB
[runlim] sample:		987.2 time, 1020.3 real, 772.6 MB
[runlim] sample:		1026.9 time, 1030.3 real, 786.8 MB
[runlim] sample:		1066.5 time, 1040.3 real, 797.2 MB
[runlim] sample:		1106.1 time, 1050.3 real, 796.2 MB
[runlim] sample:		1145.8 time, 1060.3 real, 806.5 MB
[runlim] sample:		1185.4 time, 1070.3 real, 809.9 MB
[runlim] sample:		1225.1 time, 1080.3 real, 811.4 MB
[runlim] sample:		1264.7 time, 1090.3 real, 814.0 MB
[runlim] sample:		1304.4 time, 1100.3 real, 816.2 MB
[runlim] sample:		1344.0 time, 1110.3 real, 820.1 MB
[runlim] sample:		1383.7 time, 1120.3 real, 823.4 MB
[runlim] sample:		1423.3 time, 1130.3 real, 825.0 MB
[runlim] sample:		1463.0 time, 1140.3 real, 827.6 MB
[runlim] sample:		1502.6 time, 1150.3 real, 830.0 MB
[runlim] sample:		1542.3 time, 1160.3 real, 834.1 MB
[runlim] sample:		1581.9 time, 1170.3 real, 838.9 MB
[runlim] sample:		1621.5 time, 1180.3 real, 845.8 MB
[runlim] sample:		1661.2 time, 1190.3 real, 849.6 MB
[runlim] end:			Sat Sep 19 16:29:16 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		140488
[runlim] real:			1198.53 seconds
[runlim] time:			1692.90 seconds
[runlim] space:			1021.7 MB
[runlim] samples:		11982
