c launch: /data/cnf/sc2014/app/9dlx_vliw_at_b_iq6.used-as.sat04-347.cnf.bz2
c host: atom05
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_iq6.used-as.sat04-347.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/9dlx_vliw_at_b_iq6.used-as.sat04-347.cnf.bz2
c no embedded options
c found 'p cnf 209724 3634677' header
c read 209724 variables, 3634677 clauses, 10547961 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 209723 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  209723  3634676         0       0      0     0    0     0   98   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 908669 based on 3634676 irredundant clauses
c [card-1] found 5 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 908669 for elimination
c [card-1] 5 out of 5 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 9 variables
c [simpleprobe-1] all 209715 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 7269278 based on 3634639 irredundant clauses
c [simpleprobe-1] 200437 variables remain 96% (9278 retained 4%)
c [simpleprobe-1] removed 0 variables, found 1948 hbrs, 0 units
c [unhide-1] limit 227164 based on 3634639 irredundant clauses
c [unhide-1-1] 448 units, 0 failed, 4678 tauts, 0 hbrs, 42964 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 209267 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 208401 not tried 100% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 866 = 0% variables out of 209267 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3618122 negative 100.0% of 3618654 except 532 0.0%
c [phase-count-1] 946457 positive 26.2% of 3618654 except 2672197 73.8%
c [phase-count-1] less non-negative clauses 532 than limit 361800 (10.0%)
c [phase-count-1] non-pos/non-neg = 2672197/532 = 5022.93 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 208401 negative 100%
c [sort-queue-1] sorted 208401 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 208401 (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 1314 variables 0.6% (208401 remain 99%)
c [simplification-1] removed 16022 irredundant clauses 0.4% (3618654 remain 100%)
c [simplification-1] maximum reduction of 1% = max (1%, 0%)
c [simplification-1] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-1] new conflict interval 10000
c [simplification-1] penalized conflict interval 10000 = 1 * 10000
c [simplification-1] hard conflict limit 20000 (soft 10000 + delta 10000)
c [simplification-1] new conflict limit 10000 (hard 20000)
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [treelook-1] limit 904663 based on 3618654 irredundant clauses
c [treelook-1] scheduled 157880 literals 38%
c [treelook-1] scheduling used 905650 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 904663 based on 3618654 irredundant clauses
c [treelook-1] used 1120449 steps
c [treelook-1] 157877 literals remain 38%
c [treelook-1] 151775 variables remain to probed next time 73%
c [treelook-1] removed 2 variables, found 30 hbrs
c [basicprobe-1] limit 28947944 based on 3618493 irredundant clauses
c [basicprobe-1-0] 206744 probes remain 99% after last round
c [basicprobe-1-0] 60 units = 60 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 60 variables, found 23997 hbrs
c [unhide-2] limit 226155 based on 3618493 irredundant clauses
c [unhide-2-2] 4677 units, 22 failed, 181 tauts, 0 hbrs, 90503 literals
c [elim-2] 196665 variables 100% will be scheduled this time
c [elim-2] scheduled 196665 variables 100%
c [elim-2] limit of 15194513 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 191050 not tried 97% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 5615 = 3% variables out of 196665 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 158389 enqueued variables after 5283 conflicts
c [score-dist-2] active 32661 (17%), one 0 (0%), zero 158389 (83%)
c [score-dist-2] max exp 514, different 13 (3%)
c [score-dist-2] median active exp 513, avg 512.5
c [simplification-2] removed 17351 variables 8.3% (191050 remain 91%)
c [simplification-2] removed 258790 irredundant clauses 7.2% (3359864 remain 92%)
c [simplification-2] maximum reduction of 8% = max (8%, 7%)
c [simplification-2] forced so keeping old conflict interval 10000
c [simplification-2] conflict limit remains at 10000 (hard 20000)
c [simplification-2] 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   35.2  191049  3359864      7557    6856    246 25492   24  1200  118   2%     97 1123   32    3 1118%
c 
c [simplification-3] limit 10000 conflicts (hard 20000) hit after 10003 conflicts
c [card-2] limit 839966 based on 3359864 irredundant clauses
c [card-2] found 5 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 839966 for elimination
c [card-2] 5 out of 5 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 3492 variables
c [simpleprobe-2] 179294 schedulable variables 96%
c [simpleprobe-2] limit 6629214 based on 3314607 irredundant clauses
c [simpleprobe-2] 179414 variables remain 96% (8144 retained 4%)
c [simpleprobe-2] removed 0 variables, found 2055 hbrs, 0 units
c [unhide-3] limit 207162 based on 3314607 irredundant clauses
c [unhide-3-3] 112 units, 6 failed, 15786 tauts, 0 hbrs, 34272 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 185468 variables 100%
c [elim-3] limit of 27055501 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 180291 not tried 97% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 5177 = 3% variables out of 185468 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 137555 enqueued variables after 10003 conflicts
c [score-dist-3] active 42736 (24%), one 0 (0%), zero 137555 (76%)
c [score-dist-3] max exp 515, different 14 (3%)
c [score-dist-3] median active exp 514, avg 513.5
c [simplification-3] removed 8164 variables 4.3% (180291 remain 86%)
c [simplification-3] removed 111150 irredundant clauses 3.3% (3248714 remain 89%)
c [simplification-3] maximum reduction of 4% = max (4%, 3%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 14000
c [simplification-3] penalized conflict interval 14000 = 1 * 14000
c [simplification-3] hard conflict limit 34003 (soft 24003 + delta 10000)
c [simplification-3] new conflict limit 24003 (hard 34003)
c 
c [simplification-4] limit 24003 conflicts (hard 34003) hit after 24003 conflicts
c [decomp-7] removed 24 variables
c [treelook-2] limit 812169 based on 3248676 irredundant clauses
c [treelook-2] scheduled 149618 literals 41%
c [treelook-2] scheduling used 812184 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 812169 based on 3248676 irredundant clauses
c [treelook-2] used 824636 steps
c [treelook-2] 149616 literals remain 41%
c [treelook-2] 123989 variables remain to probed next time 69%
c [treelook-2] removed 0 variables, found 34 hbrs
c [unhide-4] limit 203042 based on 3248676 irredundant clauses
c [unhide-4-4] 4154 units, 12 failed, 634 tauts, 0 hbrs, 64096 literals
c [elim-4] 176062 variables 100% will be scheduled this time
c [elim-4] scheduled 176062 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1199444095 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 40043 variables 23% in round 1 in 966143429 steps
c [elim-4-1] backward subsumption/strengthening limit 233300666
c [elim-4-1-1] backward checking 145796 touched variables 83%
c [elim-4-1-1] incomplete backward checking 145792 remain 100%
c [elim-4-1] subsumed 2 and strengthened 1 clauses in 233335185 steps
c [elim-4] incomplete 13 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 40043 = 23% variables out of 176062 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 82812 enqueued variables after 24003 conflicts
c [score-dist-4] active 53207 (39%), one 0 (0%), zero 82812 (61%)
c [score-dist-4] max exp 516, different 13 (3%)
c [score-dist-4] median active exp 515, avg 515.0
c [simplification-4] removed 44272 variables 24.6% (136019 remain 65%)
c [simplification-4] removed 242067 irredundant clauses 7.5% (3006647 remain 83%)
c [simplification-4] maximum reduction of 25% = max (25%, 7%)
c [simplification-4] large reduction 25% >= 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 36003 (soft 26003 + delta 10000)
c [simplification-4] new conflict limit 26003 (hard 36003)
c 
c [simplification-5] limit 26003 conflicts (hard 36003) hit after 26005 conflicts
c [quatres-1] found 34871 quaternary clauses 16% in total
c [quatres-1-1] removed 4 duplicate quaternary clauses
c [quatres-1-2] added 91 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1914 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 16082148 with penalty 2 = 0 + 2
c [ternres-1] all 136019 free variables schedulable
c [ternres-1] 35054 ternary resolvents (0 bin, 35054 trn)
c [ternres-1] 7298 variables remain 5% (128721 retained 95%)
c [gauss-1] limit 1503323 based on 3006646 irredundant clauses
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 45 variables
c [basicprobe-2] limit 24048552 based on 3006069 irredundant clauses
c [basicprobe-2-0] 127782 probes remain 95% after last round
c [basicprobe-2-0] 47 units = 47 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1268 variables, found 15301 hbrs
c [unhide-5] limit 321642 with penalty 3 = 0 + 3
c [unhide-5-5] 318 units, 12 failed, 30873 tauts, 0 hbrs, 26685 literals
c [transred-1] limit 2953134 based on 2953134 irredundant clauses
c [transred-1] removed 1 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 134373 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 643285985 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 232414 blocked clauses
c [cce-1] limit of 32164299 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 149
c [cce-1-1] eliminated 1 clauses out of 7 (14%) of length 141
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 137
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 133
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 130
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 129
c [cce-1-1] eliminated 5 clauses out of 6 (83%) of length 127
c [cce-1-1] eliminated 10 clauses out of 11 (91%) of length 125
c [cce-1-1] eliminated 2 clauses out of 7 (29%) of length 124
c [cce-1-1] eliminated 6 clauses out of 9 (67%) of length 123
c [cce-1-1] eliminated 4 clauses out of 23 (17%) of length 122
c [cce-1-1] eliminated 3 clauses out of 15 (20%) of length 121
c [cce-1-1] eliminated 13 clauses out of 29 (45%) of length 120
c [cce-1-1] eliminated 7 clauses out of 31 (23%) of length 119
c [cce-1-1] eliminated 7 clauses out of 29 (24%) of length 118
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 65 large clauses in 32164370 steps
c [cce-1-1] allowing another 16082185 steps for small clauses
c [cce-1-1] scheduling 2479385 clauses = 2409707 binary + 69678 ternary
c [cce-1-1] tried to eliminate 45 small clauses 0%
c [cce-1-1] eliminated 33 binary clauses 0%
c [cce-1-1] eliminated 33 small clauses 0%
c [cce-1-1] eliminated 33 small clauses in 32174025 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 98 covered clauses in round 1
c [cce-1] eliminated 98 covered clauses in TOTAL during 1 rounds
c [cce-1] 98 < 1/100 * 2712812 = 27128 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 130865 variables 100%
c [elim-5] limit of 128657197 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 49894 not tried 38% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 5726 = 4% variables out of 130865 scheduled
c [bca-1] limit of 10000000 steps and 5395900 added (scaled 2)
c [bca-1] 222303 out of 250280 literals actually usable 89%
c [bca-1] added 28924 blocked clauses in 818314 steps
c [sweep-1] limit 5395400 based on 2697700 irredundant clauses
c [sweep-1-1] 3248 pos 2.6% + 121891 neg 97.4% = 125139 sched 100.0% ret 0
c [sweep-1-1] 5551228 steps 17 queries 12979.76 avg class size
c [sweep-1-1] 368 decisions 13 SAT calls 1257.69 avg env size
c [sweep-1-1] 125042 variables remain 100% (97 retained 0%)
c [decomp-10] removed 31 variables
c [sweep-1-1] removed 31 vars (0 failed, 3 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 31 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-5] sorted 73352 enqueued variables after 26005 conflicts
c [score-dist-5] active 51756 (41%), one 0 (0%), zero 73352 (59%)
c [score-dist-5] max exp 516, different 13 (3%)
c [score-dist-5] median active exp 515, avg 515.1
c [simplification-5] removed 10911 variables 8.0% (125108 remain 60%)
c [simplification-5] removed 310458 irredundant clauses 10.3% (2696188 remain 74%)
c [simplification-5] maximum reduction of 10% = max (8%, 10%)
c [simplification-5] large reduction 10% >= 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 38005 (soft 28005 + delta 10000)
c [simplification-5] new conflict limit 28005 (hard 38005)
c 
c [simplification-6] limit 28005 conflicts (hard 38005) hit after 28005 conflicts
c [quatres-2] found 35829 quaternary clauses 17% in total
c [quatres-2-2] added 2 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2345 quaternary resolvents
c [ternres-2] limit 10784692 based on 2696173 irredundant clauses
c [ternres-2] 7087 schedulable variables 6%
c [ternres-2] 13765 ternary resolvents (1 bin, 13764 trn)
c [ternres-2] 5616 variables remain 4% (119492 retained 96%)
c [card-3] limit 858129 penalty 3 = 2 + 1
c [card-3] found 13 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 858129 for elimination
c [card-3] 13 out of 13 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-6] limit 343251 with penalty 3 = 0 + 3
c [unhide-6-6] 1296 units, 6 failed, 1271 tauts, 0 hbrs, 34574 literals
c [transred-2] limit 2694897 based on 2694897 irredundant clauses
c [transred-2] removed 2 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 123374 variables 100%
c [block-2] limit of 68650361 steps penalty 1 = 0 + 1
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 54741 blocked clauses
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 123193 variables 100%
c [elim-6] limit of 137300722 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 37626 not tried 31% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1481 = 1% variables out of 123193 scheduled
c [bca-2] limit of 10000000 steps and 5225060 added (scaled 2)
c [bca-2] 211726 out of 243426 literals actually usable 87%
c [bca-2] added 3161 blocked clauses in 768501 steps
c [sweep-2] limit 5210098 based on 2605049 irredundant clauses
c [sweep-2-1] 4093 pos 3.4% + 117525 neg 96.6% = 121618 sched 99.9% ret 94
c [sweep-2-1] 5338707 steps 30 queries 12401.07 avg class size
c [sweep-2-1] 1257 decisions 26 SAT calls 315.04 avg env size
c [sweep-2-1] 119500 variables remain 100% (404 retained 0%)
c [decomp-12] removed 1830 variables
c [sweep-2-1] removed 1830 vars (0 failed, 4 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 1830 vars in TOTAL (1 rounds, 29 queries)
c [sort-queue-6] sorted 68980 enqueued variables after 28005 conflicts
c [score-dist-6] active 50902 (42%), one 0 (0%), zero 68980 (58%)
c [score-dist-6] max exp 516, different 13 (3%)
c [score-dist-6] median active exp 516, avg 515.1
c [simplification-6] removed 5226 variables 4.2% (119882 remain 57%)
c [simplification-6] removed 126904 irredundant clauses 4.7% (2569282 remain 71%)
c [simplification-6] maximum reduction of 5% = max (4%, 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 40005 (soft 30005 + delta 10000)
c [simplification-6] new conflict limit 30005 (hard 40005)
c 
c [simplification-7] limit 30005 conflicts (hard 40005) hit after 30005 conflicts
c [quatres-3] found 37870 quaternary clauses 19% in total
c [quatres-3-2] added 8 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1074 quaternary resolvents
c [ternres-3] limit 10277120 based on 2569280 irredundant clauses
c [ternres-3] 5552 schedulable variables 5%
c [ternres-3] 26167 ternary resolvents (0 bin, 26167 trn)
c [ternres-3] 1297 variables remain 1% (118585 retained 99%)
c [gauss-2] limit 1284640 based on 2569280 irredundant clauses
c [gauss-2] extracted 1 xors of average arity 3.0
c [gauss-2] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-2] limit 1284640 based on 2569280 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-7] limit 361679 with penalty 3 = 0 + 3
c [unhide-7-7] 57 units, 2 failed, 28187 tauts, 0 hbrs, 16669 literals
c [transred-3] limit 2543174 based on 2543174 irredundant clauses
c [transred-3] removed 0 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 119823 variables 100%
c [block-3] limit of 72335999 steps penalty 1 = 0 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 158175 blocked clauses
c [cce-2] limit of 18083999 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 138
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 134
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 124
c [cce-2-1] eliminated 1 clauses out of 12 (8%) of length 118
c [cce-2-1] eliminated 8 clauses out of 24 (33%) of length 117
c [cce-2-1] eliminated 4 clauses out of 52 (8%) of length 116
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 16 large clauses in 18084627 steps
c [cce-2-1] allowing another 9042313 steps for small clauses
c [cce-2-1] scheduling 2165072 clauses = 2096159 binary + 68913 ternary
c [cce-2-1] tried to eliminate 115 small clauses 0%
c [cce-2-1] eliminated 9 binary clauses 0%
c [cce-2-1] eliminated 9 small clauses 0%
c [cce-2-1] eliminated 9 small clauses in 18087435 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 25 covered clauses in round 1
c [cce-2] eliminated 25 covered clauses in TOTAL during 1 rounds
c [cce-2] 25 < 1/100 * 2383665 = 23836 considered unsuccessful
c [elim-7] 37046 variables 31% will be scheduled this time
c [elim-7] scheduled 37046 variables 31%
c [elim-7] limit of 144671998 steps penalty 1 = 0 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 9917 not tried 8% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 1345 = 4% variables out of 37046 scheduled
c [bca-3] limit of 10000000 steps and 4769792 added (scaled 2)
c [bca-3] 202698 out of 234914 literals actually usable 86%
c [bca-3] added 5616 blocked clauses in 736313 steps
c [sweep-3] limit 4753250 based on 2376625 irredundant clauses
c [sweep-3-1] 3684 pos 3.1% + 113386 neg 96.9% = 117070 sched 99.7% ret 386
c [sweep-3-1] 4824573 steps 8 queries 25822.38 avg class size
c [sweep-3-1] 365 decisions 7 SAT calls 2212.29 avg env size
c [sweep-3-1] 117053 variables remain 100% (402 retained 0%)
c [decomp-14] removed 14 variables
c [sweep-3-1] removed 14 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 14 vars in TOTAL (1 rounds, 7 queries)
c [sort-queue-7] sorted 66354 enqueued variables after 30005 conflicts
c [score-dist-7] active 51088 (44%), one 0 (0%), zero 66354 (56%)
c [score-dist-7] max exp 516, different 13 (3%)
c [score-dist-7] median active exp 516, avg 515.2
c [simplification-7] removed 2440 variables 2.0% (117442 remain 56%)
c [simplification-7] removed 196603 irredundant clauses 7.7% (2372677 remain 65%)
c [simplification-7] maximum reduction of 8% = max (2%, 8%)
c [simplification-7] large reduction 8% >= 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 42005 (soft 32005 + delta 10000)
c [simplification-7] new conflict limit 32005 (hard 42005)
c 
c [simplification-8] limit 32005 conflicts (hard 42005) hit after 32005 conflicts
c [quatres-4] found 35631 quaternary clauses 18% in total
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1033 quaternary resolvents
c [ternres-4] limit 9490700 based on 2372675 irredundant clauses
c [ternres-4] 1296 schedulable variables 1%
c [ternres-4] 34 ternary resolvents (0 bin, 34 trn)
c [ternres-4] 1290 variables remain 1% (116152 retained 99%)
c [simpleprobe-3] 112324 schedulable variables 96%
c [simpleprobe-3] limit 7488076 penalty 3 = 2 + 1
c [simpleprobe-3] 112344 variables remain 96% (5098 retained 4%)
c [simpleprobe-3] removed 0 variables, found 632 hbrs, 0 units
c [unhide-8] limit 374403 with penalty 3 = 0 + 3
c [unhide-8-8] 1759 units, 14 failed, 1999 tauts, 0 hbrs, 29020 literals
c [block-4] scheduling all variables this time
c [block-4] scheduled 114083 variables 100%
c [block-4] limit of 74880766 steps penalty 1 = 0 + 1
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 23692 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 113960 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2995230670 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3492 variables 3% in round 1 in 962460484 steps
c [elim-8-1] backward subsumption/strengthening limit 962460400
c [elim-8-1-1] backward checking 32421 touched variables 28%
c [elim-8-1-1] incomplete backward checking 32570 remain 100%
c [elim-8-1] subsumed 68 and strengthened 106 clauses in 962462769 steps
c [elim-8-1] rescheduled 520 variables 0% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 52234701 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 3492 = 3% variables out of 113960 scheduled
c [bca-4] limit of 10000000 steps and 4510786 added (scaled 2)
c [bca-4] 189280 out of 220938 literals actually usable 86%
c [bca-4] added 6732 blocked clauses in 701193 steps
c [sweep-4] limit 4491436 based on 2245718 irredundant clauses
c [sweep-4-1] 2965 pos 2.7% + 107127 neg 97.3% = 110092 sched 99.7% ret 376
c [sweep-4-1] 4495705 steps 13 queries 19500.85 avg class size
c [sweep-4-1] 409 decisions 12 SAT calls 431.58 avg env size
c [sweep-4-1] 110027 variables remain 100% (441 retained 0%)
c [decomp-17] removed 19 variables
c [sweep-4-1] removed 19 vars (0 failed, 0 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 19 vars in TOTAL (1 rounds, 12 queries)
c [sort-queue-8] sorted 61125 enqueued variables after 32005 conflicts
c [score-dist-8] active 49324 (45%), one 0 (0%), zero 61125 (55%)
c [score-dist-8] max exp 516, different 13 (3%)
c [score-dist-8] median active exp 516, avg 515.2
c [simplification-8] removed 6993 variables 6.0% (110449 remain 53%)
c [simplification-8] removed 126997 irredundant clauses 5.4% (2245678 remain 62%)
c [simplification-8] maximum reduction of 6% = max (6%, 5%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 44005 (soft 34005 + delta 10000)
c [simplification-8] new conflict limit 34005 (hard 44005)
c 
c [simplification-9] limit 34005 conflicts (hard 44005) hit after 34005 conflicts
c [quatres-5] found 31557 quaternary clauses 18% in total
c [quatres-5-2] added 793 single-self-subsuming ternary resolvents
c [quatres-5-2] added 825 quaternary resolvents
c [ternres-5] limit 8982676 based on 2245669 irredundant clauses
c [ternres-5] 1269 schedulable variables 1%
c [ternres-5] 3927 ternary resolvents (1 bin, 3926 trn)
c [ternres-5] 1014 variables remain 1% (109435 retained 99%)
c [decomp-18] removed 1 variables
c [unhide-9] limit 390417 with penalty 3 = 0 + 3
c [unhide-9-9] 7 units, 1 failed, 12160 tauts, 0 hbrs, 15563 literals
c [transred-4] limit 2234073 based on 2234073 irredundant clauses
c [transred-4] removed 4 transitive binary clauses
c [transred-4] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 110439 variables 100%
c [block-5] limit of 78083554 steps penalty 1 = 0 + 1
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 54967 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 110209 variables 100%
c [elim-9] limit of 156167108 steps penalty 1 = 0 + 1
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 11610 not tried 11% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1705 = 2% variables out of 110209 scheduled
c [bca-5] limit of 10000000 steps and 4369254 added (scaled 2)
c [bca-5] 184051 out of 217010 literals actually usable 85%
c [bca-5] added 2721 blocked clauses in 698786 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 23425065 penalty 1 = 0 + 1
c [sweep-5-1] 3307 pos 3.1% + 104758 neg 96.9% = 108065 sched 99.6% ret 439
c [sweep-5-1] 23448765 steps 106 queries 5557.74 avg class size
c [sweep-5-1] 3223 decisions 90 SAT calls 290.23 avg env size
c [sweep-5-1] 106160 variables remain 98% (1939 retained 2%)
c [decomp-19] removed 438 variables
c [sweep-5-1] removed 438 vars (1 failed, 18 eqs, 34 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 438 vars in TOTAL (1 rounds, 105 queries)
c [sort-queue-9] sorted 58295 enqueued variables after 34005 conflicts
c [score-dist-9] active 49771 (46%), one 0 (0%), zero 58295 (54%)
c [score-dist-9] max exp 517, different 14 (3%)
c [score-dist-9] median active exp 516, avg 515.3
c [simplification-9] removed 2383 variables 2.2% (108066 remain 52%)
c [simplification-9] removed 89802 irredundant clauses 4.0% (2155869 remain 59%)
c [simplification-9] maximum reduction of 4% = max (2%, 4%)
c [simplification-9] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-9] new conflict interval 18000
c [simplification-9] penalized conflict interval 18000 = 1 * 18000
c [simplification-9] hard conflict limit 62005 (soft 52005 + delta 10000)
c [simplification-9] new conflict limit 52005 (hard 62005)
c 
c [simplification-10] limit 52005 conflicts (hard 62005) hit after 52005 conflicts
c [quatres-6] found 29197 quaternary clauses 17% in total
c [quatres-6-2] added 507 single-self-subsuming ternary resolvents
c [quatres-6-2] added 985 quaternary resolvents
c [ternres-6] limit 10506400 with penalty 1 = 0 + 1
c [ternres-6] 1004 schedulable variables 1%
c [ternres-6] 5525 ternary resolvents (1 bin, 5524 trn)
c [ternres-6] 369 variables remain 0% (107697 retained 100%)
c [card-4] limit 656650 penalty 4 = 3 + 1
c [card-4] found 16 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 656650 for elimination
c [card-4] 16 out of 16 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1077912 based on 2155825 irredundant clauses
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 538956 based on 2155825 irredundant clauses
c [treelook-3] scheduled 81880 literals 38%
c [treelook-3] scheduling used 539092 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 538956 based on 2155825 irredundant clauses
c [treelook-3] used 1315966 steps
c [treelook-3] 81874 literals remain 38%
c [treelook-3] 69536 variables remain to probed next time 64%
c [treelook-3] removed 1 variables, found 3 hbrs
c [unhide-10] limit 525320 with penalty 3 = 0 + 3
c [unhide-10-10] 2389 units, 13 failed, 1614 tauts, 0 hbrs, 29144 literals
c [transred-5] limit 2149675 based on 2149675 irredundant clauses
c [transred-5] removed 8 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 104201 variables 100%
c [block-6] limit of 105064003 steps penalty 1 = 0 + 1
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 53699 blocked clauses
c [cce-3] limit of 13133000 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 2 clauses out of 5 (40%) of length 137
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 128
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 3 large clauses in 13133203 steps
c [cce-3-1] allowing another 6566601 steps for small clauses
c [cce-3-1] scheduling 1859124 clauses = 1795873 binary + 63251 ternary
c [cce-3-1] tried to eliminate 82 small clauses 0%
c [cce-3-1] eliminated 3 binary clauses 0%
c [cce-3-1] eliminated 3 small clauses 0%
c [cce-3-1] eliminated 3 small clauses in 13139691 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 6 covered clauses in round 1
c [cce-3] eliminated 6 covered clauses in TOTAL during 1 rounds
c [cce-3] 6 < 1/100 * 2040027 = 20400 considered unsuccessful
c [elim-10] 11514 variables 11% will be scheduled this time
c [elim-10] scheduled 11514 variables 11%
c [elim-10] limit of 210128006 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 3699 not tried 4% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 22 = 0% variables out of 11514 scheduled
c [elim-10] 22 < 1/100 * 11514 = 115 considered unsuccessful
c [bca-6] limit of 10000000 steps and 4099683 added (scaled 2)
c [bca-6] 168501 out of 207352 literals actually usable 81%
c [bca-6] added 6703 blocked clauses in 640119 steps
c [sweep-6] limit 4075606 based on 2037803 irredundant clauses
c [sweep-6-1] 2961 pos 2.9% + 98822 neg 97.1% = 101783 sched 98.2% ret 1892
c [sweep-6-1] 4249966 steps 13 queries 13324.15 avg class size
c [sweep-6-1] 387 decisions 12 SAT calls 110.83 avg env size
c [sweep-6-1] 101735 variables remain 98% (1940 retained 2%)
c [decomp-22] removed 467 variables
c [sweep-6-1] removed 467 vars (0 failed, 0 eqs, 2 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 467 vars in TOTAL (1 rounds, 12 queries)
c [sort-queue-10] sorted 52479 enqueued variables after 52005 conflicts
c [score-dist-10] active 50729 (49%), one 0 (0%), zero 52479 (51%)
c [score-dist-10] max exp 517, different 14 (3%)
c [score-dist-10] median active exp 517, avg 516.0
c [simplification-10] removed 4858 variables 4.5% (103208 remain 49%)
c [simplification-10] removed 119066 irredundant clauses 5.5% (2036799 remain 56%)
c [simplification-10] maximum reduction of 6% = max (4%, 6%)
c [simplification-10] large reduction 6% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 64005 (soft 54005 + delta 10000)
c [simplification-10] new conflict limit 54005 (hard 64005)
c 
c [simplification-11] limit 54005 conflicts (hard 64005) hit after 54005 conflicts
c [quatres-7] found 27527 quaternary clauses 17% in total
c [quatres-7-1] removed 10 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 451 quaternary resolvents
c [ternres-7] limit 10708789 with penalty 1 = 0 + 1
c [ternres-7] 366 schedulable variables 0%
c [ternres-7] 3258 ternary resolvents (0 bin, 3258 trn)
c [ternres-7] 68 variables remain 0% (103140 retained 100%)
c [basicprobe-3] limit 53543946 penalty 1 = 0 + 1
c [basicprobe-3-0] 92297 probes remain 92% after last round
c [basicprobe-3-0] 71 units = 71 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 2368 variables, found 5329 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-11] limit 535439 with penalty 3 = 0 + 3
c [unhide-11-11] 472 units, 19 failed, 20820 tauts, 0 hbrs, 19206 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 100353 variables 100%
c [block-7] limit of 214175785 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 9459 blocked clauses
c [block-7] 9459 < 1/100 * 1975690 = 19756 considered unsuccessful
c [bca-7] limit of 10000000 steps and 3949914 added (scaled 2)
c [bca-7] 160532 out of 199476 literals actually usable 80%
c [bca-7] added 3185 blocked clauses in 589452 steps
c [sweep-7] limit 6425273 penalty 0 = 0 + 0
c [sweep-7-1] 3051 pos 3.1% + 94771 neg 96.9% = 97822 sched 98.1% ret 1915
c [sweep-7-1] 6512398 steps 55 queries 11909.31 avg class size
c [sweep-7-1] 1555 decisions 47 SAT calls 113.28 avg env size
c [sweep-7-1] 97035 variables remain 97% (2702 retained 3%)
c [decomp-24] removed 325 variables
c [sweep-7-1] removed 325 vars (0 failed, 7 eqs, 15 impls)
c [sweep-7] removed 325 vars in TOTAL (1 rounds, 54 queries)
c [sort-queue-11] sorted 50237 enqueued variables after 54005 conflicts
c [score-dist-11] active 49175 (49%), one 0 (0%), zero 50237 (51%)
c [score-dist-11] max exp 517, different 14 (3%)
c [score-dist-11] median active exp 517, avg 516.0
c [simplification-11] removed 3796 variables 3.7% (99412 remain 47%)
c [simplification-11] removed 76129 irredundant clauses 3.7% (1960670 remain 54%)
c [simplification-11] maximum reduction of 4% = max (4%, 4%)
c [simplification-11] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-11] new conflict interval 22000
c [simplification-11] penalized conflict interval 22000 = 1 * 22000
c [simplification-11] hard conflict limit 87005 (soft 76005 + delta 11000)
c [simplification-11] new conflict limit 76005 (hard 87005)
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 -  323.6   99412  1960670     70398   20779  72038 96815   33   765   99   4%    623  297   40   20  204%
c 
c [simplification-12] limit 76005 conflicts (hard 87005) hit after 76005 conflicts
c [quatres-8] found 26205 quaternary clauses 18% in total
c [quatres-8-1] removed 6 duplicate quaternary clauses
c [quatres-8-2] added 45 single-self-subsuming ternary resolvents
c [quatres-8-2] added 314 quaternary resolvents
c [ternres-8] limit 25779589 with penalty 0 = 0 + 0
c [ternres-8] 63 schedulable variables 0%
c [ternres-8] 983 ternary resolvents (1 bin, 982 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-25] removed 2 variables
c [unhide-12] limit 644489 with penalty 3 = 0 + 3
c [unhide-12-12] 351 units, 31 failed, 1325 tauts, 0 hbrs, 32894 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 4 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 98766 variables 100%
c [elim-11] limit of 257795894 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 5650 not tried 6% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 3373 = 3% variables out of 98766 scheduled
c [bca-8] limit of 10000000 steps and 3884225 added (scaled 2)
c [bca-8] 157171 out of 190788 literals actually usable 82%
c [bca-8] added 2777 blocked clauses in 579332 steps
c [sweep-8] limit 7733876 penalty 0 = 0 + 0
c [sweep-8-1] 3249 pos 3.5% + 89553 neg 96.5% = 92802 sched 97.3% ret 2591
c [sweep-8-1] 7841427 steps 58 queries 5791.84 avg class size
c [sweep-8-1] 2324 decisions 53 SAT calls 220.85 avg env size
c [sweep-8-1] 91960 variables remain 96% (3433 retained 4%)
c [decomp-26] removed 15 variables
c [sweep-8-1] removed 15 vars (0 failed, 4 eqs, 9 impls)
c [sweep-8] 15 < 1/1000 * 95393 = 95 considered unsuccessful
c [sweep-8] removed 15 vars in TOTAL (1 rounds, 57 queries)
c [sort-queue-12] sorted 42679 enqueued variables after 76005 conflicts
c [score-dist-12] active 52699 (55%), one 0 (0%), zero 42679 (45%)
c [score-dist-12] max exp 518, different 14 (3%)
c [score-dist-12] median active exp 517, avg 516.7
c [simplification-12] removed 4034 variables 4.1% (95378 remain 45%)
c [simplification-12] removed 33175 irredundant clauses 1.7% (1927493 remain 53%)
c [simplification-12] maximum reduction of 4% = max (4%, 2%)
c [simplification-12] geometric conflict interval increment 4400 = 22000 / 5
c [simplification-12] new conflict interval 26400
c [simplification-12] penalized conflict interval 26400 = 1 * 26400
c [simplification-12] hard conflict limit 115605 (soft 102405 + delta 13200)
c [simplification-12] new conflict limit 102405 (hard 115605)
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  340.8   95377  1927481     81733   30324  71100 70272   22   374  101   6%    686 -150   16   20   79%
c i  341.2   95376  1927481     84502   32529  71106 70281   18   217  101   8%   -350 -297   12   20   58%
c 
c [simplification-13] limit 102405 conflicts (hard 115605) hit after 109355 conflicts
c [quatres-9] found 28950 quaternary clauses 20% in total
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 24 single-self-subsuming ternary resolvents
c [quatres-9-2] added 654 quaternary resolvents
c [ternres-9] limit 29809631 with penalty 0 = 0 + 0
c [ternres-9] all 95376 free variables schedulable
c [ternres-9] 5008 ternary resolvents (3 bin, 5005 trn)
c [ternres-9] 10435 variables remain 11% (84941 retained 89%)
c [decomp-27] removed 30 variables
c [unhide-13] limit 745240 with penalty 3 = 0 + 3
c [unhide-13-13] 63 units, 6 failed, 15366 tauts, 0 hbrs, 37505 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 5 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 95279 variables 100%
c [block-8] limit of 149048155 steps penalty 1 = 1 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 8366 blocked clauses
c [block-8] 8366 < 1/100 * 1911855 = 19118 considered unsuccessful
c [elim-12] 3652 variables 4% will be scheduled this time
c [elim-12] scheduled 3652 variables 4%
c [elim-12] limit of 596192623 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 459 not tried 0% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 5 = 0% variables out of 3652 scheduled
c [elim-12] 5 < 1/100 * 3652 = 36 considered unsuccessful
c [bca-9] limit of 10000000 steps and 3831479 added (scaled 2)
c [bca-9] 148067 out of 189426 literals actually usable 78%
c [bca-9] added 2190 blocked clauses in 558613 steps
c [sort-queue-13] sorted 38728 enqueued variables after 109355 conflicts
c [score-dist-13] active 55984 (59%), one 0 (0%), zero 38728 (41%)
c [score-dist-13] max exp 518, different 14 (3%)
c [score-dist-13] median active exp 518, avg 517.1
c [simplification-13] removed 664 variables 0.7% (94712 remain 45%)
c [simplification-13] removed 26946 irredundant clauses 1.4% (1900535 remain 52%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 13200 = 26400 / 2
c [simplification-13] new conflict interval 39600
c [simplification-13] penalized conflict interval 39600 = 1 * 39600
c [simplification-13] hard conflict limit 168755 (soft 148955 + delta 19800)
c [simplification-13] new conflict limit 148955 (hard 168755)
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 -  379.1   94712  1900535    116558   27749  74277 67885   31   857   98   4%    107  328   28   24  117%
c 
c [simplification-14] limit 148955 conflicts (hard 168755) hit after 151229 conflicts
c [quatres-10] found 26018 quaternary clauses 18% in total
c [quatres-10-2] added 34 single-self-subsuming ternary resolvents
c [quatres-10-2] added 39 quaternary resolvents
c [ternres-10] limit 35277538 with penalty 0 = 0 + 0
c [ternres-10] 10348 schedulable variables 11%
c [ternres-10] 1047 ternary resolvents (29 bin, 1018 trn)
c [ternres-10] 8637 variables remain 9% (86075 retained 91%)
c [gauss-4] limit 950265 based on 1900530 irredundant clauses
c [gauss-4] extracted 1 xors of average arity 3.0
c [gauss-4] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-4] limit 950265 based on 1900530 irredundant clauses
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 7 variables
c [unhide-14] limit 881938 with penalty 3 = 0 + 3
c [unhide-14-14] 307 units, 3 failed, 1145 tauts, 0 hbrs, 66695 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 10 transitive binary clauses
c [transred-9] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 220484616 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 49 (2%) of length 113
c [cce-4-1] eliminated 1 clauses out of 38 (3%) of length 111
c [cce-4-1] eliminated 1 clauses out of 32 (3%) of length 109
c [cce-4-1] eliminated 3 clauses out of 55 (5%) of length 108
c [cce-4-1] eliminated 3 clauses out of 91 (3%) of length 107
c [cce-4-1] eliminated 9 clauses out of 52 (17%) of length 106
c [cce-4-1] eliminated 4 clauses out of 96 (4%) of length 102
c [cce-4-1] eliminated 1 clauses out of 134 (1%) of length 101
c [cce-4-1] eliminated 4 clauses out of 80 (5%) of length 100
c [cce-4-1] eliminated 22 clauses out of 128 (17%) of length 99
c [cce-4-1] eliminated 22 clauses out of 96 (23%) of length 97
c [cce-4-1] eliminated 5 clauses out of 161 (3%) of length 96
c [cce-4-1] eliminated 4 clauses out of 176 (2%) of length 95
c [cce-4-1] eliminated 6 clauses out of 123 (5%) of length 94
c [cce-4-1] eliminated 3 clauses out of 153 (2%) of length 93
c [cce-4-1] eliminated 4 clauses out of 147 (3%) of length 92
c [cce-4-1] eliminated 4 clauses out of 113 (4%) of length 91
c [cce-4-1] eliminated 6 clauses out of 218 (3%) of length 90
c [cce-4-1] eliminated 1 clauses out of 198 (1%) of length 89
c [cce-4-1] eliminated 6 clauses out of 157 (4%) of length 88
c [cce-4-1] eliminated 8 clauses out of 177 (5%) of length 87
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 118 large clauses in 220486827 steps
c [cce-4-1] allowing another 110243413 steps for small clauses
c [cce-4-1] scheduling 1705003 clauses = 1672096 binary + 32907 ternary
c [cce-4-1] tried to eliminate 254 small clauses 0%
c [cce-4-1] eliminated 3 binary clauses 0%
c [cce-4-1] eliminated 1 ternary clauses 0%
c [cce-4-1] eliminated 4 small clauses 0%
c [cce-4-1] eliminated 5112 small clauses in 220488663 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 5230 covered clauses in round 1
c [cce-4] eliminated 5230 covered clauses in TOTAL during 1 rounds
c [cce-4] 5230 < 1/100 * 1899731 = 18997 considered unsuccessful
c [bca-10] limit of 10000000 steps and 3820506 added (scaled 2)
c [bca-10] 142931 out of 188422 literals actually usable 76%
c [bca-10] added 1862 blocked clauses in 543135 steps
c [sweep-9] limit 5291630 penalty 1 = 1 + 0
c [sweep-9-1] 3146 pos 3.5% + 87706 neg 96.5% = 90852 sched 96.4% ret 3358
c [sweep-9-1] 6294909 steps 23 queries 9205.00 avg class size
c [sweep-9-1] 460 decisions 21 SAT calls 99.90 avg env size
c [sweep-9-1] 89297 variables remain 96% (3421 retained 4%)
c [decomp-29] removed 2068 variables
c [sweep-9-1] removed 2068 vars (0 failed, 2 eqs, 3 impls)
c [sweep-9] removed 2068 vars in TOTAL (1 rounds, 22 queries)
c [sort-queue-14] sorted 32704 enqueued variables after 151229 conflicts
c [score-dist-14] active 59438 (65%), one 0 (0%), zero 32704 (35%)
c [score-dist-14] max exp 519, different 14 (3%)
c [score-dist-14] median active exp 518, avg 517.8
c [simplification-14] removed 2570 variables 2.7% (92142 remain 44%)
c [simplification-14] removed 34529 irredundant clauses 1.8% (1866006 remain 51%)
c [simplification-14] maximum reduction of 3% = max (3%, 2%)
c [simplification-14] geometric conflict interval increment 9900 = 39600 / 4
c [simplification-14] new conflict interval 49500
c [simplification-14] penalized conflict interval 49500 = 1 * 49500
c [simplification-14] hard conflict limit 225479 (soft 200729 + delta 24750)
c [simplification-14] new conflict limit 200729 (hard 225479)
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 -  406.3   92142  1866006    155111   29497  71805 68248   30   429   97   7%    515 -124   29   25  116%
c -  413.9   92142  1866006    192891   33148  71838 68292   15    30   98  50%    738 -324   13   23   56%
c 
c [simplification-15] limit 200729 conflicts (hard 225479) hit after 223432 conflicts
c [quatres-11] found 25594 quaternary clauses 19% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 121 single-self-subsuming ternary resolvents
c [quatres-11-2] added 44 quaternary resolvents
c [ternres-11] limit 38682191 with penalty 0 = 0 + 0
c [ternres-11] 8407 schedulable variables 9%
c [ternres-11] 3831 ternary resolvents (1 bin, 3830 trn)
c [ternres-11] 63 variables remain 0% (92079 retained 100%)
c [card-5] limit 1208818 penalty 4 = 4 + 0
c [card-5] found 24 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1208818 for elimination
c [card-5] 24 out of 24 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-30] removed 7 variables
c [simpleprobe-4] 88132 schedulable variables 96%
c [simpleprobe-4] limit 19341095 penalty 3 = 3 + 0
c [decomp-31] removed 10 variables
c [simpleprobe-4] 88767 variables remain 96% (3358 retained 4%)
c [simpleprobe-4] removed 10 variables, found 25972 hbrs, 0 units
c [unhide-15] limit 967054 with penalty 3 = 0 + 3
c [unhide-15-15] 6 units, 1 failed, 12413 tauts, 0 hbrs, 219681 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 7 transitive binary clauses
c [transred-10] found 1 units
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 92104 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 2229 variables 2% in round 1 in 2233187587 steps
c [elim-13-1] backward subsumption/strengthening limit 2233187500
c [elim-13-1-1] backward checking 21438 touched variables 23%
c [elim-13-1-1] incomplete backward checking 21724 remain 101%
c [elim-13-1] subsumed 0 and strengthened 235 clauses in 2233191684 steps
c [elim-13-1] rescheduled 824 variables 1% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 500666832 steps
c [elim-13-2] backward subsumption/strengthening limit 500666800
c [elim-13-2-1] backward checking 21725 touched variables 24%
c [elim-13-2-1] incomplete backward checking 21882 remain 101%
c [elim-13-2] subsumed 0 and strengthened 841 clauses in 500676623 steps
c [elim-13-2] rescheduled 2501 variables 3% by backward subsumption
c [elim-13-3] eliminated 20 variables 0% in round 3 in 817084933 steps
c [elim-13-3] backward subsumption/strengthening limit 817084900
c [elim-13-3-1] backward checking 21886 touched variables 24%
c [elim-13-3-1] incomplete backward checking 21889 remain 100%
c [elim-13-3] subsumed 18 and strengthened 89 clauses in 817090494 steps
c [elim-13] incomplete 376 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 2254 = 2% variables out of 92104 scheduled
c [bca-11] limit of 10000000 steps and 3645381 added (scaled 2)
c [bca-11] 144829 out of 179702 literals actually usable 81%
c [bca-11] added 13053 blocked clauses in 574690 steps
c [sweep-10] limit 11604657 penalty 0 = 0 + 0
c [sweep-10-1] 3342 pos 3.9% + 83175 neg 96.1% = 86517 sched 96.3% ret 3333
c [sweep-10-1] 11745390 steps 98 queries 6447.20 avg class size
c [sweep-10-1] 3281 decisions 92 SAT calls 95.46 avg env size
c [sweep-10-1] 85257 variables remain 95% (4592 retained 5%)
c [decomp-32] removed 22 variables
c [sweep-10-1] removed 22 vars (1 failed, 5 eqs, 13 impls)
c [sweep-10] 22 < 1/1000 * 89850 = 89 considered unsuccessful
c [sweep-10] removed 22 vars in TOTAL (1 rounds, 97 queries)
c [sort-queue-15] sorted 31216 enqueued variables after 223432 conflicts
c [score-dist-15] active 58612 (65%), one 0 (0%), zero 31216 (35%)
c [score-dist-15] max exp 519, different 14 (3%)
c [score-dist-15] median active exp 518, avg 517.9
c [simplification-15] removed 2314 variables 2.5% (89828 remain 43%)
c [simplification-15] removed 60151 irredundant clauses 3.2% (1805855 remain 50%)
c [simplification-15] maximum reduction of 3% = max (3%, 3%)
c [simplification-15] geometric conflict interval increment 12375 = 49500 / 4
c [simplification-15] new conflict interval 61875
c [simplification-15] penalized conflict interval 61875 = 1 * 61875
c [simplification-15] hard conflict limit 316244 (soft 285307 + delta 30937)
c [simplification-15] new conflict limit 285307 (hard 316244)
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 -  505.9   89828  1805855    229830   32838  71163 100896   18   230   97   8%    861  -35   15   20   71%
c -  527.1   89828  1805854    267008   31652  71380 101047   31   936   96   3%    932  581   32   21  151%
c 
c [simplification-16] limit 285307 conflicts (hard 316244) hit after 286088 conflicts
c [quatres-12] found 25460 quaternary clauses 20% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-2] added 19 single-self-subsuming ternary resolvents
c [quatres-12-2] added 107 quaternary resolvents
c [ternres-12] limit 47283402 with penalty 0 = 0 + 0
c [ternres-12] 60 schedulable variables 0%
c [ternres-12] 1325 ternary resolvents (2 bin, 1323 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-33] removed 12 variables
c [treelook-4] limit 4728340 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 148232 literals 83%
c [treelook-4] scheduling used 4196546 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 4728340 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 4971289 steps
c [treelook-4] 148219 literals remain 83%
c [treelook-4] 55329 variables remain to probed next time 62%
c [treelook-4] removed 0 variables, found 37 hbrs
c [unhide-16] limit 1182085 with penalty 3 = 0 + 3
c [unhide-16-16] 1110 units, 25 failed, 6792 tauts, 0 hbrs, 58521 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 3 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 88489 variables 100%
c [block-9] limit of 118208507 steps penalty 2 = 2 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 46297 blocked clauses
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 87620 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14] incomplete 450 not tried 1% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 2951 = 3% variables out of 87620 scheduled
c [bca-12] limit of 10000000 steps and 3462626 added (scaled 2)
c [bca-12] 128137 out of 169340 literals actually usable 76%
c [bca-12] added 3660 blocked clauses in 496939 steps
c [sort-queue-16] sorted 24160 enqueued variables after 286088 conflicts
c [score-dist-16] active 60509 (71%), one 0 (0%), zero 24160 (29%)
c [score-dist-16] max exp 520, different 14 (3%)
c [score-dist-16] median active exp 519, avg 518.8
c [simplification-16] removed 5159 variables 5.7% (84669 remain 40%)
c [simplification-16] removed 94022 irredundant clauses 5.2% (1711832 remain 47%)
c [simplification-16] maximum reduction of 6% = max (6%, 5%)
c [simplification-16] large reduction 6% >= 5% limit
c [simplification-16] next conflict interval 2860 = min (286088/100, 61875)
c [simplification-16] penalized conflict interval 2860 = 1 * 2860
c [simplification-16] hard conflict limit 298948 (soft 288948 + delta 10000)
c [simplification-16] new conflict limit 288948 (hard 298948)
c 
c [simplification-17] limit 288948 conflicts (hard 298948) hit after 288961 conflicts
c [quatres-13] found 24980 quaternary clauses 20% in total
c [quatres-13-2] added 17 single-self-subsuming ternary resolvents
c [quatres-13-2] added 31 quaternary resolvents
c [ternres-13] limit 47814447 with penalty 0 = 0 + 0
c [ternres-13] all 84669 free variables schedulable
c [ternres-13] 2097 ternary resolvents (2 bin, 2095 trn)
c [ternres-13] 79 variables remain 0% (84590 retained 100%)
c [decomp-35] removed 131 variables
c [basicprobe-4] limit 239072235 penalty 0 = 0 + 0
c [basicprobe-4-0] 70969 probes remain 85% after last round
c [basicprobe-4-0] 238 units = 238 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 615 variables, found 18124 hbrs
c [bate-2] eliminated 121 asymmetric tautologies during probing
c [unhide-17] limit 1195361 with penalty 3 = 0 + 3
c [unhide-17-17] 79 units, 3 failed, 14269 tauts, 0 hbrs, 43183 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 2 transitive binary clauses
c [elim-15] 444 variables 1% will be scheduled this time
c [elim-15] scheduled 444 variables 1%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15] incomplete 19 not tried 0% in round 1
c [elim-15] transition to [ all 0 rem 1 ] state
c [elim-15] eliminated 0 = 0% variables out of 444 scheduled
c [bca-13] limit of 10000000 steps and 3363986 added (scaled 2)
c [bca-13] 125254 out of 167684 literals actually usable 75%
c [bca-13] added 701 blocked clauses in 467644 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 71721670 penalty 1 = 1 + 0
c [sweep-11-1] 2866 pos 3.6% + 76732 neg 96.4% = 79598 sched 94.9% ret 4243
c [sweep-11-1] 71805411 steps 541 queries 1949.44 avg class size
c [sweep-11-1] 15545 decisions 499 SAT calls 105.31 avg env size
c [sweep-11-1] 63322 variables remain 76% (20519 retained 24%)
c [decomp-36] removed 1719 variables
c [sweep-11-1] removed 1719 vars (0 failed, 44 eqs, 81 impls)
c [sweep-11] removed 1719 vars in TOTAL (1 rounds, 540 queries)
c [sort-queue-17] sorted 23188 enqueued variables after 288961 conflicts
c [score-dist-17] active 58934 (72%), one 0 (0%), zero 23188 (28%)
c [score-dist-17] max exp 520, different 14 (3%)
c [score-dist-17] median active exp 519, avg 518.9
c [simplification-17] removed 2547 variables 3.0% (82122 remain 39%)
c [simplification-17] removed 57328 irredundant clauses 3.3% (1654504 remain 46%)
c [simplification-17] maximum reduction of 3% = max (3%, 3%)
c [simplification-17] geometric conflict interval increment 15468 = 61875 / 4
c [simplification-17] new conflict interval 77343
c [simplification-17] penalized conflict interval 77343 = 1 * 77343
c [simplification-17] hard conflict limit 404975 (soft 366304 + delta 38671)
c [simplification-17] new conflict limit 366304 (hard 404975)
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 -  606.2   82122  1654504    315424   28845  60022 71882   37  1047   90   4%    980  461   37   26  140%
c -  629.7   82122  1654504    358893   32173  60307 72052   33   799   90   4%   1001  181   33   27  120%
c 
c [simplification-18] limit 366304 conflicts (hard 404975) hit after 369154 conflicts
c [quatres-14] found 23870 quaternary clauses 20% in total
c [quatres-14-1] removed 4 duplicate quaternary clauses
c [quatres-14-2] added 59 single-self-subsuming ternary resolvents
c [quatres-14-2] added 45 quaternary resolvents
c [ternres-14] limit 57721053 with penalty 0 = 0 + 0
c [ternres-14] 70 schedulable variables 0%
c [ternres-14] 511 ternary resolvents (0 bin, 511 trn)
c [ternres-14] 1 variables remain 0% (82121 retained 100%)
c [decomp-37] removed 4 variables
c [unhide-18] limit 1443026 with penalty 3 = 0 + 3
c [unhide-18-18] 220 units, 22 failed, 2984 tauts, 0 hbrs, 49547 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 11 transitive binary clauses
c [transred-13] found 2 units
c [block-10] scheduling all variables this time
c [block-10] scheduled 80750 variables 100%
c [block-10] limit of 288605267 steps penalty 1 = 1 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 116964 blocked clauses
c [bca-14] limit of 10000000 steps and 3042022 added (scaled 2)
c [bca-14] 114284 out of 158988 literals actually usable 72%
c [bca-14] added 10311 blocked clauses in 429708 steps
c [sweep-12] limit 17316316 penalty 0 = 0 + 0
c [sweep-12-1] 2088 pos 3.5% + 57611 neg 96.5% = 59699 sched 75.1% ret 19794
c [sweep-12-1] 17334459 steps 131 queries 3064.92 avg class size
c [sweep-12-1] 3071 decisions 121 SAT calls 76.50 avg env size
c [sweep-12-1] 58298 variables remain 73% (21195 retained 27%)
c [decomp-38] removed 20 variables
c [sweep-12-1] removed 20 vars (0 failed, 10 eqs, 24 impls)
c [sweep-12] 20 < 1/1000 * 79493 = 79 considered unsuccessful
c [sweep-12] removed 20 vars in TOTAL (1 rounds, 130 queries)
c [sort-queue-18] sorted 15566 enqueued variables after 369154 conflicts
c [score-dist-18] active 63907 (80%), one 0 (0%), zero 15566 (20%)
c [score-dist-18] max exp 520, different 13 (2%)
c [score-dist-18] median active exp 520, avg 519.6
c [simplification-18] removed 2649 variables 3.2% (79473 remain 38%)
c [simplification-18] removed 154086 irredundant clauses 9.3% (1500418 remain 41%)
c [simplification-18] maximum reduction of 9% = max (3%, 9%)
c [simplification-18] large reduction 9% >= 5% limit
c [simplification-18] next conflict interval 3691 = min (369154/100, 77343)
c [simplification-18] penalized conflict interval 3691 = 1 * 3691
c [simplification-18] hard conflict limit 382845 (soft 372845 + delta 10000)
c [simplification-18] new conflict limit 372845 (hard 382845)
c 
c [simplification-19] limit 372845 conflicts (hard 382845) hit after 372845 conflicts
c [quatres-15] found 23180 quaternary clauses 21% in total
c [quatres-15-1] removed 4 duplicate quaternary clauses
c [quatres-15-2] added 5 single-self-subsuming ternary resolvents
c [quatres-15-2] added 34 quaternary resolvents
c [ternres-15] limit 58147165 with penalty 0 = 0 + 0
c [ternres-15] 1 schedulable variables 0%
c [ternres-15] 847 ternary resolvents (0 bin, 847 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 750192 based on 1500385 irredundant clauses
c [gauss-5] extracted 3 xors of average arity 3.0
c [gauss-5] connected 9 occurrences of 9 variables (average 1.0)
c [gauss-5] limit 750192 based on 1500385 irredundant clauses
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] 76598 schedulable variables 96%
c [simpleprobe-5] limit 50000000 penalty 2 = 2 + 0
c [decomp-40] removed 940 variables
c [simpleprobe-5] 54159 variables remain 69% (24374 retained 31%)
c [simpleprobe-5] removed 940 variables, found 26991 hbrs, 750 units
c [unhide-19] limit 2907358 with penalty 2 = 0 + 2
c [unhide-19-19] 3 units, 0 failed, 9383 tauts, 0 hbrs, 14601 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 11 transitive binary clauses
c [transred-14] found 1 units
c [block-11] scheduling all variables this time
c [block-11] scheduled 78529 variables 100%
c [block-11] limit of 581471654 steps penalty 0 = 0 + 0
c [block-11] fully completed
c [block-11] transition to [ all 0 rem 0 ] state
c [block-11] eliminated 28705 blocked clauses
c [cce-5] limit of 18170989 steps penalty 4 = 4 + 0
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 9086538 steps for small clauses
c [cce-5-1] scheduling 1308211 clauses = 1288157 binary + 20054 ternary
c [cce-5-1] tried to eliminate 132 small clauses 0%
c [cce-5-1] eliminated 6 binary clauses 0%
c [cce-5-1] eliminated 1 ternary clauses 0%
c [cce-5-1] eliminated 7 small clauses 0%
c [cce-5-1] eliminated 7 small clauses in 18170990 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 7 covered clauses in round 1
c [cce-5] eliminated 7 covered clauses in TOTAL during 1 rounds
c [cce-5] 7 < 1/100 * 1454220 = 14542 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 78454 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16] incomplete 1312 not tried 2% in round 1
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 4227 = 5% variables out of 78454 scheduled
c [bca-15] limit of 10000000 steps and 2890166 added (scaled 2)
c [bca-15] 104781 out of 148456 literals actually usable 71%
c [bca-15] added 1370 blocked clauses in 399442 steps
c [sort-queue-19] sorted 13051 enqueued variables after 372845 conflicts
c [score-dist-19] active 61176 (82%), one 0 (0%), zero 13051 (18%)
c [score-dist-19] max exp 520, different 13 (2%)
c [score-dist-19] median active exp 520, avg 519.6
c [simplification-19] removed 5246 variables 6.6% (74227 remain 35%)
c [simplification-19] removed 78484 irredundant clauses 5.2% (1421934 remain 39%)
c [simplification-19] maximum reduction of 7% = max (7%, 5%)
c [simplification-19] large reduction 7% >= 5% limit
c [simplification-19] next conflict interval 3728 = min (372845/100, 77343)
c [simplification-19] penalized conflict interval 3728 = 1 * 3728
c [simplification-19] hard conflict limit 386573 (soft 376573 + delta 10000)
c [simplification-19] new conflict limit 376573 (hard 386573)
c 
c [simplification-20] limit 376573 conflicts (hard 386573) hit after 376574 conflicts
c [quatres-16] found 22167 quaternary clauses 20% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 39 single-self-subsuming ternary resolvents
c [quatres-16-2] added 236 quaternary resolvents
c [ternres-16] limit 58437354 with penalty 0 = 0 + 0
c [ternres-16] all 74227 free variables schedulable
c [ternres-16] 2527 ternary resolvents (0 bin, 2527 trn)
c [ternres-16] 17 variables remain 0% (74210 retained 100%)
c [decomp-41] removed 5 variables
c [unhide-20] limit 2921867 with penalty 2 = 0 + 2
c [unhide-20-20] 421 units, 8 failed, 2338 tauts, 0 hbrs, 56323 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 12 transitive binary clauses
c [block-12] scheduling all variables this time
c [block-12] scheduled 73798 variables 100%
c [block-12] limit of 584373542 steps penalty 0 = 0 + 0
c [block-12] fully completed
c [block-12] transition to [ all 0 rem 0 ] state
c [block-12] eliminated 9852 blocked clauses
c [block-12] 9852 < 1/100 * 1421713 = 14217 considered unsuccessful
c [elim-17] 16 variables 0% will be scheduled this time
c [elim-17] scheduled 16 variables 0%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] no variable eliminated in round 1 in 548001325 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 0 = 0% variables out of 16 scheduled
c [bca-16] limit of 10000000 steps and 2858101 added (scaled 2)
c [bca-16] 103098 out of 147216 literals actually usable 70%
c [bca-16] added 1681 blocked clauses in 404990 steps
c [sweep-13] limit 8765603 penalty 1 = 1 + 0
c [sweep-13-1] 2019 pos 3.8% + 51812 neg 96.2% = 53831 sched 73.1% ret 19776
c [sweep-13-1] 8775691 steps 70 queries 6164.17 avg class size
c [sweep-13-1] 1768 decisions 67 SAT calls 75.93 avg env size
c [sweep-13-1] 53383 variables remain 73% (20223 retained 27%)
c [decomp-42] removed 10 variables
c [sweep-13-1] removed 10 vars (0 failed, 3 eqs, 3 impls)
c [sweep-13] 10 < 1/1000 * 73607 = 73 considered unsuccessful
c [sweep-13] removed 10 vars in TOTAL (1 rounds, 69 queries)
c [sort-queue-20] sorted 12739 enqueued variables after 376574 conflicts
c [score-dist-20] active 60858 (83%), one 0 (0%), zero 12739 (17%)
c [score-dist-20] max exp 520, different 13 (2%)
c [score-dist-20] median active exp 520, avg 519.6
c [simplification-20] removed 630 variables 0.8% (73597 remain 35%)
c [simplification-20] removed 16411 irredundant clauses 1.2% (1405523 remain 39%)
c [simplification-20] maximum reduction of 1% = max (1%, 1%)
c [simplification-20] geometric conflict interval increment 38671 = 77343 / 2
c [simplification-20] new conflict interval 116014
c [simplification-20] penalized conflict interval 116014 = 1 * 116014
c [simplification-20] hard conflict limit 550595 (soft 492588 + delta 58007)
c [simplification-20] new conflict limit 492588 (hard 550595)
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 -  685.9   73597  1405523    405938   33372  60096 84546   27   326   86   8%   1013 -179   39   27  142%
c -  701.7   73597  1405523    446247   34522  60305 84668   24   119   87  20%   1018 -365   19   28   69%
c -  716.9   73597  1405523    488274   36413  60446 84789   27   502   87   5%   1021  132   29   24  118%
c 
c [simplification-21] limit 492588 conflicts (hard 550595) hit after 492589 conflicts
c [quatres-17] found 22589 quaternary clauses 21% in total
c [quatres-17-2] added 8 single-self-subsuming ternary resolvents
c [quatres-17-2] added 86 quaternary resolvents
c [ternres-17] limit 67106676 with penalty 0 = 0 + 0
c [ternres-17] 17 schedulable variables 0%
c [ternres-17] 907 ternary resolvents (0 bin, 907 trn)
c [ternres-17] 7 variables remain 0% (73590 retained 100%)
c [card-6] limit 2097083 penalty 4 = 4 + 0
c [card-6] found 43 at-most-one constraints of average size 3.2
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2097083 for elimination
c [card-6] 43 out of 43 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [treelook-5] limit 3355333 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 120611 literals 82%
c [treelook-5] scheduling used 3314504 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3355333 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 3692849 steps
c [treelook-5] 120597 literals remain 82%
c [treelook-5] 44426 variables remain to probed next time 60%
c [treelook-5] removed 0 variables, found 246 hbrs
c [unhide-21] limit 3355333 with penalty 2 = 0 + 2
c [unhide-21-21] 0 units, 2 failed, 6754 tauts, 0 hbrs, 20589 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 12 transitive binary clauses
c [bca-17] limit of 10000000 steps and 2846753 added (scaled 2)
c [bca-17] 105047 out of 147192 literals actually usable 71%
c [bca-17] added 3162 blocked clauses in 424252 steps
c [sort-queue-21] sorted 11232 enqueued variables after 492589 conflicts
c [score-dist-21] active 62363 (85%), one 0 (0%), zero 11232 (15%)
c [score-dist-21] max exp 520, different 13 (2%)
c [score-dist-21] median active exp 520, avg 519.7
c [simplification-21] removed 2 variables 0.0% (73595 remain 35%)
c [simplification-21] removed 6058 irredundant clauses 0.4% (1399465 remain 39%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 116014
c [simplification-21] new conflict interval 232028
c [simplification-21] penalized conflict interval 232028 = 1 * 232028
c [simplification-21] hard conflict limit 840631 (soft 724617 + delta 116014)
c [simplification-21] new conflict limit 724617 (hard 840631)
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  732.2   73594  1399465    508249   54226  61182 87412   26   788   94   3%   1022  312    6   26   23%
c -  737.9   72193  1399465    530308   37052  61226 87450   21    59   87  36%  -3781 -385   18   26   72%
c -  749.3   72193  1399465    574323   39823  61292 87521   25   198   87  13%  -1431 -119   23   24  100%
c -  759.5   72193  1399465    616484   41343  61329 87566   19    75   88  25%   -266 -132   14   22   66%
c i  766.2   72192  1399465    639373   61157  61383 87612   22   515   96   4%    114  340   28   20  139%
c -  778.0   72151  1399465    658779   40458  61467 87710   38  1002   87   4%  -1201  627   34   25  140%
c -  802.1   72151  1399465    704837   41741  61780 87865   38  1040   88   4%    -78  441   43   30  143%
c 
c [simplification-22] limit 724617 conflicts (hard 840631) hit after 738076 conflicts
c [quatres-18] found 19860 quaternary clauses 22% in total
c [quatres-18-1] added 1 double-self-subsuming ternary resolvents
c [quatres-18-2] added 39 single-self-subsuming ternary resolvents
c [quatres-18-2] added 74 quaternary resolvents
c [ternres-18] limit 84437868 with penalty 0 = 0 + 0
c [ternres-18] 7 schedulable variables 0%
c [ternres-18] 166 ternary resolvents (0 bin, 166 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-45] removed 1465 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 44514 probes remain 66% after last round
c [basicprobe-5-0] 4066 units = 2522 failed (62%) + 1544 lifted (38%)
c [basicprobe-5-0] removed 4257 variables, found 40267 hbrs
c [bate-3] eliminated 184 asymmetric tautologies during probing
c [unhide-22] limit 4221893 with penalty 2 = 0 + 2
c [unhide-22-22] 45 units, 2 failed, 6845 tauts, 0 hbrs, 132874 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 19 transitive binary clauses
c [transred-17] found 2 units
c [block-13] scheduling all variables this time
c [block-13] scheduled 67818 variables 100%
c [block-13] limit of 400000000 steps penalty 1 = 1 + 0
c [block-13] fully completed
c [block-13] transition to [ all 0 rem 0 ] state
c [block-13] eliminated 30520 blocked clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 67594 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 3761 variables 6% in round 1 in 1504259364 steps
c [elim-18-1] backward subsumption/strengthening limit 1504259300
c [elim-18-1-1] backward checking 26504 touched variables 39%
c [elim-18-1-1] incomplete backward checking 26637 remain 101%
c [elim-18-1] subsumed 0 and strengthened 925 clauses in 1504259549 steps
c [elim-18-1] rescheduled 2161 variables 3% by backward subsumption
c [elim-18-2] eliminated 5 variables 0% in round 2 in 593671584 steps
c [elim-18-2] backward subsumption/strengthening limit 593671500
c [elim-18-2-1] backward checking 26655 touched variables 39%
c [elim-18-2-1] incomplete backward checking 26655 remain 100%
c [elim-18-2] subsumed 7 and strengthened 28 clauses in 593685392 steps
c [elim-18-2] rescheduled 241 variables 0% by backward subsumption
c [elim-18-3] eliminated 9 variables 0% in round 3 in 75216412 steps
c [elim-18-3] backward subsumption/strengthening limit 75216400
c [elim-18-3-1] backward checking 26656 touched variables 39%
c [elim-18-3-1] incomplete backward checking 26655 remain 100%
c [elim-18-3] subsumed 0 and strengthened 4 clauses in 75219766 steps
c [elim-18] incomplete 16 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 3775 = 6% variables out of 67594 scheduled
c [bca-18] limit of 10000000 steps and 2463276 added (scaled 2)
c [bca-18] 81042 out of 127640 literals actually usable 63%
c [bca-18] added 7299 blocked clauses in 305284 steps
c [sort-queue-22] sorted 4238 enqueued variables after 738076 conflicts
c [score-dist-22] active 59581 (93%), one 0 (0%), zero 4238 (7%)
c [score-dist-22] max exp 521, different 13 (2%)
c [score-dist-22] median active exp 521, avg 520.8
c [simplification-22] removed 8332 variables 11.5% (63819 remain 30%)
c [simplification-22] removed 192529 irredundant clauses 13.8% (1206936 remain 33%)
c [simplification-22] maximum reduction of 14% = max (12%, 14%)
c [simplification-22] large reduction 14% >= 5% limit
c [simplification-22] next conflict interval 7380 = min (738076/100, 232028)
c [simplification-22] penalized conflict interval 7380 = 1 * 7380
c [simplification-22] hard conflict limit 755456 (soft 745456 + delta 10000)
c [simplification-22] new conflict limit 745456 (hard 755456)
c 
c [simplification-23] limit 745456 conflicts (hard 755456) hit after 745456 conflicts
c [quatres-19] found 23896 quaternary clauses 26% in total
c [quatres-19-1] removed 13 duplicate quaternary clauses
c [quatres-19-2] added 55 single-self-subsuming ternary resolvents
c [quatres-19-2] added 605 quaternary resolvents
c [ternres-19] limit 85043245 with penalty 0 = 0 + 0
c [ternres-19] all 63819 free variables schedulable
c [ternres-19] 6889 ternary resolvents (2 bin, 6887 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-46] removed 60 variables
c [simpleprobe-6] 43606 schedulable variables 68%
c [simpleprobe-6] limit 100000000 penalty 1 = 1 + 0
c [decomp-47] removed 32 variables
c [simpleprobe-6] 43244 variables remain 68% (20483 retained 32%)
c [simpleprobe-6] removed 32 variables, found 8121 hbrs, 22 units
c [unhide-23] limit 4252162 with penalty 2 = 0 + 2
c [unhide-23-24] 1 units, 2 failed, 8097 tauts, 0 hbrs, 70932 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 35 transitive binary clauses
c [transred-18] found 1 units
c [block-14] scheduling all variables this time
c [block-14] scheduled 63723 variables 100%
c [block-14] limit of 800000000 steps penalty 0 = 0 + 0
c [block-14] fully completed
c [block-14] transition to [ all 0 rem 0 ] state
c [block-14] eliminated 36093 blocked clauses
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 63473 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19] incomplete 83 not tried 0% in round 1
c [elim-19] transition to [ all 1 rem 1 ] state
c [elim-19] eliminated 2036 = 3% variables out of 63473 scheduled
c [bca-19] limit of 10000000 steps and 2347308 added (scaled 2)
c [bca-19] 74951 out of 122876 literals actually usable 61%
c [bca-19] added 4079 blocked clauses in 299452 steps
c [sweep-14] limit 6378243 penalty 2 = 2 + 0
c [sweep-14-1] 1495 pos 3.4% + 41912 neg 96.6% = 43407 sched 70.7% ret 18030
c [sweep-14-1] 6466578 steps 67 queries 3888.84 avg class size
c [sweep-14-1] 2474 decisions 63 SAT calls 94.81 avg env size
c [sweep-14-1] 42745 variables remain 70% (18692 retained 30%)
c [decomp-48] removed 15 variables
c [sweep-14-1] removed 15 vars (0 failed, 3 eqs, 7 impls)
c [sweep-14] 15 < 1/1000 * 61437 = 61 considered unsuccessful
c [sweep-14] removed 15 vars in TOTAL (1 rounds, 66 queries)
c [sort-queue-23] sorted 3671 enqueued variables after 745456 conflicts
c [score-dist-23] active 57751 (94%), one 0 (0%), zero 3671 (6%)
c [score-dist-23] max exp 521, different 12 (2%)
c [score-dist-23] median active exp 521, avg 520.8
c [simplification-23] removed 2397 variables 3.8% (61422 remain 29%)
c [simplification-23] removed 59920 irredundant clauses 5.0% (1147016 remain 32%)
c [simplification-23] maximum reduction of 5% = max (4%, 5%)
c [simplification-23] large reduction 5% >= 5% limit
c [simplification-23] next conflict interval 7454 = min (745456/100, 232028)
c [simplification-23] penalized conflict interval 7454 = 1 * 7454
c [simplification-23] hard conflict limit 762910 (soft 752910 + delta 10000)
c [simplification-23] new conflict limit 752910 (hard 762910)
c 
c [simplification-24] limit 752910 conflicts (hard 762910) hit after 752910 conflicts
c [quatres-20] found 24294 quaternary clauses 26% in total
c [quatres-20-1] removed 16 duplicate quaternary clauses
c [quatres-20-2] added 36 single-self-subsuming ternary resolvents
c [quatres-20-2] added 346 quaternary resolvents
c [ternres-20] limit 85727974 with penalty 0 = 0 + 0
c [ternres-20] all 61422 free variables schedulable
c [ternres-20] 5546 ternary resolvents (5 bin, 5541 trn)
c [ternres-20] 2 variables remain 0% (61420 retained 100%)
c [unhide-24] limit 4286398 with penalty 2 = 0 + 2
c [unhide-24-26] 625 units, 20 failed, 9813 tauts, 0 hbrs, 75868 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 28 transitive binary clauses
c [transred-19] found 2 units
c [block-15] scheduling all variables this time
c [block-15] scheduled 60745 variables 100%
c [block-15] limit of 800000000 steps penalty 0 = 0 + 0
c [block-15] fully completed
c [block-15] transition to [ all 0 rem 0 ] state
c [block-15] eliminated 30543 blocked clauses
c [elim-20] 81 variables 0% will be scheduled this time
c [elim-20] scheduled 81 variables 0%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] no variable eliminated in round 1 in 593910436 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 0 = 0% variables out of 81 scheduled
c [bca-20] limit of 10000000 steps and 2242351 added (scaled 2)
c [bca-20] 72143 out of 121304 literals actually usable 59%
c [bca-20] added 3530 blocked clauses in 289800 steps
c [sort-queue-24] sorted 3465 enqueued variables after 752910 conflicts
c [score-dist-24] active 57186 (94%), one 0 (0%), zero 3465 (6%)
c [score-dist-24] max exp 521, different 12 (2%)
c [score-dist-24] median active exp 521, avg 520.8
c [simplification-24] removed 771 variables 1.3% (60651 remain 29%)
c [simplification-24] removed 53387 irredundant clauses 4.7% (1093629 remain 30%)
c [simplification-24] maximum reduction of 5% = max (1%, 5%)
c [simplification-24] large reduction 5% >= 5% limit
c [simplification-24] next conflict interval 7529 = min (752910/100, 232028)
c [simplification-24] penalized conflict interval 7529 = 1 * 7529
c [simplification-24] hard conflict limit 770439 (soft 760439 + delta 10000)
c [simplification-24] new conflict limit 760439 (hard 770439)
c 
c [simplification-25] limit 760439 conflicts (hard 770439) hit after 760440 conflicts
c [quatres-21] found 22532 quaternary clauses 26% in total
c [quatres-21-1] removed 1 duplicate quaternary clauses
c [quatres-21-2] added 9 single-self-subsuming ternary resolvents
c [quatres-21-2] added 468 quaternary resolvents
c [ternres-21] limit 86211599 with penalty 0 = 0 + 0
c [ternres-21] 2 schedulable variables 0%
c [ternres-21] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 1077644 penalty 4 = 4 + 0
c [gauss-6] extracted 0 xors of average arity 0.0
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-50] removed 20 variables
c [unhide-25] limit 4310579 with penalty 2 = 0 + 2
c [unhide-25-28] 107 units, 5 failed, 6193 tauts, 0 hbrs, 38430 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 4 transitive binary clauses
c [transred-20] found 1 units
c [block-16] scheduling all variables this time
c [block-16] scheduled 60519 variables 100%
c [block-16] limit of 800000000 steps penalty 0 = 0 + 0
c [block-16] fully completed
c [block-16] transition to [ all 0 rem 0 ] state
c [block-16] eliminated 1920 blocked clauses
c [block-16] 1920 < 1/100 * 1091701 = 10917 considered unsuccessful
c [cce-6] limit of 26941124 steps penalty 4 = 4 + 0
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] allowing another 13470639 steps for small clauses
c [cce-6-1] scheduling 972302 clauses = 952258 binary + 20044 ternary
c [cce-6-1] tried to eliminate 381 small clauses 0%
c [cce-6-1] eliminated 26 binary clauses 0%
c [cce-6-1] eliminated 26 small clauses 0%
c [cce-6-1] eliminated 26 small clauses in 26941434 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 26 covered clauses in round 1
c [cce-6] eliminated 26 covered clauses in TOTAL during 1 rounds
c [cce-6] 26 < 1/100 * 1088895 = 10888 considered unsuccessful
c [bca-21] limit of 10000000 steps and 2234596 added (scaled 2)
c [bca-21] 70176 out of 121036 literals actually usable 58%
c [bca-21] added 2591 blocked clauses in 286133 steps
c [sort-queue-25] sorted 2959 enqueued variables after 760440 conflicts
c [score-dist-25] active 57558 (95%), one 0 (0%), zero 2959 (5%)
c [score-dist-25] max exp 521, different 12 (2%)
c [score-dist-25] median active exp 521, avg 520.8
c [simplification-25] removed 134 variables 0.2% (60517 remain 29%)
c [simplification-25] removed 4760 irredundant clauses 0.4% (1088869 remain 30%)
c [simplification-25] maximum reduction of 0% = max (0%, 0%)
c [simplification-25] full geometric conflict interval increment 232028
c [simplification-25] new conflict interval 464056
c [simplification-25] penalized conflict interval 464056 = 1 * 464056
c [simplification-25] hard conflict limit 1456524 (soft 1224496 + delta 232028)
c [simplification-25] new conflict limit 1224496 (hard 1456524)
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 -  954.3   60517  1088869    768770   38774  59614 110349   39   762   80   5%    609  146   33   30  112%
c -  969.9   60517  1088869    818578   42826  59967 110484   28   160   81  17%    830 -384   26   30   88%
c -  978.7   60517  1088869    864271   46073  59998 110500   17    26   81  65%    927 -275   16   24   67%
c -  991.8   60517  1088869    907541   44395  60151 110601   38   850   81   4%    974  538   45   24  182%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 307 basic ate = 262 trn 85% + 45 lrg 15% in 3 updates
c bcas: 21 count, 115308 added (26229 skipped), 11012092 steps
c bkwd: tried 993353 clauses, 1984393 lits, 2.00 lits/clause
c bkwd: checked 6188550832 occs, 6229.96 occs/clause, 3118.61 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 95 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 2229 large (0% self)
c blkd: 16 bces, 896407 removed, 145353669 resolutions, 417120006 steps
c blkd: 53371 blocking literals 13%, 9708 pure
c bump: 894133 bumped seen, 95282260 lits 106.6 on average
c card: 6 count, 0 units, 0 am1, 35941239 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1580 subsumed
c card: 106 at-most-one constraints found, average size 3.16
c card: 106 at-most-one constraints used 100%, average size 3.16
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: 6 cces, 284 eliminated, 283 ate 100%, 1 abce 0%
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: 14182638 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 146 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 50 decompositions, 4751 equivalent 2%
c deco: 263 decision-only clauses 0%, 44% reduction
c decs: 49205449 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 20 elims, 93794 eliminated 45%, 1322 pure 1%
c elms: 28 rounds, 1.4 rounds/bve
c elms: 32337 small 34%, 50427 large 54%
c elms: 49919 tried small, 32337 succeeded 65%, 17582 failed 35%
c elms: 112017 subsumed, 678779 strengthened, 106309 blocked
c elms: 46578876 copies, 77605228 resolutions, 1048666 ipos
c elms: 473450245 subchks, 572992830 strchks
c gaus: 6 extractions, 5 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13292948 steps, 6646474 extr 50%, 20 elim 0%
c glue: 25.8 orig avg, 25.8 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 191350 = 65719 simple 34% + 125437 trn 66% + 194 lrg 0%, 7005 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 894133 clauses, 57.7 length
c lrnd: 51588786 lits = 77557755 orig - 25968969 removed 33%
c lrnd: 388707 uips 43%, 337211 flips 38%
c mins: 878832 mins 98%, 2196 bin 0%, 12729 size 1%
c mins: 72698196 poisoned searches, 14362858 hits, 20% hit rate
c mins: 134578318 used twice searches, 13490313 hits, 10% hit rate
c move: moved 839408, 821724 bin 98%, 17684 trn 2%
c otfs: 26689 driving 28%, 68530 restarting 72%
c otfs: str 95219, 94436 red 99%, 783 irr 1%
c otfs: str 95219, 0 bin 0%, 487 trn 1%, 94732 lrg 99%
c otfs: sub 1029, 996 red 97%, 33 irr 3%
c otfs: sub 1029, 0 bin 0%, 3 trn 0%, 1026 lrg 100%
c phas: 1 computed, 208401 set, 0 pos (0%), 208401 neg (100%)
c prbs: 5 basic, 35002 probed, 2938 failed, 1544 lifted
c prbs: 6 simple, 447848 probed, 772 failed, 33 eqs
c prbs: 5 treelook, 38 probed, 3 failed, 0 lifted
c prom: 110962 locked 5% out of 2245925 tried
c prps: 2050715914 props, 40 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 21 count, 11710 quat, 1914 self1, 3 self2, 484 dup
c queu: 25 sorted, 49205450 next (115304 steps 0.00)
c queu: 96769559 enq (2567381362 steps 26.53), 95282260 deq 98%
c redc: 11550 clauses 25%, 45361 tried 5%, 104 sat 0%
c redc: 26129 lits 5%, 512098 tried 1%, 104 sat 0%
c redc: 1034 times jump level reduced, 89.3 levels on average
c reds: 20 count, 46025.5 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595085 collected 84%, 113390 retired 16%
c rmbd: 60869 removed, 40706 red 67%
c rsts: 16356 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: 25 count, 24 confs 96%, 0 vars 0%
c simp: 0 its 0%, 1 bin 4%, 0 trns 0%
c subl: 894133 count (1060761 tried 1.2), 75224 sub out of 886097 (8.5%)
c swps: 14 count, 14 rounds, 1216 queries (86.9/round)
c swps: 1123 sat calls, 13 unsat (0.3% success rate)
c swps: 36487 decisions 32.5, 312 conflicts 0.3
c swps; 4767.9 avg class size, 154.4 avg environment size
c swps: 2 failed, 204 impls, 103 equivs
c swp0: 403 type 0 queries, 74 unsat (18.4%), 374 sat (92.8%)
c swp1: 813 type 1 queries, 227 unsat (27.9%), 739 sat (90.9%)
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: 100199658 calls to obtain time
c tops: 50662 fixed 24%, 5 its, 184102.00 confs/it
c trds: 20 transitive reductions, 180 removed, 14 failed
c trds: 3647 nodes, 29101 edges, 42661260 steps
c trim: 814537 words, 3.1 MB
c trnr: 21 count, 48 bin, 119366 trn, 798127629 steps
c unhd: 25 count, 28 rounds, 145898187 steps
c unhd: 2114 non-trivial sccs of average size 2.0
c unhd: 19027 units, 19026 bin, 1 trn, 0 lrg
c unhd: 237 failed, 224 stamp, 0 lits, 5 bin, 6 trn, 0 lrg
c unhd: 221920 tauts, 4530 bin 2%, 25617 trn 12%, 31321 lrg 14%
c unhd: 221920 tauts, 160452 stamp 72%, 55320 red 25%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1320339 str, 19026 bin 1%, 20897 trn 2%, 1280416 lrg 97%, 880061 red 67%
c vars: 60517 remaining 29% and 149207 removed 71% out of 209724
c vars: 50662 fixed 24%, 93794 eliminated 45%, 4751 equivalent 2%
c vsts: 10239259193 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 4.9 search visits per propagation, 10377.2 per conflict
c wchs: 1266793070 pushed, 143432113 enlarged, 221 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         897807        595085        113390      29765312       8558790        584861
c 
c  0 0         40638   5      2741   0         0   0  13286523  45   2121402  25     43631   7     0.7
c  1 5         15258   2      4797   1      4147   4   2699358   9    644383   8     18637   3     0.3
c  2 6         62512   7     30668   5     11434  10   4574931  15<  1552919  18<    72367  12     1.3
c  3 9        155401  17    104412  18     16462  15   4174038  14   1847536  22    149369  26     3.2
c  4 14       203529  23    158545  27     16979  15   2508615   8   1225065  14    149747  26<    4.4
c  5 21       154371  17<   115398  19<    17715  16<  1254341   4    598278   7     79438  14     3.0
c  6 30       106504  12     74616  13     15875  14    644989   2    301349   4     38267   7     3.0
c  7 41        70418   8     47127   8     12528  11    344079   1    141701   2     18150   3     2.1
c  8 54        45463   5     29689   5      8834   8    162860   1     71360   1      8426   1     1.8
c  9 69        24357   3     15558   3      5075   4     67217   0     31476   0      3907   1     1.5
c 10 86        17396   2     10438   2      3838   3     43020   0     21372   0      2656   0     1.5
c 11 126        1881   0      1050   0       486   0      5055   0      1824   0       228   0     0.2
c 12 230          79   0        46   0        17   0       286   0       125   0        38   0     0.0
c 
c avg                  4.6           4.8           5.1           1.7           2.5           3.6
c std                  2.2           1.9           2.3           1.9           2.0           1.8
c 
c  333.764  33% elim
c   68.566   7% block
c   51.036   5% bump
c   36.017   4% probe
c   33.316   3% decide
c   28.101   3% unhide
c   17.607   2% quatres
c   16.283   2% sweep
c    9.563   1% bca
c 
c   15.130 < 1% rest (below)
c 
c    6.458   1% cce
c    4.990   0% ternres
c    2.278   0% gauss
c    1.168   0% transred
c    0.236   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    7.107   1% preprocessing     1%
c  538.682  54% inprocessing     99%
c ==================================
c  545.788  55% simplifying
c  452.153  45% search
c ==================================
c  997.946 100% all
c 
c        920510 conflicts,         922.4 confs/sec
c          5115 ternaries,         180.0 confs/ternary
c          2774 binaries,          331.8 confs/binary
c             5 iterations,     184102.0 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  46025.5 confs/reduction
c         16356 restarts,           16.4 rests/sec,     56.3 confs/restart
c      49205449 decisions,       49306.7 decis/sec,     53.5 decis/conflict
c    2050715914 propagations,  2054937.3 props/sec,     41.7 props/decision
c 
c 997.9 seconds, 266.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
