[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/beemcycschd3b1.aig
[launch.sh] host:  atom06 (atom06)
[launch.sh] start: Sat Sep 19 16:51:19 CEST 2015
[launch.sh] jobid: 7195957
[launch.sh] name:  beemcycschd3b1avy
[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/7195957.1.queue/avy-MILSTj
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/beemcycschd3b1.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/beemcycschd3b1.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/beemcycschd3b1.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/beemcycschd3b1.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.pp.aig".

[pavy] finished pp, output=/tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.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/7195957.1.queue/avy-MILSTj/navy_avy0.cex /tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7195957.1.queue/avy-MILSTj/abcpdr_avy1.cex /tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.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/7195957.1.queue/avy-MILSTj/avyabsmus_avy2.cex /tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7195957.1.queue/avy-MILSTj/fib_avy3.cex /tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.pp.aig
[pavy] running: [6285, 6286, 6287, 6288]
[pavy] finished pid 6286 with code 0 and signal 0
[pavy] trying to kill  6285
[pavy] waiting for  6285
[pavy] trying to kill  6287
[pavy] waiting for  6287
[pavy] trying to kill  6288
[pavy] waiting for  6288


************** BRUNCH STATS ***************** 
BRUNCH_STAT run 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
	Reading AIG from '/tmp/7195957.1.queue/avy-MILSTj/beemcycschd3b1.pp.aig'
VarMax = 300. FrameMax = 10000. QueMax = 0. TimeMax = 0. MonoCNF = no. SkipGen = no. SolveAll = no.
  1 : 0 0                                                                  0      0.01 sec
  1 : 0 1                                                                  1      0.01 sec
  1 : 0 1                                                                  1      0.01 sec
  2 : 0 1 0                                                                0      0.01 sec
  2 : 0 1 1                                                                2      0.01 sec
  2 : 0 1 1                                                                2      0.01 sec
  3 : 0 1 1 0                                                              0      0.02 sec
  3 : 0 1 2 2                                                              3      0.02 sec
  3 : 0 1 2 2                                                              3      0.02 sec
  4 : 0 1 2 2 0                                                            0      0.02 sec
  4 : 0 1 2 3 3                                                            4      0.03 sec
  4 : 0 1 2 3 3                                                            4      0.03 sec
  5 : 0 1 2 3 3 0                                                          0      0.03 sec
  5 : 0 1 2 3 3 3                                                          4      0.04 sec
  5 : 0 1 2 3 3 3                                                          4      0.04 sec
  6 : 0 1 2 3 3 3 0                                                        0      0.05 sec
  6 : 0 1 2 3 3 3 3                                                        4      0.05 sec
  6 : 0 1 2 3 3 3 3                                                        4      0.05 sec
  7 : 0 1 2 3 3 3 3 0                                                      0      0.06 sec
  7 : 0 1 2 3 3 3 3 3                                                      4      0.07 sec
  7 : 0 1 2 3 3 3 3 3                                                      4      0.07 sec
  8 : 0 1 2 3 3 3 3 3 0                                                    0      0.07 sec
  8 : 0 1 2 3 3 3 3 3 3                                                    4      0.08 sec
  8 : 0 1 2 3 3 3 3 3 3                                                    4      0.08 sec
  9 : 0 1 2 3 3 3 3 3 3 0                                                  0      0.09 sec
  9 : 0 1 2 3 3 3 3 3 3 3                                                  4      0.10 sec
  9 : 0 1 2 3 3 3 3 3 3 3                                                  4      0.10 sec
 10 : 0 1 2 3 3 3 3 3 3 3 0                                                0      0.11 sec
 10 : 0 1 2 3 3 3 3 3 3 3 3                                                4      0.12 sec
 10 : 0 1 2 3 3 3 3 3 3 3 3                                                4      0.12 sec
 11 : 0 1 2 3 3 3 3 3 3 3 3 0                                              0      0.13 sec
 11 : 0 1 2 3 3 3 3 3 3 3 3 3                                              4      0.14 sec
 11 : 0 1 2 3 3 3 3 3 3 3 3 3                                              4      0.14 sec
 12 : 0 1 2 3 3 3 3 3 3 3 3 3 0                                            0      0.15 sec
 12 : 0 1 2 3 3 3 3 3 3 3 3 3 3                                            4      0.16 sec
 12 : 0 1 2 3 3 3 3 3 3 3 3 3 3                                            4      0.16 sec
 13 : 0 1 2 3 3 3 3 3 3 3 3 3 3 0                                          0      0.17 sec
 13 : 0 1 2 3 3 3 3 3 3 3 3 3 3 3                                          4      0.18 sec
 13 : 0 1 2 3 3 3 3 3 3 3 3 3 3 3                                          4      0.18 sec
 14 : 0 1 2 3 3 3 3 3 3 3 3 3 3 3 0                                        0      0.19 sec
 14 : 0 1 3 5 6 5 5 5 5 5 5 5 5 5 4                                       18      0.26 sec
 14 : 0 1 3 5 6 5 5 5 5 5 5 5 5 5 4                                       18      0.26 sec
 15 : 0 1 2 1 1 1 1 1 1 1 1 1 1 1 0 4                                      0      0.27 sec
Invariant F[14] : 4 clauses with 9 flops (out of 301)
Verification of invariant with 4 clauses was successful.  Time =     0.00 sec
Block =   14  Oblig =   110  Clause =    64  Call =   996 (sat=76.1%)  Start =   0
SAT solving =     0.19 sec ( 68.00 %)
  unsat     =     0.02 sec (  6.17 %)
  sat       =     0.17 sec ( 61.83 %)
Generalize  =     0.13 sec ( 46.19 %)
Push clause =     0.09 sec ( 30.73 %)
Ternary sim =     0.01 sec (  3.99 %)
Containment =     0.00 sec (  0.07 %)
CNF compute =     0.02 sec (  8.11 %)
TOTAL       =     0.28 sec (100.00 %)
Property proved.  Time =     0.30 sec
Result: false


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 14
BRUNCH_STAT run 0.28
BRUNCH_STAT run.loop 0.28
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 16:51:23 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 16:51:26 CEST 2015
[launch.sh] done: Sat Sep 19 16:51:26 CEST 2015
