c launch: /data/cnf/sc2014/app/9dlx_vliw_at_b_iq3.cnf.bz2
c host: atom28
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/9dlx_vliw_at_b_iq3.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/9dlx_vliw_at_b_iq3.cnf.bz2
c no embedded options
c found 'p cnf 69789 968295' header
c read 69789 variables, 968295 clauses, 2788367 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=6
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 69788 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] AVG (--score=6)
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   69788   968294         0       0      0     0    0     0   27   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 25 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] 25 out of 25 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 6 variables
c [simpleprobe-1] all 69783 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 256 variables
c [simpleprobe-1] 29988 variables remain 43% (39539 retained 57%)
c [simpleprobe-1] removed 256 variables, found 21181 hbrs, 255 units
c [unhide-1] limit 60196 based on 963140 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 203 tauts, 0 hbrs, 2749 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 69527 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 61005 not tried 88% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 8522 = 12% variables out of 69527 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 945930 negative 100.0% of 946239 except 309 0.0%
c [phase-count-1] 271273 positive 28.7% of 946239 except 674966 71.3%
c [phase-count-1] less non-negative clauses 309 than limit 94600 (10.0%)
c [phase-count-1] non-pos/non-neg = 674966/309 = 2184.36 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 61005 negative 100%
c [sort-queue-1] sorted 61005 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 61005 (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 8778 variables 12.6% (61005 remain 87%)
c [simplification-1] removed 22055 irredundant clauses 2.3% (946239 remain 98%)
c [simplification-1] maximum reduction of 13% = max (13%, 2%)
c [simplification-1] large reduction 13% >= 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 1007 conflicts
c [simpleprobe-2] 27453 schedulable variables 45%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 27626 variables remain 45% (33379 retained 55%)
c [simpleprobe-2] removed 0 variables, found 332 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 50877 literals 42%
c [treelook-1] scheduling used 300082 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 351813 steps
c [treelook-1] 50869 literals remain 42%
c [treelook-1] 48808 variables remain to probed next time 80%
c [treelook-1] removed 0 variables, found 92 hbrs
c [basicprobe-1] limit 7569912 based on 946239 irredundant clauses
c [basicprobe-1-0] 56845 probes remain 95% after last round
c [basicprobe-1-0] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1423 variables, found 4794 hbrs
c [elim-2] 59582 variables 100% will be scheduled this time
c [elim-2] scheduled 59582 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 42885 not tried 72% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 7825 = 13% variables out of 59582 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 46204 enqueued variables after 1007 conflicts
c [score-dist-2] active 5553 (11%), one 0 (0%), zero 46204 (89%)
c [score-dist-2] max exp 511, different 8 (2%)
c [score-dist-2] median active exp 510, avg 510.1
c [simplification-2] removed 9248 variables 15.2% (51757 remain 74%)
c [simplification-2] removed 37813 irredundant clauses 4.0% (908426 remain 94%)
c [simplification-2] maximum reduction of 15% = max (15%, 4%)
c [simplification-2] large reduction 15% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13007 (soft 3007 + delta 10000)
c [simplification-2] new conflict limit 3007 (hard 13007)
c 
c [simplification-3] limit 3007 conflicts (hard 13007) hit after 3007 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 20 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 20 out of 20 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 288 variables
c [unhide-2] limit 56739 based on 907837 irredundant clauses
c [unhide-2-2] 384 units, 22 failed, 151 tauts, 0 hbrs, 16657 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 50192 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 31992 not tried 64% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2476 = 5% variables out of 50192 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 37207 enqueued variables after 3007 conflicts
c [score-dist-3] active 10509 (22%), one 0 (0%), zero 37207 (78%)
c [score-dist-3] max exp 513, different 9 (2%)
c [score-dist-3] median active exp 512, avg 512.0
c [simplification-3] removed 4041 variables 7.8% (47716 remain 68%)
c [simplification-3] removed 27702 irredundant clauses 3.0% (880722 remain 91%)
c [simplification-3] maximum reduction of 8% = max (8%, 3%)
c [simplification-3] large reduction 8% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15007 (soft 5007 + delta 10000)
c [simplification-3] new conflict limit 5007 (hard 15007)
c 
c [simplification-4] limit 5007 conflicts (hard 15007) hit after 5008 conflicts
c [decomp-7] removed 7 variables
c [treelook-2] limit 220095 based on 880380 irredundant clauses
c [treelook-2] scheduled 37006 literals 39%
c [treelook-2] scheduling used 223425 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 220095 based on 880380 irredundant clauses
c [treelook-2] used 634394 steps
c [treelook-2] 37003 literals remain 39%
c [treelook-2] 33284 variables remain to probed next time 70%
c [decomp-8] removed 2 variables
c [treelook-2] removed 2 variables, found 2 hbrs
c [unhide-3] limit 84550 with penalty 1 = 0 + 1
c [unhide-3-3] 0 units, 0 failed, 5818 tauts, 0 hbrs, 7710 literals
c [elim-4] 31628 variables 66% will be scheduled this time
c [elim-4] scheduled 31628 variables 66%
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 1147 variables 2% in round 1 in 160473983 steps
c [elim-4-1] backward subsumption/strengthening limit 160473900
c [elim-4-1-1] backward checking 24241 touched variables 51%
c [elim-4-1-1] incomplete backward checking 24239 remain 100%
c [elim-4-1] subsumed 84 and strengthened 32 clauses in 160477945 steps
c [elim-4-1] rescheduled 156 variables 0% by backward subsumption
c [elim-4-2] eliminated 12 variables 0% in round 2 in 814474 steps
c [elim-4-2] backward subsumption/strengthening limit 814400
c [elim-4-2-1] backward checking 24248 touched variables 51%
c [elim-4-2-1] incomplete backward checking 24247 remain 100%
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 815846 steps
c [elim-4-2] fully rescheduled 46548 variables 98%
c [elim-4] incomplete 3726 not tried 8% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 2522 = 8% variables out of 31628 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 28225 enqueued variables after 5008 conflicts
c [score-dist-4] active 16960 (38%), one 0 (0%), zero 28225 (62%)
c [score-dist-4] max exp 514, different 10 (2%)
c [score-dist-4] median active exp 513, avg 512.9
c [simplification-4] removed 2531 variables 5.3% (45185 remain 65%)
c [simplification-4] removed 50131 irredundant clauses 5.7% (830591 remain 86%)
c [simplification-4] maximum reduction of 6% = max (5%, 6%)
c [simplification-4] large reduction 6% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17008 (soft 7008 + delta 10000)
c [simplification-4] new conflict limit 7008 (hard 17008)
c 
c [simplification-5] limit 7008 conflicts (hard 17008) hit after 7008 conflicts
c [quatres-1] found 9585 quaternary clauses 15% in total
c [quatres-1-2] added 16 single-self-subsuming ternary resolvents
c [quatres-1-2] added 750 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 45185 free variables schedulable
c [ternres-1] 27028 ternary resolvents (5 bin, 27023 trn)
c [ternres-1] 273 variables remain 1% (44912 retained 99%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1 xors of average arity 2.0
c [gauss-1] connected 2 occurrences of 2 variables (average 1.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 3 variables
c [basicprobe-2] limit 6644664 based on 830583 irredundant clauses
c [basicprobe-2-0] 40649 probes remain 91% after last round
c [basicprobe-2-0] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 658 variables, found 4802 hbrs
c [bate-1] eliminated 16 asymmetric tautologies during probing
c [transred-1] limit 1210064 with penalty 0 = 0 + 0
c [transred-1] removed 6 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 44524 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 18952 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 99
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 98
c [cce-1-1] eliminated 7 clauses out of 14 (50%) of length 97
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 96
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 92
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 89
c [cce-1-1] eliminated 6 clauses out of 13 (46%) of length 88
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 87
c [cce-1-1] eliminated 11 clauses out of 27 (41%) of length 86
c [cce-1-1] eliminated 2 clauses out of 13 (15%) of length 85
c [cce-1-1] eliminated 5 clauses out of 20 (25%) of length 84
c [cce-1-1] eliminated 1 clauses out of 23 (4%) of length 82
c [cce-1-1] eliminated 1 clauses out of 36 (3%) of length 79
c [cce-1-1] eliminated 1 clauses out of 35 (3%) of length 78
c [cce-1-1] eliminated 1 clauses out of 32 (3%) of length 76
c [cce-1-1] eliminated 1 clauses out of 38 (3%) of length 75
c [cce-1-1] eliminated 7 clauses out of 68 (10%) of length 74
c [cce-1-1] eliminated 4 clauses out of 53 (8%) of length 73
c [cce-1-1] eliminated 10 clauses out of 81 (12%) of length 72
c [cce-1-1] eliminated 6 clauses out of 113 (5%) of length 71
c [cce-1-1] eliminated 1 clauses out of 56 (2%) of length 70
c [cce-1-1] eliminated 4 clauses out of 96 (4%) of length 69
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 78 large clauses in 30001318 steps
c [cce-1-1] allowing another 15000659 steps for small clauses
c [cce-1-1] scheduling 722532 clauses = 699419 binary + 23113 ternary
c [cce-1-1] tried to eliminate 557 small clauses 0%
c [cce-1-1] eliminated 64 binary clauses 0%
c [cce-1-1] eliminated 64 small clauses 0%
c [cce-1-1] eliminated 64 small clauses in 30000050 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 142 covered clauses in round 1
c [cce-1] eliminated 142 covered clauses in TOTAL during 1 rounds
c [cce-1] 142 < 1/100 * 799332 = 7993 considered unsuccessful
c [elim-5] 3702 variables 8% will be scheduled this time
c [elim-5] scheduled 3702 variables 8%
c [elim-5] limit of 24201280 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 2276 not tried 5% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 1 = 0% variables out of 3702 scheduled
c [elim-5] 1 < 1/100 * 3702 = 37 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1598760 added (scaled 2)
c [bca-1] 72272 out of 88644 literals actually usable 82%
c [bca-1] added 23490 blocked clauses in 270310 steps
c [sweep-1] limit 1598260 based on 799130 irredundant clauses
c [sweep-1-1] 2508 pos 5.7% + 41813 neg 94.3% = 44321 sched 100.0% ret 0
c [sweep-1-1] 1605664 steps 30 queries 5977.00 avg class size
c [sweep-1-1] 1157 decisions 28 SAT calls 115.86 avg env size
c [sweep-1-1] 43926 variables remain 99% (395 retained 1%)
c [decomp-10] removed 12 variables
c [sweep-1-1] removed 12 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 12 vars in TOTAL (1 rounds, 29 queries)
c [sort-queue-5] sorted 24066 enqueued variables after 7008 conflicts
c [score-dist-5] active 20243 (46%), one 0 (0%), zero 24066 (54%)
c [score-dist-5] max exp 514, different 10 (2%)
c [score-dist-5] median active exp 514, avg 513.4
c [simplification-5] removed 876 variables 1.9% (44309 remain 63%)
c [simplification-5] removed 31508 irredundant clauses 3.8% (799083 remain 83%)
c [simplification-5] maximum reduction of 4% = max (2%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 4000
c [simplification-5] penalized conflict interval 4000 = 1 * 4000
c [simplification-5] hard conflict limit 21008 (soft 11008 + delta 10000)
c [simplification-5] new conflict limit 11008 (hard 21008)
c 
c [simplification-6] limit 11008 conflicts (hard 21008) hit after 11008 conflicts
c [quatres-2] found 10382 quaternary clauses 17% in total
c [quatres-2-2] added 6 single-self-subsuming ternary resolvents
c [quatres-2-2] added 274 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 272 schedulable variables 1%
c [ternres-2] 1448 ternary resolvents (5 bin, 1443 trn)
c [ternres-2] 124 variables remain 0% (44185 retained 100%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 26 at-most-one constraints of average size 3.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 26 out of 26 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-4] limit 97359 with penalty 2 = 1 + 1
c [unhide-4-4] 1245 units, 14 failed, 1440 tauts, 0 hbrs, 19224 literals
c [transred-2] limit 1947190 with penalty 0 = 0 + 0
c [transred-2] removed 5 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 43054 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 4361 blocked clauses
c [block-2] 4361 < 1/100 * 798368 = 7983 considered unsuccessful
c [bca-2] limit of 10000000 steps and 1560653 added (scaled 2)
c [bca-2] 66354 out of 85944 literals actually usable 77%
c [bca-2] added 541 blocked clauses in 244389 steps
c [sweep-2] limit 1548408 based on 774204 irredundant clauses
c [sweep-2-1] 2558 pos 6.0% + 40031 neg 94.0% = 42589 sched 99.1% ret 382
c [sweep-2-1] 1699412 steps 19 queries 8587.89 avg class size
c [sweep-2-1] 749 decisions 18 SAT calls 191.56 avg env size
c [sweep-2-1] 41883 variables remain 99% (530 retained 1%)
c [decomp-12] removed 932 variables
c [sweep-2-1] removed 932 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 932 vars in TOTAL (1 rounds, 18 queries)
c [sort-queue-6] sorted 19819 enqueued variables after 11008 conflicts
c [score-dist-6] active 22220 (53%), one 0 (0%), zero 19819 (47%)
c [score-dist-6] max exp 515, different 11 (2%)
c [score-dist-6] median active exp 514, avg 514.2
c [simplification-6] removed 2270 variables 5.1% (42039 remain 60%)
c [simplification-6] removed 39061 irredundant clauses 4.9% (760022 remain 78%)
c [simplification-6] maximum reduction of 5% = max (5%, 5%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 23008 (soft 13008 + delta 10000)
c [simplification-6] new conflict limit 13008 (hard 23008)
c 
c [simplification-7] limit 13008 conflicts (hard 23008) hit after 13008 conflicts
c [quatres-3] found 8280 quaternary clauses 15% in total
c [quatres-3-2] added 323 single-self-subsuming ternary resolvents
c [quatres-3-2] added 81 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 117 schedulable variables 0%
c [ternres-3] 461 ternary resolvents (5 bin, 456 trn)
c [ternres-3] 59 variables remain 0% (41980 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 3 xors of average arity 3.0
c [gauss-2] connected 9 occurrences of 6 variables (average 1.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 [simpleprobe-3] 18197 schedulable variables 43%
c [simpleprobe-3] limit 4523260 penalty 1 = 1 + 0
c [simpleprobe-3] 18727 variables remain 45% (23312 retained 55%)
c [simpleprobe-3] removed 0 variables, found 898 hbrs, 0 units
c [unhide-5] limit 226163 with penalty 1 = 0 + 1
c [unhide-5-5] 2 units, 4 failed, 8904 tauts, 0 hbrs, 10266 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 18 transitive binary clauses
c [transred-3] found 5 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 69 (1%) of length 72
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1 large clauses in 15000013 steps
c [cce-2-1] allowing another 7500006 steps for small clauses
c [cce-2-1] scheduling 678418 clauses = 663939 binary + 14479 ternary
c [cce-2-1] tried to eliminate 188 small clauses 0%
c [cce-2-1] eliminated 11 binary clauses 0%
c [cce-2-1] eliminated 11 small clauses 0%
c [cce-2-1] eliminated 147 small clauses in 15000251 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 148 covered clauses in round 1
c [cce-2] eliminated 148 covered clauses in TOTAL during 1 rounds
c [cce-2] 148 < 1/100 * 751920 = 7519 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 42030 variables 100%
c [elim-6] limit of 22616301 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 13118 not tried 31% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 2811 = 7% variables out of 42030 scheduled
c [bca-3] limit of 10000000 steps and 1449813 added (scaled 2)
c [bca-3] 58625 out of 78440 literals actually usable 75%
c [bca-3] added 530 blocked clauses in 193320 steps
c [sweep-3] limit 1437298 based on 718649 irredundant clauses
c [sweep-3-1] 2497 pos 6.4% + 36222 neg 93.6% = 38719 sched 98.7% ret 500
c [sweep-3-1] 1568447 steps 32 queries 6807.09 avg class size
c [sweep-3-1] 1060 decisions 30 SAT calls 88.93 avg env size
c [sweep-3-1] 38348 variables remain 98% (871 retained 2%)
c [decomp-15] removed 12 variables
c [sweep-3-1] removed 12 vars (0 failed, 1 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 12 vars in TOTAL (1 rounds, 31 queries)
c [sort-queue-7] sorted 17003 enqueued variables after 13008 conflicts
c [score-dist-7] active 22204 (57%), one 0 (0%), zero 17003 (43%)
c [score-dist-7] max exp 515, different 11 (2%)
c [score-dist-7] median active exp 515, avg 514.4
c [simplification-7] removed 2832 variables 6.7% (39207 remain 56%)
c [simplification-7] removed 41446 irredundant clauses 5.5% (718576 remain 74%)
c [simplification-7] maximum reduction of 7% = max (7%, 5%)
c [simplification-7] large reduction 7% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 25008 (soft 15008 + delta 10000)
c [simplification-7] new conflict limit 15008 (hard 25008)
c 
c [simplification-8] limit 15008 conflicts (hard 25008) hit after 15010 conflicts
c [quatres-4] found 8056 quaternary clauses 15% in total
c [quatres-4-2] added 6 single-self-subsuming ternary resolvents
c [quatres-4-2] added 330 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 58 schedulable variables 0%
c [ternres-4] 506 ternary resolvents (0 bin, 506 trn)
c [ternres-4] 6 variables remain 0% (39201 retained 100%)
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 34653 literals 44%
c [treelook-3] scheduling used 300086 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 403537 steps
c [treelook-3] 34650 literals remain 44%
c [treelook-3] 26048 variables remain to probed next time 66%
c [treelook-3] removed 0 variables, found 15 hbrs
c [unhide-6] limit 258562 with penalty 1 = 0 + 1
c [unhide-6-6] 166 units, 7 failed, 1077 tauts, 0 hbrs, 14493 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 16 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 39034 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 24381 blocked clauses
c [elim-7] 2242 variables 6% will be scheduled this time
c [elim-7] scheduled 2242 variables 6%
c [elim-7] limit of 51712477 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 1016 not tried 3% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 0 = 0% variables out of 2242 scheduled
c [bca-4] limit of 10000000 steps and 1395254 added (scaled 2)
c [bca-4] 56666 out of 77680 literals actually usable 73%
c [bca-4] added 7922 blocked clauses in 198089 steps
c [sweep-4] limit 1382474 based on 691237 irredundant clauses
c [sweep-4-1] 3215 pos 8.5% + 34755 neg 91.5% = 37970 sched 97.8% ret 869
c [sweep-4-1] 1394314 steps 30 queries 3230.37 avg class size
c [sweep-4-1] 1215 decisions 27 SAT calls 184.44 avg env size
c [sweep-4-1] 37622 variables remain 97% (1217 retained 3%)
c [decomp-18] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 2 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2 vars in TOTAL (1 rounds, 29 queries)
c [sort-queue-8] sorted 15728 enqueued variables after 15010 conflicts
c [score-dist-8] active 23109 (60%), one 0 (0%), zero 15728 (40%)
c [score-dist-8] max exp 515, different 11 (2%)
c [score-dist-8] median active exp 515, avg 514.5
c [simplification-8] removed 370 variables 0.9% (38837 remain 56%)
c [simplification-8] removed 27339 irredundant clauses 3.8% (691237 remain 71%)
c [simplification-8] maximum reduction of 4% = max (1%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 8000
c [simplification-8] penalized conflict interval 8000 = 1 * 8000
c [simplification-8] hard conflict limit 33010 (soft 23010 + delta 10000)
c [simplification-8] new conflict limit 23010 (hard 33010)
c 
c [simplification-9] limit 23010 conflicts (hard 33010) hit after 23010 conflicts
c [quatres-5] found 8818 quaternary clauses 17% in total
c [quatres-5-2] added 31 single-self-subsuming ternary resolvents
c [quatres-5-2] added 28 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] 6 schedulable variables 0%
c [ternres-5] 503 ternary resolvents (5 bin, 498 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-19] removed 1 variables
c [basicprobe-3] limit 18560806 penalty 0 = 0 + 0
c [basicprobe-3-0] 33435 probes remain 86% after last round
c [basicprobe-3-0] 33 units = 33 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 33 variables, found 2089 hbrs
c [bate-2] eliminated 4 asymmetric tautologies during probing
c [unhide-7] limit 371216 with penalty 1 = 0 + 1
c [unhide-7-7] 0 units, 0 failed, 6693 tauts, 0 hbrs, 5189 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 17 transitive binary clauses
c [transred-5] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 38801 variables 100%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 3475 blocked clauses
c [block-4] 3475 < 1/100 * 684623 = 6846 considered unsuccessful
c [bca-5] limit of 10000000 steps and 1379003 added (scaled 2)
c [bca-5] 54121 out of 77546 literals actually usable 70%
c [bca-5] added 356 blocked clauses in 190228 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 11136480 penalty 0 = 0 + 0
c [sweep-5-1] 1981 pos 5.3% + 35577 neg 94.7% = 37558 sched 96.9% ret 1214
c [sweep-5-1] 11172578 steps 163 queries 1317.09 avg class size
c [sweep-5-1] 4794 decisions 154 SAT calls 115.34 avg env size
c [sweep-5-1] 32885 variables remain 85% (5887 retained 15%)
c [decomp-20] removed 12 variables
c [sweep-5-1] removed 12 vars (0 failed, 9 eqs, 22 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 12 vars in TOTAL (1 rounds, 162 queries)
c [sort-queue-9] sorted 13721 enqueued variables after 23010 conflicts
c [score-dist-9] active 25039 (65%), one 0 (0%), zero 13721 (35%)
c [score-dist-9] max exp 516, different 11 (2%)
c [score-dist-9] median active exp 516, avg 515.3
c [simplification-9] removed 77 variables 0.2% (38760 remain 56%)
c [simplification-9] removed 10099 irredundant clauses 1.5% (681124 remain 70%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-9] new conflict interval 18000
c [simplification-9] penalized conflict interval 18000 = 1 * 18000
c [simplification-9] hard conflict limit 51010 (soft 41010 + delta 10000)
c [simplification-9] new conflict limit 41010 (hard 51010)
c 
c [simplification-10] limit 41010 conflicts (hard 51010) hit after 41011 conflicts
c [quatres-6] found 9011 quaternary clauses 17% in total
c [quatres-6-2] added 7 single-self-subsuming ternary resolvents
c [quatres-6-2] added 23 quaternary resolvents
c [ternres-6] limit 5811869 with penalty 0 = 0 + 0
c [ternres-6] all 38760 free variables schedulable
c [ternres-6] 150 ternary resolvents (0 bin, 150 trn)
c [ternres-6] 35537 variables remain 92% (3223 retained 8%)
c [card-4] limit 363241 penalty 3 = 3 + 0
c [card-4] found 12 at-most-one constraints of average size 4.9
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 363241 for elimination
c [card-4] 12 out of 12 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 4 xors of average arity 2.5
c [gauss-3] connected 10 occurrences of 10 variables (average 1.0)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-21] removed 4 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 17 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 22 (18%) of length 82
c [cce-3-1] eliminated 4 clauses out of 32 (12%) of length 80
c [cce-3-1] eliminated 8 clauses out of 32 (25%) of length 79
c [cce-3-1] eliminated 8 clauses out of 64 (12%) of length 77
c [cce-3-1] eliminated 4 clauses out of 26 (15%) of length 76
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 28 large clauses in 7500444 steps
c [cce-3-1] allowing another 3750222 steps for small clauses
c [cce-3-1] scheduling 616927 clauses = 595748 binary + 21179 ternary
c [cce-3-1] tried to eliminate 91 small clauses 0%
c [cce-3-1] eliminated 25 binary clauses 0%
c [cce-3-1] eliminated 25 small clauses 0%
c [cce-3-1] eliminated 49 small clauses in 7504096 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 77 covered clauses in round 1
c [cce-3] eliminated 77 covered clauses in TOTAL during 1 rounds
c [cce-3] 77 < 1/100 * 681114 = 6811 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 38754 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1162373910 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1344 variables 3% in round 1 in 365747385 steps
c [elim-8-1] backward subsumption/strengthening limit 365747300
c [elim-8-1-1] backward checking 11198 touched variables 29%
c [elim-8-1-1] incomplete backward checking 11419 remain 102%
c [elim-8-1] subsumed 0 and strengthened 314 clauses in 365750299 steps
c [elim-8-1] rescheduled 863 variables 2% by backward subsumption
c [elim-8-2] eliminated 6 variables 0% in round 2 in 55075529 steps
c [elim-8-2] backward subsumption/strengthening limit 55075500
c [elim-8-2-1] backward checking 11451 touched variables 30%
c [elim-8-2-1] incomplete backward checking 11450 remain 100%
c [elim-8-2] subsumed 0 and strengthened 11 clauses in 55075523 steps
c [elim-8-2] rescheduled 38 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 18835512 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1350 = 3% variables out of 38754 scheduled
c [bca-6] limit of 10000000 steps and 1336053 added (scaled 2)
c [bca-6] 46973 out of 74810 literals actually usable 63%
c [bca-6] added 343 blocked clauses in 181114 steps
c [sweep-6] limit 1743560 penalty 0 = 0 + 0
c [sweep-6-1] 1193 pos 3.7% + 30687 neg 96.3% = 31880 sched 85.2% ret 5524
c [sweep-6-1] 1787541 steps 20 queries 3275.10 avg class size
c [sweep-6-1] 519 decisions 17 SAT calls 77.18 avg env size
c [sweep-6-1] 31799 variables remain 85% (5605 retained 15%)
c [decomp-22] removed 1 variables
c [sweep-6-1] removed 1 vars (0 failed, 3 eqs, 3 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 1 vars in TOTAL (1 rounds, 19 queries)
c [sort-queue-10] sorted 9288 enqueued variables after 41011 conflicts
c [score-dist-10] active 28115 (75%), one 0 (0%), zero 9288 (25%)
c [score-dist-10] max exp 517, different 12 (2%)
c [score-dist-10] median active exp 517, avg 516.3
c [simplification-10] removed 1357 variables 3.5% (37403 remain 54%)
c [simplification-10] removed 21554 irredundant clauses 3.2% (659567 remain 68%)
c [simplification-10] maximum reduction of 4% = max (4%, 3%)
c [simplification-10] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-10] new conflict interval 22000
c [simplification-10] penalized conflict interval 22000 = 1 * 22000
c [simplification-10] hard conflict limit 74011 (soft 63011 + delta 11000)
c [simplification-10] new conflict limit 63011 (hard 74011)
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   68.5   37402   659567     44718   40505  22049 28890   29   397   46   7%    498  154   26   13  198%
c i   68.5   36686   659567     44806   40578  22053 28892   29   391   46   7%    441  147   24   13  176%
c -   73.9   36686   659567     59787   16883  22196 29033   30   179   36  17%     41  -84   20   17  120%
c 
c [simplification-11] limit of 319 binary hit after 410 binaries
c [quatres-7] found 8392 quaternary clauses 20% in total
c [quatres-7-2] added 4 single-self-subsuming ternary resolvents
c [quatres-7-2] added 36 quaternary resolvents
c [ternres-7] limit 7861275 with penalty 0 = 0 + 0
c [ternres-7] 33610 schedulable variables 90%
c [ternres-7] 1692 ternary resolvents (0 bin, 1692 trn)
c [ternres-7] 242 variables remain 1% (36444 retained 99%)
c [decomp-23] removed 1046 variables
c [unhide-8] limit 786127 with penalty 1 = 1 + 0
c [unhide-8-8] 889 units, 13 failed, 496 tauts, 0 hbrs, 22161 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 9 transitive binary clauses
c [transred-7] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 35452 variables 100%
c [block-5] limit of 39306379 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 7444 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 35369 variables 100%
c [elim-9] limit of 157225518 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 544 not tried 2% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1561 = 4% variables out of 35369 scheduled
c [bca-7] limit of 10000000 steps and 1231603 added (scaled 2)
c [bca-7] 45558 out of 67618 literals actually usable 67%
c [bca-7] added 194 blocked clauses in 148761 steps
c [sweep-7] limit 2358382 penalty 0 = 0 + 0
c [sweep-7-1] 1393 pos 4.9% + 27065 neg 95.1% = 28458 sched 84.2% ret 5350
c [sweep-7-1] 2397465 steps 62 queries 2751.81 avg class size
c [sweep-7-1] 1624 decisions 59 SAT calls 83.51 avg env size
c [sweep-7-1] 27846 variables remain 82% (5961 retained 18%)
c [decomp-24] removed 58 variables
c [sweep-7-1] removed 58 vars (0 failed, 6 eqs, 5 impls)
c [sweep-7] removed 58 vars in TOTAL (1 rounds, 61 queries)
c [sort-queue-11] sorted 6552 enqueued variables after 61820 conflicts
c [score-dist-11] active 27198 (81%), one 0 (0%), zero 6552 (19%)
c [score-dist-11] max exp 517, different 11 (2%)
c [score-dist-11] median active exp 517, avg 516.7
c [simplification-11] removed 2936 variables 8.0% (33750 remain 48%)
c [simplification-11] removed 52620 irredundant clauses 8.0% (606947 remain 63%)
c [simplification-11] maximum reduction of 8% = max (8%, 8%)
c [simplification-11] forced so keeping old conflict interval 22000
c [simplification-11] conflict limit remains at 63011 (hard 74011)
c [simplification-11] new binary interval 1000
c 
c [simplification-12] limit 63011 conflicts (hard 74011) hit after 63013 conflicts
c [quatres-8] found 11239 quaternary clauses 24% in total
c [quatres-8-1] removed 5 duplicate quaternary clauses
c [quatres-8-2] added 3 single-self-subsuming ternary resolvents
c [quatres-8-2] added 43 quaternary resolvents
c [ternres-8] limit 7967836 with penalty 0 = 0 + 0
c [ternres-8] 230 schedulable variables 1%
c [ternres-8] 158 ternary resolvents (1 bin, 157 trn)
c [ternres-8] 3 variables remain 0% (33747 retained 100%)
c [simpleprobe-4] 15017 schedulable variables 44%
c [simpleprobe-4] limit 7967836 penalty 2 = 2 + 0
c [decomp-26] removed 24 variables
c [simpleprobe-4] 17226 variables remain 51% (16500 retained 49%)
c [simpleprobe-4] removed 24 variables, found 6544 hbrs, 1 units
c [unhide-9] limit 1593567 with penalty 0 = 0 + 0
c [unhide-9-9] 0 units, 0 failed, 4349 tauts, 0 hbrs, 3033 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 27 transitive binary clauses
c [transred-8] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 33725 variables 100%
c [block-6] limit of 79678363 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 1973 blocked clauses
c [block-6] 1973 < 1/100 * 601054 = 6010 considered unsuccessful
c [elim-10] 539 variables 2% will be scheduled this time
c [elim-10] scheduled 539 variables 2%
c [elim-10] limit of 159356726 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 60 not tried 0% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 1 = 0% variables out of 539 scheduled
c [elim-10] 1 < 1/100 * 539 = 5 considered unsuccessful
c [bca-8] limit of 10000000 steps and 1212196 added (scaled 2)
c [bca-8] 44923 out of 67286 literals actually usable 67%
c [bca-8] added 335 blocked clauses in 149033 steps
c [sweep-8] limit 2390350 penalty 0 = 0 + 0
c [sweep-8-1] 1563 pos 5.6% + 26160 neg 94.4% = 27723 sched 82.4% ret 5919
c [sweep-8-1] 2527307 steps 45 queries 1831.16 avg class size
c [sweep-8-1] 1462 decisions 42 SAT calls 81.86 avg env size
c [sweep-8-1] 27271 variables remain 81% (6371 retained 19%)
c [decomp-27] removed 6 variables
c [sweep-8-1] removed 6 vars (0 failed, 2 eqs, 5 impls)
c [sweep-8] 6 < 1/1000 * 33642 = 33 considered unsuccessful
c [sweep-8] removed 6 vars in TOTAL (1 rounds, 44 queries)
c [sort-queue-12] sorted 6374 enqueued variables after 63013 conflicts
c [score-dist-12] active 27262 (81%), one 0 (0%), zero 6374 (19%)
c [score-dist-12] max exp 517, different 11 (2%)
c [score-dist-12] median active exp 517, avg 516.7
c [simplification-12] removed 114 variables 0.3% (33636 remain 48%)
c [simplification-12] removed 9447 irredundant clauses 1.6% (597500 remain 62%)
c [simplification-12] maximum reduction of 2% = max (0%, 2%)
c [simplification-12] geometric conflict interval increment 7333 = 22000 / 3
c [simplification-12] new conflict interval 29333
c [simplification-12] penalized conflict interval 29333 = 1 * 29333
c [simplification-12] hard conflict limit 107012 (soft 92346 + delta 14666)
c [simplification-12] new conflict limit 92346 (hard 107012)
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   87.6   33635   597500     73630   27319  22316 24402   20   245   36   8%    228  -46   17   18   95%
c 
c [simplification-13] limit 92346 conflicts (hard 107012) hit after 92347 conflicts
c [quatres-9] found 11070 quaternary clauses 24% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 25 single-self-subsuming ternary resolvents
c [quatres-9-2] added 3 quaternary resolvents
c [ternres-9] limit 9697458 with penalty 0 = 0 + 0
c [ternres-9] 3 schedulable variables 0%
c [ternres-9] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-28] removed 12 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 53 transitive binary clauses
c [transred-9] found 5 units
c [bca-9] limit of 10000000 steps and 1212067 added (scaled 2)
c [bca-9] 39313 out of 67240 literals actually usable 58%
c [bca-9] added 3 blocked clauses in 152272 steps
c [sort-queue-13] sorted 4752 enqueued variables after 92347 conflicts
c [score-dist-13] active 28867 (86%), one 0 (0%), zero 4752 (14%)
c [score-dist-13] max exp 518, different 10 (2%)
c [score-dist-13] median active exp 518, avg 517.6
c [simplification-13] removed 16 variables 0.0% (33619 remain 48%)
c [simplification-13] removed 144 irredundant clauses 0.0% (597356 remain 62%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 29333
c [simplification-13] new conflict interval 58666
c [simplification-13] penalized conflict interval 58666 = 1 * 58666
c [simplification-13] hard conflict limit 180346 (soft 151013 + delta 29333)
c [simplification-13] new conflict limit 151013 (hard 180346)
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   97.4   33618   597356    103921   53829  22500 24430   28   500   45   6%    235  172   23   20  114%
c -   98.0   33618   597356    106135   23815  22515 24437   26   401   34   7%   -149   70   26   20  129%
c i  100.5   33617   597354    116107   32576  22594 24483   24   321   38   7%    -31  -19   19   21   95%
c i  103.7   33616   597354    131911   46228  22688 24530   25   457   41   5%     43  140   26   21  127%
c -  106.9   33616   597354    145121   27417  22758 24583   27   366   35   7%     17   41   20   21   95%
c 
c [simplification-14] limit 151013 conflicts (hard 180346) hit after 173063 conflicts
c [quatres-10] found 11512 quaternary clauses 24% in total
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 10 single-self-subsuming ternary resolvents
c [quatres-10-2] added 5 quaternary resolvents
c [gauss-4] limit 341063 penalty 3 = 3 + 0
c [gauss-4] extracted 2 xors of average arity 2.0
c [gauss-4] connected 4 occurrences of 2 variables (average 2.0)
c [gauss-4] limit 341063 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-29] removed 3 variables
c [treelook-4] limit 682127 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 39676 literals 59%
c [treelook-4] scheduling used 682133 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 682127 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 735972 steps
c [treelook-4] 39664 literals remain 59%
c [treelook-4] 21670 variables remain to probed next time 64%
c [treelook-4] removed 0 variables, found 49 hbrs
c [unhide-10] limit 682127 with penalty 2 = 1 + 1
c [unhide-10-10] 124 units, 16 failed, 3441 tauts, 0 hbrs, 75037 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 27 transitive binary clauses
c [transred-10] found 7 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 33374 variables 100%
c [block-7] limit of 68212727 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 1138 blocked clauses
c [block-7] 1138 < 1/100 * 596233 = 5962 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 85265908 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 5 clauses out of 37 (14%) of length 78
c [cce-4-1] eliminated 4 clauses out of 24 (17%) of length 76
c [cce-4-1] eliminated 4 clauses out of 55 (7%) of length 74
c [cce-4-1] eliminated 6 clauses out of 67 (9%) of length 72
c [cce-4-1] eliminated 4 clauses out of 48 (8%) of length 70
c [cce-4-1] eliminated 4 clauses out of 92 (4%) of length 68
c [cce-4-1] eliminated 4 clauses out of 104 (4%) of length 66
c [cce-4-1] eliminated 1 clauses out of 142 (1%) of length 65
c [cce-4-1] eliminated 5 clauses out of 77 (6%) of length 64
c [cce-4-1] eliminated 1 clauses out of 115 (1%) of length 63
c [cce-4-1] eliminated 5 clauses out of 107 (5%) of length 62
c [cce-4-1] eliminated 1 clauses out of 61 (2%) of length 61
c [cce-4-1] eliminated 5 clauses out of 152 (3%) of length 60
c [cce-4-1] eliminated 9 clauses out of 160 (6%) of length 59
c [cce-4-1] eliminated 4 clauses out of 176 (2%) of length 58
c [cce-4-1] eliminated 4 clauses out of 140 (3%) of length 57
c [cce-4-1] eliminated 4 clauses out of 112 (4%) of length 55
c [cce-4-1] eliminated 10 clauses out of 168 (6%) of length 53
c [cce-4-1] eliminated 6 clauses out of 186 (3%) of length 52
c [cce-4-1] eliminated 25 clauses out of 190 (13%) of length 51
c [cce-4-1] eliminated 17 clauses out of 326 (5%) of length 50
c [cce-4-1] eliminated 10 clauses out of 123 (8%) of length 49
c [cce-4-1] eliminated 10 clauses out of 278 (4%) of length 48
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 148 large clauses in 85267749 steps
c [cce-4-1] allowing another 42633874 steps for small clauses
c [cce-4-1] scheduling 531326 clauses = 519741 binary + 11585 ternary
c [cce-4-1] tried to eliminate 2003 small clauses 0%
c [cce-4-1] eliminated 255 binary clauses 0%
c [cce-4-1] eliminated 255 small clauses 0%
c [cce-4-1] eliminated 255 small clauses in 85266039 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 403 covered clauses in round 1
c [cce-4] eliminated 403 covered clauses in TOTAL during 1 rounds
c [cce-4] 403 < 1/100 * 588148 = 5881 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 33339 variables 100%
c [elim-11] limit of 136425455 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 652 not tried 2% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 1367 = 4% variables out of 33339 scheduled
c [bca-10] limit of 10000000 steps and 1183815 added (scaled 2)
c [bca-10] 37654 out of 63946 literals actually usable 59%
c [bca-10] added 283 blocked clauses in 151660 steps
c [sweep-9] limit 2046381 penalty 1 = 1 + 0
c [sweep-9-1] 1549 pos 6.0% + 24269 neg 94.0% = 25818 sched 80.8% ret 6154
c [sweep-9-1] 2103437 steps 44 queries 3817.07 avg class size
c [sweep-9-1] 1062 decisions 38 SAT calls 134.34 avg env size
c [sweep-9-1] 25530 variables remain 80% (6442 retained 20%)
c [decomp-31] removed 29 variables
c [sweep-9-1] removed 29 vars (0 failed, 6 eqs, 10 impls)
c [sweep-9] 29 < 1/1000 * 31972 = 31 considered unsuccessful
c [sweep-9] removed 29 vars in TOTAL (1 rounds, 43 queries)
c [sort-queue-14] sorted 2952 enqueued variables after 173063 conflicts
c [score-dist-14] active 28991 (91%), one 0 (0%), zero 2952 (9%)
c [score-dist-14] max exp 519, different 10 (2%)
c [score-dist-14] median active exp 519, avg 518.6
c [simplification-14] removed 1673 variables 5.0% (31943 remain 46%)
c [simplification-14] removed 14687 irredundant clauses 2.5% (582667 remain 60%)
c [simplification-14] maximum reduction of 5% = max (5%, 2%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 185063 (soft 175063 + delta 10000)
c [simplification-14] new conflict limit 175063 (hard 185063)
c 
c [simplification-15] limit 175063 conflicts (hard 185063) hit after 175063 conflicts
c [quatres-11] found 9451 quaternary clauses 21% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 17 single-self-subsuming ternary resolvents
c [quatres-11-2] added 186 quaternary resolvents
c [ternres-10] limit 6913140 with penalty 1 = 1 + 0
c [ternres-10] all 31943 free variables schedulable
c [ternres-10] 1006 ternary resolvents (1 bin, 1005 trn)
c [ternres-10] 12974 variables remain 41% (18969 retained 59%)
c [card-5] limit 432071 penalty 4 = 4 + 0
c [card-5] found 8 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 432071 for elimination
c [card-5] 8 out of 8 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-32] removed 2 variables
c [basicprobe-4] limit 69131400 penalty 0 = 0 + 0
c [basicprobe-4-0] 20065 probes remain 63% after last round
c [basicprobe-4-0] 172 units = 172 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 175 variables, found 16112 hbrs
c [bate-3] eliminated 120 asymmetric tautologies during probing
c [unhide-11] limit 1382628 with penalty 1 = 0 + 1
c [unhide-11-11] 467 units, 13 failed, 10161 tauts, 0 hbrs, 41474 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 26 transitive binary clauses
c [elim-12] 54 variables 0% will be scheduled this time
c [elim-12] scheduled 54 variables 0%
c [elim-12] limit of 276525602 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] no variable eliminated in round 1 in 112497045 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 0 = 0% variables out of 54 scheduled
c [bca-11] limit of 10000000 steps and 1148380 added (scaled 2)
c [bca-11] 35967 out of 62598 literals actually usable 57%
c [bca-11] added 82 blocked clauses in 146653 steps
c [sort-queue-15] sorted 2868 enqueued variables after 175063 conflicts
c [score-dist-15] active 28430 (91%), one 0 (0%), zero 2868 (9%)
c [score-dist-15] max exp 519, different 10 (2%)
c [score-dist-15] median active exp 519, avg 518.6
c [simplification-15] removed 645 variables 2.0% (31298 remain 45%)
c [simplification-15] removed 17226 irredundant clauses 3.0% (565441 remain 58%)
c [simplification-15] maximum reduction of 3% = max (2%, 3%)
c [simplification-15] geometric conflict interval increment 14666 = 58666 / 4
c [simplification-15] new conflict interval 73332
c [simplification-15] penalized conflict interval 73332 = 1 * 73332
c [simplification-15] hard conflict limit 285061 (soft 248395 + delta 36666)
c [simplification-15] new conflict limit 248395 (hard 285061)
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 -  126.4   31298   565441    185135   26925  21806 32861   30   440   34   7%    477  157   31   22  141%
c -  135.5   31298   565441    222593   27747  22064 32927   19   164   34  11%    715 -165   19   23   82%
c 
c [simplification-16] limit 248395 conflicts (hard 285061) hit after 248396 conflicts
c [quatres-12] found 9847 quaternary clauses 23% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 11 single-self-subsuming ternary resolvents
c [quatres-12-2] added 45 quaternary resolvents
c [ternres-11] limit 17612063 with penalty 0 = 0 + 0
c [ternres-11] 12672 schedulable variables 40%
c [ternres-11] 1550 ternary resolvents (1 bin, 1549 trn)
c [ternres-11] 1 variables remain 0% (31297 retained 100%)
c [decomp-33] removed 57 variables
c [unhide-12] limit 1761206 with penalty 1 = 0 + 1
c [unhide-12-12] 13 units, 0 failed, 1768 tauts, 0 hbrs, 67837 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 48 transitive binary clauses
c [transred-12] found 1 units
c [bca-12] limit of 10000000 steps and 1147245 added (scaled 2)
c [bca-12] 34438 out of 62456 literals actually usable 55%
c [bca-12] added 182 blocked clauses in 139980 steps
c [sort-queue-16] sorted 1663 enqueued variables after 248396 conflicts
c [score-dist-16] active 29564 (95%), one 0 (0%), zero 1663 (5%)
c [score-dist-16] max exp 519, different 9 (2%)
c [score-dist-16] median active exp 519, avg 518.9
c [simplification-16] removed 71 variables 0.2% (31227 remain 45%)
c [simplification-16] removed 588 irredundant clauses 0.1% (564853 remain 58%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 73332
c [simplification-16] new conflict interval 146664
c [simplification-16] penalized conflict interval 146664 = 1 * 146664
c [simplification-16] hard conflict limit 468392 (soft 395060 + delta 73332)
c [simplification-16] new conflict limit 395060 (hard 468392)
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  141.3   31226   564853    249346   50552  23191 31590   20   315   44   6%    819   62   24   21  114%
c -  144.7   31226   564853    262196   30020  23260 31621   18   248   34   7%   -677  -18   12   21   56%
c -  155.1   31226   564846    300930   30398  23462 31677   17    90   34  18%     82 -203   15   22   68%
c -  164.0   31226   564846    341565   31560  23642 31722   27   302   35   9%    517   54   29   23  130%
c -  171.1   31226   564846    382320   33866  23790 31816   19   109   35  18%    752 -101   20   21   93%
c -  177.1   31226   564846    421426   35234  23867 31883   16    36   35  44%    874 -110   13   19   70%
c 
c [simplification-17] limit 395060 conflicts (hard 468392) hit after 436037 conflicts
c [quatres-13] found 10563 quaternary clauses 23% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 26 single-self-subsuming ternary resolvents
c [quatres-13-2] added 82 quaternary resolvents
c [ternres-12] limit 25372150 with penalty 0 = 0 + 0
c [ternres-12] 1 schedulable variables 0%
c [ternres-12] 1309 ternary resolvents (1 bin, 1308 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-34] removed 5 variables
c [simpleprobe-5] 15699 schedulable variables 50%
c [simpleprobe-5] limit 50744301 penalty 1 = 1 + 0
c [decomp-35] removed 96 variables
c [simpleprobe-5] 15218 variables remain 49% (15908 retained 51%)
c [simpleprobe-5] removed 96 variables, found 44511 hbrs, 31 units
c [unhide-13] limit 5074430 with penalty 0 = 0 + 0
c [unhide-13-15] 77 units, 1 failed, 25719 tauts, 0 hbrs, 57177 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 5 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 31048 variables 100%
c [block-8] limit of 63430376 steps penalty 2 = 2 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 16638 blocked clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 30951 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1163 variables 4% in round 1 in 442018707 steps
c [elim-13-1] backward subsumption/strengthening limit 442018700
c [elim-13-1-1] backward checking 8226 touched variables 27%
c [elim-13-1-1] incomplete backward checking 8278 remain 101%
c [elim-13-1] subsumed 7 and strengthened 104 clauses in 442021449 steps
c [elim-13-1] rescheduled 392 variables 1% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 135300349 steps
c [elim-13-2] backward subsumption/strengthening limit 135300300
c [elim-13-2-1] backward checking 8278 touched variables 27%
c [elim-13-2-1] incomplete backward checking 8278 remain 100%
c [elim-13-2] subsumed 2 and strengthened 26 clauses in 135303185 steps
c [elim-13-2] rescheduled 203 variables 1% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 81059451 steps
c [elim-13-3] backward subsumption/strengthening limit 81059400
c [elim-13-3-1] backward checking 8280 touched variables 27%
c [elim-13-3-1] incomplete backward checking 8200 remain 99%
c [elim-13-3] subsumed 2 and strengthened 9 clauses in 81064882 steps
c [elim-13] incomplete 81 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 1165 = 4% variables out of 30951 scheduled
c [bca-13] limit of 10000000 steps and 1058710 added (scaled 2)
c [bca-13] 33055 out of 59574 literals actually usable 55%
c [bca-13] added 1498 blocked clauses in 122765 steps
c [sweep-10] limit 1902911 penalty 2 = 2 + 0
c [sweep-10-1] 1593 pos 6.7% + 22103 neg 93.3% = 23696 sched 79.6% ret 6090
c [sweep-10-1] 1927730 steps 29 queries 4147.66 avg class size
c [sweep-10-1] 827 decisions 28 SAT calls 93.04 avg env size
c [sweep-10-1] 23500 variables remain 79% (6285 retained 21%)
c [decomp-36] removed 13 variables
c [sweep-10-1] removed 13 vars (1 failed, 0 eqs, 3 impls)
c [sweep-10] 13 < 1/1000 * 29786 = 29 considered unsuccessful
c [sweep-10] removed 13 vars in TOTAL (1 rounds, 28 queries)
c [sort-queue-17] sorted 995 enqueued variables after 436037 conflicts
c [score-dist-17] active 28778 (97%), one 0 (0%), zero 995 (3%)
c [score-dist-17] max exp 520, different 9 (2%)
c [score-dist-17] median active exp 520, avg 519.7
c [simplification-17] removed 1453 variables 4.7% (29773 remain 43%)
c [simplification-17] removed 44374 irredundant clauses 7.9% (520472 remain 54%)
c [simplification-17] maximum reduction of 8% = max (5%, 8%)
c [simplification-17] large reduction 8% >= 5% limit
c [simplification-17] next conflict interval 4360 = min (436037/100, 146664)
c [simplification-17] penalized conflict interval 4360 = 1 * 4360
c [simplification-17] hard conflict limit 450397 (soft 440397 + delta 10000)
c [simplification-17] new conflict limit 440397 (hard 450397)
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  207.7   29772   520472    436483   32332  23627 64677   15   181   37   8%    905   55   26   18  143%
c 
c [simplification-18] limit 440397 conflicts (hard 450397) hit after 450397 conflicts
c [quatres-14] found 10049 quaternary clauses 26% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 32 single-self-subsuming ternary resolvents
c [quatres-14-2] added 89 quaternary resolvents
c [ternres-13] limit 26171388 with penalty 0 = 0 + 0
c [ternres-13] all 29736 free variables schedulable
c [ternres-13] 1290 ternary resolvents (6 bin, 1284 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-37] removed 46 variables
c [unhide-14] limit 5234277 with penalty 0 = 0 + 0
c [unhide-14-18] 53 units, 47 failed, 9739 tauts, 0 hbrs, 65360 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 10 transitive binary clauses
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 29624 variables 100%
c [elim-14] limit of 523427765 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 1358 = 5% variables out of 29624 scheduled
c [bca-14] limit of 10000000 steps and 970957 added (scaled 2)
c [bca-14] 28843 out of 56534 literals actually usable 51%
c [bca-14] added 2070 blocked clauses in 116349 steps
c [sort-queue-18] sorted 228 enqueued variables after 450397 conflicts
c [score-dist-18] active 28038 (99%), one 0 (0%), zero 228 (1%)
c [score-dist-18] max exp 520, different 9 (2%)
c [score-dist-18] median active exp 520, avg 519.8
c [simplification-18] removed 1470 variables 4.9% (28266 remain 41%)
c [simplification-18] removed 44183 irredundant clauses 8.5% (476289 remain 49%)
c [simplification-18] maximum reduction of 8% = max (5%, 8%)
c [simplification-18] large reduction 8% >= 5% limit
c [simplification-18] next conflict interval 4503 = min (450397/100, 146664)
c [simplification-18] penalized conflict interval 4503 = 1 * 4503
c [simplification-18] hard conflict limit 464900 (soft 454900 + delta 10000)
c [simplification-18] new conflict limit 454900 (hard 464900)
c 
c [simplification-19] limit 454900 conflicts (hard 464900) hit after 464900 conflicts
c [quatres-15] found 10582 quaternary clauses 26% in total
c [quatres-15-1] removed 2 duplicate quaternary clauses
c [quatres-15-2] added 15 single-self-subsuming ternary resolvents
c [quatres-15-2] added 88 quaternary resolvents
c [ternres-14] limit 26654673 with penalty 0 = 0 + 0
c [ternres-14] all 28266 free variables schedulable
c [ternres-14] 710 ternary resolvents (1 bin, 709 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 333183 penalty 4 = 4 + 0
c [gauss-5] extracted 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-38] removed 12 variables
c [unhide-15] limit 5330934 with penalty 0 = 0 + 0
c [unhide-15-21] 11 units, 10 failed, 14102 tauts, 0 hbrs, 54149 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 42 transitive binary clauses
c [transred-15] found 2 units
c [block-9] scheduling all variables this time
c [block-9] scheduled 28233 variables 100%
c [block-9] limit of 133273368 steps penalty 1 = 1 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 1653 blocked clauses
c [block-9] 1653 < 1/100 * 473951 = 4739 considered unsuccessful
c [cce-5] limit of 8329585 steps penalty 4 = 4 + 0
c [cce-5-1] eliminated 1 clauses out of 25 (4%) of length 83
c [cce-5-1] eliminated 1 clauses out of 19 (5%) of length 79
c [cce-5-1] eliminated 2 clauses out of 55 (4%) of length 77
c [cce-5-1] eliminated 1 clauses out of 37 (3%) of length 75
c [cce-5-1] eliminated 4 clauses out of 31 (13%) of length 73
c [cce-5-1] eliminated 2 clauses out of 54 (4%) of length 72
c [cce-5-1] eliminated 1 clauses out of 74 (1%) of length 71
c [cce-5-1] eliminated 1 clauses out of 36 (3%) of length 70
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 13 large clauses in 8330429 steps
c [cce-5-1] allowing another 4165214 steps for small clauses
c [cce-5-1] scheduling 423931 clauses = 413706 binary + 10225 ternary
c [cce-5-1] tried to eliminate 114 small clauses 0%
c [cce-5-1] eliminated 29 binary clauses 0%
c [cce-5-1] eliminated 29 small clauses 0%
c [cce-5-1] eliminated 29 small clauses in 8333984 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 42 covered clauses in round 1
c [cce-5] eliminated 42 covered clauses in TOTAL during 1 rounds
c [cce-5] 42 < 1/100 * 472282 = 4722 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 28179 variables 100%
c [elim-15] limit of 533093475 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 197 = 1% variables out of 28179 scheduled
c [elim-15] 197 < 1/100 * 28179 = 281 considered unsuccessful
c [bca-15] limit of 10000000 steps and 961972 added (scaled 2)
c [bca-15] 28273 out of 55966 literals actually usable 51%
c [bca-15] added 1144 blocked clauses in 114800 steps
c [sort-queue-19] sorted 186 enqueued variables after 464900 conflicts
c [score-dist-19] active 27796 (99%), one 0 (0%), zero 186 (1%)
c [score-dist-19] max exp 520, different 9 (2%)
c [score-dist-19] median active exp 520, avg 519.8
c [simplification-19] removed 284 variables 1.0% (27982 remain 40%)
c [simplification-19] removed 5010 irredundant clauses 1.1% (471279 remain 49%)
c [simplification-19] maximum reduction of 1% = max (1%, 1%)
c [simplification-19] geometric conflict interval increment 73332 = 146664 / 2
c [simplification-19] new conflict interval 219996
c [simplification-19] penalized conflict interval 219996 = 1 * 219996
c [simplification-19] hard conflict limit 794894 (soft 684896 + delta 109998)
c [simplification-19] new conflict limit 684896 (hard 794894)
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  233.6   27981   471279    471572   46098  23480 53208   13   100   38  13%   -785  -31   10   17   57%
c i  233.6   25751   471279    471573   46098  23480 53208   13   100   38  13%   -785  -31   10   17   57%
c i  236.0   25750   471279    490213   62270  23504 53221   12    25   43  47%   -756  -91    9   16   55%
c -  238.6   25750   471279    497890   33087  23629 53235   21   297   33   7%   -822  174   28   17  172%
c i  240.4   25749   471279    504865   39245  23708 53240   27   286   37   9%   -636  143   27   18  151%
c i  240.4   25748   471279    504870   39247  23708 53240   27   286   37   9%   -637  143   26   18  150%
c i  240.6   25747   471279    506009   40178  23734 53242   27   262   37  10%   -760  116   28   18  157%
c i  244.6   25746   471279    528611   59371  23912 53281   12    63   41  19%   -306  -90   10   17   55%
c i  246.3   25691   471279    540338   69475  23926 53305   12    34   46  34%   -388 -105    8   17   51%
c -  246.7   25691   471279    542870   35934  23926 53305   13    31   34  41%   -498 -104   15   17   90%
c i  247.3   25690   471279    546840   39251  23944 53320   12    47   37  26%   -423  -83    6   16   36%
c 0  247.3   23335   471279    546840   39251  23944 53320   12    47   37  26%   -423  -83    6   16   36%
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: 140 basic ate = 100 trn 71% + 40 lrg 29% in 3 updates
c bcas: 15 count, 38973 added (8179 skipped), 2519723 steps
c bkwd: tried 317889 clauses, 635221 lits, 2.00 lits/clause
c bkwd: checked 1114071933 occs, 3504.59 occs/clause, 1753.83 occs/lit
c bkwd: subsumed 0 binary, 91 ternary, 4 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 496 large (0% self)
c blkd: 9 bces, 80015 removed, 28796339 resolutions, 72503982 steps
c blkd: 9925 blocking literals 7%, 860 pure
c bump: 530940 bumped seen, 45135184 lits 85.0 on average
c card: 5 count, 0 units, 0 am1, 19893773 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 560 subsumed
c card: 91 at-most-one constraints found, average size 3.33
c card: 91 at-most-one constraints used 100%, average size 3.33
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 5 cces, 652 eliminated, 591 ate 91%, 61 abce 9%
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: 3756662 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 107 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 38 decompositions, 1338 equivalent 2%
c deco: 15 decision-only clauses 0%, 41% reduction
c decs: 20693888 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 32016 eliminated 46%, 1117 pure 3%
c elms: 22 rounds, 1.5 rounds/bve
c elms: 13883 small 43%, 16156 large 50%
c elms: 22905 tried small, 13883 succeeded 61%, 9022 failed 39%
c elms: 39691 subsumed, 171744 strengthened, 42585 blocked
c elms: 14356482 copies, 23100943 resolutions, 460705 ipos
c elms: 102849129 subchks, 139188511 strchks
c gaus: 5 extractions, 10 extracted, 2.5 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8360506 steps, 4180253 extr 50%, 42 elim 0%
c glue: 20.9 orig avg, 20.9 real avg, 4.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 105808 = 73466 simple 69% + 32257 trn 30% + 85 lrg 0%, 2171 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 530940 clauses, 45.6 length
c lrnd: 24209210 lits = 35450524 orig - 11241314 removed 32%
c lrnd: 236418 uips 45%, 189558 flips 36%
c mins: 523098 mins 99%, 779 bin 0%, 7036 size 1%
c mins: 32530956 poisoned searches, 5848761 hits, 18% hit rate
c mins: 61538243 used twice searches, 6458682 hits, 10% hit rate
c move: moved 73249, 69214 bin 94%, 4035 trn 6%
c otfs: 16029 driving 31%, 35603 restarting 69%
c otfs: str 51632, 50298 red 97%, 1334 irr 3%
c otfs: str 51632, 0 bin 0%, 267 trn 1%, 51365 lrg 99%
c otfs: sub 707, 679 red 96%, 28 irr 4%
c otfs: sub 707, 0 bin 0%, 4 trn 1%, 703 lrg 99%
c phas: 1 computed, 61005 set, 0 pos (0%), 61005 neg (100%)
c prbs: 4 basic, 15423 probed, 265 failed, 0 lifted
c prbs: 5 simple, 149198 probed, 287 failed, 90 eqs
c prbs: 4 treelook, 26 probed, 0 failed, 0 lifted
c prom: 84575 locked 6% out of 1515030 tried
c prps: 551199764 props, 26 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 15 count, 2063 quat, 532 self1, 2 self2, 332 dup
c queu: 19 sorted, 20693888 next (46376 steps 0.00)
c queu: 45503809 enq (879801787 steps 19.33), 45135184 deq 99%
c redc: 9016 clauses 28%, 31758 tried 6%, 56 sat 0%
c redc: 20371 lits 5%, 411287 tried 1%, 56 sat 0%
c redc: 749 times jump level reduced, 53.2 levels on average
c reds: 12 count, 45570.0 conflicts per reduce
c reds: 0 memlim 0%, 12 arith 100%
c reds: 333035 collected 83%, 66429 retired 17%
c rmbd: 15075 removed, 9753 red 65%
c rsts: 13008 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 19 count, 18 confs 95%, 0 vars 0%
c simp: 0 its 0%, 1 bin 5%, 0 trns 0%
c subl: 530940 count (506032 tried 1.0), 46537 sub out of 526775 (8.8%)
c swps: 10 count, 10 rounds, 464 queries (46.4/round)
c swps: 441 sat calls, 9 unsat (0.3% success rate)
c swps: 14469 decisions 32.8, 129 conflicts 0.3
c swps; 3186.8 avg class size, 112.2 avg environment size
c swps: 1 failed, 64 impls, 30 equivs
c swp0: 151 type 0 queries, 4 unsat (2.6%), 150 sat (99.3%)
c swp1: 313 type 1 queries, 98 unsat (31.3%), 284 sat (90.7%)
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: 42450023 calls to obtain time
c tops: 13100 fixed 19%, 17 its, 32167.06 confs/it
c trds: 15 transitive reductions, 326 removed, 31 failed
c trds: 8262 nodes, 57114 edges, 29180068 steps
c trim: 407268 words, 1.6 MB
c trnr: 14 count, 31 bin, 37780 trn, 160438083 steps
c unhd: 15 count, 21 rounds, 43095678 steps
c unhd: 30 non-trivial sccs of average size 3.1
c unhd: 3431 units, 3431 bin, 0 trn, 0 lrg
c unhd: 147 failed, 143 stamp, 0 lits, 3 bin, 1 trn, 0 lrg
c unhd: 94061 tauts, 1480 bin 2%, 10197 trn 11%, 35094 lrg 37%
c unhd: 94061 tauts, 47290 stamp 50%, 53760 red 57%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 462516 str, 3431 bin 1%, 7583 trn 2%, 451502 lrg 98%, 366119 red 79%
c vars: 23335 remaining 33% and 46454 removed 67% out of 69789
c vars: 13100 fixed 19%, 32016 eliminated 46%, 1338 equivalent 2%
c vsts: 3108741375 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 5.6 search visits per propagation, 5502.3 per conflict
c wchs: 448937800 pushed, 44074762 enlarged, 164 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         528838        333035         66429      16381523       4784039        359538
c 
c  0 0         18626   4      1775   1         0   0   5699562  35    890996  19     25441   7     0.5
c  1 5         10862   2      3893   1      1799   3   1650204  10    395039   8     13323   4     0.3
c  2 6         53396  10     27012   8      5877   9   3351240  20<  1079025  23<    58738  16     1.5
c  3 9        122536  23     77798  23      9248  14   3065783  19   1211441  25    110668  31<    2.6
c  4 14       128168  24<    92177  28<    11636  18   1400422   9    665774  14     82336  23     3.5
c  5 21        85777  16     60156  18     12033  18<   687621   4    318819   7     38362  11     2.6
c  6 30        50609  10     33701  10     10193  15    317144   2    134763   3     17601   5     1.9
c  7 41        31479   6     20119   6      7621  11    139776   1     57719   1      8624   2     1.7
c  8 54        17843   3     11057   3      4825   7     50290   0     22129   0      3189   1     1.3
c  9 69         7443   1      4284   1      2384   4     15033   0      6588   0       945   0     0.5
c 10 86         1981   0      1000   0       774   1      4053   0      1637   0       299   0     0.2
c 11 126         113   0        60   0        37   0       368   0       105   0        11   0     0.0
c 12 230           5   0         3   0         2   0        27   0         4   0         1   0     0.0
c 
c avg                  4.1           4.3           5.0           1.8           2.5           3.3
c std                  1.9           1.7           2.0           1.8           1.7           1.6
c 
c   71.508  29% elim
c   16.571   7% bump
c   13.139   5% decide
c   10.646   4% block
c    8.368   3% probe
c    7.874   3% unhide
c    2.999   1% sweep
c    2.559   1% quatres
c    2.280   1% cce
c    2.226   1% bca
c 
c    2.642 < 1% rest (below)
c 
c    0.951   0% ternres
c    0.790   0% gauss
c    0.767   0% transred
c    0.134   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.866   2% preprocessing     3%
c  112.890  46% inprocessing     97%
c ==================================
c  116.756  47% simplifying
c  130.503  53% search
c ==================================
c  247.261 100% all
c 
c        546840 conflicts,        2211.6 confs/sec
c          2968 ternaries,         184.2 confs/ternary
c          1127 binaries,          485.2 confs/binary
c            17 iterations,      32167.1 confs/iteration
c 
c            12 reductions,          0.0 redus/sec,  45570.0 confs/reduction
c         13008 restarts,           52.6 rests/sec,     42.0 confs/restart
c      20693888 decisions,       83692.5 decis/sec,     37.8 decis/conflict
c     551199764 propagations,  2229221.7 props/sec,     26.6 props/decision
c 
c 247.3 seconds, 69.3 MB
c launch: done
