[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/intel059.aig
[launch.sh] host:  atom23 (atom23)
[launch.sh] start: Sat Sep 19 11:35:11 CEST 2015
[launch.sh] jobid: 7195621
[launch.sh] name:  intel059avy
[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/7195621.1.queue/avy-6CZUU3
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/intel059.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/intel059.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/intel059.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7195621.1.queue/avy-6CZUU3/intel059.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/intel059.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7195621.1.queue/avy-6CZUU3/intel059.pp.aig".

[pavy] finished pp, output=/tmp/7195621.1.queue/avy-6CZUU3/intel059.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/7195621.1.queue/avy-6CZUU3/navy_avy0.cex /tmp/7195621.1.queue/avy-6CZUU3/intel059.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7195621.1.queue/avy-6CZUU3/abcpdr_avy1.cex /tmp/7195621.1.queue/avy-6CZUU3/intel059.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/7195621.1.queue/avy-6CZUU3/avyabsmus_avy2.cex /tmp/7195621.1.queue/avy-6CZUU3/intel059.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7195621.1.queue/avy-6CZUU3/fib_avy3.cex /tmp/7195621.1.queue/avy-6CZUU3/intel059.pp.aig
[pavy] running: [8798, 8799, 8800, 8801]
[pavy] finished pid 8799 with code 0 and signal 0
[pavy] trying to kill  8798
[pavy] waiting for  8798
[pavy] trying to kill  8800
[pavy] waiting for  8800
[pavy] trying to kill  8801
[pavy] waiting for  8801


************** BRUNCH STATS ***************** 
BRUNCH_STAT run 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
	Reading AIG from '/tmp/7195621.1.queue/avy-6CZUU3/intel059.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 20 29                                                             30      0.05 sec
  2 : 0 20 29                                                             30      0.05 sec
  3 : 0 14 26 3                                                            0      0.06 sec
  3 : 0 14 45 31                                                          31      0.11 sec
  3 : 0 14 45 31                                                          31      0.11 sec
  4 : 0 12 40 14 21                                                        0      0.12 sec
  4 : 0 16 68 125 203                                                    185      0.58 sec
  4 : 0 16 68 125 203                                                    185      0.58 sec
  5 : 0 10 46 74 111 64                                                    0      0.63 sec
  5 : 0 10 46 80 147 126                                                 187      0.78 sec
  5 : 0 10 46 80 147 126                                                 187      0.78 sec
  6 : 0 10 44 65 125 55 78                                                 0      0.84 sec
  6 : 0 10 44 66 168 345 484                                             407      2.12 sec
  6 : 0 10 44 66 168 345 484                                             407      2.12 sec
  7 : 0 10 40 44 90 122 213 187                                            0      2.26 sec
  7 : 0 10 40 44 90 122 213 187                                            0      2.26 sec
  8 : 0 10 40 44 90 121 204 54 133                                         0      2.38 sec
  8 : 0 10 40 44 91 124 249 291 416                                      407      3.48 sec
  8 : 0 10 40 44 91 124 249 291 416                                      407      3.48 sec
  9 : 0 10 40 40 72 56 71 170 154 256                                      0      3.63 sec
  9 : 0 10 40 41 75 61 77 204 248 402                                    292      4.23 sec
  9 : 0 10 40 41 75 61 77 204 248 402                                    292      4.23 sec
 10 : 0 10 40 38 72 54 66 125 112 113 205                                  0      4.38 sec
 10 : 0 10 40 38 72 54 66 125 112 113 205                                  0      4.38 sec
 11 : 0 10 40 38 72 54 66 125 105 113 37 167                               0      4.52 sec
 11 : 0 10 40 38 72 54 66 125 105 120 78 222                             147      4.71 sec
 11 : 0 10 40 38 72 54 66 125 105 120 78 222                             147      4.71 sec
 12 : 0 10 40 38 69 54 63 127 82 91 71 67 155                              0      4.86 sec
 12 : 0 10 40 38 69 54 63 127 82 94 90 161 295                           141      5.32 sec
 12 : 0 10 40 38 69 54 63 127 82 94 90 161 295                           141      5.32 sec
 13 : 0 10 40 38 69 54 63 127 77 77 40 83 43 207                           0      5.47 sec
 13 : 0 10 40 38 69 54 63 127 77 77 41 94 95 285                         142      5.73 sec
 13 : 0 10 40 38 69 54 63 127 77 77 41 94 95 285                         142      5.73 sec
 14 : 0 10 40 38 69 54 63 127 77 69 25 19 29 37 257                        0      5.87 sec
 14 : 0 10 40 38 69 54 63 127 77 69 25 19 29 37 257                        0      5.87 sec
 15 : 0 10 40 38 69 54 63 127 77 69 25 19 28 37 42 215                     0      6.02 sec
 15 : 0 10 40 38 69 54 63 127 77 69 25 19 28 37 42 215                     0      6.02 sec
 16 : 0 10 40 38 69 54 63 127 77 69 25 19 28 37 42 9 206                   0      6.15 sec
 16 : 0 10 40 38 69 54 63 127 77 69 25 19 31 47 76 34 262                 79      6.39 sec
 16 : 0 10 40 38 69 54 63 127 77 69 25 19 31 47 76 34 262                 79      6.39 sec
 17 : 0 10 40 38 69 54 63 125 79 68 23 17 7 6 1 0 0 312                    0      6.52 sec
Invariant F[15] : 312 clauses with 128 flops (out of 140)
Verification of invariant with 312 clauses was successful.  Time =     0.01 sec
Block =   12  Oblig =  5848  Clause =  2752  Call = 38311 (sat=62.8%)  Start = 120
SAT solving =     5.05 sec ( 77.19 %)
  unsat     =     0.54 sec (  8.28 %)
  sat       =     4.51 sec ( 68.92 %)
Generalize  =     3.88 sec ( 59.38 %)
Push clause =     1.68 sec ( 25.62 %)
Ternary sim =     0.54 sec (  8.24 %)
Containment =     0.11 sec (  1.69 %)
CNF compute =     0.17 sec (  2.57 %)
TOTAL       =     6.54 sec (100.00 %)
Property proved.  Time =     6.56 sec
Result: false


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 16
BRUNCH_STAT run 6.45
BRUNCH_STAT run.loop 6.45
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 11:35:21 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 11:35:24 CEST 2015
[launch.sh] done: Sat Sep 19 11:35:24 CEST 2015
