[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014bmc /home/biere/hwmcc15/benchmarks/hwmcc14/single/6s188.aig
[launch.sh] host:  atom05 (atom05)
[launch.sh] start: Thu Oct  1 10:19:43 CEST 2015
[launch.sh] jobid: 7202426
[launch.sh] name:  h6s188tip2014bmc
[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/6s188.aig /tmp/7202426.1.queue/6s188.tip.out
max_var   = 6682
n_inputs  = 30
n_outputs = 1
n_flops   = 786
n_gates   = 5866
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 6682
circ-stats: #flops=786, #gates=5866, #inps=30, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=786, #gates=5866, #inps=30, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 21 to 20!
[temporalDecomposition] unrolling 2 cycles.
[bmc] k=  0, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  1, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  1, vrs=       0, cls=       0, con=       0, time=0.0 s
restarts              : 2
conflicts             : 0              (0 /sec)
decisions             : 0              (-nan % random) (0 /sec)
propagations          : 1              (148 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 7.59 MB
CPU time              : 0.006742 s
circ-stats: #flops=786, #gates=5782, #inps=30, #reset-gates=245, #reset-inps=60
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=785, #gates=5782, #inps=30, #reset-gates=161, #reset-inps=43
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=785, #gates=5782, #inps=30, #reset-gates=161, #reset-inps=43
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=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  2, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  3, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  4, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  5, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  6, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  7, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  8, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  9, vrs=7.05e+03, cls=2.49e+04, con=      86, time=0.0 s
[bmc] k= 10, vrs=1.01e+04, cls=3.56e+04, con=     156, time=0.0 s
[bmc] k= 11, vrs=1.32e+04, cls=4.58e+04, con=     296, time=0.0 s
[bmc] k= 12, vrs=1.64e+04, cls=5.69e+04, con=     680, time=0.0 s
[bmc] k= 13, vrs=1.97e+04, cls=6.83e+04, con=1.43e+03, time=0.1 s
[bmc] k= 14, vrs= 2.3e+04, cls=7.97e+04, con=2.84e+03, time=0.2 s
[bmc] k= 15, vrs=2.62e+04, cls=9.11e+04, con=5.96e+03, time=0.4 s
[bmc] k= 16, vrs=2.98e+04, cls=1.03e+05, con=8.12e+03, time=0.5 s
[bmc] k= 17, vrs=3.33e+04, cls=1.16e+05, con=1.05e+04, time=0.7 s
[bmc] k= 18, vrs=3.68e+04, cls=1.28e+05, con=1.34e+04, time=0.9 s
[bmc] k= 19, vrs=4.04e+04, cls=1.41e+05, con= 1.7e+04, time=1.1 s
[bmc] k= 20, vrs= 4.4e+04, cls=1.53e+05, con=2.02e+04, time=1.4 s
[bmc] k= 21, vrs=4.76e+04, cls=1.65e+05, con=2.38e+04, time=1.6 s
[bmc] k= 22, vrs=5.12e+04, cls=1.78e+05, con=2.73e+04, time=1.9 s
[bmc] k= 23, vrs=5.49e+04, cls=1.91e+05, con=3.18e+04, time=2.2 s
[bmc] k= 24, vrs=5.85e+04, cls=2.03e+05, con=3.46e+04, time=2.4 s
[bmc] k= 25, vrs=6.21e+04, cls=2.16e+05, con=3.72e+04, time=2.6 s
[bmc] k= 26, vrs=6.58e+04, cls=2.29e+05, con=4.03e+04, time=2.9 s
[bmc] k= 27, vrs=6.94e+04, cls=2.41e+05, con=4.46e+04, time=3.3 s
[bmc] k= 28, vrs=7.26e+04, cls=2.52e+05, con= 3.3e+05, time=131.4 s
[bmc] k= 29, vrs=7.62e+04, cls=2.65e+05, con=3.77e+05, time=141.1 s
[bmc] k= 30, vrs=7.98e+04, cls=2.77e+05, con=4.15e+05, time=153.2 s
[bmc] k= 31, vrs=8.34e+04, cls= 2.9e+05, con=4.86e+05, time=174.8 s
[bmc] k= 32, vrs= 8.7e+04, cls=3.02e+05, con=5.46e+05, time=200.1 s
[bmc] k= 33, vrs=9.05e+04, cls=3.14e+05, con=6.29e+05, time=232.8 s
[bmc] k= 34, vrs=9.41e+04, cls=3.27e+05, con=7.19e+05, time=272.9 s
[bmc] k= 35, vrs=9.77e+04, cls=3.39e+05, con= 9.1e+05, time=372.9 s
[bmc] k= 36, vrs=1.01e+05, cls=3.52e+05, con=1.17e+06, time=531.3 s
[bmc] k= 37, vrs=1.05e+05, cls=3.64e+05, con=1.44e+06, time=714.1 s
[bmc] k= 38, vrs=1.08e+05, cls=3.76e+05, con= 1.8e+06, time=1024.6 s
[bmc] k= 39, vrs=1.12e+05, cls=3.89e+05, con=2.32e+06, time=1502.0 s
[bmc] k= 40, vrs=1.16e+05, cls=4.01e+05, con=2.98e+06, time=2191.2 s
[bmc] k= 41, vrs=1.19e+05, cls=4.14e+05, con=3.78e+06, time=3087.6 s

*** INTERRUPTED***
[launch.sh] stop:  Thu Oct  1 11:19:46 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:19:49 CEST 2015
[launch.sh] out: cat /tmp/7202426.1.queue/6s188.tip.out
u42
[launch.sh] done: Thu Oct  1 11:19:49 CEST 2015
