[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b27s.aig
[launch.sh] host:  atom10 (atom10)
[launch.sh] start: Thu Sep 17 06:15:15 CEST 2015
[launch.sh] jobid: 7191344
[launch.sh] name:  oski15a14b27stip2014
[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/oski15a14b27s.aig /tmp/7191344.1.queue/oski15a14b27s.tip.out
max_var   = 47383
n_inputs  = 1071
n_outputs = 1
n_flops   = 3519
n_gates   = 42793
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 47383
circ-stats: #flops=3519, #gates=42793, #inps=1071, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=3455, #gates=33410, #inps=1023, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 8 to 7!
[detectEquivalentFlops] equivs 7: { 1, i4477 }
[detectEquivalentFlops] equivs holds at an earlier time point: 1
[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              (62 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 8.91 MB
CPU time              : 0.016157 s
circ-stats: #flops=3455, #gates=29996, #inps=1023, #reset-gates=9903, #reset-inps=2046
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=3454, #gates=29996, #inps=1023, #reset-gates=6747, #reset-inps=1736
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=3454, #gates=29996, #inps=1023, #reset-gates=6747, #reset-inps=1736
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[bmc] k=  0, vrs=5.16e+03, cls=1.28e+04, con=       1, time=0.0 s
[bmc] k=  1, vrs=9.72e+03, cls=2.82e+04, con=       3, time=0.0 s
[bmc] k=  2, vrs=1.93e+04, cls= 6.2e+04, con=       7, time=0.0 s
[bmc] k=  3, vrs=3.04e+04, cls=1.02e+05, con=      10, time=0.0 s
[rip] 2: 96 | 316 76 73 (2) = 563, time = 20.9 s, #safes=1, #lives=0
[rip] 3: 188 367 | 97 83 67 6 (17) = 825, time = 32.8 s, #safes=1, #lives=0
[rip] 4: 164 505 398 | 142 100 14 1 (95) = 1420, time = 56.4 s, #safes=1, #lives=0
[rip] 5: 146 554 668 617 | 266 38 15 3 2 (293) = 2604, time = 104.1 s, #safes=1, #lives=0
[rip] 6: 137 585 761 3245 2246 | 380 179 24 14 3 17 15 2 (1015) = 8632, time = 324.0 s, #safes=1, #lives=0

*** INTERRUPTED***
[launch.sh] stop:  Thu Sep 17 07:15:18 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 07:15:21 CEST 2015
[launch.sh] out: cat /tmp/7191344.1.queue/oski15a14b27s.tip.out
u4
[launch.sh] done: Thu Sep 17 07:15:21 CEST 2015
