c launch: /data/cnf/sc2014/app/6s11-opt.cnf.bz2
c host: atom25
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/6s11-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s11-opt.cnf.bz2
c no embedded options
c found 'p cnf 33279 97312' header
c read 33279 variables, 97312 clauses, 227060 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=2
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 33275 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] VMTF (--score=2)
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   33275    97311         0       0      0     0    0     0    5   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 33275 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 957 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 957 variables, found 1677 hbrs, 84 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 1 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 32318 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 23568 variables 73% in round 1 in 6707541 steps
c [elim-1-1] backward subsumption/strengthening limit 6707500
c [elim-1-1-1] backward checking 23181 touched variables 72%
c [elim-1-1-1] incomplete backward checking 23158 remain 100%
c [elim-1-1] subsumed 2 and strengthened 83 clauses in 6707846 steps
c [elim-1-1] rescheduled 202 variables 1% by backward subsumption
c [elim-1-2] eliminated 3 variables 0% in round 2 in 177080 steps
c [elim-1-2] backward subsumption/strengthening limit 177000
c [elim-1-2-1] backward checking 23163 touched variables 72%
c [elim-1-2-1] incomplete backward checking 23040 remain 99%
c [elim-1-2] subsumed 3 and strengthened 63 clauses in 178371 steps
c [elim-1-2] rescheduled 102 variables 0% by backward subsumption
c [elim-1-3] eliminated 1 variables 0% in round 3 in 134938 steps
c [elim-1-3] backward subsumption/strengthening limit 134900
c [elim-1-3-1] backward checking 23046 touched variables 71%
c [elim-1-3-1] incomplete backward checking 22910 remain 99%
c [elim-1-3] subsumed 0 and strengthened 55 clauses in 134971 steps
c [elim-1] incomplete 74 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 23572 = 73% variables out of 32318 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 42967 negative 89.1% of 48241 except 5274 10.9%
c [phase-count-1] 40636 positive 84.2% of 48241 except 7605 15.8%
c [phase-1] phase bias: 2347 positive 27%, 6399 negative 73%
c [sort-queue-1] sorted 8746 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 8746 (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 24529 variables 73.7% (8746 remain 26%)
c [simplification-1] removed 49070 irredundant clauses 50.4% (48241 remain 50%)
c [simplification-1] maximum reduction of 74% = max (74%, 50%)
c [simplification-1] large reduction 74% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  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    1.0    8745    48241       659     494     73    47    1    23    6   3%      3   23    5    0 8882%
c i    1.1    8744    48241       919     641    114    53    1    28    6   3%      3   28    4    0 6671%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 8 variables
c [simpleprobe-2] all 8738 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 1835 variables remain 21% (6900 retained 79%)
c [simpleprobe-2] removed 3 variables, found 679 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 17470 literals 100%
c [treelook-1] scheduling used 204477 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 305254 steps
c [treelook-1] 17365 literals remain 99%
c [treelook-1] 8735 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 1842 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 3621 probes remain 41% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 3941 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 8734 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 163 variables 2% in round 1 in 7362835 steps
c [elim-2-1] backward subsumption/strengthening limit 7362800
c [elim-2-1-1] backward checking 1388 touched variables 16%
c [elim-2-1-1] incomplete backward checking 1426 remain 103%
c [elim-2-1] subsumed 0 and strengthened 31 clauses in 7363888 steps
c [elim-2-1] rescheduled 77 variables 1% by backward subsumption
c [elim-2-2] eliminated 1 variables 0% in round 2 in 221148 steps
c [elim-2-2] backward subsumption/strengthening limit 221100
c [elim-2-2-1] backward checking 1431 touched variables 16%
c [elim-2-2-1] incomplete backward checking 855 remain 60%
c [elim-2-2] subsumed 20 and strengthened 1 clauses in 221181 steps
c [elim-2-2] rescheduled 46 variables 1% by backward subsumption
c [elim-2-3] eliminated 19 variables 0% in round 3 in 30511 steps
c [elim-2-3] backward subsumption/strengthening limit 30500
c [elim-2-3-1] backward checking 895 touched variables 10%
c [elim-2-3-1] incomplete backward checking 851 remain 95%
c [elim-2-3] subsumed 2 and strengthened 24 clauses in 30513 steps
c [elim-2] incomplete 54 not tried 1% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 183 = 2% variables out of 8734 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 8551 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 3789 (44%), zero 4762 (56%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 193 variables 2.2% (8551 remain 26%)
c [simplification-2] removed 447 irredundant clauses 0.9% (47794 remain 49%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17666 (soft 7666 + delta 10000)
c [simplification-2] new conflict limit 7666 (hard 17666)
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    2.3    8550    47792      5482    4252    481  6179    4    89    6   5%     54   85    6    0 1432%
c i    2.3    8549    47792      5483    4252    481  6179    4    89    6   5%     54   85    6    0 1426%
c i    2.6    8548    47792      7230    5642    637  6208    5   107    6   5%     22  101    5    1  925%
c i    2.6    8547    47792      7493    5865    657  6209    5   106    6   5%     17   99    6    1 1013%
c 
c [simplification-3] limit 7676 conflicts (hard 17666) hit after 7676 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 207 at-most-one constraints of average size 3.0
c [card-2] found 6 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 213 out of 213 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 25 at-most-one constraints, 21 used 84%
c [card-2] exported 21 binary clauses, 1.0 per/constraint
c [decomp-6] removed 27 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 3 units, 0 failed, 742 tauts, 0 hbrs, 3337 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 8521 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 59 variables 1% in round 1 in 8767925 steps
c [elim-3-1] backward subsumption/strengthening limit 8767900
c [elim-3-1-1] backward checking 583 touched variables 7%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 3 and strengthened 19 clauses in 7879084 steps
c [elim-3-1] rescheduled 51 variables 1% by backward subsumption
c [elim-3-2] eliminated 3 variables 0% in round 2 in 221696 steps
c [elim-3-2] backward subsumption/strengthening limit 221600
c [elim-3-2-1] backward checking 22 touched variables 0%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 2 and strengthened 12 clauses in 28028 steps
c [elim-3-2] rescheduled 22 variables 0% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 18531 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 62 = 1% variables out of 8521 scheduled
c [elim-3] 62 < 1/100 * 8521 = 85 considered unsuccessful
c [sort-queue-3] sorted 8459 enqueued variables after 7676 conflicts
c [score-dist-3] active 0 (0%), one 6786 (80%), zero 1673 (20%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 88 variables 1.0% (8459 remain 25%)
c [simplification-3] removed 265 irredundant clauses 0.6% (47527 remain 49%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 16666
c [simplification-3] penalized conflict interval 16666 = 1 * 16666
c [simplification-3] hard conflict limit 34342 (soft 24342 + delta 10000)
c [simplification-3] new conflict limit 24342 (hard 34342)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.6    8458    47527     10989    8561    870  5362    6   114    6   5%     36  102    6    1  670%
c i    4.1    8457    47527     14401   11360   1101  5396    6   114    7   5%     35   97    6    1  546%
c i    4.1    8456    47527     14610   11549   1105  5403    6   115    7   6%     28   97    7    1  603%
c i    4.2    8455    47527     15655   12461   1152  5406    6   111    7   6%     13   92    7    1  556%
c i    4.6    8454    47527     18759   15109   1305  5436    7   110    7   6%     28   87    8    2  504%
c 
c [simplification-4] limit of 201 binary hit after 201 binaries
c [decomp-7] removed 30 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 11834 literals 70%
c [treelook-2] scheduling used 150028 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 154060 steps
c [treelook-2] 11821 literals remain 70%
c [treelook-2] 7549 variables remain to probed next time 90%
c [treelook-2] removed 0 variables, found 331 hbrs
c [unhide-3] limit 145700 with penalty 0 = 0 + 0
c [unhide-3-3] 4 units, 0 failed, 64 tauts, 0 hbrs, 4994 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 8425 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 1638 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 36 (6%) of length 15
c [cce-1-1] eliminated 3 clauses out of 22 (14%) of length 14
c [cce-1-1] eliminated 2 clauses out of 107 (2%) of length 10
c [cce-1-1] eliminated 10 clauses out of 185 (5%) of length 9
c [cce-1-1] eliminated 50 clauses out of 417 (12%) of length 8
c [cce-1-1] eliminated 106 clauses out of 896 (12%) of length 7
c [cce-1-1] eliminated 213 clauses out of 2140 (10%) of length 6
c [cce-1-1] eliminated 362 clauses out of 3902 (9%) of length 5
c [cce-1-1] eliminated 371 clauses out of 9339 (4%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1119 large clauses in 30000024 steps
c [cce-1-1] allowing another 15000012 steps for small clauses
c [cce-1-1] scheduling 22484 clauses = 8205 binary + 14279 ternary
c [cce-1-1] tried to eliminate 12169 small clauses 54%
c [cce-1-1] eliminated 45 binary clauses 1%
c [cce-1-1] eliminated 351 ternary clauses 2%
c [cce-1-1] eliminated 396 small clauses 2%
c [cce-1-1] eliminated 396 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1515 covered clauses in round 1
c [cce-1] eliminated 1515 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 88904 added (scaled 2)
c [bca-1] 5596 out of 16852 literals actually usable 33%
c [bca-1] added 5 blocked clauses in 29002 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3431 pos 40.7% + 4994 neg 59.3% = 8425 sched 100.0% ret 0
c [sweep-1-1] 1004557 steps 51 queries 595.24 avg class size
c [sweep-1-1] 1371 decisions 46 SAT calls 57.20 avg env size
c [sweep-1-1] 7512 variables remain 89% (913 retained 11%)
c [decomp-9] removed 7 variables
c [sweep-1-1] removed 7 vars (0 failed, 4 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 7 vars in TOTAL (1 rounds, 50 queries)
c [sort-queue-4] sorted 8418 enqueued variables after 20005 conflicts
c [score-dist-4] active 0 (0%), one 7960 (95%), zero 458 (5%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 36 variables 0.4% (8418 remain 25%)
c [simplification-4] removed 3325 irredundant clauses 7.0% (44202 remain 45%)
c [simplification-4] maximum reduction of 7% = max (0%, 7%)
c [simplification-4] forced so keeping old conflict interval 16666
c [simplification-4] conflict limit remains at 24342 (hard 34342)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 24342 conflicts (hard 34342) hit after 24342 conflicts
c [quatres-1] found 10943 quaternary clauses 48% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 2 double-self-subsuming ternary resolvents
c [quatres-1-2] added 133 single-self-subsuming ternary resolvents
c [quatres-1-2] added 911 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 8418 free variables schedulable
c [ternres-1] 5763 ternary resolvents (62 bin, 5701 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4596 xors of average arity 3.0
c [gauss-1] connected 13792 occurrences of 965 variables (average 14.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-10] removed 8 variables
c [gauss-1] exported 1 unary, 0 binary and 9 ternary equations
c [basicprobe-2] limit 4422113 penalty 0 = 0 + 0
c [basicprobe-2-0] 3557 sched 42%, 15 failed, 0 lifted, 8588 hbrs
c [decomp-12] removed 65 variables
c [basicprobe-2-1] 4660 probes remain 56% after last round
c [basicprobe-2-1] 15 units = 15 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 65 variables, found 8720 hbrs
c [bate-1] eliminated 9 asymmetric tautologies during probing
c [unhide-4] limit 176884 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 0 failed, 1648 tauts, 0 hbrs, 6908 literals
c [transred-1] limit 884422 with penalty 0 = 0 + 0
c [transred-1] removed 250 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 8344 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 155 blocked clauses
c [block-2] 155 < 1/100 * 44024 = 440 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 360 (1%) of length 8
c [cce-2-1] eliminated 2 clauses out of 1915 (0%) of length 6
c [cce-2-1] eliminated 4 clauses out of 3505 (0%) of length 5
c [cce-2-1] eliminated 162 clauses out of 8845 (2%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 170 large clauses in 29659094 steps
c [cce-2-1] allowing another 14829547 steps for small clauses
c [cce-2-1] scheduling 21831 clauses = 8146 binary + 13685 ternary
c [cce-2-1] tried to eliminate 989 small clauses 5%
c [cce-2-1] eliminated 3 binary clauses 0%
c [cce-2-1] eliminated 16 ternary clauses 0%
c [cce-2-1] eliminated 19 small clauses 0%
c [cce-2-1] eliminated 19 small clauses in 30000020 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 189 covered clauses in round 1
c [cce-2] eliminated 189 covered clauses in TOTAL during 1 rounds
c [cce-2] 189 < 1/100 * 43866 = 438 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 8333 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 200000000 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 533 variables 6% in round 1 in 8956634 steps
c [elim-4-1] backward subsumption/strengthening limit 8956600
c [elim-4-1-1] backward checking 2572 touched variables 31%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 4 and strengthened 22 clauses in 2704662 steps
c [elim-4-1] rescheduled 72 variables 1% by backward subsumption
c [elim-4-2] eliminated 1 variables 0% in round 2 in 1180275 steps
c [elim-4-2] backward subsumption/strengthening limit 1180200
c [elim-4-2-1] backward checking 9 touched variables 0%
c [elim-4-2-1] incomplete backward checking 7 remain 78%
c [elim-4-2] subsumed 0 and strengthened 2 clauses in 1181171 steps
c [elim-4-2] rescheduled 5 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 2014 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 534 = 6% variables out of 8333 scheduled
c [bca-2] limit of 10000000 steps and 86668 added (scaled 2)
c [bca-2] 4556 out of 15600 literals actually usable 29%
c [bca-2] added 7 blocked clauses in 29165 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2937 pos 42.3% + 4005 neg 57.7% = 6942 sched 89.0% ret 857
c [sweep-2-1] 1012650 steps 85 queries 326.44 avg class size
c [sweep-2-1] 1829 decisions 77 SAT calls 55.65 avg env size
c [sweep-2-1] 5726 variables remain 73% (2073 retained 27%)
c [decomp-13] removed 21 variables
c [sweep-2-1] removed 21 vars (0 failed, 8 eqs, 14 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 21 vars in TOTAL (1 rounds, 84 queries)
c [sort-queue-5] sorted 7778 enqueued variables after 24342 conflicts
c [score-dist-5] active 0 (0%), one 7563 (97%), zero 215 (3%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 640 variables 7.6% (7778 remain 23%)
c [simplification-5] removed 1132 irredundant clauses 2.6% (43070 remain 44%)
c [simplification-5] maximum reduction of 8% = max (8%, 3%)
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 36342 (soft 26342 + delta 10000)
c [simplification-5] new conflict limit 26342 (hard 36342)
c 
c [simplification-6] limit 26342 conflicts (hard 36342) hit after 26342 conflicts
c [quatres-2] found 11403 quaternary clauses 47% in total
c [quatres-2-1] removed 10 duplicate quaternary clauses
c [quatres-2-2] added 75 single-self-subsuming ternary resolvents
c [quatres-2-2] added 573 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7778 free variables schedulable
c [ternres-2] 1169 ternary resolvents (57 bin, 1112 trn)
c [ternres-2] 1 variables remain 0% (7777 retained 100%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 196 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] 196 out of 196 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 4506 xors of average arity 3.0
c [gauss-2] connected 13494 occurrences of 906 variables (average 14.9)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 14 variables
c [simpleprobe-3] 1571 schedulable variables 20%
c [simpleprobe-3] limit 3858831 penalty 0 = 0 + 0
c [decomp-15] removed 34 variables
c [simpleprobe-3] 384 variables remain 5% (7346 retained 95%)
c [simpleprobe-3] removed 34 variables, found 1738 hbrs, 1 units
c [unhide-5] limit 192941 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 173 tauts, 0 hbrs, 2413 literals
c [transred-2] limit 964707 with penalty 0 = 0 + 0
c [transred-2] removed 563 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 7730 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 37 variables 0% in round 1 in 10941609 steps
c [elim-5-1] backward subsumption/strengthening limit 9058391
c [elim-5-1-1] backward checking 261 touched variables 3%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 4 clauses in 769230 steps
c [elim-5-1] rescheduled 21 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 9057 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 37 = 0% variables out of 7730 scheduled
c [elim-5] 37 < 1/100 * 7730 = 77 considered unsuccessful
c [bca-3] limit of 10000000 steps and 85956 added (scaled 2)
c [bca-3] 4135 out of 15388 literals actually usable 27%
c [bca-3] added 0 blocked clauses in 30026 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2428 pos 43.0% + 3212 neg 57.0% = 5640 sched 73.3% ret 2053
c [sweep-3-1] 1007718 steps 75 queries 354.36 avg class size
c [sweep-3-1] 1525 decisions 74 SAT calls 47.04 avg env size
c [sweep-3-1] 4921 variables remain 64% (2772 retained 36%)
c [decomp-16] removed 9 variables
c [sweep-3-1] removed 9 vars (0 failed, 6 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 9 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-6] sorted 7684 enqueued variables after 26342 conflicts
c [score-dist-6] active 0 (0%), one 7480 (97%), zero 204 (3%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 94 variables 1.2% (7684 remain 23%)
c [simplification-6] removed 352 irredundant clauses 0.8% (42718 remain 44%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 26666
c [simplification-6] penalized conflict interval 26666 = 1 * 26666
c [simplification-6] hard conflict limit 66341 (soft 53008 + delta 13333)
c [simplification-6] new conflict limit 53008 (hard 66341)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.1    7683    42718     26838   20912   7993 12611    8   120    9   6%     99   86    7    2  331%
c i    9.1    7682    42718     26866   20931   7996 12612    8   120    9   6%     96   86    7    2  313%
c i    9.2    7681    42718     27279   21277   8017 12616    7   120    9   6%     61   86    7    2  301%
c i    9.7    7680    42718     31616   25079   8152 12639    7   107    9   7%     39   68    7    3  270%
c i    9.7    7679    42718     31723   25166   8157 12640    7   106    9   7%     34   67    7    3  268%
c i   10.1    7678    42718     34419   27597   8237 12650    8   101    9   7%     17   59    7    3  247%
c i   11.0    7677    42718     40684   33216   8379 12682    8   106   10   7%     65   58    7    3  221%
c i   11.3    7676    42718     43042   35336   8449 12686    8   106   10   7%     13   57    8    3  235%
c i   11.7    7675    42718     46281   38199   8499 12695    8   102   11   8%     19   50    8    4  216%
c 
c [simplification-7] limit 53008 conflicts (hard 66341) hit after 53008 conflicts
c [quatres-3] found 12983 quaternary clauses 43% in total
c [quatres-3-1] removed 4 duplicate quaternary clauses
c [quatres-3-1] added 3 double-self-subsuming ternary resolvents
c [quatres-3-2] added 122 single-self-subsuming ternary resolvents
c [quatres-3-2] added 360 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 1 schedulable variables 0%
c [ternres-3] 901 ternary resolvents (2 bin, 899 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-17] removed 27 variables
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 657 transitive binary clauses
c [transred-3] found 9 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 7648 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 88 blocked clauses
c [block-3] 88 < 1/100 * 42656 = 426 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 13219 clauses = 7280 binary + 5939 ternary
c [cce-3-1] tried to eliminate 2071 small clauses 16%
c [cce-3-1] eliminated 21 binary clauses 0%
c [cce-3-1] eliminated 72 ternary clauses 1%
c [cce-3-1] eliminated 93 small clauses 1%
c [cce-3-1] eliminated 93 small clauses in 15000046 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 93 covered clauses in round 1
c [cce-3] eliminated 93 covered clauses in TOTAL during 1 rounds
c [cce-3] 93 < 1/100 * 42524 = 425 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2049 pos 42.0% + 2833 neg 58.0% = 4882 sched 63.9% ret 2755
c [sweep-4-1] 1040841 steps 54 queries 417.93 avg class size
c [sweep-4-1] 1178 decisions 48 SAT calls 52.44 avg env size
c [sweep-4-1] 4503 variables remain 59% (3132 retained 41%)
c [decomp-18] removed 14 variables
c [sweep-4-1] removed 14 vars (0 failed, 10 eqs, 12 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 14 vars in TOTAL (1 rounds, 53 queries)
c [sort-queue-7] sorted 7623 enqueued variables after 53008 conflicts
c [score-dist-7] active 0 (0%), one 7596 (100%), zero 27 (0%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 52 variables 0.7% (7623 remain 23%)
c [simplification-7] removed 315 irredundant clauses 0.7% (42403 remain 44%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-7] new conflict interval 39999
c [simplification-7] penalized conflict interval 39999 = 1 * 39999
c [simplification-7] hard conflict limit 113006 (soft 93007 + delta 19999)
c [simplification-7] new conflict limit 93007 (hard 113006)
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   15.6    7622    42403     59924   50162   9497 12055    8   102   13   8%    164   41    8    4  188%
c i   16.0    7621    42403     62456   52442   9550 12065    8    94   13   9%      7   32    8    5  165%
c i   16.4    7620    42403     64713   54455   9609 12078    8    94   13   9%     -9   30    7    5  159%
c i   16.6    7619    42403     65603   55217   9629 12080    8    90   13   9%    -19   26    8    5  165%
c i   16.8    7618    42403     66969   56421   9663 12086    8    93   13   9%    -20   29    8    5  167%
c i   18.4    7617    42403     75658   64267   9821 12116    8    95   14   9%     83   27    9    5  172%
c i   18.5    7616    42403     75856   64441   9827 12119    8    95   14   9%     62   27    8    5  153%
c i   19.1    7615    42403     79025   67315   9892 12139    9    94   14   9%      2   25   10    5  176%
c -   19.4    7615    42403     80276   29058   9909 12145    8    89   10   9%    -17   20    9    5  163%
c i   20.2    7614    42403     85696   33973  10013 12173    8    90   10   9%     50   19    8    6  134%
c i   21.0    7613    42402     90755   38626  10103 12194    8    87   11   9%     25   15    8    6  143%
c 
c [simplification-8] limit of 30 iterations hit after 30 iterations
c [quatres-4] found 14469 quaternary clauses 39% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 4 double-self-subsuming ternary resolvents
c [quatres-4-2] added 126 single-self-subsuming ternary resolvents
c [quatres-4-2] added 421 quaternary resolvents
c [ternres-4] limit 4235147 with penalty 0 = 0 + 0
c [ternres-4] all 7613 free variables schedulable
c [ternres-4] 2018 ternary resolvents (50 bin, 1968 trn)
c [ternres-4] 3 variables remain 0% (7610 retained 100%)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 2277 xors of average arity 3.0
c [gauss-3] connected 6764 occurrences of 887 variables (average 7.6)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-19] removed 30 variables
c [unhide-6] limit 423514 with penalty 1 = 1 + 0
c [unhide-6-6] 0 units, 1 failed, 1423 tauts, 0 hbrs, 14780 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 430 transitive binary clauses
c [transred-4] found 3 units
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 7579 variables 100%
c [elim-6] limit of 42351479 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 86 variables 1% in round 1 in 10794494 steps
c [elim-6-1] backward subsumption/strengthening limit 10794400
c [elim-6-1-1] backward checking 515 touched variables 7%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 3 and strengthened 9 clauses in 811799 steps
c [elim-6-1] rescheduled 28 variables 0% by backward subsumption
c [elim-6-2] eliminated 5 variables 0% in round 2 in 98057 steps
c [elim-6-2] backward subsumption/strengthening limit 98000
c [elim-6-2-1] backward checking 41 touched variables 1%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 1 and strengthened 3 clauses in 70390 steps
c [elim-6-2] rescheduled 6 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 22856 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 91 = 1% variables out of 7579 scheduled
c [bca-4] limit of 10000000 steps and 83986 added (scaled 2)
c [bca-4] 2200 out of 14978 literals actually usable 15%
c [bca-4] added 18 blocked clauses in 41807 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12705440 penalty 0 = 0 + 0
c [sweep-5-1] 2004 pos 45.3% + 2418 neg 54.7% = 4422 sched 59.1% ret 3066
c [sweep-5-1] 12707437 steps 828 queries 51.62 avg class size
c [sweep-5-1] 12487 decisions 724 SAT calls 44.73 avg env size
c [sweep-5-1] 193 variables remain 3% (7289 retained 97%)
c [decomp-20] removed 323 variables
c [sweep-5-1] removed 323 vars (0 failed, 309 eqs, 240 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 323 vars in TOTAL (1 rounds, 827 queries)
c [sort-queue-8] sorted 7165 enqueued variables after 90755 conflicts
c [score-dist-8] active 0 (0%), one 7157 (100%), zero 8 (0%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 448 variables 5.9% (7165 remain 22%)
c [simplification-8] removed 911 irredundant clauses 2.1% (41491 remain 43%)
c [simplification-8] maximum reduction of 6% = max (6%, 2%)
c [simplification-8] forced so keeping old conflict interval 39999
c [simplification-8] conflict limit remains at 93007 (hard 113006)
c [simplification-8] new iteration interval 100
c 
c [simplification-9] limit 93007 conflicts (hard 113006) hit after 94007 conflicts
c [quatres-5] found 14731 quaternary clauses 40% in total
c [quatres-5-1] removed 44 duplicate quaternary clauses
c [quatres-5-1] added 13 double-self-subsuming ternary resolvents
c [quatres-5-2] added 168 single-self-subsuming ternary resolvents
c [quatres-5-2] added 290 quaternary resolvents
c [ternres-5] limit 4411645 with penalty 0 = 0 + 0
c [ternres-5] 3 schedulable variables 0%
c [ternres-5] 1637 ternary resolvents (49 bin, 1588 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-21] removed 18 variables
c [treelook-3] limit 110291 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 6410 literals 45%
c [treelook-3] scheduling used 110349 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 110291 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 116253 steps
c [treelook-3] 6405 literals remain 45%
c [treelook-3] 5065 variables remain to probed next time 71%
c [treelook-3] removed 0 variables, found 50 hbrs
c [unhide-7] limit 882329 with penalty 0 = 0 + 0
c [unhide-7-8] 0 units, 28 failed, 1123 tauts, 0 hbrs, 9414 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 329 transitive binary clauses
c [transred-5] found 5 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 7133 variables 100%
c [elim-7] limit of 88232917 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 189 variables 3% in round 1 in 10449815 steps
c [elim-7-1] backward subsumption/strengthening limit 10449800
c [elim-7-1-1] backward checking 774 touched variables 11%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 7 and strengthened 10 clauses in 922975 steps
c [elim-7-1] rescheduled 61 variables 1% by backward subsumption
c [elim-7-2] eliminated 7 variables 0% in round 2 in 384000 steps
c [elim-7-2] backward subsumption/strengthening limit 384000
c [elim-7-2-1] backward checking 43 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 2 and strengthened 0 clauses in 31767 steps
c [elim-7-2] rescheduled 11 variables 0% by backward subsumption
c [elim-7-3] eliminated 2 variables 0% in round 3 in 26436 steps
c [elim-7-3] backward subsumption/strengthening limit 26400
c [elim-7-3-1] backward checking 20 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 1 clauses in 26401 steps
c [elim-7] incomplete 6 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 198 = 3% variables out of 7133 scheduled
c [bca-5] limit of 10000000 steps and 80095 added (scaled 2)
c [bca-5] 1963 out of 13872 literals actually usable 14%
c [bca-5] added 23 blocked clauses in 42390 steps
c [sweep-6] limit 1323493 penalty 0 = 0 + 0
c [sweep-6-1] 78 pos 50.3% + 77 neg 49.7% = 155 sched 2.2% ret 6780
c [sweep-6-1] 927903 steps 95 queries 12.05 avg class size
c [sweep-6-1] 1314 decisions 100 SAT calls 30.51 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-23] removed 34 variables
c [sweep-6-1] removed 34 vars (0 failed, 25 eqs, 9 impls)
c [sweep-6-2] 2960 pos 42.9% + 3941 neg 57.1% = 6901 sched 100.0% ret 0
c [sweep-6-2] 430689 steps 30 queries 569.23 avg class size
c [sweep-6-2] 742 decisions 26 SAT calls 58.27 avg env size
c [sweep-6-2] 6554 variables remain 95% (347 retained 5%)
c [decomp-24] removed 5 variables
c [sweep-6-2] removed 5 vars (0 failed, 4 eqs, 7 impls)
c [sweep-6] removed 39 vars in TOTAL (2 rounds, 123 queries)
c [sort-queue-9] sorted 6896 enqueued variables after 94007 conflicts
c [score-dist-9] active 0 (0%), one 6888 (100%), zero 8 (0%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 269 variables 3.8% (6896 remain 21%)
c [simplification-9] removed 1747 irredundant clauses 4.2% (39740 remain 41%)
c [simplification-9] maximum reduction of 4% = max (4%, 4%)
c [simplification-9] geometric conflict interval increment 7999 = 39999 / 5
c [simplification-9] new conflict interval 47998
c [simplification-9] penalized conflict interval 47998 = 1 * 47998
c [simplification-9] hard conflict limit 166004 (soft 142005 + delta 23999)
c [simplification-9] new conflict limit 142005 (hard 166004)
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   24.6    6895    39735     99887   43158  10329 10146    8    80   11  10%     85    7    7    6  121%
c i   24.7    6893    39735    100319   43539  10338 10150    8    82   11   9%     42    9    8    6  125%
c i   24.7    6892    39735    100329   43546  10339 10150    8    83   11   9%     41    9    8    6  124%
c i   25.0    6891    39735    102391   45394  10382 10160    8    90   11   9%    -13   16   10    6  158%
c i   27.1    6890    39735    116100   58136  10505 10182    8    73   13  11%    145   -1    8    6  128%
c i   27.1    6889    39735    116104   58138  10505 10182    8    73   13  11%    145   -1    8    6  127%
c -   30.5    6889    39733    138073   41888  10731 10220    8    66   16  12%    240   -7    9    7  128%
c i   31.0    6888    39733    141639   45242  10746 10222    8    59   18  14%    282  -14    8    7  113%
c i   31.3    6887    39733    144596   48013  10771 10226    8    60   18  13%    -51  -12    8    7  115%
c 
c [simplification-10] limit 142008 conflicts (hard 166004) hit after 162061 conflicts
c [quatres-6] found 15562 quaternary clauses 33% in total
c [quatres-6-1] removed 22 duplicate quaternary clauses
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 188 single-self-subsuming ternary resolvents
c [quatres-6-2] added 363 quaternary resolvents
c [ternres-6] limit 7503018 with penalty 0 = 0 + 0
c [ternres-6] all 6887 free variables schedulable
c [ternres-6] 3168 ternary resolvents (92 bin, 3076 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 468938 penalty 3 = 3 + 0
c [card-4] found 157 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 468938 for elimination
c [card-4] 157 out of 157 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-25] removed 33 variables
c [basicprobe-3] limit 37515090 penalty 0 = 0 + 0
c [basicprobe-3-0] 3902 sched 57%, 27 failed, 0 lifted, 6727 hbrs
c [decomp-26] removed 62 variables
c [basicprobe-3-1] 3998 sched 59%, 3 failed, 0 lifted, 607 hbrs
c [decomp-27] removed 6 variables
c [basicprobe-3-2] 3991 sched 59%, 0 failed, 0 lifted, 45 hbrs
c [basicprobe-3-3] 3993 sched 59%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-3-4] 3991 sched 59%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-3-5] 416 probes remain 6% after last round
c [basicprobe-3-5] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 68 variables, found 7401 hbrs
c [bate-2] eliminated 12 asymmetric tautologies during probing
c [unhide-8] limit 1500603 with penalty 0 = 0 + 0
c [unhide-8-10] 0 units, 0 failed, 1774 tauts, 0 hbrs, 38161 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 272 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6795 variables 100%
c [block-4] limit of 18757545 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 79 blocked clauses
c [block-4] 79 < 1/100 * 39381 = 393 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 93787725 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 9 clauses out of 51 (18%) of length 11
c [cce-4-1] eliminated 9 clauses out of 122 (7%) of length 10
c [cce-4-1] eliminated 11 clauses out of 221 (5%) of length 9
c [cce-4-1] eliminated 47 clauses out of 458 (10%) of length 8
c [cce-4-1] eliminated 97 clauses out of 997 (10%) of length 7
c [cce-4-1] eliminated 116 clauses out of 1930 (6%) of length 6
c [cce-4-1] eliminated 189 clauses out of 3640 (5%) of length 5
c [cce-4-1] eliminated 361 clauses out of 8241 (4%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 839 large clauses in 29032498 steps
c [cce-4-1] allowing another 14516249 steps for small clauses
c [cce-4-1] scheduling 17784 clauses = 6642 binary + 11142 ternary
c [cce-4-1] tried to eliminate 17784 small clauses 100%
c [cce-4-1] eliminated 82 binary clauses 1%
c [cce-4-1] eliminated 513 ternary clauses 5%
c [cce-4-1] eliminated 595 small clauses 3%
c [cce-4-1] eliminated 595 small clauses in 45612584 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 1434 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 13386059 steps for small clauses
c [cce-4-2] scheduling 17189 clauses = 6560 binary + 10629 ternary
c [cce-4-2] tried to eliminate 17189 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 1434 covered clauses in TOTAL during 2 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 6790 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3001207220 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 173 variables 3% in round 1 in 9524763 steps
c [elim-8-1] backward subsumption/strengthening limit 9524700
c [elim-8-1-1] backward checking 910 touched variables 13%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 4 and strengthened 1 clauses in 862648 steps
c [elim-8-1] rescheduled 11 variables 0% by backward subsumption
c [elim-8-2] eliminated 3 variables 0% in round 2 in 7444 steps
c [elim-8-2] backward subsumption/strengthening limit 7400
c [elim-8-2-1] backward checking 17 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 7401 steps
c [elim-8-2] fully rescheduled 6614 variables 97%
c [elim-8-3] eliminated 5 variables 0% in round 3 in 9442702 steps
c [elim-8-3] backward subsumption/strengthening limit 9442700
c [elim-8-3-1] backward checking 39 touched variables 1%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 535708 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 181 = 3% variables out of 6790 scheduled
c [bca-6] limit of 10000000 steps and 75364 added (scaled 2)
c [bca-6] 1603 out of 13220 literals actually usable 12%
c [bca-6] added 11 blocked clauses in 63590 steps
c [sweep-7] limit 2250905 penalty 0 = 0 + 0
c [sweep-7-1] 2662 pos 42.4% + 3616 neg 57.6% = 6278 sched 95.0% ret 331
c [sweep-7-1] 2353666 steps 80 queries 341.32 avg class size
c [sweep-7-1] 2393 decisions 72 SAT calls 72.97 avg env size
c [sweep-7-1] 4788 variables remain 72% (1821 retained 28%)
c [decomp-31] removed 16 variables
c [sweep-7-1] removed 16 vars (0 failed, 12 eqs, 10 impls)
c [sweep-7] removed 16 vars in TOTAL (1 rounds, 79 queries)
c [sort-queue-10] sorted 6593 enqueued variables after 162061 conflicts
c [score-dist-10] active 0 (0%), one 6587 (100%), zero 6 (0%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 294 variables 4.3% (6593 remain 20%)
c [simplification-10] removed 2321 irredundant clauses 5.8% (37412 remain 38%)
c [simplification-10] maximum reduction of 6% = max (4%, 6%)
c [simplification-10] large reduction 6% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 174061 (soft 164061 + delta 10000)
c [simplification-10] new conflict limit 164061 (hard 174061)
c 
c [simplification-11] limit 164061 conflicts (hard 174061) hit after 164063 conflicts
c [quatres-7] found 14933 quaternary clauses 33% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-1] added 4 double-self-subsuming ternary resolvents
c [quatres-7-2] added 93 single-self-subsuming ternary resolvents
c [quatres-7-2] added 197 quaternary resolvents
c [ternres-7] limit 7604042 with penalty 0 = 0 + 0
c [ternres-7] all 6593 free variables schedulable
c [ternres-7] 2173 ternary resolvents (70 bin, 2103 trn)
c [ternres-7] 1 variables remain 0% (6592 retained 100%)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] extracted 845 xors of average arity 3.0
c [gauss-4] connected 2513 occurrences of 625 variables (average 4.0)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 16 variables
c [simpleprobe-4] 324 schedulable variables 5%
c [simpleprobe-4] limit 30416171 penalty 0 = 0 + 0
c [decomp-33] removed 12 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 12 variables, found 1249 hbrs, 2 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 503 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 6565 variables 100%
c [elim-9] limit of 152080858 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 18 variables 0% in round 1 in 9432979 steps
c [elim-9-1] backward subsumption/strengthening limit 9432900
c [elim-9-1-1] backward checking 146 touched variables 2%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 5 and strengthened 6 clauses in 552421 steps
c [elim-9-1] rescheduled 24 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 21912 steps
c [elim-9-2] backward subsumption/strengthening limit 21900
c [elim-9-2-1] backward checking 11 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 16795 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 19 = 0% variables out of 6565 scheduled
c [elim-9] 19 < 1/100 * 6565 = 65 considered unsuccessful
c [bca-7] limit of 10000000 steps and 74870 added (scaled 2)
c [bca-7] 1532 out of 13094 literals actually usable 12%
c [bca-7] added 6 blocked clauses in 64176 steps
c [sweep-8] limit 2281212 penalty 0 = 0 + 0
c [sweep-8-1] 2029 pos 42.8% + 2714 neg 57.2% = 4743 sched 72.5% ret 1803
c [sweep-8-1] 2307838 steps 115 queries 274.76 avg class size
c [sweep-8-1] 3546 decisions 106 SAT calls 76.23 avg env size
c [sweep-8-1] 3152 variables remain 48% (3394 retained 52%)
c [decomp-34] removed 21 variables
c [sweep-8-1] removed 21 vars (0 failed, 19 eqs, 19 impls)
c [sweep-8] removed 21 vars in TOTAL (1 rounds, 114 queries)
c [sort-queue-11] sorted 6525 enqueued variables after 164063 conflicts
c [score-dist-11] active 0 (0%), one 6519 (100%), zero 6 (0%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 68 variables 1.0% (6525 remain 20%)
c [simplification-11] removed 252 irredundant clauses 0.7% (37160 remain 38%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 23999 = 47998 / 2
c [simplification-11] new conflict interval 71997
c [simplification-11] penalized conflict interval 71997 = 1 * 71997
c [simplification-11] hard conflict limit 272058 (soft 236060 + delta 35998)
c [simplification-11] new conflict limit 236060 (hard 272058)
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 -   42.4    6525    37160    191915   55522  13947 13826    8    52   17  15%    468   -9    8    7  116%
c -   48.5    6525    37159    231145   61412  14062 13836    8    54   17  15%    719   -1    9    7  122%
c -   55.2    6525    37158    268382   62746  14159 13855    9    42   13  21%    851   -9   10    8  123%
c 
c [simplification-12] limit 236060 conflicts (hard 272058) hit after 272058 conflicts
c [quatres-8] found 15640 quaternary clauses 28% in total
c [quatres-8-1] removed 4 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 110 single-self-subsuming ternary resolvents
c [quatres-8-2] added 152 quaternary resolvents
c [ternres-8] limit 13376006 with penalty 0 = 0 + 0
c [ternres-8] 1 schedulable variables 0%
c [ternres-8] 1898 ternary resolvents (42 bin, 1856 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-35] removed 22 variables
c [unhide-9] limit 1337600 with penalty 1 = 1 + 0
c [unhide-9-12] 1 units, 4 failed, 1701 tauts, 0 hbrs, 18408 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 249 transitive binary clauses
c [transred-8] found 5 units
c [cce-5] limit of 33440016 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 2 clauses out of 46 (4%) of length 11
c [cce-5-1] eliminated 4 clauses out of 105 (4%) of length 10
c [cce-5-1] eliminated 8 clauses out of 213 (4%) of length 9
c [cce-5-1] eliminated 30 clauses out of 448 (7%) of length 8
c [cce-5-1] eliminated 56 clauses out of 946 (6%) of length 7
c [cce-5-1] eliminated 88 clauses out of 1860 (5%) of length 6
c [cce-5-1] eliminated 57 clauses out of 3415 (2%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 245 large clauses in 33440032 steps
c [cce-5-1] allowing another 16720016 steps for small clauses
c [cce-5-1] scheduling 11858 clauses = 6298 binary + 5560 ternary
c [cce-5-1] tried to eliminate 4673 small clauses 39%
c [cce-5-1] eliminated 58 binary clauses 1%
c [cce-5-1] eliminated 164 ternary clauses 3%
c [cce-5-1] eliminated 222 small clauses 2%
c [cce-5-1] eliminated 247 small clauses in 33440020 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 492 covered clauses in round 1
c [cce-5] eliminated 492 covered clauses in TOTAL during 1 rounds
c [bca-8] limit of 10000000 steps and 73745 added (scaled 2)
c [bca-8] 1581 out of 12992 literals actually usable 12%
c [bca-8] added 7 blocked clauses in 68811 steps
c [sweep-9] limit 4012802 penalty 0 = 0 + 0
c [sweep-9-1] 1274 pos 40.7% + 1858 neg 59.3% = 3132 sched 48.2% ret 3363
c [sweep-9-1] 4150610 steps 151 queries 65.21 avg class size
c [sweep-9-1] 3714 decisions 136 SAT calls 69.32 avg env size
c [sweep-9-1] 1792 variables remain 28% (4703 retained 72%)
c [decomp-36] removed 33 variables
c [sweep-9-1] removed 33 vars (0 failed, 26 eqs, 31 impls)
c [sweep-9] removed 33 vars in TOTAL (1 rounds, 150 queries)
c [sort-queue-12] sorted 6462 enqueued variables after 272058 conflicts
c [score-dist-12] active 0 (0%), one 6456 (100%), zero 6 (0%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 63 variables 1.0% (6462 remain 19%)
c [simplification-12] removed 604 irredundant clauses 1.6% (36554 remain 38%)
c [simplification-12] maximum reduction of 2% = max (1%, 2%)
c [simplification-12] geometric conflict interval increment 23999 = 71997 / 3
c [simplification-12] new conflict interval 95996
c [simplification-12] penalized conflict interval 95996 = 1 * 95996
c [simplification-12] hard conflict limit 416052 (soft 368054 + delta 47998)
c [simplification-12] new conflict limit 368054 (hard 416052)
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   59.8    6461    36554    285314   78089  14676 13483    7    18   17  38%    890  -31    5    8   68%
c -   63.7    6461    36554    310115   69508  14706 13486    7    24   18  28%   -597  -20    6    8   80%
c -   71.2    6461    36554    347840   70472  14759 13496   10    40   18  24%    112   -0   11    8  134%
c 
c [simplification-13] limit 368054 conflicts (hard 416052) hit after 373512 conflicts
c [quatres-9] found 15980 quaternary clauses 25% in total
c [quatres-9-1] removed 20 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 71 single-self-subsuming ternary resolvents
c [quatres-9-2] added 131 quaternary resolvents
c [ternres-9] limit 19670012 with penalty 0 = 0 + 0
c [ternres-9] all 6461 free variables schedulable
c [ternres-9] 1864 ternary resolvents (57 bin, 1807 trn)
c [ternres-9] 1 variables remain 0% (6460 retained 100%)
c [decomp-37] removed 15 variables
c [unhide-10] limit 3934002 with penalty 0 = 0 + 0
c [unhide-10-15] 2 units, 18 failed, 2020 tauts, 0 hbrs, 53902 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 219 transitive binary clauses
c [cce-6] limit of 98350064 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 61 (2%) of length 13
c [cce-6-1] eliminated 2 clauses out of 53 (4%) of length 11
c [cce-6-1] eliminated 2 clauses out of 394 (1%) of length 8
c [cce-6-1] eliminated 4 clauses out of 862 (0%) of length 7
c [cce-6-1] eliminated 6 clauses out of 1754 (0%) of length 6
c [cce-6-1] eliminated 46 clauses out of 3336 (1%) of length 5
c [cce-6-1] eliminated 105 clauses out of 7844 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 166 large clauses in 24888064 steps
c [cce-6-1] allowing another 12444032 steps for small clauses
c [cce-6-1] scheduling 11644 clauses = 6237 binary + 5407 ternary
c [cce-6-1] tried to eliminate 11644 small clauses 100%
c [cce-6-1] eliminated 19 binary clauses 0%
c [cce-6-1] eliminated 139 ternary clauses 3%
c [cce-6-1] eliminated 158 small clauses 1%
c [cce-6-1] eliminated 165 small clauses in 31883666 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 331 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 12151781 steps for small clauses
c [cce-6-2] scheduling 11486 clauses = 6218 binary + 5268 ternary
c [cce-6-2] tried to eliminate 11486 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 331 covered clauses in TOTAL during 2 rounds
c [cce-6] 331 < 1/100 * 36487 = 364 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 6440 variables 100%
c [elim-10] limit of 196700128 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 166 variables 3% in round 1 in 8840682 steps
c [elim-10-1] backward subsumption/strengthening limit 8840600
c [elim-10-1-1] backward checking 802 touched variables 12%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 1 and strengthened 2 clauses in 1520054 steps
c [elim-10-1] rescheduled 15 variables 0% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 1252430 steps
c [elim-10-2] backward subsumption/strengthening limit 1252400
c [elim-10-2-1] backward checking 0 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 19511 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 167 = 3% variables out of 6440 scheduled
c [bca-9] limit of 10000000 steps and 71772 added (scaled 2)
c [bca-9] 1568 out of 12548 literals actually usable 12%
c [bca-9] added 17 blocked clauses in 94331 steps
c [sweep-10] limit 5901003 penalty 0 = 0 + 0
c [sweep-10-1] 701 pos 40.9% + 1012 neg 59.1% = 1713 sched 27.3% ret 4560
c [sweep-10-1] 5962557 steps 198 queries 51.82 avg class size
c [sweep-10-1] 3623 decisions 178 SAT calls 62.36 avg env size
c [sweep-10-1] 885 variables remain 14% (5388 retained 86%)
c [decomp-38] removed 47 variables
c [sweep-10-1] removed 47 vars (0 failed, 48 eqs, 45 impls)
c [sweep-10] removed 47 vars in TOTAL (1 rounds, 197 queries)
c [sort-queue-13] sorted 6226 enqueued variables after 373512 conflicts
c [score-dist-13] active 0 (0%), one 6221 (100%), zero 5 (0%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 235 variables 3.6% (6226 remain 19%)
c [simplification-13] removed 959 irredundant clauses 2.6% (35594 remain 37%)
c [simplification-13] maximum reduction of 4% = max (4%, 3%)
c [simplification-13] geometric conflict interval increment 19199 = 95996 / 5
c [simplification-13] new conflict interval 115195
c [simplification-13] penalized conflict interval 115195 = 1 * 115195
c [simplification-13] hard conflict limit 546304 (soft 488707 + delta 57597)
c [simplification-13] new conflict limit 488707 (hard 546304)
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 -   82.0    6226    35593    391476   73568  14869 11319    6    24   14  27%    555  -14    6    8   73%
c -   89.7    6226    35590    432320   76571  14909 11323    9    43   21  20%    773    6   10    8  118%
c -   97.1    6226    35590    472920   81194  14922 11324    9    35   21  24%    889   -3    8    8   99%
c i  104.1    6225    35589    503563  110530  14939 11326   10    35   29  30%    939   -1   11    9  129%
c -  105.5    6225    35589    511001   81371  14940 11326    8    40   21  21%  -2142    4    9    9  102%
c 
c [simplification-14] limit 488707 conflicts (hard 546304) hit after 546304 conflicts
c [quatres-10] found 16033 quaternary clauses 21% in total
c [quatres-10-1] removed 21 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 119 single-self-subsuming ternary resolvents
c [quatres-10-2] added 179 quaternary resolvents
c [ternres-10] limit 32669669 with penalty 0 = 0 + 0
c [ternres-10] 1 schedulable variables 0%
c [ternres-10] 866 ternary resolvents (16 bin, 850 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-39] removed 10 variables
c [unhide-11] limit 6533933 with penalty 0 = 0 + 0
c [unhide-11-19] 0 units, 0 failed, 691 tauts, 0 hbrs, 66327 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 69 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 6216 variables 100%
c [block-5] limit of 40837087 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 42 blocked clauses
c [block-5] 42 < 1/100 * 35529 = 355 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 6209 variables 100%
c [elim-11] limit of 653393395 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 32 variables 1% in round 1 in 8606573 steps
c [elim-11-1] backward subsumption/strengthening limit 8606500
c [elim-11-1-1] backward checking 231 touched variables 4%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 2 clauses in 556552 steps
c [elim-11-1] rescheduled 9 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 1172973 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 32 = 1% variables out of 6209 scheduled
c [elim-11] 32 < 1/100 * 6209 = 62 considered unsuccessful
c [bca-10] limit of 10000000 steps and 71157 added (scaled 2)
c [bca-10] 1667 out of 12356 literals actually usable 13%
c [bca-10] added 8 blocked clauses in 116777 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 98009000 penalty 0 = 0 + 0
c [sweep-11-1] 394 pos 45.5% + 471 neg 54.5% = 865 sched 14.0% ret 5312
c [sweep-11-1] 10413270 steps 351 queries 16.88 avg class size
c [sweep-11-1] 6343 decisions 331 SAT calls 55.24 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-40] removed 91 variables
c [sweep-11-1] removed 91 vars (0 failed, 93 eqs, 65 impls)
c [sweep-11-2] 2558 pos 42.0% + 3528 neg 58.0% = 6086 sched 100.0% ret 0
c [sweep-11-2] 25578257 steps 705 queries 26.34 avg class size
c [sweep-11-2] 13886 decisions 660 SAT calls 69.75 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-41] removed 146 variables
c [sweep-11-2] removed 146 vars (0 failed, 157 eqs, 135 impls)
c [sweep-11-3] 2488 pos 41.9% + 3452 neg 58.1% = 5940 sched 100.0% ret 0
c [sweep-11-3] 22587980 steps 608 queries 37.59 avg class size
c [sweep-11-3] 12729 decisions 595 SAT calls 61.77 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-42] removed 51 variables
c [sweep-11-3] removed 51 vars (0 failed, 66 eqs, 39 impls)
c [sweep-11] removed 288 vars in TOTAL (3 rounds, 1661 queries)
c [sort-queue-14] sorted 5889 enqueued variables after 546304 conflicts
c [score-dist-14] active 0 (0%), one 5884 (100%), zero 5 (0%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 336 variables 5.4% (5889 remain 18%)
c [simplification-14] removed 462 irredundant clauses 1.3% (35127 remain 36%)
c [simplification-14] maximum reduction of 5% = max (5%, 1%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] next conflict interval 5463 = min (546304/100, 115195)
c [simplification-14] penalized conflict interval 5463 = 1 * 5463
c [simplification-14] hard conflict limit 561767 (soft 551767 + delta 10000)
c [simplification-14] new conflict limit 551767 (hard 561767)
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 -  119.1    5889    35127    553381   84535  13479 11314    9    44   15  21%   -635    7    8    9   93%
c 
c [simplification-15] limit 551767 conflicts (hard 561767) hit after 561767 conflicts
c [quatres-11] found 16047 quaternary clauses 22% in total
c [quatres-11-1] removed 109 duplicate quaternary clauses
c [quatres-11-1] added 3 double-self-subsuming ternary resolvents
c [quatres-11-2] added 72 single-self-subsuming ternary resolvents
c [quatres-11-2] added 332 quaternary resolvents
c [ternres-11] limit 33632391 with penalty 0 = 0 + 0
c [ternres-11] all 5889 free variables schedulable
c [ternres-11] 4941 ternary resolvents (62 bin, 4879 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1051012 penalty 4 = 4 + 0
c [card-5] found 302 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1051012 for elimination
c [card-5] 302 out of 302 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 840809 penalty 3 = 3 + 0
c [gauss-5] extracted 834 xors of average arity 3.0
c [gauss-5] connected 2480 occurrences of 563 variables (average 4.4)
c [gauss-5] limit 840809 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [decomp-43] removed 3 variables
c [gauss-5] exported 1 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 420404 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 9562 literals 81%
c [treelook-4] scheduling used 405797 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 420404 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 452956 steps
c [treelook-4] 9544 literals remain 81%
c [treelook-4] 4104 variables remain to probed next time 70%
c [decomp-45] removed 1 variables
c [treelook-4] removed 1 variables, found 1737 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 455 transitive binary clauses
c [transred-11] found 3 units
c [cce-7] limit of 84080978 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 5 clauses out of 57 (9%) of length 13
c [cce-7-1] eliminated 3 clauses out of 47 (6%) of length 11
c [cce-7-1] eliminated 6 clauses out of 91 (7%) of length 10
c [cce-7-1] eliminated 19 clauses out of 201 (9%) of length 9
c [cce-7-1] eliminated 41 clauses out of 424 (10%) of length 8
c [cce-7-1] eliminated 107 clauses out of 841 (13%) of length 7
c [cce-7-1] eliminated 207 clauses out of 1722 (12%) of length 6
c [cce-7-1] eliminated 394 clauses out of 3208 (12%) of length 5
c [cce-7-1] eliminated 703 clauses out of 7573 (9%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1485 large clauses in 36389178 steps
c [cce-7-1] allowing another 18194589 steps for small clauses
c [cce-7-1] scheduling 11078 clauses = 5834 binary + 5244 ternary
c [cce-7-1] tried to eliminate 11078 small clauses 100%
c [cce-7-1] eliminated 235 binary clauses 4%
c [cce-7-1] eliminated 300 ternary clauses 6%
c [cce-7-1] eliminated 535 small clauses 5%
c [cce-7-1] eliminated 541 small clauses in 38075361 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 2026 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 182 (1%) of length 9
c [cce-7-2] eliminated 3 clauses out of 1515 (0%) of length 6
c [cce-7-2] eliminated 7 clauses out of 2814 (0%) of length 5
c [cce-7-2] eliminated 27 clauses out of 6870 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 38 large clauses in 30933297 steps
c [cce-7-2] allowing another 15466648 steps for small clauses
c [cce-7-2] scheduling 10544 clauses = 5599 binary + 4945 ternary
c [cce-7-2] tried to eliminate 10544 small clauses 100%
c [cce-7-2] eliminated 10 binary clauses 0%
c [cce-7-2] eliminated 20 ternary clauses 0%
c [cce-7-2] eliminated 30 small clauses 0%
c [cce-7-2] eliminated 30 small clauses in 33944805 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 68 covered clauses in round 2
c [cce-7-3] eliminated 1 clauses out of 1512 (0%) of length 6
c [cce-7-3] incomplete large round (ACCE)
c [cce-7-3] eliminated 1 large clauses in 12060819 steps
c [cce-7-3] allowing another 6030409 steps for small clauses
c [cce-7-3] scheduling 10514 clauses = 5589 binary + 4925 ternary
c [cce-7-3] tried to eliminate 2545 small clauses 24%
c [cce-7-3] incomplete small round (ACCE)
c [cce-7-3] eliminated 1 covered clauses in round 3
c [cce-7] eliminated 2095 covered clauses in TOTAL during 3 rounds
c [bca-11] limit of 10000000 steps and 66203 added (scaled 2)
c [bca-11] 1566 out of 11766 literals actually usable 13%
c [bca-11] added 1 blocked clauses in 95928 steps
c [sweep-12] limit 10089717 penalty 0 = 0 + 0
c [sweep-12-1] 2601 pos 44.2% + 3281 neg 55.8% = 5882 sched 100.0% ret 0
c [sweep-12-1] 10126840 steps 321 queries 60.64 avg class size
c [sweep-12-1] 8016 decisions 315 SAT calls 65.54 avg env size
c [sweep-12-1] 868 variables remain 15% (5014 retained 85%)
c [decomp-46] removed 8 variables
c [sweep-12-1] removed 8 vars (0 failed, 9 eqs, 9 impls)
c [sweep-12] removed 8 vars in TOTAL (1 rounds, 320 queries)
c [sort-queue-15] sorted 5874 enqueued variables after 561767 conflicts
c [score-dist-15] active 0 (0%), one 5869 (100%), zero 5 (0%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 15 variables 0.3% (5874 remain 18%)
c [simplification-15] removed 2302 irredundant clauses 6.6% (32824 remain 34%)
c [simplification-15] maximum reduction of 7% = max (0%, 7%)
c [simplification-15] large reduction 7% >= 5% limit
c [simplification-15] next conflict interval 5617 = min (561767/100, 115195)
c [simplification-15] penalized conflict interval 5617 = 1 * 5617
c [simplification-15] hard conflict limit 577384 (soft 567384 + delta 10000)
c [simplification-15] new conflict limit 567384 (hard 577384)
c 
c [simplification-16] limit 567384 conflicts (hard 577384) hit after 577384 conflicts
c [quatres-12] found 15372 quaternary clauses 21% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-1] added 11 double-self-subsuming ternary resolvents
c [quatres-12-2] added 115 single-self-subsuming ternary resolvents
c [quatres-12-2] added 76 quaternary resolvents
c [ternres-12] limit 34701812 with penalty 0 = 0 + 0
c [ternres-12] all 5874 free variables schedulable
c [ternres-12] 2481 ternary resolvents (40 bin, 2441 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-47] removed 4 variables
c [basicprobe-4] limit 173509060 penalty 0 = 0 + 0
c [basicprobe-4-0] 568 sched 10%, 0 failed, 0 lifted, 132 hbrs
c [basicprobe-4-1] 3471 sched 59%, 8 failed, 0 lifted, 1339 hbrs
c [decomp-49] removed 9 variables
c [basicprobe-4-2] 3457 sched 59%, 0 failed, 0 lifted, 93 hbrs
c [basicprobe-4-3] 3457 sched 59%, 0 failed, 0 lifted, 82 hbrs
c [basicprobe-4-4] 3457 sched 59%, 0 failed, 0 lifted, 2 hbrs
c [decomp-52] removed 1 variables
c [basicprobe-4-5] 3456 sched 59%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-6] 3456 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-6] fully completed probing
c [basicprobe-4-6] 8 units = 8 failed (100%) + 0 lifted (0%)
c [basicprobe-4-6] removed 10 variables, found 1650 hbrs
c [bate-3] eliminated 4 asymmetric tautologies during probing
c [unhide-12] limit 3470181 with penalty 1 = 1 + 0
c [unhide-12-22] 0 units, 0 failed, 2007 tauts, 0 hbrs, 51730 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 77 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 1735090600 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 715 (0%) of length 7
c [cce-8-1] eliminated 9 clauses out of 1504 (1%) of length 6
c [cce-8-1] eliminated 27 clauses out of 2794 (1%) of length 5
c [cce-8-1] eliminated 20 clauses out of 6830 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 58 large clauses in 17135696 steps
c [cce-8-1] allowing another 8567848 steps for small clauses
c [cce-8-1] scheduling 10497 clauses = 5560 binary + 4937 ternary
c [cce-8-1] tried to eliminate 10497 small clauses 100%
c [cce-8-1] eliminated 5 binary clauses 0%
c [cce-8-1] eliminated 8 ternary clauses 0%
c [cce-8-1] eliminated 13 small clauses 0%
c [cce-8-1] eliminated 13 small clauses in 23429592 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 71 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 8446048 steps for small clauses
c [cce-8-2] scheduling 10484 clauses = 5555 binary + 4929 ternary
c [cce-8-2] tried to eliminate 10484 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 71 covered clauses in TOTAL during 2 rounds
c [cce-8] 71 < 1/100 * 32732 = 327 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5860 variables 100%
c [elim-12] limit of 347018120 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 351 variables 6% in round 1 in 7846614 steps
c [elim-12-1] backward subsumption/strengthening limit 7846600
c [elim-12-1-1] backward checking 1364 touched variables 23%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 11 clauses in 1425122 steps
c [elim-12-1] rescheduled 20 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 878902 steps
c [elim-12-2] backward subsumption/strengthening limit 878900
c [elim-12-2-1] backward checking 5 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 23429 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 352 = 6% variables out of 5860 scheduled
c [bca-12] limit of 10000000 steps and 64077 added (scaled 2)
c [bca-12] 1591 out of 11018 literals actually usable 14%
c [bca-12] added 13 blocked clauses in 103781 steps
c [sweep-13] limit 10410543 penalty 0 = 0 + 0
c [sweep-13-1] 339 pos 42.7% + 455 neg 57.3% = 794 sched 14.4% ret 4714
c [sweep-13-1] 9077058 steps 302 queries 15.27 avg class size
c [sweep-13-1] 5902 decisions 294 SAT calls 62.64 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-54] removed 25 variables
c [sweep-13-1] removed 25 vars (0 failed, 31 eqs, 16 impls)
c [sweep-13-2] 2244 pos 40.9% + 3239 neg 59.1% = 5483 sched 100.0% ret 0
c [sweep-13-2] 1389931 steps 12 queries 944.42 avg class size
c [sweep-13-2] 663 decisions 11 SAT calls 110.00 avg env size
c [sweep-13-2] 5372 variables remain 98% (111 retained 2%)
c [sweep-13-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-13] removed 25 vars in TOTAL (2 rounds, 312 queries)
c [sort-queue-16] sorted 5483 enqueued variables after 577384 conflicts
c [score-dist-16] active 0 (0%), one 5482 (100%), zero 1 (0%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 391 variables 6.7% (5483 remain 16%)
c [simplification-16] removed 1072 irredundant clauses 3.3% (31749 remain 33%)
c [simplification-16] maximum reduction of 7% = max (7%, 3%)
c [simplification-16] large reduction 7% >= 5% limit
c [simplification-16] next conflict interval 5773 = min (577384/100, 115195)
c [simplification-16] penalized conflict interval 5773 = 1 * 5773
c [simplification-16] hard conflict limit 593157 (soft 583157 + delta 10000)
c [simplification-16] new conflict limit 583157 (hard 593157)
c 
c [simplification-17] limit 583157 conflicts (hard 593157) hit after 585019 conflicts
c [quatres-13] found 14349 quaternary clauses 21% in total
c [quatres-13-1] removed 31 duplicate quaternary clauses
c [quatres-13-1] added 2 double-self-subsuming ternary resolvents
c [quatres-13-2] added 81 single-self-subsuming ternary resolvents
c [quatres-13-2] added 203 quaternary resolvents
c [ternres-13] limit 35175343 with penalty 0 = 0 + 0
c [ternres-13] all 5483 free variables schedulable
c [ternres-13] 2552 ternary resolvents (46 bin, 2506 trn)
c [ternres-13] 7 variables remain 0% (5476 retained 100%)
c [gauss-6] limit 1758767 penalty 2 = 2 + 0
c [gauss-6] extracted 1244 xors of average arity 3.0
c [gauss-6] connected 3710 occurrences of 392 variables (average 9.5)
c [gauss-6] limit 1758767 penalty 2 = 2 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] all 5483 free variables schedulable
c [simpleprobe-5] limit 140701374 penalty 0 = 0 + 0
c [decomp-57] removed 9 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 9 variables, found 1383 hbrs, 1 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 141 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 5474 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 19 variables 0% in round 1 in 7855305 steps
c [elim-13-1] backward subsumption/strengthening limit 7855300
c [elim-13-1-1] backward checking 175 touched variables 3%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 490081 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 19 = 0% variables out of 5474 scheduled
c [elim-13] 19 < 1/100 * 5474 = 54 considered unsuccessful
c [bca-13] limit of 10000000 steps and 63714 added (scaled 2)
c [bca-13] 1547 out of 10912 literals actually usable 14%
c [bca-13] added 3 blocked clauses in 110338 steps
c [sweep-14] limit 10552603 penalty 0 = 0 + 0
c [sweep-14-1] 2212 pos 41.4% + 3134 neg 58.6% = 5346 sched 98.0% ret 109
c [sweep-14-1] 10604340 steps 201 queries 78.62 avg class size
c [sweep-14-1] 5807 decisions 201 SAT calls 82.80 avg env size
c [sweep-14-1] 1591 variables remain 29% (3864 retained 71%)
c [decomp-58] removed 5 variables
c [sweep-14-1] removed 5 vars (0 failed, 5 eqs, 6 impls)
c [sweep-14] removed 5 vars in TOTAL (1 rounds, 200 queries)
c [sort-queue-17] sorted 5450 enqueued variables after 585019 conflicts
c [score-dist-17] active 0 (0%), one 5449 (100%), zero 1 (0%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 33 variables 0.6% (5450 remain 16%)
c [simplification-17] removed 183 irredundant clauses 0.6% (31565 remain 32%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 57597 = 115195 / 2
c [simplification-17] new conflict interval 172792
c [simplification-17] penalized conflict interval 172792 = 1 * 172792
c [simplification-17] hard conflict limit 844207 (soft 757811 + delta 86396)
c [simplification-17] new conflict limit 757811 (hard 844207)
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 -  137.8    5450    31565    599372   85218  18518 11251    9    41   23  23%    201   -3   12    9  137%
c -  145.4    5450    31565    640257   88551  18533 11254    8    34   23  25%    583   -8    9    9  103%
c i  152.8    5449    31565    678032  124354  18566 11262    8    40   32  21%    776    1    8    9   88%
c -  154.3    5449    31565    682130   90724  18569 11262   10    37   23  27%  -1760   -2   11    9  125%
c -  163.8    5449    31565    723633   91450  18590 11265   10    36   23  28%   -480   -1   10    9  105%
c -  171.4    5449    31565    767739   96032  18604 11265    9    23   24  39%    256  -16    8    9   89%
c 
c [simplification-18] limit 757811 conflicts (hard 844207) hit after 771326 conflicts
c [quatres-14] found 14597 quaternary clauses 19% in total
c [quatres-14-1] removed 8 duplicate quaternary clauses
c [quatres-14-1] added 2 double-self-subsuming ternary resolvents
c [quatres-14-2] added 93 single-self-subsuming ternary resolvents
c [quatres-14-2] added 112 quaternary resolvents
c [ternres-14] limit 49202640 with penalty 0 = 0 + 0
c [ternres-14] 7 schedulable variables 0%
c [ternres-14] 2478 ternary resolvents (11 bin, 2467 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-59] removed 2 variables
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 273 transitive binary clauses
c [cce-9] limit of 123006600 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 2 clauses out of 50 (4%) of length 13
c [cce-9-1] eliminated 3 clauses out of 53 (6%) of length 12
c [cce-9-1] eliminated 8 clauses out of 53 (15%) of length 11
c [cce-9-1] eliminated 17 clauses out of 115 (15%) of length 10
c [cce-9-1] eliminated 33 clauses out of 231 (14%) of length 9
c [cce-9-1] eliminated 45 clauses out of 469 (10%) of length 8
c [cce-9-1] eliminated 95 clauses out of 879 (11%) of length 7
c [cce-9-1] eliminated 79 clauses out of 1602 (5%) of length 6
c [cce-9-1] eliminated 122 clauses out of 2818 (4%) of length 5
c [cce-9-1] eliminated 190 clauses out of 6664 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 594 large clauses in 24130968 steps
c [cce-9-1] allowing another 12065484 steps for small clauses
c [cce-9-1] scheduling 9907 clauses = 5189 binary + 4718 ternary
c [cce-9-1] tried to eliminate 9907 small clauses 100%
c [cce-9-1] eliminated 76 binary clauses 1%
c [cce-9-1] eliminated 69 ternary clauses 1%
c [cce-9-1] eliminated 145 small clauses 1%
c [cce-9-1] eliminated 145 small clauses in 28467851 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 739 covered clauses in round 1
c [cce-9-2] eliminated 2 clauses out of 198 (1%) of length 9
c [cce-9-2] eliminated 1 clauses out of 424 (0%) of length 8
c [cce-9-2] eliminated 5 clauses out of 784 (1%) of length 7
c [cce-9-2] eliminated 3 clauses out of 1523 (0%) of length 6
c [cce-9-2] eliminated 4 clauses out of 2696 (0%) of length 5
c [cce-9-2] eliminated 5 clauses out of 6474 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 20 large clauses in 22954215 steps
c [cce-9-2] allowing another 11477107 steps for small clauses
c [cce-9-2] scheduling 9762 clauses = 5113 binary + 4649 ternary
c [cce-9-2] tried to eliminate 9762 small clauses 100%
c [cce-9-2] eliminated 1 binary clauses 0%
c [cce-9-2] eliminated 2 ternary clauses 0%
c [cce-9-2] eliminated 3 small clauses 0%
c [cce-9-2] eliminated 3 small clauses in 27685524 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 23 covered clauses in round 2
c [cce-9-3] eliminated 2 clauses out of 6469 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 2 large clauses in 22862389 steps
c [cce-9-3] allowing another 11431194 steps for small clauses
c [cce-9-3] scheduling 9759 clauses = 5112 binary + 4647 ternary
c [cce-9-3] tried to eliminate 9759 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 2 covered clauses in round 3
c [cce-9] eliminated 764 covered clauses in TOTAL during 3 rounds
c [bca-14] limit of 10000000 steps and 62147 added (scaled 2)
c [bca-14] 1509 out of 10898 literals actually usable 14%
c [bca-14] added 3 blocked clauses in 102796 steps
c [sweep-15] limit 14760792 penalty 0 = 0 + 0
c [sweep-15-1] 713 pos 44.8% + 878 neg 55.2% = 1591 sched 29.2% ret 3857
c [sweep-15-1] 9160947 steps 414 queries 20.05 avg class size
c [sweep-15-1] 7575 decisions 414 SAT calls 50.10 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-60] removed 12 variables
c [sweep-15-1] removed 12 vars (0 failed, 13 eqs, 10 impls)
c [sweep-15-2] 2264 pos 41.6% + 3172 neg 58.4% = 5436 sched 100.0% ret 0
c [sweep-15-2] 5609415 steps 109 queries 139.72 avg class size
c [sweep-15-2] 4005 decisions 109 SAT calls 103.61 avg env size
c [sweep-15-2] 2875 variables remain 53% (2561 retained 47%)
c [decomp-61] removed 1 variables
c [sweep-15-2] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-15] removed 13 vars in TOTAL (2 rounds, 521 queries)
c [sort-queue-18] sorted 5435 enqueued variables after 771326 conflicts
c [score-dist-18] active 0 (0%), one 5434 (100%), zero 1 (0%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 14 variables 0.3% (5435 remain 16%)
c [simplification-18] removed 778 irredundant clauses 2.5% (30787 remain 32%)
c [simplification-18] maximum reduction of 2% = max (0%, 2%)
c [simplification-18] geometric conflict interval increment 57597 = 172792 / 3
c [simplification-18] new conflict interval 230389
c [simplification-18] penalized conflict interval 230389 = 1 * 230389
c [simplification-18] hard conflict limit 1116909 (soft 1001715 + delta 115194)
c [simplification-18] new conflict limit 1001715 (hard 1116909)
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 -  183.8    5435    30787    808343   97756  20806 11108   11    33   23  32%    611   -4   12    9  133%
c -  193.2    5435    30787    853459  101804  20820 11109   10    42   24  25%    816    6   11    9  122%
c -  201.7    5435    30787    896510  103970  20832 11109    8    37   24  23%    916    1   10    9  111%
c i  202.7    5434    30787    902521  109739  20833 11112    9    34   28  26%    926   -2    8    9   88%
c -  213.0    5434    30787    938613  102153  20860 11112   11    36   23  30%  -1087    2   11   10  117%
c -  222.5    5434    30787    988137  108755  20868 11112   10    38   24  25%     33    6    9   10   95%
c 
c [simplification-19] limit 1001715 conflicts (hard 1116909) hit after 1001717 conflicts
c [quatres-15] found 14675 quaternary clauses 17% in total
c [quatres-15-1] removed 3 duplicate quaternary clauses
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 56 single-self-subsuming ternary resolvents
c [quatres-15-2] added 90 quaternary resolvents
c [ternres-15] limit 67982093 with penalty 0 = 0 + 0
c [ternres-15] all 5434 free variables schedulable
c [ternres-15] 2638 ternary resolvents (37 bin, 2601 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-62] removed 2 variables
c [treelook-5] limit 1699552 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 8840 literals 81%
c [treelook-5] scheduling used 466826 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1699552 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 1704040 steps
c [treelook-5] 8633 literals remain 79%
c [treelook-5] 3760 variables remain to probed next time 69%
c [treelook-5] removed 0 variables, found 1993 hbrs
c [unhide-13] limit 3399104 with penalty 2 = 2 + 0
c [unhide-13-24] 0 units, 0 failed, 1930 tauts, 0 hbrs, 38035 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 157 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5433 variables 100%
c [block-6] limit of 42488808 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 216 blocked clauses
c [block-6] 216 < 1/100 * 30779 = 307 considered unsuccessful
c [cce-10] limit of 339910466 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 4 clauses out of 408 (1%) of length 8
c [cce-10-1] eliminated 26 clauses out of 751 (3%) of length 7
c [cce-10-1] eliminated 24 clauses out of 1527 (2%) of length 6
c [cce-10-1] eliminated 20 clauses out of 2678 (1%) of length 5
c [cce-10-1] eliminated 22 clauses out of 6429 (0%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 96 large clauses in 16084253 steps
c [cce-10-1] allowing another 8042126 steps for small clauses
c [cce-10-1] scheduling 9700 clauses = 5074 binary + 4626 ternary
c [cce-10-1] tried to eliminate 9700 small clauses 100%
c [cce-10-1] eliminated 1 binary clauses 0%
c [cce-10-1] eliminated 10 ternary clauses 0%
c [cce-10-1] eliminated 11 small clauses 0%
c [cce-10-1] eliminated 11 small clauses in 21439414 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 107 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 7965110 steps for small clauses
c [cce-10-2] scheduling 9689 clauses = 5073 binary + 4616 ternary
c [cce-10-2] tried to eliminate 9689 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 107 covered clauses in TOTAL during 2 rounds
c [cce-10] 107 < 1/100 * 30563 = 305 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 5384 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 113 variables 2% in round 1 in 7293766 steps
c [elim-14-1] backward subsumption/strengthening limit 7293700
c [elim-14-1-1] backward checking 595 touched variables 11%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 3 clauses in 1217097 steps
c [elim-14-1] rescheduled 13 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 902235 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 113 = 2% variables out of 5384 scheduled
c [bca-15] limit of 10000000 steps and 61027 added (scaled 2)
c [bca-15] 1535 out of 10544 literals actually usable 15%
c [bca-15] added 3 blocked clauses in 123255 steps
c [sweep-16] limit 20394628 penalty 0 = 0 + 0
c [sweep-16-1] 1184 pos 42.8% + 1585 neg 57.2% = 2769 sched 52.5% ret 2502
c [sweep-16-1] 14990076 steps 480 queries 25.64 avg class size
c [sweep-16-1] 9665 decisions 495 SAT calls 52.63 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-64] removed 33 variables
c [sweep-16-1] removed 33 vars (0 failed, 32 eqs, 12 impls)
c [sweep-16-2] 2133 pos 40.7% + 3105 neg 59.3% = 5238 sched 100.0% ret 0
c [sweep-16-2] 5555701 steps 84 queries 141.92 avg class size
c [sweep-16-2] 2712 decisions 84 SAT calls 105.80 avg env size
c [sweep-16-2] 3120 variables remain 60% (2118 retained 40%)
c [decomp-65] removed 2 variables
c [sweep-16-2] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-16] removed 35 vars in TOTAL (2 rounds, 562 queries)
c [sort-queue-19] sorted 5236 enqueued variables after 1001717 conflicts
c [score-dist-19] active 0 (0%), one 5235 (100%), zero 1 (0%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 198 variables 3.6% (5236 remain 16%)
c [simplification-19] removed 558 irredundant clauses 1.8% (30229 remain 31%)
c [simplification-19] maximum reduction of 4% = max (4%, 2%)
c [simplification-19] geometric conflict interval increment 46077 = 230389 / 5
c [simplification-19] new conflict interval 276466
c [simplification-19] penalized conflict interval 276466 = 1 * 276466
c [simplification-19] hard conflict limit 1416416 (soft 1278183 + delta 138233)
c [simplification-19] new conflict limit 1278183 (hard 1416416)
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 -  236.7    5236    30227   1031895  107790  19821 11508    9    44   25  20%    515    9   10   10  103%
c -  244.6    5236    30227   1077997  109037  19822 11508    9    12   25  76%    772  -24    9   10   88%
c -  253.6    5236    30227   1125505  110872  19841 11509   11    30   25  37%    902   -0   12   10  125%
c i  257.7    5235    30227   1157963  137458  19896 11518    7     8   33  85%    950  -18    5    9   50%
c -  262.7    3718    30227   1177669  114488  19900 11520    8    30   26  25%  -2033    2    6    9   70%
c i  269.9    3717    30227   1203263  138921  19912 11522   11    35   33  33%  -1044    7   11    9  117%
c -  275.1    3717    30227   1224491  114757  19920 11523    8    43   26  19%   -992   13    8    9   83%
c -  288.0    3717    30227   1273417  116548  19944 11525   11    30   26  35%     68   -3   12   10  122%
c 
c [simplification-20] limit 1278183 conflicts (hard 1416416) hit after 1278804 conflicts
c [quatres-16] found 7830 quaternary clauses 11% in total
c [quatres-16-1] removed 29 duplicate quaternary clauses
c [quatres-16-1] added 3 double-self-subsuming ternary resolvents
c [quatres-16-2] added 93 single-self-subsuming ternary resolvents
c [quatres-16-2] added 239 quaternary resolvents
c [ternres-16] limit 92022065 with penalty 0 = 0 + 0
c [ternres-16] all 3717 free variables schedulable
c [ternres-16] 2104 ternary resolvents (42 bin, 2062 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-7] limit 2300551 penalty 3 = 3 + 0
c [gauss-7] extracted 2665 xors of average arity 2.4
c [gauss-7] connected 6287 occurrences of 1084 variables (average 5.8)
c [gauss-7] limit 2300551 penalty 3 = 3 + 0
c [gauss-7] fully completed
c [decomp-66] removed 603 variables
c [gauss-7] exported 0 unary, 57 binary and 3 ternary equations
c [decomp-67] removed 1 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 1709 sched 56%, 47 failed, 11 lifted, 2477 hbrs
c [decomp-68] removed 95 variables
c [basicprobe-5-1] 1601 sched 53%, 8 failed, 0 lifted, 352 hbrs
c [decomp-69] removed 9 variables
c [basicprobe-5-2] 1587 sched 53%, 1 failed, 0 lifted, 79 hbrs
c [decomp-70] removed 1 variables
c [basicprobe-5-3] 1589 sched 53%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-5-4] 1588 sched 53%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-5-5] 1588 sched 53%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-5-6] 1588 sched 53%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-5-7] 1588 sched 53%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-5-8] 1590 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 67 units = 56 failed (84%) + 11 lifted (16%)
c [basicprobe-5-8] removed 105 variables, found 2949 hbrs
c [bate-4] eliminated 259 asymmetric tautologies during probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 702 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 3008 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 506 variables 17% in round 1 in 2478388 steps
c [elim-15-1] backward subsumption/strengthening limit 2478300
c [elim-15-1-1] backward checking 1107 touched variables 37%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 15 and strengthened 14 clauses in 211111 steps
c [elim-15-1] rescheduled 82 variables 3% by backward subsumption
c [elim-15-2] eliminated 6 variables 0% in round 2 in 116635 steps
c [elim-15-2] backward subsumption/strengthening limit 116600
c [elim-15-2-1] backward checking 40 touched variables 1%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 3 and strengthened 0 clauses in 30988 steps
c [elim-15-2] rescheduled 9 variables 0% by backward subsumption
c [elim-15-3] eliminated 3 variables 0% in round 3 in 8722 steps
c [elim-15-3] backward subsumption/strengthening limit 8700
c [elim-15-3-1] backward checking 9 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 0 and strengthened 0 clauses in 8701 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 515 = 17% variables out of 3008 scheduled
c [bca-16] limit of 10000000 steps and 28964 added (scaled 2)
c [bca-16] 499 out of 4988 literals actually usable 10%
c [bca-16] added 12 blocked clauses in 101080 steps
c [sweep-17] limit 27606619 penalty 0 = 0 + 0
c [sweep-17-1] 541 pos 43.1% + 713 neg 56.9% = 1254 sched 50.3% ret 1239
c [sweep-17-1] 10738458 steps 194 queries 16.08 avg class size
c [sweep-17-1] 4904 decisions 188 SAT calls 77.90 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-76] removed 28 variables
c [sweep-17-1] removed 28 vars (0 failed, 28 eqs, 21 impls)
c [sweep-17-2] 1044 pos 42.4% + 1421 neg 57.6% = 2465 sched 100.0% ret 0
c [sweep-17-2] 12449200 steps 209 queries 18.98 avg class size
c [sweep-17-2] 5535 decisions 197 SAT calls 80.33 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-77] removed 24 variables
c [sweep-17-2] removed 24 vars (0 failed, 25 eqs, 19 impls)
c [sweep-17-3] 1032 pos 42.3% + 1409 neg 57.7% = 2441 sched 100.0% ret 0
c [sweep-17-3] 4657027 steps 50 queries 138.26 avg class size
c [sweep-17-3] 1644 decisions 50 SAT calls 110.14 avg env size
c [sweep-17-3] 962 variables remain 40% (1471 retained 60%)
c [decomp-78] removed 18 variables
c [sweep-17-3] removed 18 vars (0 failed, 2 eqs, 0 impls)
c [sweep-17] removed 70 vars in TOTAL (3 rounds, 450 queries)
c [sort-queue-20] sorted 2423 enqueued variables after 1278804 conflicts
c [score-dist-20] active 0 (0%), one 2422 (100%), zero 1 (0%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 1294 variables 34.8% (2423 remain 7%)
c [simplification-20] removed 16328 irredundant clauses 54.0% (13899 remain 14%)
c [simplification-20] maximum reduction of 54% = max (35%, 54%)
c [simplification-20] large reduction 54% >= 5% limit
c [simplification-20] next conflict interval 12788 = min (1278804/100, 276466)
c [simplification-20] penalized conflict interval 12788 = 1 * 12788
c [simplification-20] hard conflict limit 1301592 (soft 1291592 + delta 10000)
c [simplification-20] new conflict limit 1291592 (hard 1301592)
c 
c [simplification-21] limit 1291592 conflicts (hard 1301592) hit after 1295281 conflicts
c [quatres-17] found 8205 quaternary clauses 11% in total
c [quatres-17-1] removed 121 duplicate quaternary clauses
c [quatres-17-1] added 2 double-self-subsuming ternary resolvents
c [quatres-17-2] added 69 single-self-subsuming ternary resolvents
c [quatres-17-2] added 130 quaternary resolvents
c [ternres-17] limit 93237187 with penalty 0 = 0 + 0
c [ternres-17] all 2423 free variables schedulable
c [ternres-17] 1136 ternary resolvents (33 bin, 1103 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2913662 penalty 4 = 4 + 0
c [card-6] found 213 at-most-one constraints of average size 3.0
c [card-6] found 42 at-most-two constraints of average size 4.0
c [card-6] using previous limit 2913662 for elimination
c [card-6] 255 out of 255 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-79] removed 2 variables
c [simpleprobe-6] all 2421 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-80] removed 7 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 7 variables, found 1072 hbrs, 3 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 521 transitive binary clauses
c [cce-11] limit of 233092968 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 14
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 13
c [cce-11-1] eliminated 2 clauses out of 10 (20%) of length 12
c [cce-11-1] eliminated 11 clauses out of 23 (48%) of length 11
c [cce-11-1] eliminated 6 clauses out of 17 (35%) of length 10
c [cce-11-1] eliminated 18 clauses out of 80 (22%) of length 9
c [cce-11-1] eliminated 16 clauses out of 76 (21%) of length 8
c [cce-11-1] eliminated 24 clauses out of 172 (14%) of length 7
c [cce-11-1] eliminated 79 clauses out of 440 (18%) of length 6
c [cce-11-1] eliminated 128 clauses out of 1104 (12%) of length 5
c [cce-11-1] eliminated 252 clauses out of 3131 (8%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 538 large clauses in 7600749 steps
c [cce-11-1] allowing another 3800374 steps for small clauses
c [cce-11-1] scheduling 6286 clauses = 2133 binary + 4153 ternary
c [cce-11-1] tried to eliminate 6286 small clauses 100%
c [cce-11-1] eliminated 201 binary clauses 9%
c [cce-11-1] eliminated 243 ternary clauses 6%
c [cce-11-1] eliminated 444 small clauses 7%
c [cce-11-1] eliminated 444 small clauses in 8638702 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 982 covered clauses in round 1
c [cce-11-2] eliminated 2 clauses out of 60 (3%) of length 8
c [cce-11-2] eliminated 1 clauses out of 361 (0%) of length 6
c [cce-11-2] eliminated 4 clauses out of 976 (0%) of length 5
c [cce-11-2] eliminated 7 clauses out of 2879 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 14 large clauses in 6974245 steps
c [cce-11-2] allowing another 3487122 steps for small clauses
c [cce-11-2] scheduling 5842 clauses = 1932 binary + 3910 ternary
c [cce-11-2] tried to eliminate 5842 small clauses 100%
c [cce-11-2] eliminated 5 binary clauses 0%
c [cce-11-2] eliminated 15 ternary clauses 0%
c [cce-11-2] eliminated 20 small clauses 0%
c [cce-11-2] eliminated 20 small clauses in 7904465 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 34 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 3475929 steps for small clauses
c [cce-11-3] scheduling 5822 clauses = 1927 binary + 3895 ternary
c [cce-11-3] tried to eliminate 5822 small clauses 100%
c [cce-11-3] eliminated 1 binary clauses 0%
c [cce-11-3] eliminated 2 ternary clauses 0%
c [cce-11-3] eliminated 3 small clauses 0%
c [cce-11-3] eliminated 3 small clauses in 7872926 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 3 covered clauses in round 3
c [cce-11] eliminated 1019 covered clauses in TOTAL during 3 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2414 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 205 variables 8% in round 1 in 1887629 steps
c [elim-16-1] backward subsumption/strengthening limit 1887600
c [elim-16-1-1] backward checking 580 touched variables 24%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 2 and strengthened 8 clauses in 101281 steps
c [elim-16-1] rescheduled 41 variables 2% by backward subsumption
c [elim-16-2] eliminated 4 variables 0% in round 2 in 46758 steps
c [elim-16-2] backward subsumption/strengthening limit 46700
c [elim-16-2-1] backward checking 41 touched variables 2%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 1 and strengthened 6 clauses in 26097 steps
c [elim-16-2] rescheduled 21 variables 1% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 74979 steps
c [elim-16-3] backward subsumption/strengthening limit 74900
c [elim-16-3-1] backward checking 11 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 0 and strengthened 0 clauses in 11535 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 211 = 9% variables out of 2414 scheduled
c [bca-17] limit of 10000000 steps and 25172 added (scaled 2)
c [bca-17] 303 out of 4408 literals actually usable 7%
c [bca-17] added 58 blocked clauses in 115329 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 334 pos 40.8% + 485 neg 59.2% = 819 sched 37.2% ret 1384
c [sweep-18-1] 8919153 steps 149 queries 13.90 avg class size
c [sweep-18-1] 4039 decisions 148 SAT calls 86.99 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-81] removed 4 variables
c [sweep-18-1] removed 4 vars (0 failed, 5 eqs, 6 impls)
c [sweep-18-2] 914 pos 41.6% + 1285 neg 58.4% = 2199 sched 100.0% ret 0
c [sweep-18-2] 10602191 steps 194 queries 29.66 avg class size
c [sweep-18-2] 4640 decisions 195 SAT calls 88.67 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-82] removed 6 variables
c [sweep-18-2] removed 6 vars (0 failed, 7 eqs, 3 impls)
c [sweep-18-3] 910 pos 41.5% + 1283 neg 58.5% = 2193 sched 100.0% ret 0
c [sweep-18-3] 10193314 steps 187 queries 22.04 avg class size
c [sweep-18-3] 5145 decisions 189 SAT calls 93.88 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-83] removed 1 variables
c [sweep-18-3] removed 1 vars (0 failed, 2 eqs, 0 impls)
c [sweep-18] removed 11 vars in TOTAL (3 rounds, 527 queries)
c [sort-queue-21] sorted 2192 enqueued variables after 1295281 conflicts
c [score-dist-21] active 0 (0%), one 2192 (100%), zero 0 (0%)
c [score-dist-21] max exp 1, different 1 (50%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 231 variables 9.5% (2192 remain 7%)
c [simplification-21] removed 1598 irredundant clauses 11.5% (12300 remain 13%)
c [simplification-21] maximum reduction of 11% = max (10%, 11%)
c [simplification-21] large reduction 11% >= 5% limit
c [simplification-21] next conflict interval 12952 = min (1295281/100, 276466)
c [simplification-21] penalized conflict interval 12952 = 1 * 12952
c [simplification-21] hard conflict limit 1318233 (soft 1308233 + delta 10000)
c [simplification-21] new conflict limit 1308233 (hard 1318233)
c 
c [simplification-22] limit 1308233 conflicts (hard 1318233) hit after 1308233 conflicts
c [quatres-18] found 7606 quaternary clauses 10% in total
c [quatres-18-1] removed 4 duplicate quaternary clauses
c [quatres-18-2] added 20 single-self-subsuming ternary resolvents
c [quatres-18-2] added 61 quaternary resolvents
c [ternres-18] limit 94306283 with penalty 0 = 0 + 0
c [ternres-18] all 2192 free variables schedulable
c [ternres-18] 179 ternary resolvents (18 bin, 161 trn)
c [ternres-18] fully completed ternary resolution
c [gauss-8] limit 4715314 penalty 2 = 2 + 0
c [gauss-8] extracted 1454 xors of average arity 3.0
c [gauss-8] connected 4374 occurrences of 315 variables (average 13.9)
c [gauss-8] limit 4715314 penalty 2 = 2 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 2 ternary equations
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 255 transitive binary clauses
c [transred-18] found 1 units
c [cce-12] limit of 471531415 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 6 (17%) of length 12
c [cce-12-1] eliminated 4 clauses out of 20 (20%) of length 10
c [cce-12-1] eliminated 1 clauses out of 68 (1%) of length 9
c [cce-12-1] eliminated 3 clauses out of 113 (3%) of length 8
c [cce-12-1] eliminated 5 clauses out of 171 (3%) of length 7
c [cce-12-1] eliminated 4 clauses out of 381 (1%) of length 6
c [cce-12-1] eliminated 15 clauses out of 1000 (2%) of length 5
c [cce-12-1] eliminated 29 clauses out of 2858 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 62 large clauses in 3309229 steps
c [cce-12-1] allowing another 1654614 steps for small clauses
c [cce-12-1] scheduling 5456 clauses = 1748 binary + 3708 ternary
c [cce-12-1] tried to eliminate 5456 small clauses 100%
c [cce-12-1] eliminated 13 binary clauses 1%
c [cce-12-1] eliminated 16 ternary clauses 0%
c [cce-12-1] eliminated 29 small clauses 1%
c [cce-12-1] eliminated 33 small clauses in 4260877 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 95 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1608334 steps for small clauses
c [cce-12-2] scheduling 5427 clauses = 1735 binary + 3692 ternary
c [cce-12-2] tried to eliminate 5427 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 95 covered clauses in TOTAL during 2 rounds
c [cce-12] 95 < 1/100 * 12293 = 122 considered unsuccessful
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 2191 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 13 variables 1% in round 1 in 1801629 steps
c [elim-17-1] backward subsumption/strengthening limit 1801600
c [elim-17-1-1] backward checking 96 touched variables 4%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 11 clauses in 26371 steps
c [elim-17-1] rescheduled 19 variables 1% by backward subsumption
c [elim-17-2] eliminated 1 variables 0% in round 2 in 16902 steps
c [elim-17-2] backward subsumption/strengthening limit 16900
c [elim-17-2-1] backward checking 7 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 6736 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 14 = 1% variables out of 2191 scheduled
c [elim-17] 14 < 1/100 * 2191 = 21 considered unsuccessful
c [bca-18] limit of 10000000 steps and 24907 added (scaled 2)
c [bca-18] 255 out of 4356 literals actually usable 6%
c [bca-18] added 0 blocked clauses in 127402 steps
c [sweep-19] limit 28291884 penalty 0 = 0 + 0
c [sweep-19-1] 916 pos 42.1% + 1261 neg 57.9% = 2177 sched 100.0% ret 0
c [sweep-19-1] 14706746 steps 193 queries 18.76 avg class size
c [sweep-19-1] 5656 decisions 194 SAT calls 104.96 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-85] removed 10 variables
c [sweep-19-1] removed 10 vars (0 failed, 10 eqs, 5 impls)
c [sweep-19-2] 913 pos 42.1% + 1254 neg 57.9% = 2167 sched 100.0% ret 0
c [sweep-19-2] 13588468 steps 145 queries 28.46 avg class size
c [sweep-19-2] 4944 decisions 146 SAT calls 116.25 avg env size
c [sweep-19-2] 80 variables remain 4% (2087 retained 96%)
c [decomp-86] removed 2 variables
c [sweep-19-2] removed 2 vars (0 failed, 2 eqs, 2 impls)
c [sweep-19] removed 12 vars in TOTAL (2 rounds, 336 queries)
c [sort-queue-22] sorted 2165 enqueued variables after 1308233 conflicts
c [score-dist-22] active 0 (0%), one 2165 (100%), zero 0 (0%)
c [score-dist-22] max exp 1, different 1 (50%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 27 variables 1.2% (2165 remain 7%)
c [simplification-22] removed 145 irredundant clauses 1.2% (12155 remain 12%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 138233 = 276466 / 2
c [simplification-22] new conflict interval 414699
c [simplification-22] penalized conflict interval 414699 = 1 * 414699
c [simplification-22] hard conflict limit 1930281 (soft 1722932 + delta 207349)
c [simplification-22] new conflict limit 1722932 (hard 1930281)
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  308.9    2164    12155   1326784  143171   5179  4241    9    31   34  30%    601   -4   11    9  115%
c -  311.1    2164    12155   1331190  102244   5185  4242   11    34   21  31%  -1178   -1   10    9  103%
c -  323.2    2164    12155   1383621  106997   5214  4246   11    31   24  35%     23   -2   12    9  126%
c -  335.0    2164    12155   1432647  106784   5236  4252   10    36   24  29%    550    3   12   10  119%
c -  346.2    2164    12155   1485023  110897   5267  4252   10    39   24  25%    811    6   12   10  119%
c -  356.7    2164    12155   1535937  113353   5290  4253    9    36   24  26%    926    1    8   10   87%
c -  368.1    2164    12155   1586963  115324   5318  4262   10    29   24  33%    979   -5   10   10  100%
c i  374.0    2163    12155   1613740  140889   5324  4275   10    36   33  27%    994    1    8   10   77%
c i  380.3    2162    12155   1632767  159040   5352  4284    9    20   35  44%  -2405  -15    6   10   58%
c -  382.4    2162    12155   1638717  116435   5359  4286   10    36   24  28%  -2383    2   10   10  106%
c -  394.9    2162    12155   1691754  119309   5378  4291   11    33   24  32%   -493   -1    9   10   96%
c 
c [simplification-23] limit 1722932 conflicts (hard 1930281) hit after 1729807 conflicts
c [quatres-19] found 8092 quaternary clauses 9% in total
c [quatres-19-1] removed 8 duplicate quaternary clauses
c [quatres-19-2] added 33 single-self-subsuming ternary resolvents
c [quatres-19-2] added 85 quaternary resolvents
c [ternres-19] limit 132477792 with penalty 0 = 0 + 0
c [ternres-19] all 2162 free variables schedulable
c [ternres-19] 425 ternary resolvents (20 bin, 405 trn)
c [ternres-19] fully completed ternary resolution
c [gauss-9] limit 13247779 penalty 1 = 1 + 0
c [gauss-9] extracted 1484 xors of average arity 3.0
c [gauss-9] connected 4440 occurrences of 318 variables (average 14.0)
c [gauss-9] limit 13247779 penalty 1 = 1 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 3 ternary equations
c [decomp-87] removed 6 variables
c [unhide-14] limit 2500000 with penalty 3 = 3 + 0
c [unhide-14-26] 0 units, 0 failed, 2416 tauts, 0 hbrs, 128930 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 171 transitive binary clauses
c [sweep-20] limit 39743337 penalty 0 = 0 + 0
c [sweep-20-1] 40 pos 50.0% + 40 neg 50.0% = 80 sched 3.7% ret 2076
c [sweep-20-1] 2206264 steps 38 queries 7.71 avg class size
c [sweep-20-1] 1133 decisions 37 SAT calls 76.35 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-88] removed 4 variables
c [sweep-20-1] removed 4 vars (0 failed, 2 eqs, 2 impls)
c [sweep-20-2] 912 pos 42.4% + 1240 neg 57.6% = 2152 sched 100.0% ret 0
c [sweep-20-2] 22334606 steps 221 queries 15.35 avg class size
c [sweep-20-2] 7128 decisions 211 SAT calls 110.38 avg env size
c [sweep-20-2] fully completed sweeping round
c [decomp-89] removed 39 variables
c [sweep-20-2] removed 39 vars (0 failed, 42 eqs, 26 impls)
c [sweep-20-3] 899 pos 42.5% + 1214 neg 57.5% = 2113 sched 100.0% ret 0
c [sweep-20-3] 15718609 steps 104 queries 30.61 avg class size
c [sweep-20-3] 4602 decisions 101 SAT calls 141.83 avg env size
c [sweep-20-3] 288 variables remain 14% (1825 retained 86%)
c [decomp-90] removed 7 variables
c [sweep-20-3] removed 7 vars (0 failed, 8 eqs, 4 impls)
c [sweep-20] removed 50 vars in TOTAL (3 rounds, 360 queries)
c [sort-queue-23] sorted 2106 enqueued variables after 1729807 conflicts
c [score-dist-23] active 0 (0%), one 2106 (100%), zero 0 (0%)
c [score-dist-23] max exp 1, different 1 (50%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 56 variables 2.6% (2106 remain 6%)
c [simplification-23] removed 66 irredundant clauses 0.5% (12089 remain 12%)
c [simplification-23] maximum reduction of 3% = max (3%, 1%)
c [simplification-23] geometric conflict interval increment 103674 = 414699 / 4
c [simplification-23] new conflict interval 518373
c [simplification-23] penalized conflict interval 518373 = 1 * 518373
c [simplification-23] hard conflict limit 2507366 (soft 2248180 + delta 259186)
c [simplification-23] new conflict limit 2248180 (hard 2507366)
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 -  411.1    2106    12089   1744562  119530   4974  3220   11    29   25  38%    346   -1   12   10  120%
c -  426.2    2106    12089   1797479  120264   5009  3227   11    32   25  33%    722   -0   10   10   99%
c i  427.1    2105    12089   1802636  125170   5009  3228   10    34   31  30%    745    2   10   10  104%
c -  437.4    2105    12088   1853004  125141   5015  3230    9    17   26  49%   -356  -14    8   10   84%
c -  451.5    2105    12088   1905742  124909   5023  3233   11    33   26  34%    407    3   12   10  119%
c -  466.6    2105    12088   1961374  126756   5047  3234    9    27   26  32%    760   -3    7   10   67%
c -  483.8    2105    12088   2016912  126659   5066  3238   13    30   26  41%    911   -1   13   10  129%
c -  495.7    2105    12088   2074037  131488   5075  3239    9    34   24  28%    977    4    9   10   87%
c -  510.4    2105    12088   2129030  132821   5080  3243   10    29   24  35%   1004   -3   10   10  100%
c -  527.4    2105    12088   2184835  132360   5099  3246   12    32   24  37%   1015    1   12   10  119%
c -  542.8    2105    12088   2244169  136229   5104  3246   11    31   25  37%   1020    2   13   10  128%
c 
c [simplification-24] limit 2248180 conflicts (hard 2507366) hit after 2248182 conflicts
c [quatres-20] found 8453 quaternary clauses 9% in total
c [quatres-20-1] removed 23 duplicate quaternary clauses
c [quatres-20-1] added 1 double-self-subsuming ternary resolvents
c [quatres-20-2] added 61 single-self-subsuming ternary resolvents
c [quatres-20-2] added 137 quaternary resolvents
c [ternres-20] limit 188641998 with penalty 0 = 0 + 0
c [ternres-20] all 2105 free variables schedulable
c [ternres-20] 754 ternary resolvents (26 bin, 728 trn)
c [ternres-20] fully completed ternary resolution
c [gauss-10] limit 37728399 penalty 0 = 0 + 0
c [gauss-10] extracted 1541 xors of average arity 3.0
c [gauss-10] connected 4599 occurrences of 318 variables (average 14.5)
c [gauss-10] limit 37728399 penalty 0 = 0 + 0
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-91] removed 7 variables
c [treelook-6] limit 2358024 penalty 3 = 3 + 0 boost 1
c [treelook-6] scheduled 3161 literals 75%
c [treelook-6] scheduling used 374791 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2358024 penalty 3 = 3 + 0 boost 1
c [treelook-6] used 1567568 steps
c [treelook-6] fully completed tree based probing
c [decomp-92] removed 7 variables
c [treelook-6] removed 13 variables, found 1212 hbrs
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 317 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 4716049965 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 5 clauses out of 6 (83%) of length 12
c [cce-13-1] eliminated 15 clauses out of 97 (15%) of length 8
c [cce-13-1] eliminated 27 clauses out of 176 (15%) of length 7
c [cce-13-1] eliminated 41 clauses out of 385 (11%) of length 6
c [cce-13-1] eliminated 91 clauses out of 954 (10%) of length 5
c [cce-13-1] eliminated 158 clauses out of 2772 (6%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 337 large clauses in 5203142 steps
c [cce-13-1] allowing another 2601571 steps for small clauses
c [cce-13-1] scheduling 5324 clauses = 1687 binary + 3637 ternary
c [cce-13-1] tried to eliminate 5324 small clauses 100%
c [cce-13-1] eliminated 100 binary clauses 6%
c [cce-13-1] eliminated 102 ternary clauses 3%
c [cce-13-1] eliminated 202 small clauses 4%
c [cce-13-1] eliminated 202 small clauses in 5974260 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 539 covered clauses in round 1
c [cce-13-2] eliminated 4 clauses out of 53 (8%) of length 9
c [cce-13-2] eliminated 7 clauses out of 82 (9%) of length 8
c [cce-13-2] eliminated 10 clauses out of 149 (7%) of length 7
c [cce-13-2] eliminated 2 clauses out of 344 (1%) of length 6
c [cce-13-2] eliminated 8 clauses out of 863 (1%) of length 5
c [cce-13-2] eliminated 53 clauses out of 2614 (2%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 84 large clauses in 4783920 steps
c [cce-13-2] allowing another 2391960 steps for small clauses
c [cce-13-2] scheduling 5122 clauses = 1587 binary + 3535 ternary
c [cce-13-2] tried to eliminate 5122 small clauses 100%
c [cce-13-2] eliminated 19 binary clauses 1%
c [cce-13-2] eliminated 28 ternary clauses 1%
c [cce-13-2] eliminated 47 small clauses 1%
c [cce-13-2] eliminated 47 small clauses in 5570647 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 131 covered clauses in round 2
c [cce-13-3] eliminated 3 clauses out of 2561 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 3 large clauses in 4663321 steps
c [cce-13-3] allowing another 2331660 steps for small clauses
c [cce-13-3] scheduling 5075 clauses = 1568 binary + 3507 ternary
c [cce-13-3] tried to eliminate 5075 small clauses 100%
c [cce-13-3] eliminated 4 binary clauses 0%
c [cce-13-3] eliminated 2 ternary clauses 0%
c [cce-13-3] eliminated 6 small clauses 0%
c [cce-13-3] eliminated 6 small clauses in 5457066 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 9 covered clauses in round 3
c [cce-13] eliminated 679 covered clauses in TOTAL during 3 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2085 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 142 variables 7% in round 1 in 1713483 steps
c [elim-18-1] backward subsumption/strengthening limit 1713400
c [elim-18-1-1] backward checking 370 touched variables 18%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 2 and strengthened 11 clauses in 99586 steps
c [elim-18-1] rescheduled 26 variables 1% by backward subsumption
c [elim-18-2] eliminated 2 variables 0% in round 2 in 13836 steps
c [elim-18-2] backward subsumption/strengthening limit 13800
c [elim-18-2-1] backward checking 10 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 0 and strengthened 5 clauses in 10883 steps
c [elim-18-2] rescheduled 15 variables 1% by backward subsumption
c [elim-18-3] eliminated 2 variables 0% in round 3 in 8562 steps
c [elim-18-3] backward subsumption/strengthening limit 8500
c [elim-18-3-1] backward checking 10 touched variables 0%
c [elim-18-3-1] incomplete backward checking 6 remain 60%
c [elim-18-3] subsumed 0 and strengthened 2 clauses in 8501 steps
c [elim-18] incomplete 7 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 146 = 7% variables out of 2085 scheduled
c [bca-19] limit of 10000000 steps and 22505 added (scaled 2)
c [bca-19] 210 out of 3880 literals actually usable 5%
c [bca-19] added 16 blocked clauses in 133203 steps
c [sweep-21] limit 56592599 penalty 0 = 0 + 0
c [sweep-21-1] 110 pos 43.7% + 142 neg 56.3% = 252 sched 13.0% ret 1687
c [sweep-21-1] 7671367 steps 92 queries 9.39 avg class size
c [sweep-21-1] 2381 decisions 90 SAT calls 84.23 avg env size
c [sweep-21-1] fully completed sweeping round
c [decomp-93] removed 9 variables
c [sweep-21-1] removed 9 vars (0 failed, 8 eqs, 6 impls)
c [sweep-21-2] 759 pos 39.3% + 1171 neg 60.7% = 1930 sched 100.0% ret 0
c [sweep-21-2] 24195135 steps 197 queries 16.39 avg class size
c [sweep-21-2] 6754 decisions 205 SAT calls 101.53 avg env size
c [sweep-21-2] fully completed sweeping round
c [decomp-94] removed 34 variables
c [sweep-21-2] removed 34 vars (0 failed, 34 eqs, 16 impls)
c [sweep-21-3] 745 pos 39.3% + 1151 neg 60.7% = 1896 sched 100.0% ret 0
c [sweep-21-3] 15406763 steps 161 queries 25.55 avg class size
c [sweep-21-3] 4822 decisions 156 SAT calls 86.79 avg env size
c [sweep-21-3] fully completed sweeping round
c [decomp-95] removed 4 variables
c [sweep-21-3] removed 4 vars (0 failed, 5 eqs, 4 impls)
c [sweep-21] removed 47 vars in TOTAL (3 rounds, 447 queries)
c [sort-queue-24] sorted 1892 enqueued variables after 2248182 conflicts
c [score-dist-24] active 0 (0%), one 1892 (100%), zero 0 (0%)
c [score-dist-24] max exp 1, different 1 (50%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 213 variables 10.1% (1892 remain 6%)
c [simplification-24] removed 1161 irredundant clauses 9.6% (10927 remain 11%)
c [simplification-24] maximum reduction of 10% = max (10%, 10%)
c [simplification-24] large reduction 10% >= 5% limit
c [simplification-24] next conflict interval 22481 = min (2248182/100, 518373)
c [simplification-24] penalized conflict interval 22481 = 1 * 22481
c [simplification-24] hard conflict limit 2281903 (soft 2270663 + delta 11240)
c [simplification-24] new conflict limit 2270663 (hard 2281903)
c 
c [simplification-25] limit 2270663 conflicts (hard 2281903) hit after 2270664 conflicts
c [quatres-21] found 7933 quaternary clauses 9% in total
c [quatres-21-1] removed 54 duplicate quaternary clauses
c [quatres-21-1] added 2 double-self-subsuming ternary resolvents
c [quatres-21-2] added 68 single-self-subsuming ternary resolvents
c [quatres-21-2] added 94 quaternary resolvents
c [ternres-21] limit 190740598 with penalty 0 = 0 + 0
c [ternres-21] all 1892 free variables schedulable
c [ternres-21] 438 ternary resolvents (31 bin, 407 trn)
c [ternres-21] fully completed ternary resolution
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 1036 sched 55%, 2 failed, 0 lifted, 85 hbrs
c [decomp-97] removed 3 variables
c [basicprobe-6-1] 1028 sched 54%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-6-2] 1028 sched 54%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-6-3] 1028 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-3] fully completed probing
c [basicprobe-6-3] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-6-3] removed 3 variables, found 117 hbrs
c [bate-5] eliminated 10 asymmetric tautologies during probing
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 184 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 1889 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 60 blocked clauses
c [block-7] 60 < 1/100 * 10833 = 108 considered unsuccessful
c [cce-14] limit of 953702994 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 44 (2%) of length 9
c [cce-14-1] eliminated 1 clauses out of 75 (1%) of length 8
c [cce-14-1] eliminated 1 clauses out of 129 (1%) of length 7
c [cce-14-1] eliminated 3 clauses out of 326 (1%) of length 6
c [cce-14-1] eliminated 16 clauses out of 870 (2%) of length 5
c [cce-14-1] eliminated 49 clauses out of 2490 (2%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 71 large clauses in 2600087 steps
c [cce-14-1] allowing another 1300043 steps for small clauses
c [cce-14-1] scheduling 3477 clauses = 1440 binary + 2037 ternary
c [cce-14-1] tried to eliminate 3477 small clauses 100%
c [cce-14-1] eliminated 7 binary clauses 0%
c [cce-14-1] eliminated 60 ternary clauses 3%
c [cce-14-1] eliminated 67 small clauses 2%
c [cce-14-1] eliminated 67 small clauses in 2973052 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 138 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1258191 steps for small clauses
c [cce-14-2] scheduling 3410 clauses = 1433 binary + 1977 ternary
c [cce-14-2] tried to eliminate 3410 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 138 covered clauses in TOTAL during 2 rounds
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 1889 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 33 variables 2% in round 1 in 1668422 steps
c [elim-19-1] backward subsumption/strengthening limit 1668400
c [elim-19-1-1] backward checking 273 touched variables 14%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 13 clauses in 70342 steps
c [elim-19-1] rescheduled 24 variables 1% by backward subsumption
c [elim-19-2] eliminated 4 variables 0% in round 2 in 63153 steps
c [elim-19-2] backward subsumption/strengthening limit 63100
c [elim-19-2-1] backward checking 12 touched variables 1%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 0 and strengthened 5 clauses in 9560 steps
c [elim-19-2] rescheduled 7 variables 0% by backward subsumption
c [elim-19-3] eliminated 2 variables 0% in round 3 in 1953 steps
c [elim-19-3] backward subsumption/strengthening limit 1900
c [elim-19-3-1] backward checking 13 touched variables 1%
c [elim-19-3-1] incomplete backward checking 3 remain 23%
c [elim-19-3] subsumed 0 and strengthened 0 clauses in 1918 steps
c [elim-19] fully completed in 3 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 39 = 2% variables out of 1889 scheduled
c [bca-20] limit of 10000000 steps and 21483 added (scaled 2)
c [bca-20] 199 out of 3702 literals actually usable 5%
c [bca-20] added 7 blocked clauses in 152229 steps
c [sweep-22] limit 57222179 penalty 0 = 0 + 0
c [sweep-22-1] 797 pos 43.1% + 1053 neg 56.9% = 1850 sched 100.0% ret 0
c [sweep-22-1] 28156585 steps 163 queries 19.96 avg class size
c [sweep-22-1] 6981 decisions 169 SAT calls 116.20 avg env size
c [sweep-22-1] fully completed sweeping round
c [decomp-100] removed 12 variables
c [sweep-22-1] removed 12 vars (0 failed, 14 eqs, 3 impls)
c [sweep-22-2] 792 pos 43.1% + 1046 neg 56.9% = 1838 sched 100.0% ret 0
c [sweep-22-2] 23694690 steps 165 queries 18.54 avg class size
c [sweep-22-2] 5567 decisions 173 SAT calls 113.92 avg env size
c [sweep-22-2] fully completed sweeping round
c [decomp-101] removed 15 variables
c [sweep-22-2] removed 15 vars (0 failed, 16 eqs, 4 impls)
c [sweep-22-3] 787 pos 43.2% + 1036 neg 56.8% = 1823 sched 100.0% ret 0
c [sweep-22-3] 5386356 steps 23 queries 138.26 avg class size
c [sweep-22-3] 1121 decisions 23 SAT calls 136.61 avg env size
c [sweep-22-3] 1202 variables remain 66% (621 retained 34%)
c [sweep-22-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-22] removed 27 vars in TOTAL (3 rounds, 348 queries)
c [sort-queue-25] sorted 1823 enqueued variables after 2270664 conflicts
c [score-dist-25] active 0 (0%), one 1823 (100%), zero 0 (0%)
c [score-dist-25] max exp 1, different 1 (50%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 69 variables 3.6% (1823 remain 5%)
c [simplification-25] removed 486 irredundant clauses 4.5% (10435 remain 11%)
c [simplification-25] maximum reduction of 4% = max (4%, 4%)
c [simplification-25] geometric conflict interval increment 103674 = 518373 / 5
c [simplification-25] new conflict interval 622047
c [simplification-25] penalized conflict interval 622047 = 1 * 622047
c [simplification-25] hard conflict limit 3203734 (soft 2892711 + delta 311023)
c [simplification-25] new conflict limit 2892711 (hard 3203734)
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 -  565.0    1823    10435   2303885  128673   5102  2905   12    28   25  43%   1023    3   13   10  124%
c -  581.3    1823    10435   2365451  130621   5126  2907   10    26   26  37%   1023    1   12   10  117%
c -  596.4    1823    10435   2425519  132902   5149  2915   12    30   26  39%   1024    4   10   10   96%
c -  608.2    1823    10435   2486285  136227   5180  2923    9    24   26  39%   1024   -1   10   10   99%
c i  609.5    1822    10435   2496248  145755   5183  2924   10    25   33  40%   1024   -0   13   10  126%
c i  612.5    1821    10435   2509067  157790   5201  2928   11    27   35  41%  -8030    2   13   10  131%
c i  614.2    1820    10435   2512889  161411   5216  2930   12    25   35  48%  -7704   -0   12   10  120%
c i  616.3    1819    10435   2521353  169526   5229  2931   11    19   36  59%  -6704   -6   12   10  122%
c -  621.0    1819    10435   2550218  136739   5245  2935    9    11   20  84%  -4037  -10    9   10   91%
c i  621.0    1818    10435   2550231  136750   5245  2935    9    10   25  84%  -4036  -10    9   10   88%
c i  623.0    1817    10435   2562890  147411   5252  2938   10    12   27  80%  -3525   -7    9   10   95%
c i  627.2    1816    10435   2586104  166591   5287  2947    7     9   29  86%  -2309   -8    5   10   53%
c i  628.7    1806    10435   2595116  173461   5318  2955    7     9   29  86%  -2202   -7    5    9   58%
c i  629.9    1794    10435   2601183  177541   5359  2967    7     8   31  88%  -2047   -7    5    9   58%
c i  630.3    1783    10435   2603566  179039   5385  2972    7     8   31  89%  -2021   -7    5    9   50%
c i  630.7    1777    10435   2605194  180249   5391  2974    7     8   40  88%  -1983   -7    7    9   76%
c i  630.8    1770    10435   2605937  180756   5412  2979    7     8   40  88%  -1967   -7    5    9   54%
c i  630.9    1763    10435   2606741  181240   5443  2988    6     7   40  88%  -1946   -7    5    9   50%
c i  631.1    1754    10435   2607446  181699   5456  2990    6     7   40  88%  -1927   -7    5    9   58%
c i  631.1    1746    10435   2607543  181760   5460  2994    6     7   40  88%  -1925   -7    5    9   55%
c i  631.1    1741    10435   2607568  181773   5463  2995    6     7   40  88%  -1924   -7    5    9   53%
c i  631.1    1740    10435   2607581  181774   5467  2996    6     7   40  88%  -1924   -7    5    9   52%
c i  631.1    1193    10435   2607582  181774   5467  2996    6     7   40  88%  -1924   -7    5    9   52%
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  631.1    1163    10435   2607583  181774   5467  2996    6     7   40  88%  -1924   -7    5    9   52%
c 0  631.1    1039    10435   2607583  181774   5467  2996    6     7   40  88%  -1924   -7    5    9   52%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 294 basic ate = 205 trn 70% + 89 lrg 30% in 5 updates
c bcas: 20 count, 218 added (126 skipped), 1745416 steps
c bkwd: tried 122486 clauses, 244691 lits, 2.00 lits/clause
c bkwd: checked 27305274 occs, 222.93 occs/clause, 111.59 occs/lit
c bkwd: subsumed 29 binary, 17 ternary, 38 large
c bkwd: strengthened 1 binary, 5 ternary (100% self), 433 large (0% self)
c blkd: 7 bces, 2278 removed, 1352276 resolutions, 3411152 steps
c blkd: 2073 blocking literals 3%, 83 pure
c bump: 2633612 bumped seen, 158555728 lits 60.2 on average
c card: 6 count, 0 units, 21 am1, 13790964 steps
c card: 17 rescheduled, 168 eliminated, 10074 resolved, 4743 subsumed
c card: 1075 at-most-one constraints found, average size 3.03
c card: 1075 at-most-one constraints used 100%, average size 3.03
c card: 48 at-most-two constraints found, average size 4.00
c card: 48 at-most-two constraints used 100%, average size 4.00
c cces: 14 cces, 8980 eliminated, 7229 ate 81%, 1751 abce 19%
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: 324372 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 164 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 102 decompositions, 2979 equivalent 9%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 8674179 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 19 elims, 26567 eliminated 80%, 233 pure 1%
c elms: 61 rounds, 3.2 rounds/bve
c elms: 24967 small 94%, 1284 large 5%
c elms: 51905 tried small, 24967 succeeded 48%, 26938 failed 52%
c elms: 3419 subsumed, 3763 strengthened, 633 blocked
c elms: 3375018 copies, 4516069 resolutions, 1769345 ipos
c elms: 1476939 subchks, 936753 strchks
c gaus: 10 extractions, 21446 extracted, 2.9 size, 4 max
c gaus: exported 2 units, 57 binary and 17 ternary equations
c gaus: 0 gc, 23734576 steps, 11867288 extr 50%, 1217716 elim 5%
c glue: 9.3 orig avg, 9.3 real avg, 2.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 45458 = 7798 simple 17% + 34902 trn 77% + 2758 lrg 6%, 1060 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2633612 clauses, 26.8 length
c lrnd: 70599820 lits = 99871264 orig - 29271444 removed 29%
c lrnd: 503534 uips 19%, 1940277 flips 74%
c mins: 2609757 mins 99%, 711 bin 0%, 23144 size 1%
c mins: 119639388 poisoned searches, 18811072 hits, 16% hit rate
c mins: 197948623 used twice searches, 9615609 hits, 5% hit rate
c move: moved 4825, 1380 bin 29%, 3445 trn 71%
c otfs: 10433 driving 30%, 24407 restarting 70%
c otfs: str 34840, 34471 red 99%, 369 irr 1%
c otfs: str 34840, 0 bin 0%, 818 trn 2%, 34022 lrg 98%
c otfs: sub 628, 587 red 93%, 41 irr 7%
c otfs: sub 628, 0 bin 0%, 63 trn 10%, 565 lrg 90%
c phas: 1 computed, 8746 set, 2347 pos (27%), 6399 neg (73%)
c prbs: 6 basic, 137136 probed, 112 failed, 11 lifted
c prbs: 6 simple, 110655 probed, 92 failed, 1832 eqs
c prbs: 6 treelook, 3500 probed, 5 failed, 0 lifted
c prom: 893076 locked 14% out of 6216731 tried
c prps: 421981934 props, 47 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 21 count, 5136 quat, 1966 self1, 61 self2, 982 dup
c queu: 25 sorted, 8674179 next (118 steps 0.00)
c queu: 158732098 enq (158732052 steps 1.00), 158555728 deq 100%
c redc: 88035 clauses 14%, 638917 tried 25%, 11 sat 0%
c redc: 123368 lits 1%, 10074148 tried 10%, 11 sat 0%
c redc: 1147 times jump level reduced, 4.9 levels on average
c reds: 51 count, 51129.1 conflicts per reduce
c reds: 0 memlim 0%, 51 arith 100%
c reds: 1912619 collected 87%, 291189 retired 13%
c rmbd: 2097 removed, 1532 red 73%
c rsts: 75275 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 25 count, 23 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 2633612 count (1076050 tried 0.4), 149256 sub out of 2625051 (5.7%)
c swps: 22 count, 39 rounds, 7795 queries (199.9/round)
c swps: 7568 sat calls, 870 unsat (4.8% success rate)
c swps: 188021 decisions 24.8, 36462 conflicts 4.8
c swps; 58.0 avg class size, 73.3 avg environment size
c swps: 0 failed, 811 impls, 1090 equivs
c swp0: 2583 type 0 queries, 635 unsat (24.6%), 2374 sat (91.9%)
c swp1: 5212 type 1 queries, 2442 unsat (46.9%), 4331 sat (83.1%)
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: 22616193 calls to obtain time
c tops: 2691 fixed 8%, 67 its, 38919.15 confs/it
c trds: 21 transitive reductions, 6794 removed, 26 failed
c trds: 152032 nodes, 170853 edges, 28904776 steps
c trim: 1020770 words, 3.9 MB
c trnr: 21 count, 863 bin, 40720 trn, 416419769 steps
c unhd: 14 count, 26 rounds, 34589860 steps
c unhd: 178 non-trivial sccs of average size 2.0
c unhd: 11 units, 11 bin, 0 trn, 0 lrg
c unhd: 51 failed, 50 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 17713 tauts, 253 bin 1%, 5925 trn 33%, 4948 lrg 28%
c unhd: 17713 tauts, 6587 stamp 37%, 17488 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 437339 str, 11 bin 0%, 1072 trn 0%, 436256 lrg 100%, 434548 red 99%
c vars: 1042 remaining 3% and 32237 removed 97% out of 33279
c vars: 2691 fixed 8%, 26567 eliminated 80%, 2979 equivalent 9%
c vsts: 23197412891 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 56.1 search visits per propagation, 8708.8 per conflict
c wchs: 9015514645 pushed, 9932122 enlarged, 303 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2630187       1912619        291189      99207702      28764148       1664083
c 
c  0 0        272528  10    110560   6         0   0  71086113  72< 16522405  57    736154  44     4.1
c  1 5        221996   8    160594   8     30608  11  11815537  12   4001252  14<   235974  14<    1.0
c  2 6        820452  31<   641912  34<    80772  28  12074296  12   5384357  19    416986  25     3.1
c  3 9        928239  35    726571  38     98653  34<  3495230   4   2333926   8    228054  14     4.9
c  4 14       326221  12    235691  12     61835  21    648590   1    470678   2     43651   3     1.8
c  5 21        52651   2     32854   2     16189   6     71470   0     45757   0      2991   0     0.4
c  6 30         7077   0      3913   0      2703   1     15172   0      5101   0       239   0     0.1
c  7 41          857   0       437   0       359   0      1085   0       566   0        32   0     0.0
c  8 54          149   0        79   0        61   0       185   0        98   0         2   0     0.0
c  9 69           15   0         8   0         7   0        21   0         8   0         0   0     0.0
c 10 86            2   0         0   0         2   0         3   0         0   0         0   0     0.0
c 
c avg                  2.4           2.5           2.9           0.5           0.8           1.2
c std                  1.2           1.1           1.1           0.9           1.1           1.2
c 
c   17.697   3% cce
c   16.558   3% sweep
c    8.236   1% bump
c    6.091   1% probe
c    5.635   1% decide
c    5.315   1% ternres
c    5.164   1% elim
c 
c   10.046 < 1% rest (below)
c 
c    4.242   1% unhide
c    1.902   0% transred
c    1.592   0% quatres
c    0.916   0% gauss
c    0.794   0% bca
c    0.457   0% block
c    0.142   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.939   0% preprocessing     1%
c   62.238  10% inprocessing     99%
c ==================================
c   63.177  10% simplifying
c  567.908  90% search
c ==================================
c  631.087 100% all
c 
c       2607583 conflicts,        4131.9 confs/sec
c          5006 ternaries,         520.9 confs/ternary
c           764 binaries,         3413.1 confs/binary
c            67 iterations,      38919.1 confs/iteration
c 
c            51 reductions,          0.1 redus/sec,  51129.1 confs/reduction
c         75275 restarts,          119.3 rests/sec,     34.6 confs/restart
c       8674179 decisions,       13744.8 decis/sec,      3.3 decis/conflict
c     421981934 propagations,   668659.2 props/sec,     48.6 props/decision
c 
c 631.1 seconds, 57.2 MB
c launch: done
