[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/beemmcs6f1.aig
[launch.sh] host:  atom18 (atom18)
[launch.sh] start: Sat Sep 19 03:12:43 CEST 2015
[launch.sh] jobid: 7194853
[launch.sh] name:  beemmcs6f1avy
[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
Working directory /tmp/7194853.1.queue/avy-YV5cuY
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/beemmcs6f1.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/beemmcs6f1.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/beemmcs6f1.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/beemmcs6f1.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig".

[pavy] finished pp, output=/tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/navy --reset-cover=1 --opt-bmc --kstep=1 --shallow-push=1 --min-suffix=1 --glucose --glucose-inc-mode=0 --sat-simp=0 --glucose_itp=1 --verbose=2 --cex=/tmp/7194853.1.queue/avy-YV5cuY/navy_avy0.cex /tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7194853.1.queue/avy-YV5cuY/abcpdr_avy1.cex /tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avy --reset-cover=1 -a --kstep=2 --shallow-push=1 --tr0=1 --min-suffix=1 --glucose --glucose-inc-mode=0 --min-core=1 --glucose_itp=1 --stick-error=1 --sat-simp=1 --verbose=2 --cex=/tmp/7194853.1.queue/avy-YV5cuY/avyabsmus_avy2.cex /tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7194853.1.queue/avy-YV5cuY/fib_avy3.cex /tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig
[pavy] running: [2551, 2552, 2553, 2554]
[pavy] finished pid 2552 with code 0 and signal 0
[pavy] trying to kill  2551
[pavy] waiting for  2551
[pavy] trying to kill  2553
[pavy] waiting for  2553
[pavy] trying to kill  2554
[pavy] waiting for  2554


************** BRUNCH STATS ***************** 
BRUNCH_STAT run 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
	Reading AIG from '/tmp/7194853.1.queue/avy-YV5cuY/beemmcs6f1.pp.aig'
VarMax = 300. FrameMax = 10000. QueMax = 0. TimeMax = 0. MonoCNF = no. SkipGen = no. SolveAll = no.
  1 : 0 0                                                                  0      0.00 sec
  1 : 0 1                                                                  1      0.00 sec
  1 : 0 2                                                                  2      0.00 sec
  1 : 0 3                                                                  3      0.00 sec
  1 : 0 4                                                                  4      0.00 sec
  1 : 0 4                                                                  4      0.00 sec
  2 : 0 4 0                                                                0      0.01 sec
  2 : 0 9 9                                                               10      0.01 sec
  2 : 0 10 11                                                             11      0.01 sec
  2 : 0 14 15                                                             16      0.02 sec
  2 : 0 14 15                                                             16      0.02 sec
  3 : 0 10 9 4                                                             0      0.02 sec
  3 : 0 10 14 19                                                          17      0.03 sec
  3 : 0 10 14 20                                                          17      0.04 sec
  3 : 0 10 14 21                                                          17      0.04 sec
  3 : 0 10 14 22                                                          18      0.04 sec
  3 : 0 10 14 23                                                          19      0.04 sec
  3 : 0 10 14 23                                                          19      0.04 sec
  4 : 0 10 14 19 4                                                         0      0.04 sec
  4 : 0 10 28 59 54                                                       52      0.15 sec
  4 : 0 10 28 59 54                                                       52      0.15 sec
  5 : 0 10 25 43 42 16                                                     0      0.16 sec
  5 : 0 10 28 54 73 70                                                    65      0.29 sec
  5 : 0 10 28 54 73 71                                                    65      0.29 sec
  5 : 0 10 28 54 73 72                                                    65      0.29 sec
  5 : 0 10 28 54 73 72                                                    65      0.29 sec
  6 : 0 10 28 51 59 56 17                                                  0      0.32 sec
  6 : 0 10 29 54 76 111 99                                                89      0.56 sec
  6 : 0 10 29 54 76 112 101                                               89      0.56 sec
  6 : 0 10 29 54 76 112 101                                               89      0.56 sec
  7 : 0 10 28 50 63 75 67 27                                               0      0.60 sec
  7 : 0 10 28 51 71 102 122 122                                          119      0.89 sec
  7 : 0 10 28 51 71 102 122 122                                          119      0.89 sec
  8 : 0 10 28 50 60 70 63 64 48                                            0      0.94 sec
  8 : 0 10 28 50 60 71 66 93 118                                          98      1.12 sec
  8 : 0 10 28 50 60 71 66 94 120                                          98      1.12 sec
  8 : 0 10 28 50 60 71 66 94 120                                          98      1.12 sec
  9 : 0 10 28 50 60 65 44 45 61 63                                         0      1.17 sec
  9 : 0 10 28 50 60 65 44 46 67 92                                        74      1.22 sec
  9 : 0 10 28 50 60 65 44 46 68 94                                        74      1.22 sec
  9 : 0 10 28 50 60 65 44 46 68 94                                        74      1.22 sec
 10 : 0 10 28 50 60 65 44 43 47 39 60                                      0      1.27 sec
 10 : 0 10 28 50 60 65 44 43 47 39 60                                      0      1.27 sec
 11 : 0 10 28 50 60 65 44 43 45 39 26 34                                   0      1.32 sec
 11 : 0 10 28 50 60 65 44 43 48 47 52 61                                  32      1.43 sec
 11 : 0 10 28 50 60 65 44 43 48 47 53 63                                  32      1.44 sec
 11 : 0 10 28 50 60 65 44 43 49 49 64 73                                  40      1.48 sec
 11 : 0 10 28 50 60 65 44 43 50 52 68 78                                  46      1.50 sec
 11 : 0 10 28 50 60 65 44 43 50 52 69 80                                  46      1.50 sec
 11 : 0 10 28 50 60 65 44 43 50 52 73 85                                  51      1.52 sec
 11 : 0 10 28 50 60 65 44 43 50 52 74 87                                  53      1.52 sec
 11 : 0 10 28 50 60 65 44 43 50 52 75 89                                  55      1.52 sec
 11 : 0 10 28 50 60 65 44 43 50 52 75 89                                  55      1.52 sec
 12 : 0 10 28 50 60 65 44 43 40 27 33 52 52                                0      1.58 sec
 12 : 0 10 28 50 60 65 44 43 40 29 39 82 112                              60      1.75 sec
 12 : 0 10 28 50 60 65 44 43 40 29 39 82 114                              62      1.75 sec
 12 : 0 10 28 50 60 65 44 43 40 29 39 82 114                              62      1.75 sec
 13 : 0 10 28 50 60 65 44 42 40 23 2 0 0 117                               0      1.80 sec
Invariant F[11] : 117 clauses with 76 flops (out of 85)
Verification of invariant with 117 clauses was successful.  Time =     0.01 sec
Block =   33  Oblig =  1843  Clause =   972  Call = 20749 (sat=55.2%)  Start =  64
SAT solving =     1.51 sec ( 83.27 %)
  unsat     =     0.29 sec ( 15.81 %)
  sat       =     1.23 sec ( 67.47 %)
Generalize  =     1.23 sec ( 67.73 %)
Push clause =     0.38 sec ( 20.84 %)
Ternary sim =     0.06 sec (  3.18 %)
Containment =     0.01 sec (  0.40 %)
CNF compute =     0.06 sec (  3.06 %)
TOTAL       =     1.82 sec (100.00 %)
Property proved.  Time =     1.83 sec
Result: false


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 12
BRUNCH_STAT run 1.77
BRUNCH_STAT run.loop 1.77
BRUNCH_STAT Result UNSAT
************** BRUNCH STATS END ***************** 
[pavy] Witness begin
0
b0
.
[pavy] Witness end
WINNER:  abcpdr
BRUNCH_STAT config 1
BRUNCH_STAT config_name abcpdr
BRUNCH_STAT Result UNSAT
[launch.sh] stop:  Sat Sep 19 03:12:49 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 03:12:52 CEST 2015
[launch.sh] done: Sat Sep 19 03:12:52 CEST 2015
