[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014bmc /home/biere/hwmcc15/benchmarks/all/selection/random/irstdme5.aig
[launch.sh] host:  atom11 (atom11)
[launch.sh] start: Thu Oct  1 06:04:39 CEST 2015
[launch.sh] jobid: 7202163
[launch.sh] name:  irstdme5tip2014bmc
[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/all/selection/random/irstdme5.aig /tmp/7202163.1.queue/irstdme5.tip.out
max_var   = 1461
n_inputs  = 148
n_outputs = 1
n_flops   = 165
n_gates   = 1148
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 1461
circ-stats: #flops=165, #gates=1148, #inps=148, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=165, #gates=1148, #inps=148, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 4 to 3!
[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              (-nan /sec)
decisions             : 0              (-nan % random) (-nan /sec)
propagations          : 1              (inf /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 7.28 MB
CPU time              : 0 s
circ-stats: #flops=165, #gates=1148, #inps=148, #reset-gates=34, #reset-inps=34
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=165, #gates=1148, #inps=148, #reset-gates=34, #reset-inps=34
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=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 10, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 11, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 12, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 13, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 14, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 15, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 16, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 17, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 18, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 19, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k= 20, vrs=4.39e+03, cls=1.19e+04, con=       2, time=0.0 s
[bmc] k= 21, vrs=4.84e+03, cls=1.32e+04, con=       7, time=0.0 s
[bmc] k= 22, vrs=5.27e+03, cls=1.46e+04, con=      84, time=0.0 s
[bmc] k= 23, vrs=5.76e+03, cls=1.56e+04, con=     181, time=0.0 s
[bmc] k= 24, vrs=6.26e+03, cls=1.71e+04, con=     252, time=0.0 s
[bmc] k= 25, vrs=6.84e+03, cls=1.88e+04, con=     345, time=0.0 s
[bmc] k= 26, vrs=7.41e+03, cls=2.02e+04, con=1.52e+03, time=0.0 s
[bmc] k= 27, vrs=7.93e+03, cls=2.16e+04, con= 2.9e+03, time=0.1 s
[bmc] k= 28, vrs=8.44e+03, cls=2.29e+04, con=3.69e+03, time=0.1 s
[bmc] k= 29, vrs=   9e+03, cls=2.44e+04, con=4.87e+03, time=0.2 s
[bmc] k= 30, vrs=9.61e+03, cls=2.61e+04, con=6.64e+03, time=0.2 s
[bmc] k= 31, vrs=1.02e+04, cls=2.78e+04, con=8.47e+03, time=0.3 s
[bmc] k= 32, vrs=1.08e+04, cls=2.96e+04, con=1.11e+04, time=0.4 s
[bmc] k= 33, vrs=1.14e+04, cls=3.13e+04, con=1.74e+04, time=0.6 s
[bmc] k= 34, vrs= 1.2e+04, cls= 3.3e+04, con= 3.4e+04, time=1.4 s
[bmc] k= 35, vrs=1.25e+04, cls=3.44e+04, con=5.01e+04, time=2.3 s
[bmc] k= 36, vrs=1.31e+04, cls=3.61e+04, con=6.81e+04, time=3.4 s
[bmc] k= 37, vrs=1.37e+04, cls=3.77e+04, con= 8.7e+04, time=4.4 s
[bmc] k= 38, vrs=1.43e+04, cls=3.94e+04, con=1.14e+05, time=6.0 s
[bmc] k= 39, vrs=1.49e+04, cls=4.11e+04, con=1.41e+05, time=7.7 s
[bmc] k= 40, vrs=1.55e+04, cls=4.29e+04, con=1.81e+05, time=10.5 s
[bmc] k= 41, vrs=1.61e+04, cls=4.46e+04, con=2.09e+05, time=12.2 s
[bmc] k= 42, vrs=1.68e+04, cls=4.63e+04, con=2.42e+05, time=14.5 s
[bmc] k= 43, vrs=1.74e+04, cls= 4.8e+04, con=2.67e+05, time=15.8 s
[bmc] k= 44, vrs= 1.8e+04, cls=4.98e+04, con=2.88e+05, time=17.1 s
[bmc] k= 45, vrs=1.86e+04, cls=5.15e+04, con=3.03e+05, time=18.2 s
[bmc] k= 46, vrs=1.92e+04, cls=5.32e+04, con=3.22e+05, time=19.5 s
[bmc] k= 47, vrs=1.98e+04, cls= 5.5e+04, con=3.53e+05, time=21.7 s
[bmc] k= 48, vrs=2.04e+04, cls=5.67e+04, con=3.87e+05, time=24.1 s
[bmc] k= 49, vrs= 2.1e+04, cls=5.84e+04, con=4.29e+05, time=27.4 s
[bmc] k= 50, vrs=2.16e+04, cls=6.01e+04, con=5.38e+05, time=37.1 s
[tip] Safety property 0 was falsified (bmc)
[bmc] k= 50, vrs=2.22e+04, cls=6.19e+04, con=5.48e+05, time=38.0 s
restarts              : 1902
conflicts             : 548345         (14420 /sec)
decisions             : 3390334        (0.00 % random) (89160 /sec)
propagations          : 192547300      (5063639 /sec)
conflict literals     : 32880619       (30.90 % deleted)
Memory used           : 78.24 MB
CPU time              : 38.0255 s
Resources used
================================================================================
  CPU time:       38.03 s
  Peak memory:    78.2 Mb

Verification results
================================================================================
  Proved:     0
  Falsified:  1
  Unknown:    0
[launch.sh] stop:  Thu Oct  1 06:05:20 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 06:05:23 CEST 2015
[launch.sh] out: cat /tmp/7202163.1.queue/irstdme5.tip.out
1
b0
[encoded data, 8009 characters]
.
[launch.sh] done: Thu Oct  1 06:05:24 CEST 2015
