c launch: /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c host: atom08
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/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c no embedded options
c found 'p cnf 52444 217642' header
c read 52444 variables, 217642 clauses, 547043 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=1
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 50629 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] INC (--score=1)
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   50629   210196         0       0      0     0    0     0   10   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 2338 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2338 out of 2338 constraints (100%) meet size limits
c [card-1] found 9 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 16385 variables
c [simpleprobe-1] all 36059 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 5612 variables
c [simpleprobe-1] 130 variables remain 0% (30317 retained 100%)
c [simpleprobe-1] removed 5612 variables, found 35460 hbrs, 747 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 9 units, 7 failed, 349 tauts, 0 hbrs, 644 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 30420 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 18857 variables 62% in round 1 in 12327619 steps
c [elim-1-1] backward subsumption/strengthening limit 7672381
c [elim-1-1-1] backward checking 21884 touched variables 72%
c [elim-1-1-1] incomplete backward checking 21619 remain 99%
c [elim-1-1] subsumed 5 and strengthened 111 clauses in 7675938 steps
c [elim-1] incomplete 385 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 18859 = 62% variables out of 30420 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 75533 negative 93.8% of 80551 except 5018 6.2%
c [phase-count-1] 69933 positive 86.8% of 80551 except 10618 13.2%
c [phase-count-1] less non-negative clauses 5018 than limit 8000 (10.0%)
c [phase-count-1] non-pos/non-neg = 10618/5018 = 2.12 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 11561 negative 100%
c [sort-queue-1] sorted 11561 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 11561 (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 34588 variables 74.9% (11561 remain 23%)
c [simplification-1] removed 129645 irredundant clauses 61.7% (80551 remain 38%)
c [simplification-1] maximum reduction of 75% = max (75%, 62%)
c [simplification-1] large reduction 75% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 11 variables
c [simpleprobe-2] 40 schedulable variables 0%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 80 variables
c [simpleprobe-2] 118 variables remain 1% (11352 retained 99%)
c [simpleprobe-2] removed 80 variables, found 68 hbrs, 9 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 22940 literals 100%
c [treelook-1] scheduling used 263183 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300143 steps
c [treelook-1] 22859 literals remain 100%
c [treelook-1] 11470 variables remain to probed next time 100%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 450 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6843 probes remain 60% after last round
c [basicprobe-1-0] 55 units = 33 failed (60%) + 22 lifted (40%)
c [basicprobe-1-0] removed 85 variables, found 1563 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 4 units, 9 failed, 386 tauts, 0 hbrs, 5764 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 11368 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 286 variables 3% in round 1 in 14354156 steps
c [elim-2-1] backward subsumption/strengthening limit 5645844
c [elim-2-1-1] backward checking 3186 touched variables 28%
c [elim-2-1-1] incomplete backward checking 3101 remain 97%
c [elim-2-1] subsumed 5 and strengthened 10 clauses in 5646943 steps
c [elim-2] incomplete 45 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 286 = 3% variables out of 11368 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 72214 negative 93.5% of 77201 except 4987 6.5%
c [phase-count-2] 67011 positive 86.8% of 77201 except 10190 13.2%
c [phase-count-2] less non-negative clauses 4987 than limit 7700 (10.0%)
c [phase-count-2] non-pos/non-neg = 10190/4987 = 2.04 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 127 negative 100%
c [sort-queue-2] sorted 6248 enqueued variables after 1000 conflicts
c [score-dist-2] active 4834 (44%), one 0 (0%), zero 6248 (56%)
c [score-dist-2] max exp 509, different 9 (2%)
c [score-dist-2] median active exp 504, avg 504.2
c [simplification-2] removed 479 variables 4.1% (11082 remain 22%)
c [simplification-2] removed 3350 irredundant clauses 4.2% (77201 remain 37%)
c [simplification-2] maximum reduction of 4% = max (4%, 4%)
c [simplification-2] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-2] new conflict interval 4000
c [simplification-2] penalized conflict interval 4000 = 1 * 4000
c [simplification-2] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-2] new conflict limit 5000 (hard 15000)
c 
c [simplification-3] limit 5000 conflicts (hard 15000) hit after 5005 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 723 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 723 out of 723 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 3 at-most-one constraints, 1 used 33%
c [card-2] exported 1 binary clauses, 1.0 per/constraint
c [decomp-6] removed 17 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 22130 literals 100%
c [treelook-2] scheduling used 263130 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300162 steps
c [treelook-2] 21831 literals remain 99%
c [treelook-2] 11062 variables remain to probed next time 100%
c [decomp-7] removed 23 variables
c [treelook-2] removed 26 variables, found 1151 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 4 units, 10 failed, 397 tauts, 0 hbrs, 6156 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 11027 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 134 variables 1% in round 1 in 13791750 steps
c [elim-3-1] backward subsumption/strengthening limit 6208250
c [elim-3-1-1] backward checking 910 touched variables 8%
c [elim-3-1-1] incomplete backward checking 850 remain 93%
c [elim-3-1] subsumed 0 and strengthened 24 clauses in 6208897 steps
c [elim-3] incomplete 107 not tried 1% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 134 = 1% variables out of 11027 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 71023 negative 93.6% of 75910 except 4887 6.4%
c [phase-count-3] 66023 positive 87.0% of 75910 except 9887 13.0%
c [phase-count-3] less non-negative clauses 4887 than limit 7500 (10.0%)
c [phase-count-3] non-pos/non-neg = 9887/4887 = 2.02 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 102 negative 100%
c [sort-queue-3] sorted 4224 enqueued variables after 5005 conflicts
c [score-dist-3] active 6669 (61%), one 0 (0%), zero 4224 (39%)
c [score-dist-3] max exp 513, different 13 (3%)
c [score-dist-3] median active exp 507, avg 506.5
c [simplification-3] removed 189 variables 1.7% (10893 remain 22%)
c [simplification-3] removed 1291 irredundant clauses 1.7% (75910 remain 36%)
c [simplification-3] maximum reduction of 2% = max (2%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 10666
c [simplification-3] penalized conflict interval 10666 = 1 * 10666
c [simplification-3] hard conflict limit 25671 (soft 15671 + delta 10000)
c [simplification-3] new conflict limit 15671 (hard 25671)
c 
c [simplification-4] limit 15671 conflicts (hard 25671) hit after 15671 conflicts
c [decomp-8] removed 9 variables
c [basicprobe-2] limit 5894691 penalty 0 = 0 + 0
c [basicprobe-2-0] 1307 probes remain 12% after last round
c [basicprobe-2-0] 45 units = 45 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 55 variables, found 5448 hbrs
c [unhide-4] limit 235787 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 537 tauts, 0 hbrs, 96029 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 10829 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 471575280 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 80 variables 1% in round 1 in 13550711 steps
c [elim-4-1] backward subsumption/strengthening limit 13550700
c [elim-4-1-1] backward checking 654 touched variables 6%
c [elim-4-1-1] incomplete backward checking 616 remain 94%
c [elim-4-1] subsumed 0 and strengthened 16 clauses in 13551553 steps
c [elim-4-1] rescheduled 45 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 40532 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 80 = 1% variables out of 10829 scheduled
c [elim-4] 80 < 1/100 * 10829 = 108 considered unsuccessful
c [phase-count-4] 70065 negative 93.5% of 74950 except 4885 6.5%
c [phase-count-4] 65098 positive 86.9% of 74950 except 9852 13.1%
c [phase-count-4] less non-negative clauses 4885 than limit 7400 (10.0%)
c [phase-count-4] non-pos/non-neg = 9852/4885 = 2.02 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 88 negative 100%
c [sort-queue-4] sorted 3641 enqueued variables after 15671 conflicts
c [score-dist-4] active 7108 (66%), one 0 (0%), zero 3641 (34%)
c [score-dist-4] max exp 515, different 15 (3%)
c [score-dist-4] median active exp 508, avg 508.1
c [simplification-4] removed 144 variables 1.3% (10749 remain 21%)
c [simplification-4] removed 960 irredundant clauses 1.3% (74950 remain 36%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 20666
c [simplification-4] penalized conflict interval 20666 = 1 * 20666
c [simplification-4] hard conflict limit 46670 (soft 36337 + delta 10333)
c [simplification-4] new conflict limit 36337 (hard 46670)
c 
c [simplification-5] limit 36337 conflicts (hard 46670) hit after 36337 conflicts
c [quatres-1] found 7683 quaternary clauses 30% in total
c [quatres-1-2] added 35 single-self-subsuming ternary resolvents
c [quatres-1-2] added 470 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 10749 free variables schedulable
c [ternres-1] 4133 ternary resolvents (258 bin, 3875 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4021 xors of average arity 2.9
c [gauss-1] connected 11633 occurrences of 574 variables (average 20.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 82 variables
c [simpleprobe-3] 79 schedulable variables 1%
c [simpleprobe-3] limit 14039601 penalty 0 = 0 + 0
c [decomp-10] removed 484 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 484 variables, found 3060 hbrs, 13 units
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 1692 transitive binary clauses
c [transred-1] found 3 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 10180 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 91 blocked clauses
c [block-1] 91 < 1/100 * 70772 = 707 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 26 clauses out of 120 (22%) of length 12
c [cce-1-1] eliminated 59 clauses out of 474 (12%) of length 11
c [cce-1-1] eliminated 5 clauses out of 274 (2%) of length 10
c [cce-1-1] eliminated 106 clauses out of 1024 (10%) of length 9
c [cce-1-1] eliminated 106 clauses out of 1485 (7%) of length 8
c [cce-1-1] eliminated 59 clauses out of 2837 (2%) of length 7
c [cce-1-1] eliminated 318 clauses out of 4183 (8%) of length 6
c [cce-1-1] eliminated 157 clauses out of 5531 (3%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 836 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 41736 clauses = 34918 binary + 6818 ternary
c [cce-1-1] tried to eliminate 5141 small clauses 12%
c [cce-1-1] eliminated 546 binary clauses 2%
c [cce-1-1] eliminated 79 ternary clauses 1%
c [cce-1-1] eliminated 625 small clauses 1%
c [cce-1-1] eliminated 625 small clauses in 30000016 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1461 covered clauses in round 1
c [cce-1] eliminated 1461 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 138894 added (scaled 2)
c [bca-1] 13143 out of 20362 literals actually usable 65%
c [bca-1] added 5 blocked clauses in 62826 steps
c [sweep-1] limit 1052970 penalty 0 = 0 + 0
c [sweep-1-1] 3363 pos 33.0% + 6817 neg 67.0% = 10180 sched 100.0% ret 0
c [sweep-1-1] 1058058 steps 81 queries 529.57 avg class size
c [sweep-1-1] 2164 decisions 77 SAT calls 105.91 avg env size
c [sweep-1-1] 9028 variables remain 89% (1152 retained 11%)
c [decomp-11] removed 7 variables
c [sweep-1-1] removed 7 vars (0 failed, 4 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 7 vars in TOTAL (1 rounds, 80 queries)
c [phase-count-5] 64992 negative 93.9% of 69191 except 4199 6.1%
c [phase-count-5] 59449 positive 85.9% of 69191 except 9742 14.1%
c [phase-count-5] less non-negative clauses 4199 than limit 6900 (10.0%)
c [phase-count-5] non-pos/non-neg = 9742/4199 = 2.32 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 78 negative 100%
c [sort-queue-5] sorted 3208 enqueued variables after 36337 conflicts
c [score-dist-5] active 6965 (68%), one 0 (0%), zero 3208 (32%)
c [score-dist-5] max exp 516, different 16 (3%)
c [score-dist-5] median active exp 509, avg 509.1
c [simplification-5] removed 576 variables 5.4% (10173 remain 20%)
c [simplification-5] removed 5759 irredundant clauses 7.7% (69191 remain 33%)
c [simplification-5] maximum reduction of 8% = max (5%, 8%)
c [simplification-5] large reduction 8% >= 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 48337 (soft 38337 + delta 10000)
c [simplification-5] new conflict limit 38337 (hard 48337)
c 
c [simplification-6] limit 38337 conflicts (hard 48337) hit after 38337 conflicts
c [quatres-2] found 7833 quaternary clauses 32% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 6 single-self-subsuming ternary resolvents
c [quatres-2-2] added 366 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 10173 free variables schedulable
c [ternres-2] 23 ternary resolvents (0 bin, 23 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 403 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 403 out of 403 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 376677 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 20346 literals 100%
c [treelook-3] scheduling used 324950 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 376677 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 378299 steps
c [treelook-3] 20122 literals remain 99%
c [treelook-3] 10172 variables remain to probed next time 100%
c [treelook-3] removed 1 variables, found 194 hbrs
c [unhide-5] limit 376677 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 197 tauts, 0 hbrs, 81925 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 954 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 1293 (0%) of length 8
c [cce-2-1] eliminated 4 clauses out of 2844 (0%) of length 7
c [cce-2-1] eliminated 3 clauses out of 3846 (0%) of length 6
c [cce-2-1] eliminated 279 clauses out of 5269 (5%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 287 large clauses in 30000006 steps
c [cce-2-1] allowing another 15000003 steps for small clauses
c [cce-2-1] scheduling 40137 clauses = 34220 binary + 5917 ternary
c [cce-2-1] tried to eliminate 7049 small clauses 18%
c [cce-2-1] eliminated 534 binary clauses 2%
c [cce-2-1] eliminated 96 ternary clauses 2%
c [cce-2-1] eliminated 630 small clauses 2%
c [cce-2-1] eliminated 630 small clauses in 30000036 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 917 covered clauses in round 1
c [cce-2] eliminated 917 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 10172 variables 100%
c [elim-5] limit of 37667726 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 205 variables 2% in round 1 in 14950601 steps
c [elim-5-1] backward subsumption/strengthening limit 14950600
c [elim-5-1-1] backward checking 2115 touched variables 21%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 7 and strengthened 13 clauses in 2203549 steps
c [elim-5-1] rescheduled 63 variables 1% by backward subsumption
c [elim-5-2] eliminated 4 variables 0% in round 2 in 3338771 steps
c [elim-5-2] backward subsumption/strengthening limit 3338700
c [elim-5-2-1] backward checking 39 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 3 and strengthened 6 clauses in 54809 steps
c [elim-5-2] rescheduled 24 variables 0% by backward subsumption
c [elim-5-3] eliminated 2 variables 0% in round 3 in 23569 steps
c [elim-5-3] backward subsumption/strengthening limit 23500
c [elim-5-3-1] backward checking 20 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 0 and strengthened 0 clauses in 23501 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 211 = 2% variables out of 10172 scheduled
c [bca-2] limit of 10000000 steps and 134158 added (scaled 2)
c [bca-2] 12729 out of 19924 literals actually usable 64%
c [bca-2] added 20 blocked clauses in 58118 steps
c [sweep-2] limit 1130031 penalty 0 = 0 + 0
c [sweep-2-1] 2997 pos 33.9% + 5833 neg 66.1% = 8830 sched 88.6% ret 1131
c [sweep-2-1] 1130222 steps 54 queries 633.65 avg class size
c [sweep-2-1] 1449 decisions 53 SAT calls 91.42 avg env size
c [sweep-2-1] 7997 variables remain 80% (1962 retained 20%)
c [decomp-14] removed 6 variables
c [sweep-2-1] removed 6 vars (0 failed, 3 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 6 vars in TOTAL (1 rounds, 53 queries)
c [phase-count-6] 62703 negative 93.9% of 66798 except 4095 6.1%
c [phase-count-6] 57448 positive 86.0% of 66798 except 9350 14.0%
c [phase-count-6] less non-negative clauses 4095 than limit 6600 (10.0%)
c [phase-count-6] non-pos/non-neg = 9350/4095 = 2.28 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 71 negative 100%
c [sort-queue-6] sorted 2985 enqueued variables after 38337 conflicts
c [score-dist-6] active 6970 (70%), one 0 (0%), zero 2985 (30%)
c [score-dist-6] max exp 517, different 17 (3%)
c [score-dist-6] median active exp 509, avg 509.2
c [simplification-6] removed 218 variables 2.1% (9955 remain 20%)
c [simplification-6] removed 2393 irredundant clauses 3.5% (66798 remain 32%)
c [simplification-6] maximum reduction of 3% = max (2%, 3%)
c [simplification-6] geometric conflict interval increment 5166 = 20666 / 4
c [simplification-6] new conflict interval 25832
c [simplification-6] penalized conflict interval 25832 = 1 * 25832
c [simplification-6] hard conflict limit 77085 (soft 64169 + delta 12916)
c [simplification-6] new conflict limit 64169 (hard 77085)
c 
c [simplification-7] limit 64169 conflicts (hard 77085) hit after 64173 conflicts
c [quatres-3] found 8386 quaternary clauses 34% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [quatres-3-2] added 194 quaternary resolvents
c [ternres-3] limit 6702316 with penalty 0 = 0 + 0
c [ternres-3] all 9955 free variables schedulable
c [ternres-3] 77 ternary resolvents (0 bin, 77 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1615 xors of average arity 3.0
c [gauss-2] connected 4841 occurrences of 459 variables (average 10.5)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 33511584 penalty 0 = 0 + 0
c [basicprobe-3-0] 1204 sched 12%, 10 failed, 0 lifted, 1270 hbrs
c [decomp-16] removed 18 variables
c [basicprobe-3-1] 5840 sched 59%, 36 failed, 0 lifted, 1346 hbrs
c [decomp-17] removed 58 variables
c [basicprobe-3-2] 5767 sched 58%, 5 failed, 0 lifted, 215 hbrs
c [decomp-18] removed 5 variables
c [basicprobe-3-3] 5752 sched 58%, 0 failed, 0 lifted, 36 hbrs
c [decomp-19] removed 2 variables
c [basicprobe-3-4] 5750 sched 58%, 0 failed, 0 lifted, 30 hbrs
c [basicprobe-3-5] 4127 probes remain 42% after last round
c [basicprobe-3-5] 51 units = 51 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 83 variables, found 2899 hbrs
c [bate-1] eliminated 91 asymmetric tautologies during probing
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 905 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 9872 variables 100%
c [block-2] limit of 33511584 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 7 blocked clauses
c [block-2] 7 < 1/100 * 65993 = 659 considered unsuccessful
c [cce-3] limit of 33511584 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 86 (1%) of length 12
c [cce-3-1] eliminated 5 clauses out of 417 (1%) of length 11
c [cce-3-1] eliminated 4 clauses out of 660 (1%) of length 9
c [cce-3-1] eliminated 6 clauses out of 1371 (0%) of length 8
c [cce-3-1] eliminated 91 clauses out of 2884 (3%) of length 7
c [cce-3-1] eliminated 132 clauses out of 3912 (3%) of length 6
c [cce-3-1] eliminated 187 clauses out of 4832 (4%) of length 5
c [cce-3-1] eliminated 6 clauses out of 7096 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 432 large clauses in 33511629 steps
c [cce-3-1] allowing another 16755814 steps for small clauses
c [cce-3-1] scheduling 39003 clauses = 32773 binary + 6230 ternary
c [cce-3-1] tried to eliminate 7477 small clauses 19%
c [cce-3-1] eliminated 1083 binary clauses 3%
c [cce-3-1] eliminated 88 ternary clauses 1%
c [cce-3-1] eliminated 1171 small clauses 3%
c [cce-3-1] eliminated 1171 small clauses in 33511584 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1603 covered clauses in round 1
c [cce-3] eliminated 1603 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 9872 variables 100%
c [elim-6] limit of 134046337 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 241 variables 2% in round 1 in 14197770 steps
c [elim-6-1] backward subsumption/strengthening limit 14197700
c [elim-6-1-1] backward checking 1713 touched variables 17%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 3 and strengthened 11 clauses in 1874202 steps
c [elim-6-1] rescheduled 43 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 103626 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 241 = 2% variables out of 9872 scheduled
c [bca-3] limit of 10000000 steps and 127794 added (scaled 2)
c [bca-3] 11777 out of 19264 literals actually usable 61%
c [bca-3] added 77 blocked clauses in 68751 steps
c [sweep-3] limit 2010695 penalty 0 = 0 + 0
c [sweep-3-1] 2679 pos 34.8% + 5020 neg 65.2% = 7699 sched 79.9% ret 1932
c [sweep-3-1] 2025144 steps 155 queries 241.30 avg class size
c [sweep-3-1] 4482 decisions 147 SAT calls 109.10 avg env size
c [sweep-3-1] 5126 variables remain 53% (4505 retained 47%)
c [decomp-21] removed 9 variables
c [sweep-3-1] removed 9 vars (0 failed, 7 eqs, 17 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 9 vars in TOTAL (1 rounds, 154 queries)
c [phase-count-7] 59840 negative 94.0% of 63627 except 3787 6.0%
c [phase-count-7] 54793 positive 86.1% of 63627 except 8834 13.9%
c [phase-count-7] less non-negative clauses 3787 than limit 6300 (10.0%)
c [phase-count-7] non-pos/non-neg = 8834/3787 = 2.33 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 32 negative 100%
c [sort-queue-7] sorted 2603 enqueued variables after 64173 conflicts
c [score-dist-7] active 7019 (73%), one 0 (0%), zero 2603 (27%)
c [score-dist-7] max exp 517, different 17 (3%)
c [score-dist-7] median active exp 510, avg 509.7
c [simplification-7] removed 333 variables 3.3% (9622 remain 19%)
c [simplification-7] removed 3171 irredundant clauses 4.7% (63627 remain 30%)
c [simplification-7] maximum reduction of 5% = max (3%, 5%)
c [simplification-7] large reduction 5% >= 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 76173 (soft 66173 + delta 10000)
c [simplification-7] new conflict limit 66173 (hard 76173)
c 
c [simplification-8] limit 66173 conflicts (hard 76173) hit after 66173 conflicts
c [quatres-4] found 8437 quaternary clauses 35% in total
c [quatres-4-1] removed 6 duplicate quaternary clauses
c [quatres-4-2] added 4 single-self-subsuming ternary resolvents
c [quatres-4-2] added 158 quaternary resolvents
c [ternres-4] limit 6909500 with penalty 0 = 0 + 0
c [ternres-4] all 9622 free variables schedulable
c [ternres-4] 118 ternary resolvents (3 bin, 115 trn)
c [ternres-4] fully completed ternary resolution
c [simpleprobe-4] all 9622 free variables schedulable
c [simpleprobe-4] limit 27638001 penalty 0 = 0 + 0
c [decomp-23] removed 143 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 143 variables, found 3174 hbrs, 14 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1951 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 345475010 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 22 clauses out of 69 (32%) of length 12
c [cce-4-1] eliminated 70 clauses out of 411 (17%) of length 11
c [cce-4-1] eliminated 54 clauses out of 282 (19%) of length 10
c [cce-4-1] eliminated 1 clauses out of 593 (0%) of length 9
c [cce-4-1] eliminated 1 clauses out of 1268 (0%) of length 8
c [cce-4-1] eliminated 3 clauses out of 2930 (0%) of length 7
c [cce-4-1] eliminated 33 clauses out of 3864 (1%) of length 6
c [cce-4-1] eliminated 84 clauses out of 4645 (2%) of length 5
c [cce-4-1] eliminated 860 clauses out of 7038 (12%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 1128 large clauses in 37113266 steps
c [cce-4-1] allowing another 18556633 steps for small clauses
c [cce-4-1] scheduling 35531 clauses = 30117 binary + 5414 ternary
c [cce-4-1] tried to eliminate 35531 small clauses 100%
c [cce-4-1] eliminated 1320 binary clauses 4%
c [cce-4-1] eliminated 361 ternary clauses 7%
c [cce-4-1] eliminated 1681 small clauses 5%
c [cce-4-1] eliminated 1681 small clauses in 85821920 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 2809 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 16988265 steps for small clauses
c [cce-4-2] scheduling 33850 clauses = 28797 binary + 5053 ternary
c [cce-4-2] tried to eliminate 33850 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 2809 covered clauses in TOTAL during 2 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 9479 variables 100%
c [elim-7] limit of 138190005 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 178 variables 2% in round 1 in 13309975 steps
c [elim-7-1] backward subsumption/strengthening limit 13309900
c [elim-7-1-1] backward checking 1881 touched variables 20%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 4 and strengthened 12 clauses in 1807146 steps
c [elim-7-1] rescheduled 58 variables 1% by backward subsumption
c [elim-7-2] eliminated 5 variables 0% in round 2 in 59216 steps
c [elim-7-2] backward subsumption/strengthening limit 59200
c [elim-7-2-1] backward checking 33 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 2 and strengthened 5 clauses in 51674 steps
c [elim-7-2] rescheduled 19 variables 0% by backward subsumption
c [elim-7-3] eliminated 2 variables 0% in round 3 in 20612 steps
c [elim-7-3] backward subsumption/strengthening limit 20600
c [elim-7-3-1] backward checking 17 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 5 and strengthened 0 clauses in 20601 steps
c [elim-7] incomplete 9 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 185 = 2% variables out of 9479 scheduled
c [bca-4] limit of 10000000 steps and 119213 added (scaled 2)
c [bca-4] 11243 out of 18590 literals actually usable 60%
c [bca-4] added 43 blocked clauses in 51047 steps
c [sweep-4] limit 2072850 penalty 0 = 0 + 0
c [sweep-4-1] 1615 pos 33.0% + 3282 neg 67.0% = 4897 sched 52.7% ret 4397
c [sweep-4-1] 2073280 steps 300 queries 213.20 avg class size
c [sweep-4-1] 4816 decisions 291 SAT calls 45.93 avg env size
c [sweep-4-1] 2544 variables remain 27% (6747 retained 73%)
c [decomp-24] removed 17 variables
c [sweep-4-1] removed 17 vars (0 failed, 11 eqs, 22 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 17 vars in TOTAL (1 rounds, 299 queries)
c [phase-count-8] 55783 negative 94.1% of 59309 except 3526 5.9%
c [phase-count-8] 50858 positive 85.8% of 59309 except 8451 14.2%
c [phase-count-8] less non-negative clauses 3526 than limit 5900 (10.0%)
c [phase-count-8] non-pos/non-neg = 8451/3526 = 2.40 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 13 negative 100%
c [sort-queue-8] sorted 2253 enqueued variables after 66173 conflicts
c [score-dist-8] active 7024 (76%), one 0 (0%), zero 2253 (24%)
c [score-dist-8] max exp 517, different 17 (3%)
c [score-dist-8] median active exp 510, avg 509.5
c [simplification-8] removed 345 variables 3.6% (9277 remain 18%)
c [simplification-8] removed 4318 irredundant clauses 6.8% (59309 remain 28%)
c [simplification-8] maximum reduction of 7% = max (4%, 7%)
c [simplification-8] large reduction 7% >= 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 78173 (soft 68173 + delta 10000)
c [simplification-8] new conflict limit 68173 (hard 78173)
c 
c [simplification-9] limit 68173 conflicts (hard 78173) hit after 68173 conflicts
c [quatres-5] found 7683 quaternary clauses 33% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-2] added 9 single-self-subsuming ternary resolvents
c [quatres-5-2] added 118 quaternary resolvents
c [ternres-5] limit 7050928 with penalty 0 = 0 + 0
c [ternres-5] all 9277 free variables schedulable
c [ternres-5] 73 ternary resolvents (3 bin, 70 trn)
c [ternres-5] fully completed ternary resolution
c [treelook-4] limit 705092 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 18554 literals 100%
c [treelook-4] scheduling used 281558 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 705092 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 707115 steps
c [treelook-4] 18187 literals remain 98%
c [treelook-4] 9276 variables remain to probed next time 100%
c [decomp-26] removed 26 variables
c [treelook-4] removed 27 variables, found 524 hbrs
c [unhide-6] limit 352546 with penalty 2 = 2 + 0
c [unhide-6-6] 0 units, 16 failed, 1762 tauts, 0 hbrs, 70634 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1042 transitive binary clauses
c [transred-5] found 2 units
c [cce-5] limit of 35254644 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-5-1] eliminated 21 clauses out of 43 (49%) of length 12
c [cce-5-1] eliminated 25 clauses out of 404 (6%) of length 11
c [cce-5-1] eliminated 5 clauses out of 230 (2%) of length 10
c [cce-5-1] eliminated 1 clauses out of 667 (0%) of length 9
c [cce-5-1] eliminated 7 clauses out of 809 (1%) of length 8
c [cce-5-1] eliminated 31 clauses out of 3123 (1%) of length 7
c [cce-5-1] eliminated 115 clauses out of 3992 (3%) of length 6
c [cce-5-1] eliminated 162 clauses out of 4528 (4%) of length 5
c [cce-5-1] eliminated 123 clauses out of 6200 (2%) of length 4
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 492 large clauses in 35254646 steps
c [cce-5-1] allowing another 17627323 steps for small clauses
c [cce-5-1] scheduling 34045 clauses = 28152 binary + 5893 ternary
c [cce-5-1] tried to eliminate 8876 small clauses 26%
c [cce-5-1] eliminated 738 binary clauses 3%
c [cce-5-1] eliminated 87 ternary clauses 1%
c [cce-5-1] eliminated 825 small clauses 2%
c [cce-5-1] eliminated 864 small clauses in 35254650 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1356 covered clauses in round 1
c [cce-5] eliminated 1356 covered clauses in TOTAL during 1 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 9242 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2820371560 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 223 variables 2% in round 1 in 12124858 steps
c [elim-8-1] backward subsumption/strengthening limit 12124800
c [elim-8-1-1] backward checking 1756 touched variables 19%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 6 and strengthened 15 clauses in 1782372 steps
c [elim-8-1] rescheduled 58 variables 1% by backward subsumption
c [elim-8-2] eliminated 3 variables 0% in round 2 in 160206 steps
c [elim-8-2] backward subsumption/strengthening limit 160200
c [elim-8-2-1] backward checking 32 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 2 and strengthened 5 clauses in 48267 steps
c [elim-8-2] rescheduled 10 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 39038 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 226 = 2% variables out of 9242 scheduled
c [bca-5] limit of 10000000 steps and 114946 added (scaled 2)
c [bca-5] 10797 out of 18034 literals actually usable 60%
c [bca-5] added 123 blocked clauses in 47509 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 21152780 penalty 0 = 0 + 0
c [sweep-5-1] 828 pos 34.1% + 1603 neg 65.9% = 2431 sched 27.0% ret 6585
c [sweep-5-1] 3608219 steps 624 queries 35.21 avg class size
c [sweep-5-1] 8959 decisions 593 SAT calls 36.45 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-27] removed 49 variables
c [sweep-5-1] removed 49 vars (0 failed, 37 eqs, 61 impls)
c [sweep-5-2] 2958 pos 33.0% + 6009 neg 67.0% = 8967 sched 100.0% ret 0
c [sweep-5-2] 6363688 steps 933 queries 47.57 avg class size
c [sweep-5-2] 14056 decisions 879 SAT calls 45.97 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-28] removed 65 variables
c [sweep-5-2] removed 65 vars (0 failed, 55 eqs, 101 impls)
c [sweep-5-3] 2924 pos 32.8% + 5978 neg 67.2% = 8902 sched 100.0% ret 0
c [sweep-5-3] 6554965 steps 900 queries 42.91 avg class size
c [sweep-5-3] 14213 decisions 879 SAT calls 43.66 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-29] removed 25 variables
c [sweep-5-3] removed 25 vars (0 failed, 24 eqs, 55 impls)
c [sweep-5] removed 139 vars in TOTAL (3 rounds, 2454 queries)
c [sort-queue-9] sorted 1428 enqueued variables after 68173 conflicts
c [score-dist-9] active 7449 (84%), one 0 (0%), zero 1428 (16%)
c [score-dist-9] max exp 517, different 17 (3%)
c [score-dist-9] median active exp 509, avg 509.0
c [simplification-9] removed 400 variables 4.3% (8877 remain 18%)
c [simplification-9] removed 2375 irredundant clauses 4.0% (56934 remain 27%)
c [simplification-9] maximum reduction of 4% = max (4%, 4%)
c [simplification-9] geometric conflict interval increment 5166 = 25832 / 5
c [simplification-9] new conflict interval 30998
c [simplification-9] penalized conflict interval 30998 = 1 * 30998
c [simplification-9] hard conflict limit 114670 (soft 99171 + delta 15499)
c [simplification-9] new conflict limit 99171 (hard 114670)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   47.6    8876    56934     72927   23685   3200 12962   32    41   18  76%    682    7   23   24   99%
c i   47.7    8874    56934     73643   24325   3229 12973   29    55   18  54%    116   21   23   24   97%
c 
c [simplification-10] limit 99171 conflicts (hard 114670) hit after 103384 conflicts
c [quatres-6] found 7864 quaternary clauses 33% in total
c [quatres-6-1] removed 7 duplicate quaternary clauses
c [quatres-6-2] added 21 single-self-subsuming ternary resolvents
c [quatres-6-2] added 131 quaternary resolvents
c [ternres-6] limit 10147710 with penalty 0 = 0 + 0
c [ternres-6] all 8874 free variables schedulable
c [ternres-6] 239 ternary resolvents (7 bin, 232 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 634231 penalty 3 = 3 + 0
c [card-4] found 485 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 634231 for elimination
c [card-4] 485 out of 485 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 507385 penalty 2 = 2 + 0
c [gauss-3] extracted 889 xors of average arity 3.0
c [gauss-3] connected 2662 occurrences of 416 variables (average 6.4)
c [gauss-3] limit 507385 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 1 variables
c [basicprobe-4] limit 50738551 penalty 0 = 0 + 0
c [basicprobe-4-0] 3678 sched 42%, 33 failed, 0 lifted, 866 hbrs
c [decomp-31] removed 51 variables
c [basicprobe-4-1] 4980 sched 57%, 18 failed, 0 lifted, 498 hbrs
c [decomp-32] removed 22 variables
c [basicprobe-4-2] 4945 sched 56%, 4 failed, 0 lifted, 173 hbrs
c [decomp-33] removed 4 variables
c [basicprobe-4-3] 4935 sched 56%, 0 failed, 0 lifted, 73 hbrs
c [basicprobe-4-4] 4930 sched 56%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-4-5] 4929 sched 56%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-6] 4929 sched 56%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-4-7] 4929 sched 56%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-8] 1140 probes remain 13% after last round
c [basicprobe-4-8] 55 units = 55 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 77 variables, found 1637 hbrs
c [bate-2] eliminated 40 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1303 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 8796 variables 100%
c [block-3] limit of 25369275 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 19 blocked clauses
c [block-3] 19 < 1/100 * 56023 = 560 considered unsuccessful
c [cce-6] limit of 50738551 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 40 clauses out of 336 (12%) of length 11
c [cce-6-1] eliminated 3 clauses out of 203 (1%) of length 10
c [cce-6-1] eliminated 15 clauses out of 691 (2%) of length 9
c [cce-6-1] eliminated 15 clauses out of 805 (2%) of length 8
c [cce-6-1] eliminated 36 clauses out of 2993 (1%) of length 7
c [cce-6-1] eliminated 99 clauses out of 3824 (3%) of length 6
c [cce-6-1] eliminated 80 clauses out of 4418 (2%) of length 5
c [cce-6-1] eliminated 166 clauses out of 5952 (3%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 454 large clauses in 28892311 steps
c [cce-6-1] allowing another 14446155 steps for small clauses
c [cce-6-1] scheduling 31790 clauses = 26272 binary + 5518 ternary
c [cce-6-1] tried to eliminate 21958 small clauses 69%
c [cce-6-1] eliminated 103 binary clauses 0%
c [cce-6-1] eliminated 146 ternary clauses 3%
c [cce-6-1] eliminated 249 small clauses 1%
c [cce-6-1] eliminated 249 small clauses in 50738603 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 703 covered clauses in round 1
c [cce-6] eliminated 703 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8795 variables 100%
c [elim-9] limit of 202954206 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 119 variables 1% in round 1 in 11382014 steps
c [elim-9-1] backward subsumption/strengthening limit 11382000
c [elim-9-1-1] backward checking 704 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 1 and strengthened 2 clauses in 884373 steps
c [elim-9-1] rescheduled 17 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 71102 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 119 = 1% variables out of 8795 scheduled
c [bca-6] limit of 10000000 steps and 110298 added (scaled 2)
c [bca-6] 8768 out of 17354 literals actually usable 51%
c [bca-6] added 5 blocked clauses in 67059 steps
c [sweep-6] limit 3044313 penalty 0 = 0 + 0
c [sweep-6-1] 2859 pos 33.0% + 5817 neg 67.0% = 8676 sched 100.0% ret 0
c [sweep-6-1] 3044454 steps 252 queries 106.00 avg class size
c [sweep-6-1] 6307 decisions 252 SAT calls 77.74 avg env size
c [sweep-6-1] 3205 variables remain 37% (5471 retained 63%)
c [decomp-39] removed 1 variables
c [sweep-6-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-6] 1 < 1/1000 * 8676 = 8 considered unsuccessful
c [sweep-6] removed 1 vars in TOTAL (1 rounds, 251 queries)
c [sort-queue-10] sorted 1274 enqueued variables after 103384 conflicts
c [score-dist-10] active 7401 (85%), one 0 (0%), zero 1274 (15%)
c [score-dist-10] max exp 518, different 18 (3%)
c [score-dist-10] median active exp 510, avg 509.6
c [simplification-10] removed 199 variables 2.2% (8675 remain 17%)
c [simplification-10] removed 2104 irredundant clauses 3.7% (54830 remain 26%)
c [simplification-10] maximum reduction of 4% = max (2%, 4%)
c [simplification-10] geometric conflict interval increment 6199 = 30998 / 5
c [simplification-10] new conflict interval 37197
c [simplification-10] penalized conflict interval 37197 = 1 * 37197
c [simplification-10] hard conflict limit 159179 (soft 140581 + delta 18598)
c [simplification-10] new conflict limit 140581 (hard 159179)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   69.1    8675    54830    118251   27776   3520 12446   29    32   15  89%    267   -7   28   27  103%
c 
c [simplification-11] limit 140581 conflicts (hard 159179) hit after 159180 conflicts
c [quatres-7] found 7655 quaternary clauses 32% in total
c [quatres-7-1] removed 5 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 8 single-self-subsuming ternary resolvents
c [quatres-7-2] added 71 quaternary resolvents
c [ternres-7] limit 16853268 with penalty 0 = 0 + 0
c [ternres-7] all 8675 free variables schedulable
c [ternres-7] 62 ternary resolvents (7 bin, 55 trn)
c [ternres-7] fully completed ternary resolution
c [simpleprobe-5] all 8675 free variables schedulable
c [simpleprobe-5] limit 67413072 penalty 0 = 0 + 0
c [decomp-41] removed 7 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 7 variables, found 3493 hbrs, 0 units
c [unhide-7] limit 1685326 with penalty 1 = 1 + 0
c [unhide-7-8] 0 units, 0 failed, 1882 tauts, 0 hbrs, 283778 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1507 transitive binary clauses
c [cce-7] limit of 84266340 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 293 (0%) of length 11
c [cce-7-1] eliminated 4 clauses out of 202 (2%) of length 10
c [cce-7-1] eliminated 4 clauses out of 670 (1%) of length 9
c [cce-7-1] eliminated 9 clauses out of 771 (1%) of length 8
c [cce-7-1] eliminated 2 clauses out of 2881 (0%) of length 7
c [cce-7-1] eliminated 16 clauses out of 3721 (0%) of length 6
c [cce-7-1] eliminated 38 clauses out of 4335 (1%) of length 5
c [cce-7-1] eliminated 115 clauses out of 5790 (2%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 189 large clauses in 29790931 steps
c [cce-7-1] allowing another 14895465 steps for small clauses
c [cce-7-1] scheduling 30764 clauses = 25798 binary + 4966 ternary
c [cce-7-1] tried to eliminate 30764 small clauses 100%
c [cce-7-1] eliminated 1475 binary clauses 6%
c [cce-7-1] eliminated 110 ternary clauses 2%
c [cce-7-1] eliminated 1585 small clauses 5%
c [cce-7-1] eliminated 1585 small clauses in 67306303 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 1774 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 198 (1%) of length 10
c [cce-7-2] eliminated 3 clauses out of 666 (0%) of length 9
c [cce-7-2] eliminated 5 clauses out of 762 (1%) of length 8
c [cce-7-2] eliminated 14 clauses out of 2879 (0%) of length 7
c [cce-7-2] eliminated 5 clauses out of 3705 (0%) of length 6
c [cce-7-2] eliminated 4 clauses out of 4297 (0%) of length 5
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 32 large clauses in 16960043 steps
c [cce-7-2] allowing another 8480021 steps for small clauses
c [cce-7-2] scheduling 29179 clauses = 24323 binary + 4856 ternary
c [cce-7-2] tried to eliminate 5279 small clauses 18%
c [cce-7-2] eliminated 7 binary clauses 0%
c [cce-7-2] eliminated 7 small clauses 0%
c [cce-7-2] eliminated 7 small clauses in 16960045 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 39 covered clauses in round 2
c [cce-7] eliminated 1813 covered clauses in TOTAL during 2 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8668 variables 100%
c [elim-10] limit of 337065361 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 278 variables 3% in round 1 in 10980871 steps
c [elim-10-1] backward subsumption/strengthening limit 10980800
c [elim-10-1-1] backward checking 1952 touched variables 23%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 6 clauses in 1292269 steps
c [elim-10-1] rescheduled 40 variables 0% by backward subsumption
c [elim-10-2] eliminated 3 variables 0% in round 2 in 35182 steps
c [elim-10-2] backward subsumption/strengthening limit 35100
c [elim-10-2-1] backward checking 26 touched variables 0%
c [elim-10-2-1] incomplete backward checking 16 remain 62%
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 36262 steps
c [elim-10-2] fully rescheduled 8387 variables 97%
c [elim-10-3] eliminated 23 variables 0% in round 3 in 10897907 steps
c [elim-10-3] backward subsumption/strengthening limit 10897900
c [elim-10-3-1] backward checking 192 touched variables 2%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 1 clauses in 643713 steps
c [elim-10] incomplete 6 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 304 = 4% variables out of 8668 scheduled
c [bca-7] limit of 10000000 steps and 105562 added (scaled 2)
c [bca-7] 8494 out of 16730 literals actually usable 51%
c [bca-7] added 17 blocked clauses in 57597 steps
c [sort-queue-11] sorted 1167 enqueued variables after 159180 conflicts
c [score-dist-11] active 7197 (86%), one 0 (0%), zero 1167 (14%)
c [score-dist-11] max exp 519, different 19 (4%)
c [score-dist-11] median active exp 511, avg 510.2
c [simplification-11] removed 311 variables 3.6% (8364 remain 17%)
c [simplification-11] removed 2367 irredundant clauses 4.3% (52463 remain 25%)
c [simplification-11] maximum reduction of 4% = max (4%, 4%)
c [simplification-11] geometric conflict interval increment 7439 = 37197 / 5
c [simplification-11] new conflict interval 44636
c [simplification-11] penalized conflict interval 44636 = 1 * 44636
c [simplification-11] hard conflict limit 226134 (soft 203816 + delta 22318)
c [simplification-11] new conflict limit 203816 (hard 226134)
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  100.8    8363    52463    183353   54220   3161 12678   28    35   33  80%    744    0   27   27  102%
c -  101.2    8363    52463    184792   29353   3163 12678   28    37   15  75%   -527    3   32   27  121%
c -  119.8    8363    52463    223159   30426   3172 12684   27    30   20  89%    -77   -5   19   28   69%
c 
c [simplification-12] limit 203816 conflicts (hard 226134) hit after 226135 conflicts
c [quatres-8] found 7663 quaternary clauses 33% in total
c [quatres-8-1] removed 10 duplicate quaternary clauses
c [quatres-8-2] added 20 single-self-subsuming ternary resolvents
c [quatres-8-2] added 114 quaternary resolvents
c [ternres-8] limit 24994865 with penalty 0 = 0 + 0
c [ternres-8] all 8363 free variables schedulable
c [ternres-8] 292 ternary resolvents (6 bin, 286 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-42] removed 1 variables
c [treelook-5] limit 2499486 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 16726 literals 100%
c [treelook-5] scheduling used 280951 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2499486 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2499911 steps
c [treelook-5] 15335 literals remain 92%
c [treelook-5] 8354 variables remain to probed next time 100%
c [decomp-43] removed 3 variables
c [treelook-5] removed 4 variables, found 2373 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1209 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 1249743250 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 3 clauses out of 28 (11%) of length 12
c [cce-8-1] eliminated 1 clauses out of 299 (0%) of length 11
c [cce-8-1] eliminated 4 clauses out of 203 (2%) of length 10
c [cce-8-1] eliminated 7 clauses out of 696 (1%) of length 9
c [cce-8-1] eliminated 7 clauses out of 806 (1%) of length 8
c [cce-8-1] eliminated 13 clauses out of 2830 (0%) of length 7
c [cce-8-1] eliminated 34 clauses out of 3761 (1%) of length 6
c [cce-8-1] eliminated 42 clauses out of 4266 (1%) of length 5
c [cce-8-1] eliminated 80 clauses out of 5901 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 191 large clauses in 26416615 steps
c [cce-8-1] allowing another 13208307 steps for small clauses
c [cce-8-1] scheduling 28383 clauses = 23658 binary + 4725 ternary
c [cce-8-1] tried to eliminate 28383 small clauses 100%
c [cce-8-1] eliminated 17 binary clauses 0%
c [cce-8-1] eliminated 27 ternary clauses 1%
c [cce-8-1] eliminated 44 small clauses 0%
c [cce-8-1] eliminated 44 small clauses in 56507675 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 235 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 13134595 steps for small clauses
c [cce-8-2] scheduling 28339 clauses = 23641 binary + 4698 ternary
c [cce-8-2] tried to eliminate 28339 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 235 covered clauses in TOTAL during 2 rounds
c [cce-8] 235 < 1/100 * 52435 = 524 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 8359 variables 100%
c [elim-11] limit of 499897300 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 27 variables 0% in round 1 in 10812048 steps
c [elim-11-1] backward subsumption/strengthening limit 10812000
c [elim-11-1-1] backward checking 209 touched variables 3%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 1 clauses in 147547 steps
c [elim-11-1] rescheduled 5 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 4618 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 27 = 0% variables out of 8359 scheduled
c [elim-11] 27 < 1/100 * 8359 = 83 considered unsuccessful
c [bca-8] limit of 10000000 steps and 104979 added (scaled 2)
c [bca-8] 8520 out of 16666 literals actually usable 51%
c [bca-8] added 2 blocked clauses in 52558 steps
c [sweep-7] limit 3749229 penalty 1 = 1 + 0
c [sweep-7-1] 985 pos 32.3% + 2068 neg 67.7% = 3053 sched 36.6% ret 5279
c [sweep-7-1] 3750124 steps 459 queries 40.42 avg class size
c [sweep-7-1] 7016 decisions 455 SAT calls 41.11 avg env size
c [sweep-7-1] 326 variables remain 4% (8005 retained 96%)
c [decomp-44] removed 5 variables
c [sweep-7-1] removed 5 vars (0 failed, 4 eqs, 11 impls)
c [sweep-7] 5 < 1/1000 * 8332 = 8 considered unsuccessful
c [sweep-7] removed 5 vars in TOTAL (1 rounds, 458 queries)
c [sort-queue-12] sorted 1056 enqueued variables after 226135 conflicts
c [score-dist-12] active 7271 (87%), one 0 (0%), zero 1056 (13%)
c [score-dist-12] max exp 519, different 19 (4%)
c [score-dist-12] median active exp 512, avg 510.6
c [simplification-12] removed 36 variables 0.4% (8327 remain 16%)
c [simplification-12] removed 309 irredundant clauses 0.6% (52154 remain 25%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 22318 = 44636 / 2
c [simplification-12] new conflict interval 66954
c [simplification-12] penalized conflict interval 66954 = 1 * 66954
c [simplification-12] hard conflict limit 326566 (soft 293089 + delta 33477)
c [simplification-12] new conflict limit 293089 (hard 326566)
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 -  141.4    8327    52154    263896   28685   3505 13791   24    27   19  90%    433   -6   25   28   91%
c 
c [simplification-13] limit 293089 conflicts (hard 326566) hit after 293091 conflicts
c [quatres-9] found 7771 quaternary clauses 32% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 15 single-self-subsuming ternary resolvents
c [quatres-9-2] added 42 quaternary resolvents
c [ternres-9] limit 32100679 with penalty 0 = 0 + 0
c [ternres-9] all 8327 free variables schedulable
c [ternres-9] 85 ternary resolvents (6 bin, 79 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-45] removed 1 variables
c [basicprobe-5] limit 160503395 penalty 0 = 0 + 0
c [basicprobe-5-0] 1120 sched 13%, 0 failed, 0 lifted, 214 hbrs
c [basicprobe-5-1] 4515 sched 54%, 4 failed, 0 lifted, 556 hbrs
c [decomp-47] removed 4 variables
c [basicprobe-5-2] 4496 sched 54%, 3 failed, 0 lifted, 96 hbrs
c [decomp-48] removed 3 variables
c [basicprobe-5-3] 4498 sched 54%, 1 failed, 0 lifted, 116 hbrs
c [decomp-49] removed 1 variables
c [basicprobe-5-4] 4497 sched 54%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-5-5] 4497 sched 54%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-5-6] 4497 sched 54%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-5-7] 4497 sched 54%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-5-8] 4497 sched 54%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 8 units = 8 failed (100%) + 0 lifted (0%)
c [basicprobe-5-8] removed 8 variables, found 1027 hbrs
c [bate-3] eliminated 6 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 857 transitive binary clauses
c [bca-9] limit of 10000000 steps and 104820 added (scaled 2)
c [bca-9] 8227 out of 16638 literals actually usable 49%
c [bca-9] added 6 blocked clauses in 76253 steps
c [sort-queue-13] sorted 1043 enqueued variables after 293091 conflicts
c [score-dist-13] active 7275 (87%), one 0 (0%), zero 1043 (13%)
c [score-dist-13] max exp 520, different 20 (4%)
c [score-dist-13] median active exp 512, avg 510.9
c [simplification-13] removed 9 variables 0.1% (8318 remain 16%)
c [simplification-13] removed 67 irredundant clauses 0.1% (52087 remain 25%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 66954
c [simplification-13] new conflict interval 133908
c [simplification-13] penalized conflict interval 133908 = 1 * 133908
c [simplification-13] hard conflict limit 493953 (soft 426999 + delta 66954)
c [simplification-13] new conflict limit 426999 (hard 493953)
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 -  153.4    8318    52087    297712   28282   3627 13836   39    59   14  66%    671   19   36   29  121%
c -  165.2    8318    52087    334520   30923   3651 13841   27    32   20  86%    823   -9   26   29   91%
c -  177.2    8318    52087    370317   31334   3674 13849   29    38   22  77%    907   -4   28   29   97%
c -  191.3    8318    52087    407537   31879   3685 13850   28    36   22  79%    958   -3   28   28  101%
c 
c [simplification-14] limit 426999 conflicts (hard 493953) hit after 444859 conflicts
c [quatres-10] found 7831 quaternary clauses 32% in total
c [quatres-10-2] added 7 single-self-subsuming ternary resolvents
c [quatres-10-2] added 9 quaternary resolvents
c [ternres-10] limit 47157686 with penalty 0 = 0 + 0
c [ternres-10] all 8318 free variables schedulable
c [ternres-10] 30 ternary resolvents (7 bin, 23 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1178942 penalty 3 = 3 + 0
c [gauss-4] extracted 1766 xors of average arity 3.0
c [gauss-4] connected 5298 occurrences of 445 variables (average 11.9)
c [gauss-4] limit 1178942 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 8318 free variables schedulable
c [simpleprobe-6] limit 188630745 penalty 0 = 0 + 0
c [decomp-55] removed 3 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 3 variables, found 3343 hbrs, 0 units
c [unhide-8] limit 2357884 with penalty 2 = 2 + 0
c [unhide-8-10] 0 units, 0 failed, 2040 tauts, 0 hbrs, 297133 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1297 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 8315 variables 100%
c [block-4] limit of 58947108 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 21 blocked clauses
c [block-4] 21 < 1/100 * 52079 = 520 considered unsuccessful
c [cce-9] limit of 117894216 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 13
c [cce-9-1] eliminated 3 clauses out of 27 (11%) of length 12
c [cce-9-1] eliminated 2 clauses out of 294 (1%) of length 11
c [cce-9-1] eliminated 5 clauses out of 198 (3%) of length 10
c [cce-9-1] eliminated 1 clauses out of 692 (0%) of length 9
c [cce-9-1] eliminated 8 clauses out of 783 (1%) of length 8
c [cce-9-1] eliminated 12 clauses out of 2769 (0%) of length 7
c [cce-9-1] eliminated 32 clauses out of 3685 (1%) of length 6
c [cce-9-1] eliminated 22 clauses out of 4137 (1%) of length 5
c [cce-9-1] eliminated 51 clauses out of 5838 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 137 large clauses in 27624541 steps
c [cce-9-1] allowing another 13812270 steps for small clauses
c [cce-9-1] scheduling 28329 clauses = 23612 binary + 4717 ternary
c [cce-9-1] tried to eliminate 28329 small clauses 100%
c [cce-9-1] eliminated 126 binary clauses 1%
c [cce-9-1] eliminated 24 ternary clauses 1%
c [cce-9-1] eliminated 150 small clauses 1%
c [cce-9-1] eliminated 150 small clauses in 60158381 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 287 covered clauses in round 1
c [cce-9-2] eliminated 2 clauses out of 193 (1%) of length 10
c [cce-9-2] eliminated 4 clauses out of 691 (1%) of length 9
c [cce-9-2] eliminated 1 clauses out of 2757 (0%) of length 7
c [cce-9-2] eliminated 3 clauses out of 3653 (0%) of length 6
c [cce-9-2] eliminated 1 clauses out of 4115 (0%) of length 5
c [cce-9-2] eliminated 3 clauses out of 5787 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 14 large clauses in 27343626 steps
c [cce-9-2] allowing another 13671813 steps for small clauses
c [cce-9-2] scheduling 28179 clauses = 23486 binary + 4693 ternary
c [cce-9-2] tried to eliminate 26864 small clauses 95%
c [cce-9-2] eliminated 3 binary clauses 0%
c [cce-9-2] eliminated 3 small clauses 0%
c [cce-9-2] eliminated 3 small clauses in 57735842 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 17 covered clauses in round 2
c [cce-9] eliminated 304 covered clauses in TOTAL during 2 rounds
c [cce-9] 304 < 1/100 * 52058 = 520 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 8314 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 107 variables 1% in round 1 in 10728698 steps
c [elim-12-1] backward subsumption/strengthening limit 10728600
c [elim-12-1-1] backward checking 710 touched variables 9%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 5 clauses in 778158 steps
c [elim-12-1] rescheduled 17 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 40997 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 107 = 1% variables out of 8314 scheduled
c [bca-10] limit of 10000000 steps and 103853 added (scaled 2)
c [bca-10] 8091 out of 16416 literals actually usable 49%
c [bca-10] added 5 blocked clauses in 64656 steps
c [sort-queue-14] sorted 970 enqueued variables after 444859 conflicts
c [score-dist-14] active 7237 (88%), one 0 (0%), zero 970 (12%)
c [score-dist-14] max exp 520, different 20 (4%)
c [score-dist-14] median active exp 513, avg 511.4
c [simplification-14] removed 111 variables 1.3% (8207 remain 16%)
c [simplification-14] removed 485 irredundant clauses 0.9% (51602 remain 25%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 66954 = 133908 / 2
c [simplification-14] new conflict interval 200862
c [simplification-14] penalized conflict interval 200862 = 1 * 200862
c [simplification-14] hard conflict limit 746152 (soft 645721 + delta 100431)
c [simplification-14] new conflict limit 645721 (hard 746152)
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 -  222.0    8207    51602    470719   32832   3584 13597   27    30   19  89%    999   -6   27   27  101%
c -  242.5    8207    51602    517621   33704   3592 13599   22    23   23  94%   1012   -8   20   25   79%
c -  262.8    8207    51602    564205   33737   3598 13599   21    24   23  90%   1018   -4   20   23   88%
c -  285.3    8207    51602    615149   33115   3605 13600   23    25   22  90%   1021   -0   21   22   96%
c 
c [simplification-15] limit 645721 conflicts (hard 746152) hit after 645721 conflicts
c [quatres-11] found 7841 quaternary clauses 32% in total
c [quatres-11-1] removed 4 duplicate quaternary clauses
c [quatres-11-2] added 5 single-self-subsuming ternary resolvents
c [quatres-11-2] added 108 quaternary resolvents
c [ternres-11] limit 73332458 with penalty 0 = 0 + 0
c [ternres-11] all 8207 free variables schedulable
c [ternres-11] 180 ternary resolvents (6 bin, 174 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2291639 penalty 4 = 4 + 0
c [card-5] found 1089 at-most-one constraints of average size 3.0
c [card-5] found 33 at-most-two constraints of average size 4.1
c [card-5] using previous limit 2291639 for elimination
c [card-5] 1122 out of 1122 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] generated 63 at-most-one constraints, 35 used 56%
c [card-5] exported 38 binary clauses, 1.1 per/constraint
c [treelook-6] limit 7333245 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 16412 literals 100%
c [treelook-6] scheduling used 326970 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 7333245 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 7333927 steps
c [treelook-6] 11897 literals remain 72%
c [treelook-6] 8003 variables remain to probed next time 98%
c [decomp-57] removed 13 variables
c [treelook-6] removed 15 variables, found 4221 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1073 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 8192 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 3 variables 0% in round 1 in 10688636 steps
c [elim-13-1] backward subsumption/strengthening limit 10688600
c [elim-13-1-1] backward checking 25 touched variables 0%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 0 clauses in 22968 steps
c [elim-13-1] rescheduled 3 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 2255 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 3 = 0% variables out of 8192 scheduled
c [elim-13] 3 < 1/100 * 8192 = 81 considered unsuccessful
c [bca-11] limit of 10000000 steps and 103759 added (scaled 2)
c [bca-11] 8071 out of 16380 literals actually usable 49%
c [bca-11] added 1 blocked clauses in 67992 steps
c [sweep-8] limit 5499934 penalty 2 = 2 + 0
c [sweep-8-1] 108 pos 34.2% + 208 neg 65.8% = 316 sched 3.9% ret 7873
c [sweep-8-1] 1116161 steps 165 queries 12.35 avg class size
c [sweep-8-1] 2373 decisions 163 SAT calls 39.40 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-58] removed 3 variables
c [sweep-8-1] removed 3 vars (0 failed, 2 eqs, 5 impls)
c [sweep-8-2] 2715 pos 33.2% + 5471 neg 66.8% = 8186 sched 100.0% ret 0
c [sweep-8-2] 4385512 steps 349 queries 89.30 avg class size
c [sweep-8-2] 7338 decisions 343 SAT calls 62.90 avg env size
c [sweep-8-2] 1870 variables remain 23% (6316 retained 77%)
c [decomp-59] removed 6 variables
c [sweep-8-2] removed 6 vars (0 failed, 6 eqs, 11 impls)
c [sweep-8] removed 9 vars in TOTAL (2 rounds, 512 queries)
c [sort-queue-15] sorted 875 enqueued variables after 645721 conflicts
c [score-dist-15] active 7305 (89%), one 0 (0%), zero 875 (11%)
c [score-dist-15] max exp 521, different 21 (4%)
c [score-dist-15] median active exp 513, avg 511.8
c [simplification-15] removed 27 variables 0.3% (8180 remain 16%)
c [simplification-15] removed 60 irredundant clauses 0.1% (51542 remain 25%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 200862
c [simplification-15] new conflict interval 401724
c [simplification-15] penalized conflict interval 401724 = 1 * 401724
c [simplification-15] hard conflict limit 1248307 (soft 1047445 + delta 200862)
c [simplification-15] new conflict limit 1047445 (hard 1248307)
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 -  311.6    8180    51542    670823   34169   3826 16703   20    26   16  78%   1023   -2   19   22   86%
c -  329.2    8180    51542    716231   34944   3863 16709   23    36   23  63%   1023    7   30   22  135%
c -  342.9    8180    51542    762790   35099   3901 16729   27    58   22  46%   1024   19   26   24  107%
c -  360.4    8180    51542    814245   35910   3913 16733   27    29   23  92%   1024   -9   28   26  106%
c -  381.7    8180    51542    870565   38533   3924 16733   22    28   23  78%   1024   -4   21   24   85%
c -  406.0    8180    51542    927687   38987   3934 16734   21    23   23  93%   1024   -5   22   22   99%
c -  424.3    8180    51542    979771   38766   3945 16743   26    28   23  93%   1024   -3   25   24  105%
c -  447.9    8180    51542   1038510   39510   3952 16744   25    28   24  90%   1024   -1   25   24  104%
c -  478.9    8180    51542   1110576   40520   3959 16744   22    24   24  89%   1024   -2   23   23  100%
c 
c [simplification-16] limit 1047445 conflicts (hard 1248307) hit after 1154861 conflicts
c [quatres-12] found 8149 quaternary clauses 31% in total
c [quatres-12-2] added 13 single-self-subsuming ternary resolvents
c [quatres-12-2] added 31 quaternary resolvents
c [ternres-12] limit 136866929 with penalty 0 = 0 + 0
c [ternres-12] all 8180 free variables schedulable
c [ternres-12] 80 ternary resolvents (8 bin, 72 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-60] removed 3 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 4336 sched 53%, 19 failed, 0 lifted, 610 hbrs
c [decomp-61] removed 27 variables
c [basicprobe-6-1] 4340 sched 53%, 3 failed, 0 lifted, 292 hbrs
c [decomp-62] removed 3 variables
c [basicprobe-6-2] 4327 sched 53%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-6-3] 4327 sched 53%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-6-4] 4327 sched 53%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-6-5] 4327 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-6] 4327 sched 53%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-6-7] 4327 sched 53%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-6-8] 4327 sched 53%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 22 units = 22 failed (100%) + 0 lifted (0%)
c [basicprobe-6-8] removed 30 variables, found 960 hbrs
c [bate-4] eliminated 16 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 767 transitive binary clauses
c [bca-12] limit of 10000000 steps and 103182 added (scaled 2)
c [bca-12] 7777 out of 16296 literals actually usable 48%
c [bca-12] added 3 blocked clauses in 85047 steps
c [sort-queue-16] sorted 859 enqueued variables after 1154861 conflicts
c [score-dist-16] active 7288 (89%), one 0 (0%), zero 859 (11%)
c [score-dist-16] max exp 522, different 22 (4%)
c [score-dist-16] median active exp 514, avg 512.3
c [simplification-16] removed 33 variables 0.4% (8147 remain 16%)
c [simplification-16] removed 277 irredundant clauses 0.5% (51265 remain 24%)
c [simplification-16] maximum reduction of 1% = max (0%, 1%)
c [simplification-16] geometric conflict interval increment 200862 = 401724 / 2
c [simplification-16] new conflict interval 602586
c [simplification-16] penalized conflict interval 602586 = 1 * 602586
c [simplification-16] hard conflict limit 2058740 (soft 1757447 + delta 301293)
c [simplification-16] new conflict limit 1757447 (hard 2058740)
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 -  503.1    8147    51265   1169915   39737   3985 16655   18    38   15  48%   1024   12   17   21   81%
c -  518.7    8147    51265   1211168   41785   3988 16656   18    20   24  91%   1024   -4   19   20   95%
c -  542.7    8147    51265   1269247   41940   3997 16657   20    22   25  95%   1024   -3   23   21  109%
c -  571.0    8147    51265   1333224   40328   4000 16657   18    19   25  93%   1024   -3   20   20  102%
c -  609.0    8147    51265   1416129   43166   4008 16661   14    29   28  49%   1024    9   13   18   72%
c -  630.3    8147    51265   1475312   42754   4021 16664   17    19   29  91%   1024   -3   18   18  100%
c -  659.0    8147    51265   1543010   42990   4030 16665   21    24   29  87%   1024    6   29   17  178%
c -  679.7    8147    51265   1595350   43976   4045 16667   25    28   29  91%   1024    4   25   21  121%
c -  705.0    8147    51265   1652503   42945   4048 16667   26    28   29  90%   1024    3   27   23  115%
c -  733.7    8147    51265   1716837   43643   4052 16667   21    23   30  92%   1024   -3   20   23   88%
c 
c [simplification-17] limit 1757447 conflicts (hard 2058740) hit after 1760600 conflicts
c [quatres-13] found 8225 quaternary clauses 31% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 5 single-self-subsuming ternary resolvents
c [quatres-13-2] added 18 quaternary resolvents
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] all 8147 free variables schedulable
c [ternres-13] 33 ternary resolvents (7 bin, 26 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-69] removed 1 variables
c [simpleprobe-7] all 8146 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-70] removed 4 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 4 variables, found 4096 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 1932 transitive binary clauses
c [cce-10] limit of 279797240 steps penalty 2 = 2 + 0
c [cce-10-1] eliminated 2 clauses out of 288 (1%) of length 11
c [cce-10-1] eliminated 2 clauses out of 189 (1%) of length 10
c [cce-10-1] eliminated 7 clauses out of 674 (1%) of length 9
c [cce-10-1] eliminated 3 clauses out of 772 (0%) of length 8
c [cce-10-1] eliminated 21 clauses out of 2732 (1%) of length 7
c [cce-10-1] eliminated 24 clauses out of 3646 (1%) of length 6
c [cce-10-1] eliminated 41 clauses out of 4113 (1%) of length 5
c [cce-10-1] eliminated 62 clauses out of 5855 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 162 large clauses in 25172115 steps
c [cce-10-1] allowing another 12586057 steps for small clauses
c [cce-10-1] scheduling 28302 clauses = 23100 binary + 5202 ternary
c [cce-10-1] tried to eliminate 28302 small clauses 100%
c [cce-10-1] eliminated 65 binary clauses 0%
c [cce-10-1] eliminated 130 ternary clauses 2%
c [cce-10-1] eliminated 195 small clauses 1%
c [cce-10-1] eliminated 195 small clauses in 57402934 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 357 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 12545395 steps for small clauses
c [cce-10-2] scheduling 28107 clauses = 23035 binary + 5072 ternary
c [cce-10-2] tried to eliminate 28107 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 357 covered clauses in TOTAL during 2 rounds
c [cce-10] 357 < 1/100 * 51249 = 512 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 8142 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 59 variables 1% in round 1 in 10557442 steps
c [elim-14-1] backward subsumption/strengthening limit 10557400
c [elim-14-1-1] backward checking 477 touched variables 6%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 2 clauses in 688041 steps
c [elim-14-1] rescheduled 13 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 64581 steps
c [elim-14-2] backward subsumption/strengthening limit 64500
c [elim-14-2-1] backward checking 9 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 26443 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 60 = 1% variables out of 8142 scheduled
c [elim-14] 60 < 1/100 * 8142 = 81 considered unsuccessful
c [bca-13] limit of 10000000 steps and 102189 added (scaled 2)
c [bca-13] 7586 out of 16166 literals actually usable 47%
c [bca-13] added 5 blocked clauses in 84068 steps
c [sweep-9] limit 33575668 penalty 1 = 1 + 0
c [sweep-9-1] 626 pos 34.0% + 1214 neg 66.0% = 1840 sched 22.8% ret 6242
c [sweep-9-1] 4512622 steps 497 queries 35.14 avg class size
c [sweep-9-1] 7415 decisions 494 SAT calls 44.05 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-71] removed 6 variables
c [sweep-9-1] removed 6 vars (0 failed, 5 eqs, 17 impls)
c [sweep-9-2] 2645 pos 32.8% + 5431 neg 67.2% = 8076 sched 100.0% ret 0
c [sweep-9-2] 8933663 steps 761 queries 32.75 avg class size
c [sweep-9-2] 13055 decisions 758 SAT calls 47.15 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-72] removed 6 variables
c [sweep-9-2] removed 6 vars (0 failed, 6 eqs, 19 impls)
c [sweep-9-3] 2642 pos 32.7% + 5428 neg 67.3% = 8070 sched 100.0% ret 0
c [sweep-9-3] 9204663 steps 761 queries 60.75 avg class size
c [sweep-9-3] 13151 decisions 753 SAT calls 60.44 avg env size
c [sweep-9-3] fully completed sweeping round
c [decomp-73] removed 11 variables
c [sweep-9-3] removed 11 vars (0 failed, 10 eqs, 24 impls)
c [sweep-9] removed 23 vars in TOTAL (3 rounds, 2016 queries)
c [sort-queue-17] sorted 713 enqueued variables after 1760600 conflicts
c [score-dist-17] active 7346 (91%), one 0 (0%), zero 713 (9%)
c [score-dist-17] max exp 522, different 22 (4%)
c [score-dist-17] median active exp 514, avg 512.6
c [simplification-17] removed 88 variables 1.1% (8059 remain 16%)
c [simplification-17] removed 554 irredundant clauses 1.1% (50711 remain 24%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 301293 = 602586 / 2
c [simplification-17] new conflict interval 903879
c [simplification-17] penalized conflict interval 903879 = 1 * 903879
c [simplification-17] hard conflict limit 3116418 (soft 2664479 + delta 451939)
c [simplification-17] new conflict limit 2664479 (hard 3116418)
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 -  773.5    8059    50711   1798274   45032   4218 18323   21    22   19  95%   1024   -1   20   22   89%
c -  803.8    8059    50711   1870458   47082   4220 18323   23    25   26  92%   1024    2   25   22  116%
c -  829.8    8059    50711   1931592   46581   4230 18325   22    24   26  91%   1024    1   21   21   99%
c -  858.2    8059    50711   1994389   45321   4234 18325   21    24   26  89%   1024    1   27   21  130%
c -  887.4    8059    50711   2057508   46743   4237 18326   22    25   26  89%   1024    0   23   22  105%
c -  908.5    8059    50711   2117604   45668   4255 18335   34    52   26  65%   1024   20   29   24  120%
c -  921.9    8059    50711   2171006   47024   4283 18340   22    40   37  56%   1024   -0   19   25   74%
c -  937.7    8059    50711   2227358   48707   4301 18343   28    34   37  82%   1024   -2   27   25  111%
c -  963.8    8059    50711   2291034   51353   4309 18343   32    37   38  85%   1024    4   26   27   98%
c -  991.7    8059    50711   2354337   51614   4315 18346   26    27   38  95%   1024   -5   26   27   97%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 153 basic ate = 74 trn 48% + 79 lrg 52% in 4 updates
c bcas: 13 count, 312 added (7 skipped), 843481 steps
c bkwd: tried 132796 clauses, 265461 lits, 2.00 lits/clause
c bkwd: checked 31150974 occs, 234.58 occs/clause, 117.35 occs/lit
c bkwd: subsumed 0 binary, 23 ternary, 26 large
c bkwd: strengthened 0 binary, 2 ternary (100% self), 243 large (0% self)
c blkd: 4 bces, 138 removed, 1126336 resolutions, 2966092 steps
c blkd: 2272 blocking literals 2%, 2 pure
c bump: 2377407 bumped seen, 928454729 lits 390.5 on average
c card: 5 count, 9 units, 39 am1, 15465692 steps
c card: 174 rescheduled, 1580 eliminated, 47672 resolved, 12043 subsumed
c card: 5038 at-most-one constraints found, average size 3.01
c card: 5038 at-most-one constraints used 100%, average size 3.01
c card: 33 at-most-two constraints found, average size 4.12
c card: 33 at-most-two constraints used 100%, average size 4.12
c cces: 10 cces, 11519 eliminated, 8704 ate 76%, 2815 abce 24%
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: 764685 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 109 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 73 decompositions, 15289 equivalent 29%
c deco: 78 decision-only clauses 0%, 72% reduction
c decs: 3878607 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 20842 eliminated 40%, 164 pure 1%
c elms: 36 rounds, 2.6 rounds/bve
c elms: 18417 small 88%, 2259 large 11%
c elms: 24613 tried small, 18417 succeeded 75%, 6196 failed 25%
c elms: 6349 subsumed, 20096 strengthened, 291 blocked
c elms: 4062179 copies, 5150970 resolutions, 501306 ipos
c elms: 2840749 subchks, 3655014 strchks
c gaus: 4 extractions, 8291 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9372848 steps, 4686424 extr 50%, 274004 elim 3%
c glue: 23.8 orig avg, 23.8 real avg, 4.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 76282 = 52694 simple 69% + 19071 trn 25% + 4517 lrg 6%, 1957 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2377406 clauses, 72.0 length
c lrnd: 171103774 lits = 541924019 orig - 370820245 removed 68%
c lrnd: 300943 uips 13%, 1832526 flips 77%
c mins: 2375156 mins 100%, 247 bin 0%, 1925 size 0%
c mins: 617683436 poisoned searches, 67651469 hits, 11% hit rate
c mins: 1089538641 used twice searches, 20686323 hits, 2% hit rate
c move: moved 7372, 6064 bin 82%, 1308 trn 18%
c otfs: 2090 driving 17%, 9945 restarting 83%
c otfs: str 12035, 11873 red 99%, 162 irr 1%
c otfs: str 12035, 0 bin 0%, 60 trn 0%, 11975 lrg 100%
c otfs: sub 79, 79 red 100%, 0 irr 0%
c otfs: sub 79, 0 bin 0%, 1 trn 1%, 78 lrg 99%
c phas: 8 computed, 12072 set, 0 pos (0%), 12072 neg (100%)
c prbs: 6 basic, 299672 probed, 214 failed, 22 lifted
c prbs: 7 simple, 192655 probed, 783 failed, 13524 eqs
c prbs: 6 treelook, 6858 probed, 7 failed, 0 lifted
c prom: 140034 locked 1% out of 24460946 tried
c prps: 2232476000 props, 569 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 13 count, 1830 quat, 151 self1, 1 self2, 98 dup
c queu: 17 sorted, 3878607 next (196020 steps 0.05)
c queu: 928553431 enq (1654610265 steps 1.78), 928454956 deq 100%
c redc: 5874 clauses 31%, 19091 tried 1%, 17 sat 0%
c redc: 10685 lits 5%, 200155 tried 0%, 17 sat 0%
c redc: 312 times jump level reduced, 10.8 levels on average
c reds: 41 count, 57925.3 conflicts per reduce
c reds: 0 memlim 0%, 41 arith 100%
c reds: 1435258 collected 92%, 129795 retired 8%
c rmbd: 7964 removed, 7539 red 95%
c rsts: 11506 restarts 83%, 2297 skipped 17%
c rsts: 2297 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 17 count, 17 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2377406 count (5886546 tried 2.5), 645662 sub out of 2375183 (27.2%)
c swps: 9 count, 14 rounds, 6277 queries (448.4/round)
c swps: 6137 sat calls, 41 unsat (0.7% success rate)
c swps: 106794 decisions 17.4, 4559 conflicts 0.7
c swps; 71.8 avg class size, 50.9 avg environment size
c swps: 0 failed, 357 impls, 175 equivs
c swp0: 2085 type 0 queries, 385 unsat (18.5%), 2047 sat (98.2%)
c swp1: 4192 type 1 queries, 1155 unsat (27.6%), 4055 sat (96.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 12512398 calls to obtain time
c tops: 8254 fixed 16%, 3 its, 791646.00 confs/it
c trds: 13 transitive reductions, 16489 removed, 5 failed
c trds: 206546 nodes, 464633 edges, 24501361 steps
c trim: 5047551 words, 19.3 MB
c trnr: 13 count, 318 bin, 5107 trn, 42101401 steps
c unhd: 8 count, 10 rounds, 8841871 steps
c unhd: 36 non-trivial sccs of average size 2.6
c unhd: 17 units, 17 bin, 0 trn, 0 lrg
c unhd: 42 failed, 41 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 7550 tauts, 66 bin 1%, 584 trn 8%, 196 lrg 3%
c unhd: 7550 tauts, 6704 stamp 89%, 6653 red 88%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 842063 str, 17 bin 0%, 941 trn 0%, 841105 lrg 100%, 833716 red 99%
c vars: 8059 remaining 15% and 44385 removed 85% out of 52444
c vars: 8254 fixed 16%, 20842 eliminated 40%, 15289 equivalent 29%
c vsts: 31367049576 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 14.1 search visits per propagation, 13117.8 per conflict
c wchs: 4300290171 pushed, 34159023 enlarged, 199 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2377013       1435258        129795     287065201     124912564       1580709
c 
c  0 0         12376   1       360   0         0   0 152348636  53  54255764  43    263133  17     0.3
c  1 5          4881   0       813   0      2264   2  28392841  10< 11417704   9     61997   4     0.1
c  2 6         21753   1      8242   1      7305   6  48746071  17  21725328  17<   171882  11     0.4
c  3 9        122574   5     72858   5     20254  16  34119347  12  19900000  16    348400  22<    4.7
c  4 14       684081  29    395286  28     55367  43< 16211722   6  11740404   9    440421  28    12.3
c  5 21      1081090  45<   670594  47<    34221  26   5859393   2   4788090   4    242731  15    14.4
c  6 30       357543  15    232847  16      7895   6   1165239   0    936948   1     44401   3     9.5
c  7 41        78355   3     47028   3      2010   2    191919   0    129929   0      6490   0     9.2
c  8 54        12561   1      6434   0       419   0     26098   0     16226   0      1090   0     1.7
c  9 69         1612   0       751   0        58   0      3492   0      1989   0       155   0     0.3
c 10 86          161   0        45   0         2   0       388   0       163   0         9   0     0.1
c 11 126          26   0         0   0         0   0        55   0        19   0         0   0     0.0
c 
c avg                  4.8           4.8           4.1           1.2           1.5           3.0
c std                  1.0           0.9           1.1           1.5           1.6           1.7
c 
c  181.815  18% bump
c   13.165   1% cce
c   13.102   1% probe
c    5.350   1% elim
c 
c   14.032 < 1% rest (below)
c 
c    4.550   0% unhide
c    3.811   0% sweep
c    2.127   0% decide
c    1.186   0% transred
c    0.701   0% bca
c    0.414   0% block
c    0.392   0% gauss
c    0.361   0% ternres
c    0.271   0% quatres
c    0.219   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.535   0% preprocessing     3%
c   44.030   4% inprocessing     97%
c ==================================
c   45.565   5% simplifying
c  954.360  95% search
c ==================================
c  999.926 100% all
c 
c       2374938 conflicts,        2375.1 confs/sec
c          1115 ternaries,        2130.0 confs/ternary
c           362 binaries,         6560.6 confs/binary
c             3 iterations,     791646.0 confs/iteration
c 
c            41 reductions,          0.0 redus/sec,  57925.3 confs/reduction
c         11506 restarts,           11.5 rests/sec,    206.4 confs/restart
c       3878607 decisions,        3878.9 decis/sec,      1.6 decis/conflict
c    2232476000 propagations,  2232640.9 props/sec,    575.6 props/decision
c 
c 999.9 seconds, 70.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
