[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/all/selection/random/bob12s03.aig
[launch.sh] host:  atom14 (atom14)
[launch.sh] start: Sun Sep 20 17:00:07 CEST 2015
[launch.sh] jobid: 7197600
[launch.sh] name:  bob12s03tip2014
[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/bob12s03.aig /tmp/7197600.1.queue/bob12s03.tip.out
max_var   = 38126
n_inputs  = 617
n_outputs = 1
n_flops   = 5174
n_gates   = 32335
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 38126
circ-stats: #flops=5174, #gates=32327, #inps=617, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=4889, #gates=31969, #inps=591, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 20 to 18!
[detectEquivalentFlops] equivs 18: { 1, i594, i600, i615, i624, -i1582, -i2806, -i2835, -i3050, -i3060, -i4983, -i5231, -i5232, -i5419, -i5420 }{ i592, i616, i617, i618, i619, i620, i621, i622, i623, i593, i595, i596, i597, i598, i599, i601, i602, i603, i604, i605, i606, i607, i608, i609, i610, i611, i612, i613, i614 }
[detectEquivalentFlops] equivs holds at an earlier time point: 2
[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              (48 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 8.80 MB
CPU time              : 0.020747 s
circ-stats: #flops=4889, #gates=30503, #inps=591, #reset-gates=2515, #reset-inps=1182
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=4753, #gates=30426, #inps=408, #reset-gates=1907, #reset-inps=675
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=4753, #gates=30426, #inps=408, #reset-gates=1907, #reset-inps=675
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: 5 | 1279 (69) = 1353, time = 34.5 s, #safes=1, #lives=0
[rip] 3: 5 1293 | 4 2 (81) = 1385, time = 38.9 s, #safes=1, #lives=0
[rip] 4: 5 1049 2310 | 2317 379 135 20 16 0 0 (747) = 6988, time = 280.2 s, #safes=1, #lives=0
[rip] 5: 5 1014 2218 2401 | 380 284 23 16 0 0 (757) = 7108, time = 306.4 s, #safes=1, #lives=0
[rip] 6: 5 776 2376 2489 2391 | 1072 334 1040 96 66 9 1 1 0 0 (857) = 11528, time = 591.1 s, #safes=1, #lives=0
[rip] 7: 5 776 2377 2468 2267 1288 | 350 1051 98 66 9 1 1 0 0 (860) = 11632, time = 632.6 s, #safes=1, #lives=0
[tip] Safety property 0 was falsified (rip)
[rip] 7: 5 778 2379 2468 2268 1289 | 354 1053 100 68 12 1 1 0 0 (860) = 11651, time = 633.4 s, #safes=0, #lives=0
Rip statistics:
================================================================================

Clauses:
  Added:             14162
  Backward subsumed: 2526
  Moved:             9968
  Revived:           0
  Avg. size:         3.0
  Total Literals:    42374 (95.0% deleted)
  Generalizations:   69118 (4.9 / clause)


Candidate Clauses:
  Added:             13478
  Forward subsumed:  637
  Revived:           138
  Avg. size:         55.8
  Total Literals:    751562 (98.8% deleted)

SAT-solving:      Init-Instance  Step-Instance Prop-Instance
  Solves:                 44973         244861         47842
  Conflicts:                587          99386        267994
  Propagations:         4915598     2885535612     553081838
  CPU-Time:                 0.9 s        514.4 s        117.1 s

CPU-time:
  Rip:   633.36 s
  Bmc:   0.00 s
  Total: 633.60 s

Resources used
================================================================================
  CPU time:       633.64 s
  Peak memory:    54.3 Mb

Verification results
================================================================================
  Proved:     0
  Falsified:  1
  Unknown:    0
[launch.sh] stop:  Sun Sep 20 17:10:45 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 17:10:48 CEST 2015
[launch.sh] out: cat /tmp/7197600.1.queue/bob12s03.tip.out
1
b0
[encoded data, 14429 characters]
.
[launch.sh] done: Sun Sep 20 17:10:48 CEST 2015
