c launch: /data/cnf/sc2014/app/hwmcc10-timeframe-expansion-k50-pdtvisns3p00-tseitin.cnf.bz2
c host: atom04
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/hwmcc10-timeframe-expansion-k50-pdtvisns3p00-tseitin.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/hwmcc10-timeframe-expansion-k50-pdtvisns3p00-tseitin.cnf.bz2
c no embedded options
c found 'p cnf 183325 546914' header
c read 183325 variables, 546914 clauses, 1276130 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=3
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 183323 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] SUM (--score=3)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  183323   546912         0       0      0     0    0     0   34   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 992 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 992 out of 992 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 2 at-most-one constraints, 2 used 100%
c [card-1] exported 2 binary clauses, 1.0 per/constraint
c [decomp-1] removed 2 variables
c [simpleprobe-1] all 183323 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 12265 variables
c [simpleprobe-1] 5431 variables remain 3% (165627 retained 97%)
c [simpleprobe-1] removed 12265 variables, found 15391 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 12 units, 181 failed, 754 tauts, 0 hbrs, 326 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 170970 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 19557 not tried 11% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 148238 = 87% variables out of 170970 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 162732 negative 92.9% of 175240 except 12508 7.1%
c [phase-count-1] 153535 positive 87.6% of 175240 except 21705 12.4%
c [phase-1] phase bias: 5935 positive 26%, 16797 negative 74%
c [sort-queue-1] sorted 22732 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 22732 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 160591 variables 87.6% (22732 remain 12%)
c [simplification-1] removed 371672 irredundant clauses 68.0% (175240 remain 32%)
c [simplification-1] maximum reduction of 88% = max (88%, 68%)
c [simplification-1] large reduction 88% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.5   22731   175233       300     205     46   661    0     7   25   3%      1    7    2    0 15835%
c i    4.8   22730   175229       965     679    151   697    1    18   25   6%      3   18    7    0 10097%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 10 variables
c [simpleprobe-2] 467 schedulable variables 2%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 6 variables
c [simpleprobe-2] 593 variables remain 3% (22123 retained 97%)
c [simpleprobe-2] removed 6 variables, found 67 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 23341 literals 51%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302858 steps
c [treelook-1] 23171 literals remain 51%
c [treelook-1] 17120 variables remain to probed next time 75%
c [decomp-5] removed 4 variables
c [treelook-1] removed 5 variables, found 169 hbrs
c [basicprobe-1] limit 1400608 based on 175076 irredundant clauses
c [basicprobe-1-0] 9907 probes remain 44% after last round
c [basicprobe-1-0] 23 units = 23 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 109 variables, found 3582 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 14 failed, 100 tauts, 0 hbrs, 30974 literals
c [elim-2] 19437 variables 86% will be scheduled this time
c [elim-2] scheduled 19437 variables 86%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 952 not tried 4% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 4179 = 22% variables out of 19437 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 143210 negative 92.8% of 154354 except 11144 7.2%
c [phase-count-2] 139762 positive 90.5% of 154354 except 14592 9.5%
c [phase-2] phase bias: 112 positive 77%, 33 negative 23%
c [sort-queue-2] sorted 14288 enqueued variables after 1000 conflicts
c [score-dist-2] active 4119 (22%), one 0 (0%), zero 14288 (78%)
c [score-dist-2] max exp 517, different 17 (3%)
c [score-dist-2] median active exp 512, avg 511.7
c [simplification-2] removed 4323 variables 19.0% (18407 remain 10%)
c [simplification-2] removed 20875 irredundant clauses 11.9% (154354 remain 28%)
c [simplification-2] maximum reduction of 19% = max (19%, 12%)
c [simplification-2] large reduction 19% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 305 at-most-one constraints of average size 3.0
c [card-2] found 12 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 317 out of 317 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 70 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 19240 literals 52%
c [treelook-2] scheduling used 300011 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 308489 steps
c [treelook-2] 19157 literals remain 52%
c [treelook-2] 11863 variables remain to probed next time 65%
c [decomp-7] removed 12 variables
c [treelook-2] removed 22 variables, found 1145 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 3 failed, 6408 tauts, 0 hbrs, 15360 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 18311 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 606 not tried 3% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1286 = 7% variables out of 18311 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 133189 negative 92.8% of 143466 except 10277 7.2%
c [phase-count-3] 129758 positive 90.4% of 143466 except 13708 9.6%
c [phase-3] phase bias: 6 positive 19%, 25 negative 81%
c [sort-queue-3] sorted 10099 enqueued variables after 3000 conflicts
c [score-dist-3] active 6926 (41%), one 0 (0%), zero 10099 (59%)
c [score-dist-3] max exp 520, different 20 (4%)
c [score-dist-3] median active exp 514, avg 514.1
c [simplification-3] removed 1382 variables 7.5% (17025 remain 9%)
c [simplification-3] removed 10888 irredundant clauses 7.1% (143466 remain 26%)
c [simplification-3] maximum reduction of 8% = max (8%, 7%)
c [simplification-3] large reduction 8% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-3] new conflict limit 5000 (hard 15000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.1   17024   143465      3556    2413    367  3171    6    60   23   9%     26   58   21    0 4596%
c 
c [simplification-4] limit 5000 conflicts (hard 15000) hit after 5000 conflicts
c [decomp-8] removed 3 variables
c [basicprobe-2] limit 2945894 penalty 0 = 0 + 0
c [basicprobe-2-0] 7130 sched 42%, 41 failed, 1 lifted, 4756 hbrs
c [decomp-9] removed 79 variables
c [basicprobe-2-1] 6814 probes remain 40% after last round
c [basicprobe-2-1] 44 units = 43 failed (98%) + 1 lifted (2%)
c [basicprobe-2-1] removed 81 variables, found 4986 hbrs
c [unhide-4] limit 117835 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 433 tauts, 0 hbrs, 15397 literals
c [elim-4] 596 variables 4% will be scheduled this time
c [elim-4] scheduled 596 variables 4%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 48200342 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 596 scheduled
c [phase-count-4] 120869 negative 92.1% of 131209 except 10340 7.9%
c [phase-count-4] 117219 positive 89.3% of 131209 except 13990 10.7%
c [phase-4] phase bias: 3 positive 33%, 6 negative 67%
c [sort-queue-4] sorted 8464 enqueued variables after 5000 conflicts
c [score-dist-4] active 8477 (50%), one 0 (0%), zero 8464 (50%)
c [score-dist-4] max exp 523, different 23 (4%)
c [score-dist-4] median active exp 516, avg 515.8
c [simplification-4] removed 83 variables 0.5% (16941 remain 9%)
c [simplification-4] removed 12255 irredundant clauses 8.5% (131209 remain 24%)
c [simplification-4] maximum reduction of 9% = max (0%, 9%)
c [simplification-4] large reduction 9% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17000 (soft 7000 + delta 10000)
c [simplification-4] new conflict limit 7000 (hard 17000)
c 
c [simplification-5] limit 7000 conflicts (hard 17000) hit after 7000 conflicts
c [quatres-1] found 30084 quaternary clauses 47% in total
c [quatres-1-1] removed 4 duplicate quaternary clauses
c [quatres-1-1] added 4 double-self-subsuming ternary resolvents
c [quatres-1-2] added 522 single-self-subsuming ternary resolvents
c [quatres-1-2] added 2488 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 16941 free variables schedulable
c [ternres-1] 50768 ternary resolvents (1104 bin, 49664 trn)
c [ternres-1] 1 variables remain 0% (16940 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 582 xors of average arity 2.9
c [gauss-1] connected 1690 occurrences of 218 variables (average 7.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 35 variables
c [simpleprobe-3] 248 schedulable variables 1%
c [simpleprobe-3] limit 3453551 penalty 0 = 0 + 0
c [decomp-11] removed 24 variables
c [simpleprobe-3] 471 variables remain 3% (16411 retained 97%)
c [simpleprobe-3] removed 24 variables, found 335 hbrs, 4 units
c [transred-1] limit 863387 with penalty 0 = 0 + 0
c [transred-1] removed 1146 transitive binary clauses
c [transred-1] found 26 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 16856 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 539 blocked clauses
c [block-1] 539 < 1/100 * 130323 = 1303 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 26 (12%) of length 11
c [cce-1-1] eliminated 2 clauses out of 44 (5%) of length 10
c [cce-1-1] eliminated 19 clauses out of 316 (6%) of length 9
c [cce-1-1] eliminated 114 clauses out of 1117 (10%) of length 8
c [cce-1-1] eliminated 645 clauses out of 3251 (20%) of length 7
c [cce-1-1] eliminated 1676 clauses out of 7949 (21%) of length 6
c [cce-1-1] eliminated 218 clauses out of 19118 (1%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2677 large clauses in 30000049 steps
c [cce-1-1] allowing another 15000024 steps for small clauses
c [cce-1-1] scheduling 31447 clauses = 16036 binary + 15411 ternary
c [cce-1-1] tried to eliminate 20333 small clauses 65%
c [cce-1-1] eliminated 727 binary clauses 5%
c [cce-1-1] eliminated 2939 ternary clauses 19%
c [cce-1-1] eliminated 3666 small clauses 12%
c [cce-1-1] eliminated 3666 small clauses in 30000004 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 6343 covered clauses in round 1
c [cce-1] eliminated 6343 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 246882 added (scaled 2)
c [bca-1] 23421 out of 33712 literals actually usable 69%
c [bca-1] added 145 blocked clauses in 84335 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 7576 pos 44.9% + 9279 neg 55.1% = 16855 sched 100.0% ret 0
c [sweep-1-1] 1005065 steps 111 queries 2206.37 avg class size
c [sweep-1-1] 2628 decisions 107 SAT calls 47.74 avg env size
c [sweep-1-1] 15574 variables remain 92% (1281 retained 8%)
c [decomp-12] removed 4 variables
c [sweep-1-1] removed 4 vars (0 failed, 3 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 4 vars in TOTAL (1 rounds, 110 queries)
c [phase-count-5] 114060 negative 92.6% of 123176 except 9116 7.4%
c [phase-count-5] 109931 positive 89.2% of 123176 except 13245 10.8%
c [phase-5] phase bias: 7 positive 44%, 9 negative 56%
c [sort-queue-5] sorted 7447 enqueued variables after 7000 conflicts
c [score-dist-5] active 9404 (56%), one 0 (0%), zero 7447 (44%)
c [score-dist-5] max exp 524, different 23 (4%)
c [score-dist-5] median active exp 517, avg 516.8
c [simplification-5] removed 90 variables 0.5% (16851 remain 9%)
c [simplification-5] removed 8033 irredundant clauses 6.1% (123176 remain 23%)
c [simplification-5] maximum reduction of 6% = max (1%, 6%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19000 (soft 9000 + delta 10000)
c [simplification-5] new conflict limit 9000 (hard 19000)
c 
c [simplification-6] limit 9000 conflicts (hard 19000) hit after 9003 conflicts
c [quatres-2] found 31958 quaternary clauses 51% in total
c [quatres-2-1] removed 5 duplicate quaternary clauses
c [quatres-2-1] added 16 double-self-subsuming ternary resolvents
c [quatres-2-2] added 446 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1199 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 505 ternary resolvents (12 bin, 493 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 293 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 293 out of 293 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-13] removed 2 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15390 literals 46%
c [treelook-3] scheduling used 300049 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 300019 steps
c [treelook-3] 15179 literals remain 45%
c [treelook-3] 9514 variables remain to probed next time 56%
c [decomp-14] removed 1 variables
c [treelook-3] removed 2 variables, found 167 hbrs
c [unhide-5] limit 130323 with penalty 1 = 1 + 0
c [unhide-5-5] 3 units, 0 failed, 1373 tauts, 0 hbrs, 12250 literals
c [transred-2] limit 1303237 with penalty 0 = 0 + 0
c [transred-2] removed 1220 transitive binary clauses
c [transred-2] found 3 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 314 clauses out of 18240 (2%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 314 large clauses in 30000007 steps
c [cce-2-1] allowing another 15000003 steps for small clauses
c [cce-2-1] scheduling 52569 clauses = 15352 binary + 37217 ternary
c [cce-2-1] tried to eliminate 18504 small clauses 35%
c [cce-2-1] eliminated 129 binary clauses 1%
c [cce-2-1] eliminated 3888 ternary clauses 10%
c [cce-2-1] eliminated 4017 small clauses 8%
c [cce-2-1] eliminated 4101 small clauses in 30000005 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 4415 covered clauses in round 1
c [cce-2] eliminated 4415 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 16835 variables 100%
c [elim-5] limit of 13032374 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 703 not tried 4% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1192 = 7% variables out of 16835 scheduled
c [bca-2] limit of 10000000 steps and 229944 added (scaled 2)
c [bca-2] 20762 out of 31288 literals actually usable 66%
c [bca-2] added 39 blocked clauses in 76238 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 6864 pos 47.5% + 7593 neg 52.5% = 14457 sched 92.4% ret 1186
c [sweep-2-1] 1014713 steps 140 queries 2140.03 avg class size
c [sweep-2-1] 2918 decisions 136 SAT calls 46.52 avg env size
c [sweep-2-1] 13056 variables remain 83% (2587 retained 17%)
c [decomp-15] removed 48 variables
c [sweep-2-1] removed 48 vars (0 failed, 4 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 48 vars in TOTAL (1 rounds, 139 queries)
c [phase-count-6] 106410 negative 92.9% of 114586 except 8176 7.1%
c [phase-count-6] 102417 positive 89.4% of 114586 except 12169 10.6%
c [phase-6] phase bias: 1 positive 10%, 9 negative 90%
c [sort-queue-6] sorted 6267 enqueued variables after 9003 conflicts
c [score-dist-6] active 9328 (60%), one 0 (0%), zero 6267 (40%)
c [score-dist-6] max exp 526, different 25 (5%)
c [score-dist-6] median active exp 518, avg 517.7
c [simplification-6] removed 1256 variables 7.5% (15595 remain 9%)
c [simplification-6] removed 8590 irredundant clauses 7.0% (114586 remain 21%)
c [simplification-6] maximum reduction of 7% = max (7%, 7%)
c [simplification-6] large reduction 7% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21003 (soft 11003 + delta 10000)
c [simplification-6] new conflict limit 11003 (hard 21003)
c 
c [simplification-7] limit 11003 conflicts (hard 21003) hit after 11004 conflicts
c [quatres-3] found 31981 quaternary clauses 51% in total
c [quatres-3-1] removed 4 duplicate quaternary clauses
c [quatres-3-1] added 23 double-self-subsuming ternary resolvents
c [quatres-3-2] added 470 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1023 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 15595 free variables schedulable
c [ternres-3] 1512 ternary resolvents (68 bin, 1444 trn)
c [ternres-3] 4128 variables remain 26% (11467 retained 74%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 302 xors of average arity 3.0
c [gauss-2] connected 900 occurrences of 273 variables (average 3.3)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-16] removed 9 variables
c [basicprobe-3] limit 8215420 penalty 0 = 0 + 0
c [basicprobe-3-0] 6876 sched 44%, 80 failed, 0 lifted, 4130 hbrs
c [decomp-17] removed 157 variables
c [basicprobe-3-1] 8796 sched 57%, 26 failed, 0 lifted, 1253 hbrs
c [decomp-18] removed 46 variables
c [basicprobe-3-2] 3698 probes remain 24% after last round
c [basicprobe-3-2] 106 units = 106 failed (100%) + 0 lifted (0%)
c [basicprobe-3-2] removed 203 variables, found 5493 hbrs
c [bate-1] eliminated 450 asymmetric tautologies during probing
c [unhide-6] limit 328616 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 0 failed, 8663 tauts, 0 hbrs, 30407 literals
c [transred-3] limit 1643084 with penalty 0 = 0 + 0
c [transred-3] removed 1260 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 15383 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 81 blocked clauses
c [block-2] 81 < 1/100 * 112478 = 1124 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 40 (5%) of length 10
c [cce-3-1] eliminated 18 clauses out of 344 (5%) of length 9
c [cce-3-1] eliminated 45 clauses out of 872 (5%) of length 8
c [cce-3-1] eliminated 143 clauses out of 2298 (6%) of length 7
c [cce-3-1] eliminated 868 clauses out of 6028 (14%) of length 6
c [cce-3-1] eliminated 871 clauses out of 15672 (6%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1947 large clauses in 30000152 steps
c [cce-3-1] allowing another 15000076 steps for small clauses
c [cce-3-1] scheduling 45855 clauses = 13627 binary + 32228 ternary
c [cce-3-1] tried to eliminate 14973 small clauses 33%
c [cce-3-1] eliminated 525 binary clauses 4%
c [cce-3-1] eliminated 2935 ternary clauses 9%
c [cce-3-1] eliminated 3460 small clauses 8%
c [cce-3-1] eliminated 3460 small clauses in 30000019 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5407 covered clauses in round 1
c [cce-3] eliminated 5407 covered clauses in TOTAL during 1 rounds
c [elim-6] 700 variables 5% will be scheduled this time
c [elim-6] scheduled 700 variables 5%
c [elim-6] limit of 32861682 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 21206465 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 700 scheduled
c [bca-3] limit of 10000000 steps and 213866 added (scaled 2)
c [bca-3] 19582 out of 30766 literals actually usable 64%
c [bca-3] added 14 blocked clauses in 70534 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 6096 pos 47.5% + 6735 neg 52.5% = 12831 sched 83.4% ret 2551
c [sweep-3-1] 1000307 steps 134 queries 2018.96 avg class size
c [sweep-3-1] 2927 decisions 133 SAT calls 47.55 avg env size
c [sweep-3-1] 11518 variables remain 75% (3864 retained 25%)
c [decomp-19] removed 3 variables
c [sweep-3-1] removed 3 vars (0 failed, 2 eqs, 11 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3 vars in TOTAL (1 rounds, 133 queries)
c [phase-count-7] 99540 negative 93.3% of 106631 except 7091 6.7%
c [phase-count-7] 95314 positive 89.4% of 106631 except 11317 10.6%
c [phase-7] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-7] sorted 5998 enqueued variables after 11004 conflicts
c [score-dist-7] active 9381 (61%), one 0 (0%), zero 5998 (39%)
c [score-dist-7] max exp 526, different 24 (5%)
c [score-dist-7] median active exp 518, avg 518.1
c [simplification-7] removed 216 variables 1.4% (15379 remain 8%)
c [simplification-7] removed 7955 irredundant clauses 6.9% (106631 remain 19%)
c [simplification-7] maximum reduction of 7% = max (1%, 7%)
c [simplification-7] large reduction 7% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 23004 (soft 13004 + delta 10000)
c [simplification-7] new conflict limit 13004 (hard 23004)
c 
c [simplification-8] limit 13004 conflicts (hard 23004) hit after 13005 conflicts
c [quatres-4] found 33516 quaternary clauses 58% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 8 double-self-subsuming ternary resolvents
c [quatres-4-2] added 553 single-self-subsuming ternary resolvents
c [quatres-4-2] added 815 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 4044 schedulable variables 26%
c [ternres-4] 5535 ternary resolvents (146 bin, 5389 trn)
c [ternres-4] 146 variables remain 1% (15233 retained 99%)
c [decomp-20] removed 20 variables
c [simpleprobe-4] 439 schedulable variables 3%
c [simpleprobe-4] limit 7738360 penalty 0 = 0 + 0
c [decomp-21] removed 11 variables
c [simpleprobe-4] 448 variables remain 3% (14900 retained 97%)
c [simpleprobe-4] removed 11 variables, found 868 hbrs, 0 units
c [transred-4] limit 1934590 with penalty 0 = 0 + 0
c [transred-4] removed 1235 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 3282 clauses out of 14437 (23%) of length 5
c [cce-4-1] eliminated 3979 clauses out of 28594 (14%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 7261 large clauses in 79573098 steps
c [cce-4-1] allowing another 39786549 steps for small clauses
c [cce-4-1] scheduling 25433 clauses = 13104 binary + 12329 ternary
c [cce-4-1] tried to eliminate 25433 small clauses 100%
c [cce-4-1] eliminated 217 binary clauses 2%
c [cce-4-1] eliminated 1982 ternary clauses 16%
c [cce-4-1] eliminated 2199 small clauses 9%
c [cce-4-1] eliminated 2199 small clauses in 56509238 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 9460 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 34228107 steps for small clauses
c [cce-4-2] scheduling 23234 clauses = 12887 binary + 10347 ternary
c [cce-4-2] tried to eliminate 23234 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 9460 covered clauses in TOTAL during 2 rounds
c [bca-4] limit of 10000000 steps and 194583 added (scaled 2)
c [bca-4] 18373 out of 30698 literals actually usable 60%
c [bca-4] added 15 blocked clauses in 69089 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 5115 pos 44.5% + 6377 neg 55.5% = 11492 sched 74.9% ret 3856
c [sweep-4-1] 1003871 steps 131 queries 1620.00 avg class size
c [sweep-4-1] 3290 decisions 131 SAT calls 53.54 avg env size
c [sweep-4-1] 10072 variables remain 66% (5276 retained 34%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 130 queries)
c [phase-count-8] 90771 negative 93.6% of 96992 except 6221 6.4%
c [phase-count-8] 86051 positive 88.7% of 96992 except 10941 11.3%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-8] sorted 5647 enqueued variables after 13005 conflicts
c [score-dist-8] active 9701 (63%), one 0 (0%), zero 5647 (37%)
c [score-dist-8] max exp 527, different 25 (5%)
c [score-dist-8] median active exp 518, avg 518.4
c [simplification-8] removed 31 variables 0.2% (15348 remain 8%)
c [simplification-8] removed 9639 irredundant clauses 9.0% (96992 remain 18%)
c [simplification-8] maximum reduction of 9% = max (0%, 9%)
c [simplification-8] large reduction 9% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 25005 (soft 15005 + delta 10000)
c [simplification-8] new conflict limit 15005 (hard 25005)
c 
c [simplification-9] limit 15005 conflicts (hard 25005) hit after 15006 conflicts
c [quatres-5] found 29822 quaternary clauses 58% in total
c [quatres-5-1] removed 11 duplicate quaternary clauses
c [quatres-5-1] added 3 double-self-subsuming ternary resolvents
c [quatres-5-2] added 83 single-self-subsuming ternary resolvents
c [quatres-5-2] added 391 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] 146 schedulable variables 1%
c [ternres-5] 4337 ternary resolvents (136 bin, 4201 trn)
c [ternres-5] 6 variables remain 0% (15342 retained 100%)
c [decomp-23] removed 8 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 14773 literals 48%
c [treelook-4] scheduling used 300032 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 302526 steps
c [treelook-4] 14526 literals remain 47%
c [treelook-4] 7882 variables remain to probed next time 51%
c [decomp-24] removed 1 variables
c [treelook-4] removed 1 variables, found 223 hbrs
c [unhide-7] limit 223952 with penalty 1 = 1 + 0
c [unhide-7-7] 0 units, 0 failed, 1516 tauts, 0 hbrs, 15201 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 986 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 21 (5%) of length 11
c [cce-5-1] eliminated 3 clauses out of 28 (11%) of length 10
c [cce-5-1] eliminated 1 clauses out of 5058 (0%) of length 6
c [cce-5-1] eliminated 1027 clauses out of 10804 (10%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1032 large clauses in 30000007 steps
c [cce-5-1] allowing another 15000003 steps for small clauses
c [cce-5-1] scheduling 42457 clauses = 12972 binary + 29485 ternary
c [cce-5-1] tried to eliminate 16918 small clauses 40%
c [cce-5-1] eliminated 356 binary clauses 3%
c [cce-5-1] eliminated 2684 ternary clauses 9%
c [cce-5-1] eliminated 3040 small clauses 7%
c [cce-5-1] eliminated 3040 small clauses in 30000020 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 4072 covered clauses in round 1
c [cce-5] eliminated 4072 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 15339 variables 100%
c [elim-7] limit of 22395270 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 62 not tried 0% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2048 = 13% variables out of 15339 scheduled
c [bca-5] limit of 10000000 steps and 176214 added (scaled 2)
c [bca-5] 16224 out of 26584 literals actually usable 61%
c [bca-5] added 81 blocked clauses in 61013 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 4085 pos 47.2% + 4565 neg 52.8% = 8650 sched 65.1% ret 4641
c [sweep-5-1] 7040628 steps 1517 queries 130.45 avg class size
c [sweep-5-1] 23469 decisions 1473 SAT calls 31.33 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-25] removed 88 variables
c [sweep-5-1] removed 88 vars (0 failed, 90 eqs, 190 impls)
c [sweep-5-2] 5943 pos 45.0% + 7260 neg 55.0% = 13203 sched 100.0% ret 0
c [sweep-5-2] 2968890 steps 396 queries 449.28 avg class size
c [sweep-5-2] 8510 decisions 395 SAT calls 45.96 avg env size
c [sweep-5-2] 5829 variables remain 44% (7374 retained 56%)
c [decomp-26] removed 5 variables
c [sweep-5-2] removed 5 vars (0 failed, 4 eqs, 16 impls)
c [sweep-5] removed 93 vars in TOTAL (2 rounds, 1911 queries)
c [phase-count-9] 82701 negative 94.4% of 87615 except 4914 5.6%
c [phase-count-9] 78065 positive 89.1% of 87615 except 9550 10.9%
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-9] sorted 4053 enqueued variables after 15006 conflicts
c [score-dist-9] active 9145 (69%), one 0 (0%), zero 4053 (31%)
c [score-dist-9] max exp 527, different 22 (4%)
c [score-dist-9] median active exp 519, avg 519.0
c [simplification-9] removed 2150 variables 14.0% (13198 remain 7%)
c [simplification-9] removed 9377 irredundant clauses 9.7% (87615 remain 16%)
c [simplification-9] maximum reduction of 14% = max (14%, 10%)
c [simplification-9] large reduction 14% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 27006 (soft 17006 + delta 10000)
c [simplification-9] new conflict limit 17006 (hard 27006)
c 
c [simplification-10] limit 17006 conflicts (hard 27006) hit after 17006 conflicts
c [quatres-6] found 27940 quaternary clauses 56% in total
c [quatres-6-1] removed 7 duplicate quaternary clauses
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 692 single-self-subsuming ternary resolvents
c [quatres-6-2] added 956 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] 6 schedulable variables 0%
c [ternres-6] 2825 ternary resolvents (53 bin, 2772 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 53 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 53 out of 53 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 234 xors of average arity 3.0
c [gauss-3] connected 700 occurrences of 274 variables (average 2.6)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-27] removed 2 variables
c [basicprobe-4] limit 12767741 penalty 0 = 0 + 0
c [basicprobe-4-0] 3141 sched 24%, 9 failed, 0 lifted, 334 hbrs
c [decomp-28] removed 10 variables
c [basicprobe-4-1] 6850 sched 52%, 5 failed, 0 lifted, 357 hbrs
c [decomp-29] removed 5 variables
c [basicprobe-4-2] 6802 sched 52%, 0 failed, 0 lifted, 63 hbrs
c [basicprobe-4-3] 6803 sched 52%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-4] 6803 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-4] fully completed probing
c [basicprobe-4-4] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-4-4] removed 15 variables, found 762 hbrs
c [bate-2] eliminated 198 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 831 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 13181 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 54 blocked clauses
c [block-3] 54 < 1/100 * 87251 = 872 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 10 clauses out of 459 (2%) of length 9
c [cce-6-1] eliminated 87 clauses out of 1056 (8%) of length 8
c [cce-6-1] eliminated 173 clauses out of 2365 (7%) of length 7
c [cce-6-1] eliminated 372 clauses out of 5506 (7%) of length 6
c [cce-6-1] eliminated 332 clauses out of 10626 (3%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 974 large clauses in 30000076 steps
c [cce-6-1] allowing another 15000038 steps for small clauses
c [cce-6-1] scheduling 20083 clauses = 10999 binary + 9084 ternary
c [cce-6-1] tried to eliminate 20083 small clauses 100%
c [cce-6-1] eliminated 66 binary clauses 1%
c [cce-6-1] eliminated 691 ternary clauses 8%
c [cce-6-1] eliminated 757 small clauses 4%
c [cce-6-1] eliminated 757 small clauses in 28293369 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 1731 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 853338 steps for small clauses
c [cce-6-2] scheduling 19326 clauses = 10933 binary + 8393 ternary
c [cce-6-2] tried to eliminate 1218 small clauses 6%
c [cce-6-2] incomplete small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 1731 covered clauses in TOTAL during 2 rounds
c [elim-8] 62 variables 0% will be scheduled this time
c [elim-8] scheduled 62 variables 0%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1021419340 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 3639653 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 62 scheduled
c [bca-6] limit of 10000000 steps and 171265 added (scaled 2)
c [bca-6] 14458 out of 26358 literals actually usable 55%
c [bca-6] added 15 blocked clauses in 59450 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 2845 pos 48.9% + 2972 neg 51.1% = 5817 sched 44.1% ret 7361
c [sweep-6-1] 1000418 steps 177 queries 653.50 avg class size
c [sweep-6-1] 3603 decisions 175 SAT calls 39.08 avg env size
c [sweep-6-1] 4498 variables remain 34% (8680 retained 66%)
c [decomp-32] removed 3 variables
c [sweep-6-1] removed 3 vars (0 failed, 2 eqs, 3 impls)
c [sweep-6] 3 < 1/1000 * 13178 = 13 considered unsuccessful
c [sweep-6] removed 3 vars in TOTAL (1 rounds, 176 queries)
c [phase-count-10] 80671 negative 94.6% of 85305 except 4634 5.4%
c [phase-count-10] 75884 positive 89.0% of 85305 except 9421 11.0%
c [phase-count-10] less non-negative clauses 4634 than limit 8500 (10.0%)
c [phase-count-10] non-pos/non-neg = 9421/4634 = 2.03 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-10] sorted 3738 enqueued variables after 17006 conflicts
c [score-dist-10] active 9437 (72%), one 0 (0%), zero 3738 (28%)
c [score-dist-10] max exp 527, different 22 (4%)
c [score-dist-10] median active exp 520, avg 519.5
c [simplification-10] removed 23 variables 0.2% (13175 remain 7%)
c [simplification-10] removed 2310 irredundant clauses 2.6% (85305 remain 16%)
c [simplification-10] maximum reduction of 3% = max (0%, 3%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 5000
c [simplification-10] penalized conflict interval 5000 = 1 * 5000
c [simplification-10] hard conflict limit 32006 (soft 22006 + delta 10000)
c [simplification-10] new conflict limit 22006 (hard 32006)
c 
c [simplification-11] limit 22006 conflicts (hard 32006) hit after 22006 conflicts
c [quatres-7] found 28523 quaternary clauses 58% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-1] added 4 double-self-subsuming ternary resolvents
c [quatres-7-2] added 87 single-self-subsuming ternary resolvents
c [quatres-7-2] added 95 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 13175 free variables schedulable
c [ternres-7] 1656 ternary resolvents (36 bin, 1620 trn)
c [ternres-7] 988 variables remain 7% (12187 retained 93%)
c [simpleprobe-5] 405 schedulable variables 3%
c [simpleprobe-5] limit 14591339 penalty 0 = 0 + 0
c [decomp-34] removed 1 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1 variables, found 877 hbrs, 0 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 810 transitive binary clauses
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 3 clauses out of 449 (1%) of length 9
c [cce-7-1] eliminated 4 clauses out of 966 (0%) of length 8
c [cce-7-1] eliminated 31 clauses out of 2181 (1%) of length 7
c [cce-7-1] eliminated 185 clauses out of 5014 (4%) of length 6
c [cce-7-1] eliminated 609 clauses out of 9834 (6%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 832 large clauses in 30000002 steps
c [cce-7-1] allowing another 15000001 steps for small clauses
c [cce-7-1] scheduling 35146 clauses = 10928 binary + 24218 ternary
c [cce-7-1] tried to eliminate 17340 small clauses 49%
c [cce-7-1] eliminated 181 binary clauses 2%
c [cce-7-1] eliminated 1934 ternary clauses 8%
c [cce-7-1] eliminated 2115 small clauses 6%
c [cce-7-1] eliminated 2115 small clauses in 30000072 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 2947 covered clauses in round 1
c [cce-7] eliminated 2947 covered clauses in TOTAL during 1 rounds
c [bca-7] limit of 10000000 steps and 165352 added (scaled 2)
c [bca-7] 13932 out of 26350 literals actually usable 53%
c [bca-7] added 17 blocked clauses in 62222 steps
c [phase-count-11] 77985 negative 94.7% of 82349 except 4364 5.3%
c [phase-count-11] 73146 positive 88.8% of 82349 except 9203 11.2%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 3452 enqueued variables after 22006 conflicts
c [score-dist-11] active 9722 (74%), one 0 (0%), zero 3452 (26%)
c [score-dist-11] max exp 528, different 23 (4%)
c [score-dist-11] median active exp 521, avg 520.5
c [simplification-11] removed 1 variables 0.0% (13174 remain 7%)
c [simplification-11] removed 2956 irredundant clauses 3.5% (82349 remain 15%)
c [simplification-11] maximum reduction of 3% = max (0%, 3%)
c [simplification-11] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-11] new conflict interval 10000
c [simplification-11] penalized conflict interval 10000 = 1 * 10000
c [simplification-11] hard conflict limit 42006 (soft 32006 + delta 10000)
c [simplification-11] new conflict limit 32006 (hard 42006)
c 
c [simplification-12] limit 32006 conflicts (hard 42006) hit after 32010 conflicts
c [quatres-8] found 28600 quaternary clauses 58% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 38 single-self-subsuming ternary resolvents
c [quatres-8-2] added 43 quaternary resolvents
c [ternres-8] limit 6272496 with penalty 0 = 0 + 0
c [ternres-8] 988 schedulable variables 7%
c [ternres-8] 4749 ternary resolvents (129 bin, 4620 trn)
c [ternres-8] 1 variables remain 0% (13173 retained 100%)
c [decomp-35] removed 3 variables
c [treelook-5] limit 627249 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 16278 literals 62%
c [treelook-5] scheduling used 444436 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 627249 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 628943 steps
c [treelook-5] 15747 literals remain 60%
c [treelook-5] 6739 variables remain to probed next time 51%
c [treelook-5] removed 0 variables, found 531 hbrs
c [unhide-8] limit 313624 with penalty 2 = 2 + 0
c [unhide-8-8] 0 units, 0 failed, 6069 tauts, 0 hbrs, 92712 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 542 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 313624830 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 4581 (0%) of length 6
c [cce-8-1] eliminated 283 clauses out of 8783 (3%) of length 5
c [cce-8-1] eliminated 763 clauses out of 22861 (3%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1047 large clauses in 54285469 steps
c [cce-8-1] allowing another 27142734 steps for small clauses
c [cce-8-1] scheduling 33740 clauses = 10880 binary + 22860 ternary
c [cce-8-1] tried to eliminate 33740 small clauses 100%
c [cce-8-1] eliminated 26 binary clauses 0%
c [cce-8-1] eliminated 1591 ternary clauses 7%
c [cce-8-1] eliminated 1617 small clauses 5%
c [cce-8-1] eliminated 1617 small clauses in 49341180 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 2664 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 26292292 steps for small clauses
c [cce-8-2] scheduling 32123 clauses = 10854 binary + 21269 ternary
c [cce-8-2] tried to eliminate 32123 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 2664 covered clauses in TOTAL during 2 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 13171 variables 100%
c [elim-9] limit of 62724966 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 993 variables 8% in round 1 in 20593763 steps
c [elim-9-1] backward subsumption/strengthening limit 20593700
c [elim-9-1-1] backward checking 3925 touched variables 30%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 24 and strengthened 85 clauses in 1394413 steps
c [elim-9-1] rescheduled 310 variables 2% by backward subsumption
c [elim-9-2] eliminated 9 variables 0% in round 2 in 1201232 steps
c [elim-9-2] backward subsumption/strengthening limit 1201200
c [elim-9-2-1] backward checking 78 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 3 and strengthened 15 clauses in 139614 steps
c [elim-9-2] rescheduled 26 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 144998 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1002 = 8% variables out of 13171 scheduled
c [bca-8] limit of 10000000 steps and 155507 added (scaled 2)
c [bca-8] 13141 out of 24340 literals actually usable 54%
c [bca-8] added 62 blocked clauses in 58479 steps
c [sweep-7] limit 940874 penalty 1 = 1 + 0
c [sweep-7-1] 2044 pos 49.9% + 2054 neg 50.1% = 4098 sched 33.7% ret 8071
c [sweep-7-1] 947713 steps 162 queries 463.19 avg class size
c [sweep-7-1] 3834 decisions 162 SAT calls 45.70 avg env size
c [sweep-7-1] 3237 variables remain 27% (8932 retained 73%)
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-7] removed 0 vars in TOTAL (1 rounds, 161 queries)
c [phase-count-12] 73580 negative 95.0% of 77422 except 3842 5.0%
c [phase-count-12] 68567 positive 88.6% of 77422 except 8855 11.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 3006 enqueued variables after 32010 conflicts
c [score-dist-12] active 9163 (75%), one 0 (0%), zero 3006 (25%)
c [score-dist-12] max exp 530, different 25 (5%)
c [score-dist-12] median active exp 522, avg 521.7
c [simplification-12] removed 1005 variables 7.6% (12169 remain 7%)
c [simplification-12] removed 4927 irredundant clauses 6.0% (77422 remain 14%)
c [simplification-12] maximum reduction of 8% = max (8%, 6%)
c [simplification-12] large reduction 8% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 44010 (soft 34010 + delta 10000)
c [simplification-12] new conflict limit 34010 (hard 44010)
c 
c [simplification-13] limit 34010 conflicts (hard 44010) hit after 34011 conflicts
c [quatres-9] found 25997 quaternary clauses 57% in total
c [quatres-9-1] removed 4 duplicate quaternary clauses
c [quatres-9-1] added 4 double-self-subsuming ternary resolvents
c [quatres-9-2] added 227 single-self-subsuming ternary resolvents
c [quatres-9-2] added 557 quaternary resolvents
c [ternres-9] limit 6739354 with penalty 0 = 0 + 0
c [ternres-9] 1 schedulable variables 0%
c [ternres-9] 1820 ternary resolvents (11 bin, 1809 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-5] limit 33696771 penalty 0 = 0 + 0
c [basicprobe-5-0] 6132 sched 50%, 3 failed, 0 lifted, 420 hbrs
c [decomp-39] removed 3 variables
c [basicprobe-5-1] 6097 sched 50%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-5-2] 6097 sched 50%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-2] fully completed probing
c [basicprobe-5-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-5-2] removed 3 variables, found 431 hbrs
c [bate-3] eliminated 28 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 246 transitive binary clauses
c [cce-9] limit of 33696771 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 43 (2%) of length 10
c [cce-9-1] eliminated 6 clauses out of 422 (1%) of length 9
c [cce-9-1] eliminated 25 clauses out of 1015 (2%) of length 8
c [cce-9-1] eliminated 80 clauses out of 2113 (4%) of length 7
c [cce-9-1] eliminated 289 clauses out of 4753 (6%) of length 6
c [cce-9-1] eliminated 764 clauses out of 8689 (9%) of length 5
c [cce-9-1] eliminated 607 clauses out of 21295 (3%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 1772 large clauses in 33696778 steps
c [cce-9-1] allowing another 16848389 steps for small clauses
c [cce-9-1] scheduling 30193 clauses = 10048 binary + 20145 ternary
c [cce-9-1] tried to eliminate 20031 small clauses 66%
c [cce-9-1] eliminated 142 binary clauses 1%
c [cce-9-1] eliminated 668 ternary clauses 3%
c [cce-9-1] eliminated 810 small clauses 3%
c [cce-9-1] eliminated 810 small clauses in 33696772 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 2582 covered clauses in round 1
c [cce-9] eliminated 2582 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 12166 variables 100%
c [elim-10] limit of 134787086 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 312 variables 3% in round 1 in 18540106 steps
c [elim-10-1] backward subsumption/strengthening limit 18540100
c [elim-10-1-1] backward checking 1959 touched variables 16%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 1 and strengthened 13 clauses in 803860 steps
c [elim-10-1] rescheduled 55 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 234886 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 312 = 3% variables out of 12166 scheduled
c [bca-9] limit of 10000000 steps and 148818 added (scaled 2)
c [bca-9] 12449 out of 23710 literals actually usable 53%
c [bca-9] added 41 blocked clauses in 57531 steps
c [phase-count-13] 70700 negative 95.5% of 74062 except 3362 4.5%
c [phase-count-13] 65527 positive 88.5% of 74062 except 8535 11.5%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 2877 enqueued variables after 34011 conflicts
c [score-dist-13] active 8977 (76%), one 0 (0%), zero 2877 (24%)
c [score-dist-13] max exp 530, different 25 (5%)
c [score-dist-13] median active exp 523, avg 521.9
c [simplification-13] removed 315 variables 2.6% (11854 remain 6%)
c [simplification-13] removed 3360 irredundant clauses 4.3% (74062 remain 14%)
c [simplification-13] maximum reduction of 4% = max (3%, 4%)
c [simplification-13] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-13] new conflict interval 14000
c [simplification-13] penalized conflict interval 14000 = 1 * 14000
c [simplification-13] hard conflict limit 58011 (soft 48011 + delta 10000)
c [simplification-13] new conflict limit 48011 (hard 58011)
c 
c [simplification-14] limit 48011 conflicts (hard 58011) hit after 48013 conflicts
c [quatres-10] found 25289 quaternary clauses 57% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 71 single-self-subsuming ternary resolvents
c [quatres-10-2] added 181 quaternary resolvents
c [ternres-10] limit 9420267 with penalty 0 = 0 + 0
c [ternres-10] all 11854 free variables schedulable
c [ternres-10] 4117 ternary resolvents (44 bin, 4073 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 138 xors of average arity 3.0
c [gauss-4] connected 414 occurrences of 174 variables (average 2.4)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 11854 free variables schedulable
c [simpleprobe-6] limit 37681069 penalty 0 = 0 + 0
c [decomp-42] removed 1 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 1 variables, found 1416 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 806 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 11853 variables 100%
c [block-4] limit of 11775334 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 6 blocked clauses
c [block-4] 6 < 1/100 * 74060 = 740 considered unsuccessful
c [cce-10] limit of 47101336 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 15 (7%) of length 11
c [cce-10-1] eliminated 5 clauses out of 463 (1%) of length 9
c [cce-10-1] eliminated 14 clauses out of 1109 (1%) of length 8
c [cce-10-1] eliminated 24 clauses out of 2072 (1%) of length 7
c [cce-10-1] eliminated 35 clauses out of 4442 (1%) of length 6
c [cce-10-1] eliminated 73 clauses out of 7986 (1%) of length 5
c [cce-10-1] eliminated 109 clauses out of 20386 (1%) of length 4
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 261 large clauses in 47101354 steps
c [cce-10-1] allowing another 23550677 steps for small clauses
c [cce-10-1] scheduling 28730 clauses = 9660 binary + 19070 ternary
c [cce-10-1] tried to eliminate 28730 small clauses 100%
c [cce-10-1] eliminated 7 binary clauses 0%
c [cce-10-1] eliminated 172 ternary clauses 1%
c [cce-10-1] eliminated 179 small clauses 1%
c [cce-10-1] eliminated 179 small clauses in 41956340 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 440 covered clauses in round 1
c [cce-10-2] incomplete large round (ATE)
c [cce-10-2] allowing another 2572533 steps for small clauses
c [cce-10-2] scheduling 28551 clauses = 9653 binary + 18898 ternary
c [cce-10-2] tried to eliminate 3924 small clauses 14%
c [cce-10-2] incomplete small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 440 covered clauses in TOTAL during 2 rounds
c [cce-10] 440 < 1/100 * 74054 = 740 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 11853 variables 100%
c [elim-11] limit of 188405345 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 42 variables 0% in round 1 in 17993055 steps
c [elim-11-1] backward subsumption/strengthening limit 17993000
c [elim-11-1-1] backward checking 332 touched variables 3%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 6 clauses in 203399 steps
c [elim-11-1] rescheduled 27 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 129592 steps
c [elim-11-2] backward subsumption/strengthening limit 129500
c [elim-11-2-1] backward checking 9 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 2 clauses in 42577 steps
c [elim-11-2] rescheduled 5 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 15399 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 43 = 0% variables out of 11853 scheduled
c [elim-11] 43 < 1/100 * 11853 = 118 considered unsuccessful
c [bca-10] limit of 10000000 steps and 147736 added (scaled 2)
c [bca-10] 11836 out of 23622 literals actually usable 50%
c [bca-10] added 22 blocked clauses in 69314 steps
c [phase-count-14] 70193 negative 95.5% of 73511 except 3318 4.5%
c [phase-count-14] 64995 positive 88.4% of 73511 except 8516 11.6%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 2589 enqueued variables after 48013 conflicts
c [score-dist-14] active 9221 (78%), one 0 (0%), zero 2589 (22%)
c [score-dist-14] max exp 531, different 26 (5%)
c [score-dist-14] median active exp 524, avg 522.9
c [simplification-14] removed 44 variables 0.4% (11810 remain 6%)
c [simplification-14] removed 551 irredundant clauses 0.7% (73511 remain 13%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-14] new conflict interval 24000
c [simplification-14] penalized conflict interval 24000 = 1 * 24000
c [simplification-14] hard conflict limit 84013 (soft 72013 + delta 12000)
c [simplification-14] new conflict limit 72013 (hard 84013)
c 
c [simplification-15] limit 72013 conflicts (hard 84013) hit after 72014 conflicts
c [quatres-11] found 25311 quaternary clauses 57% in total
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 56 single-self-subsuming ternary resolvents
c [quatres-11-2] added 63 quaternary resolvents
c [ternres-11] limit 14866423 with penalty 0 = 0 + 0
c [ternres-11] all 11810 free variables schedulable
c [ternres-11] 351 ternary resolvents (27 bin, 324 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 464575 penalty 4 = 4 + 0
c [card-5] found 138 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 464575 for elimination
c [card-5] 138 out of 138 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 410 transitive binary clauses
c [bca-11] limit of 10000000 steps and 147747 added (scaled 2)
c [bca-11] 11501 out of 23622 literals actually usable 49%
c [bca-11] added 9 blocked clauses in 91830 steps
c [sweep-8] limit 1114981 penalty 2 = 2 + 0
c [sweep-8-1] 1561 pos 50.2% + 1548 neg 49.8% = 3109 sched 26.3% ret 8701
c [sweep-8-1] 1122551 steps 98 queries 465.64 avg class size
c [sweep-8-1] 2949 decisions 96 SAT calls 91.78 avg env size
c [sweep-8-1] 2666 variables remain 23% (9144 retained 77%)
c [decomp-44] removed 1 variables
c [sweep-8-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-8] 1 < 1/1000 * 11810 = 11 considered unsuccessful
c [sweep-8] removed 1 vars in TOTAL (1 rounds, 97 queries)
c [phase-count-15] 70190 negative 95.5% of 73509 except 3319 4.5%
c [phase-count-15] 64992 positive 88.4% of 73509 except 8517 11.6%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 2492 enqueued variables after 72014 conflicts
c [score-dist-15] active 9317 (79%), one 0 (0%), zero 2492 (21%)
c [score-dist-15] max exp 532, different 27 (5%)
c [score-dist-15] median active exp 525, avg 523.8
c [simplification-15] removed 1 variables 0.0% (11809 remain 6%)
c [simplification-15] removed 2 irredundant clauses 0.0% (73509 remain 13%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 24000
c [simplification-15] new conflict interval 48000
c [simplification-15] penalized conflict interval 48000 = 1 * 48000
c [simplification-15] hard conflict limit 144014 (soft 120014 + delta 24000)
c [simplification-15] new conflict limit 120014 (hard 144014)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   74.6   11809    73509     73711   31683  33395  6680   71    82   31  86%    667   25   71   38  187%
c -   91.5   11809    73509    102093   33485  33437  6685   69    81   33  85%    793   15   67   48  139%
c 
c [simplification-16] limit 120014 conflicts (hard 144014) hit after 120014 conflicts
c [quatres-12] found 25411 quaternary clauses 57% in total
c [quatres-12-2] added 12 single-self-subsuming ternary resolvents
c [quatres-12-2] added 8 quaternary resolvents
c [ternres-12] limit 25217018 with penalty 0 = 0 + 0
c [ternres-12] all 11809 free variables schedulable
c [ternres-12] 108 ternary resolvents (26 bin, 82 trn)
c [ternres-12] fully completed ternary resolution
c [treelook-6] limit 1260850 penalty 1 = 1 + 0 boost 1
c [treelook-6] scheduled 14540 literals 62%
c [treelook-6] scheduling used 450904 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1260850 penalty 1 = 1 + 0 boost 1
c [treelook-6] used 1263942 steps
c [treelook-6] 13731 literals remain 58%
c [treelook-6] 6163 variables remain to probed next time 52%
c [treelook-6] removed 1 variables, found 1114 hbrs
c [unhide-9] limit 630425 with penalty 3 = 3 + 0
c [unhide-9-9] 0 units, 0 failed, 448 tauts, 0 hbrs, 144815 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 265 transitive binary clauses
c [cce-11] limit of 63042547 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 2 clauses out of 450 (0%) of length 9
c [cce-11-1] eliminated 1 clauses out of 1101 (0%) of length 8
c [cce-11-1] eliminated 10 clauses out of 2040 (0%) of length 7
c [cce-11-1] eliminated 70 clauses out of 4394 (2%) of length 6
c [cce-11-1] eliminated 114 clauses out of 7915 (1%) of length 5
c [cce-11-1] eliminated 2623 clauses out of 20223 (13%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 2820 large clauses in 55650040 steps
c [cce-11-1] allowing another 27825020 steps for small clauses
c [cce-11-1] scheduling 28497 clauses = 9618 binary + 18879 ternary
c [cce-11-1] tried to eliminate 28497 small clauses 100%
c [cce-11-1] eliminated 171 binary clauses 2%
c [cce-11-1] eliminated 295 ternary clauses 2%
c [cce-11-1] eliminated 466 small clauses 2%
c [cce-11-1] eliminated 466 small clauses in 50168477 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] completed small and large (ACCE)
c [cce-11-1] eliminated 3286 covered clauses in round 1
c [cce-11-2] eliminated 2 clauses out of 2030 (0%) of length 7
c [cce-11-2] incomplete large round (ACCE)
c [cce-11-2] eliminated 2 large clauses in 12874071 steps
c [cce-11-2] allowing another 6437035 steps for small clauses
c [cce-11-2] scheduling 28031 clauses = 9447 binary + 18584 ternary
c [cce-11-2] tried to eliminate 8337 small clauses 30%
c [cce-11-2] eliminated 1 binary clauses 0%
c [cce-11-2] eliminated 2 ternary clauses 0%
c [cce-11-2] eliminated 3 small clauses 0%
c [cce-11-2] eliminated 3 small clauses in 12874130 steps
c [cce-11-2] incomplete small round (ACCE)
c [cce-11-2] eliminated 5 covered clauses in round 2
c [cce-11] eliminated 3291 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 11808 variables 100%
c [elim-12] limit of 252170189 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 419 variables 4% in round 1 in 17365035 steps
c [elim-12-1] backward subsumption/strengthening limit 17365000
c [elim-12-1-1] backward checking 2676 touched variables 23%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 2 and strengthened 14 clauses in 891006 steps
c [elim-12-1] rescheduled 75 variables 1% by backward subsumption
c [elim-12-2] eliminated 2 variables 0% in round 2 in 242861 steps
c [elim-12-2] backward subsumption/strengthening limit 242800
c [elim-12-2-1] backward checking 24 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 2 and strengthened 5 clauses in 67389 steps
c [elim-12-2] rescheduled 9 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 24481 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 421 = 4% variables out of 11808 scheduled
c [bca-12] limit of 10000000 steps and 139434 added (scaled 2)
c [bca-12] 11628 out of 22776 literals actually usable 51%
c [bca-12] added 88 blocked clauses in 76048 steps
c [phase-count-16] 66543 negative 95.9% of 69352 except 2809 4.1%
c [phase-count-16] 61155 positive 88.2% of 69352 except 8197 11.8%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 2315 enqueued variables after 120014 conflicts
c [score-dist-16] active 9072 (80%), one 0 (0%), zero 2315 (20%)
c [score-dist-16] max exp 534, different 29 (5%)
c [score-dist-16] median active exp 526, avg 524.9
c [simplification-16] removed 422 variables 3.6% (11387 remain 6%)
c [simplification-16] removed 4157 irredundant clauses 5.7% (69352 remain 13%)
c [simplification-16] maximum reduction of 6% = max (4%, 6%)
c [simplification-16] large reduction 6% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 132014 (soft 122014 + delta 10000)
c [simplification-16] new conflict limit 122014 (hard 132014)
c 
c [simplification-17] limit 122014 conflicts (hard 132014) hit after 122014 conflicts
c [quatres-13] found 22005 quaternary clauses 53% in total
c [quatres-13-1] removed 3 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 63 single-self-subsuming ternary resolvents
c [quatres-13-2] added 150 quaternary resolvents
c [ternres-13] limit 25638048 with penalty 0 = 0 + 0
c [ternres-13] all 11387 free variables schedulable
c [ternres-13] 414 ternary resolvents (12 bin, 402 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-6] limit 128190242 penalty 0 = 0 + 0
c [basicprobe-6-0] 5444 sched 48%, 10 failed, 0 lifted, 322 hbrs
c [decomp-48] removed 10 variables
c [basicprobe-6-1] 5432 sched 48%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-6-2] 5429 sched 48%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-2] fully completed probing
c [basicprobe-6-2] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-6-2] removed 10 variables, found 342 hbrs
c [bate-4] eliminated 17 asymmetric tautologies during probing
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 199 transitive binary clauses
c [cce-12] limit of 128190242 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 45 (2%) of length 10
c [cce-12-1] eliminated 4 clauses out of 520 (1%) of length 9
c [cce-12-1] eliminated 26 clauses out of 1277 (2%) of length 8
c [cce-12-1] eliminated 22 clauses out of 2270 (1%) of length 7
c [cce-12-1] eliminated 34 clauses out of 4433 (1%) of length 6
c [cce-12-1] eliminated 72 clauses out of 7897 (1%) of length 5
c [cce-12-1] eliminated 101 clauses out of 17180 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 260 large clauses in 42858354 steps
c [cce-12-1] allowing another 21429177 steps for small clauses
c [cce-12-1] scheduling 17541 clauses = 9177 binary + 8364 ternary
c [cce-12-1] tried to eliminate 17541 small clauses 100%
c [cce-12-1] eliminated 368 ternary clauses 4%
c [cce-12-1] eliminated 368 small clauses 2%
c [cce-12-1] eliminated 368 small clauses in 31619244 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 628 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 21199422 steps for small clauses
c [cce-12-2] scheduling 17173 clauses = 9177 binary + 7996 ternary
c [cce-12-2] tried to eliminate 17173 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 628 covered clauses in TOTAL during 2 rounds
c [cce-12] 628 < 1/100 * 69293 = 692 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 11377 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 46 variables 0% in round 1 in 16787575 steps
c [elim-13-1] backward subsumption/strengthening limit 16787500
c [elim-13-1-1] backward checking 405 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 1 clauses in 233193 steps
c [elim-13-1] rescheduled 6 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 20601 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 46 = 0% variables out of 11377 scheduled
c [elim-13] 46 < 1/100 * 11377 = 113 considered unsuccessful
c [bca-13] limit of 10000000 steps and 137944 added (scaled 2)
c [bca-13] 11484 out of 22664 literals actually usable 51%
c [bca-13] added 19 blocked clauses in 75851 steps
c [phase-count-17] 65856 negative 96.0% of 68585 except 2729 4.0%
c [phase-count-17] 60461 positive 88.2% of 68585 except 8124 11.8%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 2304 enqueued variables after 122014 conflicts
c [score-dist-17] active 9027 (80%), one 0 (0%), zero 2304 (20%)
c [score-dist-17] max exp 534, different 29 (5%)
c [score-dist-17] median active exp 526, avg 524.9
c [simplification-17] removed 56 variables 0.5% (11331 remain 6%)
c [simplification-17] removed 767 irredundant clauses 1.1% (68585 remain 13%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 24000 = 48000 / 2
c [simplification-17] new conflict interval 72000
c [simplification-17] penalized conflict interval 72000 = 1 * 72000
c [simplification-17] hard conflict limit 230014 (soft 194014 + delta 36000)
c [simplification-17] new conflict limit 194014 (hard 230014)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  123.7   11331    68585    142308   33674  31127  7278   72    84   32  86%    899   10   72   59  121%
c -  141.6   11331    68585    170966   32336  31144  7283   80    85   32  95%    943    7   76   66  116%
c 
c [simplification-18] limit 194014 conflicts (hard 230014) hit after 194015 conflicts
c [quatres-14] found 21958 quaternary clauses 53% in total
c [quatres-14-2] added 31 single-self-subsuming ternary resolvents
c [quatres-14-2] added 31 quaternary resolvents
c [ternres-14] limit 42085294 with penalty 0 = 0 + 0
c [ternres-14] all 11331 free variables schedulable
c [ternres-14] 172 ternary resolvents (17 bin, 155 trn)
c [ternres-14] fully completed ternary resolution
c [simpleprobe-7] all 11331 free variables schedulable
c [simpleprobe-7] limit 168341178 penalty 0 = 0 + 0
c [decomp-51] removed 1 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 1 variables, found 1427 hbrs, 1 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 792 transitive binary clauses
c [bca-14] limit of 10000000 steps and 137947 added (scaled 2)
c [bca-14] 11557 out of 22662 literals actually usable 51%
c [bca-14] added 15 blocked clauses in 90258 steps
c [phase-count-18] 65852 negative 96.0% of 68582 except 2730 4.0%
c [phase-count-18] 60458 positive 88.2% of 68582 except 8124 11.8%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 2272 enqueued variables after 194015 conflicts
c [score-dist-18] active 9058 (80%), one 0 (0%), zero 2272 (20%)
c [score-dist-18] max exp 535, different 30 (6%)
c [score-dist-18] median active exp 527, avg 525.7
c [simplification-18] removed 1 variables 0.0% (11330 remain 6%)
c [simplification-18] removed 3 irredundant clauses 0.0% (68582 remain 13%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 72000
c [simplification-18] new conflict interval 144000
c [simplification-18] penalized conflict interval 144000 = 1 * 144000
c [simplification-18] hard conflict limit 410015 (soft 338015 + delta 72000)
c [simplification-18] new conflict limit 338015 (hard 410015)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  160.7   11330    68582    201820   33657  31331  7943   73    80   33  92%    973    1   76   69  110%
c -  178.0   11330    68582    232554   33543  31357  7943   74    82   33  90%    992    2   74   70  105%
c -  193.6   11330    68582    264650   34361  31407  7943   70    81   33  86%   1005    1   74   68  110%
c -  212.7   11330    68582    297101   35435  31431  7943   65    83   33  78%   1012    2   62   69   90%
c -  229.8   11330    68582    329531   36082  31451  7946   67    81   33  83%   1017   -0   72   68  106%
c 
c [simplification-19] limit 338015 conflicts (hard 410015) hit after 352903 conflicts
c [quatres-15] found 22161 quaternary clauses 52% in total
c [quatres-15-2] added 31 single-self-subsuming ternary resolvents
c [quatres-15-2] added 6 quaternary resolvents
c [ternres-15] limit 73505180 with penalty 0 = 0 + 0
c [ternres-15] all 11330 free variables schedulable
c [ternres-15] 114 ternary resolvents (22 bin, 92 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 918814 penalty 4 = 4 + 0
c [gauss-5] extracted 490 xors of average arity 3.0
c [gauss-5] connected 1468 occurrences of 373 variables (average 3.9)
c [gauss-5] limit 918814 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-52] removed 1 variables
c [treelook-7] limit 7350518 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 13963 literals 62%
c [treelook-7] scheduling used 447353 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 7350518 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5353808 steps
c [treelook-7] fully completed tree based probing
c [decomp-53] removed 4 variables
c [treelook-7] removed 6 variables, found 1896 hbrs
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 581 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 11323 variables 100%
c [block-5] limit of 45940737 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 1837629500 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 1 clauses out of 19 (5%) of length 11
c [cce-13-1] eliminated 2 clauses out of 539 (0%) of length 9
c [cce-13-1] eliminated 7 clauses out of 1256 (1%) of length 8
c [cce-13-1] eliminated 21 clauses out of 2232 (1%) of length 7
c [cce-13-1] eliminated 117 clauses out of 4406 (3%) of length 6
c [cce-13-1] eliminated 249 clauses out of 7820 (3%) of length 5
c [cce-13-1] eliminated 213 clauses out of 17048 (1%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 610 large clauses in 49804865 steps
c [cce-13-1] allowing another 24902432 steps for small clauses
c [cce-13-1] scheduling 17108 clauses = 9133 binary + 7975 ternary
c [cce-13-1] tried to eliminate 17108 small clauses 100%
c [cce-13-1] eliminated 40 binary clauses 0%
c [cce-13-1] eliminated 949 ternary clauses 12%
c [cce-13-1] eliminated 989 small clauses 6%
c [cce-13-1] eliminated 989 small clauses in 38421417 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 1599 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 4289 (0%) of length 6
c [cce-13-2] eliminated 8 clauses out of 7571 (0%) of length 5
c [cce-13-2] eliminated 5 clauses out of 16835 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 14 large clauses in 48035725 steps
c [cce-13-2] allowing another 24017862 steps for small clauses
c [cce-13-2] scheduling 16119 clauses = 9093 binary + 7026 ternary
c [cce-13-2] tried to eliminate 16119 small clauses 100%
c [cce-13-2] eliminated 10 binary clauses 0%
c [cce-13-2] eliminated 71 ternary clauses 1%
c [cce-13-2] eliminated 81 small clauses 1%
c [cce-13-2] eliminated 81 small clauses in 36331161 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 95 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 23957797 steps for small clauses
c [cce-13-3] scheduling 16038 clauses = 9083 binary + 6955 ternary
c [cce-13-3] tried to eliminate 16038 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 0 covered clauses in round 3
c [cce-13] eliminated 1694 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 11323 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 257 variables 2% in round 1 in 16556920 steps
c [elim-14-1] backward subsumption/strengthening limit 16556900
c [elim-14-1-1] backward checking 1729 touched variables 15%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 3 clauses in 621716 steps
c [elim-14-1] rescheduled 14 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 10353 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 257 = 2% variables out of 11323 scheduled
c [bca-15] limit of 10000000 steps and 133633 added (scaled 2)
c [bca-15] 11034 out of 22134 literals actually usable 50%
c [bca-15] added 48 blocked clauses in 72062 steps
c [sweep-9] limit 2756444 penalty 3 = 3 + 0
c [sweep-9-1] 1272 pos 51.5% + 1198 neg 48.5% = 2470 sched 22.3% ret 8596
c [sweep-9-1] 2764235 steps 386 queries 143.30 avg class size
c [sweep-9-1] 10065 decisions 382 SAT calls 56.60 avg env size
c [sweep-9-1] 980 variables remain 9% (10086 retained 91%)
c [decomp-54] removed 2 variables
c [sweep-9-1] removed 2 vars (0 failed, 3 eqs, 6 impls)
c [sweep-9] 2 < 1/1000 * 11066 = 11 considered unsuccessful
c [sweep-9] removed 2 vars in TOTAL (1 rounds, 385 queries)
c [sort-queue-19] sorted 2011 enqueued variables after 352903 conflicts
c [score-dist-19] active 9053 (82%), one 0 (0%), zero 2011 (18%)
c [score-dist-19] max exp 537, different 32 (6%)
c [score-dist-19] median active exp 528, avg 527.0
c [simplification-19] removed 266 variables 2.3% (11064 remain 6%)
c [simplification-19] removed 2163 irredundant clauses 3.2% (66419 remain 12%)
c [simplification-19] maximum reduction of 3% = max (2%, 3%)
c [simplification-19] geometric conflict interval increment 36000 = 144000 / 4
c [simplification-19] new conflict interval 180000
c [simplification-19] penalized conflict interval 180000 = 1 * 180000
c [simplification-19] hard conflict limit 622903 (soft 532903 + delta 90000)
c [simplification-19] new conflict limit 532903 (hard 622903)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  265.1   11064    66419    383451   37362  30723  9054   71    80   32  89%   1021   -0   74   68  109%
c -  284.1   11064    66419    416569   38135  30739  9054   69    83   32  83%   1022    3   71   68  104%
c -  302.2   11064    66419    450213   38547  30749  9056   54    80   38  68%   1023   -1   34   67   51%
c -  322.3   11064    66419    484549   37782  30760  9057   72    80   38  89%   1023   -0   77   67  115%
c -  343.3   11064    66419    520589   39188  30771  9057   71    83   39  86%   1024    3   69   68  102%
c 
c [simplification-20] limit 532903 conflicts (hard 622903) hit after 533290 conflicts
c [quatres-16] found 21633 quaternary clauses 50% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 81 single-self-subsuming ternary resolvents
c [quatres-16-2] added 28 quaternary resolvents
c [ternres-16] limit 110239178 with penalty 0 = 0 + 0
c [ternres-16] all 11064 free variables schedulable
c [ternres-16] 275 ternary resolvents (24 bin, 251 trn)
c [ternres-16] fully completed ternary resolution
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 5005 sched 45%, 6 failed, 0 lifted, 377 hbrs
c [decomp-56] removed 6 variables
c [basicprobe-7-1] 4976 sched 45%, 0 failed, 0 lifted, 126 hbrs
c [basicprobe-7-2] 4976 sched 45%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-7-3] 4975 sched 45%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-4] 4973 sched 45%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-4] fully completed probing
c [basicprobe-7-4] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-7-4] removed 6 variables, found 512 hbrs
c [bate-5] eliminated 13 asymmetric tautologies during probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 397 transitive binary clauses
c [cce-14] limit of 551195891 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 61 (2%) of length 10
c [cce-14-1] eliminated 5 clauses out of 551 (1%) of length 9
c [cce-14-1] eliminated 46 clauses out of 1342 (3%) of length 8
c [cce-14-1] eliminated 10 clauses out of 2290 (0%) of length 7
c [cce-14-1] eliminated 40 clauses out of 4485 (1%) of length 6
c [cce-14-1] eliminated 35 clauses out of 7563 (0%) of length 5
c [cce-14-1] eliminated 47 clauses out of 16439 (0%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 184 large clauses in 40600908 steps
c [cce-14-1] allowing another 20300454 steps for small clauses
c [cce-14-1] scheduling 15768 clauses = 8905 binary + 6863 ternary
c [cce-14-1] tried to eliminate 15768 small clauses 100%
c [cce-14-1] eliminated 5 binary clauses 0%
c [cce-14-1] eliminated 35 ternary clauses 1%
c [cce-14-1] eliminated 40 small clauses 0%
c [cce-14-1] eliminated 40 small clauses in 28941108 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 224 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 20224380 steps for small clauses
c [cce-14-2] scheduling 15728 clauses = 8900 binary + 6828 ternary
c [cce-14-2] tried to eliminate 15728 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 224 covered clauses in TOTAL during 2 rounds
c [cce-14] 224 < 1/100 * 66363 = 663 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 11058 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 27 variables 0% in round 1 in 16121977 steps
c [elim-15-1] backward subsumption/strengthening limit 16121900
c [elim-15-1-1] backward checking 275 touched variables 2%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 140642 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 27 = 0% variables out of 11058 scheduled
c [elim-15] 27 < 1/100 * 11058 = 110 considered unsuccessful
c [bca-16] limit of 10000000 steps and 132981 added (scaled 2)
c [bca-16] 10771 out of 22064 literals actually usable 49%
c [bca-16] added 21 blocked clauses in 83890 steps
c [sort-queue-20] sorted 1967 enqueued variables after 533290 conflicts
c [score-dist-20] active 9064 (82%), one 0 (0%), zero 1967 (18%)
c [score-dist-20] max exp 538, different 33 (6%)
c [score-dist-20] median active exp 529, avg 527.9
c [simplification-20] removed 33 variables 0.3% (11031 remain 6%)
c [simplification-20] removed 336 irredundant clauses 0.5% (66083 remain 12%)
c [simplification-20] maximum reduction of 1% = max (0%, 1%)
c [simplification-20] geometric conflict interval increment 90000 = 180000 / 2
c [simplification-20] new conflict interval 270000
c [simplification-20] penalized conflict interval 270000 = 1 * 270000
c [simplification-20] hard conflict limit 938290 (soft 803290 + delta 135000)
c [simplification-20] new conflict limit 803290 (hard 938290)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  369.2   11031    66083    556996   39012  30606  8907   76    80   32  95%   1024   -1   75   70  108%
c -  389.9   11031    66083    593884   39672  30624  8908   66    78   32  84%   1024   -1   73   67  109%
c -  410.8   11031    66083    631151   39923  30636  8908   72    81   40  88%   1024    2   73   68  107%
c -  434.8   11031    66083    669137   40898  30643  8908   72    78   41  92%   1024   -1   72   70  102%
c -  456.8   11031    66083    707557   42146  30668  8911   67    81   41  83%   1024    2   68   68  100%
c -  480.1   11031    66083    745511   42788  30674  8912   76    79   42  97%   1024   -0   76   71  108%
c -  502.2   11031    66083    783961   43604  30682  8913   66    79   41  84%   1024   -0   69   70   99%
c 
c [simplification-21] limit 803290 conflicts (hard 938290) hit after 803291 conflicts
c [quatres-17] found 21650 quaternary clauses 50% in total
c [quatres-17-2] added 37 single-self-subsuming ternary resolvents
c [quatres-17-2] added 35 quaternary resolvents
c [ternres-17] limit 167424290 with penalty 0 = 0 + 0
c [ternres-17] all 11031 free variables schedulable
c [ternres-17] 126 ternary resolvents (24 bin, 102 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 5232009 penalty 4 = 4 + 0
c [card-6] found 243 at-most-one constraints of average size 3.0
c [card-6] found 56 at-most-two constraints of average size 4.0
c [card-6] using previous limit 5232009 for elimination
c [card-6] 298 out of 299 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 50 at-most-one constraints, 4 used 8%
c [card-6] exported 4 binary clauses, 1.0 per/constraint
c [simpleprobe-8] all 11031 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-61] removed 3 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 3 variables, found 1594 hbrs, 0 units
c [unhide-10] limit 1250000 with penalty 4 = 4 + 0
c [unhide-10-10] 0 units, 0 failed, 2525 tauts, 0 hbrs, 290140 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 662 transitive binary clauses
c [bca-17] limit of 10000000 steps and 132983 added (scaled 2)
c [bca-17] 10741 out of 22058 literals actually usable 49%
c [bca-17] added 18 blocked clauses in 95173 steps
c [sort-queue-21] sorted 1899 enqueued variables after 803291 conflicts
c [score-dist-21] active 9129 (83%), one 0 (0%), zero 1899 (17%)
c [score-dist-21] max exp 540, different 35 (6%)
c [score-dist-21] median active exp 531, avg 528.9
c [simplification-21] removed 3 variables 0.0% (11028 remain 6%)
c [simplification-21] removed 4 irredundant clauses 0.0% (66079 remain 12%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 270000
c [simplification-21] new conflict interval 540000
c [simplification-21] penalized conflict interval 540000 = 1 * 540000
c [simplification-21] hard conflict limit 1613291 (soft 1343291 + delta 270000)
c [simplification-21] new conflict limit 1343291 (hard 1613291)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  526.0   11028    66079    822904   42132  29388  8852   69    77   34  90%   1024   -1   71   70  102%
c -  549.5   11028    66079    864217   43675  29393  8853   70    74   36  95%   1024   -4   72   70  102%
c -  572.1   11028    66079    904894   44286  29400  8853   68    75   43  90%   1024   -1   65   69   94%
c -  596.8   11028    66079    946125   44629  29402  8853   71    76   44  94%   1024    0   74   69  107%
c -  621.8   11028    66079    988468   44532  29405  8853   69    72   44  95%   1024   -2   69   69  100%
c -  642.4   11028    66079   1031880   45517  29430  8853   59    74   43  80%   1024   -0   65   63  102%
c -  664.6   11028    66079   1075801   46485  29460  8854   54    86   42  63%   1024   12   65   62  106%
c -  690.3   11028    66079   1119667   47375  29481  8856   65    73   43  89%   1024   -3   66   63  105%
c -  713.2   11028    66079   1164236   47705  29520  8856   53    83   41  64%   1024    5   60   59  103%
c -  736.5   11028    66079   1209854   48241  29548  8858   57    84   41  68%   1024    4   61   57  107%
c -  763.8   11028    66079   1255980   48527  29558  8860   63    83   42  76%   1024    2   60   59  101%
c -  793.1   11028    66079   1302864   49763  29564  8860   66    83   43  79%   1024    1   69   61  112%
c -  824.8   11028    66079   1349576   49697  29566  8860   70    80   43  87%   1024   -1   67   63  106%
c -  861.0   11028    66079   1398313   50080  29569  8861   65    76   43  86%   1024   -3   66   64  104%
c 
c [simplification-22] limit 1343291 conflicts (hard 1613291) hit after 1431605 conflicts
c [quatres-18] found 22022 quaternary clauses 49% in total
c [quatres-18-1] removed 4 duplicate quaternary clauses
c [quatres-18-2] added 68 single-self-subsuming ternary resolvents
c [quatres-18-2] added 103 quaternary resolvents
c [ternres-18] limit 200000000 with penalty 0 = 0 + 0
c [ternres-18] all 11028 free variables schedulable
c [ternres-18] 1016 ternary resolvents (19 bin, 997 trn)
c [ternres-18] fully completed ternary resolution
c [treelook-8] limit 30020077 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 22056 literals 100%
c [treelook-8] scheduling used 627496 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 30020077 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 5724177 steps
c [treelook-8] fully completed tree based probing
c [decomp-63] removed 5 variables
c [treelook-8] removed 14 variables, found 1367 hbrs
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 527 transitive binary clauses
c [cce-15] limit of 750501933 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 1 clauses out of 15 (7%) of length 11
c [cce-15-1] eliminated 1 clauses out of 65 (2%) of length 10
c [cce-15-1] eliminated 2 clauses out of 355 (1%) of length 9
c [cce-15-1] eliminated 1 clauses out of 971 (0%) of length 8
c [cce-15-1] eliminated 13 clauses out of 2548 (1%) of length 7
c [cce-15-1] eliminated 63 clauses out of 4283 (1%) of length 6
c [cce-15-1] eliminated 74 clauses out of 7461 (1%) of length 5
c [cce-15-1] eliminated 88 clauses out of 16455 (1%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 243 large clauses in 45833057 steps
c [cce-15-1] allowing another 22916528 steps for small clauses
c [cce-15-1] scheduling 15818 clauses = 8898 binary + 6920 ternary
c [cce-15-1] tried to eliminate 15818 small clauses 100%
c [cce-15-1] eliminated 53 binary clauses 1%
c [cce-15-1] eliminated 63 ternary clauses 1%
c [cce-15-1] eliminated 116 small clauses 1%
c [cce-15-1] eliminated 116 small clauses in 34565438 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 359 covered clauses in round 1
c [cce-15-2] eliminated 2 clauses out of 4220 (0%) of length 6
c [cce-15-2] eliminated 2 clauses out of 16367 (0%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 4 large clauses in 45274250 steps
c [cce-15-2] allowing another 22637125 steps for small clauses
c [cce-15-2] scheduling 15702 clauses = 8845 binary + 6857 ternary
c [cce-15-2] tried to eliminate 15702 small clauses 100%
c [cce-15-2] eliminated 1 ternary clauses 0%
c [cce-15-2] eliminated 1 small clauses 0%
c [cce-15-2] eliminated 1 small clauses in 34190457 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 5 covered clauses in round 2
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] allowing another 22637118 steps for small clauses
c [cce-15-3] scheduling 15701 clauses = 8845 binary + 6856 ternary
c [cce-15-3] tried to eliminate 15701 small clauses 100%
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 0 covered clauses in round 3
c [cce-15] eliminated 364 covered clauses in TOTAL during 3 rounds
c [cce-15] 364 < 1/100 * 66010 = 660 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 11014 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 113 variables 1% in round 1 in 15603008 steps
c [elim-16-1] backward subsumption/strengthening limit 15603000
c [elim-16-1-1] backward checking 893 touched variables 8%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 1 clauses in 367648 steps
c [elim-16-1] rescheduled 7 variables 0% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 45125 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 113 = 1% variables out of 11014 scheduled
c [bca-18] limit of 10000000 steps and 131778 added (scaled 2)
c [bca-18] 9657 out of 21804 literals actually usable 44%
c [bca-18] added 25 blocked clauses in 109108 steps
c [sort-queue-22] sorted 1395 enqueued variables after 1431605 conflicts
c [score-dist-22] active 9506 (87%), one 0 (0%), zero 1395 (13%)
c [score-dist-22] max exp 541, different 36 (7%)
c [score-dist-22] median active exp 535, avg 531.7
c [simplification-22] removed 127 variables 1.2% (10901 remain 6%)
c [simplification-22] removed 607 irredundant clauses 0.9% (65472 remain 12%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 270000 = 540000 / 2
c [simplification-22] new conflict interval 810000
c [simplification-22] penalized conflict interval 810000 = 1 * 810000
c [simplification-22] hard conflict limit 2646605 (soft 2241605 + delta 405000)
c [simplification-22] new conflict limit 2241605 (hard 2646605)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  896.6   10901    65472   1451852   52379  29726  8738   33   127   35  26%   1024   32   35   56   62%
c -  923.3   10901    65472   1501282   53251  29760  8739   67    82   35  82%   1024  -14   69   55  124%
c -  962.4   10901    65472   1551398   52852  29781  8741   56    90   44  62%   1024   -1   39   60   65%
c -  998.7   10901    65472   1603867   52649  29799  8742   59    86   45  68%   1024   -3   74   59  126%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 706 basic ate = 314 trn 44% + 392 lrg 56% in 5 updates
c bcas: 18 count, 694 added (230 skipped), 1362425 steps
c bkwd: tried 69203 clauses, 138282 lits, 2.00 lits/clause
c bkwd: checked 2287142 occs, 33.05 occs/clause, 16.54 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 31 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 145 large (0% self)
c blkd: 5 bces, 680 removed, 2537839 resolutions, 6579940 steps
c blkd: 6762 blocking literals 2%, 5 pure
c bump: 1606921 bumped seen, 780136884 lits 485.5 on average
c card: 6 count, 0 units, 6 am1, 15806457 steps
c card: 25 rescheduled, 234 eliminated, 51874 resolved, 10303 subsumed
c card: 2024 at-most-one constraints found, average size 3.00
c card: 2024 at-most-one constraints used 100%, average size 3.00
c card: 68 at-most-two constraints found, average size 4.00
c card: 67 at-most-two constraints used 99%, average size 4.00
c cces: 15 cces, 46178 eliminated, 37154 ate 80%, 9024 abce 20%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1823044 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 126 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 63 decompositions, 12775 equivalent 7%
c deco: 67 decision-only clauses 0%, 65% reduction
c decs: 3825093 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 159161 eliminated 87%, 30 pure 0%
c elms: 27 rounds, 1.7 rounds/bve
c elms: 155155 small 97%, 3971 large 2%
c elms: 167194 tried small, 155155 succeeded 93%, 12039 failed 7%
c elms: 25946 subsumed, 48007 strengthened, 738 blocked
c elms: 5819238 copies, 7918429 resolutions, 2732432 ipos
c elms: 2322553 subchks, 1627833 strchks
c gaus: 5 extractions, 1746 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9340316 steps, 4670158 extr 50%, 74847 elim 1%
c glue: 64.5 orig avg, 64.5 real avg, 8.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 45844 = 21975 simple 48% + 21938 trn 48% + 1931 lrg 4%, 2370 sub 5%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1606920 clauses, 136.9 length
c lrnd: 219914715 lits = 430906195 orig - 210991480 removed 49%
c lrnd: 281856 uips 18%, 1063677 flips 66%
c mins: 1604132 mins 100%, 194 bin 0%, 2527 size 0%
c mins: 718191482 poisoned searches, 48611282 hits, 7% hit rate
c mins: 1098850000 used twice searches, 54394956 hits, 5% hit rate
c move: moved 25422, 2821 bin 11%, 22601 trn 89%
c otfs: 1020 driving 21%, 3927 restarting 79%
c otfs: str 4947, 4546 red 92%, 401 irr 8%
c otfs: str 4947, 0 bin 0%, 155 trn 3%, 4792 lrg 97%
c otfs: sub 75, 60 red 80%, 15 irr 20%
c otfs: sub 75, 0 bin 0%, 14 trn 19%, 61 lrg 81%
c phas: 18 computed, 22947 set, 6066 pos (26%), 16881 neg (74%)
c prbs: 7 basic, 247880 probed, 205 failed, 1 lifted
c prbs: 8 simple, 452137 probed, 6 failed, 20255 eqs
c prbs: 8 treelook, 38026 probed, 21 failed, 0 lifted
c prom: 51887 locked 1% out of 4569180 tried
c prps: 2061484662 props, 538 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 18 count, 8172 quat, 3568 self1, 69 self2, 69 dup
c queu: 22 sorted, 3825093 next (192167 steps 0.05)
c queu: 780437521 enq (1514640529 steps 1.94), 780136884 deq 100%
c redc: 2851 clauses 13%, 22486 tried 1%, 2 sat 0%
c redc: 3607 lits 2%, 222568 tried 0%, 2 sat 0%
c redc: 115 times jump level reduced, 14.2 levels on average
c reds: 39 count, 41172.8 conflicts per reduce
c reds: 0 memlim 0%, 39 arith 100%
c reds: 1345695 collected 92%, 122786 retired 8%
c rmbd: 4923 removed, 2063 red 42%
c rsts: 9540 restarts 72%, 3697 skipped 28%
c rsts: 3697 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 22 count, 22 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1606920 count (5579886 tried 3.5), 30945 sub out of 1604379 (1.9%)
c swps: 9 count, 10 rounds, 3242 queries (324.2/round)
c swps: 3190 sat calls, 57 unsat (0.7% success rate)
c swps: 64193 decisions 20.1, 2202 conflicts 0.7
c swps; 522.7 avg class size, 41.9 avg environment size
c swps: 0 failed, 244 impls, 109 equivs
c swp0: 1076 type 0 queries, 139 unsat (12.9%), 1047 sat (97.3%)
c swp1: 2166 type 1 queries, 504 unsat (23.3%), 2086 sat (96.3%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 10864469 calls to obtain time
c tops: 488 fixed 0%, 3 its, 535246.33 confs/it
c trds: 18 transitive reductions, 12915 removed, 29 failed
c trds: 460803 nodes, 326720 edges, 8500692 steps
c trim: 320787 words, 1.2 MB
c trnr: 18 count, 1910 bin, 78490 trn, 111556276 steps
c unhd: 10 count, 10 rounds, 12221404 steps
c unhd: 54 non-trivial sccs of average size 2.0
c unhd: 18 units, 18 bin, 0 trn, 0 lrg
c unhd: 198 failed, 191 stamp, 0 lits, 1 bin, 6 trn, 0 lrg
c unhd: 28289 tauts, 200 bin 1%, 18686 trn 66%, 5436 lrg 19%
c unhd: 28289 tauts, 3967 stamp 14%, 20984 red 74%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 647582 str, 18 bin 0%, 6031 trn 1%, 641533 lrg 99%, 571874 red 88%
c vars: 10901 remaining 6% and 172424 removed 94% out of 183325
c vars: 488 fixed 0%, 159161 eliminated 87%, 12775 equivalent 7%
c vsts: 33262643162 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 16.1 search visits per propagation, 20675.5 per conflict
c wchs: 3344813716 pushed, 21090744 enlarged, 211 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1612551       1345695        122786     155569544      56378023        779238
c 
c  0 0         23283   1       625   0         0   0 102503100  66  28615519  51    147183  19     0.6
c  1 5          5288   0       969   0      2109   2   9867495   6<  4231927   8     22060   3     0.2
c  2 6         18193   1      7393   1      5527   5  15249128  10   6594819  12<    47875   6     1.0
c  3 9         30311   2     13247   1     10183   8  11646957   7   6097709  11     67471   9     1.2
c  4 14        43851   3     22984   2     14356  12   6074377   4   3298148   6     58373   7     1.3
c  5 21        45308   3     30018   2      8794   7   3230169   2   1964566   3     54990   7<    1.9
c  6 30        81563   5     59541   4     14410  12   1792243   1   1231745   2     63276   8     3.4
c  7 41        87173   5     72755   5      7755   6<  1173006   1    875532   2     61028   8     4.5
c  8 54       257740  16<   235552  18<    12875  10   1877988   1   1550471   3    144019  18    11.3
c  9 69       990005  61    876100  65     46051  38   2106566   1   1878554   3    111231  14    26.0
c 10 86        29821   2     26506   2       721   1     48480   0     39025   0      1731   0     6.4
c 11 126          15   0         5   0         5   0        35   0         8   0         1   0     0.0
c 
c avg                  8.0           8.3           6.6           1.1           1.8           4.9
c std                  1.9           1.4           2.5           1.9           2.5           3.2
c 
c  159.570  16% bump
c   20.947   2% cce
c    9.013   1% elim
c    7.632   1% probe
c    3.408   0% unhide
c 
c   10.501 < 1% rest (below)
c 
c    2.492   0% decide
c    1.888   0% sweep
c    1.425   0% bca
c    1.374   0% quatres
c    1.176   0% ternres
c    0.698   0% block
c    0.637   0% transred
c    0.415   0% card
c    0.397   0% gauss
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.449   0% preprocessing     8%
c   48.800   5% inprocessing     92%
c ==================================
c   53.248   5% simplifying
c  946.478  95% search
c ==================================
c  999.729 100% all
c 
c       1605739 conflicts,        1606.2 confs/sec
c          1601 ternaries,        1003.0 confs/ternary
c           232 binaries,         6921.3 confs/binary
c             3 iterations,     535246.3 confs/iteration
c 
c            39 reductions,          0.0 redus/sec,  41172.8 confs/reduction
c          9540 restarts,            9.5 rests/sec,    168.3 confs/restart
c       3825093 decisions,        3826.1 decis/sec,      2.4 decis/conflict
c    2061484662 propagations,  2062043.2 props/sec,    538.9 props/decision
c 
c 999.7 seconds, 103.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
