[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b28s.aig
[launch.sh] host:  atom11 (atom11)
[launch.sh] start: Fri Sep 18 04:27:47 CEST 2015
[launch.sh] jobid: 7193120
[launch.sh] name:  oski15a01b28stip2014
[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/oski15a01b28s.aig /tmp/7193120.1.queue/oski15a01b28s.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=25198, #gates=288631, #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, -i16728, i16737, -i16866, i16875, -i17004, i17013, -i17142, i17151, -i17280, i17289, -i17418, i17427, -i17556, i17565, -i17694, i17703, -i17832, i17841, -i17970, i17979, -i18108, i18117, -i18246, i18255, -i18384, i18393, -i18522, i18531, -i18660, i18669, -i18798, i18807, -i18936, i18945, -i19074, i19083, i19268, i19271, i19286, i19289, -i19328, i19337, -i19490, i19499, -i19652, i19661, -i19814, i19823, -i19976, i19985, -i20138, i20147, -i20300, i20309, -i20462, i20471, -i20624, i20633, -i20786, i20795, -i20948, i20957, -i21110, i21119, -i21272, i21281, -i21434, i21443, -i21596, i21605, -i21758, i21767, -i21920, i21929, -i22082, i22091, i23705, i25952, i26686, i26687, i26688, i26689, i26690, i26691, i26692, i26693, i26694, i26695, i26696, i26697, i26698, i26699, i26700, i26701, i26702, i26703, i26869, i26870, i26871, i26872, i26873, i26874, i26875, i26876, i26877, i26878, i26879, i26880, i26881, i26882, i26883, i26884, i26885, i26886, i40324 }
[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.58 MB
CPU time              : 0.19371 s
circ-stats: #flops=25198, #gates=264921, #inps=15127, #reset-gates=211151, #reset-inps=45381
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=24939, #gates=264641, #inps=15127, #reset-gates=135491, #reset-inps=39749
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=24939, #gates=264641, #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
[rip] 2: 1118 | 67 1 (10) = 1196, time = 2744.1 s, #safes=1, #lives=0

*** INTERRUPTED***
[launch.sh] stop:  Fri Sep 18 05:27:50 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 05:27:53 CEST 2015
[launch.sh] out: cat /tmp/7193120.1.queue/oski15a01b28s.tip.out
u5
[launch.sh] done: Fri Sep 18 05:27:53 CEST 2015
