c launch: /data/cnf/sc2014/app/ACG-20-5p1.cnf.bz2
c host: atom22
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/ACG-20-5p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ACG-20-5p1.cnf.bz2
c no embedded options
c found 'p cnf 331196 1416850' header
c read 331196 variables, 1416850 clauses, 3333531 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 --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 319793 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 
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  319793  1404697         0       0      0     0    0     0   64   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 5850 at-most-one constraints of average size 5.5
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 5850 out of 5850 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51681 variables
c [simpleprobe-1] all 279515 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 581 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 581 variables, found 13886 hbrs, 20 units
c [unhide-1] limit 71153 based on 1138458 irredundant clauses
c [unhide-1-1] 23 units, 2177 failed, 16953 tauts, 0 hbrs, 9933 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 266243 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 105188 not tried 40% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 112696 = 42% variables out of 266243 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 907028 negative 99.4% of 912791 except 5763 0.6%
c [phase-count-1] 758363 positive 83.1% of 912791 except 154428 16.9%
c [phase-count-1] less non-negative clauses 5763 than limit 91200 (10.0%)
c [phase-count-1] non-pos/non-neg = 154428/5763 = 26.80 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 153547 negative 100%
c [sort-queue-1] sorted 153547 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 153547 (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 130805 variables 46.0% (153547 remain 48%)
c [simplification-1] removed 491906 irredundant clauses 35.0% (912791 remain 65%)
c [simplification-1] maximum reduction of 46% = max (46%, 35%)
c [simplification-1] large reduction 46% >= 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    6.8  153546   912791        65      58      2  6311    0     9   63   2%      0    9    2    0 23234%
c i    6.8  151790   912791        68      59      3  6311    0     9   63   2%      0    9    2    0 22998%
c i    6.8  149355   912791        69      59      3  6311    0     9   63   2%      0    9    2    0 22909%
c i    6.8  149280   912791       119      88     12  6320    0    11   63   2%      0   10    2    0 20150%
c i    6.9  147370   912791       137      97     14  6324    0    11   63   2%      0   11    2    0 19158%
c i    6.9  146134   912791       156     108     16  6329    0    11   63   2%      0   11    3    0 18350%
c i    7.0  146109   912791       216     154     21  6333    0    13   63   3%      0   13    4    0 17274%
c i    7.0  146098   912791       217     154     21  6333    0    13   63   3%      0   12    4    0 17207%
c i    7.2  145984   912791       367     265     36  6345    1    15   64   4%      0   15    5    0 14112%
c i    7.2  144602   912791       373     270     36  6345    1    15   64   4%      0   15    5    0 13924%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 12289 variables
c [simpleprobe-2] all 141258 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 84 variables
c [simpleprobe-2] 133127 variables remain 94% (8047 retained 6%)
c [simpleprobe-2] removed 84 variables, found 3035 hbrs, 9 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 123860 literals 44%
c [treelook-1] scheduling used 676946 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 463455 steps
c [treelook-1] 123855 literals remain 44%
c [treelook-1] 120812 variables remain to probed next time 86%
c [decomp-5] removed 1 variables
c [treelook-1] removed 1 variables, found 3800 hbrs
c [basicprobe-1] limit 6667856 based on 833482 irredundant clauses
c [basicprobe-1-0] 30760 probes remain 25% after last round
c [basicprobe-1-0] 47 units = 47 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 17636 variables, found 13993 hbrs
c [unhide-2] limit 52092 based on 833482 irredundant clauses
c [unhide-2-2] 7 units, 2250 failed, 2669 tauts, 0 hbrs, 24131 literals
c [elim-2] 82549 variables 70% will be scheduled this time
c [elim-2] scheduled 82549 variables 70%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 18850 not tried 16% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 5097 = 6% variables out of 82549 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 647499 negative 99.1% of 653326 except 5827 0.9%
c [phase-count-2] 533424 positive 81.6% of 653326 except 119902 18.4%
c [phase-count-2] less non-negative clauses 5827 than limit 65300 (10.0%)
c [phase-count-2] non-pos/non-neg = 119902/5827 = 20.58 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 11924 negative 100%
c [sort-queue-2] sorted 113176 enqueued variables after 373 conflicts
c [score-dist-2] active 0 (0%), one 10224 (9%), zero 102952 (91%)
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 28920 variables 20.4% (113176 remain 35%)
c [simplification-2] removed 259465 irredundant clauses 28.4% (653326 remain 47%)
c [simplification-2] maximum reduction of 28% = max (20%, 28%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1024 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.1  113175   653326       374     229     32 16493    1    15   49   4%      0   15    5    0 13870%
c i   12.1  112486   653326       396     248     33 16494    1    16   49   4%      0   16    6    0 13741%
c i   12.2  112476   653326       542     374     40 16503    1    18   49   5%      0   18    6    0 10917%
c i   12.2  112463   653326       563     386     43 16507    1    18   49   5%      0   18    6    0 10530%
c i   12.2  112460   653326       564     386     43 16507    1    18   49   5%      0   18    6    0 10489%
c i   12.2  111864   653326       565     386     43 16507    1    18   49   5%      0   18    6    0 10448%
c i   12.5  111862   653326       848     594     74 16538    1    22   49   6%      1   22    7    0 8101%
c i   12.5  111855   653326       886     625     74 16543    1    23   49   6%      1   23    7    0 7681%
c i   12.5  111840   653326       929     660     78 16546    1    23   49   6%      1   23    7    0 7190%
c i   12.6  111796   653326       953     680     79 16546    1    24   49   6%      1   23    7    0 7003%
c i   12.6  110787   653326       957     682     79 16547    1    23   49   6%      1   23    7    0 6998%
c i   12.6  110775   653326      1015     726     86 16553    2    24   49   6%      1   24    7    0 6340%
c i   12.6  110754   653326      1016     726     86 16553    2    24   49   6%      1   24    7    0 6316%
c 
c [simplification-3] limit 1066 conflicts (hard 11000) hit after 1066 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3614 at-most-one constraints of average size 4.3
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3614 out of 3614 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 3629 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 68781 literals 31%
c [treelook-2] scheduling used 332672 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 307253 steps
c [treelook-2] 68767 literals remain 31%
c [treelook-2] 57783 variables remain to probed next time 53%
c [decomp-7] removed 3 variables
c [treelook-2] removed 9 variables, found 2000 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 5 units, 781 failed, 11704 tauts, 0 hbrs, 9362 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 107661 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 25004 not tried 23% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 4670 = 4% variables out of 107661 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 593438 negative 99.1% of 599005 except 5567 0.9%
c [phase-count-3] 487443 positive 81.4% of 599005 except 111562 18.6%
c [phase-count-3] less non-negative clauses 5567 than limit 59900 (10.0%)
c [phase-count-3] non-pos/non-neg = 111562/5567 = 20.04 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 10811 negative 100%
c [sort-queue-3] sorted 102991 enqueued variables after 1066 conflicts
c [score-dist-3] active 0 (0%), one 12878 (13%), zero 90113 (87%)
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 7760 variables 7.0% (102991 remain 32%)
c [simplification-3] removed 54321 irredundant clauses 8.3% (599005 remain 43%)
c [simplification-3] maximum reduction of 8% = max (7%, 8%)
c [simplification-3] large reduction 8% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13066 (soft 3066 + delta 10000)
c [simplification-3] new conflict limit 3066 (hard 13066)
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   16.4  102990   599005      1067     647     89 14832    2    25   47   7%      1   25    8    0 6999%
c i   16.4  102986   599005      1075     654     89 14832    2    26   47   7%      1   25    8    0 6954%
c i   16.4  102981   599005      1103     671     92 14838    2    26   47   7%      1   26    8    0 6529%
c i   16.5  102980   599005      1123     687     92 14840    2    26   47   7%      1   26    8    0 6398%
c i   16.5  102930   599005      1197     743    100 14848    2    27   47   7%      1   27    8    0 5969%
c i   16.7  102929   599005      1484     967    130 14877    2    32   47   7%      1   31    7    0 4467%
c i   16.8  102927   599005      1538    1005    137 14884    2    33   47   7%      1   32    7    0 4440%
c i   16.8  102922   599005      1581    1038    140 14888    2    33   47   7%      1   32    7    0 4247%
c i   16.9  102914   599005      1747    1182    145 14902    3    36   47   7%      1   36   10    0 4744%
c i   17.0  102911   599005      1789    1214    149 14907    3    37   47   7%      1   36    9    0 4556%
c i   17.0  102903   599005      1815    1236    150 14909    3    37   47   7%      1   37    9    0 4325%
c 
c [simplification-4] limit of 196 binary hit after 196 binaries
c [decomp-8] removed 165 variables
c [basicprobe-2] limit 4784704 based on 598088 irredundant clauses
c [basicprobe-2-0] 28002 probes remain 28% after last round
c [basicprobe-2-0] 46 units = 46 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1816 variables, found 11148 hbrs
c [unhide-4] limit 112010 with penalty 0 = 0 + 0
c [unhide-4-4] 10 units, 1040 failed, 3191 tauts, 0 hbrs, 8003 literals
c [elim-4] 17632 variables 18% will be scheduled this time
c [elim-4] scheduled 17632 variables 18%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 27 variables 0% in round 1 in 24972179 steps
c [elim-4-1] backward subsumption/strengthening limit 24972100
c [elim-4-1-1] backward checking 9492 touched variables 10%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 293 and strengthened 38 clauses in 1503602 steps
c [elim-4-1] rescheduled 888 variables 1% by backward subsumption
c [elim-4-2] eliminated 162 variables 0% in round 2 in 524296 steps
c [elim-4-2] backward subsumption/strengthening limit 524200
c [elim-4-2-1] backward checking 1140 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 121 and strengthened 88 clauses in 412792 steps
c [elim-4-2] rescheduled 503 variables 1% by backward subsumption
c [elim-4-3] eliminated 27 variables 0% in round 3 in 457591 steps
c [elim-4-3] backward subsumption/strengthening limit 457500
c [elim-4-3-1] backward checking 215 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 13 and strengthened 1 clauses in 163711 steps
c [elim-4] incomplete 33 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 218 = 1% variables out of 17632 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 557122 negative 99.0% of 562686 except 5564 1.0%
c [phase-count-4] 454269 positive 80.7% of 562686 except 108417 19.3%
c [phase-count-4] less non-negative clauses 5564 than limit 56200 (10.0%)
c [phase-count-4] non-pos/non-neg = 108417/5564 = 19.49 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 10124 negative 100%
c [sort-queue-4] sorted 98667 enqueued variables after 2244 conflicts
c [score-dist-4] active 0 (0%), one 15588 (16%), zero 83079 (84%)
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 4229 variables 4.1% (98667 remain 31%)
c [simplification-4] removed 36319 irredundant clauses 6.1% (562686 remain 40%)
c [simplification-4] maximum reduction of 6% = max (4%, 6%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3067 (hard 13066)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.2   98666   562686      2320    1622    191 20443    4    48   45   8%      2   47   13    0 4162%
c i   19.3   98656   562686      2330    1629    191 20445    4    48   45   8%      2   47   12    0 4042%
c i   19.3   98655   562686      2431    1709    201 20451    4    50   45   8%      2   49   11    0 3482%
c i   19.4   98647   562686      2534    1796    208 20459    4    50   45   8%      2   49   10    0 3040%
c i   19.5   98639   562686      2697    1924    222 20474    5    54   45   8%      2   53   12    0 3392%
c i   19.5   98636   562686      2709    1931    225 20475    5    54   45   8%      2   53   12    0 3303%
c i   19.5   98635   562686      2710    1931    225 20475    5    54   45   8%      2   53   12    0 3290%
c i   19.7   98634   562686      2963    2139    248 20491    5    58   45   9%      2   57   13    0 3140%
c i   19.8   98633   562686      3041    2203    254 20495    5    59   45   9%      2   57   12    0 2762%
c i   19.8   98629   562686      3068    2225    258 20495    5    60   45   9%      2   58   14    0 3160%
c 
c [simplification-5] limit 3078 conflicts (hard 13066) hit after 3078 conflicts
c [quatres-1] found 40513 quaternary clauses 46% in total
c [quatres-1-2] added 34 single-self-subsuming ternary resolvents
c [quatres-1-2] added 8 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 98610 free variables schedulable
c [ternres-1] 2018 ternary resolvents (16 bin, 2002 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1177 xors of average arity 2.0
c [gauss-1] connected 2407 occurrences of 1285 variables (average 1.9)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 1210 variables
c [gauss-1] exported 0 unary, 4 binary and 0 ternary equations
c [decomp-10] removed 2 variables
c [simpleprobe-3] 91866 schedulable variables 94%
c [simpleprobe-3] limit 2968123 penalty 0 = 0 + 0
c [decomp-11] removed 1148 variables
c [simpleprobe-3] 57557 variables remain 60% (38693 retained 40%)
c [simpleprobe-3] removed 1148 variables, found 7420 hbrs, 138 units
c [unhide-5] limit 148406 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 317 failed, 7734 tauts, 0 hbrs, 3479 literals
c [transred-1] limit 742030 with penalty 0 = 0 + 0
c [transred-1] removed 53 transitive binary clauses
c [transred-1] found 2 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 95509 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 7518 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 10 clauses out of 167 (6%) of length 10
c [cce-1-1] eliminated 38 clauses out of 682 (6%) of length 9
c [cce-1-1] eliminated 61 clauses out of 583 (10%) of length 8
c [cce-1-1] eliminated 175 clauses out of 1043 (17%) of length 7
c [cce-1-1] eliminated 3183 clauses out of 4781 (67%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3467 large clauses in 30000001 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 327193 clauses = 271485 binary + 55708 ternary
c [cce-1-1] tried to eliminate 345 small clauses 0%
c [cce-1-1] eliminated 98 binary clauses 0%
c [cce-1-1] eliminated 15 ternary clauses 0%
c [cce-1-1] eliminated 113 small clauses 0%
c [cce-1-1] eliminated 113 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3580 covered clauses in round 1
c [cce-1] eliminated 3580 covered clauses in TOTAL during 1 rounds
c [cce-1] 3580 < 1/100 * 531896 = 5318 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 95509 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 15304 not tried 16% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2487 = 3% variables out of 95509 scheduled
c [bca-1] limit of 10000000 steps and 1049860 added (scaled 2)
c [bca-1] 177491 out of 186046 literals actually usable 95%
c [bca-1] added 201 blocked clauses in 515364 steps
c [sweep-1] limit 1049360 based on 524680 irredundant clauses
c [sweep-1-1] 3569 pos 3.8% + 89453 neg 96.2% = 93022 sched 100.0% ret 0
c [sweep-1-1] 1159949 steps 14 queries 23603.36 avg class size
c [sweep-1-1] 131 decisions 11 SAT calls 59.91 avg env size
c [sweep-1-1] 92995 variables remain 100% (27 retained 0%)
c [decomp-12] removed 16 variables
c [sweep-1-1] removed 16 vars (0 failed, 2 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 16 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-5] 522302 negative 99.6% of 524650 except 2348 0.4%
c [phase-count-5] 426430 positive 81.3% of 524650 except 98220 18.7%
c [phase-count-5] less non-negative clauses 2348 than limit 52400 (10.0%)
c [phase-count-5] non-pos/non-neg = 98220/2348 = 41.83 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 9563 negative 100%
c [sort-queue-5] sorted 93006 enqueued variables after 3078 conflicts
c [score-dist-5] active 0 (0%), one 16441 (18%), zero 76565 (82%)
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 5604 variables 5.7% (93006 remain 29%)
c [simplification-5] removed 38036 irredundant clauses 6.8% (524650 remain 37%)
c [simplification-5] maximum reduction of 7% = max (6%, 7%)
c [simplification-5] large reduction 7% >= 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 15078 (soft 5078 + delta 10000)
c [simplification-5] new conflict limit 5078 (hard 15078)
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   25.8   93005   524650      3133    2032   1547 34323    5    63   44   9%      2   61   13    0 2953%
c i   25.8   93004   524650      3150    2044   1549 34325    5    63   44   9%      2   61   13    0 2835%
c i   25.9   92992   524650      3174    2065   1550 34326    5    63   44   9%      2   61   12    0 2730%
c i   25.9   92981   524650      3204    2087   1552 34329    5    63   44   8%      2   61   12    0 2567%
c i   25.9   92979   524650      3267    2142   1556 34331    5    63   44   9%      1   62   11    0 2446%
c i   25.9   92973   524650      3271    2145   1556 34331    5    63   44   9%      1   62   11    0 2424%
c i   26.0   92971   524650      3329    2193   1560 34335    6    65   44   8%      1   63   11    0 2369%
c i   26.0   92908   524650      3400    2249   1566 34340    6    65   44   9%      1   63   10    0 2147%
c i   26.0   92904   524650      3415    2261   1568 34340    6    65   44   9%      1   63   10    0 2078%
c i   26.2   92901   524650      3581    2389   1580 34360    6    66   44   8%      1   64    9    0 1831%
c i   26.2   92893   524650      3604    2406   1583 34362    6    67   44   8%      1   65    9    0 1735%
c i   26.5   92887   524650      3854    2590   1615 34390    6    69   44   8%      1   67    7    1 1346%
c i   26.5   92836   524650      3859    2594   1615 34390    6    69   44   8%      1   67    7    1 1332%
c i   26.5   92835   524650      3892    2617   1619 34393    6    69   44   8%      1   67    7    1 1374%
c i   26.5   92833   524650      3958    2677   1623 34394    6    69   44   8%      1   67    8    1 1467%
c i   26.7   92831   524650      4111    2792   1640 34410    6    71   44   8%      1   68    8    1 1409%
c i   26.7   92824   524650      4137    2810   1645 34412    6    71   44   8%      1   68    7    1 1357%
c i   26.7   92818   524650      4148    2812   1646 34416    6    71   44   8%      1   68    7    1 1319%
c i   26.9   92708   524650      4443    3062   1660 34441    6    76   44   8%      2   73   10    1 1635%
c i   26.9   92705   524650      4455    3070   1661 34442    6    76   44   8%      2   73   10    1 1588%
c i   26.9   92515   524650      4481    3088   1664 34446    6    76   44   8%      1   73    9    1 1505%
c i   27.0   92357   524650      4554    3154   1665 34448    6    76   44   9%      1   73   12    1 1926%
c i   27.0   92343   524650      4583    3175   1666 34454    7    76   44   9%      1   73   12    1 1896%
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   27.4   92328   524650      4976    3494   1694 34488    7    85   45   8%      2   81   13    1 1805%
c i   27.4   92323   524650      4986    3500   1695 34490    7    85   45   8%      2   82   13    1 1758%
c i   27.4   92317   524650      4987    3500   1695 34490    7    85   45   8%      2   82   12    1 1751%
c i   27.4   92307   524650      5000    3510   1695 34490    7    85   45   8%      2   81   12    1 1705%
c i   27.4   92306   524650      5028    3528   1699 34495    7    86   45   8%      2   82   12    1 1629%
c i   27.4   92160   524650      5056    3547   1700 34502    7    85   45   8%      2   82   11    1 1515%
c i   27.5   92159   524650      5081    3564   1700 34508    7    86   45   8%      2   82   11    1 1507%
c 
c [simplification-6] limit 5093 conflicts (hard 15078) hit after 5093 conflicts
c [quatres-2] found 41188 quaternary clauses 50% in total
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 23 single-self-subsuming ternary resolvents
c [quatres-2-2] added 44 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 92156 free variables schedulable
c [ternres-2] 538 ternary resolvents (0 bin, 538 trn)
c [ternres-2] 41124 variables remain 45% (51032 retained 55%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2798 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2798 out of 2798 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 114 xors of average arity 2.5
c [gauss-2] connected 285 occurrences of 235 variables (average 1.2)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-13] removed 63 variables
c [gauss-2] exported 1 unary, 1 binary and 0 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 56430 literals 31%
c [treelook-3] scheduling used 309249 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 305709 steps
c [treelook-3] 56425 literals remain 31%
c [treelook-3] 32883 variables remain to probed next time 36%
c [treelook-3] removed 0 variables, found 2221 hbrs
c [unhide-6] limit 242015 with penalty 0 = 0 + 0
c [unhide-6-6] 15 units, 319 failed, 2736 tauts, 0 hbrs, 5127 literals
c [transred-2] limit 1210079 with penalty 0 = 0 + 0
c [transred-2] removed 143 transitive binary clauses
c [transred-2] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 91004 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 1143 blocked clauses
c [block-2] 1143 < 1/100 * 518758 = 5187 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 90991 variables 100%
c [elim-6] limit of 24201584 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 8220 not tried 9% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1330 = 1% variables out of 90991 scheduled
c [bca-2] limit of 10000000 steps and 1010140 added (scaled 2)
c [bca-2] 168514 out of 179324 literals actually usable 94%
c [bca-2] added 119 blocked clauses in 487434 steps
c [sweep-2] limit 1009540 based on 504770 irredundant clauses
c [sweep-2-1] 4023 pos 4.5% + 85616 neg 95.5% = 89639 sched 100.0% ret 22
c [sweep-2-1] 1413754 steps 12 queries 18999.33 avg class size
c [sweep-2-1] 32 decisions 10 SAT calls 31.50 avg env size
c [sweep-2-1] 89616 variables remain 100% (45 retained 0%)
c [decomp-16] removed 79 variables
c [sweep-2-1] removed 79 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 79 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-6] 502369 negative 99.5% of 504661 except 2292 0.5%
c [phase-count-6] 408630 positive 81.0% of 504661 except 96031 19.0%
c [phase-count-6] less non-negative clauses 2292 than limit 50400 (10.0%)
c [phase-count-6] non-pos/non-neg = 96031/2292 = 41.90 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 6372 negative 100%
c [sort-queue-6] sorted 89582 enqueued variables after 5093 conflicts
c [score-dist-6] active 0 (0%), one 19862 (22%), zero 69720 (78%)
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 2574 variables 2.8% (89582 remain 28%)
c [simplification-6] removed 19989 irredundant clauses 3.8% (504661 remain 36%)
c [simplification-6] maximum reduction of 4% = max (3%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 19093 (soft 9093 + delta 10000)
c [simplification-6] new conflict limit 9093 (hard 19093)
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   32.1   89581   504661      5119    3344   1702 35350    7    87   44   8%      2   83   10    1 1399%
c i   32.1   89578   504661      5123    3347   1702 35350    7    87   44   8%      2   83   10    1 1379%
c i   32.1   89577   504661      5136    3358   1703 35350    7    87   44   8%      2   83   10    1 1383%
c i   32.1   89575   504661      5137    3358   1703 35350    7    87   44   8%      2   83   10    1 1378%
c i   32.1   89566   504661      5139    3358   1703 35351    7    86   44   8%      2   83   10    1 1368%
c i   32.2   89555   504661      5222    3426   1708 35359    7    88   44   8%      2   84   11    1 1439%
c i   32.4   89550   504661      5578    3715   1736 35391    7    90   44   8%      2   86   10    1 1282%
c i   32.6   89549   504661      5779    3876   1752 35412    8    91   44   8%      2   86   10    1 1205%
c i   32.7   89535   504661      5875    3958   1758 35418    8    92   44   8%      2   87   11    1 1286%
c i   32.9   89534   504661      6027    4092   1763 35424    8    92   44   9%      2   87   13    1 1530%
c i   33.0   89530   504661      6158    4188   1776 35442    8    96   44   9%      2   91   14    1 1572%
c i   33.0   89527   504661      6191    4218   1776 35442    8    96   44   9%      2   91   14    1 1568%
c i   33.1   89523   504661      6243    4260   1779 35447    8    96   44   9%      1   91   15    1 1600%
c i   33.1   88879   504661      6249    4262   1780 35449    8    96   44   9%      1   91   15    1 1569%
c i   33.1   88860   504661      6259    4263   1783 35452    8    96   44   9%      1   91   14    1 1524%
c i   33.1   88846   504661      6261    4264   1783 35452    8    96   44   9%      1   91   14    1 1513%
c i   33.2   88833   504661      6401    4374   1799 35465    9   101   44   8%      1   95   12    1 1251%
c i   33.2   88651   504661      6443    4406   1802 35469    9   100   44   9%      1   95   12    1 1220%
c i   33.3   88642   504661      6505    4445   1811 35482    8    99   44   8%      1   94   10    1 1019%
c i   33.4   88593   504661      6610    4518   1828 35494    8    99   44   8%      1   94    8    1  829%
c i   33.4   88584   504661      6634    4527   1831 35498    8    99   44   8%      1   93    8    1  790%
c i   33.4   88578   504661      6680    4559   1837 35505    8    98   44   8%      1   93    7    1  724%
c i   33.4   88569   504661      6683    4561   1837 35505    8    98   44   8%      1   93    7    1  717%
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   33.4   88568   504661      6684    4561   1837 35505    8    98   44   8%      1   93    7    1  714%
c i   33.4   88567   504661      6685    4561   1837 35505    8    98   44   8%      1   93    7    1  712%
c i   33.4   88566   504661      6693    4561   1839 35510    8    98   44   8%      1   92    7    1  694%
c i   33.5   88560   504661      6735    4586   1843 35522    8    98   44   8%      1   92    6    1  637%
c i   33.5   88558   504661      6746    4594   1844 35522    8    98   44   8%      1   92    7    1  717%
c i   33.5   88551   504661      6768    4612   1845 35523    8    98   44   8%      1   92    7    1  730%
c i   33.5   88543   504661      6782    4622   1846 35525    8    98   44   8%      1   92    7    1  712%
c i   33.6   88527   504661      6874    4687   1856 35540    8    98   44   8%      1   92    6    1  608%
c i   33.6   88418   504661      6905    4708   1860 35545    8    98   44   8%      1   91    6    1  604%
c i   33.7   88402   504661      6923    4720   1862 35548    8    98   44   8%      1   91    6    1  596%
c i   33.7   88200   504661      6952    4745   1862 35551    8    98   44   8%      1   92    6    1  592%
c i   33.7   88194   504661      6981    4769   1863 35554    8    98   44   8%      1   92    6    1  576%
c i   33.9   88192   504661      7068    4829   1874 35565    8   101   44   8%      1   94    5    1  557%
c i   33.9   88185   504661      7070    4830   1874 35565    8   101   44   8%      1   94    5    1  555%
c i   33.9   88141   504661      7119    4862   1880 35574    8   102   44   8%      1   95    6    1  576%
c i   34.0   88139   504661      7155    4887   1884 35580    8   101   44   8%      1   95    5    1  554%
c i   34.0   88136   504661      7156    4887   1884 35580    8   101   44   8%      1   95    5    1  552%
c i   34.0   88130   504661      7207    4925   1888 35586    8   101   44   8%      1   94    6    1  556%
c i   34.0   88119   504661      7221    4932   1891 35589    8   100   44   8%      1   94    5    1  535%
c i   34.1   87851   504661      7283    4969   1898 35605    8   100   44   8%      1   93    5    1  524%
c i   34.4   87836   504661      7512    5144   1921 35633    8   102   44   8%      1   95    6    1  565%
c i   34.4   87831   504661      7527    5156   1921 35635    8   101   44   8%      1   94    6    1  551%
c i   34.4   87826   504661      7532    5157   1922 35637    8   101   44   8%      1   94    6    1  543%
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   34.5   87806   504661      7564    5181   1925 35641    8   102   44   8%      1   95    5    1  533%
c i   34.5   87726   504661      7569    5182   1926 35643    8   102   44   8%      1   95    5    1  525%
c i   34.5   87680   504661      7580    5190   1928 35643    8   101   44   8%      1   94    5    1  518%
c i   34.5   87510   504661      7601    5207   1930 35644    8   101   44   8%      1   94    5    1  530%
c i   34.6   87503   504661      7633    5232   1932 35648    8   102   44   8%      1   95    5    1  535%
c i   34.6   87502   504661      7670    5260   1935 35653    8   102   44   8%      1   95    5    1  527%
c i   34.7   87354   504661      7710    5291   1938 35655    8   101   44   8%      1   94    5    1  512%
c i   34.7   87348   504661      7712    5291   1938 35656    8   101   44   8%      1   94    5    1  508%
c i   34.7   87314   504661      7714    5291   1938 35657    8   101   44   8%      1   94    5    1  505%
c i   34.7   87307   504661      7736    5308   1940 35659    8   101   44   8%      1   94    5    1  512%
c i   34.9   87305   504661      7978    5493   1968 35682    8   103   44   8%      1   95    9    1  834%
c i   35.0   87294   504661      7999    5507   1972 35684    8   103   44   8%      1   95    9    1  804%
c i   35.0   87264   504661      8019    5520   1973 35688    8   103   44   8%      1   95    9    1  811%
c i   35.0   87258   504661      8037    5527   1978 35693    8   103   44   8%      1   95    8    1  780%
c i   35.0   87180   504661      8038    5527   1978 35693    8   103   44   8%      1   95    8    1  777%
c i   35.0   87103   504661      8047    5535   1978 35693    8   103   44   8%      1   95    8    1  766%
c i   35.1   87095   504661      8106    5571   1983 35708    8   103   44   8%      1   95    7    1  670%
c i   35.1   87091   504661      8133    5593   1984 35711    8   103   44   8%      1   95    7    1  678%
c i   35.2   87090   504661      8169    5620   1987 35714    8   104   44   7%      1   96    7    1  646%
c i   35.2   87000   504661      8188    5634   1988 35717    8   104   44   7%      1   96    7    1  639%
c i   35.3   86995   504661      8289    5710   1999 35728    8   104   44   7%      1   95    6    1  580%
c i   35.3   86984   504661      8330    5744   2001 35732    8   104   44   7%      1   96    7    1  594%
c i   35.4   86977   504661      8371    5769   2008 35739    8   104   44   7%      1   96    6    1  577%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   35.5   86971   504661      8485    5869   2014 35746    8   105   44   7%      1   96    7    1  653%
c i   35.6   86970   504661      8525    5902   2017 35749    8   105   44   7%      1   97    7    1  636%
c i   35.8   86969   504661      8661    6012   2026 35765    8   105   44   7%      1   97    7    1  627%
c i   35.8   86964   504661      8727    6059   2033 35774    8   105   44   7%      1   97    6    1  568%
c i   35.9   86926   504661      8773    6093   2035 35782    8   105   44   7%      1   97    7    1  574%
c i   35.9   86922   504661      8791    6107   2037 35783    8   106   44   7%      1   97    7    1  577%
c i   35.9   86914   504661      8793    6108   2037 35783    8   106   44   7%      1   97    7    1  577%
c i   36.0   86907   504661      8819    6124   2041 35788    8   106   44   7%      1   97    6    1  562%
c i   36.0   86899   504661      8857    6149   2044 35796    8   106   44   7%      1   97    6    1  547%
c i   36.1   86895   504661      8958    6225   2052 35811    8   106   44   7%      1   97    7    1  612%
c i   36.1   86878   504661      8965    6228   2054 35811    8   106   44   7%      1   97    7    1  606%
c i   36.2   86874   504661      9015    6270   2057 35815    8   107   44   7%      1   98    7    1  596%
c i   36.2   86849   504661      9016    6270   2057 35815    8   107   44   7%      1   98    7    1  594%
c i   36.2   86848   504661      9018    6270   2057 35816    8   107   44   7%      1   97    7    1  590%
c i   36.2   86847   504661      9019    6270   2057 35816    8   107   44   7%      1   97    7    1  587%
c i   36.3   86846   504661      9074    6305   2061 35828    8   107   44   7%      1   98    6    1  553%
c i   36.5   86840   504661      9195    6395   2075 35843    7   108   45   7%      1   99    6    1  529%
c 
c [simplification-7] limit 9212 conflicts (hard 19093) hit after 9212 conflicts
c [quatres-3] found 39108 quaternary clauses 52% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 9 single-self-subsuming ternary resolvents
c [quatres-3-2] added 45 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 38699 schedulable variables 43%
c [ternres-3] 2220 ternary resolvents (5 bin, 2215 trn)
c [ternres-3] 4 variables remain 0% (86831 retained 100%)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 933 xors of average arity 2.1
c [gauss-3] connected 1984 occurrences of 921 variables (average 2.2)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [decomp-17] removed 459 variables
c [gauss-3] exported 1 unary, 24 binary and 0 ternary equations
c [basicprobe-3] limit 11837503 penalty 0 = 0 + 0
c [basicprobe-3-0] 23532 probes remain 28% after last round
c [basicprobe-3-0] 96 units = 96 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1845 variables, found 21285 hbrs
c [bate-1] eliminated 32 asymmetric tautologies during probing
c [unhide-7] limit 473500 with penalty 0 = 0 + 0
c [unhide-7-7] 57 units, 133 failed, 7851 tauts, 0 hbrs, 6614 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 185 transitive binary clauses
c [transred-3] found 8 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 4 clauses out of 663 (1%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 4 large clauses in 15000004 steps
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 340265 clauses = 236418 binary + 103847 ternary
c [cce-2-1] tried to eliminate 249 small clauses 0%
c [cce-2-1] eliminated 34 binary clauses 0%
c [cce-2-1] eliminated 31 ternary clauses 0%
c [cce-2-1] eliminated 65 small clauses 0%
c [cce-2-1] eliminated 4637 small clauses in 15000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 4641 covered clauses in round 1
c [cce-2] eliminated 4641 covered clauses in TOTAL during 1 rounds
c [cce-2] 4641 < 1/100 * 467811 = 4678 considered unsuccessful
c [elim-7] 7762 variables 9% will be scheduled this time
c [elim-7] scheduled 7762 variables 9%
c [elim-7] limit of 47350014 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 11 variables 0% in round 1 in 14300680 steps
c [elim-7-1] backward subsumption/strengthening limit 14300600
c [elim-7-1-1] backward checking 906 touched variables 1%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 13 and strengthened 0 clauses in 290012 steps
c [elim-7-1] rescheduled 35 variables 0% by backward subsumption
c [elim-7-2] eliminated 4 variables 0% in round 2 in 22175 steps
c [elim-7-2] backward subsumption/strengthening limit 22100
c [elim-7-2-1] backward checking 23 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 3 and strengthened 0 clauses in 22101 steps
c [elim-7-2] rescheduled 8 variables 0% by backward subsumption
c [elim-7-3] eliminated 4 variables 0% in round 3 in 1832 steps
c [elim-7-3] backward subsumption/strengthening limit 1800
c [elim-7-3-1] backward checking 21 touched variables 0%
c [elim-7-3-1] incomplete backward checking 15 remain 71%
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 1807 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 19 = 0% variables out of 7762 scheduled
c [elim-7] 19 < 1/100 * 7762 = 77 considered unsuccessful
c [bca-3] limit of 10000000 steps and 922914 added (scaled 2)
c [bca-3] 147210 out of 167752 literals actually usable 88%
c [bca-3] added 39 blocked clauses in 386539 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 5428 pos 6.5% + 78403 neg 93.5% = 83831 sched 99.9% ret 44
c [sweep-3-1] 1113105 steps 12 queries 18385.75 avg class size
c [sweep-3-1] 158 decisions 9 SAT calls 102.67 avg env size
c [sweep-3-1] 83817 variables remain 100% (58 retained 0%)
c [decomp-19] removed 525 variables
c [sweep-3-1] removed 525 vars (0 failed, 2 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 525 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-7] 457802 negative 99.5% of 460081 except 2279 0.5%
c [phase-count-7] 374174 positive 81.3% of 460081 except 85907 18.7%
c [phase-count-7] less non-negative clauses 2279 than limit 46000 (10.0%)
c [phase-count-7] non-pos/non-neg = 85907/2279 = 37.70 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 1150 negative 100%
c [sort-queue-7] sorted 83350 enqueued variables after 9212 conflicts
c [score-dist-7] active 0 (0%), one 34790 (42%), zero 48560 (58%)
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 3485 variables 4.0% (83350 remain 26%)
c [simplification-7] removed 44580 irredundant clauses 8.8% (460081 remain 33%)
c [simplification-7] maximum reduction of 9% = max (4%, 9%)
c [simplification-7] large reduction 9% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 21212 (soft 11212 + delta 10000)
c [simplification-7] new conflict limit 11212 (hard 21212)
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   39.9   83349   460081      9224    6354   3260 48371    7   108   43   7%      1   99    6    1  529%
c i   40.3   83261   460081      9479    6556   3281 48396    8   111   44   7%      1  101    9    1  759%
c i   40.3   83235   460081      9498    6571   3281 48399    8   111   44   7%      1  101   10    1  796%
c i   40.3   83225   460081      9519    6586   3283 48402    8   111   44   7%      1  101   10    1  794%
c i   40.3   83213   460081      9551    6605   3290 48407    8   111   44   7%      1  101    9    1  761%
c i   40.4   83197   460081      9582    6625   3294 48413    8   112   44   7%      1  102    9    1  717%
c i   40.4   83189   460081      9583    6625   3294 48413    8   111   44   7%      1  101    9    1  714%
c i   40.4   83185   460081      9607    6644   3298 48413    8   112   44   7%      1  102   10    1  848%
c i   40.5   83019   460081      9638    6664   3303 48418    8   112   44   7%      1  102   10    1  806%
c i   40.5   83007   460081      9659    6677   3305 48423    8   112   44   7%      1  102    9    1  760%
c i   40.5   82835   460081      9661    6678   3305 48423    8   112   44   7%      1  102    9    1  772%
c i   40.6   82832   460081      9739    6740   3306 48436    8   112   44   7%      1  101    8    1  689%
c i   40.6   82822   460081      9762    6755   3307 48438    8   112   44   7%      1  101    9    1  729%
c i   40.7   82695   460081      9822    6800   3314 48444    8   111   44   7%      1  101    9    1  691%
c i   40.8   82692   460081      9928    6882   3323 48450    8   110   44   7%      1  100    8    1  655%
c i   40.9   82690   460081     10158    7098   3332 48453    8   109   44   8%      1   98   15    1 1142%
c i   40.9   82679   460081     10168    7105   3333 48453    8   109   44   8%      1   98   15    1 1124%
c i   41.0   82675   460081     10406    7314   3340 48462    9   107   44   8%      1   96   15    1 1082%
c i   41.0   82674   460081     10438    7341   3341 48463    9   108   44   8%      1   97   14    1 1054%
c i   41.1   82669   460081     10499    7395   3343 48465    9   108   44   8%      1   97   15    1 1062%
c i   41.1   82666   460081     10507    7401   3344 48465    9   108   44   8%      1   97   15    1 1069%
c i   41.1   82660   460081     10540    7427   3345 48467    9   108   44   8%      1   97   18    1 1301%
c i   41.2   82658   460081     10652    7522   3354 48473    9   109   44   9%      1   97   18    1 1294%
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   41.3   82657   460081     10693    7554   3360 48473    9   109   44   9%      1   97   18    1 1246%
c i   41.3   82644   460081     10760    7612   3364 48477    9   110   44   9%      1   98   17    1 1191%
c i   41.3   82641   460081     10761    7612   3364 48477    9   110   44   9%      1   98   17    1 1187%
c i   41.4   82640   460081     10782    7630   3365 48478    9   111   44   8%      1  100   16    1 1129%
c i   41.4   82624   460081     10784    7631   3364 48479    9   111   44   8%      1  100   16    1 1121%
c i   41.4   82621   460081     10785    7631   3364 48479    9   111   44   8%      1  100   16    1 1116%
c i   41.4   82619   460081     10814    7655   3365 48481    9   113   44   8%      1  101   16    1 1098%
c i   41.5   82608   460081     10831    7667   3367 48482   10   114   44   8%      1  102   17    1 1138%
c 
c [simplification-8] limit 11254 conflicts (hard 21212) hit after 11254 conflicts
c [quatres-4] found 37723 quaternary clauses 54% in total
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [quatres-4-2] added 2 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 2 schedulable variables 0%
c [ternres-4] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 285 xors of average arity 2.5
c [gauss-4] connected 707 occurrences of 511 variables (average 1.4)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [decomp-20] removed 92 variables
c [gauss-4] exported 2 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 49185 schedulable variables 60%
c [simpleprobe-4] limit 11587573 penalty 0 = 0 + 0
c [decomp-22] removed 2143 variables
c [simpleprobe-4] 19925 variables remain 25% (60443 retained 75%)
c [simpleprobe-4] removed 2143 variables, found 34441 hbrs, 298 units
c [unhide-8] limit 579378 with penalty 0 = 0 + 0
c [unhide-8-8] 19 units, 301 failed, 8049 tauts, 0 hbrs, 6783 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 229 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 79223 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 381 blocked clauses
c [block-3] 381 < 1/100 * 441476 = 4414 considered unsuccessful
c [bca-4] limit of 10000000 steps and 867885 added (scaled 2)
c [bca-4] 136665 out of 158364 literals actually usable 86%
c [bca-4] added 78 blocked clauses in 357157 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 4654 pos 5.9% + 74478 neg 94.1% = 79132 sched 99.9% ret 49
c [sweep-4-1] 1057486 steps 13 queries 17438.23 avg class size
c [sweep-4-1] 76 decisions 11 SAT calls 45.55 avg env size
c [sweep-4-1] 78897 variables remain 100% (66 retained 0%)
c [decomp-23] removed 870 variables
c [sweep-4-1] removed 870 vars (0 failed, 2 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 870 vars in TOTAL (1 rounds, 12 queries)
c [phase-count-8] 427805 negative 99.5% of 430079 except 2274 0.5%
c [phase-count-8] 347556 positive 80.8% of 430079 except 82523 19.2%
c [phase-count-8] less non-negative clauses 2274 than limit 43000 (10.0%)
c [phase-count-8] non-pos/non-neg = 82523/2274 = 36.29 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 951 negative 100%
c [sort-queue-8] sorted 78311 enqueued variables after 11254 conflicts
c [score-dist-8] active 0 (0%), one 34928 (45%), zero 43383 (55%)
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 4292 variables 5.2% (78311 remain 24%)
c [simplification-8] removed 30002 irredundant clauses 6.5% (430079 remain 31%)
c [simplification-8] maximum reduction of 7% = max (5%, 7%)
c [simplification-8] large reduction 7% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 23254 (soft 13254 + delta 10000)
c [simplification-8] new conflict limit 13254 (hard 23254)
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   44.8   78310   430079     11280    7887   2440 71087   11   117   42  10%      2  104   33    2 2002%
c i   44.9   78306   430079     11316    7913   2444 71091   11   118   43  10%      2  105   30    2 1801%
c i   45.1   78305   430079     11464    8036   2451 71105   12   122   43   9%      2  109   23    2 1368%
c i   45.2   78283   430079     11544    8098   2454 71117   11   122   43   9%      2  109   19    2 1132%
c i   45.2   77973   430079     11611    8139   2464 71132   11   122   43   9%      1  109   16    2  929%
c i   45.3   77956   430079     11642    8164   2465 71136   11   123   43   9%      1  109   16    2  959%
c i   45.3   77951   430079     11709    8219   2469 71143   11   122   43   9%      1  109   14    2  825%
c i   45.3   77946   430079     11751    8252   2474 71145   11   122   43   9%      1  108   13    2  772%
c i   45.5   77941   430079     11882    8351   2492 71154   11   123   43   9%      1  109   10    2  590%
c i   45.5   77929   430079     11950    8401   2496 71163   11   122   43   9%      1  109   12    2  679%
c i   45.6   77925   430079     11990    8434   2498 71166   11   122   43   9%      1  108   11    2  633%
c i   45.6   77916   430079     12048    8483   2501 71171   11   122   43   9%      1  108   10    2  592%
c i   45.7   77874   430079     12091    8514   2505 71177   11   121   43   9%      1  108   11    2  643%
c i   45.8   77866   430079     12203    8604   2517 71184   11   122   43   9%      1  108   10    2  563%
c i   45.8   77863   430079     12229    8621   2520 71188   11   122   43   9%      1  108    9    2  538%
c i   45.9   77809   430079     12272    8652   2526 71193   11   122   43   9%      1  108   11    2  608%
c i   45.9   77781   430079     12298    8666   2531 71199   11   122   43   9%      1  107   10    2  562%
c i   46.0   77752   430079     12378    8733   2536 71206   11   122   43   9%      1  108    9    2  504%
c i   46.0   77744   430079     12389    8743   2536 71206   11   122   43   9%      1  108    9    2  503%
c i   46.0   77743   430079     12404    8753   2536 71210   11   122   43   9%      1  108    9    2  497%
c i   46.0   77732   430079     12407    8753   2536 71212   11   122   43   9%      1  108    9    2  492%
c i   46.0   77728   430079     12408    8753   2536 71212   11   122   43   9%      1  108    9    2  490%
c i   46.1   77687   430079     12515    8833   2544 71228   11   122   43   9%      1  107    8    2  439%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   46.3   77686   430079     12677    8961   2558 71244   11   124   43   9%      1  109    7    2  374%
c i   46.3   77655   430079     12691    8972   2560 71244   11   124   43   9%      1  109    6    2  360%
c i   46.6   77641   430079     12945    9176   2581 71265   11   125   43   9%      1  110   12    2  646%
c i   46.8   77628   430079     13050    9259   2592 71274   11   125   43   9%      1  110   11    2  589%
c i   46.9   77603   430079     13162    9338   2608 71285   11   126   43   9%      1  111   10    2  526%
c 
c [simplification-9] limit 13267 conflicts (hard 23254) hit after 13267 conflicts
c [quatres-5] found 34326 quaternary clauses 52% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] extracted 790 xors of average arity 2.3
c [gauss-5] connected 1806 occurrences of 893 variables (average 2.0)
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [decomp-24] removed 179 variables
c [gauss-5] exported 1 unary, 0 binary and 0 ternary equations
c [unhide-9] limit 698050 with penalty 0 = 0 + 0
c [unhide-9-9] 14 units, 63 failed, 5815 tauts, 0 hbrs, 8417 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 196 transitive binary clauses
c [transred-5] found 2 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 77237 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 698050240 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3547 variables 5% in round 1 in 34433436 steps
c [elim-8-1] backward subsumption/strengthening limit 34433400
c [elim-8-1-1] backward checking 12987 touched variables 17%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 66 and strengthened 151 clauses in 3122932 steps
c [elim-8-1] rescheduled 545 variables 1% by backward subsumption
c [elim-8-2] eliminated 68 variables 0% in round 2 in 441318 steps
c [elim-8-2] backward subsumption/strengthening limit 441300
c [elim-8-2-1] backward checking 449 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 32 and strengthened 22 clauses in 262756 steps
c [elim-8-2] rescheduled 108 variables 0% by backward subsumption
c [elim-8-3] eliminated 11 variables 0% in round 3 in 124989 steps
c [elim-8-3] backward subsumption/strengthening limit 124900
c [elim-8-3-1] backward checking 57 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 16 and strengthened 7 clauses in 124901 steps
c [elim-8] incomplete 32 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 3660 = 5% variables out of 77237 scheduled
c [bca-5] limit of 10000000 steps and 823146 added (scaled 2)
c [bca-5] 126550 out of 147156 literals actually usable 86%
c [bca-5] added 75 blocked clauses in 329913 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10470750 penalty 0 = 0 + 0
c [sweep-5-1] 5037 pos 6.9% + 68479 neg 93.1% = 73516 sched 99.9% ret 61
c [sweep-5-1] 10512120 steps 116 queries 4272.53 avg class size
c [sweep-5-1] 680 decisions 90 SAT calls 50.63 avg env size
c [sweep-5-1] 71566 variables remain 97% (1955 retained 3%)
c [decomp-26] removed 243 variables
c [sweep-5-1] removed 243 vars (0 failed, 30 eqs, 45 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 243 vars in TOTAL (1 rounds, 115 queries)
c [phase-count-9] 408535 negative 99.5% of 410480 except 1945 0.5%
c [phase-count-9] 331158 positive 80.7% of 410480 except 79322 19.3%
c [phase-count-9] less non-negative clauses 1945 than limit 41000 (10.0%)
c [phase-count-9] non-pos/non-neg = 79322/1945 = 40.78 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 291 negative 100%
c [sort-queue-9] sorted 73334 enqueued variables after 13267 conflicts
c [score-dist-9] active 0 (0%), one 36442 (50%), zero 36892 (50%)
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 4262 variables 5.5% (73334 remain 23%)
c [simplification-9] removed 19599 irredundant clauses 4.6% (410480 remain 29%)
c [simplification-9] maximum reduction of 5% = max (5%, 5%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 25267 (soft 15267 + delta 10000)
c [simplification-9] new conflict limit 15267 (hard 25267)
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   51.4   73333   410480     13323    7308   2151 70465   11   126   41   8%      1  110    9    2  479%
c i   51.6   73322   410480     13457    7415   2158 70482   11   126   41   8%      1  110    9    2  480%
c i   51.8   73321   410480     13761    7657   2185 70506   11   125   41   9%      1  109   11    2  561%
c i   51.9   73314   410480     13881    7758   2190 70510   11   124   41   9%      1  107   14    2  724%
c i   51.9   73313   410480     13951    7814   2200 70513   11   124   41   9%      1  107   13    2  671%
c i   52.0   73271   410480     13955    7817   2200 70513   11   124   41   9%      1  107   13    2  664%
c i   52.0   73262   410480     13959    7820   2200 70513   11   124   41   9%      1  107   13    2  655%
c i   52.1   73258   410480     14164    7991   2214 70527   11   126   41   9%      1  108   15    2  751%
c i   52.1   73252   410480     14202    8020   2218 70530   11   125   41   9%      1  108   15    2  713%
c i   52.3   73231   410480     14297    8094   2231 70537   11   128   41   9%      1  111   12    2  610%
c i   52.9   73228   410480     14928    8642   2260 70577   11   132   41   9%      3  113   12    2  548%
c i   52.9   73224   410480     14933    8643   2261 70579   11   132   41   9%      3  113   12    2  539%
c i   52.9   73213   410480     14945    8652   2261 70581   11   132   41   9%      3  113   11    2  527%
c i   52.9   73212   410480     14948    8654   2261 70581   11   132   41   9%      3  113   11    2  522%
c i   53.0   73204   410480     14993    8694   2261 70585   11   134   41   9%      3  115   11    2  509%
c i   53.3   73131   410480     15236    8907   2274 70597   12   140   41   8%      3  120   12    2  541%
c 
c [simplification-10] limit 15276 conflicts (hard 25267) hit after 15276 conflicts
c [quatres-6] found 35992 quaternary clauses 54% in total
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 3 single-self-subsuming ternary resolvents
c [quatres-6-2] added 10 quaternary resolvents
c [ternres-5] limit 2019907 with penalty 1 = 1 + 0
c [ternres-5] all 73128 free variables schedulable
c [ternres-5] 258 ternary resolvents (1 bin, 257 trn)
c [ternres-5] 48712 variables remain 67% (24416 retained 33%)
c [card-4] limit 252488 penalty 3 = 3 + 0
c [card-4] found 1391 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 252488 for elimination
c [card-4] 1391 out of 1391 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-6] limit 2000000 penalty 0 = 0 + 0
c [gauss-6] extracted 104 xors of average arity 2.7
c [gauss-6] connected 284 occurrences of 207 variables (average 1.4)
c [gauss-6] limit 2000000 penalty 0 = 0 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-27] removed 22 variables
c [treelook-4] limit 201990 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 38111 literals 26%
c [treelook-4] scheduling used 219007 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 201990 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 261111 steps
c [treelook-4] 38105 literals remain 26%
c [treelook-4] 16316 variables remain to probed next time 22%
c [treelook-4] removed 0 variables, found 1908 hbrs
c [unhide-10] limit 807962 with penalty 0 = 0 + 0
c [unhide-10-10] 23 units, 211 failed, 3881 tauts, 0 hbrs, 7123 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 158 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 40
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 38
c [cce-3-1] eliminated 4 clauses out of 5 (80%) of length 37
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 36
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 35
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 34
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 33
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 32
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 31
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 30
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 29
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 28
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 27
c [cce-3-1] eliminated 2 clauses out of 5 (40%) of length 26
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 25
c [cce-3-1] eliminated 3 clauses out of 8 (38%) of length 24
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 23
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 22
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 21
c [cce-3-1] eliminated 4 clauses out of 9 (44%) of length 20
c [cce-3-1] eliminated 10 clauses out of 10 (100%) of length 19
c [cce-3-1] eliminated 6 clauses out of 11 (55%) of length 18
c [cce-3-1] eliminated 9 clauses out of 10 (90%) of length 17
c [cce-3-1] eliminated 6 clauses out of 9 (67%) of length 16
c [cce-3-1] eliminated 8 clauses out of 10 (80%) of length 15
c [cce-3-1] eliminated 6 clauses out of 10 (60%) of length 14
c [cce-3-1] eliminated 10 clauses out of 11 (91%) of length 13
c [cce-3-1] eliminated 8 clauses out of 11 (73%) of length 12
c [cce-3-1] eliminated 10 clauses out of 13 (77%) of length 11
c [cce-3-1] eliminated 8 clauses out of 99 (8%) of length 10
c [cce-3-1] eliminated 12 clauses out of 268 (4%) of length 9
c [cce-3-1] eliminated 10 clauses out of 360 (3%) of length 8
c [cce-3-1] eliminated 2 clauses out of 557 (0%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 181 large clauses in 7500001 steps
c [cce-3-1] allowing another 3750000 steps for small clauses
c [cce-3-1] scheduling 297114 clauses = 207391 binary + 89723 ternary
c [cce-3-1] tried to eliminate 142 small clauses 0%
c [cce-3-1] eliminated 32 binary clauses 0%
c [cce-3-1] eliminated 23 ternary clauses 0%
c [cce-3-1] eliminated 55 small clauses 0%
c [cce-3-1] eliminated 3764 small clauses in 7500006 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3945 covered clauses in round 1
c [cce-3] eliminated 3945 covered clauses in TOTAL during 1 rounds
c [cce-3] 3945 < 1/100 * 408140 = 4081 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 72639 variables 100%
c [elim-9] limit of 80796293 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1007 variables 1% in round 1 in 34612318 steps
c [elim-9-1] backward subsumption/strengthening limit 34612300
c [elim-9-1-1] backward checking 4486 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 34 and strengthened 18 clauses in 1232961 steps
c [elim-9-1] rescheduled 143 variables 0% by backward subsumption
c [elim-9-2] eliminated 11 variables 0% in round 2 in 78242 steps
c [elim-9-2] backward subsumption/strengthening limit 78200
c [elim-9-2-1] backward checking 93 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 9 and strengthened 4 clauses in 78201 steps
c [elim-9-2] rescheduled 30 variables 0% by backward subsumption
c [elim-9-3] eliminated 2 variables 0% in round 3 in 26146 steps
c [elim-9-3] backward subsumption/strengthening limit 26100
c [elim-9-3-1] backward checking 9 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 1 and strengthened 0 clauses in 26101 steps
c [elim-9] incomplete 3 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1026 = 1% variables out of 72639 scheduled
c [bca-6] limit of 10000000 steps and 803522 added (scaled 2)
c [bca-6] 120655 out of 143228 literals actually usable 84%
c [bca-6] added 53 blocked clauses in 310642 steps
c [sweep-6] limit 1211944 penalty 0 = 0 + 0
c [sweep-6-1] 4228 pos 6.1% + 65643 neg 93.9% = 69871 sched 97.6% ret 1742
c [sweep-6-1] 1927518 steps 15 queries 17030.80 avg class size
c [sweep-6-1] 163 decisions 12 SAT calls 51.33 avg env size
c [sweep-6-1] 69834 variables remain 98% (1769 retained 2%)
c [decomp-29] removed 56 variables
c [sweep-6-1] removed 56 vars (0 failed, 3 eqs, 3 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 56 vars in TOTAL (1 rounds, 14 queries)
c [phase-count-10] 399275 negative 99.5% of 401220 except 1945 0.5%
c [phase-count-10] 322544 positive 80.4% of 401220 except 78676 19.6%
c [phase-count-10] less non-negative clauses 1945 than limit 40100 (10.0%)
c [phase-count-10] non-pos/non-neg = 78676/1945 = 40.45 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 204 negative 100%
c [sort-queue-10] sorted 71557 enqueued variables after 15276 conflicts
c [score-dist-10] active 0 (0%), one 37406 (52%), zero 34151 (48%)
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 1571 variables 2.1% (71557 remain 22%)
c [simplification-10] removed 9260 irredundant clauses 2.3% (401220 remain 29%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 10666
c [simplification-10] penalized conflict interval 10666 = 1 * 10666
c [simplification-10] hard conflict limit 35942 (soft 25942 + delta 10000)
c [simplification-10] new conflict limit 25942 (hard 35942)
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   57.6   71556   401220     15339    8291   2278 67480   11   140   41   8%      2  120   11    2  476%
c i   57.6   71552   401220     15382    8327   2283 67481   11   140   41   8%      2  120   10    2  442%
c i   57.6   71547   401220     15417    8350   2288 67485   11   139   41   8%      2  120    9    2  427%
c i   57.8   71543   401220     15567    8484   2293 67495   11   140   41   8%      2  120   10    2  440%
c i   58.1   71540   401220     15866    8754   2305 67502   12   138   41   9%      2  117   18    2  786%
c i   58.2   71534   401220     15977    8855   2309 67507   12   139   41   9%      2  118   15    2  637%
c i   58.2   71529   401220     16021    8884   2316 67512   12   140   41   9%      2  119   16    2  662%
c i   58.4   71524   401220     16142    8987   2320 67521   12   139   41   9%      2  119   14    2  573%
c i   58.5   71523   401220     16249    9081   2324 67526   12   139   41   9%      2  118   14    2  578%
c i   58.6   71518   401220     16369    9185   2329 67532   12   139   41   9%      1  118   13    2  543%
c i   58.7   71496   401220     16567    9352   2338 67549   12   139   41   9%      1  117   11    2  464%
c i   58.8   71495   401220     16648    9418   2341 67555   12   139   41   9%      1  118   17    2  676%
c i   58.8   71494   401220     16688    9454   2342 67555   13   139   41   9%      1  117   17    2  687%
c i   58.8   71479   401220     16690    9455   2342 67555   13   139   41   9%      1  117   17    2  682%
c i   58.9   71473   401220     16759    9516   2343 67558   13   139   41   9%      1  117   19    2  747%
c i   58.9   71469   401220     16798    9552   2345 67558   13   139   41   9%      1  117   18    3  721%
c i   58.9   71461   401220     16854    9600   2348 67561   13   138   41   9%      1  116   17    3  672%
c i   59.1   71447   401220     16973    9696   2361 67566   13   141   41   9%      1  118   15    3  607%
c i   59.2   71441   401220     17072    9781   2364 67575   13   140   41   9%      1  117   14    3  551%
c i   59.2   71438   401220     17092    9795   2365 67579   13   139   41   9%      1  117   13    3  527%
c i   59.3   71434   401220     17156    9852   2368 67582   13   141   41   9%      1  118   13    3  491%
c i   59.5   71431   401220     17307    9977   2380 67595   13   144   41   9%      1  121   13    3  509%
c i   59.5   71430   401220     17321    9990   2380 67595   13   143   41   9%      1  120   13    3  501%
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.5   71429   401220     17431   10084   2384 67599   13   144   41   9%      1  121   18    3  689%
c i   59.7   71412   401220     17643   10273   2387 67600   14   143   42  10%      1  119   33    3 1195%
c i   59.8   71391   401220     17768   10391   2389 67603   15   143   42  10%      1  119   30    3 1066%
c i   60.0   71376   401220     18108   10683   2410 67617   15   142   42  10%      1  117   19    3  663%
c i   60.1   71369   401220     18202   10766   2413 67623   15   142   42  10%      1  117   16    3  576%
c i   60.2   71366   401220     18367   10899   2422 67640   15   141   42  11%      1  116   17    3  594%
c i   60.3   71365   401220     18459   10980   2425 67644   15   143   42  11%      1  118   19    3  656%
c i   60.3   71349   401220     18502   11019   2426 67646   15   143   42  11%      1  118   18    3  623%
c i   60.3   71344   401220     18506   11022   2426 67646   15   143   42  11%      1  118   18    3  616%
c i   60.3   71339   401220     18512   11025   2428 67646   15   143   42  11%      1  118   18    3  604%
c i   60.4   71224   401220     18576   11079   2431 67652   15   143   42  11%      1  118   18    3  602%
c i   60.4   71220   401220     18577   11079   2431 67652   15   143   42  11%      1  118   18    3  600%
c i   60.4   71219   401220     18607   11102   2433 67656   15   142   42  11%      1  117   16    3  555%
c i   60.5   71211   401220     18713   11198   2435 67658   15   143   42  11%      1  118   22    3  741%
c i   60.6   71207   401220     18937   11398   2445 67666   16   141   42  11%      1  115   23    3  739%
c i   61.3   71206   401220     19507   11908   2458 67698   16   148   42  11%      3  121   15    3  486%
c i   61.4   71195   401220     19564   11957   2462 67700   16   149   42  11%      2  122   16    3  499%
c i   61.4   71190   401220     19565   11957   2462 67700   16   149   42  11%      2  122   16    3  497%
c i   61.6   71186   401220     19772   12137   2473 67713   16   154   43  10%      2  126   15    3  460%
c i   61.6   71138   401220     19776   12138   2474 67714   16   154   43  10%      2  126   15    3  453%
c i   61.7   71111   401220     19787   12147   2474 67715   16   153   43  10%      2  126   14    3  440%
c i   61.8   71107   401220     19849   12195   2482 67718   16   154   43  10%      2  127   14    3  419%
c i   61.8   71098   401220     19871   12213   2483 67720   16   155   43  10%      2  128   15    3  473%
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   62.0   71095   401220     20036   12331   2508 67736   15   153   43  10%      2  125   11    3  348%
c i   62.4   71094   401220     20439   12662   2541 67766   15   153   43  10%      2  124   17    3  504%
c i   62.4   71090   401220     20440   12662   2541 67766   15   153   43  10%      2  124   17    3  502%
c i   62.5   71089   401220     20514   12732   2542 67767   15   152   43  10%      2  123   17    3  498%
c i   62.5   71073   401220     20540   12755   2543 67767   16   151   43  10%      2  123   19    3  577%
c i   62.5   71072   401220     20588   12795   2545 67769   16   151   43  10%      2  122   20    3  598%
c i   62.9   71059   401220     21102   13258   2565 67792   16   152   43  11%      3  122   19    3  557%
c i   63.0   71058   401220     21166   13314   2571 67793   16   153   43  11%      3  123   19    4  554%
c i   63.0   71057   401220     21167   13314   2571 67793   16   153   43  11%      3  123   19    4  552%
c i   63.3   71055   401220     21559   13663   2584 67806   18   152   43  12%      3  122   28    4  747%
c i   63.7   71013   401220     21974   14001   2614 67835   18   156   43  12%      3  125   24    4  621%
c i   63.8   71008   401220     21996   14018   2617 67836   18   156   43  12%      3  125   23    4  612%
c i   63.9   70981   401220     22108   14114   2623 67839   18   157   43  12%      2  125   20    4  517%
c i   63.9   70877   401220     22165   14166   2625 67840   18   157   43  12%      2  125   22    4  561%
c i   64.0   70876   401220     22174   14170   2625 67844   18   157   43  12%      2  125   21    4  545%
c i   64.0   70871   401220     22274   14262   2628 67847   18   156   43  12%      2  124   20    4  515%
c i   64.4   70867   401220     22649   14587   2642 67873   18   157   43  12%      2  125   19    4  472%
c i   64.5   70866   401220     22820   14739   2649 67881   18   157   44  12%      2  124   19    4  480%
c i   64.7   70767   401220     22954   14853   2656 67889   18   155   44  12%      2  122   16    4  400%
c i   64.7   70760   401220     22979   14876   2656 67890   18   156   44  12%      2  122   16    4  389%
c i   64.8   70757   401220     23032   14922   2658 67892   18   158   44  11%      2  124   15    4  380%
c i   64.8   70747   401220     23033   14922   2658 67892   18   157   44  11%      2  124   15    4  378%
c i   65.0   70746   401220     23241   15097   2672 67903   18   158   44  11%      2  124   15    4  372%
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   65.3   70742   401220     23416   15249   2681 67914   18   160   44  11%      2  126   16    4  380%
c i   65.3   70741   401220     23419   15251   2681 67914   18   160   44  11%      1  126   15    4  376%
c i   65.3   70726   401220     23436   15265   2681 67915   18   159   44  11%      1  125   16    4  388%
c i   65.3   70722   401220     23503   15319   2683 67918   18   160   44  12%      1  125   25    4  611%
c i   65.3   70719   401220     23504   15319   2683 67918   18   159   44  12%      1  125   25    4  609%
c i   65.4   70716   401220     23575   15381   2685 67921   19   159   44  12%      1  124   30    4  719%
c i   65.5   70715   401220     23660   15456   2693 67922   19   160   44  12%      1  126   27    4  644%
c i   65.5   70712   401220     23661   15456   2693 67922   19   160   44  12%      1  125   27    4  641%
c i   65.7   70711   401220     23855   15613   2703 67937   20   161   44  12%      1  126   32    4  746%
c i   65.8   70709   401220     23926   15673   2706 67942   20   162   44  12%      1  127   28    4  650%
c i   66.5   70704   401220     24560   16207   2747 67987   21   166   44  12%      3  129   27    5  600%
c i   66.6   70700   401220     24680   16316   2749 67990   21   167   44  12%      3  131   27    5  587%
c i   66.9   70687   401220     24918   16502   2769 68018   20   166   45  12%      2  129   19    5  412%
c i   67.0   70686   401220     25019   16591   2773 68022   21   167   45  12%      2  130   25    5  531%
c i   67.2   70683   401220     25168   16717   2786 68030   20   167   45  12%      2  130   19    5  415%
c i   67.2   70682   401220     25172   16719   2787 68030   20   167   45  12%      2  130   19    5  413%
c i   67.6   70681   401220     25435   16945   2799 68050   20   169   45  12%      2  131   17    5  364%
c i   67.7   70678   401220     25516   17016   2802 68056   20   170   45  12%      2  132   20    5  414%
c i   67.7   70669   401220     25558   17054   2802 68058   20   169   45  12%      2  131   19    5  408%
c i   67.7   70664   401220     25560   17054   2803 68058   20   169   45  12%      2  131   19    5  405%
c i   67.9   70663   401220     25700   17165   2815 68069   20   170   45  12%      1  132   18    5  372%
c i   68.1   70662   401220     25823   17272   2822 68076   20   173   46  12%      1  134   20    5  418%
c i   68.1   70656   401220     25841   17289   2822 68076   20   173   46  12%      1  134   20    5  405%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   68.2   70641   401220     25873   17312   2824 68081   20   173   46  12%      1  134   19    5  396%
c 
c [simplification-11] limit 26033 conflicts (hard 35942) hit after 26033 conflicts
c [quatres-7] found 33063 quaternary clauses 52% in total
c [quatres-7-2] added 6 single-self-subsuming ternary resolvents
c [quatres-7-2] added 58 quaternary resolvents
c [ternres-6] limit 6858995 with penalty 0 = 0 + 0
c [ternres-6] 47049 schedulable variables 66%
c [ternres-6] 1741 ternary resolvents (5 bin, 1736 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-30] removed 1127 variables
c [basicprobe-4] limit 34294975 penalty 0 = 0 + 0
c [basicprobe-4-0] 18302 probes remain 26% after last round
c [basicprobe-4-0] 397 units = 332 failed (84%) + 65 lifted (16%)
c [basicprobe-4-0] removed 1126 variables, found 43992 hbrs
c [bate-2] eliminated 114 asymmetric tautologies during probing
c [unhide-11] limit 1371799 with penalty 0 = 0 + 0
c [unhide-11-11] 21 units, 122 failed, 4764 tauts, 0 hbrs, 28561 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 121 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 69111 variables 100%
c [block-4] limit of 17147487 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 134 blocked clauses
c [block-4] 134 < 1/100 * 383688 = 3836 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 69106 variables 100%
c [elim-10] limit of 137179903 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1922 variables 3% in round 1 in 32358930 steps
c [elim-10-1] backward subsumption/strengthening limit 32358900
c [elim-10-1-1] backward checking 7346 touched variables 11%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 72 and strengthened 195 clauses in 1811109 steps
c [elim-10-1] rescheduled 645 variables 1% by backward subsumption
c [elim-10-2] eliminated 51 variables 0% in round 2 in 403676 steps
c [elim-10-2] backward subsumption/strengthening limit 403600
c [elim-10-2-1] backward checking 504 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 33 and strengthened 42 clauses in 236268 steps
c [elim-10-2] rescheduled 143 variables 0% by backward subsumption
c [elim-10-3] eliminated 18 variables 0% in round 3 in 95065 steps
c [elim-10-3] backward subsumption/strengthening limit 95000
c [elim-10-3-1] backward checking 111 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 4 and strengthened 13 clauses in 95001 steps
c [elim-10] incomplete 59 not tried 0% in round 3
c [gc-80] reconnected 106063 binary clauses (produced 0 empty 2 units)
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 2016 = 3% variables out of 69106 scheduled
c [bca-7] limit of 10000000 steps and 754074 added (scaled 2)
c [bca-7] 108760 out of 134182 literals actually usable 81%
c [bca-7] added 30 blocked clauses in 278254 steps
c [sweep-7] limit 2057698 penalty 0 = 0 + 0
c [sweep-7-1] 4172 pos 6.4% + 61286 neg 93.6% = 65458 sched 97.6% ret 1632
c [sweep-7-1] 2080688 steps 36 queries 7811.14 avg class size
c [sweep-7-1] 354 decisions 29 SAT calls 63.10 avg env size
c [sweep-7-1] 65241 variables remain 97% (1819 retained 3%)
c [decomp-31] removed 87 variables
c [sweep-7-1] removed 87 vars (0 failed, 6 eqs, 13 impls)
c [sweep-7] removed 87 vars in TOTAL (1 rounds, 35 queries)
c [phase-count-11] 374339 negative 99.5% of 376216 except 1877 0.5%
c [phase-count-11] 302667 positive 80.5% of 376216 except 73549 19.5%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 67003 enqueued variables after 26033 conflicts
c [score-dist-11] active 0 (0%), one 37067 (55%), zero 29936 (45%)
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 3633 variables 5.1% (67003 remain 21%)
c [simplification-11] removed 25004 irredundant clauses 6.2% (376216 remain 27%)
c [simplification-11] maximum reduction of 6% = max (5%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 38033 (soft 28033 + delta 10000)
c [simplification-11] new conflict limit 28033 (hard 38033)
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   73.3   67002   376216     26038   14202   3667 102144   20   172   42  12%      1  133   20    5  418%
c i   73.4   66995   376216     26128   14271   3675 102154   20   172   44  12%      1  133   18    5  375%
c i   73.5   66988   376216     26244   14369   3685 102159   20   172   44  12%      1  133   17    5  341%
c i   73.6   66975   376216     26293   14414   3686 102161   20   173   44  11%      1  133   16    5  324%
c i   73.7   66974   376216     26400   14505   3693 102165   20   172   45  12%      1  132   16    5  335%
c i   73.8   66973   376216     26519   14607   3696 102177   20   171   45  12%      1  131   18    5  370%
c i   73.8   66970   376216     26561   14643   3698 102178   20   172   45  12%      1  131   18    5  372%
c i   73.9   66969   376216     26595   14671   3698 102183   20   172   45  11%      1  132   18    5  353%
c i   74.0   66967   376216     26673   14743   3700 102186   20   173   45  11%      1  132   16    5  322%
c i   74.1   66964   376216     26738   14794   3704 102192   20   173   45  11%      1  132   16    5  321%
c i   74.1   66961   376216     26757   14809   3705 102193   19   173   45  11%      1  132   15    5  308%
c i   74.2   66956   376216     26777   14827   3705 102193   20   174   45  11%      1  133   17    5  335%
c i   74.3   66955   376216     26900   14936   3712 102198   20   174   45  11%      1  133   20    5  397%
c i   74.6   66550   376216     27141   15148   3724 102214   20   176   45  12%      1  135   27    5  533%
c i   74.9   66539   376216     27440   15404   3743 102234   20   174   45  11%      1  131   16    5  317%
c i   75.3   66538   376216     27736   15663   3763 102245   20   175   45  11%      1  133   20    5  391%
c i   75.3   66533   376216     27776   15696   3764 102248   20   175   45  11%      1  132   20    5  389%
c i   75.3   66532   376216     27786   15701   3766 102249   20   175   45  11%      1  132   20    5  379%
c 
c [simplification-12] limit 28034 conflicts (hard 38033) hit after 28034 conflicts
c [quatres-8] found 32214 quaternary clauses 53% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-2] added 2 single-self-subsuming ternary resolvents
c [quatres-8-2] added 17 quaternary resolvents
c [ternres-7] limit 7447635 with penalty 0 = 0 + 0
c [ternres-7] all 66521 free variables schedulable
c [ternres-7] 1216 ternary resolvents (0 bin, 1216 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-7] limit 1000000 penalty 1 = 1 + 0
c [gauss-7] extracted 73 xors of average arity 2.4
c [gauss-7] connected 175 occurrences of 128 variables (average 1.4)
c [gauss-7] limit 1000000 penalty 1 = 1 + 0
c [gauss-7] fully completed
c [decomp-32] removed 98 variables
c [gauss-7] exported 0 unary, 4 binary and 0 ternary equations
c [simpleprobe-5] 16336 schedulable variables 25%
c [simpleprobe-5] limit 29790540 penalty 0 = 0 + 0
c [decomp-34] removed 2052 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 2052 variables, found 27901 hbrs, 423 units
c [unhide-12] limit 1489527 with penalty 0 = 0 + 0
c [unhide-12-12] 14 units, 197 failed, 14910 tauts, 0 hbrs, 19951 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 185 transitive binary clauses
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 63795 variables 100%
c [elim-11] limit of 148952702 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1788 variables 3% in round 1 in 29119685 steps
c [elim-11-1] backward subsumption/strengthening limit 29119600
c [elim-11-1-1] backward checking 7383 touched variables 12%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 102 and strengthened 162 clauses in 1883200 steps
c [elim-11-1] rescheduled 602 variables 1% by backward subsumption
c [elim-11-2] eliminated 59 variables 0% in round 2 in 448290 steps
c [elim-11-2] backward subsumption/strengthening limit 448200
c [elim-11-2-1] backward checking 444 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 37 and strengthened 53 clauses in 183277 steps
c [elim-11-2] rescheduled 157 variables 0% by backward subsumption
c [elim-11-3] eliminated 10 variables 0% in round 3 in 106314 steps
c [elim-11-3] backward subsumption/strengthening limit 106300
c [elim-11-3-1] backward checking 90 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 4 and strengthened 5 clauses in 101444 steps
c [elim-11] incomplete 23 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 1870 = 3% variables out of 63795 scheduled
c [bca-8] limit of 10000000 steps and 698459 added (scaled 2)
c [bca-8] 98371 out of 123852 literals actually usable 79%
c [bca-8] added 52 blocked clauses in 250693 steps
c [sweep-8] limit 2234290 penalty 0 = 0 + 0
c [sweep-8-1] 3919 pos 6.5% + 56439 neg 93.5% = 60358 sched 97.5% ret 1567
c [sweep-8-1] 2247059 steps 39 queries 7460.00 avg class size
c [sweep-8-1] 537 decisions 27 SAT calls 122.81 avg env size
c [sweep-8-1] 60160 variables remain 97% (1762 retained 3%)
c [decomp-35] removed 87 variables
c [sweep-8-1] removed 87 vars (0 failed, 13 eqs, 15 impls)
c [sweep-8] removed 87 vars in TOTAL (1 rounds, 38 queries)
c [phase-count-12] 347086 negative 99.5% of 348690 except 1604 0.5%
c [phase-count-12] 278382 positive 79.8% of 348690 except 70308 20.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 61838 enqueued variables after 28034 conflicts
c [score-dist-12] active 0 (0%), one 35481 (57%), zero 26357 (43%)
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 4683 variables 7.0% (61838 remain 19%)
c [simplification-12] removed 27526 irredundant clauses 7.3% (348690 remain 25%)
c [simplification-12] maximum reduction of 7% = max (7%, 7%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 40034 (soft 30034 + delta 10000)
c [simplification-12] new conflict limit 30034 (hard 40034)
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   79.7   61837   348690     28059   14655   3424 104091   20   173   43  12%      1  129   22    5  412%
c i   79.8   61836   348690     28124   14708   3429 104096   20   173   43  11%      1  130   21    5  400%
c i   80.2   61833   348690     28425   14969   3446 104115   20   173   43  11%      1  129   17    5  322%
c i   80.4   61827   348690     28615   15131   3455 104127   20   174   43  11%      1  129   22    5  399%
c i   80.4   61826   348690     28638   15150   3456 104128   20   173   43  11%      1  129   21    5  382%
c i   80.4   61822   348690     28639   15150   3456 104128   20   173   43  11%      1  129   21    5  380%
c i   80.5   61791   348690     28713   15209   3464 104133   20   171   43  11%      1  127   17    5  320%
c i   80.5   61789   348690     28750   15242   3465 104135   20   171   43  11%      1  126   17    5  306%
c i   80.5   61784   348690     28751   15242   3465 104135   19   171   43  11%      1  126   17    5  305%
c i   80.5   61778   348690     28784   15265   3466 104142   19   170   43  11%      1  125   15    5  279%
c i   80.5   61772   348690     28798   15275   3469 104142   19   170   43  11%      1  125   15    5  269%
c i   80.9   61765   348690     29195   15637   3483 104154   19   171   43  11%      2  125   21    6  383%
c i   81.5   61762   348690     29906   16238   3514 104176   22   169   43  13%      4  122   32    6  553%
c i   81.6   61748   348690     29914   16244   3514 104177   22   169   43  13%      4  122   31    6  537%
c i   81.6   61745   348690     29958   16282   3516 104180   22   169   43  13%      3  122   29    6  498%
c i   81.7   61742   348690     29972   16295   3516 104180   22   170   43  13%      3  123   29    6  495%
c 
c [simplification-13] limit 30055 conflicts (hard 40034) hit after 30056 conflicts
c [quatres-9] found 28724 quaternary clauses 51% in total
c [quatres-9-1] removed 3 duplicate quaternary clauses
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 19 quaternary resolvents
c [ternres-8] limit 7983746 with penalty 0 = 0 + 0
c [ternres-8] all 61739 free variables schedulable
c [ternres-8] 1353 ternary resolvents (2 bin, 1351 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-8] limit 2000000 penalty 0 = 0 + 0
c [gauss-8] extracted 99 xors of average arity 2.7
c [gauss-8] connected 272 occurrences of 219 variables (average 1.2)
c [gauss-8] limit 2000000 penalty 0 = 0 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 22 variables
c [unhide-13] limit 1596749 with penalty 0 = 0 + 0
c [unhide-13-13] 3 units, 22 failed, 3611 tauts, 0 hbrs, 14984 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 197 transitive binary clauses
c [transred-9] found 3 units
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 61637 variables 100%
c [elim-12] limit of 159674937 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 708 variables 1% in round 1 in 28189200 steps
c [elim-12-1] backward subsumption/strengthening limit 28189200
c [elim-12-1-1] backward checking 3384 touched variables 5%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 36 and strengthened 47 clauses in 952940 steps
c [elim-12-1] rescheduled 166 variables 0% by backward subsumption
c [elim-12-2] eliminated 22 variables 0% in round 2 in 140379 steps
c [elim-12-2] backward subsumption/strengthening limit 140300
c [elim-12-2-1] backward checking 138 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 12 and strengthened 11 clauses in 115742 steps
c [elim-12-2] rescheduled 51 variables 0% by backward subsumption
c [elim-12-3] eliminated 6 variables 0% in round 3 in 112847 steps
c [elim-12-3] backward subsumption/strengthening limit 112800
c [elim-12-3-1] backward checking 52 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 4 and strengthened 5 clauses in 80362 steps
c [elim-12] incomplete 16 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 745 = 1% variables out of 61637 scheduled
c [bca-9] limit of 10000000 steps and 685571 added (scaled 2)
c [bca-9] 95946 out of 121786 literals actually usable 79%
c [bca-9] added 36 blocked clauses in 244867 steps
c [sweep-9] limit 2395124 penalty 0 = 0 + 0
c [sweep-9-1] 3730 pos 6.3% + 55446 neg 93.7% = 59176 sched 97.2% ret 1716
c [sweep-9-1] 2491226 steps 35 queries 12833.89 avg class size
c [sweep-9-1] 677 decisions 26 SAT calls 124.92 avg env size
c [sweep-9-1] 58952 variables remain 97% (1929 retained 3%)
c [decomp-37] removed 36 variables
c [sweep-9-1] removed 36 vars (0 failed, 9 eqs, 13 impls)
c [sweep-9] 36 < 1/1000 * 60892 = 60 considered unsuccessful
c [sweep-9] removed 36 vars in TOTAL (1 rounds, 34 queries)
c [phase-count-13] 340673 negative 99.5% of 342223 except 1550 0.5%
c [phase-count-13] 273760 positive 80.0% of 342223 except 68463 20.0%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 60856 enqueued variables after 30056 conflicts
c [score-dist-13] active 0 (0%), one 35108 (58%), zero 25748 (42%)
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 883 variables 1.4% (60856 remain 19%)
c [simplification-13] removed 6467 irredundant clauses 1.9% (342223 remain 24%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-13] new conflict interval 17332
c [simplification-13] penalized conflict interval 17332 = 1 * 17332
c [simplification-13] hard conflict limit 57388 (soft 47388 + delta 10000)
c [simplification-13] new conflict limit 47388 (hard 57388)
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   85.2   60855   342223     30212   15661   4254 102777   22   171   44  13%      3  123   26    6  443%
c i   85.2   60852   342223     30233   15679   4256 102777   22   171   44  13%      3  123   25    6  420%
c i   85.4   60842   342223     30425   15853   4264 102780   22   169   44  13%      2  121   24    6  408%
c i   85.7   60841   342223     30654   16062   4271 102785   22   170   44  13%      2  121   22    6  365%
c i   85.7   60839   342223     30666   16072   4272 102785   22   170   44  13%      2  121   21    6  352%
c i   85.8   60834   342223     30714   16113   4275 102787   22   170   44  13%      2  122   20    6  328%
c i   85.9   60833   342223     30830   16212   4280 102793   22   170   44  13%      2  121   18    6  306%
c i   85.9   60822   342223     30831   16212   4280 102793   22   170   44  13%      2  121   18    6  305%
c i   85.9   60820   342223     30832   16212   4280 102793   22   170   44  13%      2  121   18    6  303%
c i   86.1   60817   342223     30981   16347   4286 102797   21   169   44  13%      2  120   17    6  282%
c i   86.2   60809   342223     31121   16469   4293 102805   21   168   44  13%      2  118   14    6  231%
c i   86.8   60808   342223     31729   17003   4320 102832   20   165   44  12%      3  115   15    6  247%
c i   86.8   60793   342223     31769   17038   4322 102833   20   164   44  12%      3  114   15    6  242%
c i   86.8   60790   342223     31779   17047   4322 102833   20   165   44  12%      3  115   15    6  247%
c i   87.0   60788   342223     31867   17128   4325 102835   20   167   44  12%      2  117   19    6  304%
c i   87.1   60785   342223     31970   17220   4328 102837   21   169   44  12%      2  118   21    6  339%
c i   87.2   60781   342223     32043   17281   4332 102840   21   170   44  12%      2  119   29    6  455%
c i   87.2   60780   342223     32044   17281   4332 102840   21   170   44  12%      2  119   28    6  453%
c i   87.2   60775   342223     32045   17281   4332 102840   21   170   44  12%      2  119   28    6  451%
c i   87.2   60772   342223     32046   17281   4332 102840   21   170   44  12%      2  119   28    6  449%
c i   87.2   60771   342223     32079   17310   4334 102841   21   170   44  12%      2  120   27    6  427%
c i   87.3   60769   342223     32090   17318   4334 102843   21   171   44  12%      2  120   26    6  417%
c i   87.4   60765   342223     32170   17385   4341 102845   21   171   44  12%      2  120   24    6  374%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   87.9   60735   342223     32667   17818   4359 102865   22   171   44  13%      2  119   31    6  471%
c i   88.0   60732   342223     32756   17899   4363 102868   22   173   44  13%      2  121   28    7  436%
c i   88.0   60727   342223     32757   17899   4363 102868   22   173   44  13%      2  120   28    7  434%
c i   88.4   60697   342223     33186   18273   4377 102894   23   178   44  13%      2  125   31    7  461%
c i   88.8   60689   342223     33499   18543   4397 102906   24   178   44  13%      2  124   30    7  438%
c i   88.9   60680   342223     33622   18649   4404 102914   24   178   44  14%      2  125   32    7  464%
c i   89.4   60666   342223     34042   19011   4427 102932   24   183   44  13%      2  129   31    7  449%
c i   89.5   60662   342223     34130   19081   4436 102936   24   182   44  13%      2  127   25    7  354%
c i   89.6   60658   342223     34246   19183   4440 102943   24   181   44  13%      2  126   27    7  390%
c i   90.0   60642   342223     34647   19540   4458 102957   24   183   44  13%      2  127   26    7  368%
c i   90.5   60641   342223     35060   19899   4476 102986   24   183   44  13%      2  127   19    7  257%
c i   90.6   60639   342223     35142   19973   4480 102987   24   185   44  13%      2  128   19    7  270%
c i   90.9   60638   342223     35357   20161   4493 102994   24   183   44  13%      2  126   21    7  288%
c i   91.0   60634   342223     35512   20293   4503 102997   24   183   44  13%      2  125   30    7  404%
c i   91.8   60632   342223     36118   20834   4523 103022   25   187   45  13%      3  128   30    8  399%
c i   91.8   60620   342223     36144   20854   4526 103024   24   187   45  13%      3  128   28    8  370%
c i   91.8   60619   342223     36157   20865   4527 103024   24   186   45  13%      3  128   28    8  367%
c i   92.3   60618   342223     36650   21297   4546 103037   26   184   45  14%      3  125   34    8  444%
c i   92.6   60605   342223     36921   21546   4557 103042   27   187   45  14%      3  127   36    8  462%
c i   93.2   60602   342223     37601   22117   4578 103067   29   178   46  16%      4  116   39    8  476%
c i   93.2   60601   342223     37618   22129   4578 103068   29   178   46  16%      4  116   38    8  461%
c i   93.2   60588   342223     37619   22129   4578 103068   29   178   46  16%      4  116   38    8  459%
c i   93.4   60585   342223     37785   22268   4587 103076   29   177   46  16%      3  115   35    8  419%
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   93.4   60584   342223     37792   22274   4587 103076   29   177   46  16%      3  115   34    8  410%
c i   93.7   60583   342223     38035   22496   4596 103083   30   182   47  16%      3  120   42    8  503%
c i   93.8   60582   342223     38071   22530   4596 103084   30   182   47  16%      3  120   42    8  496%
c i   93.8   60579   342223     38114   22561   4599 103088   30   181   47  16%      2  119   38    8  448%
c i   93.9   60578   342223     38139   22580   4601 103088   30   181   47  16%      2  119   38    8  453%
c i   94.0   60577   342223     38221   22658   4602 103090   30   183   47  17%      2  120   44    9  515%
c i   94.2   60573   342223     38369   22795   4604 103093   31   184   47  17%      2  122   43    9  496%
c i   94.3   60550   342223     38472   22879   4613 103099   30   184   47  17%      2  121   36    9  417%
c i   94.4   60546   342223     38562   22956   4622 103100   30   183   47  17%      2  120   34    9  393%
c i   94.8   60540   342223     38942   23295   4631 103109   31   186   48  17%      2  123   40    9  460%
c i   95.0   60538   342223     39126   23459   4641 103112   31   185   48  17%      2  121   32    9  362%
c i   95.4   60535   342223     39414   23723   4647 103117   32   190   48  17%      2  126   42    9  466%
c i   95.5   60534   342223     39504   23802   4653 103119   32   190   49  17%      1  126   38    9  422%
c i   96.0   60533   342223     40154   24404   4670 103136   31   181   49  17%      3  115   30    9  321%
c i   97.2   60532   342223     41139   25272   4696 103169   34   185   49  19%      6  117   36   10  368%
c i   97.3   60528   342223     41278   25391   4708 103174   34   184   49  18%      5  115   29   10  300%
c i   97.3   60527   342223     41329   25434   4713 103174   34   183   49  18%      5  115   29   10  292%
c i   97.4   60526   342223     41364   25465   4713 103177   34   184   49  18%      5  115   27   10  272%
c i   97.5   60504   342223     41464   25557   4714 103181   33   185   49  18%      4  117   25   10  254%
c i   97.7   60503   342223     41645   25700   4730 103197   33   183   49  18%      4  114   21   10  216%
c i   97.8   60497   342223     41707   25750   4732 103205   32   183   49  18%      3  114   21   10  215%
c i   97.8   60496   342223     41732   25769   4732 103205   32   182   49  18%      3  113   21   10  210%
c i   97.9   60495   342223     41781   25794   4734 103207   32   180   49  18%      3  111   21   10  211%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   97.9   59999   342223     41826   25834   4734 103211   32   180   49  18%      3  111   20   10  204%
c i   98.0   59998   342223     41894   25885   4739 103219   32   180   49  18%      3  111   23   10  231%
c i   98.0   59994   342223     41895   25885   4739 103219   32   180   49  18%      3  111   23   10  230%
c i   98.7   59991   342223     42491   26426   4765 103235   32   183   50  18%      3  113   28   10  273%
c i   98.8   59986   342223     42573   26497   4771 103237   32   183   50  18%      3  113   29   10  290%
c i   99.3   59976   342223     42967   26865   4785 103242   32   183   50  17%      3  112   30   10  297%
c i   99.5   59975   342223     43067   26952   4788 103243   33   185   50  18%      2  114   47   10  457%
c i   99.5   59974   342223     43086   26968   4788 103244   33   185   50  18%      2  113   45   10  434%
c i   99.8   59970   342223     43347   27197   4796 103253   33   182   50  18%      2  111   41   10  396%
c i  100.1   59969   342223     43584   27420   4802 103257   33   183   50  18%      2  111   38   11  362%
c i  100.2   59968   342223     43648   27480   4803 103258   34   184   50  18%      2  112   40   11  378%
c i  100.4   59967   342223     43786   27603   4808 103262   33   183   51  18%      1  111   36   11  339%
c i  100.8   59966   342223     44075   27855   4819 103274   33   184   51  18%      1  111   32   11  300%
c i  101.2   59965   342223     44350   28101   4831 103285   33   184   51  18%      1  111   30   11  277%
c i  101.3   59964   342223     44422   28167   4834 103285   34   186   51  18%      1  113   48   11  443%
c i  101.4   59963   342223     44492   28228   4836 103285   35   186   51  19%      1  113   54   11  497%
c i  101.5   59961   342223     44545   28275   4836 103289   35   186   51  19%      1  112   47   11  430%
c i  101.5   59958   342223     44546   28275   4836 103289   35   186   51  19%      1  112   47   11  429%
c i  101.8   59953   342223     44819   28520   4846 103302   34   184   51  18%      1  110   29   11  261%
c i  101.8   59952   342223     44869   28567   4847 103302   34   183   51  18%      1  109   27   11  246%
c i  102.1   59949   342223     45040   28721   4849 103305   35   185   52  19%      1  110   44   11  391%
c i  102.2   59948   342223     45105   28782   4850 103305   35   185   52  19%      1  110   48   11  432%
c i  102.2   59947   342223     45111   28786   4850 103306   35   185   52  19%      1  110   47   11  424%
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  102.6   59942   342223     45458   29099   4863 103317   35   183   53  19%      1  107   37   11  324%
c i  103.1   59941   342223     45951   29540   4877 103329   34   184   53  19%      2  108   29   11  252%
c i  103.5   59940   342223     46276   29832   4889 103339   34   181   53  19%      2  105   27   12  238%
c i  103.7   59925   342223     46404   29949   4892 103340   34   181   53  19%      1  104   36   12  306%
c i  104.0   59924   342223     46614   30143   4897 103344   34   182   53  19%      1  105   36   12  313%
c i  104.2   59923   342223     46728   30248   4899 103349   34   183   53  19%      1  105   35   12  302%
c i  104.2   59922   342223     46779   30295   4899 103350   34   182   53  19%      1  105   36   12  304%
c i  104.4   59921   342223     46896   30397   4903 103355   34   181   53  19%      1  103   31   12  265%
c 
c [simplification-14] limit of 462 iterations hit after 462 iterations
c [quatres-10] found 27690 quaternary clauses 50% in total
c [quatres-10-2] added 5 single-self-subsuming ternary resolvents
c [quatres-10-2] added 24 quaternary resolvents
c [ternres-9] limit 12908515 with penalty 0 = 0 + 0
c [ternres-9] all 59908 free variables schedulable
c [ternres-9] 468 ternary resolvents (2 bin, 466 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-38] removed 1051 variables
c [unhide-14] limit 2581703 with penalty 0 = 0 + 0
c [unhide-14-15] 17 units, 246 failed, 8322 tauts, 0 hbrs, 135412 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 149 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 80678222 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 40
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 24
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 23
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 22
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 21
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 20
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 19
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 18
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 17
c [cce-4-1] eliminated 4 clauses out of 7 (57%) of length 16
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 15
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 14
c [cce-4-1] eliminated 4 clauses out of 10 (40%) of length 13
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 12
c [cce-4-1] eliminated 5 clauses out of 11 (45%) of length 11
c [cce-4-1] eliminated 4 clauses out of 60 (7%) of length 10
c [cce-4-1] eliminated 6 clauses out of 168 (4%) of length 9
c [cce-4-1] eliminated 5 clauses out of 283 (2%) of length 8
c [cce-4-1] eliminated 28 clauses out of 469 (6%) of length 7
c [cce-4-1] eliminated 93 clauses out of 1274 (7%) of length 6
c [cce-4-1] eliminated 7052 clauses out of 19416 (36%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 7242 large clauses in 80678224 steps
c [cce-4-1] allowing another 40339112 steps for small clauses
c [cce-4-1] scheduling 242651 clauses = 171129 binary + 71522 ternary
c [cce-4-1] tried to eliminate 1589 small clauses 1%
c [cce-4-1] eliminated 271 binary clauses 0%
c [cce-4-1] eliminated 181 ternary clauses 0%
c [cce-4-1] eliminated 452 small clauses 0%
c [cce-4-1] eliminated 918 small clauses in 80678222 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 8160 covered clauses in round 1
c [cce-4] eliminated 8160 covered clauses in TOTAL during 1 rounds
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 59409 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 5968 variables 10% in round 1 in 25221280 steps
c [elim-13-1] backward subsumption/strengthening limit 25221200
c [elim-13-1-1] backward checking 18198 touched variables 31%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 85 and strengthened 117 clauses in 3096990 steps
c [elim-13-1] rescheduled 494 variables 1% by backward subsumption
c [elim-13-2] eliminated 59 variables 0% in round 2 in 389218 steps
c [elim-13-2] backward subsumption/strengthening limit 389200
c [elim-13-2-1] backward checking 447 touched variables 1%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 42 and strengthened 46 clauses in 384431 steps
c [elim-13-2] rescheduled 148 variables 0% by backward subsumption
c [elim-13-3] eliminated 10 variables 0% in round 3 in 179643 steps
c [elim-13-3] backward subsumption/strengthening limit 179600
c [elim-13-3-1] backward checking 68 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 10 and strengthened 14 clauses in 179601 steps
c [elim-13] incomplete 31 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 6057 = 10% variables out of 59409 scheduled
c [bca-10] limit of 10000000 steps and 613611 added (scaled 2)
c [bca-10] 88790 out of 106706 literals actually usable 83%
c [bca-10] added 130 blocked clauses in 223049 steps
c [phase-count-14] 305269 negative 99.6% of 306385 except 1116 0.4%
c [phase-count-14] 241117 positive 78.7% of 306385 except 65268 21.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 53352 enqueued variables after 46896 conflicts
c [score-dist-14] active 0 (0%), one 30418 (57%), zero 22934 (43%)
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 6556 variables 10.9% (53352 remain 17%)
c [simplification-14] removed 35838 irredundant clauses 10.5% (306385 remain 22%)
c [simplification-14] maximum reduction of 11% = max (11%, 10%)
c [simplification-14] forced so keeping old conflict interval 17332
c [simplification-14] conflict limit remains at 47481 (hard 57388)
c [simplification-14] new iteration interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  110.8   53351   306385     46912    9454   4472 88170   34   180   37  19%      1  103   30   12  253%
c i  111.2   53348   306385     47295    9802   4488 88183   32   177   37  18%      1   99   16   12  137%
c i  111.2   53343   306385     47329    9833   4489 88183   32   176   37  18%      1   98   18   12  153%
c i  111.3   53339   306385     47362    9859   4492 88183   32   176   37  18%      1   98   17   12  143%
c 
c [simplification-15] limit 47481 conflicts (hard 57388) hit after 47481 conflicts
c [quatres-11] found 30245 quaternary clauses 62% in total
c [quatres-11-1] removed 5 duplicate quaternary clauses
c [quatres-11-2] added 41 quaternary resolvents
c [ternres-10] limit 13080634 with penalty 0 = 0 + 0
c [ternres-10] all 53338 free variables schedulable
c [ternres-10] 1068 ternary resolvents (1 bin, 1067 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 408769 penalty 4 = 4 + 0
c [card-5] found 1799 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 408769 for elimination
c [card-5] 1799 out of 1799 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-9] limit 1308063 penalty 1 = 1 + 0
c [gauss-9] extracted 74 xors of average arity 2.7
c [gauss-9] connected 200 occurrences of 101 variables (average 2.0)
c [gauss-9] limit 1308063 penalty 1 = 1 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-39] removed 17 variables
c [treelook-5] limit 327015 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 48459 literals 45%
c [treelook-5] scheduling used 327017 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 327015 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 474354 steps
c [treelook-5] 48433 literals remain 45%
c [treelook-5] 9563 variables remain to probed next time 18%
c [decomp-40] removed 9 variables
c [treelook-5] removed 21 variables, found 2946 hbrs
c [unhide-15] limit 2616126 with penalty 0 = 0 + 0
c [unhide-15-17] 6 units, 170 failed, 5738 tauts, 0 hbrs, 9249 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 120 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 53099 variables 100%
c [block-5] limit of 16350792 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 34 blocked clauses
c [block-5] 34 < 1/100 * 304432 = 3044 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 53099 variables 100%
c [elim-14] limit of 261612684 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 510 variables 1% in round 1 in 23727608 steps
c [elim-14-1] backward subsumption/strengthening limit 23727600
c [elim-14-1-1] backward checking 2993 touched variables 6%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 43 and strengthened 29 clauses in 797274 steps
c [elim-14-1] rescheduled 148 variables 0% by backward subsumption
c [elim-14-2] eliminated 16 variables 0% in round 2 in 112053 steps
c [elim-14-2] backward subsumption/strengthening limit 112000
c [elim-14-2-1] backward checking 111 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 14 and strengthened 9 clauses in 98027 steps
c [elim-14-2] rescheduled 45 variables 0% by backward subsumption
c [elim-14-3] eliminated 3 variables 0% in round 3 in 56678 steps
c [elim-14-3] backward subsumption/strengthening limit 56600
c [elim-14-3-1] backward checking 29 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 2 and strengthened 5 clauses in 56601 steps
c [elim-14] incomplete 15 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 543 = 1% variables out of 53099 scheduled
c [bca-11] limit of 10000000 steps and 603828 added (scaled 2)
c [bca-11] 86569 out of 105114 literals actually usable 82%
c [bca-11] added 28 blocked clauses in 215804 steps
c [sweep-10] limit 1962095 penalty 1 = 1 + 0
c [sweep-10-1] 3654 pos 7.2% + 47397 neg 92.8% = 51051 sched 97.1% ret 1505
c [sweep-10-1] 1988867 steps 29 queries 6585.24 avg class size
c [sweep-10-1] 270 decisions 24 SAT calls 78.29 avg env size
c [sweep-10-1] 50859 variables remain 97% (1695 retained 3%)
c [decomp-41] removed 52 variables
c [sweep-10-1] removed 52 vars (0 failed, 5 eqs, 10 impls)
c [sweep-10] removed 52 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-15] 300283 negative 99.6% of 301338 except 1055 0.4%
c [phase-count-15] 237088 positive 78.7% of 301338 except 64250 21.3%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 52504 enqueued variables after 47481 conflicts
c [score-dist-15] active 0 (0%), one 30132 (57%), zero 22372 (43%)
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 834 variables 1.6% (52504 remain 16%)
c [simplification-15] removed 5047 irredundant clauses 1.6% (301338 remain 21%)
c [simplification-15] maximum reduction of 2% = max (2%, 2%)
c [simplification-15] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-15] new conflict interval 23998
c [simplification-15] penalized conflict interval 23998 = 1 * 23998
c [simplification-15] hard conflict limit 83478 (soft 71479 + delta 11999)
c [simplification-15] new conflict limit 71479 (hard 83478)
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  114.9   52503   301338     47670    9987   4782 86914   30   174   37  17%      1   96   14   12  118%
c i  115.0   52502   301338     47736   10046   4784 86916   30   175   37  17%      1   96   16   12  135%
c i  115.1   52498   301338     47884   10166   4797 86920   30   174   37  17%      1   95   18   12  150%
c i  115.1   52497   301338     47892   10171   4798 86920   30   174   37  17%      1   95   17   12  147%
c i  115.1   52496   301338     47948   10219   4804 86921   30   174   37  17%      1   95   17   12  145%
c i  115.1   52495   301338     47949   10219   4804 86921   30   174   37  17%      1   95   17   12  145%
c i  115.3   52494   301338     48108   10360   4811 86928   29   173   37  17%      1   93   21   12  175%
c i  115.9   52486   301338     48889   11058   4854 86952   27   169   37  16%      3   89   18   12  153%
c i  116.0   52483   301338     48962   11122   4856 86954   28   170   37  16%      3   89   25   12  212%
c i  116.2   52474   301338     49117   11258   4866 86960   27   169   37  16%      3   88   19   12  162%
c i  116.3   52471   301338     49226   11342   4882 86967   26   168   37  16%      2   87   15   12  127%
c i  116.3   52470   301338     49252   11366   4883 86967   26   167   37  16%      2   87   14   12  122%
c i  116.8   52469   301338     49794   11848   4906 86989   25   167   37  15%      3   86   17   12  146%
c i  117.1   52465   301338     50181   12190   4925 86999   25   167   38  15%      2   85   20   12  166%
c i  117.1   52462   301338     50256   12259   4927 87001   25   166   38  15%      2   84   18   12  151%
c i  117.1   52459   301338     50257   12259   4927 87001   25   166   38  15%      2   84   18   12  151%
c i  117.6   52458   301338     50985   12908   4949 87028   24   168   38  14%      4   85   19   12  160%
c i  117.8   52455   301338     51235   13134   4957 87036   24   167   38  14%      3   84   20   12  165%
c i  117.9   52453   301338     51437   13313   4965 87045   24   168   38  14%      3   85   25   12  204%
c i  118.1   52413   301338     51644   13502   4970 87054   24   168   38  14%      2   84   25   12  203%
c i  118.2   52409   301338     51750   13604   4970 87055   24   172   38  14%      2   87   25   12  201%
c i  118.4   52405   301338     52031   13849   4979 87065   24   174   38  14%      2   89   27   12  217%
c i  118.7   52399   301338     52436   14209   4990 87083   24   172   39  14%      2   87   25   12  203%
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  118.7   52398   301338     52493   14263   4990 87085   24   172   39  14%      2   87   25   12  206%
c i  118.9   52396   301338     52725   14471   4997 87090   25   174   39  14%      1   89   25   12  198%
c i  119.0   52393   301338     52900   14617   5003 87098   24   170   39  14%      1   85   24   12  189%
c i  119.5   52388   301338     53527   15170   5027 87119   24   168   40  14%      2   81   18   13  148%
c i  119.5   52384   301338     53528   15170   5027 87119   24   168   40  14%      2   81   18   13  147%
c i  119.6   52376   301338     53677   15293   5033 87127   23   166   40  14%      2   80   18   13  141%
c i  119.9   52364   301338     53981   15574   5034 87131   24   165   40  14%      2   78   26   13  204%
c i  119.9   52363   301338     54135   15703   5039 87138   24   164   40  14%      2   77   27   13  213%
c i  120.2   52356   301338     54437   15976   5050 87144   24   164   40  15%      1   76   28   13  219%
c i  120.4   52349   301338     54779   16297   5062 87149   24   164   40  15%      1   77   26   13  205%
c i  121.5   52252   301338     56193   17567   5112 87184   26   166   41  16%      9   76   38   13  292%
c i  121.8   52248   301338     56528   17868   5122 87190   27   169   41  16%      7   79   42   13  314%
c i  122.8   52246   301338     57737   18978   5143 87219   29   167   42  17%      9   76   42   14  307%
c i  123.3   52243   301338     58310   19507   5160 87227   29   164   43  18%      6   72   28   14  206%
c i  123.8   52242   301338     58970   20111   5180 87244   32   166   44  19%      5   73   50   14  356%
c i  124.1   52234   301338     59361   20443   5193 87256   31   164   44  19%      4   70   30   14  209%
c i  124.2   52233   301338     59422   20498   5195 87257   31   164   44  19%      4   71   32   14  227%
c i  124.5   52231   301338     59710   20766   5200 87260   32   167   44  19%      3   74   44   14  305%
c i  124.6   52230   301338     59862   20905   5204 87262   32   165   44  19%      2   72   42   14  293%
c i  124.7   52227   301338     59968   20988   5209 87266   33   166   44  20%      2   72   51   14  351%
c i  124.7   52223   301338     59969   20988   5209 87266   33   166   44  20%      2   72   51   14  350%
c i  124.7   52213   301338     59974   20991   5208 87267   33   166   44  20%      2   72   50   14  345%
c i  125.4   52212   301338     60650   21627   5209 87275   35   168   45  21%      3   74   51   15  343%
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  126.8   52199   301338     62332   23184   5249 87314   32   161   45  20%     12   65   28   15  183%
c i  127.3   52198   301338     62806   23606   5254 87331   32   159   46  20%      8   63   25   15  164%
c i  127.3   52197   301338     62813   23612   5254 87331   31   159   46  20%      8   62   24   15  161%
c i  127.4   52181   301338     62892   23684   5256 87331   32   160   46  20%      8   63   34   15  221%
c i  127.4   52165   301338     62956   23739   5256 87332   33   160   46  20%      7   63   41   15  272%
c i  128.3   52158   301338     63924   24611   5277 87363   34   164   46  21%      7   66   40   16  253%
c i  128.4   52157   301338     63972   24654   5278 87365   34   163   46  21%      6   65   35   16  222%
c i  128.6   52156   301338     64242   24903   5284 87373   34   161   46  21%      5   63   35   16  225%
c i  128.8   52154   301338     64445   25078   5284 87376   34   161   46  21%      4   63   36   16  226%
c i  129.5   52153   301338     65195   25759   5307 87391   34   157   47  22%      4   58   33   16  205%
c i  130.3   52151   301338     66048   26543   5322 87405   34   156   47  22%      5   57   35   16  216%
c i  131.0   52138   301338     66785   27203   5346 87427   34   155   48  22%      4   54   29   16  179%
c i  131.4   52137   301338     67221   27604   5356 87430   34   153   50  22%      3   52   43   17  259%
c i  131.9   52136   301338     67702   28041   5366 87444   33   152   51  22%      3   51   30   17  182%
c i  132.3   52135   301338     68165   28461   5374 87453   33   152   51  22%      2   51   33   17  200%
c i  133.4   52130   301338     69261   29491   5395 87469   35   155   52  23%      6   52   29   17  172%
c i  134.1   52129   301338     69887   30073   5410 87476   34   151   52  23%      4   48   30   17  173%
c i  135.2   52128   301338     70987   31076   5430 87499   35   150   53  23%      6   47   39   18  222%
c i  135.6   52127   301338     71382   31423   5437 87507   37   149   54  25%      5   45   55   18  310%
c 
c [simplification-16] limit 71523 conflicts (hard 83478) hit after 71523 conflicts
c [quatres-12] found 29679 quaternary clauses 60% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-2] added 7 single-self-subsuming ternary resolvents
c [quatres-12-2] added 19 quaternary resolvents
c [ternres-11] limit 18742518 with penalty 0 = 0 + 0
c [ternres-11] all 52127 free variables schedulable
c [ternres-11] 734 ternary resolvents (4 bin, 730 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-42] removed 488 variables
c [basicprobe-5] limit 93712592 penalty 0 = 0 + 0
c [basicprobe-5-0] 8675 probes remain 17% after last round
c [basicprobe-5-0] 829 units = 805 failed (97%) + 24 lifted (3%)
c [basicprobe-5-0] removed 2231 variables, found 97799 hbrs
c [bate-3] eliminated 487 asymmetric tautologies during probing
c [unhide-16] limit 3748503 with penalty 0 = 0 + 0
c [unhide-16-19] 10 units, 302 failed, 21782 tauts, 0 hbrs, 244541 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 252 transitive binary clauses
c [transred-12] found 2 units
c [cce-5] limit of 23428148 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 20 (5%) of length 10
c [cce-5-1] eliminated 3 clauses out of 90 (3%) of length 8
c [cce-5-1] eliminated 3 clauses out of 187 (2%) of length 7
c [cce-5-1] eliminated 28 clauses out of 935 (3%) of length 6
c [cce-5-1] eliminated 1890 clauses out of 10606 (18%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1925 large clauses in 23428152 steps
c [cce-5-1] allowing another 11714076 steps for small clauses
c [cce-5-1] scheduling 203139 clauses = 143144 binary + 59995 ternary
c [cce-5-1] tried to eliminate 629 small clauses 0%
c [cce-5-1] eliminated 137 binary clauses 0%
c [cce-5-1] eliminated 52 ternary clauses 0%
c [cce-5-1] eliminated 189 small clauses 0%
c [cce-5-1] eliminated 563 small clauses in 23428153 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2488 covered clauses in round 1
c [cce-5] eliminated 2488 covered clauses in TOTAL during 1 rounds
c [cce-5] 2488 < 1/100 * 275047 = 2750 considered unsuccessful
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 49264 variables 100%
c [elim-15] limit of 374850371 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 3957 variables 8% in round 1 in 20784520 steps
c [elim-15-1] backward subsumption/strengthening limit 20784500
c [elim-15-1-1] backward checking 13804 touched variables 28%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 172 and strengthened 202 clauses in 2647490 steps
c [elim-15-1] rescheduled 971 variables 2% by backward subsumption
c [elim-15-2] eliminated 72 variables 0% in round 2 in 554055 steps
c [elim-15-2] backward subsumption/strengthening limit 554000
c [elim-15-2-1] backward checking 620 touched variables 1%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 35 and strengthened 41 clauses in 295171 steps
c [elim-15-2] rescheduled 174 variables 0% by backward subsumption
c [elim-15-3] eliminated 11 variables 0% in round 3 in 143381 steps
c [elim-15-3] backward subsumption/strengthening limit 143300
c [elim-15-3-1] backward checking 101 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 2 and strengthened 5 clauses in 133988 steps
c [elim-15] incomplete 25 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 4058 = 8% variables out of 49264 scheduled
c [bca-12] limit of 10000000 steps and 525662 added (scaled 2)
c [bca-12] 69768 out of 90414 literals actually usable 77%
c [bca-12] added 72 blocked clauses in 179106 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 56227550 penalty 0 = 0 + 0
c [sweep-11-1] 2823 pos 6.4% + 41077 neg 93.6% = 43900 sched 97.1% ret 1306
c [sweep-11-1] 56285700 steps 884 queries 261.47 avg class size
c [sweep-11-1] 8971 decisions 727 SAT calls 75.43 avg env size
c [sweep-11-1] 25410 variables remain 57% (19421 retained 43%)
c [decomp-43] removed 955 variables
c [sweep-11-1] removed 955 vars (0 failed, 179 eqs, 224 impls)
c [sweep-11] removed 955 vars in TOTAL (1 rounds, 883 queries)
c [phase-count-16] 257547 negative 99.6% of 258501 except 954 0.4%
c [phase-count-16] 197852 positive 76.5% of 258501 except 60649 23.5%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 44251 enqueued variables after 71523 conflicts
c [score-dist-16] active 0 (0%), one 28087 (63%), zero 16164 (37%)
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 7876 variables 15.1% (44251 remain 14%)
c [simplification-16] removed 42837 irredundant clauses 14.2% (258501 remain 18%)
c [simplification-16] maximum reduction of 15% = max (15%, 14%)
c [simplification-16] large reduction 15% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 83523 (soft 73523 + delta 10000)
c [simplification-16] new conflict limit 73523 (hard 83523)
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  146.7   44250   258501     72367   20393   4554 154150   34   141   43  24%      6   36   24   18  132%
c i  146.7   44248   258501     72379   20401   4557 154150   34   141   43  24%      6   36   23   18  129%
c i  146.9   44247   258501     72706   20704   4564 154156   32   139   43  23%      4   34   18   18  101%
c 
c [simplification-17] limit 73523 conflicts (hard 83523) hit after 73523 conflicts
c [quatres-13] found 26176 quaternary clauses 62% in total
c [quatres-13-1] removed 6 duplicate quaternary clauses
c [quatres-13-2] added 20 single-self-subsuming ternary resolvents
c [quatres-13-2] added 44 quaternary resolvents
c [ternres-12] limit 19163386 with penalty 0 = 0 + 0
c [ternres-12] all 44247 free variables schedulable
c [ternres-12] 2159 ternary resolvents (6 bin, 2153 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-44] removed 5 variables
c [simpleprobe-6] all 44246 free variables schedulable
c [simpleprobe-6] limit 76653547 penalty 0 = 0 + 0
c [decomp-45] removed 1573 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 1573 variables, found 36106 hbrs, 392 units
c [unhide-17] limit 3832677 with penalty 0 = 0 + 0
c [unhide-17-22] 6 units, 194 failed, 26684 tauts, 0 hbrs, 66445 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 260 transitive binary clauses
c [transred-13] found 1 units
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 42415 variables 100%
c [elim-16] limit of 383267739 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1745 variables 4% in round 1 in 19010477 steps
c [elim-16-1] backward subsumption/strengthening limit 19010400
c [elim-16-1-1] backward checking 7628 touched variables 18%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 93 and strengthened 85 clauses in 1727583 steps
c [elim-16-1] rescheduled 442 variables 1% by backward subsumption
c [elim-16-2] eliminated 50 variables 0% in round 2 in 1300030 steps
c [elim-16-2] backward subsumption/strengthening limit 1300000
c [elim-16-2-1] backward checking 369 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 30 and strengthened 35 clauses in 295660 steps
c [elim-16-2] rescheduled 126 variables 0% by backward subsumption
c [elim-16-3] eliminated 10 variables 0% in round 3 in 1017833 steps
c [elim-16-3] backward subsumption/strengthening limit 1017800
c [elim-16-3-1] backward checking 83 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 0 and strengthened 5 clauses in 138695 steps
c [elim-16] incomplete 20 not tried 0% in round 3
c [gc-131] reconnected 157693 binary clauses (produced 0 empty 1 units)
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 1810 = 4% variables out of 42415 scheduled
c [bca-13] limit of 10000000 steps and 474252 added (scaled 2)
c [bca-13] 60376 out of 81212 literals actually usable 74%
c [bca-13] added 49 blocked clauses in 156093 steps
c [sweep-12] limit 5749016 penalty 0 = 0 + 0
c [sweep-12-1] 2394 pos 10.2% + 21025 neg 89.8% = 23419 sched 57.7% ret 17186
c [sweep-12-1] 5857338 steps 100 queries 1809.24 avg class size
c [sweep-12-1] 800 decisions 76 SAT calls 53.99 avg env size
c [sweep-12-1] 22622 variables remain 56% (17895 retained 44%)
c [decomp-46] removed 156 variables
c [sweep-12-1] removed 156 vars (0 failed, 31 eqs, 28 impls)
c [sweep-12] removed 156 vars in TOTAL (1 rounds, 99 queries)
c [phase-count-17] 234935 negative 99.6% of 235773 except 838 0.4%
c [phase-count-17] 177058 positive 75.1% of 235773 except 58715 24.9%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 40449 enqueued variables after 73523 conflicts
c [score-dist-17] active 0 (0%), one 27333 (68%), zero 13116 (32%)
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 3798 variables 8.6% (40449 remain 13%)
c [simplification-17] removed 22728 irredundant clauses 8.8% (235773 remain 17%)
c [simplification-17] maximum reduction of 9% = max (9%, 9%)
c [simplification-17] large reduction 9% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 85523 (soft 75523 + delta 10000)
c [simplification-17] new conflict limit 75523 (hard 85523)
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  152.7   40448   235773     74501   20523   4992 153373   33   136   41  24%     13   30   30   18  166%
c i  152.7   40447   235773     74515   20533   4993 153375   33   135   41  24%     13   30   29   18  160%
c 
c [simplification-18] limit 75523 conflicts (hard 85523) hit after 75527 conflicts
c [quatres-14] found 24330 quaternary clauses 61% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 4 single-self-subsuming ternary resolvents
c [quatres-14-2] added 22 quaternary resolvents
c [ternres-13] limit 19567307 with penalty 0 = 0 + 0
c [ternres-13] all 40445 free variables schedulable
c [ternres-13] 1084 ternary resolvents (3 bin, 1081 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-10] limit 978365 penalty 2 = 2 + 0
c [gauss-10] extracted 51 xors of average arity 2.9
c [gauss-10] connected 150 occurrences of 100 variables (average 1.5)
c [gauss-10] limit 978365 penalty 2 = 2 + 0
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-47] removed 7 variables
c [unhide-18] limit 3913461 with penalty 0 = 0 + 0
c [unhide-18-25] 6 units, 201 failed, 12455 tauts, 0 hbrs, 48029 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 249 transitive binary clauses
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 40198 variables 100%
c [elim-17] limit of 391346151 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 584 variables 1% in round 1 in 17958018 steps
c [elim-17-1] backward subsumption/strengthening limit 17958000
c [elim-17-1-1] backward checking 3641 touched variables 9%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 49 and strengthened 32 clauses in 939079 steps
c [elim-17-1] rescheduled 185 variables 0% by backward subsumption
c [elim-17-2] eliminated 23 variables 0% in round 2 in 856681 steps
c [elim-17-2] backward subsumption/strengthening limit 856600
c [elim-17-2-1] backward checking 194 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 12 and strengthened 20 clauses in 251088 steps
c [elim-17-2] rescheduled 67 variables 0% by backward subsumption
c [elim-17-3] eliminated 3 variables 0% in round 3 in 746918 steps
c [elim-17-3] backward subsumption/strengthening limit 746900
c [elim-17-3-1] backward checking 45 touched variables 0%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 11 and strengthened 2 clauses in 75384 steps
c [elim-17] incomplete 23 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 637 = 2% variables out of 40198 scheduled
c [bca-14] limit of 10000000 steps and 462019 added (scaled 2)
c [bca-14] 58002 out of 79124 literals actually usable 73%
c [bca-14] added 31 blocked clauses in 151999 steps
c [sweep-13] limit 5870192 penalty 0 = 0 + 0
c [sweep-13-1] 2332 pos 10.5% + 19898 neg 89.5% = 22230 sched 56.2% ret 17331
c [sweep-13-1] 5893515 steps 127 queries 1711.72 avg class size
c [sweep-13-1] 1183 decisions 107 SAT calls 67.96 avg env size
c [sweep-13-1] 21336 variables remain 54% (18203 retained 46%)
c [decomp-48] removed 87 variables
c [sweep-13-1] removed 87 vars (0 failed, 23 eqs, 27 impls)
c [sweep-13] removed 87 vars in TOTAL (1 rounds, 126 queries)
c [phase-count-18] 229382 negative 99.6% of 230204 except 822 0.4%
c [phase-count-18] 171993 positive 74.7% of 230204 except 58211 25.3%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 39474 enqueued variables after 75527 conflicts
c [score-dist-18] active 0 (0%), one 27127 (69%), zero 12347 (31%)
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 971 variables 2.4% (39474 remain 12%)
c [simplification-18] removed 5569 irredundant clauses 2.4% (230204 remain 16%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 7999 = 23998 / 3
c [simplification-18] new conflict interval 31997
c [simplification-18] penalized conflict interval 31997 = 1 * 31997
c [simplification-18] hard conflict limit 123522 (soft 107524 + delta 15998)
c [simplification-18] new conflict limit 107524 (hard 123522)
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  157.6   39473   230204     77125   22689   5213 140885   27   106   42  25%     24    0   15   18   81%
c i  157.6   39472   230204     77152   22713   5213 140887   26   106   42  25%     23   -0   14   18   77%
c i  158.3   39471   230204     78161   23659   5231 140897   28   108   42  26%     12    2   36   19  191%
c i  158.5   39470   230204     78442   23909   5238 140907   28   107   42  26%      9    1   29   19  156%
c i  159.1   39469   230204     79208   24631   5245 140913   29   107   42  27%      6    1   35   19  187%
c i  159.5   39468   230204     79728   25119   5254 140917   28   106   42  27%      4   -1   23   19  123%
c i  161.0   39467   230204     81912   27148   5294 140950   28   105   42  27%     17   -1   29   19  154%
c i  161.3   39464   230204     82418   27597   5311 140961   28   106   42  26%     10    0   32   19  164%
c i  162.3   39461   230204     83631   28711   5330 140976   30   109   45  27%      8    3   30   19  156%
c i  162.5   39457   230204     83865   28910   5343 140986   29   108   46  27%      6    2   27   19  136%
c i  163.0   39456   230204     84450   29465   5348 140989   30   109   46  27%      4    2   34   20  172%
c i  163.3   39455   230204     84861   29832   5359 141003   30   110   47  27%      2    4   38   20  192%
c i  164.0   39433   230204     85751   30683   5372 141011   30   110   48  27%      3    3   27   20  137%
c i  165.0   39432   230204     87058   31899   5389 141039   29   105   49  27%      7   -1   27   20  134%
c i  166.5   39431   230204     89025   33762   5412 141049   29   106   50  27%     14   -0   26   20  129%
c i  168.5   39429   230204     91391   35999   5434 141072   30   104   50  29%     19   -2   31   21  152%
c i  168.6   39424   230204     91463   36065   5435 141072   30   105   50  29%     18   -1   29   21  142%
c i  168.8   39423   230204     91665   36261   5436 141074   30   104   50  29%     14   -3   23   21  111%
c i  168.8   39422   230204     91748   36341   5437 141075   30   107   50  28%     13    0   23   21  112%
c i  170.7   39420   230204     94572   38957   5493 141120   30    99   51  31%     25   -6   42   21  202%
c i  170.8   39414   230204     94634   39011   5496 141122   30    99   51  30%     23   -7   36   21  173%
c i  171.2   39412   230204     95139   39486   5503 141127   30    99   51  30%     13   -7   28   21  132%
c i  171.2   39410   230204     95140   39486   5503 141127   30    99   51  30%     13   -7   28   21  132%
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  171.7   39409   230204     95869   40146   5514 141144   30    98   51  31%      7   -8   34   21  162%
c i  172.2   39402   230204     96614   40845   5530 141152   28    95   53  29%      4  -11   17   21   79%
c i  172.6   39401   230204     97092   41289   5532 141154   27    89   53  30%      2  -16   17   21   82%
c i  173.2   39400   230204     97983   42095   5544 141175   28    92   55  31%      2  -13   37   21  173%
c i  175.5   39395   230204    100584   44507   5586 141211   31    99   59  31%     20   -6   31   22  145%
c i  176.3   39394   230204    101460   45313   5598 141219   32   100   59  32%      9   -5   39   22  176%
c i  177.4   39393   230204    102662   46414   5613 141234   35   107   60  33%      6    2   36   22  161%
c i  179.3   39388   230204    105242   48839   5651 141263   30    94   60  32%     20  -11   22   22   99%
c i  181.6   39387   230204    107658   51071   5680 141286   34    98   63  34%     19   -6   38   23  163%
c i  183.7   39385   230204    110416   53745   5696 141303   27    91   63  30%     22  -13   17   23   75%
c i  184.5   39384   230204    111477   54750   5700 141309   27    89   64  31%      9  -15   38   23  166%
c i  186.3   39377   230204    114077   57229   5730 141335   25    80   64  31%     19  -23   27   23  116%
c i  186.6   39376   230204    114416   57548   5732 141338   25    79   64  31%     12  -24   23   23  101%
c i  189.1   39374   230204    117282   60222   5762 141356   28    84   76  34%     22  -19   29   23  125%
c -  190.5   39374   230204    118899   26139   5771 141367   26    73   38  35%     10  -29   16   23   67%
c i  191.7   39373   230204    120964   28073   5780 141372   23    61   43  38%     33  -39   33   23  144%
c i  191.7   39356   230204    120965   28073   5780 141372   23    61   43  38%     33  -39   33   23  144%
c 
c [simplification-19] limit 107544 conflicts (hard 123522) hit after 123523 conflicts
c [quatres-15] found 24357 quaternary clauses 57% in total
c [quatres-15-2] added 7 single-self-subsuming ternary resolvents
c [quatres-15-2] added 3 quaternary resolvents
c [ternres-14] limit 29147727 with penalty 0 = 0 + 0
c [ternres-14] all 39356 free variables schedulable
c [ternres-14] 859 ternary resolvents (2 bin, 857 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-49] removed 208 variables
c [treelook-6] limit 1457386 penalty 1 = 1 + 0 boost 1
c [treelook-6] scheduled 53168 literals 68%
c [treelook-6] scheduling used 743521 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1457386 penalty 1 = 1 + 0 boost 1
c [treelook-6] used 1477928 steps
c [treelook-6] 53146 literals remain 68%
c [treelook-6] 5806 variables remain to probed next time 15%
c [treelook-6] removed 0 variables, found 8124 hbrs
c [unhide-19] limit 5829545 with penalty 0 = 0 + 0
c [unhide-19-29] 4 units, 137 failed, 10741 tauts, 0 hbrs, 117778 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 174 transitive binary clauses
c [cce-6] limit of 18217329 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 42
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 15
c [cce-6-1] eliminated 1 clauses out of 7 (14%) of length 14
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 13
c [cce-6-1] eliminated 2 clauses out of 7 (29%) of length 12
c [cce-6-1] eliminated 2 clauses out of 7 (29%) of length 11
c [cce-6-1] eliminated 1 clauses out of 6 (17%) of length 10
c [cce-6-1] eliminated 2 clauses out of 14 (14%) of length 9
c [cce-6-1] eliminated 2 clauses out of 26 (8%) of length 8
c [cce-6-1] eliminated 4 clauses out of 88 (5%) of length 7
c [cce-6-1] eliminated 10 clauses out of 921 (1%) of length 6
c [cce-6-1] eliminated 1015 clauses out of 8529 (12%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1045 large clauses in 18217335 steps
c [cce-6-1] allowing another 9108667 steps for small clauses
c [cce-6-1] scheduling 164492 clauses = 119048 binary + 45444 ternary
c [cce-6-1] tried to eliminate 720 small clauses 0%
c [cce-6-1] eliminated 112 binary clauses 0%
c [cce-6-1] eliminated 76 ternary clauses 0%
c [cce-6-1] eliminated 188 small clauses 0%
c [cce-6-1] eliminated 412 small clauses in 18217333 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1457 covered clauses in round 1
c [cce-6] eliminated 1457 covered clauses in TOTAL during 1 rounds
c [cce-6] 1457 < 1/100 * 225834 = 2258 considered unsuccessful
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 39088 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 11659091060 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 879 variables 2% in round 1 in 17074231 steps
c [elim-18-1] backward subsumption/strengthening limit 17074200
c [elim-18-1-1] backward checking 4121 touched variables 11%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 21 and strengthened 15 clauses in 890250 steps
c [elim-18-1] rescheduled 101 variables 0% by backward subsumption
c [elim-18-2] eliminated 5 variables 0% in round 2 in 137890 steps
c [elim-18-2] backward subsumption/strengthening limit 137800
c [elim-18-2-1] backward checking 54 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 2 and strengthened 6 clauses in 79354 steps
c [elim-18-2] rescheduled 21 variables 0% by backward subsumption
c [elim-18-3] eliminated 3 variables 0% in round 3 in 71036 steps
c [elim-18-3] backward subsumption/strengthening limit 71000
c [elim-18-3-1] backward checking 24 touched variables 0%
c [elim-18-3-1] fully completed backward checking in 1 rounds
c [elim-18-3] subsumed 0 and strengthened 2 clauses in 68499 steps
c [elim-18] incomplete 8 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 887 = 2% variables out of 39088 scheduled
c [bca-15] limit of 10000000 steps and 445526 added (scaled 2)
c [bca-15] 55605 out of 76404 literals actually usable 73%
c [bca-15] added 35 blocked clauses in 148308 steps
c [sweep-14] limit 8744318 penalty 0 = 0 + 0
c [sweep-14-1] 2018 pos 9.6% + 18896 neg 90.4% = 20914 sched 54.7% ret 17287
c [sweep-14-1] 8747133 steps 201 queries 820.39 avg class size
c [sweep-14-1] 1755 decisions 173 SAT calls 70.40 avg env size
c [sweep-14-1] 19353 variables remain 51% (18818 retained 49%)
c [decomp-51] removed 106 variables
c [sweep-14-1] removed 106 vars (0 failed, 29 eqs, 39 impls)
c [sweep-14] removed 106 vars in TOTAL (1 rounds, 200 queries)
c [phase-count-19] 221076 negative 99.6% of 221885 except 809 0.4%
c [phase-count-19] 164535 positive 74.2% of 221885 except 57350 25.8%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 38095 enqueued variables after 123523 conflicts
c [score-dist-19] active 0 (0%), one 26863 (71%), zero 11232 (29%)
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 1261 variables 3.2% (38095 remain 12%)
c [simplification-19] removed 8319 irredundant clauses 3.6% (221885 remain 16%)
c [simplification-19] maximum reduction of 4% = max (3%, 4%)
c [simplification-19] geometric conflict interval increment 6399 = 31997 / 5
c [simplification-19] new conflict interval 38396
c [simplification-19] penalized conflict interval 38396 = 1 * 38396
c [simplification-19] hard conflict limit 181117 (soft 161919 + delta 19198)
c [simplification-19] new conflict limit 161919 (hard 181117)
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  200.1   38094   221885    125598   24773   6005 141912   24    58   39  41%     46  -40    9   23   39%
c i  200.5   38093   221885    126285   25414   6016 141917   24    60   42  39%     20  -38   18   23   78%
c i  202.0   38089   221885    128924   27849   6054 141946   26    72   44  36%     17  -24   49   24  207%
c i  204.7   38079   221885    133370   32047   6092 141982   24    68   46  36%     41  -27   18   24   75%
c i  204.7   38078   221885    133371   32047   6092 141982   24    68   46  36%     41  -27   18   24   75%
c i  206.5   38074   221885    136282   34800   6115 141999   22    73   49  31%     20  -21   14   23   62%
c i  208.0   38073   221885    138527   36956   6126 142010   23    66   51  34%     10  -27   30   23  127%
c i  212.1   38071   221885    144339   42483   6179 142042   26    70   54  37%     59  -21   28   24  119%
c i  216.1   38070   221885    149738   47497   6218 142086   26    66   57  39%     51  -22   21   24   89%
c i  217.1   38068   221885    150991   48687   6230 142093   27    67   60  40%     10  -21   32   24  132%
c i  217.9   38067   221885    152149   49791   6243 142105   25    63   61  40%     -2  -25   17   24   72%
c i  218.3   38063   221885    152790   50403   6248 142108   24    59   61  41%     -7  -29   13   24   56%
c i  218.4   38014   221885    152832   50444   6248 142108   24    59   61  41%     -8  -29   15   24   65%
c i  219.5   38013   221885    154656   52203   6251 142115   20    45   64  44%     -1  -41   13   23   54%
c i  222.5   38012   221885    159018   56360   6298 142157   20    55   69  36%     34  -29   24   23  106%
c i  223.7   38010   221885    160198   57490   6312 142162   23    63   70  36%      5  -20   25   23  108%
c i  224.0   38009   221885    160662   57947   6312 142162   23    61   70  37%     -2  -22   22   23   93%
c i  225.2   38008   221885    162259   59470   6324 142176   22    60   70  37%     -3  -22   20   23   88%
c i  226.1   38007   221885    163317   60491   6335 142186   20    51   73  39%     -7  -31   10   23   44%
c i  228.5   38006   221885    166019   63035   6353 142202   24    57   73  42%      9  -24   18   23   77%
c i  229.7   37989   221885    167675   64576   6365 142215   22    51   76  44%     -0  -30   23   23   99%
c -  230.1   37988   221885    168107   33840   6369 142216   22    51   40  43%     -5  -29   19   23   83%
c i  230.4   37987   221885    168576   34281   6369 142218   22    52   46  41%     -6  -28   22   23   96%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  233.4   37986   221885    173550   39066   6404 142244   20    41   50  49%     42  -37   29   23  127%
c i  235.1   37984   221885    176707   42043   6437 142289   17    42   50  40%     17  -34   14   22   64%
c i  235.6   37981   221885    177432   42736   6440 142292   18    46   50  39%      1  -30   26   22  116%
c i  236.3   37980   221885    178069   43347   6445 142300   20    51   53  39%     -6  -25   27   23  118%
c i  236.4   37974   221885    178151   43426   6446 142301   20    51   53  39%     -7  -24   25   23  112%
c i  237.3   37971   221885    179786   44991   6468 142329   19    51   60  38%     -5  -24   22   22   99%
c i  238.4   37970   221885    180961   46125   6477 142332   22    55   60  40%     -7  -20   25   23  112%
c 
c [simplification-20] limit 161929 conflicts (hard 181117) hit after 181117 conflicts
c [quatres-16] found 24547 quaternary clauses 56% in total
c [quatres-16-1] removed 6 duplicate quaternary clauses
c [quatres-16-2] added 9 single-self-subsuming ternary resolvents
c [quatres-16-2] added 19 quaternary resolvents
c [ternres-15] limit 39639376 with penalty 0 = 0 + 0
c [ternres-15] all 37970 free variables schedulable
c [ternres-15] 576 ternary resolvents (0 bin, 576 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-52] removed 153 variables
c [basicprobe-6] limit 198196880 penalty 0 = 0 + 0
c [basicprobe-6-0] 8228 sched 23%, 1020 failed, 128 lifted, 126766 hbrs
c [decomp-53] removed 2556 variables
c [basicprobe-6-1] 7034 probes remain 20% after last round
c [basicprobe-6-1] 1289 units = 1161 failed (90%) + 128 lifted (10%)
c [basicprobe-6-1] removed 2817 variables, found 149315 hbrs
c [bate-4] eliminated 940 asymmetric tautologies during probing
c [unhide-20] limit 7927875 with penalty 0 = 0 + 0
c [unhide-20-33] 9 units, 160 failed, 42853 tauts, 0 hbrs, 708833 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 326 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 34951 variables 100%
c [block-6] limit of 24774610 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 75 blocked clauses
c [block-6] 75 < 1/100 * 195657 = 1956 considered unsuccessful
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 34951 variables 100%
c [elim-19] limit of 792787520 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 1609 variables 5% in round 1 in 14886231 steps
c [elim-19-1] backward subsumption/strengthening limit 14886200
c [elim-19-1-1] backward checking 6884 touched variables 20%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 71 and strengthened 48 clauses in 1341263 steps
c [elim-19-1] rescheduled 344 variables 1% by backward subsumption
c [elim-19-2] eliminated 20 variables 0% in round 2 in 182593 steps
c [elim-19-2] backward subsumption/strengthening limit 182500
c [elim-19-2-1] backward checking 301 touched variables 1%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 21 and strengthened 17 clauses in 140897 steps
c [elim-19-2] rescheduled 84 variables 0% by backward subsumption
c [elim-19-3] eliminated 4 variables 0% in round 3 in 83973 steps
c [elim-19-3] backward subsumption/strengthening limit 83900
c [elim-19-3-1] backward checking 51 touched variables 0%
c [elim-19-3-1] fully completed backward checking in 1 rounds
c [elim-19-3] subsumed 1 and strengthened 4 clauses in 66091 steps
c [elim-19] incomplete 20 not tried 0% in round 3
c [elim-19] transition to [ all 1 rem 1 ] state
c [elim-19] eliminated 1633 = 5% variables out of 34951 scheduled
c [bca-16] limit of 10000000 steps and 385942 added (scaled 2)
c [bca-16] 44636 out of 66638 literals actually usable 67%
c [bca-16] added 14 blocked clauses in 137980 steps
c [sweep-15] limit 11891812 penalty 0 = 0 + 0
c [sweep-15-1] 1950 pos 11.1% + 15607 neg 88.9% = 17557 sched 52.7% ret 15761
c [sweep-15-1] 11969947 steps 277 queries 370.26 avg class size
c [sweep-15-1] 2749 decisions 241 SAT calls 77.21 avg env size
c [sweep-15-1] 15525 variables remain 47% (17775 retained 53%)
c [decomp-54] removed 151 variables
c [sweep-15-1] removed 151 vars (0 failed, 39 eqs, 68 impls)
c [sweep-15] removed 151 vars in TOTAL (1 rounds, 276 queries)
c [sort-queue-20] sorted 33167 enqueued variables after 181117 conflicts
c [score-dist-20] active 0 (0%), one 25713 (78%), zero 7454 (22%)
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 4803 variables 12.6% (33167 remain 10%)
c [simplification-20] removed 29831 irredundant clauses 13.4% (192054 remain 14%)
c [simplification-20] maximum reduction of 13% = max (13%, 13%)
c [simplification-20] large reduction 13% >= 5% limit
c [simplification-20] next conflict interval 2000 = 2000/1
c [simplification-20] penalized conflict interval 2000 = 1 * 2000
c [simplification-20] hard conflict limit 193117 (soft 183117 + delta 10000)
c [simplification-20] new conflict limit 183117 (hard 193117)
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  252.6   33166   192054    183451   41514   5720 216485   24    60   50  40%      6  -14   27   23  119%
c i  257.0   33162   192054    190972   48541   5770 216543   19    41   51  46%     79  -30   13   22   59%
c 
c [simplification-21] limit 183117 conflicts (hard 193117) hit after 193119 conflicts
c [quatres-17] found 21611 quaternary clauses 53% in total
c [quatres-17-1] removed 2 duplicate quaternary clauses
c [quatres-17-2] added 2 single-self-subsuming ternary resolvents
c [quatres-17-2] added 11 quaternary resolvents
c [ternres-16] limit 41541804 with penalty 0 = 0 + 0
c [ternres-16] all 33161 free variables schedulable
c [ternres-16] 838 ternary resolvents (2 bin, 836 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 1298181 penalty 4 = 4 + 0
c [card-6] found 2692 at-most-one constraints of average size 3.9
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1298181 for elimination
c [card-6] 2692 out of 2692 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-55] removed 12 variables
c [simpleprobe-7] all 33155 free variables schedulable
c [simpleprobe-7] limit 166167218 penalty 0 = 0 + 0
c [decomp-56] removed 329 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 329 variables, found 47497 hbrs, 91 units
c [unhide-21] limit 8308360 with penalty 0 = 0 + 0
c [unhide-21-38] 3 units, 115 failed, 46557 tauts, 0 hbrs, 398587 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 372 transitive binary clauses
c [elim-20] no untried remaining variables left
c [elim-20] scheduled 32736 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 513 variables 2% in round 1 in 14186603 steps
c [elim-20-1] backward subsumption/strengthening limit 14186600
c [elim-20-1-1] backward checking 2932 touched variables 9%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 20 and strengthened 15 clauses in 656476 steps
c [elim-20-1] rescheduled 94 variables 0% by backward subsumption
c [elim-20-2] eliminated 6 variables 0% in round 2 in 82837 steps
c [elim-20-2] backward subsumption/strengthening limit 82800
c [elim-20-2-1] backward checking 54 touched variables 0%
c [elim-20-2-1] incomplete backward checking 0 remain 0%
c [elim-20-2] subsumed 4 and strengthened 10 clauses in 82801 steps
c [elim-20-2] rescheduled 33 variables 0% by backward subsumption
c [elim-20-3] eliminated 1 variables 0% in round 3 in 68008 steps
c [elim-20-3] backward subsumption/strengthening limit 68000
c [elim-20-3-1] backward checking 16 touched variables 0%
c [elim-20-3-1] fully completed backward checking in 1 rounds
c [elim-20-3] subsumed 0 and strengthened 2 clauses in 48023 steps
c [elim-20] incomplete 8 not tried 0% in round 3
c [elim-20] transition to [ all 1 rem 1 ] state
c [elim-20] eliminated 520 = 2% variables out of 32736 scheduled
c [bca-17] limit of 10000000 steps and 372465 added (scaled 2)
c [bca-17] 42195 out of 64434 literals actually usable 65%
c [bca-17] added 14 blocked clauses in 140191 steps
c [sweep-16] limit 12462541 penalty 0 = 0 + 0
c [sweep-16-1] 1912 pos 12.6% + 13250 neg 87.4% = 15162 sched 47.1% ret 17054
c [sweep-16-1] 12893336 steps 206 queries 466.94 avg class size
c [sweep-16-1] 3014 decisions 183 SAT calls 92.28 avg env size
c [sweep-16-1] 13975 variables remain 43% (18236 retained 57%)
c [decomp-57] removed 101 variables
c [sweep-16-1] removed 101 vars (0 failed, 27 eqs, 37 impls)
c [sweep-16] removed 101 vars in TOTAL (1 rounds, 205 queries)
c [sort-queue-21] sorted 32115 enqueued variables after 193119 conflicts
c [score-dist-21] active 0 (0%), one 25505 (79%), zero 6610 (21%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 1046 variables 3.2% (32115 remain 10%)
c [simplification-21] removed 6508 irredundant clauses 3.4% (185546 remain 13%)
c [simplification-21] maximum reduction of 3% = max (3%, 3%)
c [simplification-21] geometric conflict interval increment 9599 = 38396 / 4
c [simplification-21] new conflict interval 47995
c [simplification-21] penalized conflict interval 47995 = 1 * 47995
c [simplification-21] hard conflict limit 265111 (soft 241114 + delta 23997)
c [simplification-21] new conflict limit 241114 (hard 265111)
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  271.8   32114   185546    203314   56350   6096 215349   19    45   54  42%    142  -21   17   21   80%
c i  273.9   32113   185546    207818   60575   6154 215389   18    48   55  38%     20  -17   17   21   79%
c i  274.1   32108   185546    208073   60825   6154 215389   18    47   55  38%      8  -18   15   21   71%
c i  275.2   32097   185546    209898   62548   6162 215394   18    44   61  41%    -14  -20   18   21   86%
c -  277.6   32096   185546    214211   36762   6199 215411   17    37   39  46%     16  -25   16   21   77%
c -  299.1   32096   185546    249088   38539   6381 215559   16    33   40  49%    432  -19   13   19   70%
c i  299.3   32095   185546    249471   38906   6387 215562   17    34   45  49%    435  -18   18   19   92%
c 
c [simplification-22] limit 241114 conflicts (hard 265111) hit after 260782 conflicts
c [quatres-18] found 21526 quaternary clauses 50% in total
c [quatres-18-2] added 10 single-self-subsuming ternary resolvents
c [quatres-18-2] added 8 quaternary resolvents
c [ternres-17] limit 52594021 with penalty 0 = 0 + 0
c [ternres-17] all 32095 free variables schedulable
c [ternres-17] 419 ternary resolvents (1 bin, 418 trn)
c [ternres-17] fully completed ternary resolution
c [gauss-11] limit 1314850 penalty 3 = 3 + 0
c [gauss-11] extracted 52 xors of average arity 3.0
c [gauss-11] connected 154 occurrences of 102 variables (average 1.5)
c [gauss-11] limit 1314850 penalty 3 = 3 + 0
c [gauss-11] fully completed
c [gauss-11] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-58] removed 1 variables
c [unhide-22] limit 10518804 with penalty 0 = 0 + 0
c [unhide-22-44] 5 units, 62 failed, 22807 tauts, 0 hbrs, 326558 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 303 transitive binary clauses
c [elim-21] no untried remaining variables left
c [elim-21] scheduled 31973 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 237 variables 1% in round 1 in 13956928 steps
c [elim-21-1] backward subsumption/strengthening limit 13956900
c [elim-21-1-1] backward checking 1345 touched variables 4%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 5 and strengthened 8 clauses in 339361 steps
c [elim-21-1] rescheduled 47 variables 0% by backward subsumption
c [elim-21-2] eliminated 2 variables 0% in round 2 in 111883 steps
c [elim-21-2] backward subsumption/strengthening limit 111800
c [elim-21-2-1] backward checking 21 touched variables 0%
c [elim-21-2-1] fully completed backward checking in 1 rounds
c [elim-21-2] subsumed 2 and strengthened 0 clauses in 42558 steps
c [elim-21-2] rescheduled 6 variables 0% by backward subsumption
c [elim-21-3] eliminated 1 variables 0% in round 3 in 21671 steps
c [elim-21-3] backward subsumption/strengthening limit 21600
c [elim-21-3-1] backward checking 11 touched variables 0%
c [elim-21-3-1] incomplete backward checking 0 remain 0%
c [elim-21-3] subsumed 0 and strengthened 0 clauses in 21601 steps
c [elim-21] fully completed in 3 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 240 = 1% variables out of 31973 scheduled
c [elim-21] 240 < 1/100 * 31973 = 319 considered unsuccessful
c [bca-18] limit of 10000000 steps and 366282 added (scaled 2)
c [bca-18] 41014 out of 63468 literals actually usable 65%
c [bca-18] added 15 blocked clauses in 137623 steps
c [sweep-17] limit 15778206 penalty 0 = 0 + 0
c [sweep-17-1] 1645 pos 11.9% + 12156 neg 88.1% = 13801 sched 43.5% ret 17932
c [sweep-17-1] 15781874 steps 417 queries 248.30 avg class size
c [sweep-17-1] 4102 decisions 364 SAT calls 74.93 avg env size
c [sweep-17-1] 11382 variables remain 36% (20313 retained 64%)
c [decomp-59] removed 181 variables
c [sweep-17-1] removed 181 vars (0 failed, 57 eqs, 78 impls)
c [sweep-17] removed 181 vars in TOTAL (1 rounds, 416 queries)
c [sort-queue-22] sorted 31552 enqueued variables after 260782 conflicts
c [score-dist-22] active 0 (0%), one 25476 (81%), zero 6076 (19%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 543 variables 1.7% (31552 remain 10%)
c [simplification-22] removed 3431 irredundant clauses 1.8% (182115 remain 13%)
c [simplification-22] maximum reduction of 2% = max (2%, 2%)
c [simplification-22] geometric conflict interval increment 15998 = 47995 / 3
c [simplification-22] new conflict interval 63993
c [simplification-22] penalized conflict interval 63993 = 1 * 63993
c [simplification-22] hard conflict limit 356771 (soft 324775 + delta 31996)
c [simplification-22] new conflict limit 324775 (hard 356771)
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  324.6   31551   182115    278656   63587   6423 195296   17    30   55  56%    244  -18   12   19   64%
c i  324.6   31550   182115    278710   63640   6423 195296   17    30   55  56%    222  -18   11   19   57%
c i  329.7   31549   182115    285503   69999   6458 195319   16    35   60  48%    -96  -12    9   19   49%
c i  329.7   31548   182115    285504   69999   6458 195319   16    35   60  48%    -96  -12    9   19   49%
c -  330.8   31541   182115    286959   39256   6468 195325   17    35   39  49%   -151  -12   14   19   75%
c i  336.7   31540   182115    297742   49395   6539 195358   17    40   50  43%      5   -6   14   19   73%
c i  336.8   31539   182115    297862   49513   6540 195358   17    39   50  43%    -14   -7   11   19   58%
c i  340.6   31535   182115    303564   54923   6563 195372   19    42   53  45%    -87   -4   22   19  118%
c i  342.2   31533   182115    306411   57551   6572 195374   16    34   53  47%   -122  -12    9   19   48%
c -  354.8   31532   182115    323967   41269   6634 195419   18    36   39  50%    109   -7   20   18  109%
c 1  367.7   31532   182115    343771   59713   6702 195475   15    35   50  43%    347   -5    8   18   48%
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 SATISFIABLE
c
c bate: 1573 basic ate = 1418 trn 90% + 155 lrg 10% in 4 updates
c bcas: 18 count, 1071 added (660 skipped), 4651016 steps
c bkwd: tried 835839 clauses, 1669390 lits, 2.00 lits/clause
c bkwd: checked 18389817 occs, 22.00 occs/clause, 11.02 occs/lit
c bkwd: subsumed 123 binary, 1208 ternary, 321 large
c bkwd: strengthened 17 binary, 0 ternary (0% self), 1619 large (0% self)
c blkd: 6 bces, 9285 removed, 7773377 resolutions, 21519673 steps
c blkd: 10108 blocking literals 2%, 60 pure
c bump: 344612 bumped seen, 103905657 lits 301.5 on average
c card: 6 count, 0 units, 0 am1, 31058739 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 65505 subsumed
c card: 18144 at-most-one constraints found, average size 4.56
c card: 18144 at-most-one constraints used 100%, average size 4.56
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 6 cces, 14926 eliminated, 14896 ate 100%, 30 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4750381 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 190 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 59 decompositions, 15793 equivalent 5%
c deco: 4217 decision-only clauses 1%, 60% reduction
c decs: 2966178 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 21 elims, 152093 eliminated 46%, 41 pure 0%
c elms: 69 rounds, 3.3 rounds/bve
c elms: 139125 small 91%, 12867 large 8%
c elms: 586876 tried small, 139127 succeeded 24%, 447749 failed 76%
c elms: 52875 subsumed, 70782 strengthened, 666 blocked
c elms: 25951015 copies, 23373931 resolutions, 25692808 ipos
c elms: 3562910 subchks, 2516904 strchks
c gaus: 11 extractions, 3752 extracted, 2.2 size, 3 max
c gaus: exported 5 units, 33 binary and 0 ternary equations
c gaus: 0 gc, 37205088 steps, 18602544 extr 50%, 272475 elim 1%
c glue: 21.3 orig avg, 21.3 real avg, 3.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 584096 = 170286 simple 29% + 405497 trn 69% + 8313 lrg 1%, 4586 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 344612 clauses, 116.3 length
c lrnd: 40080806 lits = 69954204 orig - 29873398 removed 43%
c lrnd: 145759 uips 42%, 169379 flips 49%
c mins: 328601 mins 96%, 3872 bin 1%, 7187 size 2%
c mins: 164307699 poisoned searches, 27813882 hits, 17% hit rate
c mins: 202470378 used twice searches, 4026248 hits, 2% hit rate
c move: moved 20386, 9268 bin 45%, 11118 trn 55%
c otfs: 732 driving 24%, 2287 restarting 76%
c otfs: str 3019, 2847 red 94%, 172 irr 6%
c otfs: str 3019, 0 bin 0%, 189 trn 6%, 2830 lrg 94%
c otfs: sub 10, 10 red 100%, 0 irr 0%
c otfs: sub 10, 0 bin 0%, 1 trn 10%, 9 lrg 90%
c phas: 19 computed, 204939 set, 2 pos (0%), 204937 neg (100%)
c prbs: 6 basic, 32184 probed, 2487 failed, 217 lifted
c prbs: 7 simple, 1184238 probed, 1371 failed, 4582 eqs
c prbs: 6 treelook, 60 probed, 4 failed, 0 lifted
c prom: 61151 locked 8% out of 777727 tried
c prps: 971318369 props, 312 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 18 count, 394 quat, 146 self1, 2 self2, 2081 dup
c queu: 22 sorted, 2966178 next (9 steps 0.00)
c queu: 105749030 enq (0 steps 0.00), 103905657 deq 98%
c redc: 9960 clauses 27%, 36775 tried 11%, 269 sat 1%
c redc: 21623 lits 5%, 418791 tried 1%, 269 sat 0%
c redc: 1218 times jump level reduced, 17.8 levels on average
c reds: 6 count, 57295.2 conflicts per reduce
c reds: 0 memlim 0%, 6 arith 100%
c reds: 157532 collected 82%, 34933 retired 18%
c rmbd: 57043 removed, 13034 red 23%
c rsts: 10722 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 22 count, 19 confs 86%, 0 vars 0%
c simp: 2 its 9%, 1 bin 5%, 0 trns 0%
c subl: 344612 count (316086 tried 0.9), 13975 sub out of 332988 (4.2%)
c swps: 17 count, 17 rounds, 2516 queries (148.0/round)
c swps: 2120 sat calls, 80 unsat (0.7% success rate)
c swps: 25652 decisions 12.1, 1573 conflicts 0.7
c swps; 1616.0 avg class size, 75.0 avg environment size
c swps: 0 failed, 612 impls, 458 equivs
c swp0: 832 type 0 queries, 352 unsat (42.3%), 747 sat (89.8%)
c swp1: 1684 type 1 queries, 1237 unsat (73.5%), 1311 sat (77.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 6622634 calls to obtain time
c tops: 131778 fixed 40%, 619 its, 555.37 confs/it
c trds: 18 transitive reductions, 3672 removed, 26 failed
c trds: 28163 nodes, 65625 edges, 33983880 steps
c trim: 555850 words, 2.1 MB
c trnr: 17 count, 50 bin, 17499 trn, 82105584 steps
c unhd: 22 count, 44 rounds, 102065086 steps
c unhd: 5763 non-trivial sccs of average size 2.4
c unhd: 278 units, 275 bin, 3 trn, 0 lrg
c unhd: 9520 failed, 9424 stamp, 0 lits, 50 bin, 28 trn, 0 lrg
c unhd: 291807 tauts, 6055 bin 2%, 23550 trn 8%, 1768 lrg 1%
c unhd: 291807 tauts, 260434 stamp 89%, 221524 red 76%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2207900 str, 275 bin 0%, 13139 trn 1%, 2194486 lrg 99%, 2143889 red 97%
c vars: 31532 remaining 10% and 299664 removed 90% out of 331196
c vars: 131778 fixed 40%, 152093 eliminated 46%, 15793 equivalent 5%
c vsts: 7088623794 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 7.3 search visits per propagation, 19545.3 per conflict
c wchs: 1081675150 pushed, 60248416 enlarged, 271 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         333382        157532         34933      21056560       2905775        140049
c 
c  0 0         35568  11      3016   2         0   0  13770790  65   1447463  50     46818  33     1.9
c  1 5         14715   4      3767   2      1699   5   1675662   8<   270830   9     13789  10     1.1
c  2 6         50764  15     22867  15      5028  14   2222636  11    432571  15<    26561  19<    4.1
c  3 9         76974  23     44555  28      7187  21   1269919   6    274475   9     18084  13     6.1
c  4 14        55664  17<    34065  22<     5943  17    786238   4    172724   6     11086   8     5.2
c  5 21        34584  10     19501  12      4519  13<   686825   3    136004   5      9102   6     4.0
c  6 30        24047   7     13144   8      3438  10    296228   1     71894   2      5352   4     3.4
c  7 41        14999   4      7634   5      2385   7    118867   1     37313   1      3367   2     2.8
c  8 54         9351   3      4175   3      1641   5    135096   1     31906   1      2467   2     1.7
c  9 69         5842   2      2410   2      1107   3     44380   0     13107   0      1412   1     1.2
c 10 86         5157   2      1666   1       920   3     35571   0     11168   0      1211   1     1.1
c 11 126        4296   1       585   0       827   2     12044   0      5129   0       641   0     1.0
c 12 230        1393   0       147   0       239   1      2271   0      1174   0       158   0     0.5
c 13 534          28   0         0   0         0   0        33   0        17   0         1   0     0.0
c 
c avg                  3.7           4.0           4.6           1.0           1.6           2.3
c std                  2.5           1.9           2.5           1.8           2.1           2.4
c 
c   32.033   9% elim
c   23.117   6% unhide
c   19.114   5% probe
c   10.264   3% sweep
c    9.203   3% bump
c    6.653   2% cce
c    4.091   1% gauss
c    2.595   1% bca
c    2.231   1% block
c    1.953   1% transred
c 
c    3.950 < 1% rest (below)
c 
c    1.922   1% decide
c    0.871   0% quatres
c    0.768   0% ternres
c    0.389   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    6.587   2% preprocessing     6%
c  106.887  29% inprocessing     94%
c ==================================
c  113.473  31% simplifying
c  254.229  69% search
c ==================================
c  367.730 100% all
c 
c        343771 conflicts,         934.8 confs/sec
c          5464 ternaries,          62.9 confs/ternary
c          5052 binaries,           68.0 confs/binary
c           619 iterations,        555.4 confs/iteration
c 
c             6 reductions,          0.0 redus/sec,  57295.2 confs/reduction
c         10722 restarts,           29.2 rests/sec,     32.1 confs/restart
c       2966178 decisions,        8066.2 decis/sec,      8.6 decis/conflict
c     971318369 propagations,  2641390.5 props/sec,    327.5 props/decision
c 
c 367.7 seconds, 128.2 MB
c launch: done
