[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014bmc /home/biere/hwmcc15/benchmarks/hwmcc14/single/6s105.aig
[launch.sh] host:  atom02 (atom02)
[launch.sh] start: Thu Oct  1 10:12:59 CEST 2015
[launch.sh] jobid: 7202419
[launch.sh] name:  h6s105tip2014bmc
[launch.sh] round 1: killall abcpdr avy avybmc navy
[launch.sh] round 2: killall abcpdr avy avybmc navy
[launch.sh] round 3: killall abcpdr avy avybmc navy
c [single.tip2014] /home/biere/hwmcc15/solvers/tip/tip -alg=bmc -k=1000 /home/biere/hwmcc15/benchmarks/hwmcc14/single/6s105.aig /tmp/7202419.1.queue/6s105.tip.out
max_var   = 2825
n_inputs  = 49
n_outputs = 1
n_flops   = 151
n_gates   = 2625
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 2825
circ-stats: #flops=151, #gates=2613, #inps=49, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=151, #gates=2612, #inps=49, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 10 to 9!
[temporalDecomposition] unrolling 2 cycles.
[bmc] k=  0, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  1, vrs=     366, cls=1.13e+03, con=       1, time=0.0 s
[bmc] k=  1, vrs=1.52e+03, cls=4.82e+03, con=       2, time=0.0 s
restarts              : 2
conflicts             : 2              (inf /sec)
decisions             : 0              (-nan % random) (-nan /sec)
propagations          : 96             (inf /sec)
conflict literals     : 2              (0.00 % deleted)
Memory used           : 7.61 MB
CPU time              : 0 s
circ-stats: #flops=151, #gates=2453, #inps=49, #reset-gates=4174, #reset-inps=98
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=150, #gates=2188, #inps=25, #reset-gates=3857, #reset-inps=72
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=150, #gates=2188, #inps=25, #reset-gates=3857, #reset-inps=72
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[bmc] k=  0, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  1, vrs=2.98e+03, cls=9.52e+03, con=       1, time=0.0 s
[bmc] k=  2, vrs=4.45e+03, cls=1.43e+04, con=       2, time=0.0 s
[bmc] k=  3, vrs=5.93e+03, cls=1.91e+04, con=       3, time=0.0 s
[bmc] k=  4, vrs=7.41e+03, cls=2.39e+04, con=       4, time=0.0 s
[bmc] k=  5, vrs=8.93e+03, cls=2.88e+04, con=       5, time=0.0 s
[bmc] k=  6, vrs=1.05e+04, cls=3.38e+04, con=       6, time=0.0 s
[bmc] k=  7, vrs= 1.2e+04, cls=3.89e+04, con=       7, time=0.0 s
[bmc] k=  8, vrs=1.36e+04, cls= 4.4e+04, con=       8, time=0.0 s
[bmc] k=  9, vrs=1.54e+04, cls=4.97e+04, con=      77, time=0.0 s
[bmc] k= 10, vrs= 1.7e+04, cls= 5.5e+04, con=3.25e+03, time=0.3 s
[bmc] k= 11, vrs=1.86e+04, cls=6.02e+04, con=9.03e+03, time=0.9 s
[bmc] k= 12, vrs=2.02e+04, cls=6.55e+04, con= 1.4e+04, time=1.5 s
[bmc] k= 13, vrs=2.18e+04, cls=7.08e+04, con=1.88e+04, time=2.2 s
[bmc] k= 14, vrs=2.35e+04, cls=7.61e+04, con=2.43e+04, time=3.1 s
[bmc] k= 15, vrs=2.51e+04, cls=8.14e+04, con=2.96e+04, time=4.0 s
[bmc] k= 16, vrs=2.67e+04, cls=8.68e+04, con=3.54e+04, time=4.8 s
[bmc] k= 17, vrs=2.83e+04, cls=9.21e+04, con=4.04e+04, time=5.5 s
[bmc] k= 18, vrs=   3e+04, cls=9.74e+04, con=4.57e+04, time=6.4 s
[bmc] k= 19, vrs=3.16e+04, cls=1.03e+05, con=5.02e+04, time=7.3 s
[bmc] k= 20, vrs=3.32e+04, cls=1.08e+05, con=6.82e+04, time=10.9 s
[bmc] k= 21, vrs=3.49e+04, cls=1.13e+05, con=1.19e+05, time=23.6 s
[bmc] k= 22, vrs=3.65e+04, cls=1.19e+05, con=2.17e+05, time=55.9 s
[bmc] k= 23, vrs=3.81e+04, cls=1.24e+05, con=3.51e+05, time=108.5 s
[bmc] k= 24, vrs=3.98e+04, cls=1.29e+05, con=5.18e+05, time=186.0 s
[bmc] k= 25, vrs=4.14e+04, cls=1.35e+05, con=8.17e+05, time=319.2 s
[bmc] k= 26, vrs= 4.3e+04, cls= 1.4e+05, con=1.19e+06, time=495.6 s
[bmc] k= 27, vrs=4.46e+04, cls=1.45e+05, con=1.67e+06, time=733.0 s
[bmc] k= 28, vrs=4.63e+04, cls=1.51e+05, con=2.68e+06, time=1258.5 s
[bmc] k= 29, vrs=4.79e+04, cls=1.56e+05, con=3.83e+06, time=1890.8 s
[bmc] k= 30, vrs=4.95e+04, cls=1.61e+05, con=5.05e+06, time=2608.9 s

*** INTERRUPTED***
[launch.sh] stop:  Thu Oct  1 11:13:02 CEST 2015
[launch.sh] round 1: killall abcpdr avy avybmc navy
[launch.sh] round 2: killall abcpdr avy avybmc navy
[launch.sh] round 3: killall abcpdr avy avybmc navy
[launch.sh] sync: Thu Oct  1 11:13:05 CEST 2015
[launch.sh] out: cat /tmp/7202419.1.queue/6s105.tip.out
u31
[launch.sh] done: Thu Oct  1 11:13:05 CEST 2015
