[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b42s.aig
[launch.sh] host:  atom01 (atom01)
[launch.sh] start: Thu Sep 17 22:58:03 CEST 2015
[launch.sh] jobid: 7192592
[launch.sh] name:  oski15a01b42stip2014
[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/oski15a01b42s.aig /tmp/7192592.1.queue/oski15a01b42s.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=25197, #gates=287537, #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, -i16722, i16731, -i16860, i16869, -i16998, i17007, -i17136, i17145, -i17274, i17283, -i17412, i17421, -i17550, i17559, -i17688, i17697, -i17826, i17835, -i17964, i17973, -i18102, i18111, -i18240, i18249, -i18378, i18387, -i18516, i18525, -i18654, i18663, -i18792, i18801, -i18930, i18939, -i19068, i19077, i19262, i19265, i19280, i19283, -i19322, i19331, -i19484, i19493, -i19646, i19655, -i19808, i19817, -i19970, i19979, -i20132, i20141, -i20294, i20303, -i20456, i20465, -i20618, i20627, -i20780, i20789, -i20942, i20951, -i21104, i21113, -i21266, i21275, -i21428, i21437, -i21590, i21599, -i21752, i21761, -i21914, i21923, -i22076, i22085, i23699, i25948, i26682, i26683, i26684, i26685, i26686, i26687, i26688, i26689, i26690, i26691, i26692, i26693, i26694, i26695, i26696, i26697, i26698, i26699, i26865, i26866, i26867, i26868, i26869, i26870, i26871, i26872, i26873, i26874, i26875, i26876, i26877, i26878, i26879, i26880, i26881, i26882, i40323 }
[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           : 25.56 MB
CPU time              : 0.21055 s
circ-stats: #flops=25197, #gates=263812, #inps=15127, #reset-gates=207451, #reset-inps=45381
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=24938, #gates=263532, #inps=15127, #reset-gates=135491, #reset-inps=39749
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=24938, #gates=263532, #inps=15127, #reset-gates=135491, #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=       0, cls=       0, con=       0, time=0.1 s

*** INTERRUPTED***
[launch.sh] stop:  Thu Sep 17 23:58:06 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 23:58:09 CEST 2015
[launch.sh] out: cat /tmp/7192592.1.queue/oski15a01b42s.tip.out
u5
[launch.sh] done: Thu Sep 17 23:58:09 CEST 2015
