[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/all/selection/random/6s43.aig
[launch.sh] host:  atom13 (atom13)
[launch.sh] start: Sun Sep 20 04:19:27 CEST 2015
[launch.sh] jobid: 7196688
[launch.sh] name:  h6s43tip2014
[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/all/selection/random/6s43.aig /tmp/7196688.1.queue/6s43.tip.out
max_var   = 8403
n_inputs  = 30
n_outputs = 1
n_flops   = 965
n_gates   = 7408
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 8403
circ-stats: #flops=965, #gates=7408, #inps=30, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=965, #gates=7408, #inps=30, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 27 to 26!
[detectEquivalentFlops] equivs 26: { 1, i995 }
[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              (146 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 7.77 MB
CPU time              : 0.006847 s
circ-stats: #flops=965, #gates=7304, #inps=30, #reset-gates=253, #reset-inps=60
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=964, #gates=7304, #inps=30, #reset-gates=182, #reset-inps=43
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=964, #gates=7304, #inps=30, #reset-gates=182, #reset-inps=43
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.0 s
[bmc] k=  3, vrs=       0, cls=       0, con=       0, time=0.0 s
[rip] 2: 28 | 14 (1) = 43, time = 0.2 s, #safes=1, #lives=0
[rip] 3: 37 37 | 28 3 (25) = 130, time = 0.7 s, #safes=1, #lives=0
[rip] 4: 41 32 47 | 21 4 (51) = 196, time = 1.4 s, #safes=1, #lives=0
[rip] 5: 41 32 46 55 | 21 10 0 0 (85) = 290, time = 2.2 s, #safes=1, #lives=0
[rip] 6: 46 33 35 56 69 | 24 21 1 0 0 (184) = 501, time = 4.5 s, #safes=1, #lives=0
[rip] 7: 46 31 33 53 92 162 | 53 13 0 0 (247) = 762, time = 7.8 s, #safes=1, #lives=0
[rip] 8: 46 29 56 84 111 359 438 | 42 7 8 0 0 (546) = 1765, time = 21.7 s, #safes=1, #lives=0
[rip] 9: 46 29 56 81 102 356 530 379 | 81 22 2 0 0 (715) = 2455, time = 37.1 s, #safes=1, #lives=0
[rip] 10: 46 29 56 81 101 336 465 335 286 | 81 25 0 0 (840) = 2750, time = 46.4 s, #safes=1, #lives=0
[rip] 11: 48 55 135 181 158 354 442 240 124 91 | 24 9 4 0 0 0 (1521) = 3541, time = 65.8 s, #safes=1, #lives=0
[rip] 12: 48 55 135 179 159 351 434 230 124 66 23 | 18 13 0 0 0 (1582) = 3577, time = 68.7 s, #safes=1, #lives=0
[rip] 13: 48 55 135 179 159 351 434 225 119 62 22 24 | 11 5 5 4 3 0 0 (1605) = 3623, time = 71.3 s, #safes=1, #lives=0
[rip] 14: 48 55 135 179 159 351 434 225 119 62 22 24 11 | 5 5 5 3 0 0 (1606) = 3625, time = 72.8 s, #safes=1, #lives=0
[rip] 15: 48 55 135 179 159 351 434 225 119 62 22 24 11 5 | 5 5 4 0 0 (1607) = 3627, time = 74.3 s, #safes=1, #lives=0
[rip] 16: 48 55 135 179 159 351 434 225 119 62 18 16 7 1 0 | 0 0 0 0 (1643) = 3629, time = 76.0 s, #safes=1, #lives=0
[tip] Safety property 0 was proved (rip)
[rip] 16: 48 55 135 179 159 351 434 225 119 62 18 16 7 1 0 | 0 0 0 0 (1643) = 3629, time = 76.0 s, #safes=0, #lives=0
Rip statistics:
================================================================================

Clauses:
  Added:             5416
  Backward subsumed: 1964
  Moved:             2919
  Revived:           0
  Avg. size:         5.6
  Total Literals:    30487 (90.5% deleted)
  Generalizations:   47866 (8.8 / clause)


Candidate Clauses:
  Added:             4889
  Forward subsumed:  561
  Revived:           119
  Avg. size:         54.8
  Total Literals:    268073 (94.3% deleted)

SAT-solving:      Init-Instance  Step-Instance Prop-Instance
  Solves:                 15007         117672         13852
  Conflicts:                 51          34629          9742
  Propagations:           28581      398576735      29383111
  CPU-Time:                 0.1 s         71.7 s          4.1 s

CPU-time:
  Rip:   75.96 s
  Bmc:   0.00 s
  Total: 76.02 s

Resources used
================================================================================
  CPU time:       76.03 s
  Peak memory:    15.0 Mb

Verification results
================================================================================
  Proved:     1
  Falsified:  0
  Unknown:    0
[launch.sh] stop:  Sun Sep 20 04:20:46 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: Sun Sep 20 04:20:49 CEST 2015
[launch.sh] out: cat /tmp/7196688.1.queue/6s43.tip.out
0
b0
.
[launch.sh] done: Sun Sep 20 04:20:50 CEST 2015
