c launch: /data/cnf/sc2014/app/6s13-opt.cnf.bz2
c host: atom14
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/6s13-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s13-opt.cnf.bz2
c no embedded options
c found 'p cnf 52436 153557' header
c read 52436 variables, 153557 clauses, 358297 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=5
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 51981 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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   51981   151783         0       0      0     0    0     0    9   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 83 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] 83 out of 83 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 57 at-most-one constraints, 57 used 100%
c [card-1] exported 61 binary clauses, 1.1 per/constraint
c [decomp-1] removed 888 variables
c [simpleprobe-1] all 51538 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 1183 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1183 variables, found 2119 hbrs, 156 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 8 tauts, 0 hbrs, 11 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 50355 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 37049 variables 74% in round 1 in 10576975 steps
c [elim-1-1] backward subsumption/strengthening limit 9423025
c [elim-1-1-1] backward checking 36067 touched variables 72%
c [elim-1-1-1] incomplete backward checking 35910 remain 100%
c [elim-1-1] subsumed 8 and strengthened 128 clauses in 9425504 steps
c [elim-1] incomplete 313 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 37051 = 74% variables out of 50355 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 66921 negative 90.6% of 73865 except 6944 9.4%
c [phase-count-1] 62289 positive 84.3% of 73865 except 11576 15.7%
c [phase-1] phase bias: 3169 positive 24%, 10135 negative 76%
c [sort-queue-1] sorted 13304 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 13304 (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 38677 variables 74.4% (13304 remain 26%)
c [simplification-1] removed 77918 irredundant clauses 51.3% (73865 remain 49%)
c [simplification-1] maximum reduction of 74% = max (74%, 51%)
c [simplification-1] large reduction 74% >= 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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1002 conflicts
c [decomp-3] removed 3 variables
c [simpleprobe-2] all 13301 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 2 variables
c [simpleprobe-2] 7348 variables remain 55% (5951 retained 45%)
c [simpleprobe-2] removed 2 variables, found 513 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 26598 literals 100%
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 382965 steps
c [treelook-1] 26452 literals remain 99%
c [treelook-1] 13299 variables remain to probed next time 100%
c [decomp-5] removed 6 variables
c [treelook-1] removed 6 variables, found 1907 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6423 probes remain 48% after last round
c [basicprobe-1-0] removed 0 variables, found 4354 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 13293 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 211 variables 2% in round 1 in 11808897 steps
c [elim-2-1] backward subsumption/strengthening limit 8191103
c [elim-2-1-1] backward checking 2248 touched variables 17%
c [elim-2-1-1] incomplete backward checking 2170 remain 97%
c [elim-2-1] subsumed 2 and strengthened 26 clauses in 8193680 steps
c [elim-2] incomplete 66 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 211 = 2% variables out of 13293 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 9229 enqueued variables after 1002 conflicts
c [score-dist-2] active 3853 (29%), one 0 (0%), zero 9229 (71%)
c [score-dist-2] max exp 757, different 231 (30%)
c [score-dist-2] median active exp 634, avg 632.2
c [simplification-2] removed 222 variables 1.7% (13082 remain 25%)
c [simplification-2] removed 728 irredundant clauses 1.0% (73136 remain 48%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17668 (soft 7668 + delta 10000)
c [simplification-2] new conflict limit 7668 (hard 17668)
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    3.4   13081    73136      6640    5262    572  6631    5   100   10   5%     84   93    7    1 1152%
c 
c [simplification-3] limit 7668 conflicts (hard 17668) hit after 7669 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 187 at-most-one constraints of average size 3.0
c [card-2] found 6 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 193 out of 193 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 56 at-most-one constraints, 28 used 50%
c [card-2] exported 38 binary clauses, 1.4 per/constraint
c [decomp-6] removed 12 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 26140 literals 100%
c [treelook-2] scheduling used 300002 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 322906 steps
c [treelook-2] 25844 literals remain 99%
c [treelook-2] 13069 variables remain to probed next time 100%
c [treelook-2] removed 1 variables, found 1018 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 1 units, 3 failed, 992 tauts, 0 hbrs, 3189 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 13066 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 95 variables 1% in round 1 in 14713712 steps
c [elim-3-1] backward subsumption/strengthening limit 5286288
c [elim-3-1-1] backward checking 853 touched variables 7%
c [elim-3-1-1] incomplete backward checking 834 remain 98%
c [elim-3-1] subsumed 0 and strengthened 5 clauses in 5286633 steps
c [elim-3] incomplete 16 not tried 0% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 95 = 1% variables out of 13066 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 6815 enqueued variables after 7669 conflicts
c [score-dist-3] active 6156 (47%), one 1337 (10%), zero 5478 (42%)
c [score-dist-3] max exp 945, different 579 (61%)
c [score-dist-3] median active exp 780, avg 683.7
c [simplification-3] removed 110 variables 0.8% (12971 remain 25%)
c [simplification-3] removed 269 irredundant clauses 0.4% (72867 remain 48%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 16666
c [simplification-3] penalized conflict interval 16666 = 1 * 16666
c [simplification-3] hard conflict limit 34335 (soft 24335 + delta 10000)
c [simplification-3] new conflict limit 24335 (hard 34335)
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   12970    72867      9187    7193    712  6532    6   122   11   5%     27  111    6    1  681%
c 
c [simplification-4] limit of 186 binary hit after 186 binaries
c [decomp-8] removed 25 variables
c [unhide-3] limit 150945 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 1 failed, 136 tauts, 0 hbrs, 4778 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 12945 variables 100%
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] eliminated 85 variables 1% in round 1 in 14620320 steps
c [elim-4-1] backward subsumption/strengthening limit 14620300
c [elim-4-1-1] backward checking 487 touched variables 4%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 6 and strengthened 17 clauses in 13766484 steps
c [elim-4-1] rescheduled 40 variables 0% by backward subsumption
c [elim-4-2] eliminated 5 variables 0% in round 2 in 162992 steps
c [elim-4-2] backward subsumption/strengthening limit 162900
c [elim-4-2-1] backward checking 28 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 7 clauses in 44270 steps
c [elim-4-2] rescheduled 21 variables 0% by backward subsumption
c [elim-4-3] eliminated 1 variables 0% in round 3 in 42327 steps
c [elim-4-3] backward subsumption/strengthening limit 42300
c [elim-4-3-1] backward checking 10 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 1 and strengthened 0 clauses in 33009 steps
c [elim-4] incomplete 3 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 91 = 1% variables out of 12945 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 4774 enqueued variables after 19152 conflicts
c [score-dist-4] active 8080 (63%), one 3132 (24%), zero 1642 (13%)
c [score-dist-4] max exp 843, different 607 (72%)
c [score-dist-4] median active exp 578, avg 552.4
c [simplification-4] removed 116 variables 0.9% (12854 remain 25%)
c [simplification-4] removed 324 irredundant clauses 0.4% (72543 remain 48%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] forced so keeping old conflict interval 16666
c [simplification-4] conflict limit remains at 24335 (hard 34335)
c [simplification-4] new binary interval 1000
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    7.0   12853    72543     19497   15144   1253  6577    7   130   12   5%    130  103    7    2  441%
c 
c [simplification-5] limit 24335 conflicts (hard 34335) hit after 24336 conflicts
c [quatres-1] found 17641 quaternary clauses 50% in total
c [quatres-1-1] removed 2 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 118 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1867 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 12853 free variables schedulable
c [ternres-1] 8214 ternary resolvents (155 bin, 8059 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5123 xors of average arity 3.0
c [gauss-1] connected 15557 occurrences of 1110 variables (average 14.0)
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-9] removed 26 variables
c [basicprobe-2] limit 2428542 penalty 1 = 1 + 0
c [basicprobe-2-0] 4540 probes remain 35% after last round
c [basicprobe-2-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1 variables, found 7161 hbrs
c [bate-1] eliminated 13 asymmetric tautologies during probing
c [unhide-4] limit 194283 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 0 failed, 1354 tauts, 0 hbrs, 5854 literals
c [transred-1] limit 971416 with penalty 0 = 0 + 0
c [transred-1] removed 387 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 12824 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 2016 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 68 (3%) of length 13
c [cce-1-1] eliminated 6 clauses out of 85 (7%) of length 12
c [cce-1-1] eliminated 7 clauses out of 118 (6%) of length 11
c [cce-1-1] eliminated 8 clauses out of 186 (4%) of length 10
c [cce-1-1] eliminated 17 clauses out of 374 (5%) of length 9
c [cce-1-1] eliminated 35 clauses out of 601 (6%) of length 8
c [cce-1-1] eliminated 91 clauses out of 1285 (7%) of length 7
c [cce-1-1] eliminated 339 clauses out of 3427 (10%) of length 6
c [cce-1-1] eliminated 250 clauses out of 6924 (4%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 755 large clauses in 30000043 steps
c [cce-1-1] allowing another 15000021 steps for small clauses
c [cce-1-1] scheduling 22740 clauses = 14082 binary + 8658 ternary
c [cce-1-1] tried to eliminate 11040 small clauses 49%
c [cce-1-1] eliminated 67 binary clauses 0%
c [cce-1-1] eliminated 240 ternary clauses 3%
c [cce-1-1] eliminated 307 small clauses 1%
c [cce-1-1] eliminated 307 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1062 covered clauses in round 1
c [cce-1] eliminated 1062 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 12824 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 457 variables 4% in round 1 in 15395266 steps
c [elim-5-1] backward subsumption/strengthening limit 4604734
c [elim-5-1-1] backward checking 2707 touched variables 21%
c [elim-5-1-1] incomplete backward checking 2303 remain 85%
c [elim-5-1] subsumed 6 and strengthened 40 clauses in 4605016 steps
c [elim-5] incomplete 94 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 457 = 4% variables out of 12824 scheduled
c [bca-1] limit of 10000000 steps and 138216 added (scaled 2)
c [bca-1] 10236 out of 24736 literals actually usable 41%
c [bca-1] added 65 blocked clauses in 44494 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 5245 pos 42.4% + 7122 neg 57.6% = 12367 sched 100.0% ret 0
c [sweep-1-1] 1000841 steps 68 queries 1294.65 avg class size
c [sweep-1-1] 1602 decisions 64 SAT calls 46.50 avg env size
c [sweep-1-1] 11198 variables remain 91% (1169 retained 9%)
c [decomp-10] removed 51 variables
c [sweep-1-1] removed 51 vars (0 failed, 3 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 51 vars in TOTAL (1 rounds, 67 queries)
c [sort-queue-5] sorted 6914 enqueued variables after 24336 conflicts
c [score-dist-5] active 5402 (44%), one 5700 (46%), zero 1214 (10%)
c [score-dist-5] max exp 690, different 471 (68%)
c [score-dist-5] median active exp 569, avg 511.7
c [simplification-5] removed 537 variables 4.2% (12316 remain 24%)
c [simplification-5] removed 3714 irredundant clauses 5.1% (68829 remain 45%)
c [simplification-5] maximum reduction of 5% = max (4%, 5%)
c [simplification-5] large reduction 5% >= 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 36336 (soft 26336 + delta 10000)
c [simplification-5] new conflict limit 26336 (hard 36336)
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    9.9   12315    68829     25196   20534   9466 11788    8   139   13   6%     55  103    8    2  352%
c 
c [simplification-6] limit 26336 conflicts (hard 36336) hit after 26336 conflicts
c [quatres-2] found 18654 quaternary clauses 51% in total
c [quatres-2-1] removed 8 duplicate quaternary clauses
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 89 single-self-subsuming ternary resolvents
c [quatres-2-2] added 883 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12315 free variables schedulable
c [ternres-2] 970 ternary resolvents (67 bin, 903 trn)
c [ternres-2] 5 variables remain 0% (12310 retained 100%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 153 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] 153 out of 153 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 9 variables
c [simpleprobe-3] 6739 schedulable variables 55%
c [simpleprobe-3] limit 4215485 penalty 0 = 0 + 0
c [decomp-12] removed 31 variables
c [simpleprobe-3] 3272 variables remain 27% (9004 retained 73%)
c [simpleprobe-3] removed 31 variables, found 1245 hbrs, 1 units
c [unhide-5] limit 210774 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 367 tauts, 0 hbrs, 2546 literals
c [transred-2] limit 1053871 with penalty 0 = 0 + 0
c [transred-2] removed 104 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12276 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 48 blocked clauses
c [block-2] 48 < 1/100 * 68616 = 686 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 91 (1%) of length 12
c [cce-2-1] eliminated 1 clauses out of 137 (1%) of length 11
c [cce-2-1] eliminated 7 clauses out of 193 (4%) of length 10
c [cce-2-1] eliminated 8 clauses out of 428 (2%) of length 9
c [cce-2-1] eliminated 24 clauses out of 774 (3%) of length 8
c [cce-2-1] eliminated 53 clauses out of 1661 (3%) of length 7
c [cce-2-1] eliminated 86 clauses out of 3157 (3%) of length 6
c [cce-2-1] eliminated 9 clauses out of 6832 (0%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 189 large clauses in 30000004 steps
c [cce-2-1] allowing another 15000002 steps for small clauses
c [cce-2-1] scheduling 31395 clauses = 13391 binary + 18004 ternary
c [cce-2-1] tried to eliminate 8791 small clauses 28%
c [cce-2-1] eliminated 31 binary clauses 0%
c [cce-2-1] eliminated 207 ternary clauses 1%
c [cce-2-1] eliminated 238 small clauses 1%
c [cce-2-1] eliminated 238 small clauses in 30000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 427 covered clauses in round 1
c [cce-2] eliminated 427 covered clauses in TOTAL during 1 rounds
c [cce-2] 427 < 1/100 * 68568 = 685 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 12273 variables 100%
c [elim-6] limit of 21077429 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 94 variables 1% in round 1 in 15371058 steps
c [elim-6-1] backward subsumption/strengthening limit 5706371
c [elim-6-1-1] backward checking 699 touched variables 6%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 1 and strengthened 0 clauses in 3900947 steps
c [elim-6-1] rescheduled 4 variables 0% by backward subsumption
c [elim-6-2] eliminated 1 variables 0% in round 2 in 1063 steps
c [elim-6-2] backward subsumption/strengthening limit 1000
c [elim-6-2-1] backward checking 9 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 0 and strengthened 2 clauses in 1067 steps
c [elim-6-2] rescheduled 7 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 2402 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 95 = 1% variables out of 12273 scheduled
c [elim-6] 95 < 1/100 * 12273 = 122 considered unsuccessful
c [bca-2] limit of 10000000 steps and 136372 added (scaled 2)
c [bca-2] 9383 out of 24358 literals actually usable 39%
c [bca-2] added 2 blocked clauses in 44725 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4767 pos 43.2% + 6261 neg 56.8% = 11028 sched 90.6% ret 1150
c [sweep-2-1] 1421770 steps 61 queries 1406.02 avg class size
c [sweep-2-1] 1375 decisions 56 SAT calls 46.71 avg env size
c [sweep-2-1] 10306 variables remain 85% (1872 retained 15%)
c [decomp-13] removed 13 variables
c [sweep-2-1] removed 13 vars (0 failed, 8 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 13 vars in TOTAL (1 rounds, 60 queries)
c [sort-queue-6] sorted 6182 enqueued variables after 26336 conflicts
c [score-dist-6] active 5983 (49%), one 5054 (42%), zero 1128 (9%)
c [score-dist-6] max exp 723, different 505 (70%)
c [score-dist-6] median active exp 542, avg 484.5
c [simplification-6] removed 150 variables 1.2% (12165 remain 23%)
c [simplification-6] removed 915 irredundant clauses 1.3% (67914 remain 45%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 26666
c [simplification-6] penalized conflict interval 26666 = 1 * 26666
c [simplification-6] hard conflict limit 66335 (soft 53002 + delta 13333)
c [simplification-6] new conflict limit 53002 (hard 66335)
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   12.8   12164    67914     32673   27700  10362 12676    8   131   14   6%     79   85    9    3  324%
c 
c [simplification-7] limit 53002 conflicts (hard 66335) hit after 53003 conflicts
c [quatres-3] found 20393 quaternary clauses 49% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-1] added 4 double-self-subsuming ternary resolvents
c [quatres-3-2] added 101 single-self-subsuming ternary resolvents
c [quatres-3-2] added 573 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 5 schedulable variables 0%
c [ternres-3] 445 ternary resolvents (3 bin, 442 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 2131 xors of average arity 3.0
c [gauss-2] connected 6353 occurrences of 847 variables (average 7.5)
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-14] removed 20 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 18205 literals 75%
c [treelook-3] scheduling used 300034 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 362601 steps
c [treelook-3] 18188 literals remain 75%
c [treelook-3] 11297 variables remain to probed next time 93%
c [treelook-3] removed 0 variables, found 1307 hbrs
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 715 transitive binary clauses
c [transred-3] found 3 units
c [bca-3] limit of 10000000 steps and 136213 added (scaled 2)
c [bca-3] 6218 out of 24284 literals actually usable 26%
c [bca-3] added 0 blocked clauses in 60082 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 4489 pos 43.7% + 5789 neg 56.3% = 10278 sched 84.7% ret 1863
c [sweep-3-1] 1069490 steps 45 queries 1178.73 avg class size
c [sweep-3-1] 1774 decisions 42 SAT calls 77.74 avg env size
c [sweep-3-1] 9697 variables remain 80% (2444 retained 20%)
c [decomp-16] removed 7 variables
c [sweep-3-1] removed 7 vars (0 failed, 3 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 7 vars in TOTAL (1 rounds, 44 queries)
c [sort-queue-7] sorted 7023 enqueued variables after 53003 conflicts
c [score-dist-7] active 5111 (42%), one 6678 (55%), zero 345 (3%)
c [score-dist-7] max exp 629, different 415 (66%)
c [score-dist-7] median active exp 487, avg 438.3
c [simplification-7] removed 30 variables 0.2% (12134 remain 23%)
c [simplification-7] removed 76 irredundant clauses 0.1% (67838 remain 45%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 26666
c [simplification-7] new conflict interval 53332
c [simplification-7] penalized conflict interval 53332 = 1 * 53332
c [simplification-7] hard conflict limit 133001 (soft 106335 + delta 26666)
c [simplification-7] new conflict limit 106335 (hard 133001)
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   18.0   12133    67838     58501   51051  11303 13509    9   131   18   7%    306   60    9    5  188%
c i   19.1   12132    67838     63744   55668  11402 13537    9   132   18   7%    -14   56    8    5  163%
c -   21.9   12132    67837     76431   27763  11704 13598    8   125   15   7%     98   40    9    6  153%
c i   22.2   12131    67837     78088   29210  11744 13605    8   131   16   6%    121   44    9    6  157%
c i   25.5   12130    67837     94727   44220  12050 13670    9   129   17   7%    147   34    9    6  146%
c i   25.7   12129    67837     96094   45403  12101 13688    8   113   17   7%    -24   18    8    6  122%
c 
c [simplification-8] limit 106335 conflicts (hard 133001) hit after 106335 conflicts
c [quatres-4] found 22518 quaternary clauses 45% in total
c [quatres-4-1] added 9 double-self-subsuming ternary resolvents
c [quatres-4-2] added 202 single-self-subsuming ternary resolvents
c [quatres-4-2] added 445 quaternary resolvents
c [ternres-4] limit 5376466 with penalty 0 = 0 + 0
c [ternres-4] all 12129 free variables schedulable
c [ternres-4] 2605 ternary resolvents (108 bin, 2497 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 46 variables
c [basicprobe-3] limit 26882332 penalty 0 = 0 + 0
c [basicprobe-3-0] 4587 sched 38%, 30 failed, 2 lifted, 9391 hbrs
c [decomp-18] removed 99 variables
c [basicprobe-3-1] 6884 sched 58%, 19 failed, 1 lifted, 3702 hbrs
c [decomp-19] removed 40 variables
c [basicprobe-3-2] 2473 probes remain 21% after last round
c [basicprobe-3-2] 53 units = 50 failed (94%) + 3 lifted (6%)
c [basicprobe-3-2] removed 140 variables, found 13236 hbrs
c [bate-2] eliminated 42 asymmetric tautologies during probing
c [unhide-6] limit 537646 with penalty 1 = 1 + 0
c [unhide-6-6] 0 units, 0 failed, 3270 tauts, 0 hbrs, 28561 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 623 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 11947 variables 100%
c [block-3] limit of 26882332 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 299 blocked clauses
c [block-3] 299 < 1/100 * 67313 = 673 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 72 (3%) of length 13
c [cce-3-1] eliminated 2 clauses out of 81 (2%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 21539 clauses = 13069 binary + 8470 ternary
c [cce-3-1] tried to eliminate 1394 small clauses 6%
c [cce-3-1] eliminated 31 binary clauses 0%
c [cce-3-1] eliminated 9 ternary clauses 0%
c [cce-3-1] eliminated 40 small clauses 0%
c [cce-3-1] eliminated 40 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 44 covered clauses in round 1
c [cce-3] eliminated 44 covered clauses in TOTAL during 1 rounds
c [cce-3] 44 < 1/100 * 67002 = 670 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 11921 variables 100%
c [elim-7] limit of 53764665 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 99 variables 1% in round 1 in 24218951 steps
c [elim-7-1] backward subsumption/strengthening limit 24218900
c [elim-7-1-1] backward checking 665 touched variables 6%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 5 and strengthened 3 clauses in 2176358 steps
c [elim-7-1] rescheduled 18 variables 0% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 18170 steps
c [elim-7-2] backward subsumption/strengthening limit 18100
c [elim-7-2-1] backward checking 9 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 18101 steps
c [elim-7-2] fully rescheduled 11821 variables 99%
c [elim-7-3] eliminated 9 variables 0% in round 3 in 24171844 steps
c [elim-7-3] backward subsumption/strengthening limit 3161241
c [elim-7-3-1] backward checking 66 touched variables 1%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 1786783 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 109 = 1% variables out of 11921 scheduled
c [elim-7] 109 < 1/100 * 11921 = 119 considered unsuccessful
c [sweep-4] limit 1612939 penalty 0 = 0 + 0
c [sweep-4-1] 4169 pos 44.3% + 5250 neg 55.7% = 9419 sched 79.7% ret 2393
c [sweep-4-1] 1630552 steps 61 queries 781.51 avg class size
c [sweep-4-1] 1630 decisions 57 SAT calls 53.68 avg env size
c [sweep-4-1] 8652 variables remain 73% (3159 retained 27%)
c [decomp-20] removed 50 variables
c [sweep-4-1] removed 50 vars (0 failed, 7 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 50 vars in TOTAL (1 rounds, 60 queries)
c [sort-queue-8] sorted 3426 enqueued variables after 106335 conflicts
c [score-dist-8] active 8336 (71%), one 3411 (29%), zero 15 (0%)
c [score-dist-8] max exp 991, different 600 (60%)
c [score-dist-8] median active exp 805, avg 753.5
c [simplification-8] removed 367 variables 3.0% (11762 remain 23%)
c [simplification-8] removed 1286 irredundant clauses 1.9% (66551 remain 44%)
c [simplification-8] maximum reduction of 3% = max (3%, 2%)
c [simplification-8] geometric conflict interval increment 13333 = 53332 / 4
c [simplification-8] new conflict interval 66665
c [simplification-8] penalized conflict interval 66665 = 1 * 66665
c [simplification-8] hard conflict limit 206332 (soft 173000 + delta 33332)
c [simplification-8] new conflict limit 173000 (hard 206332)
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   35.0   11761    66547    128850   73234  13369 21990    8    86   19   9%    333  -14    9    7  130%
c i   35.4   11760    66547    130350   74571  13403 21995    8    97   19   8%    -40   -2    8    7  116%
c -   35.6   11760    66547    132426   40863  13418 22000    8    96   16   8%   -127   -3    9    7  133%
c i   39.4   11759    66547    163135   68702  13727 22091    8   103   19   8%    292    7    8    7  115%
c i   39.5   11758    66547    164580   70038  13729 22091    8    99   20   8%    -75    3    8    7  114%
c i   41.8   11757    66547    182169   86054  13856 22120    7    60   22  12%     70  -31   10    7  135%
c -   42.1   11757    66547    183571   55155  13870 22121    8    77   17  11%   -113  -13   11    7  143%
c i   42.5   11756    66547    185955   57360  13912 22125    8    84   19  10%   -133   -6    8    7  113%
c 
c [simplification-9] limit 173000 conflicts (hard 206332) hit after 198686 conflicts
c [quatres-5] found 23992 quaternary clauses 38% in total
c [quatres-5-1] removed 10 duplicate quaternary clauses
c [quatres-5-1] added 6 double-self-subsuming ternary resolvents
c [quatres-5-2] added 255 single-self-subsuming ternary resolvents
c [quatres-5-2] added 546 quaternary resolvents
c [ternres-5] limit 9087125 with penalty 0 = 0 + 0
c [ternres-5] all 11756 free variables schedulable
c [ternres-5] 2901 ternary resolvents (177 bin, 2724 trn)
c [ternres-5] 1 variables remain 0% (11755 retained 100%)
c [decomp-21] removed 82 variables
c [simpleprobe-4] 3096 schedulable variables 27%
c [simpleprobe-4] limit 36348502 penalty 0 = 0 + 0
c [decomp-22] removed 69 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 69 variables, found 3473 hbrs, 21 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1400 transitive binary clauses
c [bca-4] limit of 10000000 steps and 132843 added (scaled 2)
c [bca-4] 3514 out of 23224 literals actually usable 15%
c [bca-4] added 1 blocked clauses in 76179 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 27261370 penalty 0 = 0 + 0
c [sweep-5-1] 3666 pos 43.2% + 4811 neg 56.8% = 8477 sched 73.0% ret 3134
c [sweep-5-1] 27261923 steps 1210 queries 37.95 avg class size
c [sweep-5-1] 20797 decisions 1107 SAT calls 50.56 avg env size
c [sweep-5-1] 356 variables remain 3% (11246 retained 97%)
c [decomp-23] removed 431 variables
c [sweep-5-1] removed 431 vars (0 failed, 429 eqs, 318 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 431 vars in TOTAL (1 rounds, 1209 queries)
c [sort-queue-9] sorted 4523 enqueued variables after 198686 conflicts
c [score-dist-9] active 6657 (60%), one 4520 (40%), zero 3 (0%)
c [score-dist-9] max exp 765, different 655 (86%)
c [score-dist-9] median active exp 476, avg 433.1
c [simplification-9] removed 576 variables 4.9% (11180 remain 22%)
c [simplification-9] removed 744 irredundant clauses 1.1% (65803 remain 43%)
c [simplification-9] maximum reduction of 5% = max (5%, 1%)
c [simplification-9] large reduction 5% >= 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 210686 (soft 200686 + delta 10000)
c [simplification-9] new conflict limit 200686 (hard 210686)
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   46.6   11179    65803    200626   70525  14587 23471    8    92   21   9%     45    3    7    8   90%
c 
c [simplification-10] limit 200686 conflicts (hard 210686) hit after 200688 conflicts
c [quatres-6] found 24116 quaternary clauses 38% in total
c [quatres-6-1] removed 69 duplicate quaternary clauses
c [quatres-6-1] added 35 double-self-subsuming ternary resolvents
c [quatres-6-2] added 230 single-self-subsuming ternary resolvents
c [quatres-6-2] added 294 quaternary resolvents
c [ternres-6] limit 9190346 with penalty 0 = 0 + 0
c [ternres-6] 1 schedulable variables 0%
c [ternres-6] 304 ternary resolvents (24 bin, 280 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 574396 penalty 3 = 3 + 0
c [card-4] found 150 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 574396 for elimination
c [card-4] 150 out of 150 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 812 xors of average arity 3.0
c [gauss-3] connected 2413 occurrences of 576 variables (average 4.2)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [decomp-24] removed 10 variables
c [gauss-3] exported 0 unary, 1 binary and 3 ternary equations
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 825 transitive binary clauses
c [transred-6] found 8 units
c [bca-5] limit of 10000000 steps and 131536 added (scaled 2)
c [bca-5] 3278 out of 22324 literals actually usable 15%
c [bca-5] added 0 blocked clauses in 77556 steps
c [sweep-6] limit 2757103 penalty 0 = 0 + 0
c [sweep-6-1] 167 pos 48.7% + 176 neg 51.3% = 343 sched 3.1% ret 10818
c [sweep-6-1] 2828651 steps 70 queries 33.79 avg class size
c [sweep-6-1] 1423 decisions 59 SAT calls 60.80 avg env size
c [sweep-6-1] 223 variables remain 2% (10936 retained 98%)
c [decomp-26] removed 38 variables
c [sweep-6-1] removed 38 vars (0 failed, 29 eqs, 24 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 38 vars in TOTAL (1 rounds, 69 queries)
c [sort-queue-10] sorted 3532 enqueued variables after 200688 conflicts
c [score-dist-10] active 7591 (68%), one 3529 (32%), zero 3 (0%)
c [score-dist-10] max exp 840, different 633 (75%)
c [score-dist-10] median active exp 541, avg 546.9
c [simplification-10] removed 56 variables 0.5% (11123 remain 21%)
c [simplification-10] removed 368 irredundant clauses 0.6% (65435 remain 43%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 33332 = 66665 / 2
c [simplification-10] new conflict interval 99997
c [simplification-10] penalized conflict interval 99997 = 1 * 99997
c [simplification-10] hard conflict limit 350683 (soft 300685 + delta 49998)
c [simplification-10] new conflict limit 300685 (hard 350683)
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   47.5   11122    65435    200899   70604  14888 21203    8    93   21   9%     -4    4    9    8  119%
c i   47.7   11121    65435    201931   71570  14894 21204    8    92   21   9%   -101    2    9    8  120%
c i   48.0   11120    65433    204352   73697  14917 21207    9    81   21  11%   -133   -9    9    8  122%
c -   50.8   11120    65418    224208   59621  15009 21220    8    53   17  15%    135  -28    7    8   85%
c i   53.0   11119    65411    244663   78297  15070 21226    8    64   21  12%    374  -10   10    8  125%
c -   55.8   11119    65405    265118   65298  15143 21245    9   127   25   7%     80   46   11    8  134%
c 
c [simplification-11] limit 300685 conflicts (hard 350683) hit after 300685 conflicts
c [quatres-7] found 24515 quaternary clauses 33% in total
c [quatres-7-1] removed 14 duplicate quaternary clauses
c [quatres-7-1] added 5 double-self-subsuming ternary resolvents
c [quatres-7-2] added 134 single-self-subsuming ternary resolvents
c [quatres-7-2] added 215 quaternary resolvents
c [ternres-7] limit 13035843 with penalty 0 = 0 + 0
c [ternres-7] all 11119 free variables schedulable
c [ternres-7] 2798 ternary resolvents (166 bin, 2632 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 58 variables
c [treelook-4] limit 651792 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 21095 literals 95%
c [treelook-4] scheduling used 589841 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 651792 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 670614 steps
c [treelook-4] 21002 literals remain 95%
c [treelook-4] 10272 variables remain to probed next time 93%
c [decomp-28] removed 5 variables
c [treelook-4] removed 5 variables, found 2263 hbrs
c [unhide-7] limit 651792 with penalty 2 = 2 + 0
c [unhide-7-7] 1 units, 7 failed, 509 tauts, 0 hbrs, 37469 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 568 transitive binary clauses
c [transred-7] found 3 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 11053 variables 100%
c [block-4] limit of 32589609 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 1343 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 162948047 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 3 clauses out of 133 (2%) of length 11
c [cce-4-1] eliminated 2 clauses out of 227 (1%) of length 10
c [cce-4-1] eliminated 5 clauses out of 375 (1%) of length 9
c [cce-4-1] eliminated 10 clauses out of 652 (2%) of length 8
c [cce-4-1] eliminated 28 clauses out of 1349 (2%) of length 7
c [cce-4-1] eliminated 147 clauses out of 2840 (5%) of length 6
c [cce-4-1] eliminated 875 clauses out of 6508 (13%) of length 5
c [cce-4-1] eliminated 1457 clauses out of 14373 (10%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 2527 large clauses in 84293225 steps
c [cce-4-1] allowing another 42146612 steps for small clauses
c [cce-4-1] scheduling 28757 clauses = 12167 binary + 16590 ternary
c [cce-4-1] tried to eliminate 28757 small clauses 100%
c [cce-4-1] eliminated 238 binary clauses 2%
c [cce-4-1] eliminated 922 ternary clauses 6%
c [cce-4-1] eliminated 1160 small clauses 4%
c [cce-4-1] eliminated 1160 small clauses in 100518885 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 3687 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 31214581 steps for small clauses
c [cce-4-2] scheduling 27597 clauses = 11929 binary + 15668 ternary
c [cce-4-2] tried to eliminate 20486 small clauses 74%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 3687 covered clauses in TOTAL during 2 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 10929 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1303584390 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 720 variables 7% in round 1 in 19063794 steps
c [elim-8-1] backward subsumption/strengthening limit 19063700
c [elim-8-1-1] backward checking 2844 touched variables 26%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 6 and strengthened 48 clauses in 2471432 steps
c [elim-8-1] rescheduled 117 variables 1% by backward subsumption
c [elim-8-2] eliminated 9 variables 0% in round 2 in 6611415 steps
c [elim-8-2] backward subsumption/strengthening limit 6611400
c [elim-8-2-1] backward checking 85 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 2 and strengthened 2 clauses in 1402470 steps
c [elim-8-2] rescheduled 5 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 21832 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 731 = 7% variables out of 10929 scheduled
c [sweep-7] limit 3910753 penalty 0 = 0 + 0
c [sweep-7-1] 105 pos 63.6% + 60 neg 36.4% = 165 sched 1.6% ret 10033
c [sweep-7-1] 2923012 steps 111 queries 10.85 avg class size
c [sweep-7-1] 1725 decisions 101 SAT calls 36.76 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-29] removed 36 variables
c [sweep-7-1] removed 36 vars (0 failed, 27 eqs, 20 impls)
c [sweep-7-2] 4589 pos 45.2% + 5573 neg 54.8% = 10162 sched 100.0% ret 0
c [sweep-7-2] 1189838 steps 28 queries 1161.82 avg class size
c [sweep-7-2] 731 decisions 24 SAT calls 67.25 avg env size
c [sweep-7-2] 9733 variables remain 96% (429 retained 4%)
c [decomp-30] removed 2 variables
c [sweep-7-2] removed 2 vars (0 failed, 3 eqs, 4 impls)
c [sweep-7] removed 38 vars in TOTAL (2 rounds, 137 queries)
c [sort-queue-11] sorted 5467 enqueued variables after 300685 conflicts
c [score-dist-11] active 4693 (46%), one 5467 (54%), zero 0 (0%)
c [score-dist-11] max exp 539, different 321 (59%)
c [score-dist-11] median active exp 294, avg 337.5
c [simplification-11] removed 959 variables 8.6% (10160 remain 20%)
c [simplification-11] removed 7799 irredundant clauses 11.9% (57601 remain 38%)
c [simplification-11] maximum reduction of 12% = max (9%, 12%)
c [simplification-11] large reduction 12% >= 5% limit
c [simplification-11] next conflict interval 3006 = min (300685/100, 99997)
c [simplification-11] penalized conflict interval 3006 = 1 * 3006
c [simplification-11] hard conflict limit 313691 (soft 303691 + delta 10000)
c [simplification-11] new conflict limit 303691 (hard 313691)
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   64.9   10159    57601    303243   87767  16019 18614    8    79   23  10%    496   -5    6    8   70%
c 
c [simplification-12] limit 303691 conflicts (hard 313691) hit after 313692 conflicts
c [quatres-8] found 22110 quaternary clauses 32% in total
c [quatres-8-1] removed 21 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 139 single-self-subsuming ternary resolvents
c [quatres-8-2] added 387 quaternary resolvents
c [ternres-8] limit 13466027 with penalty 0 = 0 + 0
c [ternres-8] all 10159 free variables schedulable
c [ternres-8] 2406 ternary resolvents (120 bin, 2286 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-4] limit 1346602 penalty 1 = 1 + 0
c [gauss-4] extracted 1636 xors of average arity 3.0
c [gauss-4] connected 4850 occurrences of 668 variables (average 7.3)
c [gauss-4] limit 1346602 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 17 variables
c [basicprobe-4] limit 67330139 penalty 0 = 0 + 0
c [basicprobe-4-0] 2528 sched 25%, 4 failed, 0 lifted, 1381 hbrs
c [decomp-32] removed 8 variables
c [basicprobe-4-1] 5884 sched 58%, 14 failed, 0 lifted, 2345 hbrs
c [decomp-33] removed 24 variables
c [basicprobe-4-2] 5845 sched 58%, 2 failed, 0 lifted, 222 hbrs
c [decomp-34] removed 4 variables
c [basicprobe-4-3] 5837 sched 58%, 0 failed, 0 lifted, 41 hbrs
c [basicprobe-4-4] 5837 sched 58%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-4-5] 5837 sched 58%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-4-6] 5837 sched 58%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-7] 5837 sched 58%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-4-8] 4106 probes remain 41% after last round
c [basicprobe-4-8] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 36 variables, found 4031 hbrs
c [bate-3] eliminated 16 asymmetric tautologies during probing
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 816 transitive binary clauses
c [bca-6] limit of 10000000 steps and 115322 added (scaled 2)
c [bca-6] 2878 out of 20214 literals actually usable 14%
c [bca-6] added 18 blocked clauses in 103076 steps
c [sweep-8] limit 4039808 penalty 0 = 0 + 0
c [sweep-8-1] 4293 pos 44.3% + 5392 neg 55.7% = 9685 sched 95.8% ret 421
c [sweep-8-1] 4067863 steps 169 queries 340.42 avg class size
c [sweep-8-1] 4391 decisions 169 SAT calls 64.77 avg env size
c [sweep-8-1] 6841 variables remain 68% (3265 retained 32%)
c [decomp-40] removed 27 variables
c [sweep-8-1] removed 27 vars (0 failed, 19 eqs, 17 impls)
c [sweep-8] removed 27 vars in TOTAL (1 rounds, 168 queries)
c [sort-queue-12] sorted 7478 enqueued variables after 313692 conflicts
c [score-dist-12] active 2601 (26%), one 7478 (74%), zero 0 (0%)
c [score-dist-12] max exp 546, different 254 (46%)
c [score-dist-12] median active exp 479, avg 465.9
c [simplification-12] removed 80 variables 0.8% (10079 remain 19%)
c [simplification-12] removed 222 irredundant clauses 0.4% (57379 remain 38%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 49998 = 99997 / 2
c [simplification-12] new conflict interval 149995
c [simplification-12] penalized conflict interval 149995 = 1 * 149995
c [simplification-12] hard conflict limit 538684 (soft 463687 + delta 74997)
c [simplification-12] new conflict limit 463687 (hard 538684)
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 -   69.6   10079    57379    316466   68064  17401 20471    8   143   18   6%   -167   58    8    8   96%
c i   70.4   10078    57378    327404   77568  17460 20490    7    88   21   8%     16   -7    5    8   61%
c -   73.2   10078    57378    356671   72625  17588 20526    8    53   18  15%    134  -32   10    8  124%
c -   77.9   10078    57378    396583   77694  17640 20534    8    59   27  13%    540   -3    8    8  106%
c -   84.3   10078    57378    436582   79461  17732 20545    9    49   27  17%    761   -8   10    8  127%
c -   90.5   10078    57378    476898   81900  17807 20555    9    28   27  33%    882  -19    8    8  102%
c 
c [simplification-13] limit 463687 conflicts (hard 538684) hit after 496515 conflicts
c [quatres-9] found 23202 quaternary clauses 28% in total
c [quatres-9-1] removed 25 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 102 single-self-subsuming ternary resolvents
c [quatres-9-2] added 222 quaternary resolvents
c [ternres-9] limit 21941670 with penalty 0 = 0 + 0
c [ternres-9] all 10078 free variables schedulable
c [ternres-9] 2237 ternary resolvents (103 bin, 2134 trn)
c [ternres-9] 1 variables remain 0% (10077 retained 100%)
c [decomp-41] removed 15 variables
c [simpleprobe-5] all 10064 free variables schedulable
c [simpleprobe-5] limit 87766682 penalty 0 = 0 + 0
c [decomp-42] removed 53 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 53 variables, found 2683 hbrs, 16 units
c [unhide-8] limit 2194167 with penalty 1 = 1 + 0
c [unhide-8-9] 1 units, 5 failed, 5851 tauts, 0 hbrs, 53559 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 507 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 10009 variables 100%
c [block-5] limit of 109708353 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 1333 blocked clauses
c [cce-5] limit of 54854176 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 29 (3%) of length 14
c [cce-5-1] eliminated 4 clauses out of 63 (6%) of length 12
c [cce-5-1] eliminated 1 clauses out of 116 (1%) of length 11
c [cce-5-1] eliminated 9 clauses out of 220 (4%) of length 10
c [cce-5-1] eliminated 15 clauses out of 383 (4%) of length 9
c [cce-5-1] eliminated 32 clauses out of 664 (5%) of length 8
c [cce-5-1] eliminated 89 clauses out of 1342 (7%) of length 7
c [cce-5-1] eliminated 174 clauses out of 2710 (6%) of length 6
c [cce-5-1] eliminated 106 clauses out of 5652 (2%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 431 large clauses in 54854178 steps
c [cce-5-1] allowing another 27427089 steps for small clauses
c [cce-5-1] scheduling 24216 clauses = 10747 binary + 13469 ternary
c [cce-5-1] tried to eliminate 8902 small clauses 37%
c [cce-5-1] eliminated 99 binary clauses 1%
c [cce-5-1] eliminated 149 ternary clauses 1%
c [cce-5-1] eliminated 248 small clauses 1%
c [cce-5-1] eliminated 248 small clauses in 54854255 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 679 covered clauses in round 1
c [cce-5] eliminated 679 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 9879 variables 100%
c [elim-9] limit of 219416706 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 480 variables 5% in round 1 in 17947577 steps
c [elim-9-1] backward subsumption/strengthening limit 17947500
c [elim-9-1-1] backward checking 1544 touched variables 16%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 4 and strengthened 6 clauses in 3941432 steps
c [elim-9-1] rescheduled 36 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 5793669 steps
c [elim-9-2] backward subsumption/strengthening limit 5793600
c [elim-9-2-1] backward checking 9 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 8 clauses in 48362 steps
c [elim-9-2] rescheduled 8 variables 0% by backward subsumption
c [elim-9-3] eliminated 3 variables 0% in round 3 in 3102 steps
c [elim-9-3] backward subsumption/strengthening limit 3100
c [elim-9-3-1] backward checking 9 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 3101 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 484 = 5% variables out of 9879 scheduled
c [bca-7] limit of 10000000 steps and 107509 added (scaled 2)
c [bca-7] 2970 out of 18792 literals actually usable 16%
c [bca-7] added 36 blocked clauses in 101893 steps
c [sweep-9] limit 6582501 penalty 0 = 0 + 0
c [sweep-9-1] 2781 pos 43.9% + 3550 neg 56.1% = 6331 sched 67.4% ret 3064
c [sweep-9-1] 6679393 steps 173 queries 180.84 avg class size
c [sweep-9-1] 4144 decisions 165 SAT calls 75.30 avg env size
c [sweep-9-1] 4275 variables remain 46% (5118 retained 54%)
c [decomp-43] removed 37 variables
c [sweep-9-1] removed 37 vars (0 failed, 29 eqs, 31 impls)
c [sweep-9] removed 37 vars in TOTAL (1 rounds, 172 queries)
c [sort-queue-13] sorted 5437 enqueued variables after 496515 conflicts
c [score-dist-13] active 3921 (42%), one 5437 (58%), zero 0 (0%)
c [score-dist-13] max exp 526, different 274 (52%)
c [score-dist-13] median active exp 436, avg 364.5
c [simplification-13] removed 720 variables 7.1% (9358 remain 18%)
c [simplification-13] removed 3938 irredundant clauses 6.9% (53440 remain 35%)
c [simplification-13] maximum reduction of 7% = max (7%, 7%)
c [simplification-13] large reduction 7% >= 5% limit
c [simplification-13] next conflict interval 4965 = min (496515/100, 149995)
c [simplification-13] penalized conflict interval 4965 = 1 * 4965
c [simplification-13] hard conflict limit 511480 (soft 501480 + delta 10000)
c [simplification-13] new conflict limit 501480 (hard 511480)
c 
c [simplification-14] limit 501480 conflicts (hard 511480) hit after 511481 conflicts
c [quatres-10] found 21976 quaternary clauses 27% in total
c [quatres-10-1] removed 56 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 93 single-self-subsuming ternary resolvents
c [quatres-10-2] added 245 quaternary resolvents
c [ternres-10] limit 22826992 with penalty 0 = 0 + 0
c [ternres-10] 1 schedulable variables 0%
c [ternres-10] 1702 ternary resolvents (30 bin, 1672 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-44] removed 7 variables
c [treelook-5] limit 2282699 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 17807 literals 95%
c [treelook-5] scheduling used 583028 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2282699 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2286415 steps
c [treelook-5] 17154 literals remain 92%
c [treelook-5] 8643 variables remain to probed next time 92%
c [decomp-45] removed 19 variables
c [treelook-5] removed 25 variables, found 8148 hbrs
c [unhide-9] limit 4565398 with penalty 0 = 0 + 0
c [unhide-9-12] 0 units, 0 failed, 3515 tauts, 0 hbrs, 30051 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 453 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 9326 variables 100%
c [block-6] limit of 228269927 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 273 blocked clauses
c [block-6] 273 < 1/100 * 53254 = 532 considered unsuccessful
c [cce-6] limit of 114134963 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 72 (1%) of length 12
c [cce-6-1] eliminated 4 clauses out of 119 (3%) of length 11
c [cce-6-1] eliminated 4 clauses out of 201 (2%) of length 10
c [cce-6-1] eliminated 10 clauses out of 390 (3%) of length 9
c [cce-6-1] eliminated 9 clauses out of 648 (1%) of length 8
c [cce-6-1] eliminated 21 clauses out of 1248 (2%) of length 7
c [cce-6-1] eliminated 41 clauses out of 2519 (2%) of length 6
c [cce-6-1] eliminated 202 clauses out of 5484 (4%) of length 5
c [cce-6-1] eliminated 325 clauses out of 12112 (3%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 617 large clauses in 62104694 steps
c [cce-6-1] allowing another 31052347 steps for small clauses
c [cce-6-1] scheduling 17447 clauses = 10166 binary + 7281 ternary
c [cce-6-1] tried to eliminate 17447 small clauses 100%
c [cce-6-1] eliminated 46 binary clauses 0%
c [cce-6-1] eliminated 316 ternary clauses 4%
c [cce-6-1] eliminated 362 small clauses 2%
c [cce-6-1] eliminated 362 small clauses in 63573479 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 979 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 25280851 steps for small clauses
c [cce-6-2] scheduling 17085 clauses = 10120 binary + 6965 ternary
c [cce-6-2] tried to eliminate 13137 small clauses 77%
c [cce-6-2] incomplete small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 979 covered clauses in TOTAL during 2 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 9300 variables 100%
c [elim-10] limit of 456539855 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 221 variables 2% in round 1 in 16797267 steps
c [elim-10-1] backward subsumption/strengthening limit 16797200
c [elim-10-1-1] backward checking 1121 touched variables 12%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 13 and strengthened 11 clauses in 1539108 steps
c [elim-10-1] rescheduled 48 variables 1% by backward subsumption
c [elim-10-2] eliminated 2 variables 0% in round 2 in 4748094 steps
c [elim-10-2] backward subsumption/strengthening limit 4748000
c [elim-10-2-1] backward checking 21 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 77562 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 223 = 2% variables out of 9300 scheduled
c [bca-8] limit of 10000000 steps and 103507 added (scaled 2)
c [bca-8] 2828 out of 18156 literals actually usable 16%
c [bca-8] added 12 blocked clauses in 112833 steps
c [sweep-10] limit 6848097 penalty 0 = 0 + 0
c [sweep-10-1] 1860 pos 45.0% + 2270 neg 55.0% = 4130 sched 45.5% ret 4947
c [sweep-10-1] 7118147 steps 171 queries 123.16 avg class size
c [sweep-10-1] 4346 decisions 156 SAT calls 65.22 avg env size
c [sweep-10-1] 2922 variables remain 32% (6155 retained 68%)
c [decomp-46] removed 25 variables
c [sweep-10-1] removed 25 vars (0 failed, 23 eqs, 27 impls)
c [sweep-10] removed 25 vars in TOTAL (1 rounds, 170 queries)
c [sort-queue-14] sorted 5034 enqueued variables after 511481 conflicts
c [score-dist-14] active 4018 (44%), one 5034 (56%), zero 0 (0%)
c [score-dist-14] max exp 632, different 352 (56%)
c [score-dist-14] median active exp 531, avg 441.5
c [simplification-14] removed 306 variables 3.3% (9052 remain 17%)
c [simplification-14] removed 1982 irredundant clauses 3.7% (51458 remain 34%)
c [simplification-14] maximum reduction of 4% = max (3%, 4%)
c [simplification-14] geometric conflict interval increment 29999 = 149995 / 5
c [simplification-14] new conflict interval 179994
c [simplification-14] penalized conflict interval 179994 = 1 * 179994
c [simplification-14] hard conflict limit 781472 (soft 691475 + delta 89997)
c [simplification-14] new conflict limit 691475 (hard 781472)
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 -  108.3    9052    51458    522953   82133  17591 21683    8    24   19  32%    954  -18    6    8   77%
c i  110.1    9051    51458    535895   94051  17621 21690    7    16   23  44%    966  -22    6    8   66%
c -  115.8    9051    51458    565562   85249  17660 21693   10    38   28  27%  -1117    1   11    8  132%
c -  122.8    9051    51458    606409   87233  17687 21696    9    41   28  23%   -124   -4   11    9  126%
c -  132.3    9051    51457    649827   89692  17724 21701   11    38   28  29%    432   -3   10    9  114%
c 
c [simplification-15] limit 691475 conflicts (hard 781472) hit after 691475 conflicts
c [quatres-11] found 21653 quaternary clauses 24% in total
c [quatres-11-1] removed 18 duplicate quaternary clauses
c [quatres-11-1] added 6 double-self-subsuming ternary resolvents
c [quatres-11-2] added 80 single-self-subsuming ternary resolvents
c [quatres-11-2] added 194 quaternary resolvents
c [ternres-11] limit 35399570 with penalty 0 = 0 + 0
c [ternres-11] all 9051 free variables schedulable
c [ternres-11] 4119 ternary resolvents (134 bin, 3985 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1106236 penalty 4 = 4 + 0
c [card-5] found 180 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1106236 for elimination
c [card-5] 180 out of 180 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 1769978 penalty 2 = 2 + 0
c [gauss-5] extracted 1588 xors of average arity 3.0
c [gauss-5] connected 4723 occurrences of 589 variables (average 8.0)
c [gauss-5] limit 1769978 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [decomp-47] removed 18 variables
c [gauss-5] exported 1 unary, 0 binary and 1 ternary equations
c [basicprobe-5] limit 176997850 penalty 0 = 0 + 0
c [basicprobe-5-0] 3731 sched 41%, 6 failed, 0 lifted, 1402 hbrs
c [decomp-49] removed 12 variables
c [basicprobe-5-1] 5163 sched 57%, 2 failed, 0 lifted, 334 hbrs
c [decomp-50] removed 5 variables
c [basicprobe-5-2] 5139 sched 57%, 0 failed, 0 lifted, 30 hbrs
c [basicprobe-5-3] 5138 sched 57%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-5-4] 5138 sched 57%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-5-5] 5137 sched 57%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-5-6] 5137 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-7] 5137 sched 57%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-5-8] 5137 sched 57%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 8 units = 8 failed (100%) + 0 lifted (0%)
c [basicprobe-5-8] removed 17 variables, found 1797 hbrs
c [bate-4] eliminated 5 asymmetric tautologies during probing
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 458 transitive binary clauses
c [cce-7] limit of 176997850 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 76 (1%) of length 12
c [cce-7-1] eliminated 2 clauses out of 204 (1%) of length 10
c [cce-7-1] eliminated 9 clauses out of 412 (2%) of length 9
c [cce-7-1] eliminated 25 clauses out of 646 (4%) of length 8
c [cce-7-1] eliminated 21 clauses out of 1286 (2%) of length 7
c [cce-7-1] eliminated 65 clauses out of 2481 (3%) of length 6
c [cce-7-1] eliminated 199 clauses out of 5322 (4%) of length 5
c [cce-7-1] eliminated 342 clauses out of 11692 (3%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 664 large clauses in 106721226 steps
c [cce-7-1] allowing another 53360613 steps for small clauses
c [cce-7-1] scheduling 22170 clauses = 9806 binary + 12364 ternary
c [cce-7-1] tried to eliminate 22170 small clauses 100%
c [cce-7-1] eliminated 202 binary clauses 2%
c [cce-7-1] eliminated 286 ternary clauses 2%
c [cce-7-1] eliminated 488 small clauses 2%
c [cce-7-1] eliminated 488 small clauses in 107507562 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 1152 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 403 (0%) of length 9
c [cce-7-2] eliminated 22 clauses out of 621 (4%) of length 8
c [cce-7-2] eliminated 28 clauses out of 1265 (2%) of length 7
c [cce-7-2] eliminated 48 clauses out of 2416 (2%) of length 6
c [cce-7-2] eliminated 115 clauses out of 5123 (2%) of length 5
c [cce-7-2] eliminated 12 clauses out of 11350 (0%) of length 4
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 226 large clauses in 69490474 steps
c [cce-7-2] allowing another 34745237 steps for small clauses
c [cce-7-2] scheduling 21682 clauses = 9604 binary + 12078 ternary
c [cce-7-2] tried to eliminate 11388 small clauses 53%
c [cce-7-2] eliminated 50 binary clauses 1%
c [cce-7-2] eliminated 70 ternary clauses 1%
c [cce-7-2] eliminated 120 small clauses 1%
c [cce-7-2] eliminated 120 small clauses in 69490294 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 346 covered clauses in round 2
c [cce-7] eliminated 1498 covered clauses in TOTAL during 2 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 9016 variables 100%
c [elim-11] limit of 707991400 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 351 variables 4% in round 1 in 15719836 steps
c [elim-11-1] backward subsumption/strengthening limit 15719800
c [elim-11-1-1] backward checking 944 touched variables 10%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 13 clauses in 1446855 steps
c [elim-11-1] rescheduled 41 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 114155 steps
c [elim-11-2] backward subsumption/strengthening limit 114100
c [elim-11-2-1] backward checking 19 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 54962 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 352 = 4% variables out of 9016 scheduled
c [bca-9] limit of 10000000 steps and 98017 added (scaled 2)
c [bca-9] 2856 out of 17330 literals actually usable 16%
c [bca-9] added 23 blocked clauses in 128288 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 106198710 penalty 0 = 0 + 0
c [sweep-11-1] 1258 pos 45.4% + 1515 neg 54.6% = 2773 sched 32.0% ret 5891
c [sweep-11-1] 18207899 steps 797 queries 28.22 avg class size
c [sweep-11-1] 12886 decisions 752 SAT calls 50.38 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-57] removed 166 variables
c [sweep-11-1] removed 166 vars (0 failed, 170 eqs, 155 impls)
c [sweep-11-2] 3706 pos 43.6% + 4792 neg 56.4% = 8498 sched 100.0% ret 0
c [sweep-11-2] 29050321 steps 1022 queries 27.40 avg class size
c [sweep-11-2] 19012 decisions 979 SAT calls 60.12 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-58] removed 156 variables
c [sweep-11-2] removed 156 vars (0 failed, 172 eqs, 148 impls)
c [sweep-11-3] 3645 pos 43.7% + 4697 neg 56.3% = 8342 sched 100.0% ret 0
c [sweep-11-3] 27299728 steps 934 queries 34.13 avg class size
c [sweep-11-3] 18120 decisions 910 SAT calls 64.64 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-59] removed 75 variables
c [sweep-11-3] removed 75 vars (0 failed, 96 eqs, 66 impls)
c [sweep-11] removed 397 vars in TOTAL (3 rounds, 2750 queries)
c [sort-queue-15] sorted 3906 enqueued variables after 691475 conflicts
c [score-dist-15] active 4361 (53%), one 3906 (47%), zero 0 (0%)
c [score-dist-15] max exp 611, different 410 (67%)
c [score-dist-15] median active exp 498, avg 454.9
c [simplification-15] removed 784 variables 8.7% (8267 remain 16%)
c [simplification-15] removed 3013 irredundant clauses 5.9% (48444 remain 32%)
c [simplification-15] maximum reduction of 9% = max (9%, 6%)
c [simplification-15] large reduction 9% >= 5% limit
c [simplification-15] next conflict interval 6914 = min (691475/100, 179994)
c [simplification-15] penalized conflict interval 6914 = 1 * 6914
c [simplification-15] hard conflict limit 708389 (soft 698389 + delta 10000)
c [simplification-15] new conflict limit 698389 (hard 708389)
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 -  159.0    8267    48443    697734   91429  16802 19994   10    41   20  24%    739    7    9    9  103%
c 
c [simplification-16] limit 698389 conflicts (hard 708389) hit after 698389 conflicts
c [quatres-12] found 20838 quaternary clauses 25% in total
c [quatres-12-1] removed 105 duplicate quaternary clauses
c [quatres-12-1] added 14 double-self-subsuming ternary resolvents
c [quatres-12-2] added 124 single-self-subsuming ternary resolvents
c [quatres-12-2] added 333 quaternary resolvents
c [ternres-12] limit 35859879 with penalty 0 = 0 + 0
c [ternres-12] all 8267 free variables schedulable
c [ternres-12] 3398 ternary resolvents (60 bin, 3338 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-60] removed 5 variables
c [simpleprobe-6] all 8262 free variables schedulable
c [simpleprobe-6] limit 143439516 penalty 0 = 0 + 0
c [decomp-61] removed 30 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 30 variables, found 2748 hbrs, 3 units
c [unhide-10] limit 3585987 with penalty 1 = 1 + 0
c [unhide-10-15] 0 units, 0 failed, 4594 tauts, 0 hbrs, 19135 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 674 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 8232 variables 100%
c [block-7] limit of 179299395 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 451 blocked clauses
c [block-7] 451 < 1/100 * 47923 = 479 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 1792993950 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-8-1] eliminated 3 clauses out of 50 (6%) of length 13
c [cce-8-1] eliminated 2 clauses out of 70 (3%) of length 12
c [cce-8-1] eliminated 11 clauses out of 118 (9%) of length 11
c [cce-8-1] eliminated 23 clauses out of 213 (11%) of length 10
c [cce-8-1] eliminated 26 clauses out of 381 (7%) of length 9
c [cce-8-1] eliminated 28 clauses out of 584 (5%) of length 8
c [cce-8-1] eliminated 77 clauses out of 1206 (6%) of length 7
c [cce-8-1] eliminated 158 clauses out of 2292 (7%) of length 6
c [cce-8-1] eliminated 348 clauses out of 4853 (7%) of length 5
c [cce-8-1] eliminated 497 clauses out of 10730 (5%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1174 large clauses in 47396335 steps
c [cce-8-1] allowing another 23698167 steps for small clauses
c [cce-8-1] scheduling 15502 clauses = 8943 binary + 6559 ternary
c [cce-8-1] tried to eliminate 15502 small clauses 100%
c [cce-8-1] eliminated 94 binary clauses 1%
c [cce-8-1] eliminated 214 ternary clauses 3%
c [cce-8-1] eliminated 308 small clauses 2%
c [cce-8-1] eliminated 308 small clauses in 49515341 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 1482 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 22141245 steps for small clauses
c [cce-8-2] scheduling 15195 clauses = 8849 binary + 6346 ternary
c [cce-8-2] tried to eliminate 15195 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 1482 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 8190 variables 100%
c [elim-12] limit of 717197580 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 287 variables 4% in round 1 in 13835164 steps
c [elim-12-1] backward subsumption/strengthening limit 13835100
c [elim-12-1-1] backward checking 1317 touched variables 16%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 23 clauses in 2296479 steps
c [elim-12-1] rescheduled 47 variables 1% by backward subsumption
c [elim-12-2] eliminated 8 variables 0% in round 2 in 3569115 steps
c [elim-12-2] backward subsumption/strengthening limit 3569100
c [elim-12-2-1] backward checking 43 touched variables 1%
c [elim-12-2-1] incomplete backward checking 29 remain 67%
c [elim-12-2] subsumed 0 and strengthened 3 clauses in 3571533 steps
c [elim-12-2] rescheduled 6 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 3200636 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 295 = 4% variables out of 8190 scheduled
c [bca-10] limit of 10000000 steps and 90578 added (scaled 2)
c [bca-10] 2672 out of 15792 literals actually usable 17%
c [bca-10] added 19 blocked clauses in 93890 steps
c [sweep-12] limit 10757963 penalty 0 = 0 + 0
c [sweep-12-1] 3505 pos 44.4% + 4390 neg 55.6% = 7895 sched 100.0% ret 0
c [sweep-12-1] 10758138 steps 411 queries 65.28 avg class size
c [sweep-12-1] 8326 decisions 410 SAT calls 54.49 avg env size
c [sweep-12-1] 1625 variables remain 21% (6270 retained 79%)
c [decomp-62] removed 17 variables
c [sweep-12-1] removed 17 vars (0 failed, 18 eqs, 19 impls)
c [sweep-12] removed 17 vars in TOTAL (1 rounds, 410 queries)
c [sort-queue-16] sorted 5074 enqueued variables after 698389 conflicts
c [score-dist-16] active 2804 (36%), one 5074 (64%), zero 0 (0%)
c [score-dist-16] max exp 650, different 217 (33%)
c [score-dist-16] median active exp 534, avg 530.5
c [simplification-16] removed 389 variables 4.7% (7878 remain 15%)
c [simplification-16] removed 3444 irredundant clauses 7.1% (44999 remain 30%)
c [simplification-16] maximum reduction of 7% = max (5%, 7%)
c [simplification-16] large reduction 7% >= 5% limit
c [simplification-16] next conflict interval 6983 = min (698389/100, 179994)
c [simplification-16] penalized conflict interval 6983 = 1 * 6983
c [simplification-16] hard conflict limit 715372 (soft 705372 + delta 10000)
c [simplification-16] new conflict limit 705372 (hard 715372)
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  163.5    7877    44999    699039   88772  17680 17872   10    46   22  21%    745   12   10    9  114%
c 
c [simplification-17] limit 705372 conflicts (hard 715372) hit after 715372 conflicts
c [quatres-13] found 19475 quaternary clauses 24% in total
c [quatres-13-1] removed 54 duplicate quaternary clauses
c [quatres-13-2] added 104 single-self-subsuming ternary resolvents
c [quatres-13-2] added 361 quaternary resolvents
c [ternres-13] limit 36643120 with penalty 0 = 0 + 0
c [ternres-13] all 7877 free variables schedulable
c [ternres-13] 3281 ternary resolvents (85 bin, 3196 trn)
c [ternres-13] 1 variables remain 0% (7876 retained 100%)
c [gauss-6] limit 3664312 penalty 1 = 1 + 0
c [gauss-6] extracted 2792 xors of average arity 3.1
c [gauss-6] connected 8584 occurrences of 561 variables (average 15.3)
c [gauss-6] limit 3664312 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 1 ternary equations
c [treelook-6] limit 3664312 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 15061 literals 96%
c [treelook-6] scheduling used 540432 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3664312 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3681344 steps
c [treelook-6] 14275 literals remain 91%
c [treelook-6] 7272 variables remain to probed next time 92%
c [decomp-64] removed 4 variables
c [treelook-6] removed 5 variables, found 6477 hbrs
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 714 transitive binary clauses
c [cce-9] limit of 183215603 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-9-1] eliminated 9 clauses out of 109 (8%) of length 11
c [cce-9-1] eliminated 4 clauses out of 200 (2%) of length 10
c [cce-9-1] eliminated 10 clauses out of 366 (3%) of length 9
c [cce-9-1] eliminated 43 clauses out of 616 (7%) of length 8
c [cce-9-1] eliminated 58 clauses out of 1218 (5%) of length 7
c [cce-9-1] eliminated 89 clauses out of 2207 (4%) of length 6
c [cce-9-1] eliminated 134 clauses out of 4453 (3%) of length 5
c [cce-9-1] eliminated 260 clauses out of 10121 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 608 large clauses in 72336469 steps
c [cce-9-1] allowing another 36168234 steps for small clauses
c [cce-9-1] scheduling 19341 clauses = 8437 binary + 10904 ternary
c [cce-9-1] tried to eliminate 19341 small clauses 100%
c [cce-9-1] eliminated 175 binary clauses 2%
c [cce-9-1] eliminated 238 ternary clauses 2%
c [cce-9-1] eliminated 413 small clauses 2%
c [cce-9-1] eliminated 413 small clauses in 74918877 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 1021 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 100 (1%) of length 11
c [cce-9-2] eliminated 4 clauses out of 1160 (0%) of length 7
c [cce-9-2] eliminated 6 clauses out of 2118 (0%) of length 6
c [cce-9-2] eliminated 8 clauses out of 4319 (0%) of length 5
c [cce-9-2] eliminated 22 clauses out of 9861 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 41 large clauses in 68983725 steps
c [cce-9-2] allowing another 34491862 steps for small clauses
c [cce-9-2] scheduling 18928 clauses = 8262 binary + 10666 ternary
c [cce-9-2] tried to eliminate 18928 small clauses 100%
c [cce-9-2] eliminated 13 binary clauses 0%
c [cce-9-2] eliminated 16 ternary clauses 0%
c [cce-9-2] eliminated 29 small clauses 0%
c [cce-9-2] eliminated 29 small clauses in 71734320 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 70 covered clauses in round 2
c [cce-9-3] eliminated 1 clauses out of 1156 (0%) of length 7
c [cce-9-3] eliminated 1 clauses out of 2112 (0%) of length 6
c [cce-9-3] eliminated 1 clauses out of 4311 (0%) of length 5
c [cce-9-3] incomplete large round (ACCE)
c [cce-9-3] eliminated 3 large clauses in 36562407 steps
c [cce-9-3] allowing another 18281203 steps for small clauses
c [cce-9-3] scheduling 18899 clauses = 8249 binary + 10650 ternary
c [cce-9-3] tried to eliminate 8373 small clauses 44%
c [cce-9-3] eliminated 2 binary clauses 0%
c [cce-9-3] eliminated 2 small clauses 0%
c [cce-9-3] eliminated 2 small clauses in 36562500 steps
c [cce-9-3] incomplete small round (ACCE)
c [cce-9-3] eliminated 5 covered clauses in round 3
c [cce-9] eliminated 1096 covered clauses in TOTAL during 3 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 7872 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 181 variables 2% in round 1 in 13119472 steps
c [elim-13-1] backward subsumption/strengthening limit 13119400
c [elim-13-1-1] backward checking 678 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 5 and strengthened 3 clauses in 1141283 steps
c [elim-13-1] rescheduled 28 variables 0% by backward subsumption
c [elim-13-2] eliminated 3 variables 0% in round 2 in 3071741 steps
c [elim-13-2] backward subsumption/strengthening limit 3071700
c [elim-13-2-1] backward checking 23 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 34193 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 184 = 2% variables out of 7872 scheduled
c [bca-11] limit of 10000000 steps and 87862 added (scaled 2)
c [bca-11] 2452 out of 15378 literals actually usable 16%
c [bca-11] added 2 blocked clauses in 109193 steps
c [sweep-13] limit 10992936 penalty 0 = 0 + 0
c [sweep-13-1] 650 pos 41.5% + 916 neg 58.5% = 1566 sched 20.4% ret 6122
c [sweep-13-1] 10997831 steps 377 queries 21.60 avg class size
c [sweep-13-1] 6287 decisions 374 SAT calls 58.99 avg env size
c [sweep-13-1] 244 variables remain 3% (7444 retained 97%)
c [decomp-65] removed 35 variables
c [sweep-13-1] removed 35 vars (0 failed, 33 eqs, 26 impls)
c [sweep-13] removed 35 vars in TOTAL (1 rounds, 376 queries)
c [sort-queue-17] sorted 4737 enqueued variables after 715372 conflicts
c [score-dist-17] active 2916 (38%), one 4737 (62%), zero 0 (0%)
c [score-dist-17] max exp 841, different 249 (30%)
c [score-dist-17] median active exp 756, avg 733.6
c [simplification-17] removed 224 variables 2.8% (7653 remain 15%)
c [simplification-17] removed 1369 irredundant clauses 3.0% (43630 remain 29%)
c [simplification-17] maximum reduction of 3% = max (3%, 3%)
c [simplification-17] geometric conflict interval increment 44998 = 179994 / 4
c [simplification-17] new conflict interval 224992
c [simplification-17] penalized conflict interval 224992 = 1 * 224992
c [simplification-17] hard conflict limit 1052860 (soft 940364 + delta 112496)
c [simplification-17] new conflict limit 940364 (hard 1052860)
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 -  181.1    7653    43630    744273   92990  20122 22413   10    35   28  28%   -415   -0   11    9  121%
c -  188.5    7653    43630    787080   96135  20142 22415    9    39   28  23%    275   -7    7    9   77%
c -  195.2    7653    43630    829667   97908  20168 22417    8    27   28  31%    633  -19    8    9   87%
c -  204.0    7653    43630    876317  100448  20188 22418   11    44   28  25%    832    5   12    9  128%
c -  213.3    7653    43630    921642  103015  20224 22419   10    47   28  22%    928    8   12    9  124%
c 
c [simplification-18] limit 940364 conflicts (hard 1052860) hit after 940364 conflicts
c [quatres-14] found 19610 quaternary clauses 21% in total
c [quatres-14-1] removed 16 duplicate quaternary clauses
c [quatres-14-1] added 12 double-self-subsuming ternary resolvents
c [quatres-14-2] added 155 single-self-subsuming ternary resolvents
c [quatres-14-2] added 257 quaternary resolvents
c [ternres-14] limit 52527549 with penalty 0 = 0 + 0
c [ternres-14] 1 schedulable variables 0%
c [ternres-14] 3411 ternary resolvents (39 bin, 3372 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-7] limit 10505509 penalty 0 = 0 + 0
c [gauss-7] extracted 2801 xors of average arity 3.1
c [gauss-7] connected 8619 occurrences of 556 variables (average 15.5)
c [gauss-7] limit 10505509 penalty 0 = 0 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-66] removed 2 variables
c [basicprobe-6] limit 262637746 penalty 0 = 0 + 0
c [basicprobe-6-0] 4412 sched 58%, 4 failed, 0 lifted, 675 hbrs
c [decomp-67] removed 10 variables
c [basicprobe-6-1] 4397 sched 58%, 0 failed, 0 lifted, 39 hbrs
c [basicprobe-6-2] 4397 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-3] 4397 sched 58%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-6-4] 4397 sched 58%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-6-5] 4397 sched 58%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-5] fully completed probing
c [basicprobe-6-5] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-6-5] removed 10 variables, found 724 hbrs
c [bate-5] eliminated 11 asymmetric tautologies during probing
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 427 transitive binary clauses
c [cce-10] limit of 262637746 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 74 (3%) of length 12
c [cce-10-1] eliminated 2 clauses out of 110 (2%) of length 11
c [cce-10-1] eliminated 5 clauses out of 200 (2%) of length 10
c [cce-10-1] eliminated 8 clauses out of 379 (2%) of length 9
c [cce-10-1] eliminated 10 clauses out of 589 (2%) of length 8
c [cce-10-1] eliminated 6 clauses out of 1169 (1%) of length 7
c [cce-10-1] eliminated 27 clauses out of 2151 (1%) of length 6
c [cce-10-1] eliminated 53 clauses out of 4315 (1%) of length 5
c [cce-10-1] eliminated 84 clauses out of 9806 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 197 large clauses in 42112533 steps
c [cce-10-1] allowing another 21056266 steps for small clauses
c [cce-10-1] scheduling 14107 clauses = 8100 binary + 6007 ternary
c [cce-10-1] tried to eliminate 14107 small clauses 100%
c [cce-10-1] eliminated 7 binary clauses 0%
c [cce-10-1] eliminated 27 ternary clauses 0%
c [cce-10-1] eliminated 34 small clauses 0%
c [cce-10-1] eliminated 34 small clauses in 43470802 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 231 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 20774109 steps for small clauses
c [cce-10-2] scheduling 14073 clauses = 8093 binary + 5980 ternary
c [cce-10-2] tried to eliminate 14073 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 231 covered clauses in TOTAL during 2 rounds
c [cce-10] 231 < 1/100 * 43535 = 435 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 7641 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 51 variables 1% in round 1 in 13031945 steps
c [elim-14-1] backward subsumption/strengthening limit 13031900
c [elim-14-1-1] backward checking 364 touched variables 5%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 8 clauses in 1044889 steps
c [elim-14-1] rescheduled 29 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 190565 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 51 = 1% variables out of 7641 scheduled
c [elim-14] 51 < 1/100 * 7641 = 76 considered unsuccessful
c [bca-12] limit of 10000000 steps and 86861 added (scaled 2)
c [bca-12] 2423 out of 15182 literals actually usable 16%
c [bca-12] added 1 blocked clauses in 123757 steps
c [sweep-14] limit 15758264 penalty 0 = 0 + 0
c [sweep-14-1] 122 pos 50.4% + 120 neg 49.6% = 242 sched 3.2% ret 7348
c [sweep-14-1] 2409722 steps 144 queries 12.94 avg class size
c [sweep-14-1] 2280 decisions 142 SAT calls 56.23 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-72] removed 13 variables
c [sweep-14-1] removed 13 vars (0 failed, 13 eqs, 10 impls)
c [sweep-14-2] 3338 pos 44.1% + 4239 neg 55.9% = 7577 sched 100.0% ret 0
c [sweep-14-2] 13349281 steps 278 queries 87.90 avg class size
c [sweep-14-2] 7693 decisions 279 SAT calls 78.14 avg env size
c [sweep-14-2] 2524 variables remain 33% (5053 retained 67%)
c [decomp-73] removed 10 variables
c [sweep-14-2] removed 10 vars (0 failed, 10 eqs, 9 impls)
c [sweep-14] removed 23 vars in TOTAL (2 rounds, 420 queries)
c [sort-queue-18] sorted 3686 enqueued variables after 940364 conflicts
c [score-dist-18] active 3881 (51%), one 3686 (49%), zero 0 (0%)
c [score-dist-18] max exp 617, different 310 (50%)
c [score-dist-18] median active exp 516, avg 477.9
c [simplification-18] removed 86 variables 1.1% (7567 remain 15%)
c [simplification-18] removed 506 irredundant clauses 1.2% (43124 remain 28%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 112496 = 224992 / 2
c [simplification-18] new conflict interval 337488
c [simplification-18] penalized conflict interval 337488 = 1 * 337488
c [simplification-18] hard conflict limit 1446596 (soft 1277852 + delta 168744)
c [simplification-18] new conflict limit 1277852 (hard 1446596)
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 -  227.6    7567    43124    967801  103877  21604 21379   11    39   30  28%    977   -0   10   10  100%
c -  234.6    7567    43124   1014295  108512  21611 21381   10    53   30  18%   1001    9   11   10  114%
c -  242.1    7567    43124   1060232  111672  21616 21383    9    41   31  22%   1012    5   10   10  100%
c -  248.3    7567    43124   1111186  112435  21623 21385    8     9   31  87%   1019  -15    9    9   96%
c i  251.2    7566    43124   1137665  130069  21691 21401    7     8   37  92%   1020  -12    5    9   56%
c -  258.5    6014    43123   1163727  112526  21697 21402   11    39   31  28%  -3656   15   12    9  130%
c -  270.2    6014    43123   1213019  115293  21713 21410   10    34   31  29%  -1182    2    8    9   83%
c -  281.7    6014    43123   1262687  117924  21726 21411   10    38   31  26%    -10    7    8   10   80%
c 
c [simplification-19] limit 1277852 conflicts (hard 1446596) hit after 1277853 conflicts
c [quatres-15] found 10950 quaternary clauses 15% in total
c [quatres-15-1] removed 8 duplicate quaternary clauses
c [quatres-15-2] added 78 single-self-subsuming ternary resolvents
c [quatres-15-2] added 510 quaternary resolvents
c [ternres-15] limit 79304767 with penalty 0 = 0 + 0
c [ternres-15] all 6014 free variables schedulable
c [ternres-15] 3523 ternary resolvents (54 bin, 3469 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-74] removed 2507 variables
c [simpleprobe-7] all 5060 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-75] removed 155 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 155 variables, found 7326 hbrs, 38 units
c [unhide-11] limit 3965238 with penalty 2 = 2 + 0
c [unhide-11-18] 1 units, 2 failed, 7540 tauts, 0 hbrs, 59638 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1088 transitive binary clauses
c [transred-15] found 1 units
c [block-8] scheduling all variables this time
c [block-8] scheduled 4901 variables 100%
c [block-8] limit of 198261919 steps penalty 2 = 2 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 660 blocked clauses
c [bca-13] limit of 10000000 steps and 51875 added (scaled 2)
c [bca-13] 1532 out of 9516 literals actually usable 16%
c [bca-13] added 4 blocked clauses in 114411 steps
c [sweep-15] limit 23791430 penalty 0 = 0 + 0
c [sweep-15-1] 703 pos 49.5% + 718 neg 50.5% = 1421 sched 29.9% ret 3336
c [sweep-15-1] 9458708 steps 370 queries 13.37 avg class size
c [sweep-15-1] 5642 decisions 336 SAT calls 61.23 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-76] removed 126 variables
c [sweep-15-1] removed 126 vars (0 failed, 59 eqs, 51 impls)
c [sweep-15-2] 2158 pos 46.6% + 2473 neg 53.4% = 4631 sched 100.0% ret 0
c [sweep-15-2] 14481364 steps 371 queries 42.35 avg class size
c [sweep-15-2] 8073 decisions 352 SAT calls 76.04 avg env size
c [sweep-15-2] 425 variables remain 9% (4205 retained 91%)
c [decomp-77] removed 36 variables
c [sweep-15-2] removed 36 vars (0 failed, 37 eqs, 33 impls)
c [sweep-15] removed 162 vars in TOTAL (2 rounds, 739 queries)
c [sort-queue-19] sorted 1420 enqueued variables after 1277853 conflicts
c [score-dist-19] active 3175 (69%), one 1420 (31%), zero 0 (0%)
c [score-dist-19] max exp 745, different 325 (44%)
c [score-dist-19] median active exp 587, avg 570.4
c [simplification-19] removed 1419 variables 23.6% (4595 remain 9%)
c [simplification-19] removed 18200 irredundant clauses 42.2% (24923 remain 16%)
c [simplification-19] maximum reduction of 42% = max (24%, 42%)
c [simplification-19] large reduction 42% >= 5% limit
c [simplification-19] next conflict interval 12778 = min (1277853/100, 337488)
c [simplification-19] penalized conflict interval 12778 = 1 * 12778
c [simplification-19] hard conflict limit 1300631 (soft 1290631 + delta 10000)
c [simplification-19] new conflict limit 1290631 (hard 1300631)
c 
c [simplification-20] limit 1290631 conflicts (hard 1300631) hit after 1290631 conflicts
c [quatres-16] found 12224 quaternary clauses 16% in total
c [quatres-16-1] removed 118 duplicate quaternary clauses
c [quatres-16-1] added 4 double-self-subsuming ternary resolvents
c [quatres-16-2] added 248 single-self-subsuming ternary resolvents
c [quatres-16-2] added 229 quaternary resolvents
c [ternres-16] limit 80368654 with penalty 0 = 0 + 0
c [ternres-16] all 4595 free variables schedulable
c [ternres-16] 7519 ternary resolvents (156 bin, 7363 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-8] limit 8036865 penalty 1 = 1 + 0
c [gauss-8] extracted 1811 xors of average arity 3.0
c [gauss-8] connected 5521 occurrences of 411 variables (average 13.4)
c [gauss-8] limit 8036865 penalty 1 = 1 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-78] removed 18 variables
c [treelook-7] limit 8036865 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 8748 literals 96%
c [treelook-7] scheduling used 482066 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 8036865 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 8036911 steps
c [treelook-7] 3042 literals remain 33%
c [treelook-7] 2532 variables remain to probed next time 56%
c [decomp-79] removed 40 variables
c [treelook-7] removed 57 variables, found 10903 hbrs
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1330 transitive binary clauses
c [cce-11] limit of 200921635 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-11-1] eliminated 7 clauses out of 29 (24%) of length 12
c [cce-11-1] eliminated 5 clauses out of 26 (19%) of length 11
c [cce-11-1] eliminated 9 clauses out of 76 (12%) of length 10
c [cce-11-1] eliminated 10 clauses out of 83 (12%) of length 9
c [cce-11-1] eliminated 27 clauses out of 227 (12%) of length 8
c [cce-11-1] eliminated 39 clauses out of 358 (11%) of length 7
c [cce-11-1] eliminated 104 clauses out of 650 (16%) of length 6
c [cce-11-1] eliminated 286 clauses out of 1788 (16%) of length 5
c [cce-11-1] eliminated 574 clauses out of 5645 (10%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 1062 large clauses in 20378910 steps
c [cce-11-1] allowing another 10189455 steps for small clauses
c [cce-11-1] scheduling 9223 clauses = 4794 binary + 4429 ternary
c [cce-11-1] tried to eliminate 9223 small clauses 100%
c [cce-11-1] eliminated 437 binary clauses 9%
c [cce-11-1] eliminated 445 ternary clauses 10%
c [cce-11-1] eliminated 882 small clauses 10%
c [cce-11-1] eliminated 882 small clauses in 21374822 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 1944 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 9 (11%) of length 13
c [cce-11-2] eliminated 3 clauses out of 319 (1%) of length 7
c [cce-11-2] eliminated 5 clauses out of 546 (1%) of length 6
c [cce-11-2] eliminated 13 clauses out of 1502 (1%) of length 5
c [cce-11-2] eliminated 22 clauses out of 5071 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 44 large clauses in 19298511 steps
c [cce-11-2] allowing another 9649255 steps for small clauses
c [cce-11-2] scheduling 8345 clauses = 4357 binary + 3988 ternary
c [cce-11-2] tried to eliminate 8345 small clauses 100%
c [cce-11-2] eliminated 31 binary clauses 1%
c [cce-11-2] eliminated 31 ternary clauses 1%
c [cce-11-2] eliminated 62 small clauses 1%
c [cce-11-2] eliminated 62 small clauses in 19906571 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 106 covered clauses in round 2
c [cce-11-3] eliminated 1 clauses out of 1489 (0%) of length 5
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 1 large clauses in 18996414 steps
c [cce-11-3] allowing another 9498207 steps for small clauses
c [cce-11-3] scheduling 8283 clauses = 4326 binary + 3957 ternary
c [cce-11-3] tried to eliminate 8283 small clauses 100%
c [cce-11-3] eliminated 5 binary clauses 0%
c [cce-11-3] eliminated 6 ternary clauses 0%
c [cce-11-3] eliminated 11 small clauses 0%
c [cce-11-3] eliminated 11 small clauses in 19700281 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 12 covered clauses in round 3
c [cce-11] eliminated 2062 covered clauses in TOTAL during 3 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 4520 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 834 variables 18% in round 1 in 4328139 steps
c [elim-15-1] backward subsumption/strengthening limit 4328100
c [elim-15-1-1] backward checking 1603 touched variables 35%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 4 and strengthened 23 clauses in 402667 steps
c [elim-15-1] rescheduled 80 variables 2% by backward subsumption
c [elim-15-2] eliminated 4 variables 0% in round 2 in 447659 steps
c [elim-15-2] backward subsumption/strengthening limit 447600
c [elim-15-2-1] backward checking 38 touched variables 1%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 55521 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 838 = 19% variables out of 4520 scheduled
c [bca-14] limit of 10000000 steps and 42593 added (scaled 2)
c [bca-14] 919 out of 7366 literals actually usable 12%
c [bca-14] added 9 blocked clauses in 116815 steps
c [sweep-16] limit 24110596 penalty 0 = 0 + 0
c [sweep-16-1] 113 pos 45.0% + 138 neg 55.0% = 251 sched 6.8% ret 3431
c [sweep-16-1] 4501059 steps 120 queries 8.70 avg class size
c [sweep-16-1] 2784 decisions 121 SAT calls 74.99 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-80] removed 9 variables
c [sweep-16-1] removed 9 vars (0 failed, 8 eqs, 3 impls)
c [sweep-16-2] 1707 pos 46.5% + 1966 neg 53.5% = 3673 sched 100.0% ret 0
c [sweep-16-2] 17738872 steps 406 queries 20.82 avg class size
c [sweep-16-2] 9242 decisions 424 SAT calls 83.71 avg env size
c [sweep-16-2] fully completed sweeping round
c [decomp-81] removed 28 variables
c [sweep-16-2] removed 28 vars (0 failed, 31 eqs, 11 impls)
c [sweep-16-3] 1695 pos 46.5% + 1950 neg 53.5% = 3645 sched 100.0% ret 0
c [sweep-16-3] 1911410 steps 15 queries 480.07 avg class size
c [sweep-16-3] 1009 decisions 14 SAT calls 155.71 avg env size
c [sweep-16-3] 3303 variables remain 91% (342 retained 9%)
c [sweep-16-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-16] removed 37 vars in TOTAL (3 rounds, 538 queries)
c [sort-queue-20] sorted 1067 enqueued variables after 1290631 conflicts
c [score-dist-20] active 2578 (71%), one 1067 (29%), zero 0 (0%)
c [score-dist-20] max exp 784, different 339 (43%)
c [score-dist-20] median active exp 680, avg 605.6
c [simplification-20] removed 950 variables 20.7% (3645 remain 7%)
c [simplification-20] removed 3946 irredundant clauses 15.8% (20977 remain 14%)
c [simplification-20] maximum reduction of 21% = max (21%, 16%)
c [simplification-20] large reduction 21% >= 5% limit
c [simplification-20] next conflict interval 12906 = min (1290631/100, 337488)
c [simplification-20] penalized conflict interval 12906 = 1 * 12906
c [simplification-20] hard conflict limit 1313537 (soft 1303537 + delta 10000)
c [simplification-20] new conflict limit 1303537 (hard 1313537)
c 
c [simplification-21] limit 1303537 conflicts (hard 1313537) hit after 1303537 conflicts
c [quatres-17] found 10806 quaternary clauses 14% in total
c [quatres-17-1] removed 23 duplicate quaternary clauses
c [quatres-17-2] added 39 single-self-subsuming ternary resolvents
c [quatres-17-2] added 131 quaternary resolvents
c [ternres-17] limit 81352393 with penalty 0 = 0 + 0
c [ternres-17] all 3645 free variables schedulable
c [ternres-17] 615 ternary resolvents (33 bin, 582 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2542262 penalty 4 = 4 + 0
c [card-6] found 437 at-most-one constraints of average size 3.2
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2542262 for elimination
c [card-6] 437 out of 437 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 2011 sched 55%, 3 failed, 0 lifted, 414 hbrs
c [decomp-84] removed 3 variables
c [basicprobe-7-1] 2016 sched 55%, 0 failed, 0 lifted, 101 hbrs
c [basicprobe-7-2] 2016 sched 55%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-7-3] 2014 sched 55%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-7-4] 2013 sched 55%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-7-5] 2013 sched 55%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-5] fully completed probing
c [basicprobe-7-5] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-7-5] removed 3 variables, found 549 hbrs
c [bate-6] eliminated 21 asymmetric tautologies during probing
c [unhide-12] limit 8135239 with penalty 1 = 1 + 0
c [unhide-12-23] 0 units, 0 failed, 4894 tauts, 0 hbrs, 60300 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 520 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 3642 variables 100%
c [block-9] limit of 400000000 steps penalty 1 = 1 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 35 blocked clauses
c [block-9] 35 < 1/100 * 20904 = 209 considered unsuccessful
c [cce-12] limit of 406761968 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 3 clauses out of 31 (10%) of length 11
c [cce-12-1] eliminated 4 clauses out of 73 (5%) of length 10
c [cce-12-1] eliminated 6 clauses out of 105 (6%) of length 9
c [cce-12-1] eliminated 9 clauses out of 251 (4%) of length 8
c [cce-12-1] eliminated 11 clauses out of 325 (3%) of length 7
c [cce-12-1] eliminated 47 clauses out of 619 (8%) of length 6
c [cce-12-1] eliminated 128 clauses out of 1872 (7%) of length 5
c [cce-12-1] eliminated 169 clauses out of 5219 (3%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 377 large clauses in 8532608 steps
c [cce-12-1] allowing another 4266304 steps for small clauses
c [cce-12-1] scheduling 8907 clauses = 3511 binary + 5396 ternary
c [cce-12-1] tried to eliminate 8907 small clauses 100%
c [cce-12-1] eliminated 23 binary clauses 1%
c [cce-12-1] eliminated 121 ternary clauses 2%
c [cce-12-1] eliminated 144 small clauses 2%
c [cce-12-1] eliminated 144 small clauses in 10622459 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 521 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 4024078 steps for small clauses
c [cce-12-2] scheduling 8764 clauses = 3488 binary + 5276 ternary
c [cce-12-2] tried to eliminate 8764 small clauses 100%
c [cce-12-2] eliminated 1 ternary clauses 0%
c [cce-12-2] eliminated 1 small clauses 0%
c [cce-12-2] eliminated 1 small clauses in 10199363 steps
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 1 covered clauses in round 2
c [cce-12-3] completed large round (ATE)
c [cce-12-3] allowing another 4021825 steps for small clauses
c [cce-12-3] scheduling 8763 clauses = 3488 binary + 5275 ternary
c [cce-12-3] tried to eliminate 8763 small clauses 100%
c [cce-12-3] completed small round (ATE)
c [cce-12-3] eliminated 0 covered clauses in round 3
c [cce-12] eliminated 522 covered clauses in TOTAL during 3 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 3642 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 88 variables 2% in round 1 in 3818694 steps
c [elim-16-1] backward subsumption/strengthening limit 3818600
c [elim-16-1-1] backward checking 577 touched variables 16%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 3 clauses in 178872 steps
c [elim-16-1] rescheduled 9 variables 0% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 6426 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 88 = 2% variables out of 3642 scheduled
c [bca-15] limit of 10000000 steps and 40868 added (scaled 2)
c [bca-15] 831 out of 7110 literals actually usable 12%
c [bca-15] added 6 blocked clauses in 125863 steps
c [sweep-17] limit 24405718 penalty 0 = 0 + 0
c [sweep-17-1] 1544 pos 48.0% + 1671 neg 52.0% = 3215 sched 90.5% ret 339
c [sweep-17-1] 17004667 steps 366 queries 20.93 avg class size
c [sweep-17-1] 8890 decisions 363 SAT calls 85.42 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-89] removed 19 variables
c [sweep-17-1] removed 19 vars (0 failed, 22 eqs, 14 impls)
c [sweep-17-2] 1669 pos 47.2% + 1866 neg 52.8% = 3535 sched 100.0% ret 0
c [sweep-17-2] 7403038 steps 129 queries 77.30 avg class size
c [sweep-17-2] 3864 decisions 128 SAT calls 109.65 avg env size
c [sweep-17-2] 1002 variables remain 28% (2533 retained 72%)
c [decomp-90] removed 2 variables
c [sweep-17-2] removed 2 vars (0 failed, 2 eqs, 2 impls)
c [sweep-17] removed 21 vars in TOTAL (2 rounds, 493 queries)
c [sort-queue-21] sorted 1006 enqueued variables after 1303537 conflicts
c [score-dist-21] active 2527 (72%), one 1006 (28%), zero 0 (0%)
c [score-dist-21] max exp 708, different 292 (41%)
c [score-dist-21] median active exp 641, avg 590.2
c [simplification-21] removed 112 variables 3.1% (3533 remain 7%)
c [simplification-21] removed 857 irredundant clauses 4.1% (20119 remain 13%)
c [simplification-21] maximum reduction of 4% = max (3%, 4%)
c [simplification-21] geometric conflict interval increment 67497 = 337488 / 5
c [simplification-21] new conflict interval 404985
c [simplification-21] penalized conflict interval 404985 = 1 * 404985
c [simplification-21] hard conflict limit 1911014 (soft 1708522 + delta 202492)
c [simplification-21] new conflict limit 1708522 (hard 1911014)
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 -  308.8    3533    20119   1322676  100507   6676 13792    9    21   26  43%    610  -12    9    9   98%
c -  319.1    3533    20119   1372278  102470   6705 13796   11    40   26  27%    830    7   12   10  121%
c -  330.6    3533    20119   1422207  104521   6720 13798    9    36   26  26%    933    1    9   10   91%
c -  341.2    3533    20119   1472162  105979   6732 13803   10    36   26  29%    982    2   11   10  117%
c -  353.0    3533    20119   1525620  108786   6771 13808    8    14   26  60%   1005  -16    9    9   94%
c i  355.3    3532    20119   1540846  121673   6810 13817    7     9   32  75%   1009  -17    4    9   49%
c -  367.3    3532    20119   1578581  109485   6823 13818   12    33   26  35%  -2583    4   11   10  117%
c -  380.7    3532    20119   1631952  111200   6842 13818   12    37   27  31%   -573    5   13   10  131%
c -  393.1    3532    20119   1685739  114174   6860 13818   11    38   27  30%    321    5   13   11  127%
c 
c [simplification-22] limit 1708522 conflicts (hard 1911014) hit after 1708522 conflicts
c [quatres-18] found 11066 quaternary clauses 13% in total
c [quatres-18-1] removed 18 duplicate quaternary clauses
c [quatres-18-2] added 33 single-self-subsuming ternary resolvents
c [quatres-18-2] added 128 quaternary resolvents
c [ternres-18] limit 115702144 with penalty 0 = 0 + 0
c [ternres-18] all 3532 free variables schedulable
c [ternres-18] 695 ternary resolvents (33 bin, 662 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-91] removed 2 variables
c [simpleprobe-8] all 3531 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-92] removed 4 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 4 variables, found 2693 hbrs, 1 units
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 853 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 5785107230 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 2 clauses out of 13 (15%) of length 12
c [cce-13-1] eliminated 4 clauses out of 31 (13%) of length 11
c [cce-13-1] eliminated 8 clauses out of 72 (11%) of length 10
c [cce-13-1] eliminated 1 clauses out of 107 (1%) of length 9
c [cce-13-1] eliminated 11 clauses out of 243 (5%) of length 8
c [cce-13-1] eliminated 15 clauses out of 309 (5%) of length 7
c [cce-13-1] eliminated 49 clauses out of 606 (8%) of length 6
c [cce-13-1] eliminated 81 clauses out of 1763 (5%) of length 5
c [cce-13-1] eliminated 111 clauses out of 5020 (2%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 282 large clauses in 15884192 steps
c [cce-13-1] allowing another 7942096 steps for small clauses
c [cce-13-1] scheduling 8541 clauses = 3351 binary + 5190 ternary
c [cce-13-1] tried to eliminate 8541 small clauses 100%
c [cce-13-1] eliminated 58 binary clauses 2%
c [cce-13-1] eliminated 75 ternary clauses 1%
c [cce-13-1] eliminated 133 small clauses 2%
c [cce-13-1] eliminated 133 small clauses in 16079076 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 415 covered clauses in round 1
c [cce-13-2] eliminated 2 clauses out of 106 (2%) of length 9
c [cce-13-2] eliminated 3 clauses out of 294 (1%) of length 7
c [cce-13-2] eliminated 1 clauses out of 557 (0%) of length 6
c [cce-13-2] eliminated 3 clauses out of 1682 (0%) of length 5
c [cce-13-2] eliminated 13 clauses out of 4909 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 22 large clauses in 14794909 steps
c [cce-13-2] allowing another 7397454 steps for small clauses
c [cce-13-2] scheduling 8408 clauses = 3293 binary + 5115 ternary
c [cce-13-2] tried to eliminate 8408 small clauses 100%
c [cce-13-2] eliminated 3 binary clauses 0%
c [cce-13-2] eliminated 3 ternary clauses 0%
c [cce-13-2] eliminated 6 small clauses 0%
c [cce-13-2] eliminated 6 small clauses in 15208022 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 28 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 7359808 steps for small clauses
c [cce-13-3] scheduling 8402 clauses = 3290 binary + 5112 ternary
c [cce-13-3] tried to eliminate 8402 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 443 covered clauses in TOTAL during 3 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 3527 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 66 variables 2% in round 1 in 3600244 steps
c [elim-17-1] backward subsumption/strengthening limit 3600200
c [elim-17-1-1] backward checking 372 touched variables 11%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 2 clauses in 135493 steps
c [elim-17-1] rescheduled 19 variables 1% by backward subsumption
c [elim-17-2] eliminated 1 variables 0% in round 2 in 59594 steps
c [elim-17-2] backward subsumption/strengthening limit 59500
c [elim-17-2-1] backward checking 15 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 14939 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 67 = 2% variables out of 3527 scheduled
c [bca-16] limit of 10000000 steps and 39619 added (scaled 2)
c [bca-16] 735 out of 6922 literals actually usable 11%
c [bca-16] added 1 blocked clauses in 135855 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 493 pos 51.2% + 470 neg 48.8% = 963 sched 27.8% ret 2497
c [sweep-18-1] 11428366 steps 258 queries 15.56 avg class size
c [sweep-18-1] 5242 decisions 262 SAT calls 76.69 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-93] removed 19 variables
c [sweep-18-1] removed 19 vars (0 failed, 20 eqs, 12 impls)
c [sweep-18-2] 1579 pos 45.9% + 1862 neg 54.1% = 3441 sched 100.0% ret 0
c [sweep-18-2] 21660309 steps 385 queries 25.59 avg class size
c [sweep-18-2] 9101 decisions 384 SAT calls 87.04 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-94] removed 23 variables
c [sweep-18-2] removed 23 vars (0 failed, 23 eqs, 22 impls)
c [sweep-18-3] 1572 pos 46.0% + 1846 neg 54.0% = 3418 sched 100.0% ret 0
c [sweep-18-3] 18289628 steps 365 queries 25.35 avg class size
c [sweep-18-3] 7936 decisions 373 SAT calls 87.05 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-95] removed 6 variables
c [sweep-18-3] removed 6 vars (0 failed, 7 eqs, 2 impls)
c [sweep-18] removed 48 vars in TOTAL (3 rounds, 1005 queries)
c [sort-queue-22] sorted 1189 enqueued variables after 1708522 conflicts
c [score-dist-22] active 2223 (65%), one 1189 (35%), zero 0 (0%)
c [score-dist-22] max exp 582, different 279 (48%)
c [score-dist-22] median active exp 477, avg 424.4
c [simplification-22] removed 120 variables 3.4% (3412 remain 7%)
c [simplification-22] removed 636 irredundant clauses 3.2% (19483 remain 13%)
c [simplification-22] maximum reduction of 3% = max (3%, 3%)
c [simplification-22] geometric conflict interval increment 101246 = 404985 / 4
c [simplification-22] new conflict interval 506231
c [simplification-22] penalized conflict interval 506231 = 1 * 506231
c [simplification-22] hard conflict limit 2467868 (soft 2214753 + delta 253115)
c [simplification-22] new conflict limit 2214753 (hard 2467868)
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 -  410.2    3412    19480   1738247  115095   7136 15292   12    33   28  34%    708    1   11   11  106%
c -  418.7    3412    19480   1793954  121209   7139 15292    9    22   29  38%    889   -6    9   10   91%
c -  433.5    3412    19480   1844478  117303   7159 15292   13    37   28  35%    962    6   13   11  124%
c -  446.0    3412    19480   1901762  122098   7179 15301   12    34   29  35%    998    1   13   11  126%
c -  459.7    3412    19480   1956789  124237   7201 15303   11    35   29  33%   1013    4    8   11   71%
c -  472.2    3412    19480   2012263  125740   7215 15304   10    27   29  35%   1019   -3   12   10  117%
c -  485.1    3412    19480   2067728  126711   7235 15310   10    29   29  34%   1022   -1   12   11  110%
c -  501.3    3412    19480   2124716  126762   7249 15313   13    30   29  43%   1023    3   13   11  123%
c -  516.1    3412    19480   2185156  131044   7260 15315   10    29   29  33%   1024    4    7   11   62%
c 
c [simplification-23] limit 2214753 conflicts (hard 2467868) hit after 2215357 conflicts
c [quatres-19] found 11436 quaternary clauses 12% in total
c [quatres-19-1] removed 15 duplicate quaternary clauses
c [quatres-19-1] added 1 double-self-subsuming ternary resolvents
c [quatres-19-2] added 56 single-self-subsuming ternary resolvents
c [quatres-19-2] added 131 quaternary resolvents
c [ternres-19] limit 161928883 with penalty 0 = 0 + 0
c [ternres-19] all 3412 free variables schedulable
c [ternres-19] 381 ternary resolvents (28 bin, 353 trn)
c [ternres-19] fully completed ternary resolution
c [gauss-9] limit 8096444 penalty 2 = 2 + 0
c [gauss-9] extracted 1382 xors of average arity 3.1
c [gauss-9] connected 4290 occurrences of 297 variables (average 14.4)
c [gauss-9] limit 8096444 penalty 2 = 2 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-96] removed 2 variables
c [treelook-8] limit 16192888 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 5546 literals 81%
c [treelook-8] scheduling used 461604 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 16192888 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 6314054 steps
c [treelook-8] fully completed tree based probing
c [decomp-97] removed 2 variables
c [treelook-8] removed 4 variables, found 1589 hbrs
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 850 transitive binary clauses
c [cce-14] limit of 809644418 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 2 clauses out of 26 (8%) of length 11
c [cce-14-1] eliminated 5 clauses out of 103 (5%) of length 9
c [cce-14-1] eliminated 7 clauses out of 536 (1%) of length 6
c [cce-14-1] eliminated 65 clauses out of 1681 (4%) of length 5
c [cce-14-1] eliminated 75 clauses out of 4900 (2%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 154 large clauses in 7520883 steps
c [cce-14-1] allowing another 3760441 steps for small clauses
c [cce-14-1] scheduling 6534 clauses = 3239 binary + 3295 ternary
c [cce-14-1] tried to eliminate 6534 small clauses 100%
c [cce-14-1] eliminated 14 binary clauses 0%
c [cce-14-1] eliminated 65 ternary clauses 2%
c [cce-14-1] eliminated 79 small clauses 1%
c [cce-14-1] eliminated 79 small clauses in 8538586 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 233 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 3681664 steps for small clauses
c [cce-14-2] scheduling 6455 clauses = 3225 binary + 3230 ternary
c [cce-14-2] tried to eliminate 6455 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 233 covered clauses in TOTAL during 2 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 3406 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 34 variables 1% in round 1 in 3506827 steps
c [elim-18-1] backward subsumption/strengthening limit 3506800
c [elim-18-1-1] backward checking 246 touched variables 7%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 3 and strengthened 1 clauses in 115265 steps
c [elim-18-1] rescheduled 8 variables 0% by backward subsumption
c [elim-18-2] eliminated 1 variables 0% in round 2 in 28348 steps
c [elim-18-2] backward subsumption/strengthening limit 28300
c [elim-18-2-1] backward checking 12 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 0 and strengthened 2 clauses in 14299 steps
c [elim-18-2] rescheduled 10 variables 0% by backward subsumption
c [elim-18-3] no variable eliminated in round 3 in 5588 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 35 = 1% variables out of 3406 scheduled
c [bca-17] limit of 10000000 steps and 38747 added (scaled 2)
c [bca-17] 689 out of 6744 literals actually usable 10%
c [bca-17] added 2 blocked clauses in 159549 steps
c [sweep-19] limit 48578665 penalty 0 = 0 + 0
c [sweep-19-1] 1536 pos 45.6% + 1835 neg 54.4% = 3371 sched 100.0% ret 0
c [sweep-19-1] 29252438 steps 399 queries 27.86 avg class size
c [sweep-19-1] 10139 decisions 400 SAT calls 92.51 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-98] removed 41 variables
c [sweep-19-1] removed 41 vars (0 failed, 44 eqs, 24 impls)
c [sweep-19-2] 1524 pos 45.8% + 1806 neg 54.2% = 3330 sched 100.0% ret 0
c [sweep-19-2] 19724104 steps 187 queries 52.69 avg class size
c [sweep-19-2] 5916 decisions 187 SAT calls 94.93 avg env size
c [sweep-19-2] 531 variables remain 16% (2797 retained 84%)
c [decomp-99] removed 17 variables
c [sweep-19-2] removed 17 vars (0 failed, 16 eqs, 8 impls)
c [sweep-19] removed 58 vars in TOTAL (2 rounds, 584 queries)
c [sort-queue-23] sorted 1172 enqueued variables after 2215357 conflicts
c [score-dist-23] active 2141 (65%), one 1172 (35%), zero 0 (0%)
c [score-dist-23] max exp 833, different 261 (31%)
c [score-dist-23] median active exp 730, avg 636.7
c [simplification-23] removed 99 variables 2.9% (3313 remain 6%)
c [simplification-23] removed 423 irredundant clauses 2.2% (19057 remain 13%)
c [simplification-23] maximum reduction of 3% = max (3%, 2%)
c [simplification-23] geometric conflict interval increment 126557 = 506231 / 4
c [simplification-23] new conflict interval 632788
c [simplification-23] penalized conflict interval 632788 = 1 * 632788
c [simplification-23] hard conflict limit 3164539 (soft 2848145 + delta 316394)
c [simplification-23] new conflict limit 2848145 (hard 3164539)
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 -  534.5    3313    19057   2240058  128947   7187 15821   12    24   30  49%   1024   -1   14   11  136%
c -  548.2    3313    19057   2298088  130643   7200 15824   12    29   31  41%   1024    1   14   11  127%
c -  562.2    3313    19057   2358205  133435   7213 15825   11    27   31  42%   1024    0    8   10   77%
c -  578.2    3313    19057   2417585  134365   7228 15825    8    13   31  63%   1024  -13    8   10   79%
c -  595.7    3313    19057   2476299  133660   7243 15827   12    28   31  44%   1024    1   13   11  119%
c i  606.6    3312    19057   2525334  178798   7294 15845    7    10   43  69%   1024  -13    5   10   47%
c -  612.4    3312    19057   2540140  136564   7303 15846   11    25   31  46% -11443    2   10   11   96%
c -  625.7    3312    19057   2602994  139878   7333 15850   10    16   31  61%  -3754   -6   10   10   95%
c i  635.0    3311    19057   2644927  178684   7360 15858   11    26   42  44%  -1496    4   11   10  106%
c -  640.9    3306    19057   2665209  140749   7363 15858   11    16   31  67%  -2218   -6   11   11  102%
c i  644.0    3305    19057   2687313  159768   7373 15860   10    16   40  65%  -1290   -3   14   10  135%
c i  644.0    3304    19057   2687352  159803   7373 15860   10    16   40  65%  -1313   -3   14   10  134%
c i  644.0    3303    19057   2687353  159803   7373 15860   10    16   40  65%  -1314   -3   14   10  133%
c i  644.4    3302    19057   2688404  160750   7378 15860   11    18   41  61%  -1682   -2   13   10  125%
c i  655.6    3299    19057   2727982  197886   7401 15875   14    21   49  64%   -591    0   14   11  126%
c -  656.1    3299    19057   2728874  141838   7403 15878   14    21   31  65%   -927    0   14   11  127%
c i  657.1    3298    19057   2734883  147535   7403 15880   12    22   39  54%   -994    1   12   11  111%
c i  664.7    3297    19057   2771486  181417   7409 15881   13    19   42  68%   -194   -1   14   11  126%
c i  670.0    3296    19057   2796152  196364   7477 15894    7     7   45  94%   -211  -10    5   10   50%
c i  670.2    3291    19057   2797200  197286   7478 15894    8     9   45  90%   -436   -8   10   10  102%
c -  671.8    3291    19057   2801703  145419   7478 15895   11    15   49  70%   -484   -2   12   10  122%
c i  674.1    3290    19057   2813144  155575   7498 15898   12    17   56  69%   -244    0   12   10  115%
c i  680.8    3289    19057   2848020  181191   7543 15909    8     9   59  91%    131   -6    6   10   60%
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  681.5    3268    19057   2851359  183121   7577 15918    7     8   59  90%   -330   -7    5   10   56%
c i  682.0    3261    19057   2853855  184471   7611 15927    7     8   59  90%   -344   -7    5   10   48%
c i  682.0    3243    19057   2853902  184478   7613 15928    7     8   59  90%   -345   -7    5   10   47%
c i  682.1    3232    19057   2854825  184912   7638 15936    7     7   61  90%   -352   -7    5   10   53%
c 0  682.1    3195    19057   2854825  184912   7638 15936    7     7   61  90%   -352   -7    5   10   53%
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 
s UNSATISFIABLE
c
c bate: 108 basic ate = 58 trn 54% + 50 lrg 46% in 6 updates
c bcas: 17 count, 201 added (200 skipped), 1728459 steps
c bkwd: tried 153667 clauses, 307044 lits, 2.00 lits/clause
c bkwd: checked 43605823 occs, 283.77 occs/clause, 142.02 occs/lit
c bkwd: subsumed 2 binary, 30 ternary, 36 large
c bkwd: strengthened 1 binary, 12 ternary (100% self), 371 large (0% self)
c blkd: 9 bces, 6458 removed, 2556524 resolutions, 6594606 steps
c blkd: 4039 blocking literals 4%, 495 pure
c bump: 2874287 bumped seen, 171014049 lits 59.5 on average
c card: 6 count, 0 units, 99 am1, 23687863 steps
c card: 41 rescheduled, 348 eliminated, 15300 resolved, 5995 subsumed
c card: 1190 at-most-one constraints found, average size 3.09
c card: 1190 at-most-one constraints used 100%, average size 3.09
c card: 6 at-most-two constraints found, average size 4.00
c card: 6 at-most-two constraints used 100%, average size 4.00
c cces: 14 cces, 14445 eliminated, 11781 ate 82%, 2664 abce 18%
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: 511854 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 167 gcs, 0 rescored clauses, 1512 rescored vars
c dcps: 99 decompositions, 4613 equivalent 9%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 10790252 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 18 elims, 41948 eliminated 80%, 459 pure 1%
c elms: 51 rounds, 2.8 rounds/bve
c elms: 39245 small 94%, 1749 large 4%
c elms: 78247 tried small, 39245 succeeded 50%, 39002 failed 50%
c elms: 3888 subsumed, 5247 strengthened, 565 blocked
c elms: 5073906 copies, 6811555 resolutions, 2511949 ipos
c elms: 3080285 subchks, 1803498 strchks
c gaus: 9 extractions, 20076 extracted, 3.0 size, 4 max
c gaus: exported 1 units, 1 binary and 5 ternary equations
c gaus: 0 gc, 38940348 steps, 19470174 extr 50%, 943059 elim 2%
c glue: 9.6 orig avg, 9.6 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 95147 = 22800 simple 24% + 57035 trn 60% + 15312 lrg 16%, 1260 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2874287 clauses, 26.1 length
c lrnd: 74978546 lits = 109453008 orig - 34474462 removed 31%
c lrnd: 561444 uips 20%, 2072757 flips 72%
c mins: 2849031 mins 99%, 1007 bin 0%, 24249 size 1%
c mins: 121093274 poisoned searches, 17369064 hits, 14% hit rate
c mins: 210179475 used twice searches, 10901237 hits, 5% hit rate
c move: moved 9327, 2807 bin 30%, 6520 trn 70%
c otfs: 12737 driving 32%, 26467 restarting 68%
c otfs: str 39204, 38669 red 99%, 535 irr 1%
c otfs: str 39204, 0 bin 0%, 1066 trn 3%, 38138 lrg 97%
c otfs: sub 972, 893 red 92%, 79 irr 8%
c otfs: sub 972, 0 bin 0%, 106 trn 11%, 866 lrg 89%
c phas: 1 computed, 13304 set, 3169 pos (24%), 10135 neg (76%)
c prbs: 7 basic, 294872 probed, 86 failed, 3 lifted
c prbs: 8 simple, 211954 probed, 236 failed, 2898 eqs
c prbs: 8 treelook, 13158 probed, 25 failed, 0 lifted
c prom: 932333 locked 15% out of 6366829 tried
c prps: 497240244 props, 43 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 19 count, 7951 quat, 2380 self1, 104 self2, 1170 dup
c queu: 23 sorted, 10790252 next (5837503 steps 0.54)
c queu: 174532056 enq (178140827 steps 1.02), 171014049 deq 98%
c redc: 87369 clauses 13%, 674796 tried 24%, 20 sat 0%
c redc: 120407 lits 1%, 10486820 tried 10%, 20 sat 0%
c redc: 1306 times jump level reduced, 5.0 levels on average
c reds: 54 count, 52867.1 conflicts per reduce
c reds: 0 memlim 0%, 54 arith 100%
c reds: 2065610 collected 87%, 302494 retired 13%
c rmbd: 6034 removed, 5231 red 87%
c rsts: 78720 restarts 100%, 11 skipped 0%
c rsts: 11 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 23 count, 22 confs 96%, 0 vars 0%
c simp: 0 its 0%, 1 bin 4%, 0 trns 0%
c subl: 2874287 count (1276421 tried 0.4), 220614 sub out of 2863967 (7.7%)
c swps: 19 count, 30 rounds, 9471 queries (315.7/round)
c swps: 9190 sat calls, 1086 unsat (3.5% success rate)
c swps: 196380 decisions 21.4, 32199 conflicts 3.5
c swps; 74.9 avg class size, 67.5 avg environment size
c swps: 0 failed, 1080 impls, 1361 equivs
c swp0: 3147 type 0 queries, 900 unsat (28.6%), 2872 sat (91.3%)
c swp1: 6324 type 1 queries, 3198 unsat (50.6%), 5238 sat (82.8%)
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: 27332665 calls to obtain time
c tops: 2670 fixed 5%, 44 its, 64882.39 confs/it
c trds: 19 transitive reductions, 13312 removed, 16 failed
c trds: 211820 nodes, 238694 edges, 31599471 steps
c trim: 1408996 words, 5.4 MB
c trnr: 19 count, 1575 bin, 49949 trn, 357205310 steps
c unhd: 12 count, 23 rounds, 35415588 steps
c unhd: 128 non-trivial sccs of average size 2.0
c unhd: 6 units, 4 bin, 1 trn, 1 lrg
c unhd: 18 failed, 17 stamp, 0 lits, 1 bin, 0 trn, 1 lrg
c unhd: 33030 tauts, 795 bin 2%, 7318 trn 22%, 5565 lrg 17%
c unhd: 33030 tauts, 19352 stamp 59%, 32168 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 305091 str, 4 bin 0%, 1347 trn 0%, 303740 lrg 100%, 300536 red 99%
c vars: 3205 remaining 6% and 49231 removed 94% out of 52436
c vars: 2670 fixed 5%, 41948 eliminated 80%, 4613 equivalent 9%
c vsts: 23260600312 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 48.6 search visits per propagation, 7956.6 per conflict
c wchs: 8566038011 pushed, 14757098 enlarged, 295 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2871918       2065610        302494     101526782      28623427       1711082
c 
c  0 0        271205   9    100164   5         0   0  70555762  69  15310470  53    725926  42     4.3
c  1 5        224681   8    160058   8     32527  11  12493916  12<  4030049  14<   232234  14<    1.0
c  2 6        871021  30<   673445  33     80572  27  13399463  13   5827809  20    432813  25     2.9
c  3 9       1026692  36    793599  38<    98274  32<  4102503   4   2740069  10    254821  15     4.7
c  4 14       401409  14    290518  14     67387  22    871406   1    648304   2     61233   4     2.2
c  5 21        65771   2     41506   2     19565   6     90179   0     58849   0      3709   0     0.5
c  6 30         9820   0      5611   0      3636   1     11958   0      7023   0       301   0     0.1
c  7 41         1167   0       627   0       476   0      1419   0       758   0        41   0     0.0
c  8 54          145   0        79   0        53   0       169   0        93   0         4   0     0.0
c  9 69            7   0         3   0         4   0         7   0         3   0         0   0     0.0
c 
c avg                  2.5           2.6           2.9           0.5           0.9           1.2
c std                  1.2           1.1           1.1           0.9           1.2           1.3
c 
c   40.153   6% cce
c   15.294   2% sweep
c   15.132   2% bump
c   12.655   2% probe
c    8.527   1% elim
c    6.802   1% decide
c    4.489   1% unhide
c    3.806   1% ternres
c 
c    7.898 < 1% rest (below)
c 
c    2.103   0% transred
c    1.971   0% quatres
c    1.202   0% gauss
c    0.890   0% bca
c    0.857   0% block
c    0.679   0% rescore
c    0.196   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.566   0% preprocessing     2%
c   93.357  14% inprocessing     98%
c ==================================
c   94.923  14% simplifying
c  587.224  86% search
c ==================================
c  682.148 100% all
c 
c       2854825 conflicts,        4185.1 confs/sec
c          5720 ternaries,         499.1 confs/ternary
c           948 binaries,         3011.4 confs/binary
c            44 iterations,      64882.4 confs/iteration
c 
c            54 reductions,          0.1 redus/sec,  52867.1 confs/reduction
c         78720 restarts,          115.4 rests/sec,     36.3 confs/restart
c      10790252 decisions,       15818.1 decis/sec,      3.8 decis/conflict
c     497240244 propagations,   728933.1 props/sec,     46.1 props/decision
c 
c 682.1 seconds, 65.9 MB
c launch: done
