[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/bc57sensorsp1neg.aig
[runlim] start:			Sat Sep 19 07:12:22 2015
[runlim] main pid:		7209
[runlim] sample:		22.3 time, 10.3 real, 546.7 MB
[runlim] sample:		18.3 time, 20.3 real, 282.4 MB
[runlim] sample:		57.8 time, 30.3 real, 711.3 MB
[runlim] sample:		97.4 time, 40.3 real, 782.9 MB
[runlim] sample:		78.2 time, 50.3 real, 339.5 MB
[runlim] sample:		117.8 time, 60.3 real, 366.5 MB
[runlim] sample:		157.5 time, 70.3 real, 387.4 MB
[runlim] sample:		33.8 time, 80.3 real, 466.2 MB
[runlim] sample:		73.4 time, 90.3 real, 519.5 MB
[runlim] sample:		113.0 time, 100.3 real, 542.9 MB
[runlim] sample:		152.6 time, 110.3 real, 572.2 MB
[runlim] sample:		192.2 time, 120.3 real, 580.0 MB
[runlim] sample:		42.2 time, 130.3 real, 512.5 MB
[runlim] sample:		81.8 time, 140.3 real, 557.8 MB
[runlim] sample:		121.5 time, 150.3 real, 577.7 MB
[runlim] sample:		161.1 time, 160.3 real, 603.3 MB
[runlim] sample:		180.6 time, 170.3 real, 591.4 MB
[runlim] sample:		44.6 time, 180.3 real, 487.2 MB
[runlim] sample:		84.2 time, 190.3 real, 531.9 MB
[runlim] sample:		123.9 time, 200.3 real, 554.5 MB
[runlim] sample:		163.5 time, 210.3 real, 578.7 MB
[runlim] sample:		203.1 time, 220.3 real, 596.0 MB
[runlim] sample:		28.0 time, 230.3 real, 491.2 MB
[runlim] sample:		67.6 time, 240.3 real, 528.9 MB
[runlim] sample:		107.2 time, 250.3 real, 587.8 MB
[runlim] sample:		146.9 time, 260.3 real, 606.1 MB
[runlim] sample:		186.5 time, 270.3 real, 633.4 MB
[runlim] end:			Sat Sep 19 07:17:00 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		35731
[runlim] real:			278.38 seconds
[runlim] time:			219.35 seconds
[runlim] space:			811.6 MB
[runlim] samples:		2780
