[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b08s.aig
[launch.sh] host:  atom19 (atom19)
[launch.sh] start: Thu Sep 17 23:45:11 CEST 2015
[launch.sh] jobid: 7192624
[launch.sh] name:  oski15a01b08stip2014
[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/oski15a01b08s.aig /tmp/7192624.1.queue/oski15a01b08s.tip.out
max_var   = 347313
n_inputs  = 15127
n_outputs = 1
n_flops   = 25715
n_gates   = 306471
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 347313
circ-stats: #flops=25715, #gates=306471, #inps=15127, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=25208, #gates=288815, #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, i16544, -i16736, i16745, -i16874, i16883, -i17012, i17021, -i17150, i17159, -i17288, i17297, -i17426, i17435, -i17564, i17573, -i17702, i17711, -i17840, i17849, -i17978, i17987, -i18116, i18125, -i18254, i18263, -i18392, i18401, -i18530, i18539, -i18668, i18677, -i18806, i18815, -i18944, i18953, -i19082, i19091, i19276, i19279, i19294, i19297, -i19336, i19345, -i19498, i19507, -i19660, i19669, -i19822, i19831, -i19984, i19993, -i20146, i20155, -i20308, i20317, -i20470, i20479, -i20632, i20641, -i20794, i20803, -i20956, i20965, -i21118, i21127, -i21280, i21289, -i21442, i21451, -i21604, i21613, -i21766, i21775, -i21928, i21937, -i22090, i22099, i23709, i23715, i25961, i26695, i26696, i26697, i26698, i26699, i26700, i26701, i26702, i26703, i26704, i26705, i26706, i26707, i26708, i26709, i26710, i26711, i26712, i26878, i26879, i26880, i26881, i26882, i26883, i26884, i26885, i26886, i26887, i26888, i26889, i26890, i26891, i26892, i26893, i26894, i26895, i30124, i40334 }
[detectEquivalentFlops] equivs holds at an earlier time point: 4
[temporalDecomposition] unrolling 4 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=  3, vrs=       0, cls=       0, con=       0, time=0.0 s
[bmc] k=  3, vrs=       0, cls=       0, con=       0, time=0.0 s
restarts              : 4
conflicts             : 0              (0 /sec)
decisions             : 0              (-nan % random) (0 /sec)
propagations          : 1              (5 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 33.59 MB
CPU time              : 0.212384 s
circ-stats: #flops=25208, #gates=265085, #inps=15127, #reset-gates=358787, #reset-inps=60508
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=24946, #gates=264805, #inps=15127, #reset-gates=265938, #reset-inps=54876
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=24946, #gates=264805, #inps=15127, #reset-gates=265938, #reset-inps=54876
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.1 s
[bmc] k=  2, vrs=3.41e+05, cls=9.12e+05, con= 1.1e+03, time=1.4 s
[bmc] k=  3, vrs=4.51e+05, cls=1.31e+06, con=8.03e+03, time=29.5 s

*** INTERRUPTED***
[launch.sh] stop:  Fri Sep 18 00:45: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 00:45:17 CEST 2015
[launch.sh] out: cat /tmp/7192624.1.queue/oski15a01b08s.tip.out
u6
[launch.sh] done: Fri Sep 18 00:45:17 CEST 2015
