[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b21s.aig
[launch.sh] host:  atom20 (atom20)
[launch.sh] start: Thu Sep 17 06:06:19 CEST 2015
[launch.sh] jobid: 7191296
[launch.sh] name:  oski15a14b21stip2014
[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/oski15a14b21s.aig /tmp/7191296.1.queue/oski15a14b21s.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=3467, #gates=37895, #inps=1045, #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, i4511 }
[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              (64 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 9.06 MB
CPU time              : 0.015743 s
circ-stats: #flops=3467, #gates=34469, #inps=1045, #reset-gates=13537, #reset-inps=2090
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=3466, #gates=34469, #inps=1045, #reset-gates=9029, #reset-inps=1748
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=3466, #gates=34469, #inps=1045, #reset-gates=9029, #reset-inps=1748
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[bmc] k=  0, vrs=5.88e+03, cls=1.55e+04, con=       1, time=0.0 s
[bmc] k=  1, vrs=1.52e+04, cls=4.74e+04, con=       2, time=0.0 s
[bmc] k=  2, vrs=2.88e+04, cls=9.36e+04, con=       3, time=0.0 s
[bmc] k=  3, vrs=4.38e+04, cls=1.45e+05, con=      17, time=0.1 s
[rip] 2: 362 | 453 222 171 389 (204) = 1801, time = 119.8 s, #safes=1, #lives=0
[rip] 3: 362 453 | 223 171 416 3 (204) = 1832, time = 125.3 s, #safes=1, #lives=0
[rip] 4: 358 452 743 | 214 434 10 6 (268) = 2485, time = 179.0 s, #safes=1, #lives=0
[rip] 5: 314 483 535 489 | 866 195 254 57 14 (463) = 3670, time = 369.0 s, #safes=1, #lives=0
[rip] 6: 312 483 509 303 613 | 275 191 230 178 146 141 38 10 1 (500) = 3930, time = 430.0 s, #safes=1, #lives=0
[tip] Safety property 0 was falsified (rip)
[rip] 6: 312 485 511 312 655 | 496 309 305 214 244 180 63 24 5 (622) = 4737, time = 517.5 s, #safes=0, #lives=0
Rip statistics:
================================================================================

Clauses:
  Added:             7526
  Backward subsumed: 2789
  Moved:             4979
  Revived:           0
  Avg. size:         3.7
  Total Literals:    27564 (99.6% deleted)
  Generalizations:   38489 (5.1 / clause)


Candidate Clauses:
  Added:             7063
  Forward subsumed:  47
  Revived:           10
  Avg. size:         934.7
  Total Literals:    6601483 (73.0% deleted)

SAT-solving:      Init-Instance  Step-Instance Prop-Instance
  Solves:                 24671         105309         42931
  Conflicts:                117          33534         28912
  Propagations:        21393326     1108314744    1236280354
  CPU-Time:                 3.6 s        207.7 s        305.4 s

CPU-time:
  Rip:   517.46 s
  Bmc:   0.06 s
  Total: 518.40 s

Resources used
================================================================================
  CPU time:       518.43 s
  Peak memory:    113.9 Mb

Verification results
================================================================================
  Proved:     0
  Falsified:  1
  Unknown:    0
[launch.sh] stop:  Thu Sep 17 06:15:01 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 06:15:04 CEST 2015
[launch.sh] out: cat /tmp/7191296.1.queue/oski15a14b21s.tip.out
1
b0
[encoded data, 17442 characters]
.
[launch.sh] done: Thu Sep 17 06:15:05 CEST 2015
