[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/iprover/single.iproverhc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a08b15s.aig
[runlim] start:			Mon Sep 28 17:06:26 2015
[runlim] main pid:		16765
[runlim] sample:		9.6 time, 10.2 real, 509.1 MB
[runlim] sample:		19.5 time, 20.2 real, 995.2 MB
[runlim] sample:		29.5 time, 30.2 real, 1793.5 MB
[runlim] sample:		39.5 time, 40.2 real, 2267.4 MB
[runlim] sample:		49.5 time, 50.2 real, 2895.2 MB
[runlim] sample:		59.5 time, 60.2 real, 3480.1 MB
[runlim] sample:		69.5 time, 70.2 real, 4169.2 MB
[runlim] sample:		79.5 time, 80.2 real, 4685.0 MB
[runlim] sample:		89.4 time, 90.2 real, 5313.7 MB
[runlim] sample:		99.4 time, 100.2 real, 5839.5 MB
[runlim] sample:		109.4 time, 110.2 real, 6366.2 MB
[runlim] sample:		7.2 time, 120.2 real, 375.2 MB
[runlim] sample:		17.2 time, 130.2 real, 795.3 MB
[runlim] sample:		27.1 time, 140.2 real, 1603.3 MB
[runlim] sample:		37.1 time, 150.2 real, 2237.4 MB
[runlim] sample:		47.1 time, 160.2 real, 2707.1 MB
[runlim] sample:		57.1 time, 170.2 real, 3320.1 MB
[runlim] sample:		67.1 time, 180.2 real, 4007.2 MB
[runlim] sample:		77.1 time, 190.2 real, 4490.8 MB
[runlim] sample:		87.0 time, 200.2 real, 5136.5 MB
[runlim] sample:		97.0 time, 210.2 real, 5679.9 MB
[runlim] sample:		107.0 time, 220.2 real, 6196.5 MB
[runlim] sample:		4.2 time, 230.2 real, 262.7 MB
[runlim] sample:		14.2 time, 240.2 real, 621.2 MB
[runlim] sample:		24.2 time, 250.2 real, 1363.5 MB
[runlim] sample:		34.2 time, 260.2 real, 2182.3 MB
[runlim] sample:		44.2 time, 270.2 real, 2557.1 MB
[runlim] sample:		54.2 time, 280.2 real, 3224.6 MB
[runlim] sample:		64.2 time, 290.2 real, 3888.8 MB
[runlim] sample:		74.1 time, 300.2 real, 4385.4 MB
[runlim] sample:		84.1 time, 310.2 real, 5039.8 MB
[runlim] sample:		94.1 time, 320.2 real, 5597.4 MB
[runlim] sample:		104.1 time, 330.2 real, 6103.5 MB
[runlim] sample:		2.5 time, 340.2 real, 200.0 MB
[runlim] sample:		12.4 time, 350.2 real, 619.4 MB
[runlim] sample:		22.4 time, 360.2 real, 1217.4 MB
[runlim] sample:		32.4 time, 370.2 real, 2029.5 MB
[runlim] sample:		42.4 time, 380.2 real, 2402.6 MB
[runlim] sample:		52.4 time, 390.2 real, 3071.0 MB
[runlim] sample:		62.4 time, 400.2 real, 3736.9 MB
[runlim] sample:		72.3 time, 410.2 real, 4284.6 MB
[runlim] sample:		82.3 time, 420.2 real, 4875.9 MB
[runlim] sample:		92.3 time, 430.2 real, 5460.7 MB
[runlim] sample:		102.3 time, 440.2 real, 5975.0 MB
[runlim] sample:		0.0 time, 450.2 real, 3.7 MB
[runlim] sample:		9.8 time, 460.2 real, 521.1 MB
[runlim] sample:		19.8 time, 470.2 real, 1004.3 MB
[runlim] sample:		29.8 time, 480.2 real, 1799.4 MB
[runlim] sample:		39.8 time, 490.2 real, 2287.5 MB
[runlim] sample:		49.8 time, 500.2 real, 2916.3 MB
[runlim] sample:		59.7 time, 510.2 real, 3572.7 MB
[runlim] sample:		69.7 time, 520.2 real, 4226.7 MB
[runlim] sample:		79.7 time, 530.2 real, 4718.8 MB
[runlim] sample:		89.7 time, 540.2 real, 5365.8 MB
[runlim] sample:		99.7 time, 550.2 real, 5893.9 MB
[runlim] sample:		109.6 time, 560.2 real, 6429.4 MB
[runlim] end:			Mon Sep 28 17:15:47 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		33680
[runlim] real:			561.97 seconds
[runlim] time:			112.61 seconds
[runlim] space:			6553.4 MB
[runlim] samples:		5617
