[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b60s.aig
[launch.sh] host:  atom32 (atom32)
[launch.sh] start: Fri Sep 18 05:38:11 CEST 2015
[launch.sh] jobid: 7193168
[launch.sh] name:  oski15a01b60stip2014
[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/oski15/submission/single/oski15a01b60s.aig /tmp/7193168.1.queue/oski15a01b60s.tip.out
max_var   = 347345
n_inputs  = 15127
n_outputs = 1
n_flops   = 25715
n_gates   = 306503
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 347345
circ-stats: #flops=25715, #gates=306503, #inps=15127, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=25271, #gates=292327, #inps=15127, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 18 to 17!
[detectEquivalentFlops] equivs 17: { 1, -i16773, i16782, -i16911, i16920, -i17049, i17058, -i17187, i17196, -i17325, i17334, -i17463, i17472, -i17601, i17610, -i17739, i17748, -i17877, i17886, -i18015, i18024, -i18153, i18162, -i18291, i18300, -i18429, i18438, -i18567, i18576, -i18705, i18714, -i18843, i18852, -i18981, i18990, -i19119, i19128, i19313, i19316, i19331, i19334, -i19373, i19382, -i19535, i19544, -i19697, i19706, -i19859, i19868, -i20021, i20030, -i20183, i20192, -i20345, i20354, -i20507, i20516, -i20669, i20678, -i20831, i20840, -i20993, i21002, -i21155, i21164, -i21317, i21326, -i21479, i21488, -i21641, i21650, -i21803, i21812, -i21965, i21974, -i22127, i22136, i23750, i25996, i26751, i26752, i26753, i26754, i26755, i26756, i26757, i26758, i26759, i26760, i26761, i26762, i26763, i26764, i26765, i26766, i26767, i26768, i26934, i26935, i26936, i26937, i26938, i26939, i26940, i26941, i26942, i26943, i26944, i26945, i26946, i26947, i26948, i26949, i26950, i26951, i40397 }
[detectEquivalentFlops] equivs holds at an earlier time point: 3
[temporalDecomposition] unrolling 3 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=  2, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  2, vrs=       0, cls=       0, con=       0, time=0.0 s
restarts              : 3
conflicts             : 0              (0 /sec)
decisions             : 0              (-nan % random) (0 /sec)
propagations          : 1              (5 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 27.87 MB
CPU time              : 0.200339 s
circ-stats: #flops=25271, #gates=268553, #inps=15127, #reset-gates=218144, #reset-inps=45381
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=25012, #gates=268273, #inps=15127, #reset-gates=142586, #reset-inps=39749
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=25012, #gates=268273, #inps=15127, #reset-gates=142586, #reset-inps=39749
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.1 s
[bmc] k=  3, vrs=3.45e+05, cls=9.21e+05, con=1.81e+04, time=27.2 s

*** INTERRUPTED***
[launch.sh] stop:  Fri Sep 18 06:38:14 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: Fri Sep 18 06:38:17 CEST 2015
[launch.sh] out: cat /tmp/7193168.1.queue/oski15a01b60s.tip.out
u5
[launch.sh] done: Fri Sep 18 06:38:17 CEST 2015
