[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/hwmcc14/single/intel048.aig
[launch.sh] host:  atom31 (atom31)
[launch.sh] start: Thu Sep 17 00:21:07 CEST 2015
[launch.sh] jobid: 7190960
[launch.sh] name:  intel048tip2014
[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 -k=1000 /home/biere/hwmcc15/benchmarks/hwmcc14/single/intel048.aig /tmp/7190960.1.queue/intel048.tip.out
max_var   = 252431
n_inputs  = 17838
n_outputs = 1
n_flops   = 17843
n_gates   = 216750
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 252431
circ-stats: #flops=17843, #gates=216750, #inps=17838, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=8848, #gates=216750, #inps=17838, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 4 to 2!
[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              (10 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 22.76 MB
CPU time              : 0.096392 s
circ-stats: #flops=8848, #gates=216743, #inps=17838, #reset-gates=344446, #reset-inps=35676
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=8845, #gates=143331, #inps=10046, #reset-gates=216654, #reset-inps=27883
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=8845, #gates=143331, #inps=10046, #reset-gates=216654, #reset-inps=27883
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[bmc] k=  0, vrs=1.17e+05, cls=3.68e+05, con=       1, time=0.2 s
[bmc] k=  1, vrs=1.99e+05, cls= 6.7e+05, con=       2, time=0.3 s
[bmc] k=  2, vrs= 2.8e+05, cls=9.54e+05, con=       3, time=0.4 s
[bmc] k=  3, vrs=3.61e+05, cls=1.24e+06, con=       4, time=0.6 s

*** INTERRUPTED***
[launch.sh] stop:  Thu Sep 17 01:21:10 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 Sep 17 01:21:13 CEST 2015
[launch.sh] out: cat /tmp/7190960.1.queue/intel048.tip.out
u4
[launch.sh] done: Thu Sep 17 01:21:13 CEST 2015
