c launch: /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=0/benchmarks /data/starexec/2015-06-01/BV/wintersteiger/fmsd13/ /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=0 --time-limit=1200 --space-limit=7000 /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=0/boolector -v --ef:synth=0
c host: atom25
c benchmark: /data/starexec/2015-06-01/BV/wintersteiger/fmsd13/fixpoint/sdlx-fixpoint-8.smt2
c solver: /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=0/boolector
c solver options: -v --ef:synth=0
[btor>main] Boolector Version 2.999 4f7837876cf9c28f42649b368eaffaf03c7e1357
[btor>main] -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_PICOSAT -DBTOR_USE_LINGELING -DBTOR_USE_MINISAT
[btor>main] released Sat Oct 15 13:25:35 CEST 2016
[btor>main] compiled Sat Oct 15 13:25:35 CEST 2016
[btor>main] gcc (Ubuntu 4.8.4-2ubuntu1~14.04.3) 4.8.4
[btor>main] setting signal handlers
[btor>main] no time limit given
[btor>parse] parsing '/data/starexec/2015-06-01/BV/wintersteiger/fmsd13/fixpoint/sdlx-fixpoint-8.smt2'
[btor>smt2] parsed 6 commands in 0.06 seconds
[btor>slvef] enabled ef engine
[btor>skel] found 1 skeleton literals in 1 constraints
[btor>skel] skeleton preprocessing result 0
[btor>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[btor>core] 1 rewriting rounds in 0.0 seconds
[btor>core] simplification returned 0
[forall>slvfun] enabled core engine
[exists>slvfun] enabled core engine
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>sat] Lingeling allows both incremental and non-incremental mode
[forall>sat] initialized Lingeling
[lingeling] Lingeling
[lingeling] 
[lingeling] Version bbc 923038088b727dcc8bd03aa8dfb5013bd03bf8c4
[lingeling] 
[lingeling] Copyright (C) 2010-2016 Armin Biere JKU Linz Austria.
[lingeling] All rights reserved.
[lingeling] 
[lingeling] released Sat May 28 15:42:42 CEST 2016
[lingeling] compiled Sat May 28 15:42:42 CEST 2016
[lingeling] 
[lingeling] gcc (Ubuntu 4.8.4-2ubuntu1~14.04) 4.8.4
[lingeling] -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
[lingeling] -DNLGLFILES -DNLGLDEMA
[lingeling] Linux cluster2 3.13.0-63-generic x86_64
[lingeling] 
[forall>slvfun] 1192 AIG vars, 14508 AIG ands, 13537 CNF vars, 38293 CNF clauses
[forall>slvfun] SAT call 1 returned 10 in 0.246 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 3883 skeleton literals in 221 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 28 new constraints in 0.0 seconds
[exists>core] replaced 20 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.0 seconds
[exists>core] simplification returned 0
[exists>sat] Lingeling allows both incremental and non-incremental mode
[exists>sat] initialized Lingeling
[lingeling] Lingeling
[lingeling] 
[lingeling] Version bbc 923038088b727dcc8bd03aa8dfb5013bd03bf8c4
[lingeling] 
[lingeling] Copyright (C) 2010-2016 Armin Biere JKU Linz Austria.
[lingeling] All rights reserved.
[lingeling] 
[lingeling] released Sat May 28 15:42:42 CEST 2016
[lingeling] compiled Sat May 28 15:42:42 CEST 2016
[lingeling] 
[lingeling] gcc (Ubuntu 4.8.4-2ubuntu1~14.04) 4.8.4
[lingeling] -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
[lingeling] -DNLGLFILES -DNLGLDEMA
[lingeling] Linux cluster2 3.13.0-63-generic x86_64
[lingeling] 
[exists>slvfun] 559 AIG vars, 5089 AIG ands, 5028 CNF vars, 13794 CNF clauses
[exists>slvfun] SAT call 1 returned 10 in 0.106 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 7 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 7 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 7606 AIG ands, 14237 CNF vars, 40399 CNF clauses
[forall>slvfun] SAT call 2 returned 10 in 0.012 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 7340 skeleton literals in 462 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 902 new constraints in 0.2 seconds
[exists>core] replaced 70 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 1118 AIG vars, 8364 AIG ands, 10236 CNF vars, 28158 CNF clauses
[exists>slvfun] SAT call 2 returned 10 in 0.364 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 16 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 16 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9062 AIG ands, 16289 CNF vars, 46590 CNF clauses
[forall>slvfun] SAT call 3 returned 10 in 0.025 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 9567 skeleton literals in 716 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1541 new constraints in 0.2 seconds
[exists>core] replaced 103 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 1677 AIG vars, 10288 AIG ands, 15627 CNF vars, 43117 CNF clauses
[exists>slvfun] SAT call 3 returned 10 in 0.403 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 20 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 20 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9009 AIG ands, 18259 CNF vars, 52559 CNF clauses
[forall>slvfun] SAT call 4 returned 10 in 0.031 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 10825 skeleton literals in 983 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 965 new constraints in 0.3 seconds
[exists>core] replaced 63 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 2236 AIG vars, 14033 AIG ands, 20951 CNF vars, 57855 CNF clauses
[exists>slvfun] SAT call 4 returned 10 in 0.365 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 23 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 23 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 8994 AIG ands, 20178 CNF vars, 58404 CNF clauses
[forall>slvfun] SAT call 5 returned 10 in 0.034 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 13352 skeleton literals in 1241 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1278 new constraints in 0.3 seconds
[exists>core] replaced 70 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 2795 AIG vars, 17299 AIG ands, 26192 CNF vars, 72329 CNF clauses
[exists>slvfun] SAT call 5 returned 10 in 0.603 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 24 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 24 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9714 AIG ands, 22795 CNF vars, 66353 CNF clauses
[forall>slvfun] SAT call 6 returned 10 in 0.035 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 15525 skeleton literals in 1495 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3078 new constraints in 0.3 seconds
[exists>core] replaced 199 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 3354 AIG vars, 16253 AIG ands, 32433 CNF vars, 90016 CNF clauses
[exists>slvfun] SAT call 6 returned 10 in 0.467 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 26 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 26 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9748 AIG ands, 25453 CNF vars, 74426 CNF clauses
[forall>slvfun] SAT call 7 returned 10 in 0.040 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 14406 skeleton literals in 1802 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1579 new constraints in 0.3 seconds
[exists>core] replaced 68 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.4 seconds
[exists>core] simplification returned 0
[exists>slvfun] 3913 AIG vars, 19549 AIG ands, 37661 CNF vars, 104450 CNF clauses
[exists>slvfun] SAT call 7 returned 10 in 0.527 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 26 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 26 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9843 AIG ands, 28216 CNF vars, 82820 CNF clauses
[forall>slvfun] SAT call 8 returned 10 in 0.672 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 16607 skeleton literals in 2055 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1673 new constraints in 0.4 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.4 seconds
[exists>core] simplification returned 0
[exists>slvfun] 4472 AIG vars, 22845 AIG ands, 42889 CNF vars, 118884 CNF clauses
[exists>slvfun] SAT call 8 returned 10 in 0.876 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 29 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 29 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9696 AIG ands, 30806 CNF vars, 90703 CNF clauses
[forall>slvfun] SAT call 9 returned 10 in 0.036 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 18807 skeleton literals in 2308 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1830 new constraints in 0.5 seconds
[exists>core] replaced 87 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.5 seconds
[exists>core] simplification returned 0
[exists>slvfun] 5031 AIG vars, 26089 AIG ands, 48125 CNF vars, 133346 CNF clauses
[exists>slvfun] SAT call 9 returned 10 in 0.721 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 32 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 32 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9821 AIG ands, 33530 CNF vars, 98992 CNF clauses
[forall>slvfun] SAT call 10 returned 10 in 0.039 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 20956 skeleton literals in 2569 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1874 new constraints in 0.5 seconds
[exists>core] replaced 68 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.5 seconds
[exists>core] simplification returned 0
[exists>slvfun] 5590 AIG vars, 29385 AIG ands, 53353 CNF vars, 147780 CNF clauses
[exists>slvfun] SAT call 10 returned 10 in 0.817 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 32 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 32 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 9899 AIG ands, 36322 CNF vars, 107490 CNF clauses
[forall>slvfun] SAT call 11 returned 10 in 0.041 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 23157 skeleton literals in 2822 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1968 new constraints in 0.6 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 6149 AIG vars, 32678 AIG ands, 58580 CNF vars, 162210 CNF clauses
[exists>slvfun] SAT call 11 returned 10 in 0.903 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 32 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 32 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 10256 AIG ands, 39475 CNF vars, 117069 CNF clauses
[forall>slvfun] SAT call 12 returned 10 in 0.290 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 25357 skeleton literals in 3075 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2062 new constraints in 0.6 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.7 seconds
[exists>core] simplification returned 0
[exists>slvfun] 6708 AIG vars, 35974 AIG ands, 63808 CNF vars, 176644 CNF clauses
[exists>slvfun] SAT call 12 returned 10 in 1.280 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 35 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 35 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 10440 AIG ands, 42791 CNF vars, 127148 CNF clauses
[forall>slvfun] SAT call 13 returned 10 in 0.047 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 27557 skeleton literals in 3328 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2354 new constraints in 0.7 seconds
[exists>core] replaced 88 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.7 seconds
[exists>core] simplification returned 0
[exists>slvfun] 7267 AIG vars, 38636 AIG ands, 69407 CNF vars, 192258 CNF clauses
[exists>slvfun] SAT call 13 returned 10 in 1.058 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 35 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 35 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 10602 AIG ands, 46289 CNF vars, 137775 CNF clauses
[forall>slvfun] SAT call 14 returned 10 in 0.049 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 29293 skeleton literals in 3594 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2273 new constraints in 0.8 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 7826 AIG vars, 41928 AIG ands, 74635 CNF vars, 206692 CNF clauses
[exists>slvfun] SAT call 14 returned 10 in 1.155 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 35 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 35 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 10689 AIG ands, 49890 CNF vars, 148707 CNF clauses
[forall>slvfun] SAT call 15 returned 10 in 0.052 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 31490 skeleton literals in 3847 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2363 new constraints in 0.8 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 8385 AIG vars, 45224 AIG ands, 79863 CNF vars, 221126 CNF clauses
[exists>slvfun] SAT call 15 returned 10 in 1.227 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 35 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 35 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11073 AIG ands, 53881 CNF vars, 160806 CNF clauses
[forall>slvfun] SAT call 16 returned 10 in 0.551 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 33690 skeleton literals in 4100 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2457 new constraints in 0.9 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 8944 AIG vars, 48520 AIG ands, 85091 CNF vars, 235560 CNF clauses
[exists>slvfun] SAT call 16 returned 10 in 1.337 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 35 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 35 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11158 AIG ands, 57949 CNF vars, 173140 CNF clauses
[forall>slvfun] SAT call 17 returned 10 in 0.052 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 35890 skeleton literals in 4353 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2567 new constraints in 0.9 seconds
[exists>core] replaced 71 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 9503 AIG vars, 51787 AIG ands, 90335 CNF vars, 250042 CNF clauses
[exists>slvfun] SAT call 17 returned 10 in 1.524 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 35 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 35 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11236 AIG ands, 62110 CNF vars, 185751 CNF clauses
[forall>slvfun] SAT call 18 returned 10 in 0.055 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 38067 skeleton literals in 4607 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2647 new constraints in 1.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.0 seconds
[exists>core] simplification returned 0
[exists>slvfun] 10062 AIG vars, 55083 AIG ands, 95563 CNF vars, 264476 CNF clauses
[exists>slvfun] SAT call 18 returned 10 in 1.607 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 35 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 35 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11304 AIG ands, 66355 CNF vars, 198614 CNF clauses
[forall>slvfun] SAT call 19 returned 10 in 0.582 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 40267 skeleton literals in 4860 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 2741 new constraints in 1.1 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.1 seconds
[exists>core] simplification returned 0
[exists>slvfun] 10621 AIG vars, 58379 AIG ands, 100791 CNF vars, 278910 CNF clauses
[exists>slvfun] SAT call 19 returned 10 in 2.086 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 36 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 36 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11098 AIG ands, 70415 CNF vars, 210921 CNF clauses
[forall>slvfun] SAT call 20 returned 10 in 0.056 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 42467 skeleton literals in 5113 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6509 new constraints in 0.9 seconds
[exists>core] replaced 325 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 11180 AIG vars, 50322 AIG ands, 110609 CNF vars, 308000 CNF clauses
[exists>slvfun] SAT call 20 returned 10 in 1.515 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11176 AIG ands, 74537 CNF vars, 223413 CNF clauses
[forall>slvfun] SAT call 21 returned 10 in 0.058 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 35715 skeleton literals in 5460 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3189 new constraints in 0.9 seconds
[exists>core] replaced 70 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 11739 AIG vars, 53609 AIG ands, 115844 CNF vars, 322455 CNF clauses
[exists>slvfun] SAT call 21 returned 10 in 1.505 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11543 AIG ands, 79050 CNF vars, 237076 CNF clauses
[forall>slvfun] SAT call 22 returned 10 in 0.740 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 37909 skeleton literals in 5714 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3285 new constraints in 0.9 seconds
[exists>core] replaced 71 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 0.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 12298 AIG vars, 56896 AIG ands, 121079 CNF vars, 336910 CNF clauses
[exists>slvfun] SAT call 22 returned 10 in 1.547 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11898 AIG ands, 83941 CNF vars, 251872 CNF clauses
[forall>slvfun] SAT call 23 returned 10 in 0.063 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 40102 skeleton literals in 5968 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3374 new constraints in 1.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.0 seconds
[exists>core] simplification returned 0
[exists>slvfun] 12857 AIG vars, 60192 AIG ands, 126307 CNF vars, 351344 CNF clauses
[exists>slvfun] SAT call 23 returned 10 in 1.656 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 11984 AIG ands, 88907 CNF vars, 266891 CNF clauses
[forall>slvfun] SAT call 24 returned 10 in 0.065 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 42302 skeleton literals in 6221 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3468 new constraints in 1.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.0 seconds
[exists>core] simplification returned 0
[exists>slvfun] 13416 AIG vars, 63488 AIG ands, 131535 CNF vars, 365778 CNF clauses
[exists>slvfun] SAT call 24 returned 10 in 1.726 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12066 AIG ands, 93941 CNF vars, 282118 CNF clauses
[forall>slvfun] SAT call 25 returned 10 in 1.659 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 44502 skeleton literals in 6474 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3593 new constraints in 1.1 seconds
[exists>core] replaced 73 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.1 seconds
[exists>core] simplification returned 0
[exists>slvfun] 13975 AIG vars, 66733 AIG ands, 136783 CNF vars, 380271 CNF clauses
[exists>slvfun] SAT call 25 returned 10 in 1.820 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12147 AIG ands, 99086 CNF vars, 297674 CNF clauses
[forall>slvfun] SAT call 26 returned 10 in 0.067 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 46660 skeleton literals in 6728 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3660 new constraints in 1.2 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 14534 AIG vars, 70029 AIG ands, 142011 CNF vars, 394705 CNF clauses
[exists>slvfun] SAT call 26 returned 10 in 1.958 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12225 AIG ands, 104301 CNF vars, 313444 CNF clauses
[forall>slvfun] SAT call 27 returned 10 in 0.070 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 48860 skeleton literals in 6981 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3754 new constraints in 1.2 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 15093 AIG vars, 73322 AIG ands, 147238 CNF vars, 409135 CNF clauses
[exists>slvfun] SAT call 27 returned 10 in 2.029 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 37 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 37 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12302 AIG ands, 109597 CNF vars, 329455 CNF clauses
[forall>slvfun] SAT call 28 returned 10 in 0.559 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 51060 skeleton literals in 7234 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 3848 new constraints in 1.3 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 15652 AIG vars, 76618 AIG ands, 152466 CNF vars, 423569 CNF clauses
[exists>slvfun] SAT call 28 returned 10 in 2.882 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 39 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 39 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12404 AIG ands, 115020 CNF vars, 345844 CNF clauses
[forall>slvfun] SAT call 29 returned 10 in 0.076 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 53260 skeleton literals in 7487 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4030 new constraints in 1.3 seconds
[exists>core] replaced 83 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 16211 AIG vars, 79591 AIG ands, 157804 CNF vars, 438357 CNF clauses
[exists>slvfun] SAT call 29 returned 10 in 2.223 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12245 AIG ands, 120262 CNF vars, 361696 CNF clauses
[forall>slvfun] SAT call 30 returned 10 in 0.074 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 55225 skeleton literals in 7743 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4048 new constraints in 1.4 seconds
[exists>core] replaced 68 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.5 seconds
[exists>core] simplification returned 0
[exists>slvfun] 16770 AIG vars, 82887 AIG ands, 163032 CNF vars, 452791 CNF clauses
[exists>slvfun] SAT call 30 returned 10 in 2.357 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12354 AIG ands, 125632 CNF vars, 377929 CNF clauses
[forall>slvfun] SAT call 31 returned 10 in 0.787 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 57426 skeleton literals in 7996 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4142 new constraints in 1.5 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.5 seconds
[exists>core] simplification returned 0
[exists>slvfun] 17329 AIG vars, 86183 AIG ands, 168260 CNF vars, 467225 CNF clauses
[exists>slvfun] SAT call 31 returned 10 in 2.422 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12441 AIG ands, 131081 CNF vars, 394403 CNF clauses
[forall>slvfun] SAT call 32 returned 10 in 0.078 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 59626 skeleton literals in 8249 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4236 new constraints in 1.5 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 17888 AIG vars, 89476 AIG ands, 173487 CNF vars, 481655 CNF clauses
[exists>slvfun] SAT call 32 returned 10 in 2.546 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12533 AIG ands, 136650 CNF vars, 411233 CNF clauses
[forall>slvfun] SAT call 33 returned 10 in 0.080 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 61826 skeleton literals in 8502 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4330 new constraints in 1.6 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 18447 AIG vars, 92772 AIG ands, 178715 CNF vars, 496089 CNF clauses
[exists>slvfun] SAT call 33 returned 10 in 2.839 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12614 AIG ands, 142292 CNF vars, 428286 CNF clauses
[forall>slvfun] SAT call 34 returned 10 in 1.078 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 64026 skeleton literals in 8755 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4424 new constraints in 1.7 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.7 seconds
[exists>core] simplification returned 0
[exists>slvfun] 19006 AIG vars, 96065 AIG ands, 183942 CNF vars, 510519 CNF clauses
[exists>slvfun] SAT call 34 returned 10 in 2.918 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12703 AIG ands, 148027 CNF vars, 445616 CNF clauses
[forall>slvfun] SAT call 35 returned 10 in 0.082 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 66226 skeleton literals in 9008 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4525 new constraints in 1.8 seconds
[exists>core] replaced 71 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 19565 AIG vars, 99352 AIG ands, 189177 CNF vars, 524974 CNF clauses
[exists>slvfun] SAT call 35 returned 10 in 3.065 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12779 AIG ands, 153852 CNF vars, 463216 CNF clauses
[forall>slvfun] SAT call 36 returned 10 in 0.792 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 68419 skeleton literals in 9262 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4614 new constraints in 1.8 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 20124 AIG vars, 102648 AIG ands, 194405 CNF vars, 539408 CNF clauses
[exists>slvfun] SAT call 36 returned 10 in 3.125 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12848 AIG ands, 159764 CNF vars, 481077 CNF clauses
[forall>slvfun] SAT call 37 returned 10 in 0.088 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 70619 skeleton literals in 9515 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4708 new constraints in 1.9 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 1.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 20683 AIG vars, 105944 AIG ands, 199633 CNF vars, 553842 CNF clauses
[exists>slvfun] SAT call 37 returned 10 in 3.245 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 12933 AIG ands, 165751 CNF vars, 499163 CNF clauses
[forall>slvfun] SAT call 38 returned 10 in 0.572 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 72819 skeleton literals in 9768 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4802 new constraints in 2.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.0 seconds
[exists>core] simplification returned 0
[exists>slvfun] 21242 AIG vars, 109240 AIG ands, 204861 CNF vars, 568276 CNF clauses
[exists>slvfun] SAT call 38 returned 10 in 3.299 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 13013 AIG ands, 171825 CNF vars, 517510 CNF clauses
[forall>slvfun] SAT call 39 returned 10 in 0.089 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 75019 skeleton literals in 10021 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4896 new constraints in 2.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.0 seconds
[exists>core] simplification returned 0
[exists>slvfun] 21801 AIG vars, 112536 AIG ands, 210089 CNF vars, 582710 CNF clauses
[exists>slvfun] SAT call 39 returned 10 in 3.366 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 13091 AIG ands, 177953 CNF vars, 536019 CNF clauses
[forall>slvfun] SAT call 40 returned 10 in 0.090 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 77219 skeleton literals in 10274 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 4990 new constraints in 2.1 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.1 seconds
[exists>core] simplification returned 0
[exists>slvfun] 22360 AIG vars, 115832 AIG ands, 215317 CNF vars, 597144 CNF clauses
[exists>slvfun] SAT call 40 returned 10 in 3.466 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 13163 AIG ands, 184175 CNF vars, 554808 CNF clauses
[forall>slvfun] SAT call 41 returned 10 in 1.173 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 79419 skeleton literals in 10527 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5084 new constraints in 2.2 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 22919 AIG vars, 119128 AIG ands, 220545 CNF vars, 611578 CNF clauses
[exists>slvfun] SAT call 41 returned 10 in 3.612 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 13388 AIG ands, 190632 CNF vars, 574306 CNF clauses
[forall>slvfun] SAT call 42 returned 10 in 0.102 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 81619 skeleton literals in 10780 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5178 new constraints in 2.3 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 23478 AIG vars, 122421 AIG ands, 225772 CNF vars, 626008 CNF clauses
[exists>slvfun] SAT call 42 returned 10 in 4.656 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 13669 AIG ands, 197382 CNF vars, 594677 CNF clauses
[forall>slvfun] SAT call 43 returned 10 in 0.882 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 83819 skeleton literals in 11033 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5516 new constraints in 2.3 seconds
[exists>core] replaced 100 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 24037 AIG vars, 125154 AIG ands, 231253 CNF vars, 641245 CNF clauses
[exists>slvfun] SAT call 43 returned 10 in 3.784 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 13981 AIG ands, 204456 CNF vars, 616026 CNF clauses
[forall>slvfun] SAT call 44 returned 10 in 0.122 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 85561 skeleton literals in 11305 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5396 new constraints in 2.3 seconds
[exists>core] replaced 68 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 24596 AIG vars, 128447 AIG ands, 236480 CNF vars, 655675 CNF clauses
[exists>slvfun] SAT call 44 returned 10 in 3.754 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 14298 AIG ands, 211851 CNF vars, 638336 CNF clauses
[forall>slvfun] SAT call 45 returned 10 in 0.957 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 87762 skeleton literals in 11558 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5490 new constraints in 2.4 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.4 seconds
[exists>core] simplification returned 0
[exists>slvfun] 25155 AIG vars, 131743 AIG ands, 241708 CNF vars, 670109 CNF clauses
[exists>slvfun] SAT call 45 returned 10 in 3.915 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 14525 AIG ands, 219497 CNF vars, 661399 CNF clauses
[forall>slvfun] SAT call 46 returned 10 in 0.127 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 89962 skeleton literals in 11811 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5584 new constraints in 2.5 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.5 seconds
[exists>core] simplification returned 0
[exists>slvfun] 25714 AIG vars, 135039 AIG ands, 246936 CNF vars, 684543 CNF clauses
[exists>slvfun] SAT call 46 returned 10 in 3.988 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 14650 AIG ands, 227272 CNF vars, 684847 CNF clauses
[forall>slvfun] SAT call 47 returned 10 in 0.130 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 92162 skeleton literals in 12064 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5678 new constraints in 2.6 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 26273 AIG vars, 138335 AIG ands, 252164 CNF vars, 698977 CNF clauses
[exists>slvfun] SAT call 47 returned 10 in 4.088 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 14856 AIG ands, 235263 CNF vars, 708947 CNF clauses
[forall>slvfun] SAT call 48 returned 10 in 1.255 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 94362 skeleton literals in 12317 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5795 new constraints in 2.7 seconds
[exists>core] replaced 73 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.7 seconds
[exists>core] simplification returned 0
[exists>slvfun] 26832 AIG vars, 141593 AIG ands, 257411 CNF vars, 713468 CNF clauses
[exists>slvfun] SAT call 48 returned 10 in 4.171 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 15069 AIG ands, 243500 CNF vars, 733781 CNF clauses
[forall>slvfun] SAT call 49 returned 10 in 0.138 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 96532 skeleton literals in 12572 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5870 new constraints in 2.7 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.7 seconds
[exists>core] simplification returned 0
[exists>slvfun] 27391 AIG vars, 144889 AIG ands, 262639 CNF vars, 727902 CNF clauses
[exists>slvfun] SAT call 49 returned 10 in 4.297 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 15280 AIG ands, 251927 CNF vars, 759189 CNF clauses
[forall>slvfun] SAT call 50 returned 10 in 1.038 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 98732 skeleton literals in 12825 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 5964 new constraints in 2.8 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 27950 AIG vars, 148182 AIG ands, 267866 CNF vars, 742332 CNF clauses
[exists>slvfun] SAT call 50 returned 10 in 4.352 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 15589 AIG ands, 260697 CNF vars, 785622 CNF clauses
[forall>slvfun] SAT call 51 returned 10 in 0.155 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 100932 skeleton literals in 13078 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6058 new constraints in 2.8 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 28509 AIG vars, 151478 AIG ands, 273094 CNF vars, 756766 CNF clauses
[exists>slvfun] SAT call 51 returned 10 in 4.444 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 15741 AIG ands, 269611 CNF vars, 812491 CNF clauses
[forall>slvfun] SAT call 52 returned 10 in 0.872 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 103132 skeleton literals in 13331 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6152 new constraints in 2.9 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 29068 AIG vars, 154771 AIG ands, 278321 CNF vars, 771196 CNF clauses
[exists>slvfun] SAT call 52 returned 10 in 4.492 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 16077 AIG ands, 278870 CNF vars, 840391 CNF clauses
[forall>slvfun] SAT call 53 returned 10 in 0.168 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 105332 skeleton literals in 13584 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6246 new constraints in 3.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.0 seconds
[exists>core] simplification returned 0
[exists>slvfun] 29627 AIG vars, 158067 AIG ands, 283549 CNF vars, 785630 CNF clauses
[exists>slvfun] SAT call 53 returned 10 in 4.644 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 16398 AIG ands, 288442 CNF vars, 869234 CNF clauses
[forall>slvfun] SAT call 54 returned 10 in 0.178 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 107532 skeleton literals in 13837 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6340 new constraints in 3.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.1 seconds
[exists>core] simplification returned 0
[exists>slvfun] 30186 AIG vars, 161360 AIG ands, 288776 CNF vars, 800060 CNF clauses
[exists>slvfun] SAT call 54 returned 10 in 4.679 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 16745 AIG ands, 298365 CNF vars, 899128 CNF clauses
[forall>slvfun] SAT call 55 returned 10 in 1.894 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 109732 skeleton literals in 14090 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6434 new constraints in 3.1 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 30745 AIG vars, 164656 AIG ands, 294004 CNF vars, 814494 CNF clauses
[exists>slvfun] SAT call 55 returned 10 in 4.793 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 17063 AIG ands, 308605 CNF vars, 929973 CNF clauses
[forall>slvfun] SAT call 56 returned 10 in 0.197 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 111932 skeleton literals in 14343 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6528 new constraints in 3.2 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 31304 AIG vars, 167952 AIG ands, 299232 CNF vars, 828928 CNF clauses
[exists>slvfun] SAT call 56 returned 10 in 4.869 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.1 seconds
[forall>core] 1 rewriting rounds in 0.1 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 17309 AIG ands, 319090 CNF vars, 961553 CNF clauses
[forall>slvfun] SAT call 57 returned 10 in 1.300 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 114132 skeleton literals in 14596 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6622 new constraints in 3.2 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 31863 AIG vars, 171248 AIG ands, 304460 CNF vars, 843362 CNF clauses
[exists>slvfun] SAT call 57 returned 10 in 4.919 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 17608 AIG ands, 329890 CNF vars, 994078 CNF clauses
[forall>slvfun] SAT call 58 returned 10 in 0.272 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 116332 skeleton literals in 14849 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6716 new constraints in 3.3 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 32422 AIG vars, 174544 AIG ands, 309688 CNF vars, 857796 CNF clauses
[exists>slvfun] SAT call 58 returned 10 in 5.026 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 17870 AIG ands, 340969 CNF vars, 1027440 CNF clauses
[forall>slvfun] SAT call 59 returned 10 in 1.605 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 118532 skeleton literals in 15102 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6810 new constraints in 3.4 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.4 seconds
[exists>core] simplification returned 0
[exists>slvfun] 32981 AIG vars, 177840 AIG ands, 314916 CNF vars, 872230 CNF clauses
[exists>slvfun] SAT call 59 returned 10 in 5.080 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 18063 AIG ands, 352262 CNF vars, 1061444 CNF clauses
[forall>slvfun] SAT call 60 returned 10 in 0.236 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 120732 skeleton literals in 15355 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6904 new constraints in 3.4 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.4 seconds
[exists>core] simplification returned 0
[exists>slvfun] 33540 AIG vars, 181136 AIG ands, 320144 CNF vars, 886664 CNF clauses
[exists>slvfun] SAT call 60 returned 10 in 5.166 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 18323 AIG ands, 363834 CNF vars, 1096285 CNF clauses
[forall>slvfun] SAT call 61 returned 10 in 0.245 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 122932 skeleton literals in 15608 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 6998 new constraints in 3.5 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.5 seconds
[exists>core] simplification returned 0
[exists>slvfun] 34099 AIG vars, 184432 AIG ands, 325372 CNF vars, 901098 CNF clauses
[exists>slvfun] SAT call 61 returned 10 in 5.252 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 18616 AIG ands, 375721 CNF vars, 1132071 CNF clauses
[forall>slvfun] SAT call 62 returned 10 in 2.048 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 125132 skeleton literals in 15861 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 7092 new constraints in 3.5 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 34658 AIG vars, 187728 AIG ands, 330600 CNF vars, 915532 CNF clauses
[exists>slvfun] SAT call 62 returned 10 in 5.315 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 18894 AIG ands, 387885 CNF vars, 1168688 CNF clauses
[forall>slvfun] SAT call 63 returned 10 in 0.258 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 127332 skeleton literals in 16114 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 7186 new constraints in 3.6 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 35217 AIG vars, 191024 AIG ands, 335828 CNF vars, 929966 CNF clauses
[exists>slvfun] SAT call 63 returned 10 in 5.403 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 38 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 38 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 18987 AIG ands, 400168 CNF vars, 1205662 CNF clauses
[forall>slvfun] SAT call 64 returned 10 in 1.537 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 129532 skeleton literals in 16367 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 7280 new constraints in 3.7 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.7 seconds
[exists>core] simplification returned 0
[exists>slvfun] 35776 AIG vars, 194320 AIG ands, 341056 CNF vars, 944400 CNF clauses
[exists>slvfun] SAT call 64 returned 10 in 6.866 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 18944 AIG ands, 412394 CNF vars, 1242468 CNF clauses
[forall>slvfun] SAT call 65 returned 10 in 0.338 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 131732 skeleton literals in 16620 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 20310 new constraints in 2.7 seconds
[exists>core] replaced 962 embedded constraints in 0 seconds
[exists>core] replaced 1 embedded constraints in 0 seconds
[exists>core] 3 rewriting rounds in 2.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 36335 AIG vars, 155996 AIG ands, 364490 CNF vars, 1017023 CNF clauses
[exists>slvfun] SAT call 65 returned 10 in 5.060 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 39 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 39 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 19181 AIG ands, 424850 CNF vars, 1279972 CNF clauses
[forall>slvfun] SAT call 66 returned 10 in 0.300 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 101947 skeleton literals in 17212 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 8395 new constraints in 2.5 seconds
[exists>core] replaced 72 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.5 seconds
[exists>core] simplification returned 0
[exists>slvfun] 36894 AIG vars, 159259 AIG ands, 369745 CNF vars, 1031546 CNF clauses
[exists>slvfun] SAT call 66 returned 10 in 4.723 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 39 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 39 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 19409 AIG ands, 437542 CNF vars, 1318180 CNF clauses
[forall>slvfun] SAT call 67 returned 10 in 2.526 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 104120 skeleton literals in 17468 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 8475 new constraints in 2.6 seconds
[exists>core] replaced 70 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 37453 AIG vars, 162551 AIG ands, 374973 CNF vars, 1045980 CNF clauses
[exists>slvfun] SAT call 67 returned 10 in 4.803 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 39 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 39 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 19489 AIG ands, 450308 CNF vars, 1356610 CNF clauses
[forall>slvfun] SAT call 68 returned 10 in 0.288 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 106316 skeleton literals in 17721 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 8590 new constraints in 2.6 seconds
[exists>core] replaced 77 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.6 seconds
[exists>core] simplification returned 0
[exists>slvfun] 38012 AIG vars, 165814 AIG ands, 380203 CNF vars, 1060420 CNF clauses
[exists>slvfun] SAT call 68 returned 10 in 4.832 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 39 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 39 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 19575 AIG ands, 463159 CNF vars, 1395295 CNF clauses
[forall>slvfun] SAT call 69 returned 10 in 1.870 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 108487 skeleton literals in 17975 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 8663 new constraints in 2.7 seconds
[exists>core] replaced 70 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.7 seconds
[exists>core] simplification returned 0
[exists>slvfun] 38571 AIG vars, 169108 AIG ands, 385438 CNF vars, 1074879 CNF clauses
[exists>slvfun] SAT call 69 returned 10 in 4.936 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.2 seconds
[forall>core] 1 rewriting rounds in 0.2 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 19736 AIG ands, 476167 CNF vars, 1434459 CNF clauses
[forall>slvfun] SAT call 70 returned 10 in 0.339 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 110687 skeleton literals in 18229 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 8757 new constraints in 2.8 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.8 seconds
[exists>core] simplification returned 0
[exists>slvfun] 39130 AIG vars, 172404 AIG ands, 390666 CNF vars, 1089313 CNF clauses
[exists>slvfun] SAT call 70 returned 10 in 5.068 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 20011 AIG ands, 489452 CNF vars, 1474453 CNF clauses
[forall>slvfun] SAT call 71 returned 10 in 3.040 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 112887 skeleton literals in 18482 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 8851 new constraints in 2.9 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 39689 AIG vars, 175700 AIG ands, 395894 CNF vars, 1103747 CNF clauses
[exists>slvfun] SAT call 71 returned 10 in 5.138 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 20343 AIG ands, 503100 CNF vars, 1515529 CNF clauses
[forall>slvfun] SAT call 72 returned 10 in 0.345 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 115087 skeleton literals in 18735 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 8945 new constraints in 2.9 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 2.9 seconds
[exists>core] simplification returned 0
[exists>slvfun] 40248 AIG vars, 178996 AIG ands, 401122 CNF vars, 1118181 CNF clauses
[exists>slvfun] SAT call 72 returned 10 in 5.204 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 20606 AIG ands, 517030 CNF vars, 1557451 CNF clauses
[forall>slvfun] SAT call 73 returned 10 in 2.009 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 117287 skeleton literals in 18988 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 9039 new constraints in 3.0 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.0 seconds
[exists>core] simplification returned 0
[exists>slvfun] 40807 AIG vars, 182292 AIG ands, 406350 CNF vars, 1132615 CNF clauses
[exists>slvfun] SAT call 73 returned 10 in 5.351 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 20916 AIG ands, 531265 CNF vars, 1600288 CNF clauses
[forall>slvfun] SAT call 74 returned 10 in 0.428 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 119487 skeleton literals in 19241 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 9133 new constraints in 3.1 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.1 seconds
[exists>core] simplification returned 0
[exists>slvfun] 41366 AIG vars, 185588 AIG ands, 411578 CNF vars, 1147049 CNF clauses
[exists>slvfun] SAT call 74 returned 10 in 5.423 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 21172 AIG ands, 545779 CNF vars, 1643962 CNF clauses
[forall>slvfun] SAT call 75 returned 10 in 4.390 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 121687 skeleton literals in 19494 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 9227 new constraints in 3.1 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.1 seconds
[exists>core] simplification returned 0
[exists>slvfun] 41925 AIG vars, 188884 AIG ands, 416806 CNF vars, 1161483 CNF clauses
[exists>slvfun] SAT call 75 returned 10 in 5.455 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 41 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 41 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 21345 AIG ands, 560471 CNF vars, 1688168 CNF clauses
[forall>slvfun] SAT call 76 returned 10 in 0.383 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 123887 skeleton literals in 19747 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 9341 new constraints in 3.2 seconds
[exists>core] replaced 72 embedded constraints in 0 seconds
[exists>core] replaced 1 embedded constraints in 0 seconds
[exists>core] 3 rewriting rounds in 3.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 42484 AIG vars, 192133 AIG ands, 422047 CNF vars, 1175956 CNF clauses
[exists>slvfun] SAT call 76 returned 10 in 7.688 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 43 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 43 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 21491 AIG ands, 575296 CNF vars, 1732780 CNF clauses
[forall>slvfun] SAT call 77 returned 10 in 1.630 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 126046 skeleton literals in 20001 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 9626 new constraints in 3.2 seconds
[exists>core] replaced 99 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.2 seconds
[exists>core] simplification returned 0
[exists>slvfun] 43043 AIG vars, 194957 AIG ands, 427756 CNF vars, 1191922 CNF clauses
[exists>slvfun] SAT call 77 returned 10 in 5.565 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 43 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 43 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 21677 AIG ands, 590296 CNF vars, 1777922 CNF clauses
[forall>slvfun] SAT call 78 returned 10 in 0.469 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 127913 skeleton literals in 20267 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 9540 new constraints in 3.3 seconds
[exists>core] replaced 68 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.3 seconds
[exists>core] simplification returned 0
[exists>slvfun] 43602 AIG vars, 198253 AIG ands, 432984 CNF vars, 1206356 CNF clauses
[exists>slvfun] SAT call 78 returned 10 in 5.679 seconds
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>merge] merged 0 lambdas in 0.00 seconds
[forall>elimapplies] eliminate 43 applications in round 1
[forall>elimapplies] eliminate 0 applications in round 2
[forall>elimapplies] eliminated 43 function applications in 0.3 seconds
[forall>core] 1 rewriting rounds in 0.3 seconds
[forall>core] simplification returned 10
[forall>slvfun] 633 AIG vars, 21914 AIG ands, 605540 CNF vars, 1823792 CNF clauses
[forall>slvfun] SAT call 79 returned 10 in 2.014 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 219 embedded constraints in 0 seconds
[exists>skel] found 130114 skeleton literals in 20520 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 9634 new constraints in 3.4 seconds
[exists>core] replaced 69 embedded constraints in 0 seconds
[exists>core] 2 rewriting rounds in 3.4 seconds
[exists>core] simplification returned 0
[exists>slvfun] 44161 AIG vars, 201549 AIG ands, 438212 CNF vars, 1220790 CNF clauses
[exists>slvfun] SAT call 79 returned 10 in 5.747 seconds
[btor>core] 0/0/1/0 constraints 0/0/1/0 3.5 MB
[btor>core] variable substitutions: 0
[btor>core] uninterpreted function substitutions: 0
[btor>core] embedded constraint substitutions: 0
[btor>core] assumptions: 0
[btor>core] memory allocated for nodes: 6.73 MB
[btor>core] 
[btor>core] bit blasting statistics:
[btor>core]  AIG vectors (cur/max): 0/0
[btor>core]  AIG ANDs (cur/max): 0/0
[btor>core]  AIG variables: 0
[btor>core]  CNF variables: 0
[btor>core]  CNF clauses: 0
[btor>core]  CNF literals: 0
[btor>core] 
[btor>core] linear constraint equations: 0
[btor>core] gaussian elimination in linear equations: 0
[btor>core] eliminated sliced variables: 0
[btor>core] extracted skeleton constraints: 0
[btor>core] and normalizations: 0
[btor>core] add normalizations: 0
[btor>core] mul normalizations: 0
[btor>core] lambdas merged: 0
[btor>core] apply propagation during construction: 0
[btor>core] beta reductions: 0
[btor>core] clone calls: 0
[btor>slvef] 
[btor>slvef] cegqi solver refinements: 79
[btor>slvef] cegqi solver failed refinements: 0
[btor>slvef] model synthesized const: 0 (0)
[btor>slvef] model synthesized term: 0 (0)
[btor>slvef] model synthesized none: 254 (19812)
[btor>core] 
[btor>core] 0.00 seconds beta-reduction
[btor>core] 0.00 seconds synthesize expressions
[btor>core] 0.00 seconds determining failed assumptions
[btor>core] 0.00 seconds for cloning
[btor>core] 0.00 seconds beta reduction probing
[btor>core] 0.00 seconds substitute and rebuild
[btor>core] 
[btor>core] 0.00 seconds in rewriting engine
[btor>core] 0.00 seconds in variable substitution during rewriting (0%)
[btor>core] 0.00 seconds in embedded constraint replacing during rewriting (0%)
[btor>core] 0.00 seconds in apply elimination during rewriting (0%)
[btor>core] 0.00 seconds skeleton preprocessing during rewriting (100%)
[btor>slvef] 519.72 seconds exists solver
[btor>slvef] 48.08 seconds forall solver
[btor>slvef] 335.76 seconds synthesizing functions
[btor>slvef] 278.00 seconds find partial model
[btor>slvef] 10.73 seconds quantifier instantiation
[btor>slvef] 3.22 seconds check instantiation
[btor>core] 
[btor>core] 7.5 MB
[btor>main] 1200.1 seconds process
[btor>main] 1201.0 seconds real
[btor>main] unknown
[btor>main] CAUGHT SIGNAL 15
unknown
c launch: done
