[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/all/selection/random/6s281b35.aig
[launch.sh] host:  atom20 (atom20)
[launch.sh] start: Mon Sep 21 03:53:27 CEST 2015
[launch.sh] jobid: 7198624
[launch.sh] name:  h6s281b35tip2014
[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/6s281b35.aig /tmp/7198624.1.queue/6s281b35.tip.out
max_var   = 2447918
n_inputs  = 91099
n_outputs = 1
n_flops   = 177235
n_gates   = 2179584
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 2447918
circ-stats: #flops=177235, #gates=2072042, #inps=91099, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=3447, #gates=46870, #inps=1723, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 4 to 2!
[detectEquivalentFlops] equivs 2: { 1, i3602, i1725, i1899 }{ i1724, i1726, i1727, i1728, i1729, i1730, i1731, i1732, i1733, i1734, i1735, i1736, i1737 }
[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              (2 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 75.62 MB
CPU time              : 0.582317 s
circ-stats: #flops=3447, #gates=38772, #inps=1723, #reset-gates=25886, #reset-inps=3446
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=3388, #gates=38743, #inps=133, #reset-gates=25841, #reset-inps=1776
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=3388, #gates=38743, #inps=133, #reset-gates=25841, #reset-inps=1776
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[bmc] k=  0, vrs=7.85e+03, cls=2.44e+04, con=8.49e+03, time=0.2 s
[bmc] k=  1, vrs=7.85e+03, cls=2.44e+04, con=8.49e+03, time=0.2 s
[bmc] k=  2, vrs=1.83e+04, cls=6.56e+04, con=1.73e+04, time=0.5 s
[bmc] k=  3, vrs=1.83e+04, cls=6.56e+04, con=1.73e+04, time=0.5 s
[rip] 2: 3076 (16) = 3092, time = 109.9 s, #safes=1, #lives=0
[rip] 3: 1 3076 (17) = 3094, time = 249.4 s, #safes=1, #lives=0
[rip] 4: 1 2072 8193 | 0 0 (54) = 10320, time = 720.5 s, #safes=1, #lives=0
[tip] Safety property 0 was proved (rip)
[rip] 4: 1 2072 1 | 2 0 (8250) = 10326, time = 1143.3 s, #safes=0, #lives=0
Rip statistics:
================================================================================

Clauses:
  Added:             22635
  Backward subsumed: 12309
  Moved:             31
  Revived:           0
  Avg. size:         3.5
  Total Literals:    78211 (55.6% deleted)
  Generalizations:   114424 (5.1 / clause)


Candidate Clauses:
  Added:             23278
  Forward subsumed:  0
  Revived:           0
  Avg. size:         7.5
  Total Literals:    175461 (99.8% deleted)

SAT-solving:      Init-Instance  Step-Instance Prop-Instance
  Solves:                 59403         280890        112495
  Conflicts:                 34         178157        192935
  Propagations:        95033607     3015995064    2296970692
  CPU-Time:                15.7 s        587.7 s        539.2 s

CPU-time:
  Rip:   1143.30 s
  Bmc:   0.48 s
  Total: 1144.92 s

Resources used
================================================================================
  CPU time:       1145.53 s
  Peak memory:    83.0 Mb

Verification results
================================================================================
  Proved:     1
  Falsified:  0
  Unknown:    0
[launch.sh] stop:  Mon Sep 21 04:12:38 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: Mon Sep 21 04:12:41 CEST 2015
[launch.sh] out: cat /tmp/7198624.1.queue/6s281b35.tip.out
0
b0
.
[launch.sh] done: Mon Sep 21 04:12:41 CEST 2015
