[launch.sh] args:  /home/biere/hwmcc15/solvers/tip/single.tip2014 /home/biere/hwmcc15/benchmarks/all/selection/random/pdtvisblackjack2.aig
[launch.sh] host:  atom11 (atom11)
[launch.sh] start: Sat Sep 19 17:39:43 CEST 2015
[launch.sh] jobid: 7196048
[launch.sh] name:  pdtvisblackjack2tip2014
[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/pdtvisblackjack2.aig /tmp/7196048.1.queue/pdtvisblackjack2.tip.out
max_var   = 3576
n_inputs  = 5
n_outputs = 1
n_flops   = 104
n_gates   = 3467
n_bads    = 0
n_cnstrs  = 0
n_justs   = 0
n_fairs   = 0
sum       = 3576
circ-stats: #flops=104, #gates=3421, #inps=5, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=103, #gates=3378, #inps=5, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
[detectEquivalentFlops] found loop from cycle 1 to 0!
[detectEquivalentFlops] equivs 0: { 1, -i6, -i7, -i8, -i9, -i10, -i11, -i12, -i13, -i14, -i15, -i16, -i17, -i18, -i19, -i20, -i21, -i22, -i23, -i24, -i25, -i26, -i27, -i28, -i29, -i30, -i31, -i32, -i33, -i34, -i35, -i36, -i37, -i38, -i39, -i40, -i41, -i42, -i43, -i44, -i45, -i46, -i47, -i48, -i49, -i50, -i51, -i52, -i53, -i54, -i55, -i56, -i57, -i58, -i59, -i60, -i61, -i62, -i63, -i64, -i65, -i66, -i67, -i68, -i69, -i70, -i71, -i72, -i73, -i74, -i75, -i76, -i77, -i78, -i79, -i80, -i81, -i82, -i83, -i84, -i85, -i86, -i87, -i88, -i89, -i90, -i91, -i92, -i93, -i94, -i95, -i96, -i97, -i98, -i99, -i100, -i101, -i102, -i103, -i104, -i105, -i106, -i107, -i108 }
[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              (-nan /sec)
decisions             : 0              (-nan % random) (-nan /sec)
propagations          : 1              (inf /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 7.47 MB
CPU time              : 0 s
circ-stats: #flops=103, #gates=53, #inps=5, #reset-gates=106, #reset-inps=10
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
circ-stats: #flops=0, #gates=0, #inps=0, #reset-gates=0, #reset-inps=0
prop-stats: #safes=1, #lives=0, #cnstrs=0, #fairs=0
Embedding fairness constraints...
circ-stats: #flops=0, #gates=0, #inps=0, #reset-gates=0, #reset-inps=0
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
[tip] Safety property 0 was proved (rip)
[rip] 1: | 0 (0) = 0, time = 0.0 s, #safes=0, #lives=0
Rip statistics:
================================================================================

Clauses:
  Added:             0
  Backward subsumed: 0
  Moved:             0
  Revived:           0
  Avg. size:         -nan
  Total Literals:    0 (-nan% deleted)
  Generalizations:   0 (-nan / clause)


Candidate Clauses:
  Added:             0
  Forward subsumed:  0
  Revived:           0
  Avg. size:         -nan
  Total Literals:    0 (-nan% deleted)

SAT-solving:      Init-Instance  Step-Instance Prop-Instance
  Solves:                     0              0             2
  Conflicts:                  0              0             0
  Propagations:               1              0             1
  CPU-Time:                 0.0 s          0.0 s          0.0 s

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

Resources used
================================================================================
  CPU time:       0.00 s
  Peak memory:    7.5 Mb

Verification results
================================================================================
  Proved:     1
  Falsified:  0
  Unknown:    0
[launch.sh] stop:  Sat Sep 19 17:39: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: Sat Sep 19 17:39:49 CEST 2015
[launch.sh] out: cat /tmp/7196048.1.queue/pdtvisblackjack2.tip.out
0
b0
.
[launch.sh] done: Sat Sep 19 17:39:49 CEST 2015
