c launch: /data/cnf/sc2014/app/ACG-20-5p0.cnf.bz2
c host: atom32
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-5p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ACG-20-5p0.cnf.bz2
c no embedded options
c found 'p cnf 324716 1390931' header
c read 324716 variables, 1390931 clauses, 3269132 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 313313 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  313313  1378778         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 5663 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 5663 out of 5663 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51680 variables
c [simpleprobe-1] all 273036 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 559 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 559 variables, found 13627 hbrs, 20 units
c [unhide-1] limit 69539 based on 1112627 irredundant clauses
c [unhide-1-1] 14 units, 2542 failed, 15781 tauts, 0 hbrs, 8850 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 260513 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 101124 not tried 39% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 110343 = 42% variables out of 260513 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 886609 negative 99.4% of 892372 except 5763 0.6%
c [phase-count-1] 738027 positive 82.7% of 892372 except 154345 17.3%
c [phase-count-1] less non-negative clauses 5763 than limit 89200 (10.0%)
c [phase-count-1] non-pos/non-neg = 154345/5763 = 26.78 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 150170 negative 100%
c [sort-queue-1] sorted 150170 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 150170 (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 127703 variables 46.0% (150170 remain 48%)
c [simplification-1] removed 486406 irredundant clauses 35.3% (892372 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.5  150169   892372        50      45      3  6182    0     1   62   5%      0    1    1    0 23511%
c i    6.5  148717   892372        86      74      8  6183    0     2   62   9%      0    2    2    0 22720%
c i    6.6  147695   892372       123     101     12  6187    0     2   62  11%      0    2    3    0 21211%
c i    6.7  147665   892372       194     156     17  6196    0     3   62  11%      0    3    4    0 18651%
c i    6.8  146554   892372       331     273     23  6203    1     5   62  18%      0    5   10    0 16331%
c i    6.8  145823   892372       342     279     24  6205    1     6   62  16%      0    6    9    0 15789%
c i    6.8  145806   892372       349     283     25  6206    1     6   62  16%      0    6    9    0 15399%
c i    6.9  145788   892372       356     286     25  6209    1     6   62  16%      0    6    9    0 15044%
c i    6.9  144998   892372       378     294     27  6215    1     6   62  16%      0    6    9    0 13969%
c i    6.9  144747   892372       396     306     30  6217    1     6   62  15%      0    6    8    0 13219%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 6209 variables
c [simpleprobe-2] all 143961 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 363 variables
c [simpleprobe-2] 115780 variables remain 81% (27818 retained 19%)
c [simpleprobe-2] removed 363 variables, found 1857 hbrs, 42 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 100833 literals 35%
c [treelook-1] scheduling used 517459 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 407386 steps
c [treelook-1] 100827 literals remain 35%
c [treelook-1] 98747 variables remain to probed next time 69%
c [treelook-1] removed 1 variables, found 2930 hbrs
c [basicprobe-1] limit 6815056 based on 851882 irredundant clauses
c [basicprobe-1-0] 30503 probes remain 25% after last round
c [basicprobe-1-0] 52 units = 52 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 22524 variables, found 15520 hbrs
c [unhide-2] limit 53242 based on 851882 irredundant clauses
c [unhide-2-2] 10 units, 2052 failed, 2110 tauts, 0 hbrs, 19796 literals
c [elim-2] 80029 variables 69% will be scheduled this time
c [elim-2] scheduled 80029 variables 69%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 17870 not tried 15% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 4632 = 6% variables out of 80029 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 636442 negative 99.1% of 642251 except 5809 0.9%
c [phase-count-2] 521709 positive 81.2% of 642251 except 120542 18.8%
c [phase-count-2] less non-negative clauses 5809 than limit 64200 (10.0%)
c [phase-count-2] non-pos/non-neg = 120542/5809 = 20.75 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 16129 negative 100%
c [sort-queue-2] sorted 111200 enqueued variables after 396 conflicts
c [score-dist-2] active 0 (0%), one 6623 (6%), zero 104577 (94%)
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 33439 variables 23.1% (111200 remain 35%)
c [simplification-2] removed 250121 irredundant clauses 28.0% (642251 remain 47%)
c [simplification-2] maximum reduction of 28% = max (23%, 28%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1002 (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   11.8  111199   642251       456     280     32 14678    1     8   48  14%      0    7    8    0 11403%
c i   11.8  111054   642251       462     282     34 14679    1     8   48  13%      0    8    8    0 11197%
c i   11.8  111006   642251       481     293     37 14683    1     8   48  13%      0    8    7    0 10617%
c i   11.8  110423   642251       488     297     38 14684    1     8   48  13%      0    8    7    0 10392%
c i   11.8  110412   642251       521     316     43 14688    1     8   48  13%      0    8    7    0 9599%
c i   11.8  110374   642251       522     316     43 14688    1     8   48  13%      0    8    7    0 9562%
c i   11.9  110333   642251       546     335     46 14689    1     8   48  13%      0    8    7    0 9029%
c i   11.9  110326   642251       567     349     47 14694    1     8   48  13%      0    8    6    0 8516%
c i   11.9  110314   642251       578     353     48 14698    1     8   48  13%      0    8    6    0 8223%
c i   11.9  110306   642251       579     353     48 14698    1     8   48  13%      0    8    6    0 8191%
c i   11.9  109188   642251       648     402     56 14709    1    10   48  12%      0    9    6    0 7169%
c i   12.1  109187   642251       869     567     74 14738    1    13   48  11%      1   13    6    0 6215%
c 
c [simplification-3] limit 1024 conflicts (hard 11000) hit after 1024 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 5059 at-most-one constraints of average size 4.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5059 out of 5059 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 3277 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 64967 literals 30%
c [treelook-2] scheduling used 300547 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 322996 steps
c [treelook-2] 64957 literals remain 30%
c [treelook-2] 46709 variables remain to probed next time 43%
c [decomp-7] removed 2 variables
c [treelook-2] removed 3 variables, found 2665 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 9 units, 743 failed, 13516 tauts, 0 hbrs, 11976 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 106108 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 23728 not tried 22% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 4486 = 4% variables out of 106108 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 584510 negative 99.0% of 590227 except 5717 1.0%
c [phase-count-3] 477405 positive 80.9% of 590227 except 112822 19.1%
c [phase-count-3] less non-negative clauses 5717 than limit 59000 (10.0%)
c [phase-count-3] non-pos/non-neg = 112822/5717 = 19.73 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 13388 negative 100%
c [sort-queue-3] sorted 101622 enqueued variables after 1024 conflicts
c [score-dist-3] active 0 (0%), one 11437 (11%), zero 90185 (89%)
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 7515 variables 6.9% (101622 remain 32%)
c [simplification-3] removed 52024 irredundant clauses 8.1% (590227 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 13024 (soft 3024 + delta 10000)
c [simplification-3] new conflict limit 3024 (hard 13024)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.9  101621   590227      1036     597     74 13772    2    16   46  11%      1   16    7    0 5959%
c i   15.9  101442   590227      1037     597     74 13772    2    16   46  11%      1   16    7    0 5936%
c i   15.9  101438   590227      1100     644     83 13776    2    17   46  10%      1   17    7    0 5476%
c i   16.0  101430   590227      1198     723     93 13783    2    19   46  11%      1   19    9    0 6003%
c i   16.2  101304   590227      1511     983    111 13811    3    23   46  11%      1   23   10    0 5136%
c i   16.2  101297   590227      1514     985    111 13811    3    23   46  11%      1   23   10    0 5083%
c i   16.3  101292   590227      1614    1067    118 13819    3    26   46  11%      1   26   13    0 5980%
c i   16.3  101283   590227      1633    1079    121 13821    3    26   46  11%      1   26   12    0 5647%
c i   16.3  101202   590227      1641    1083    122 13823    3    26   46  11%      1   26   12    0 5494%
c i   16.3  101199   590227      1683    1115    123 13830    3    27   46  11%      1   26   11    0 4866%
c i   16.5  101195   590227      1886    1287    134 13841    4    30   46  14%      1   30   20    0 6551%
c i   16.5  101192   590227      1956    1348    139 13843    4    32   46  14%      1   31   18    0 5695%
c i   16.5  101184   590227      2009    1379    150 13851    4    32   46  14%      1   31   15    0 4776%
c i   16.6  101155   590227      2040    1400    153 13857    4    32   46  14%      1   31   14    0 4401%
c 
c [simplification-4] limit of 221 binary hit after 221 binaries
c [decomp-8] removed 602 variables
c [basicprobe-2] limit 4692992 based on 586624 irredundant clauses
c [basicprobe-2-0] 27136 probes remain 28% after last round
c [basicprobe-2-0] 39 units = 39 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2776 variables, found 10376 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 12 units, 810 failed, 2722 tauts, 0 hbrs, 7800 literals
c [elim-4] 16634 variables 17% will be scheduled this time
c [elim-4] scheduled 16634 variables 17%
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 16 variables 0% in round 1 in 23513499 steps
c [elim-4-1] backward subsumption/strengthening limit 23513400
c [elim-4-1-1] backward checking 9851 touched variables 10%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 271 and strengthened 48 clauses in 1458464 steps
c [elim-4-1] rescheduled 871 variables 1% by backward subsumption
c [elim-4-2] eliminated 101 variables 0% in round 2 in 502058 steps
c [elim-4-2] backward subsumption/strengthening limit 502000
c [elim-4-2-1] backward checking 753 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 70 and strengthened 74 clauses in 326203 steps
c [elim-4-2] rescheduled 339 variables 0% by backward subsumption
c [elim-4-3] eliminated 14 variables 0% in round 3 in 294165 steps
c [elim-4-3] backward subsumption/strengthening limit 294100
c [elim-4-3-1] backward checking 93 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 9 and strengthened 0 clauses in 139066 steps
c [elim-4] incomplete 10 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 131 = 1% variables out of 16634 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 543091 negative 99.0% of 548812 except 5721 1.0%
c [phase-count-4] 440880 positive 80.3% of 548812 except 107932 19.7%
c [phase-count-4] less non-negative clauses 5721 than limit 54800 (10.0%)
c [phase-count-4] non-pos/non-neg = 107932/5721 = 18.87 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 12258 negative 100%
c [sort-queue-4] sorted 96449 enqueued variables after 2216 conflicts
c [score-dist-4] active 0 (0%), one 15715 (16%), zero 80734 (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 4705 variables 4.7% (96449 remain 31%)
c [simplification-4] removed 41415 irredundant clauses 7.0% (548812 remain 40%)
c [simplification-4] maximum reduction of 7% = max (5%, 7%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3038 (hard 13024)
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   18.6   96448   548812      2345    1613    176 18878    6    38   44  15%      1   37   18    0 4220%
c i   18.7   96446   548812      2494    1731    189 18891    6    40   44  15%      1   39   16    0 3410%
c i   18.8   96432   548812      2570    1793    192 18900    6    42   44  15%      1   41   18    0 3774%
c i   18.8   96427   548812      2611    1827    194 18903    6    42   44  15%      1   41   19    0 3728%
c i   18.9   96421   548812      2703    1906    201 18906    6    43   44  15%      1   42   16    1 3082%
c i   18.9   96413   548812      2813    1981    212 18922    7    45   44  15%      1   44   17    1 3099%
c i   19.0   96408   548812      2871    2025    217 18929    7    46   44  15%      1   45   15    1 2775%
c i   19.0   96358   548812      2874    2026    217 18930    7    46   44  15%      1   45   15    1 2745%
c i   19.0   96322   548812      2930    2076    221 18930    7    47   44  15%      1   46   14    1 2579%
c 
c [simplification-5] limit 3041 conflicts (hard 13024) hit after 3041 conflicts
c [quatres-1] found 42945 quaternary clauses 49% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 11 single-self-subsuming ternary resolvents
c [quatres-1-2] added 10 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 96320 free variables schedulable
c [ternres-1] 2019 ternary resolvents (7 bin, 2012 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 951 xors of average arity 2.1
c [gauss-1] connected 1995 occurrences of 950 variables (average 2.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 995 variables
c [simpleprobe-3] 76693 schedulable variables 80%
c [simpleprobe-3] limit 2605470 penalty 0 = 0 + 0
c [decomp-10] removed 1133 variables
c [simpleprobe-3] 56876 variables remain 60% (37316 retained 40%)
c [simpleprobe-3] removed 1133 variables, found 7155 hbrs, 74 units
c [unhide-5] limit 130273 with penalty 0 = 0 + 0
c [unhide-5-5] 21 units, 458 failed, 8780 tauts, 0 hbrs, 3134 literals
c [transred-1] limit 651367 with penalty 0 = 0 + 0
c [transred-1] removed 50 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 93064 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 6820 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 14 clauses out of 161 (9%) of length 10
c [cce-1-1] eliminated 45 clauses out of 621 (7%) of length 9
c [cce-1-1] eliminated 45 clauses out of 517 (9%) of length 8
c [cce-1-1] eliminated 147 clauses out of 896 (16%) of length 7
c [cce-1-1] eliminated 2971 clauses out of 4519 (66%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3222 large clauses in 30000001 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 375415 clauses = 266353 binary + 109062 ternary
c [cce-1-1] tried to eliminate 402 small clauses 0%
c [cce-1-1] eliminated 106 binary clauses 0%
c [cce-1-1] eliminated 54 ternary clauses 0%
c [cce-1-1] eliminated 160 small clauses 0%
c [cce-1-1] eliminated 160 small clauses in 30000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3382 covered clauses in round 1
c [cce-1] eliminated 3382 covered clauses in TOTAL during 1 rounds
c [cce-1] 3382 < 1/100 * 514596 = 5145 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 93064 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 13679 not tried 15% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2665 = 3% variables out of 93064 scheduled
c [bca-1] limit of 10000000 steps and 1013646 added (scaled 2)
c [bca-1] 172380 out of 180800 literals actually usable 95%
c [bca-1] added 181 blocked clauses in 500105 steps
c [sweep-1] limit 1013146 based on 506573 irredundant clauses
c [sweep-1-1] 3002 pos 3.3% + 87397 neg 96.7% = 90399 sched 100.0% ret 0
c [sweep-1-1] 1355035 steps 11 queries 28399.09 avg class size
c [sweep-1-1] 107 decisions 9 SAT calls 44.67 avg env size
c [sweep-1-1] 90381 variables remain 100% (11 retained 0%)
c [decomp-11] removed 32 variables
c [sweep-1-1] removed 32 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 32 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-5] 503741 negative 99.5% of 506444 except 2703 0.5%
c [phase-count-5] 410178 positive 81.0% of 506444 except 96266 19.0%
c [phase-count-5] less non-negative clauses 2703 than limit 50600 (10.0%)
c [phase-count-5] non-pos/non-neg = 96266/2703 = 35.61 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 11581 negative 100%
c [sort-queue-5] sorted 90367 enqueued variables after 3041 conflicts
c [score-dist-5] active 0 (0%), one 16385 (18%), zero 73982 (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 5953 variables 6.2% (90367 remain 29%)
c [simplification-5] removed 42368 irredundant clauses 7.7% (506444 remain 37%)
c [simplification-5] maximum reduction of 8% = max (6%, 8%)
c [simplification-5] large reduction 8% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 15041 (soft 5041 + delta 10000)
c [simplification-5] new conflict limit 5041 (hard 15041)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   24.7   90366   506444      3070    1837   1414 30897    7    49   43  15%      1   48   17    1 2875%
c i   25.0   90361   506444      3360    2062   1436 30924    8    53   43  16%      1   52   16    1 2342%
c i   25.0   90355   506444      3366    2065   1436 30926    8    53   43  16%      1   52   16    1 2298%
c i   25.0   90352   506444      3394    2086   1441 30927    8    53   43  15%      1   52   15    1 2108%
c i   25.1   90337   506444      3534    2193   1456 30942    8    56   43  15%      1   54   14    1 1974%
c i   25.1   90312   506444      3535    2193   1456 30942    8    56   43  15%      1   54   14    1 1966%
c i   25.1   90308   506444      3550    2201   1456 30946    8    55   43  15%      1   54   14    1 1875%
c i   25.1   90307   506444      3574    2216   1458 30952    8    55   43  15%      1   54   13    1 1767%
c i   25.2   90305   506444      3757    2371   1469 30963    9    59   43  14%      1   57   12    1 1655%
c i   25.3   90304   506444      3796    2401   1474 30966    8    59   43  14%      1   57   12    1 1543%
c i   25.3   90297   506444      3882    2476   1478 30971    9    60   43  14%      1   58   13    1 1714%
c i   25.5   90295   506444      4017    2584   1489 30983    9    63   43  14%      1   61   11    1 1342%
c i   25.5   90294   506444      4036    2595   1494 30985    9    63   43  14%      1   61   10    1 1274%
c i   25.5   90292   506444      4037    2595   1494 30985    9    63   43  14%      1   61   10    1 1269%
c i   25.6   90291   506444      4057    2610   1497 30986    9    64   43  13%      1   62   10    1 1216%
c i   25.7   90182   506444      4120    2658   1501 30996    9    65   43  13%      1   63    9    1 1127%
c i   25.7   90176   506444      4146    2679   1502 30998    9    65   43  13%      1   63    9    1 1098%
c i   25.7   90135   506444      4147    2679   1502 30998    9    65   43  13%      1   63    9    1 1094%
c i   25.8   90133   506444      4285    2787   1514 31013    9    66   43  13%      1   64   10    1 1221%
c i   26.0   90131   506444      4574    3039   1527 31034    9    72   43  13%      1   69   16    1 1782%
c i   26.2   90127   506444      4774    3198   1543 31052   10    77   44  13%      1   74   16    1 1666%
c i   26.3   90124   506444      5000    3400   1552 31065   10    77   44  13%      1   74   15    1 1539%
c i   26.4   89970   506444      5021    3417   1553 31067   10    78   44  13%      1   75   15    1 1467%
c 
c [simplification-6] limit 5072 conflicts (hard 15041) hit after 5074 conflicts
c [quatres-2] found 42878 quaternary clauses 52% in total
c [quatres-2-2] added 10 single-self-subsuming ternary resolvents
c [quatres-2-2] added 35 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 89970 free variables schedulable
c [ternres-2] 554 ternary resolvents (2 bin, 552 trn)
c [ternres-2] 36936 variables remain 41% (53034 retained 59%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2698 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] 2698 out of 2698 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 464 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 64435 literals 36%
c [treelook-3] scheduling used 313435 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 318676 steps
c [treelook-3] 64424 literals remain 36%
c [treelook-3] 36171 variables remain to probed next time 40%
c [treelook-3] removed 5 variables, found 2387 hbrs
c [unhide-6] limit 219243 with penalty 0 = 0 + 0
c [unhide-6-6] 6 units, 326 failed, 2276 tauts, 0 hbrs, 3917 literals
c [transred-2] limit 1096215 with penalty 0 = 0 + 0
c [transred-2] removed 82 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 88973 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 1196 blocked clauses
c [block-2] 1196 < 1/100 * 503062 = 5030 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 88963 variables 100%
c [elim-6] limit of 21924309 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 9621 not tried 11% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1663 = 2% variables out of 88963 scheduled
c [bca-2] limit of 10000000 steps and 981176 added (scaled 2)
c [bca-2] 163583 out of 174602 literals actually usable 94%
c [bca-2] added 121 blocked clauses in 471298 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3744 pos 4.3% + 83546 neg 95.7% = 87290 sched 100.0% ret 10
c [sweep-2-1] 1011792 steps 14 queries 19434.07 avg class size
c [sweep-2-1] 117 decisions 12 SAT calls 47.33 avg env size
c [sweep-2-1] 87257 variables remain 100% (43 retained 0%)
c [decomp-14] removed 23 variables
c [sweep-2-1] removed 23 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 23 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-6] 487633 negative 99.5% of 490244 except 2611 0.5%
c [phase-count-6] 395618 positive 80.7% of 490244 except 94626 19.3%
c [phase-count-6] less non-negative clauses 2611 than limit 49000 (10.0%)
c [phase-count-6] non-pos/non-neg = 94626/2611 = 36.24 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 8035 negative 100%
c [sort-queue-6] sorted 87277 enqueued variables after 5074 conflicts
c [score-dist-6] active 0 (0%), one 19834 (23%), zero 67443 (77%)
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 2693 variables 3.0% (87277 remain 28%)
c [simplification-6] removed 16200 irredundant clauses 3.2% (490244 remain 36%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 20074 (soft 10074 + delta 10000)
c [simplification-6] new conflict limit 10074 (hard 20074)
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   30.4   87276   490244      5142    3390   1574 32285   10    81   43  12%      1   78   14    1 1344%
c i   30.4   87274   490244      5155    3396   1574 32290   10    80   43  12%      1   77   13    1 1286%
c i   30.4   87260   490244      5169    3402   1577 32294   10    80   43  12%      1   77   13    1 1229%
c i   30.7   87251   490244      5447    3636   1594 32311   11    86   43  13%      2   83   20    1 1824%
c i   30.8   87250   490244      5578    3740   1604 32322   11    88   43  12%      1   85   17    1 1526%
c i   30.9   87249   490244      5709    3858   1611 32324   11    89   43  13%      1   85   19    1 1609%
c i   31.1   87248   490244      6001    4090   1638 32351   12    92   43  13%      2   88   17    1 1331%
c i   31.2   87133   490244      6099    4175   1643 32358   12    93   43  13%      2   89   15    1 1177%
c i   31.2   87132   490244      6164    4227   1645 32365   12    93   43  13%      1   89   14    1 1082%
c i   31.5   87131   490243      6377    4400   1658 32387   12    96   43  12%      1   91   11    1  862%
c i   31.5   86994   490243      6433    4432   1669 32399   11    96   43  12%      1   91   10    1  731%
c i   31.6   86993   490243      6505    4493   1671 32405   12    96   43  12%      1   92   11    1  826%
c i   31.7   86990   490243      6569    4539   1678 32414   11    97   43  12%      1   92   10    1  748%
c i   31.8   86988   490243      6750    4704   1688 32419   12    98   43  12%      1   93   15    1 1062%
c i   31.9   86987   490243      6880    4815   1698 32425   12    99   43  12%      1   93   15    1 1042%
c i   32.0   86980   490243      7014    4927   1709 32434   12   101   43  12%      1   95   13    1  884%
c i   32.0   86971   490243      7021    4931   1709 32435   12   101   43  12%      1   95   12    1  869%
c i   32.1   86970   490243      7051    4947   1717 32439   12   101   43  12%      1   95   11    1  805%
c i   32.2   86880   490243      7169    5036   1731 32452   12   101   43  11%      1   95    9    1  643%
c i   32.2   86836   490243      7170    5036   1731 32452   12   101   43  11%      1   95    9    1  641%
c i   32.3   86788   490243      7215    5066   1737 32460   12   103   44  11%      1   97    9    1  643%
c i   32.3   86764   490243      7236    5083   1739 32461   11   103   44  11%      1   97    9    1  631%
c i   32.3   86755   490243      7237    5083   1739 32461   11   103   44  11%      1   97    9    1  629%
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.6   86744   490243      7484    5257   1767 32493   11   104   44  11%      1   98    8    1  530%
c i   32.7   86719   490243      7643    5371   1779 32520   11   104   44  11%      1   97    7    1  457%
c i   32.7   86718   490243      7660    5376   1783 32527   11   104   44  11%      1   97    6    1  436%
c i   32.8   86430   490243      7662    5377   1783 32527   11   104   44  11%      1   97    6    1  434%
c i   32.8   86425   490243      7734    5425   1790 32538   11   104   44  11%      1   97    6    1  417%
c i   32.8   86420   490243      7751    5437   1791 32541   11   103   44  11%      1   97    6    1  404%
c i   32.9   86413   490243      7807    5478   1795 32551   11   103   44  10%      1   96    6    1  399%
c i   32.9   86364   490243      7868    5519   1804 32561   11   104   44  10%      1   97    6    1  380%
c i   32.9   86360   490243      7874    5523   1805 32561   11   103   44  10%      1   97    6    1  377%
c i   32.9   86357   490243      7876    5523   1806 32561   11   103   44  10%      1   97    6    1  374%
c i   33.0   86253   490243      7937    5566   1813 32570   11   102   44  10%      1   96    5    1  351%
c i   33.0   86085   490243      7940    5568   1813 32570   11   102   44  10%      1   95    5    1  348%
c i   33.2   86081   490243      8128    5707   1833 32591   11   105   44  10%      1   98    9    2  610%
c i   33.2   86065   490243      8169    5740   1836 32595   11   105   44  10%      1   98    8    2  555%
c i   33.2   86058   490243      8180    5742   1840 32598   11   105   44  10%      1   98    8    2  536%
c i   33.3   86054   490243      8278    5809   1852 32614   11   106   44  10%      1   98    9    2  570%
c i   33.6   86052   490243      8498    5973   1877 32635   10   106   44  10%      1   99    8    2  505%
c i   33.6   86043   490243      8529    5995   1881 32639   10   106   44  10%      1   98    7    2  473%
c i   33.6   86038   490243      8542    6005   1882 32640   10   106   44  10%      1   98    7    2  464%
c i   33.6   86032   490243      8545    6005   1883 32641   10   106   44  10%      1   98    7    2  459%
c i   33.6   86026   490243      8551    6007   1885 32642   10   105   44  10%      1   98    7    2  452%
c i   33.7   86017   490243      8634    6064   1891 32659   10   104   44  10%      1   96    7    2  420%
c i   33.8   86010   490243      8754    6146   1907 32679   10   105   44  10%      1   97    6    2  400%
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.9   85978   490243      8818    6195   1914 32685   10   105   44  10%      1   97    7    2  441%
c i   34.0   85975   490243      8889    6248   1917 32699   10   106   44   9%      1   97    6    2  407%
c i   34.1   85895   490243      8963    6298   1924 32713   10   105   44   9%      1   97    6    2  406%
c i   34.2   85890   490243      9023    6338   1933 32721   10   106   44   9%      1   98    6    2  389%
c i   34.2   85881   490243      9069    6375   1934 32726   10   106   44   9%      1   98    9    2  541%
c i   34.3   85879   490243      9162    6449   1946 32731   10   109   44   9%      1  100   14    2  886%
c i   34.5   85872   490243      9349    6612   1954 32743   11   110   44  10%      1  101   14    2  869%
c i   34.5   85869   490243      9415    6673   1955 32745   11   110   44  10%      1  101   14    2  849%
c i   34.6   85868   490243      9495    6745   1958 32748   11   109   44  10%      1  100   13    2  762%
c i   34.7   85867   490243      9693    6921   1965 32754   11   112   44  10%      1  103   16    2  908%
c i   34.8   85866   490243      9722    6946   1966 32756   11   112   44  10%      1  103   15    2  883%
c i   34.9   85859   490243      9837    7042   1973 32764   11   113   45  10%      1  103   17    2  947%
c i   34.9   85855   490243      9896    7090   1976 32765   11   112   45  10%      1  103   19    2 1055%
c i   34.9   85853   490243      9975    7157   1982 32766   12   112   45  10%      1  102   20    2 1127%
c i   35.0   85852   490243     10075    7248   1986 32770   12   113   45  10%      1  103   17    2  947%
c 
c [simplification-7] limit 10113 conflicts (hard 20074) hit after 10113 conflicts
c [quatres-3] found 38687 quaternary clauses 51% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 5 single-self-subsuming ternary resolvents
c [quatres-3-2] added 75 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 35210 schedulable variables 40%
c [ternres-3] 3076 ternary resolvents (4 bin, 3072 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 247 xors of average arity 2.3
c [gauss-2] connected 556 occurrences of 281 variables (average 2.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 203 variables
c [basicprobe-3] limit 11590513 penalty 0 = 0 + 0
c [basicprobe-3-0] 23484 probes remain 28% after last round
c [basicprobe-3-0] 93 units = 93 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 2248 variables, found 22122 hbrs
c [bate-1] eliminated 33 asymmetric tautologies during probing
c [unhide-7] limit 463620 with penalty 0 = 0 + 0
c [unhide-7-7] 5 units, 120 failed, 7366 tauts, 0 hbrs, 10799 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 106 transitive binary clauses
c [transred-3] found 5 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 4 clauses out of 631 (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 285729 clauses = 233684 binary + 52045 ternary
c [cce-2-1] tried to eliminate 253 small clauses 0%
c [cce-2-1] eliminated 54 binary clauses 0%
c [cce-2-1] eliminated 17 ternary clauses 0%
c [cce-2-1] eliminated 71 small clauses 0%
c [cce-2-1] eliminated 4897 small clauses in 15000003 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 4901 covered clauses in round 1
c [cce-2] eliminated 4901 covered clauses in TOTAL during 1 rounds
c [elim-7] 9187 variables 11% will be scheduled this time
c [elim-7] scheduled 9187 variables 11%
c [elim-7] limit of 46362053 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 7 variables 0% in round 1 in 15266406 steps
c [elim-7-1] backward subsumption/strengthening limit 15266400
c [elim-7-1-1] backward checking 1097 touched variables 1%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 22 and strengthened 2 clauses in 329244 steps
c [elim-7-1] rescheduled 69 variables 0% by backward subsumption
c [elim-7-2] eliminated 11 variables 0% in round 2 in 48091 steps
c [elim-7-2] backward subsumption/strengthening limit 48000
c [elim-7-2-1] backward checking 54 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 28 and strengthened 1 clauses in 48001 steps
c [elim-7-2] rescheduled 31 variables 0% by backward subsumption
c [elim-7-3] eliminated 12 variables 0% in round 3 in 22931 steps
c [elim-7-3] backward subsumption/strengthening limit 22900
c [elim-7-3-1] backward checking 71 touched variables 0%
c [elim-7-3-1] incomplete backward checking 1 remain 1%
c [elim-7-3] subsumed 21 and strengthened 1 clauses in 22928 steps
c [elim-7] incomplete 28 not tried 0% in round 3
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 32 = 0% variables out of 9187 scheduled
c [elim-7] 32 < 1/100 * 9187 = 91 considered unsuccessful
c [bca-3] limit of 10000000 steps and 909529 added (scaled 2)
c [bca-3] 145982 out of 165380 literals actually usable 88%
c [bca-3] added 90 blocked clauses in 389931 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 4792 pos 5.8% + 77855 neg 94.2% = 82647 sched 99.9% ret 42
c [sweep-3-1] 1095321 steps 21 queries 18743.43 avg class size
c [sweep-3-1] 237 decisions 17 SAT calls 61.35 avg env size
c [sweep-3-1] 82497 variables remain 100% (144 retained 0%)
c [decomp-16] removed 517 variables
c [sweep-3-1] removed 517 vars (0 failed, 3 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 517 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-7] 450729 negative 99.4% of 453323 except 2594 0.6%
c [phase-count-7] 367115 positive 81.0% of 453323 except 86208 19.0%
c [phase-count-7] less non-negative clauses 2594 than limit 45300 (10.0%)
c [phase-count-7] non-pos/non-neg = 86208/2594 = 33.23 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 3035 negative 100%
c [sort-queue-7] sorted 82172 enqueued variables after 10113 conflicts
c [score-dist-7] active 0 (0%), one 29988 (36%), zero 52184 (64%)
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 3680 variables 4.3% (82172 remain 26%)
c [simplification-7] removed 36920 irredundant clauses 7.5% (453323 remain 33%)
c [simplification-7] maximum reduction of 8% = max (4%, 8%)
c [simplification-7] large reduction 8% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 22113 (soft 12113 + delta 10000)
c [simplification-7] new conflict limit 12113 (hard 22113)
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   38.6   82171   453323     10428    7547   4034 51301   12   114   44  11%      1  103   22    2 1147%
c i   38.7   82170   453323     10485    7599   4035 51301   13   114   44  11%      1  103   25    2 1258%
c i   38.7   82166   453323     10500    7609   4036 51304   13   114   44  11%      1  103   23    2 1198%
c i   39.0   82159   453323     10923    7966   4060 51328   13   116   44  11%      2  105   20    2  959%
c i   39.1   82157   453323     10994    8028   4065 51331   13   117   44  11%      2  105   18    2  865%
c i   39.2   82143   453323     11088    8100   4071 51343   13   117   44  11%      2  105   15    2  726%
c i   39.2   82136   453323     11146    8149   4074 51347   13   116   44  11%      2  104   13    2  637%
c i   39.2   82135   453323     11230    8225   4074 51351   13   116   44  11%      2  104   17    2  786%
c i   39.3   82127   453323     11310    8295   4077 51356   13   118   44  11%      1  106   16    2  764%
c i   39.4   82126   453323     11330    8310   4080 51357   13   118   44  11%      1  106   16    2  727%
c i   40.0   82122   453323     11983    8893   4104 51389   15   127   44  12%      3  114   22    2  927%
c i   40.0   81880   453323     11994    8902   4104 51390   15   127   44  12%      3  114   22    2  929%
c 
c [simplification-8] limit 12113 conflicts (hard 22113) hit after 12113 conflicts
c [quatres-4] found 38788 quaternary clauses 54% in total
c [quatres-4-2] added 46 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] all 81877 free variables schedulable
c [ternres-4] 153 ternary resolvents (0 bin, 153 trn)
c [ternres-4] 31380 variables remain 38% (50497 retained 62%)
c [decomp-17] removed 350 variables
c [simpleprobe-4] 49269 schedulable variables 60%
c [simpleprobe-4] limit 11128423 penalty 0 = 0 + 0
c [decomp-18] removed 1225 variables
c [simpleprobe-4] 19585 variables remain 24% (61012 retained 76%)
c [simpleprobe-4] removed 1225 variables, found 34537 hbrs, 208 units
c [unhide-8] limit 556421 with penalty 0 = 0 + 0
c [unhide-8-8] 21 units, 429 failed, 8887 tauts, 0 hbrs, 12906 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 180 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 79712 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 159 blocked clauses
c [block-3] 159 < 1/100 * 443196 = 4431 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 593 (0%) of length 7
c [cce-3-1] eliminated 116 clauses out of 1402 (8%) of length 6
c [cce-3-1] eliminated 1002 clauses out of 26709 (4%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1119 large clauses in 30000019 steps
c [cce-3-1] allowing another 15000009 steps for small clauses
c [cce-3-1] scheduling 322077 clauses = 227243 binary + 94834 ternary
c [cce-3-1] tried to eliminate 442 small clauses 0%
c [cce-3-1] eliminated 86 binary clauses 0%
c [cce-3-1] eliminated 61 ternary clauses 0%
c [cce-3-1] eliminated 147 small clauses 0%
c [cce-3-1] eliminated 147 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1266 covered clauses in round 1
c [cce-3] eliminated 1266 covered clauses in TOTAL during 1 rounds
c [cce-3] 1266 < 1/100 * 436948 = 4369 considered unsuccessful
c [bca-4] limit of 10000000 steps and 872060 added (scaled 2)
c [bca-4] 138292 out of 159416 literals actually usable 87%
c [bca-4] added 93 blocked clauses in 365432 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 4929 pos 6.2% + 74645 neg 93.8% = 79574 sched 99.8% ret 133
c [sweep-4-1] 1010416 steps 17 queries 19269.35 avg class size
c [sweep-4-1] 197 decisions 14 SAT calls 64.00 avg env size
c [sweep-4-1] 79520 variables remain 100% (187 retained 0%)
c [decomp-19] removed 470 variables
c [sweep-4-1] removed 470 vars (0 failed, 2 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 470 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-8] 433157 negative 99.6% of 434711 except 1554 0.4%
c [phase-count-8] 350130 positive 80.5% of 434711 except 84581 19.5%
c [phase-count-8] less non-negative clauses 1554 than limit 43400 (10.0%)
c [phase-count-8] non-pos/non-neg = 84581/1554 = 54.43 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 1209 negative 100%
c [sort-queue-8] sorted 79237 enqueued variables after 12113 conflicts
c [score-dist-8] active 0 (0%), one 33145 (42%), zero 46092 (58%)
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 2640 variables 3.2% (79237 remain 25%)
c [simplification-8] removed 18612 irredundant clauses 4.1% (434711 remain 32%)
c [simplification-8] maximum reduction of 4% = max (3%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 9000
c [simplification-8] penalized conflict interval 9000 = 1 * 9000
c [simplification-8] hard conflict limit 31113 (soft 21113 + delta 10000)
c [simplification-8] new conflict limit 21113 (hard 31113)
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   43.7   79236   434711     12114    8866   3325 75782   15   128   42  12%      3  115   20    2  828%
c i   43.7   79235   434711     12123    8872   3326 75783   15   128   43  12%      3  115   19    2  804%
c i   43.7   79233   434711     12134    8878   3327 75786   15   128   43  12%      3  114   19    2  784%
c i   43.7   79228   434711     12145    8886   3327 75787   15   128   44  11%      3  115   18    2  768%
c i   43.8   79223   434711     12166    8899   3333 75788   15   128   44  11%      3  115   18    2  756%
c i   43.8   79213   434711     12237    8954   3340 75796   15   128   44  11%      3  114   17    2  704%
c i   44.0   79209   434711     12449    9130   3356 75812   15   127   44  12%      2  113   14    2  576%
c i   44.2   79206   434711     12581    9243   3363 75822   14   127   44  11%      2  113   12    2  490%
c i   44.2   79205   434711     12589    9250   3363 75822   14   127   44  11%      2  113   12    2  484%
c i   44.2   79202   434711     12636    9293   3364 75824   14   127   44  11%      2  113   13    2  537%
c i   44.6   79188   434711     13062    9665   3383 75842   15   127   44  12%      3  111   16    3  644%
c i   44.6   79185   434711     13129    9722   3383 75850   15   128   44  12%      2  113   15    3  594%
c i   44.7   79183   434711     13145    9736   3384 75850   15   128   44  12%      2  113   15    3  599%
c i   44.9   79182   434711     13359    9926   3394 75859   15   132   44  11%      2  116   18    3  700%
c i   45.0   79180   434711     13456   10007   3398 75865   15   131   44  11%      2  116   16    3  619%
c i   45.2   79177   434711     13695   10216   3407 75875   16   133   44  12%      2  116   22    3  796%
c i   45.3   79169   434711     13744   10256   3412 75878   16   134   44  12%      2  117   20    3  731%
c i   45.3   79157   434711     13745   10256   3412 75878   16   133   44  12%      2  117   20    3  728%
c i   45.3   79156   434711     13746   10256   3412 75878   16   133   44  12%      2  117   20    3  726%
c i   45.7   79155   434711     14226   10662   3441 75906   16   136   44  12%      3  119   19    3  657%
c i   45.7   79154   434711     14249   10679   3443 75909   16   136   44  12%      2  118   18    3  625%
c i   45.8   79153   434711     14351   10756   3452 75918   16   135   44  12%      2  118   16    3  563%
c i   45.8   79149   434711     14367   10766   3455 75920   16   135   44  12%      2  118   16    3  545%
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   45.8   79148   434711     14368   10766   3455 75920   16   135   44  12%      2  118   16    3  543%
c i   45.8   79146   434711     14369   10766   3455 75920   16   135   44  12%      2  118   16    3  541%
c i   46.0   79145   434711     14524   10891   3468 75934   16   137   44  11%      2  119   14    3  474%
c i   46.3   79131   434711     14845   11158   3486 75952   17   139   44  12%      2  121   25    3  837%
c i   46.4   79130   434711     14878   11187   3486 75955   17   139   44  12%      2  120   24    3  786%
c i   46.6   79129   434711     15117   11383   3502 75979   17   141   44  12%      2  122   19    3  614%
c i   47.0   79127   434711     15483   11706   3522 75994   17   142   44  12%      2  122   17    3  546%
c i   47.0   79051   434711     15495   11707   3525 75997   17   142   44  12%      2  122   17    3  526%
c i   47.1   79013   434711     15549   11749   3532 76001   17   141   44  12%      2  122   15    3  486%
c i   47.2   78998   434711     15656   11837   3537 76013   16   141   44  12%      2  121   13    3  417%
c i   47.2   78996   434711     15660   11840   3537 76013   16   141   44  12%      2  121   13    3  415%
c i   47.4   78989   434711     15810   11965   3541 76025   17   141   44  12%      2  120   17    3  526%
c i   47.4   78982   434711     15813   11965   3541 76027   17   140   44  12%      2  120   17    3  520%
c i   47.4   78968   434711     15834   11981   3543 76028   17   141   44  12%      2  121   16    3  497%
c i   47.5   78955   434711     15876   12010   3547 76031   17   142   44  12%      2  121   20    3  616%
c i   47.6   78947   434711     15954   12074   3551 76040   17   143   44  12%      2  122   17    3  532%
c i   47.6   78943   434711     15955   12074   3551 76040   17   143   44  12%      2  122   17    3  530%
c i   47.9   78939   434711     16148   12239   3560 76051   18   145   44  12%      1  125   33    3  979%
c i   47.9   78933   434711     16213   12294   3564 76056   18   147   44  12%      1  126   29    3  844%
c i   48.0   78928   434711     16235   12311   3565 76059   18   147   44  12%      1  126   27    3  792%
c i   48.0   78927   434711     16282   12341   3572 76067   18   146   44  12%      1  125   23    3  684%
c i   48.1   78926   434711     16372   12414   3578 76076   18   146   45  12%      1  125   27    3  781%
c i   48.4   78914   434711     16639   12652   3594 76084   18   151   45  12%      1  129   19    3  535%
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   48.5   78894   434711     16667   12676   3595 76086   18   152   45  12%      1  130   19    3  545%
c i   48.8   78840   434711     16952   12918   3612 76101   18   155   45  11%      1  133   17    4  493%
c i   49.0   78828   434711     17031   12987   3618 76102   18   157   45  12%      1  134   24    4  663%
c i   49.0   78824   434711     17058   13010   3621 76102   18   157   45  12%      1  134   24    4  674%
c i   49.2   78823   434711     17309   13230   3629 76117   19   157   45  12%      1  134   29    4  793%
c i   49.7   78822   434711     17641   13504   3652 76138   20   160   45  12%      2  137   26    4  688%
c i   49.7   78813   434711     17647   13507   3653 76139   20   160   45  12%      2  137   26    4  675%
c i   49.8   78584   434711     17722   13571   3655 76145   20   162   45  12%      2  139   24    4  623%
c i   49.9   78575   434711     17837   13674   3659 76151   19   162   45  12%      1  138   20    4  518%
c i   50.0   78574   434711     17908   13735   3662 76156   20   164   45  12%      1  139   23    4  603%
c i   50.0   78573   434711     17919   13743   3662 76156   20   163   45  12%      1  139   23    4  586%
c i   50.3   78568   434711     18214   14006   3671 76166   20   162   45  12%      2  137   21    4  537%
c i   50.3   78560   434711     18216   14007   3671 76166   20   162   45  12%      2  137   21    4  544%
c i   50.5   78554   434711     18297   14076   3675 76171   20   163   45  12%      1  138   22    4  547%
c i   50.5   78553   434711     18298   14076   3675 76171   20   163   45  12%      1  138   22    4  545%
c i   50.5   78552   434711     18299   14076   3675 76171   20   163   45  12%      1  138   22    4  542%
c i   50.6   78551   434711     18373   14141   3677 76176   20   164   46  12%      1  138   24    4  598%
c i   50.7   78545   434711     18446   14199   3683 76184   20   164   46  12%      1  139   21    4  520%
c i   50.8   78540   434711     18499   14240   3686 76190   20   164   46  12%      1  139   23    4  558%
c i   50.9   78536   434711     18593   14326   3687 76190   20   164   46  12%      1  138   20    4  492%
c i   51.4   78500   434711     19020   14696   3710 76207   20   164   46  12%      2  138   25    4  592%
c i   51.5   78493   434711     19115   14789   3710 76208   20   164   46  12%      2  138   25    4  605%
c i   51.7   78490   434711     19309   14952   3715 76214   21   162   46  13%      2  135   31    4  720%
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.7   78464   434711     19310   14952   3715 76214   21   162   46  13%      2  135   31    4  717%
c i   51.7   78461   434711     19311   14952   3715 76214   21   162   46  13%      2  135   31    4  714%
c i   51.7   78459   434711     19351   14988   3717 76215   21   162   46  13%      2  134   31    4  715%
c i   51.7   78456   434711     19359   14994   3717 76215   21   161   46  13%      1  134   30    4  694%
c i   51.8   78448   434711     19427   15055   3717 76219   21   161   46  13%      1  133   30    4  695%
c i   51.8   78438   434711     19459   15084   3718 76220   21   161   46  13%      1  134   29    4  670%
c i   51.8   78423   434711     19463   15087   3718 76220   21   161   46  13%      1  134   29    4  663%
c i   52.1   78419   434711     19612   15222   3723 76223   22   164   48  13%      1  136   34    4  763%
c i   52.1   78418   434711     19653   15260   3724 76224   22   165   48  13%      1  137   31    4  703%
c i   52.2   78415   434711     19737   15320   3731 76238   22   163   48  13%      1  135   24    4  550%
c i   52.2   78408   434711     19773   15349   3733 76242   21   163   48  13%      1  135   23    4  513%
c i   52.3   78407   434711     19837   15405   3733 76247   21   164   48  13%      1  136   22    4  494%
c i   52.5   78401   434711     19943   15499   3740 76250   21   164   48  13%      1  136   20    4  437%
c i   52.5   78400   434711     19957   15508   3742 76252   21   164   48  13%      1  136   19    4  432%
c i   52.5   78392   434711     19964   15507   3743 76254   21   164   48  13%      1  135   20    4  448%
c i   52.7   78372   434711     20139   15656   3757 76264   21   166   48  13%      1  137   21    5  460%
c i   53.1   78281   434711     20439   15917   3767 76280   22   166   48  13%      1  137   25    5  539%
c i   53.2   78276   434711     20492   15962   3771 76282   22   168   48  13%      1  138   26    5  564%
c i   53.2   78271   434711     20493   15962   3771 76282   22   168   48  13%      1  138   26    5  562%
c i   53.2   78262   434711     20495   15963   3770 76283   22   168   48  13%      1  138   26    5  558%
c i   53.2   78256   434711     20511   15971   3772 76287   22   168   48  13%      1  138   25    5  533%
c i   53.2   78192   434711     20559   16009   3778 76290   21   168   48  13%      1  138   21    5  460%
c i   53.4   78100   434711     20733   16156   3789 76300   21   169   48  13%      1  139   21    5  445%
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   53.7   78099   434711     20968   16362   3803 76310   22   168   48  13%      1  137   23    5  479%
c i   54.0   78092   434711     21178   16539   3821 76321   21   168   48  13%      1  137   17    5  355%
c 
c [simplification-9] limit 21235 conflicts (hard 31113) hit after 21235 conflicts
c [quatres-5] found 34199 quaternary clauses 53% in total
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3 quaternary resolvents
c [ternres-5] limit 5461256 with penalty 0 = 0 + 0
c [ternres-5] 29775 schedulable variables 38%
c [ternres-5] 245 ternary resolvents (3 bin, 242 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 2186 variables
c [treelook-4] limit 546125 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 85979 literals 56%
c [treelook-4] scheduling used 546342 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 546125 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 566321 steps
c [treelook-4] 85966 literals remain 56%
c [treelook-4] 29049 variables remain to probed next time 38%
c [decomp-21] removed 5 variables
c [treelook-4] removed 6 variables, found 3896 hbrs
c [unhide-9] limit 1092251 with penalty 0 = 0 + 0
c [unhide-9-9] 32 units, 43 failed, 6190 tauts, 0 hbrs, 24681 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 129 transitive binary clauses
c [transred-5] found 1 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 76869 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1092251370 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3876 variables 5% in round 1 in 33122326 steps
c [elim-8-1] backward subsumption/strengthening limit 33122300
c [elim-8-1-1] backward checking 14525 touched variables 19%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 84 and strengthened 222 clauses in 3282828 steps
c [elim-8-1] rescheduled 741 variables 1% by backward subsumption
c [elim-8-2] eliminated 91 variables 0% in round 2 in 693196 steps
c [elim-8-2] backward subsumption/strengthening limit 693100
c [elim-8-2-1] backward checking 607 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 44 and strengthened 26 clauses in 330268 steps
c [elim-8-2] rescheduled 148 variables 0% by backward subsumption
c [elim-8-3] eliminated 26 variables 0% in round 3 in 153829 steps
c [elim-8-3] backward subsumption/strengthening limit 153800
c [elim-8-3-1] backward checking 107 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 31 and strengthened 7 clauses in 153801 steps
c [elim-8] incomplete 78 not tried 0% in round 3
c [gc-59] reconnected 76572 binary clauses (produced 0 empty 6 units)
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 4140 = 5% variables out of 76869 scheduled
c [bca-5] limit of 10000000 steps and 811516 added (scaled 2)
c [bca-5] 122660 out of 145460 literals actually usable 84%
c [bca-5] added 47 blocked clauses in 324172 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 16383770 penalty 0 = 0 + 0
c [sweep-5-1] 4241 pos 5.8% + 68316 neg 94.2% = 72557 sched 99.8% ret 172
c [sweep-5-1] 16528932 steps 179 queries 3012.54 avg class size
c [sweep-5-1] 1424 decisions 134 SAT calls 66.99 avg env size
c [sweep-5-1] 69273 variables remain 96% (3261 retained 4%)
c [decomp-22] removed 454 variables
c [sweep-5-1] removed 454 vars (0 failed, 53 eqs, 78 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 454 vars in TOTAL (1 rounds, 178 queries)
c [phase-count-9] 402301 negative 99.7% of 403385 except 1084 0.3%
c [phase-count-9] 325718 positive 80.7% of 403385 except 77667 19.3%
c [phase-count-9] less non-negative clauses 1084 than limit 40300 (10.0%)
c [phase-count-9] non-pos/non-neg = 77667/1084 = 71.65 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 385 negative 100%
c [sort-queue-9] sorted 72275 enqueued variables after 21235 conflicts
c [score-dist-9] active 0 (0%), one 36108 (50%), zero 36167 (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 5392 variables 6.9% (72275 remain 23%)
c [simplification-9] removed 31326 irredundant clauses 7.2% (403385 remain 29%)
c [simplification-9] maximum reduction of 7% = max (7%, 7%)
c [simplification-9] large reduction 7% >= 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 33235 (soft 23235 + delta 10000)
c [simplification-9] new conflict limit 23235 (hard 33235)
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   58.9   72274   403385     21252   11542   3193 77968   21   168   43  13%      1  137   17    5  355%
c i   59.4   72267   403385     21767   11998   3214 77990   20   168   44  12%      2  136   15    5  314%
c i   59.9   72256   403385     22229   12401   3234 78014   20   165   44  12%      3  131   12    5  246%
c i   60.0   72255   403385     22412   12561   3242 78024   19   164   44  12%      2  130   12    5  246%
c i   60.1   72254   403385     22449   12593   3244 78026   19   165   44  12%      2  131   12    5  247%
c i   60.1   72249   403385     22450   12593   3244 78026   19   165   44  12%      2  131   12    5  246%
c i   60.1   72247   403385     22460   12601   3245 78026   19   165   44  12%      2  131   12    5  241%
c i   60.1   72232   403385     22461   12601   3245 78026   19   165   44  12%      2  131   12    5  240%
c i   60.1   72220   403385     22462   12601   3245 78026   19   165   44  12%      2  131   12    5  239%
c i   60.4   72214   403385     22643   12764   3254 78033   19   166   44  11%      2  132   14    5  289%
c i   60.4   72213   403385     22678   12793   3254 78034   19   166   44  12%      2  132   15    5  292%
c i   60.4   72209   403385     22750   12856   3255 78035   20   165   44  12%      2  131   25    5  497%
c i   60.5   72205   403385     22766   12868   3257 78036   20   165   44  12%      2  131   24    5  481%
c i   60.5   72200   403385     22790   12887   3259 78038   20   165   44  12%      2  131   23    5  458%
c i   60.6   72196   403385     22830   12914   3262 78046   20   165   44  12%      2  131   22    5  435%
c i   60.6   72193   403385     22855   12933   3264 78049   20   166   44  12%      2  132   22    5  431%
c i   60.7   72189   403385     22883   12953   3266 78051   20   166   44  12%      2  132   20    5  399%
c i   60.7   72186   403385     22923   12990   3267 78052   20   166   44  12%      1  132   21    5  414%
c i   60.7   72182   403385     22925   12990   3267 78053   20   166   44  12%      1  132   21    5  411%
c i   60.8   72181   403385     23008   13044   3279 78066   19   165   44  12%      1  131   18    5  344%
c i   61.0   72155   403385     23189   13194   3288 78077   20   169   44  12%      1  134   25    5  490%
c i   61.1   72152   403385     23220   13219   3289 78080   20   168   44  12%      1  133   24    5  458%
c i   61.1   72150   403385     23221   13219   3289 78080   20   168   44  12%      1  133   24    5  456%
c 
c [simplification-10] limit 23281 conflicts (hard 33235) hit after 23281 conflicts
c [quatres-6] found 34648 quaternary clauses 53% in total
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [quatres-6-2] added 6 quaternary resolvents
c [ternres-6] limit 6064991 with penalty 0 = 0 + 0
c [ternres-6] all 72149 free variables schedulable
c [ternres-6] 930 ternary resolvents (2 bin, 928 trn)
c [ternres-6] 203 variables remain 0% (71946 retained 100%)
c [card-4] limit 379061 penalty 3 = 3 + 0
c [card-4] found 1878 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 379061 for elimination
c [card-4] 1878 out of 1878 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 33 xors of average arity 2.6
c [gauss-3] connected 86 occurrences of 84 variables (average 1.0)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 75 variables
c [basicprobe-4] limit 30324955 penalty 0 = 0 + 0
c [basicprobe-4-0] 19006 probes remain 27% after last round
c [basicprobe-4-0] 255 units = 255 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 862 variables, found 42573 hbrs
c [bate-2] eliminated 73 asymmetric tautologies during probing
c [unhide-10] limit 1212998 with penalty 0 = 0 + 0
c [unhide-10-10] 56 units, 356 failed, 9849 tauts, 0 hbrs, 16589 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 142 transitive binary clauses
c [transred-6] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 151624775 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 43
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-4-1] eliminated 1 clauses out of 2 (50%) 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 2 (50%) of length 38
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 35
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 33
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 31
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 29
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 27
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 15
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 14
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 13
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 12
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 11
c [cce-4-1] eliminated 2 clauses out of 77 (3%) of length 10
c [cce-4-1] eliminated 4 clauses out of 222 (2%) of length 9
c [cce-4-1] eliminated 2 clauses out of 320 (1%) of length 8
c [cce-4-1] eliminated 5 clauses out of 516 (1%) of length 7
c [cce-4-1] eliminated 16 clauses out of 1292 (1%) of length 6
c [cce-4-1] eliminated 13041 clauses out of 22541 (58%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 13173 large clauses in 151624777 steps
c [cce-4-1] allowing another 75812388 steps for small clauses
c [cce-4-1] scheduling 245502 clauses = 201943 binary + 43559 ternary
c [cce-4-1] tried to eliminate 2783 small clauses 1%
c [cce-4-1] eliminated 594 binary clauses 0%
c [cce-4-1] eliminated 147 ternary clauses 0%
c [cce-4-1] eliminated 741 small clauses 0%
c [cce-4-1] eliminated 7937 small clauses in 151624776 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 21110 covered clauses in round 1
c [cce-4] eliminated 21110 covered clauses in TOTAL during 1 rounds
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 70223 variables 100%
c [elim-9] limit of 121299822 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 10604 variables 15% in round 1 in 28924079 steps
c [elim-9-1] backward subsumption/strengthening limit 28924000
c [elim-9-1-1] backward checking 27115 touched variables 39%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 126 and strengthened 169 clauses in 4382226 steps
c [elim-9-1] rescheduled 1010 variables 1% by backward subsumption
c [elim-9-2] eliminated 97 variables 0% in round 2 in 651315 steps
c [elim-9-2] backward subsumption/strengthening limit 651300
c [elim-9-2-1] backward checking 641 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 18 and strengthened 24 clauses in 514672 steps
c [elim-9-2] rescheduled 99 variables 0% by backward subsumption
c [elim-9-3] eliminated 3 variables 0% in round 3 in 76325 steps
c [elim-9-3] backward subsumption/strengthening limit 76300
c [elim-9-3-1] backward checking 32 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 5 and strengthened 4 clauses in 76301 steps
c [elim-9] incomplete 16 not tried 0% in round 3
c [gc-68] reconnected 106178 binary clauses (produced 0 empty 7 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 10879 = 15% variables out of 70223 scheduled
c [bca-6] limit of 10000000 steps and 690806 added (scaled 2)
c [bca-6] 108616 out of 118690 literals actually usable 92%
c [bca-6] added 63 blocked clauses in 263901 steps
c [sweep-6] limit 1819497 penalty 0 = 0 + 0
c [sweep-6-1] 3991 pos 7.0% + 52843 neg 93.0% = 56834 sched 95.8% ret 2510
c [sweep-6-1] 1946933 steps 37 queries 10670.05 avg class size
c [sweep-6-1] 243 decisions 30 SAT calls 50.20 avg env size
c [sweep-6-1] 56671 variables remain 96% (2655 retained 4%)
c [decomp-24] removed 170 variables
c [sweep-6-1] removed 170 vars (0 failed, 11 eqs, 9 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 170 vars in TOTAL (1 rounds, 36 queries)
c [phase-count-10] 343591 negative 99.7% of 344637 except 1046 0.3%
c [phase-count-10] 269650 positive 78.2% of 344637 except 74987 21.8%
c [phase-count-10] less non-negative clauses 1046 than limit 34400 (10.0%)
c [phase-count-10] non-pos/non-neg = 74987/1046 = 71.69 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 366 negative 100%
c [sort-queue-10] sorted 59174 enqueued variables after 23281 conflicts
c [score-dist-10] active 0 (0%), one 28682 (48%), zero 30492 (52%)
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 12975 variables 18.0% (59174 remain 19%)
c [simplification-10] removed 58748 irredundant clauses 14.6% (344637 remain 25%)
c [simplification-10] maximum reduction of 18% = max (18%, 15%)
c [simplification-10] large reduction 18% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 35281 (soft 25281 + delta 10000)
c [simplification-10] new conflict limit 25281 (hard 35281)
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   70.9   59173   344637     23457    3839   3296 95672   20   167   37  12%      1  132   18    5  341%
c i   71.1   59172   344637     23774    4113   3304 95697   19   161   37  12%      2  125   10    5  195%
c i   71.4   59169   344637     24301    4576   3338 95718   18   154   37  11%      2  117   10    5  187%
c i   71.4   59167   344637     24421    4679   3348 95723   17   152   37  11%      2  115    9    5  163%
c i   71.5   59164   344637     24624    4851   3354 95738   17   148   37  11%      2  110    9    5  171%
c i   71.5   59162   344637     24649    4870   3357 95740   17   148   37  11%      2  110    9    5  164%
c i   71.7   59160   344637     24841    5028   3371 95750   17   146   37  11%      2  108   11    5  205%
c i   71.8   59155   344637     25052    5206   3383 95761   16   145   37  11%      2  106    8    5  159%
c 
c [simplification-11] limit 25281 conflicts (hard 35281) hit after 25281 conflicts
c [quatres-7] found 38170 quaternary clauses 74% in total
c [quatres-7-1] removed 3 duplicate quaternary clauses
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 31 quaternary resolvents
c [ternres-7] limit 6413054 with penalty 0 = 0 + 0
c [ternres-7] 156 schedulable variables 0%
c [ternres-7] 286 ternary resolvents (4 bin, 282 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 38 variables
c [simpleprobe-5] 16183 schedulable variables 27%
c [simpleprobe-5] limit 25652219 penalty 0 = 0 + 0
c [decomp-26] removed 1852 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1852 variables, found 45837 hbrs, 368 units
c [unhide-11] limit 1282610 with penalty 0 = 0 + 0
c [unhide-11-11] 1 units, 26 failed, 5956 tauts, 0 hbrs, 3523 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 208 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 57251 variables 100%
c [block-4] limit of 16032637 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 344 blocked clauses
c [block-4] 344 < 1/100 * 328190 = 3281 considered unsuccessful
c [cce-5] limit of 32065274 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 9
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 8
c [cce-5-1] eliminated 6 clauses out of 25 (24%) of length 7
c [cce-5-1] eliminated 14 clauses out of 1115 (1%) of length 6
c [cce-5-1] eliminated 423 clauses out of 9417 (4%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 445 large clauses in 32065279 steps
c [cce-5-1] allowing another 16032639 steps for small clauses
c [cce-5-1] scheduling 242764 clauses = 162134 binary + 80630 ternary
c [cce-5-1] tried to eliminate 666 small clauses 0%
c [cce-5-1] eliminated 116 binary clauses 0%
c [cce-5-1] eliminated 80 ternary clauses 0%
c [cce-5-1] eliminated 196 small clauses 0%
c [cce-5-1] eliminated 196 small clauses in 32065279 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 641 covered clauses in round 1
c [cce-5] eliminated 641 covered clauses in TOTAL during 1 rounds
c [cce-5] 641 < 1/100 * 327611 = 3276 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 57250 variables 100%
c [elim-10] limit of 128261099 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1860 variables 3% in round 1 in 26394836 steps
c [elim-10-1] backward subsumption/strengthening limit 26394800
c [elim-10-1-1] backward checking 7850 touched variables 14%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 43 and strengthened 67 clauses in 1809533 steps
c [elim-10-1] rescheduled 306 variables 1% by backward subsumption
c [elim-10-2] eliminated 22 variables 0% in round 2 in 485131 steps
c [elim-10-2] backward subsumption/strengthening limit 485100
c [elim-10-2-1] backward checking 241 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 28 and strengthened 8 clauses in 165201 steps
c [elim-10-2] rescheduled 52 variables 0% by backward subsumption
c [elim-10-3] eliminated 3 variables 0% in round 3 in 44644 steps
c [elim-10-3] backward subsumption/strengthening limit 44600
c [elim-10-3-1] backward checking 25 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 1 and strengthened 1 clauses in 44601 steps
c [elim-10] incomplete 8 not tried 0% in round 3
c [gc-77] reconnected 134750 binary clauses (produced 0 empty 1 units)
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 1902 = 3% variables out of 57250 scheduled
c [bca-7] limit of 10000000 steps and 645549 added (scaled 2)
c [bca-7] 99042 out of 110698 literals actually usable 89%
c [bca-7] added 12 blocked clauses in 236974 steps
c [sweep-7] limit 1923916 penalty 0 = 0 + 0
c [sweep-7-1] 3368 pos 6.4% + 49639 neg 93.6% = 53007 sched 95.8% ret 2341
c [sweep-7-1] 1924259 steps 23 queries 8726.39 avg class size
c [sweep-7-1] 195 decisions 18 SAT calls 69.06 avg env size
c [sweep-7-1] 52906 variables remain 96% (2442 retained 4%)
c [decomp-27] removed 12 variables
c [sweep-7-1] removed 12 vars (0 failed, 5 eqs, 10 impls)
c [sweep-7] 12 < 1/1000 * 55348 = 55 considered unsuccessful
c [sweep-7] removed 12 vars in TOTAL (1 rounds, 22 queries)
c [phase-count-11] 321330 negative 99.7% of 322355 except 1025 0.3%
c [phase-count-11] 250915 positive 77.8% of 322355 except 71440 22.2%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 21 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 55336 enqueued variables after 25281 conflicts
c [score-dist-11] active 0 (0%), one 27512 (50%), zero 27824 (50%)
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 3806 variables 6.4% (55336 remain 18%)
c [simplification-11] removed 22282 irredundant clauses 6.5% (322355 remain 23%)
c [simplification-11] maximum reduction of 6% = max (6%, 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 37281 (soft 27281 + delta 10000)
c [simplification-11] new conflict limit 27281 (hard 37281)
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   76.7   55335   322355     25409    5301   3217 130735   16   141   38  11%      2  102   11    5  200%
c i   76.7   55333   322355     25425    5316   3217 130735   16   141   38  11%      2  102   10    5  194%
c i   77.0   55318   322355     26013    5848   3243 130752   16   134   38  12%      3   94   15    5  285%
c i   77.2   55314   322355     26307    6103   3261 130762   16   133   38  12%      3   93   13    5  244%
c i   77.3   55308   322355     26497    6265   3273 130773   16   133   38  12%      2   92   14    5  264%
c i   77.7   55304   322355     27002    6695   3312 130799   15   131   38  12%      3   90   12    6  225%
c i   77.8   55302   322355     27053    6735   3318 130803   15   131   38  11%      3   90   12    6  212%
c 
c [simplification-12] limit 27281 conflicts (hard 37281) hit after 27281 conflicts
c [quatres-8] found 33974 quaternary clauses 73% in total
c [quatres-8-1] removed 3 duplicate quaternary clauses
c [quatres-8-2] added 4 single-self-subsuming ternary resolvents
c [quatres-8-2] added 22 quaternary resolvents
c [ternres-8] limit 6824228 with penalty 0 = 0 + 0
c [ternres-8] all 55302 free variables schedulable
c [ternres-8] 1214 ternary resolvents (2 bin, 1212 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 50 variables
c [treelook-5] limit 682422 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 77501 literals 70%
c [treelook-5] scheduling used 682430 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 682422 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 690576 steps
c [treelook-5] 77438 literals remain 70%
c [treelook-5] 16047 variables remain to probed next time 29%
c [decomp-29] removed 39 variables
c [treelook-5] removed 55 variables, found 5617 hbrs
c [unhide-12] limit 1364845 with penalty 0 = 0 + 0
c [unhide-12-12] 7 units, 192 failed, 13323 tauts, 0 hbrs, 4916 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 176 transitive binary clauses
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 54841 variables 100%
c [elim-11] limit of 136484570 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 622 variables 1% in round 1 in 25846282 steps
c [elim-11-1] backward subsumption/strengthening limit 25846200
c [elim-11-1-1] backward checking 3207 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 24 and strengthened 69 clauses in 881234 steps
c [elim-11-1] rescheduled 222 variables 0% by backward subsumption
c [elim-11-2] eliminated 23 variables 0% in round 2 in 162141 steps
c [elim-11-2] backward subsumption/strengthening limit 162100
c [elim-11-2-1] backward checking 181 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 13 and strengthened 21 clauses in 148099 steps
c [elim-11-2] rescheduled 69 variables 0% by backward subsumption
c [elim-11-3] eliminated 6 variables 0% in round 3 in 279675 steps
c [elim-11-3] backward subsumption/strengthening limit 279600
c [elim-11-3-1] backward checking 46 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 57465 steps
c [elim-11] incomplete 7 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 653 = 1% variables out of 54841 scheduled
c [bca-8] limit of 10000000 steps and 633547 added (scaled 2)
c [bca-8] 94933 out of 108378 literals actually usable 88%
c [bca-8] added 23 blocked clauses in 227782 steps
c [phase-count-12] 315359 negative 99.7% of 316372 except 1013 0.3%
c [phase-count-12] 245542 positive 77.6% of 316372 except 70830 22.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-12] sorted 54188 enqueued variables after 27281 conflicts
c [score-dist-12] active 0 (0%), one 27331 (50%), zero 26857 (50%)
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 1114 variables 2.0% (54188 remain 17%)
c [simplification-12] removed 5983 irredundant clauses 1.9% (316372 remain 23%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 15666
c [simplification-12] penalized conflict interval 15666 = 1 * 15666
c [simplification-12] hard conflict limit 52947 (soft 42947 + delta 10000)
c [simplification-12] new conflict limit 42947 (hard 52947)
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   80.6   54187   316372     27296    6804   4028 120365   15   133   37  11%      2   92   12    6  212%
c i   80.7   54183   316372     27325    6827   4032 120366   15   133   38  11%      2   91   11    6  199%
c i   81.0   54177   316372     27700    7151   4054 120380   15   132   38  11%      2   90   10    6  184%
c i   81.1   54168   316372     27858    7282   4065 120386   14   132   38  11%      2   90   10    6  171%
c i   81.4   54166   316372     28232    7592   4095 120406   14   133   38  11%      2   90   12    6  213%
c i   81.4   54159   316372     28233    7592   4095 120406   14   133   38  11%      2   90   12    6  212%
c i   81.6   54154   316372     28589    7903   4118 120419   14   132   38  11%      2   89   13    6  222%
c i   81.7   54153   316372     28646    7951   4121 120422   14   133   38  11%      2   89   12    6  206%
c i   81.8   54149   316372     28793    8084   4127 120426   14   133   38  11%      2   90   14    6  244%
c i   82.0   54147   316372     28978    8244   4136 120439   14   134   38  10%      2   90   12    6  213%
c i   82.0   54142   316372     29029    8280   4142 120446   14   134   38  10%      2   90   11    6  192%
c i   82.0   54136   316372     29041    8288   4144 120447   14   134   38  10%      2   90   11    6  187%
c i   82.0   54134   316372     29045    8290   4145 120447   14   134   38  10%      2   90   11    6  184%
c i   82.1   54133   316372     29088    8316   4151 120452   14   135   38  10%      1   90   10    6  181%
c i   82.1   54116   316372     29096    8323   4151 120452   14   134   38  10%      1   90   10    6  178%
c i   82.3   54114   316372     29332    8528   4164 120464   14   136   38  10%      1   92   14    6  245%
c i   82.4   54113   316372     29546    8716   4171 120474   14   135   38  10%      1   91   16    6  279%
c i   82.5   54108   316372     29706    8858   4178 120483   14   134   38  10%      1   89   14    6  242%
c i   82.6   54106   316372     29830    8973   4179 120484   14   133   38  11%      1   88   14    6  236%
c i   82.8   54104   316372     30019    9137   4192 120493   14   135   38  10%      1   89   15    6  251%
c i   82.8   54102   316372     30055    9166   4195 120496   14   135   38  10%      1   90   14    6  237%
c i   82.8   54101   316372     30075    9185   4195 120496   14   136   38  10%      1   90   16    6  265%
c i   82.9   54100   316372     30171    9269   4200 120500   14   136   38  10%      1   90   15    6  258%
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   83.0   54094   316372     30244    9332   4203 120505   14   137   38  10%      1   91   15    6  250%
c i   83.2   54093   316372     30524    9567   4217 120522   14   136   38  11%      1   90   16    6  262%
c i   83.3   54092   316372     30727    9750   4224 120533   15   136   38  11%      1   90   16    6  269%
c i   83.3   54091   316372     30729    9751   4224 120533   15   136   38  11%      1   90   16    6  268%
c i   83.5   54090   316372     30856    9857   4236 120540   14   137   38  11%      1   91   14    6  242%
c i   83.6   54087   316372     31013    9998   4243 120546   15   138   39  11%      1   92   16    6  263%
c i   83.7   54078   316372     31117   10086   4246 120551   15   139   39  11%      1   92   16    6  271%
c i   83.8   54076   316372     31243   10202   4249 120555   15   139   39  11%      1   92   16    6  272%
c i   84.0   54071   316372     31497   10416   4265 120570   15   141   39  11%      1   94   19    6  306%
c i   84.1   54067   316372     31576   10479   4273 120577   15   140   39  11%      1   93   16    6  265%
c i   84.3   54064   316372     31864   10735   4288 120589   15   141   39  11%      1   93   16    6  254%
c i   84.5   54063   316372     31980   10838   4292 120594   15   140   39  11%      1   92   15    6  236%
c i   84.7   54060   316372     32243   11070   4307 120600   15   138   39  11%      1   90   14    6  229%
c i   84.8   54059   316372     32355   11168   4313 120606   15   140   39  11%      1   91   17    6  273%
c i   85.0   54045   316372     32627   11414   4316 120624   15   140   39  11%      1   91   19    6  298%
c i   85.3   54037   316372     32982   11733   4329 120637   16   141   39  11%      1   92   25    6  396%
c i   85.4   54036   316372     33109   11853   4331 120638   17   142   39  12%      1   92   27    6  416%
c i   85.4   54035   316372     33142   11879   4335 120640   17   143   39  12%      1   93   25    6  395%
c i   85.6   54029   316372     33235   11955   4342 120644   17   143   39  12%      1   93   24    6  368%
c i   85.7   54026   316372     33324   12029   4347 120650   17   145   39  12%      1   95   23    6  354%
c i   86.0   53951   316372     33733   12387   4367 120671   17   146   39  11%      2   96   18    7  271%
c i   86.1   53936   316372     33975   12610   4375 120674   17   145   39  12%      1   94   20    7  308%
c i   86.3   53923   316372     34137   12765   4378 120676   17   145   40  12%      1   94   23    7  345%
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   86.3   53919   316372     34146   12769   4380 120678   17   145   40  12%      1   94   22    7  334%
c i   86.3   53917   316372     34147   12769   4380 120678   17   145   40  12%      1   94   22    7  332%
c i   86.3   53905   316372     34183   12804   4380 120678   17   145   40  12%      1   93   23    7  339%
c i   86.7   53878   316372     34593   13151   4407 120698   17   142   40  12%      2   90   17    7  250%
c i   86.7   53877   316372     34620   13173   4408 120698   17   141   40  12%      2   90   16    7  243%
c i   86.8   53875   316372     34741   13285   4411 120702   17   140   40  12%      1   88   19    7  277%
c i   87.0   53874   316372     34936   13455   4422 120711   18   143   40  13%      1   91   25    7  364%
c i   87.2   53873   316372     35178   13666   4434 120719   18   144   40  12%      1   91   22    7  315%
c i   87.6   53869   316372     35673   14104   4449 120742   18   144   41  13%      2   91   24    7  348%
c i   87.7   53861   316372     35738   14161   4451 120747   18   144   41  13%      2   91   22    7  312%
c i   87.7   53857   316372     35740   14161   4451 120748   18   144   41  13%      2   91   22    7  309%
c i   87.9   53851   316372     35916   14325   4455 120749   19   145   41  13%      2   91   30    7  420%
c i   88.0   53850   316372     36012   14405   4460 120750   19   145   41  13%      2   91   26    7  367%
c i   88.1   53849   316372     36092   14475   4463 120751   20   147   41  13%      1   93   35    7  489%
c i   88.1   53848   316372     36173   14545   4469 120754   20   147   41  14%      1   93   31    7  439%
c i   88.5   53843   316372     36524   14859   4482 120775   20   149   41  14%      2   94   28    7  390%
c i   88.5   53842   316372     36525   14859   4482 120775   20   148   41  14%      2   94   28    7  389%
c i   88.5   53841   316372     36527   14859   4482 120776   20   148   41  14%      2   94   28    7  386%
c i   88.7   53840   316372     36737   15061   4486 120778   20   151   41  13%      1   96   23    7  312%
c i   88.7   53833   316372     36740   15063   4486 120778   20   151   41  13%      1   96   23    7  310%
c i   88.8   53829   316372     36777   15092   4490 120780   20   151   41  13%      1   96   22    7  296%
c i   88.9   53819   316372     36867   15167   4494 120785   20   150   41  14%      1   95   26    7  354%
c i   89.2   53818   316372     37114   15377   4510 120799   21   153   41  14%      1   98   28    7  375%
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   89.2   53817   316372     37140   15397   4513 120800   21   153   41  14%      1   98   26    7  357%
c i   89.3   53814   316372     37254   15501   4515 120805   21   153   41  14%      1   98   25    7  331%
c i   89.4   53801   316372     37357   15595   4521 120806   21   153   42  14%      1   97   23    7  308%
c i   89.7   53799   316372     37743   15941   4537 120814   21   152   42  14%      1   95   18    7  237%
c i   89.7   53789   316372     37744   15941   4537 120814   20   152   42  14%      1   95   18    7  236%
c i   89.9   53787   316372     37961   16146   4541 120817   21   151   42  14%      1   95   20    8  261%
c i   90.1   53759   316372     38117   16275   4553 120827   20   151   42  13%      1   95   17    8  231%
c i   90.1   53758   316372     38128   16284   4553 120828   20   151   42  13%      1   95   18    8  232%
c i   90.1   53750   316372     38142   16293   4555 120830   20   151   42  13%      1   94   17    8  224%
c i   90.3   53740   316372     38285   16419   4557 120833   20   150   42  13%      1   93   16    8  206%
c i   91.3   53729   316372     39285   17341   4590 120858   22   154   42  14%      5   96   26    8  334%
c i   91.9   53726   316372     39785   17790   4601 120872   24   157   42  16%      5   98   47    8  576%
c i   92.3   53723   316372     40108   18079   4609 120886   25   157   43  16%      4   98   42    8  506%
c i   92.6   53722   316372     40432   18374   4618 120893   27   159   43  17%      3   99   40    8  472%
c i   92.6   53718   316372     40455   18391   4619 120897   27   159   43  17%      3   99   38    8  450%
c i   92.9   53715   316372     40707   18610   4632 120903   26   157   43  17%      3   97   26    8  300%
c i   92.9   53683   316372     40739   18634   4633 120906   26   157   43  17%      3   96   23    8  273%
c i   93.3   53678   316372     41178   19016   4658 120925   25   153   43  17%      3   91   19    9  227%
c i   93.3   53665   316372     41179   19016   4658 120925   25   153   43  17%      3   91   19    9  226%
c i   93.5   53649   316372     41432   19251   4664 120930   26   152   43  17%      2   91   26    9  305%
c i   93.6   53647   316372     41439   19256   4664 120931   26   152   43  17%      2   91   26    9  299%
c i   93.6   53645   316372     41536   19344   4665 120931   26   153   43  17%      2   92   35    9  398%
c i   93.9   53643   316372     41767   19552   4673 120938   27   153   43  17%      2   91   31    9  357%
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.9   53626   316372     41780   19563   4674 120938   26   153   43  17%      2   91   31    9  353%
c i   94.0   53625   316372     41905   19679   4677 120942   26   153   44  17%      2   91   28    9  320%
c i   94.1   53610   316372     41966   19736   4677 120944   26   153   44  17%      1   91   27    9  309%
c i   94.1   53609   316372     41967   19736   4677 120944   26   153   44  17%      1   91   27    9  308%
c i   94.1   53607   316372     41979   19747   4677 120944   26   153   44  17%      1   91   28    9  314%
c i   94.1   53591   316372     41981   19747   4678 120944   26   153   44  17%      1   91   28    9  312%
c i   94.6   53576   316372     42349   20086   4688 120956   27   154   45  18%      2   91   35    9  387%
c i   94.9   53559   316372     42661   20364   4703 120969   27   154   45  17%      2   91   27    9  294%
c 
c [simplification-13] limit of 373 iterations hit after 373 iterations
c [quatres-9] found 32113 quaternary clauses 69% in total
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 5 single-self-subsuming ternary resolvents
c [quatres-9-2] added 25 quaternary resolvents
c [ternres-9] limit 10826975 with penalty 0 = 0 + 0
c [ternres-9] all 53558 free variables schedulable
c [ternres-9] 866 ternary resolvents (1 bin, 865 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 820 variables
c [basicprobe-5] limit 54134876 penalty 0 = 0 + 0
c [basicprobe-5-0] 10145 probes remain 19% after last round
c [basicprobe-5-0] 469 units = 461 failed (98%) + 8 lifted (2%)
c [basicprobe-5-0] removed 1104 variables, found 77701 hbrs
c [bate-3] eliminated 432 asymmetric tautologies during probing
c [unhide-13] limit 2165395 with penalty 0 = 0 + 0
c [unhide-13-14] 23 units, 430 failed, 20262 tauts, 0 hbrs, 62672 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 194 transitive binary clauses
c [transred-9] found 2 units
c [cce-6] limit of 27067438 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 17 (6%) of length 7
c [cce-6-1] eliminated 10 clauses out of 957 (1%) of length 6
c [cce-6-1] eliminated 193 clauses out of 8200 (2%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 204 large clauses in 27067439 steps
c [cce-6-1] allowing another 13533719 steps for small clauses
c [cce-6-1] scheduling 218340 clauses = 149113 binary + 69227 ternary
c [cce-6-1] tried to eliminate 555 small clauses 0%
c [cce-6-1] eliminated 86 binary clauses 0%
c [cce-6-1] eliminated 77 ternary clauses 0%
c [cce-6-1] eliminated 163 small clauses 0%
c [cce-6-1] eliminated 3759 small clauses in 27067439 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 3963 covered clauses in round 1
c [cce-6] eliminated 3963 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 51582 variables 100%
c [elim-12] limit of 216539504 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 2376 variables 5% in round 1 in 23363938 steps
c [elim-12-1] backward subsumption/strengthening limit 23363900
c [elim-12-1-1] backward checking 10270 touched variables 20%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 128 and strengthened 143 clauses in 2212828 steps
c [elim-12-1] rescheduled 712 variables 1% by backward subsumption
c [elim-12-2] eliminated 50 variables 0% in round 2 in 1331979 steps
c [elim-12-2] backward subsumption/strengthening limit 1331900
c [elim-12-2-1] backward checking 482 touched variables 1%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 57 and strengthened 58 clauses in 196269 steps
c [elim-12-2] rescheduled 220 variables 0% by backward subsumption
c [elim-12-3] eliminated 15 variables 0% in round 3 in 156414 steps
c [elim-12-3] backward subsumption/strengthening limit 156400
c [elim-12-3-1] backward checking 142 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 5 and strengthened 9 clauses in 97311 steps
c [elim-12] incomplete 36 not tried 0% in round 3
c [gc-91] reconnected 170229 binary clauses (produced 0 empty 1 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 2455 = 5% variables out of 51582 scheduled
c [bca-9] limit of 10000000 steps and 573497 added (scaled 2)
c [bca-9] 79290 out of 98256 literals actually usable 81%
c [bca-9] added 35 blocked clauses in 197928 steps
c [sweep-8] limit 1624046 penalty 1 = 1 + 0
c [sweep-8-1] 3404 pos 7.2% + 43740 neg 92.8% = 47144 sched 96.0% ret 1983
c [sweep-8-1] 1696210 steps 31 queries 7627.35 avg class size
c [sweep-8-1] 166 decisions 25 SAT calls 37.48 avg env size
c [sweep-8-1] 46908 variables remain 96% (2186 retained 4%)
c [decomp-31] removed 198 variables
c [sweep-8-1] removed 198 vars (0 failed, 5 eqs, 7 impls)
c [sweep-8] removed 198 vars in TOTAL (1 rounds, 30 queries)
c [phase-count-13] 285012 negative 99.7% of 285977 except 965 0.3%
c [phase-count-13] 220006 positive 76.9% of 285977 except 65971 23.1%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-13] sorted 48929 enqueued variables after 42661 conflicts
c [score-dist-13] active 0 (0%), one 27658 (57%), zero 21271 (43%)
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 4629 variables 8.6% (48929 remain 16%)
c [simplification-13] removed 30395 irredundant clauses 9.6% (285977 remain 21%)
c [simplification-13] maximum reduction of 10% = max (9%, 10%)
c [simplification-13] forced so keeping old conflict interval 15666
c [simplification-13] conflict limit remains at 43035 (hard 52947)
c [simplification-13] 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  101.2   48928   285977     42746   17513   4553 161559   27   155   43  18%      1   91   32    9  349%
c 
c [simplification-14] limit 43035 conflicts (hard 52947) hit after 43037 conflicts
c [quatres-10] found 28304 quaternary clauses 67% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [quatres-10-2] added 12 single-self-subsuming ternary resolvents
c [quatres-10-2] added 65 quaternary resolvents
c [ternres-10] limit 10923073 with penalty 0 = 0 + 0
c [ternres-10] all 48927 free variables schedulable
c [ternres-10] 1630 ternary resolvents (7 bin, 1623 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 273076 penalty 3 = 3 + 0
c [gauss-4] extracted 9 xors of average arity 3.0
c [gauss-4] connected 27 occurrences of 27 variables (average 1.0)
c [gauss-4] limit 273076 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 48927 free variables schedulable
c [simpleprobe-6] limit 43692294 penalty 0 = 0 + 0
c [decomp-33] removed 827 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 827 variables, found 28066 hbrs, 275 units
c [unhide-14] limit 2184614 with penalty 0 = 0 + 0
c [unhide-14-16] 6 units, 105 failed, 21886 tauts, 0 hbrs, 33173 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 189 transitive binary clauses
c [transred-10] found 1 units
c [cce-7] limit of 54615367 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 79
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 78
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 76
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 74
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 72
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 70
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 69
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 68
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 67
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 66
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 65
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 64
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 63
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 62
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 61
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 60
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 59
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 58
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 56
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 54
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 53
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 52
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 51
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 50
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 49
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 48
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 47
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 46
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 45
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 44
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 43
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 42
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 41
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 40
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 37
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 36
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 33
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 32
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 28
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 26
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 24
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 23
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 22
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 20
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 19
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 18
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 17
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 16
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 15
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 14
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 13
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 12
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 11
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 10
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 9
c [cce-7-1] eliminated 6 clauses out of 13 (46%) of length 8
c [cce-7-1] eliminated 4 clauses out of 26 (15%) of length 7
c [cce-7-1] eliminated 13 clauses out of 967 (1%) of length 6
c [cce-7-1] eliminated 622 clauses out of 7918 (8%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 779 large clauses in 54615368 steps
c [cce-7-1] allowing another 27307684 steps for small clauses
c [cce-7-1] scheduling 176718 clauses = 139945 binary + 36773 ternary
c [cce-7-1] tried to eliminate 1407 small clauses 1%
c [cce-7-1] eliminated 259 binary clauses 0%
c [cce-7-1] eliminated 108 ternary clauses 0%
c [cce-7-1] eliminated 367 small clauses 0%
c [cce-7-1] eliminated 507 small clauses in 54615370 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1286 covered clauses in round 1
c [cce-7] eliminated 1286 covered clauses in TOTAL during 1 rounds
c [cce-7] 1286 < 1/100 * 275954 = 2759 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 47899 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1201 variables 3% in round 1 in 22215610 steps
c [elim-13-1] backward subsumption/strengthening limit 22215600
c [elim-13-1-1] backward checking 5756 touched variables 12%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 72 and strengthened 106 clauses in 1563845 steps
c [elim-13-1] rescheduled 415 variables 1% by backward subsumption
c [elim-13-2] eliminated 35 variables 0% in round 2 in 1802011 steps
c [elim-13-2] backward subsumption/strengthening limit 1802000
c [elim-13-2-1] backward checking 285 touched variables 1%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 28 and strengthened 20 clauses in 198271 steps
c [elim-13-2] rescheduled 99 variables 0% by backward subsumption
c [elim-13-3] eliminated 10 variables 0% in round 3 in 193341 steps
c [elim-13-3] backward subsumption/strengthening limit 193300
c [elim-13-3-1] backward checking 92 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 3 and strengthened 1 clauses in 78717 steps
c [elim-13] incomplete 13 not tried 0% in round 3
c [gc-101] reconnected 166244 binary clauses (produced 0 empty 1 units)
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 1253 = 3% variables out of 47899 scheduled
c [bca-10] limit of 10000000 steps and 543338 added (scaled 2)
c [bca-10] 74717 out of 93294 literals actually usable 80%
c [bca-10] added 22 blocked clauses in 186080 steps
c [sweep-9] limit 3276922 penalty 0 = 0 + 0
c [sweep-9-1] 3337 pos 7.5% + 41269 neg 92.5% = 44606 sched 95.6% ret 2040
c [sweep-9-1] 3340996 steps 34 queries 7401.56 avg class size
c [sweep-9-1] 682 decisions 30 SAT calls 96.00 avg env size
c [sweep-9-1] 44291 variables remain 95% (2349 retained 5%)
c [decomp-34] removed 30 variables
c [sweep-9-1] removed 30 vars (0 failed, 4 eqs, 6 impls)
c [sweep-9] 30 < 1/1000 * 46646 = 46 considered unsuccessful
c [sweep-9] removed 30 vars in TOTAL (1 rounds, 33 queries)
c [phase-count-14] 270367 negative 99.7% of 271148 except 781 0.3%
c [phase-count-14] 207537 positive 76.5% of 271148 except 63611 23.5%
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 46616 enqueued variables after 43037 conflicts
c [score-dist-14] active 0 (0%), one 26871 (58%), zero 19745 (42%)
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 2311 variables 4.7% (46616 remain 15%)
c [simplification-14] removed 14829 irredundant clauses 5.2% (271148 remain 20%)
c [simplification-14] maximum reduction of 5% = max (5%, 5%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 55037 (soft 45037 + delta 10000)
c [simplification-14] new conflict limit 45037 (hard 55037)
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  107.6   46615   271148     43646   17433   5213 162661   27   149   42  18%      5   84   31    9  332%
c i  107.6   46613   271148     43647   17433   5213 162661   27   149   42  18%      5   84   31    9  331%
c i  107.8   46611   271148     43841   17614   5220 162663   28   149   42  19%      4   84   34    9  355%
c i  108.0   46610   271148     44010   17762   5227 162670   27   150   42  18%      3   85   27    9  280%
c i  108.1   46609   271148     44121   17862   5229 162672   27   150   42  18%      3   84   26   10  276%
c i  108.2   46606   271148     44274   18009   5230 162674   27   149   42  18%      3   83   25   10  266%
c 
c [simplification-15] limit 45047 conflicts (hard 55037) hit after 45047 conflicts
c [quatres-11] found 26589 quaternary clauses 66% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 9 single-self-subsuming ternary resolvents
c [quatres-11-2] added 21 quaternary resolvents
c [ternres-11] limit 11423856 with penalty 0 = 0 + 0
c [ternres-11] all 46604 free variables schedulable
c [ternres-11] 1026 ternary resolvents (3 bin, 1023 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 356995 penalty 4 = 4 + 0
c [card-5] found 980 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 356995 for elimination
c [card-5] 980 out of 980 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 42 variables
c [treelook-6] limit 1142385 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 75335 literals 81%
c [treelook-6] scheduling used 1002949 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1142385 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1223367 steps
c [treelook-6] 75304 literals remain 81%
c [treelook-6] 12787 variables remain to probed next time 27%
c [treelook-6] removed 0 variables, found 8907 hbrs
c [unhide-15] limit 2284771 with penalty 0 = 0 + 0
c [unhide-15-18] 5 units, 93 failed, 13419 tauts, 0 hbrs, 28379 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 165 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 46318 variables 100%
c [block-5] limit of 14279820 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 237 blocked clauses
c [block-5] 237 < 1/100 * 269103 = 2691 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 46317 variables 100%
c [elim-14] limit of 228477135 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 607 variables 1% in round 1 in 21293962 steps
c [elim-14-1] backward subsumption/strengthening limit 21293900
c [elim-14-1-1] backward checking 3272 touched variables 7%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 48 and strengthened 41 clauses in 831949 steps
c [elim-14-1] rescheduled 228 variables 0% by backward subsumption
c [elim-14-2] eliminated 12 variables 0% in round 2 in 228351 steps
c [elim-14-2] backward subsumption/strengthening limit 228300
c [elim-14-2-1] backward checking 91 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 4 and strengthened 2 clauses in 73787 steps
c [elim-14-2] rescheduled 15 variables 0% by backward subsumption
c [elim-14-3] eliminated 1 variables 0% in round 3 in 7169 steps
c [elim-14-3] backward subsumption/strengthening limit 7100
c [elim-14-3-1] backward checking 8 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 7101 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 626 = 1% variables out of 46317 scheduled
c [bca-11] limit of 10000000 steps and 530965 added (scaled 2)
c [bca-11] 72400 out of 91384 literals actually usable 79%
c [bca-11] added 24 blocked clauses in 182647 steps
c [phase-count-15] 264297 negative 99.7% of 265061 except 764 0.3%
c [phase-count-15] 202055 positive 76.2% of 265061 except 63006 23.8%
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 45691 enqueued variables after 45047 conflicts
c [score-dist-15] active 0 (0%), one 26810 (59%), zero 18881 (41%)
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 913 variables 2.0% (45691 remain 15%)
c [simplification-15] removed 6087 irredundant clauses 2.2% (265061 remain 19%)
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 22332
c [simplification-15] penalized conflict interval 22332 = 1 * 22332
c [simplification-15] hard conflict limit 78545 (soft 67379 + delta 11166)
c [simplification-15] new conflict limit 67379 (hard 78545)
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  112.5   45690   265061     45525   18912   5574 157251   26   148   42  18%      8   81   22   10  222%
c i  113.3   45689   265061     46389   19689   5607 157268   27   145   42  19%      7   77   34   10  336%
c i  113.3   45684   265061     46390   19689   5607 157268   27   145   42  19%      7   76   34   10  335%
c i  113.3   45663   265061     46455   19744   5612 157271   27   144   42  19%      7   76   31   10  310%
c i  113.6   45572   265061     46706   19977   5617 157279   27   143   42  19%      5   74   28   10  272%
c i  113.6   45571   265061     46713   19982   5617 157280   27   143   42  19%      5   74   27   10  267%
c i  113.9   45568   265061     47046   20288   5628 157290   27   140   42  19%      4   71   25   10  246%
c i  114.0   45567   265061     47125   20361   5629 157291   27   140   42  19%      4   71   26   10  256%
c i  114.2   45566   265061     47344   20561   5635 157298   27   138   42  19%      3   69   26   10  252%
c i  114.7   45563   265061     47966   21144   5653 157311   27   139   42  19%      4   69   26   10  248%
c i  115.2   45560   265061     48459   21611   5663 157315   27   137   42  20%      3   66   29   11  272%
c i  116.1   45559   265061     49561   22590   5692 157340   27   128   42  21%      7   57   28   11  257%
c i  116.1   45386   265061     49630   22654   5694 157340   27   128   42  21%      6   57   27   11  252%
c i  116.2   45385   265061     49743   22755   5697 157345   27   128   42  21%      6   57   33   11  307%
c i  116.3   45384   265061     49825   22829   5703 157345   27   129   42  21%      5   57   32   11  289%
c i  116.7   45383   265061     50341   23295   5710 157355   27   128   42  21%      4   56   30   11  273%
c i  117.3   45379   265061     51174   24070   5719 157369   30   135   44  22%      5   62   34   11  296%
c i  117.5   45374   265061     51497   24369   5724 157372   30   135   44  22%      4   62   32   12  281%
c i  118.4   45367   265061     52545   25324   5752 157393   31   137   44  23%      6   63   28   12  232%
c i  118.5   45366   265061     52705   25475   5756 157397   31   137   44  23%      5   63   30   12  249%
c i  118.5   45363   265061     52741   25507   5757 157398   31   137   44  23%      5   63   30   12  252%
c i  118.6   45362   265061     52796   25560   5758 157398   31   136   44  22%      5   62   27   12  222%
c i  118.6   45361   265061     52816   25577   5759 157398   31   136   44  23%      5   62   26   12  220%
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   45358   265061     52881   25636   5762 157399   31   135   44  23%      4   61   26   12  219%
c i  118.7   45357   265061     52882   25636   5762 157399   31   135   44  23%      4   61   26   12  218%
c i  118.8   45355   265061     52982   25723   5762 157401   31   136   44  23%      4   61   34   12  280%
c i  118.9   45353   265061     53149   25872   5768 157405   31   137   44  23%      3   62   37   12  303%
c i  119.3   45352   265061     53693   26364   5782 157420   32   140   44  23%      3   65   44   12  357%
c i  120.0   45342   265061     54532   27129   5803 157438   33   137   45  24%      5   61   36   13  284%
c i  120.0   45336   265061     54533   27129   5803 157438   33   137   45  24%      5   61   36   13  283%
c i  120.2   45315   265061     54757   27340   5805 157442   32   136   45  24%      4   60   32   13  256%
c i  121.5   45229   265061     56332   28782   5833 157466   34   137   47  25%     11   60   34   13  252%
c i  121.7   45228   265061     56613   29044   5839 157471   34   134   48  25%      9   57   28   13  213%
c i  123.0   45227   265061     58183   30467   5875 157500   35   134   49  26%     12   55   52   14  374%
c i  123.4   45226   265061     58652   30893   5883 157510   35   134   49  26%      8   54   38   14  273%
c i  123.4   45225   265061     58676   30912   5884 157511   35   133   49  26%      8   54   36   14  254%
c i  123.4   45190   265061     58677   30912   5884 157511   35   133   49  26%      8   54   35   14  253%
c i  123.4   45189   265061     58699   30924   5890 157512   35   133   49  26%      8   53   33   14  235%
c i  123.8   45188   265061     59067   31277   5893 157514   35   133   50  26%      6   53   38   14  265%
c i  125.0   45186   265061     60615   32693   5926 157539   36   134   52  27%     11   53   38   15  256%
c i  125.7   45183   265061     61458   33457   5947 157560   37   137   52  27%      8   55   46   15  304%
c i  126.0   45178   265061     61726   33705   5951 157562   37   137   52  27%      6   55   47   15  312%
c i  126.0   45176   265061     61805   33778   5951 157563   37   136   52  27%      5   54   40   15  261%
c i  126.0   45175   265061     61806   33778   5951 157563   37   136   52  27%      5   54   39   15  260%
c i  126.2   45174   265061     62079   34021   5962 157570   37   137   52  27%      4   54   40   15  265%
c i  126.3   45163   265061     62136   34075   5962 157571   37   136   52  27%      4   54   36   15  239%
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.9   45154   265061     62867   34728   5975 157581   40   140   52  29%      4   57   62   16  392%
c i  128.1   45153   265061     64278   36028   5998 157605   41   136   52  30%      9   52   36   16  218%
c i  129.2   45151   265061     65492   37157   6018 157612   40   134   52  30%      9   49   32   17  192%
c i  129.7   45138   265061     65997   37612   6025 157616   41   132   52  31%      6   47   44   17  258%
c i  130.1   45135   265061     66524   38098   6033 157625   40   133   53  30%      4   47   36   17  211%
c 
c [simplification-16] limit 67430 conflicts (hard 78545) hit after 67430 conflicts
c [quatres-12] found 25196 quaternary clauses 63% in total
c [quatres-12-2] added 5 single-self-subsuming ternary resolvents
c [quatres-12-2] added 22 quaternary resolvents
c [ternres-12] limit 16639258 with penalty 0 = 0 + 0
c [ternres-12] all 45111 free variables schedulable
c [ternres-12] 540 ternary resolvents (0 bin, 540 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-37] removed 702 variables
c [basicprobe-6] limit 83196291 penalty 0 = 0 + 0
c [basicprobe-6-0] 5088 probes remain 12% after last round
c [basicprobe-6-0] 604 units = 590 failed (98%) + 14 lifted (2%)
c [basicprobe-6-0] removed 1623 variables, found 96388 hbrs
c [bate-4] eliminated 582 asymmetric tautologies during probing
c [unhide-16] limit 3327851 with penalty 0 = 0 + 0
c [unhide-16-20] 9 units, 240 failed, 22628 tauts, 0 hbrs, 195534 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 246 transitive binary clauses
c [transred-12] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 415981455 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 23
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 19
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 17
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 16
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 15
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 14
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 12
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 11
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 10
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 9
c [cce-8-1] eliminated 6 clauses out of 15 (40%) of length 8
c [cce-8-1] eliminated 1 clauses out of 23 (4%) of length 7
c [cce-8-1] eliminated 6 clauses out of 901 (1%) of length 6
c [cce-8-1] eliminated 376 clauses out of 6818 (6%) of length 5
c [cce-8-1] eliminated 9001 clauses out of 21458 (42%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 9423 large clauses in 252039756 steps
c [cce-8-1] allowing another 126019878 steps for small clauses
c [cce-8-1] scheduling 158054 clauses = 127542 binary + 30512 ternary
c [cce-8-1] tried to eliminate 22778 small clauses 14%
c [cce-8-1] eliminated 3872 binary clauses 3%
c [cce-8-1] eliminated 1609 ternary clauses 5%
c [cce-8-1] eliminated 5481 small clauses 3%
c [cce-8-1] eliminated 5984 small clauses in 415981460 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 15407 covered clauses in round 1
c [cce-8] eliminated 15407 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 42934 variables 100%
c [elim-15] limit of 332785166 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 4032 variables 9% in round 1 in 16547121 steps
c [elim-15-1] backward subsumption/strengthening limit 16547100
c [elim-15-1-1] backward checking 14866 touched variables 35%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 99 and strengthened 247 clauses in 2467265 steps
c [elim-15-1] rescheduled 826 variables 2% by backward subsumption
c [elim-15-2] eliminated 41 variables 0% in round 2 in 860317 steps
c [elim-15-2] backward subsumption/strengthening limit 860300
c [elim-15-2-1] backward checking 460 touched variables 1%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 19 and strengthened 22 clauses in 222941 steps
c [elim-15-2] rescheduled 94 variables 0% by backward subsumption
c [elim-15-3] eliminated 7 variables 0% in round 3 in 506090 steps
c [elim-15-3] backward subsumption/strengthening limit 506000
c [elim-15-3-1] backward checking 76 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 4 and strengthened 0 clauses in 82568 steps
c [elim-15] incomplete 10 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 4081 = 10% variables out of 42934 scheduled
c [bca-12] limit of 10000000 steps and 435393 added (scaled 2)
c [bca-12] 59182 out of 77708 literals actually usable 76%
c [bca-12] added 92 blocked clauses in 152113 steps
c [sweep-10] limit 2495888 penalty 1 = 1 + 0
c [sweep-10-1] 2894 pos 7.8% + 34205 neg 92.2% = 37099 sched 95.5% ret 1754
c [sweep-10-1] 2558209 steps 54 queries 4473.41 avg class size
c [sweep-10-1] 1095 decisions 47 SAT calls 97.30 avg env size
c [sweep-10-1] 36395 variables remain 94% (2413 retained 6%)
c [decomp-38] removed 88 variables
c [sweep-10-1] removed 88 vars (0 failed, 6 eqs, 6 impls)
c [sweep-10] removed 88 vars in TOTAL (1 rounds, 53 queries)
c [phase-count-16] 216388 negative 99.7% of 216964 except 576 0.3%
c [phase-count-16] 161316 positive 74.4% of 216964 except 55648 25.6%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-16] sorted 38765 enqueued variables after 67430 conflicts
c [score-dist-16] active 0 (0%), one 25267 (65%), zero 13498 (35%)
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 6346 variables 14.1% (38765 remain 12%)
c [simplification-16] removed 48097 irredundant clauses 18.1% (216964 remain 16%)
c [simplification-16] maximum reduction of 18% = max (14%, 18%)
c [simplification-16] large reduction 18% >= 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 79430 (soft 69430 + delta 10000)
c [simplification-16] new conflict limit 69430 (hard 79430)
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  149.0   38764   216964     68020   23285   6350 195953   39   129   43  30%     10   42   22   18  124%
c i  149.1   38763   216964     68192   23444   6355 195957   38   129   43  30%      8   42   21   18  121%
c i  149.4   38762   216964     68678   23902   6360 195958   36   125   43  29%      5   37   18   18  102%
c i  149.8   38760   216964     69357   24540   6370 195965   37   121   43  31%      4   34   35   18  197%
c 
c [simplification-17] limit 69430 conflicts (hard 79430) hit after 69430 conflicts
c [quatres-13] found 15927 quaternary clauses 54% in total
c [quatres-13-1] removed 3 duplicate quaternary clauses
c [quatres-13-2] added 3 single-self-subsuming ternary resolvents
c [quatres-13-2] added 23 quaternary resolvents
c [ternres-13] limit 17003617 with penalty 0 = 0 + 0
c [ternres-13] all 38760 free variables schedulable
c [ternres-13] 1841 ternary resolvents (11 bin, 1830 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-39] removed 7 variables
c [simpleprobe-7] all 38758 free variables schedulable
c [simpleprobe-7] limit 68014469 penalty 0 = 0 + 0
c [decomp-40] removed 525 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 525 variables, found 31028 hbrs, 115 units
c [unhide-17] limit 3400723 with penalty 0 = 0 + 0
c [unhide-17-23] 4 units, 33 failed, 23106 tauts, 0 hbrs, 62607 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 385 transitive binary clauses
c [cce-9] limit of 85018087 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 74
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 65
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 62
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 61
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 60
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 59
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 58
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 57
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 55
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 53
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 52
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 51
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 50
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 49
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 48
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 47
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 46
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 45
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 44
c [cce-9-1] eliminated 3 clauses out of 3 (100%) of length 43
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 42
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 41
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 40
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 38
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 37
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 36
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 35
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 34
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 33
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 31
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 29
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 27
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 25
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 24
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 23
c [cce-9-1] eliminated 4 clauses out of 4 (100%) of length 22
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 21
c [cce-9-1] eliminated 4 clauses out of 4 (100%) of length 20
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 19
c [cce-9-1] eliminated 4 clauses out of 5 (80%) of length 18
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 17
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 16
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 15
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 14
c [cce-9-1] eliminated 5 clauses out of 8 (62%) of length 13
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 12
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 11
c [cce-9-1] eliminated 5 clauses out of 12 (42%) of length 10
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 9
c [cce-9-1] eliminated 10 clauses out of 23 (43%) of length 8
c [cce-9-1] eliminated 7 clauses out of 37 (19%) of length 7
c [cce-9-1] eliminated 38 clauses out of 971 (4%) of length 6
c [cce-9-1] eliminated 175 clauses out of 6592 (3%) of length 5
c [cce-9-1] eliminated 4 clauses out of 13773 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 352 large clauses in 85018088 steps
c [cce-9-1] allowing another 42509044 steps for small clauses
c [cce-9-1] scheduling 160609 clauses = 112716 binary + 47893 ternary
c [cce-9-1] tried to eliminate 3309 small clauses 2%
c [cce-9-1] eliminated 536 binary clauses 0%
c [cce-9-1] eliminated 296 ternary clauses 1%
c [cce-9-1] eliminated 832 small clauses 1%
c [cce-9-1] eliminated 832 small clauses in 85018089 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1184 covered clauses in round 1
c [cce-9] eliminated 1184 covered clauses in TOTAL during 1 rounds
c [cce-9] 1184 < 1/100 * 209628 = 2096 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 38072 variables 100%
c [elim-16] limit of 340072349 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 803 variables 2% in round 1 in 14992069 steps
c [elim-16-1] backward subsumption/strengthening limit 14992000
c [elim-16-1-1] backward checking 4790 touched variables 13%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 25 and strengthened 37 clauses in 945383 steps
c [elim-16-1] rescheduled 180 variables 0% by backward subsumption
c [elim-16-2] eliminated 8 variables 0% in round 2 in 463460 steps
c [elim-16-2] backward subsumption/strengthening limit 463400
c [elim-16-2-1] backward checking 114 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 3 and strengthened 2 clauses in 84389 steps
c [elim-16-2] rescheduled 10 variables 0% by backward subsumption
c [elim-16-3] no variable eliminated in round 3 in 3759 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 811 = 2% variables out of 38072 scheduled
c [bca-13] limit of 10000000 steps and 415075 added (scaled 2)
c [bca-13] 55831 out of 74524 literals actually usable 75%
c [bca-13] added 72 blocked clauses in 145966 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 51010850 penalty 0 = 0 + 0
c [sweep-11-1] 2707 pos 7.7% + 32327 neg 92.3% = 35034 sched 94.0% ret 2227
c [sweep-11-1] 51204196 steps 1071 queries 225.69 avg class size
c [sweep-11-1] 11805 decisions 917 SAT calls 84.66 avg env size
c [sweep-11-1] 17546 variables remain 48% (19348 retained 52%)
c [decomp-41] removed 697 variables
c [sweep-11-1] removed 697 vars (0 failed, 182 eqs, 215 impls)
c [sweep-11] removed 697 vars in TOTAL (1 rounds, 1070 queries)
c [phase-count-17] 203676 negative 99.7% of 204238 except 562 0.3%
c [phase-count-17] 150412 positive 73.6% of 204238 except 53826 26.4%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-17] sorted 36564 enqueued variables after 69430 conflicts
c [score-dist-17] active 0 (0%), one 25471 (70%), zero 11093 (30%)
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 2196 variables 5.7% (36564 remain 12%)
c [simplification-17] removed 12726 irredundant clauses 5.9% (204238 remain 15%)
c [simplification-17] maximum reduction of 6% = max (6%, 6%)
c [simplification-17] large reduction 6% >= 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 81430 (soft 71430 + delta 10000)
c [simplification-17] new conflict limit 71430 (hard 81430)
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  159.2   36563   204238     70582   25625   7141 210320   36   118   44  30%      7   29   33   18  185%
c i  159.6   36548   204238     71145   26142   7153 210331   34   114   44  30%      5   25   28   18  157%
c 
c [simplification-18] limit 71430 conflicts (hard 81430) hit after 71430 conflicts
c [quatres-14] found 15109 quaternary clauses 53% in total
c [quatres-14-1] removed 2 duplicate quaternary clauses
c [quatres-14-2] added 4 single-self-subsuming ternary resolvents
c [quatres-14-2] added 8 quaternary resolvents
c [ternres-14] limit 17374545 with penalty 0 = 0 + 0
c [ternres-14] all 36548 free variables schedulable
c [ternres-14] 1257 ternary resolvents (10 bin, 1247 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-42] removed 25 variables
c [unhide-18] limit 3474909 with penalty 0 = 0 + 0
c [unhide-18-26] 7 units, 186 failed, 20854 tauts, 0 hbrs, 36788 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 293 transitive binary clauses
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 36159 variables 100%
c [elim-17] limit of 347490917 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 573 variables 2% in round 1 in 14391591 steps
c [elim-17-1] backward subsumption/strengthening limit 14391500
c [elim-17-1-1] backward checking 3254 touched variables 9%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 34 and strengthened 27 clauses in 653520 steps
c [elim-17-1] rescheduled 176 variables 0% by backward subsumption
c [elim-17-2] eliminated 11 variables 0% in round 2 in 82567 steps
c [elim-17-2] backward subsumption/strengthening limit 82500
c [elim-17-2-1] backward checking 112 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 8 and strengthened 5 clauses in 50089 steps
c [elim-17-2] rescheduled 26 variables 0% by backward subsumption
c [elim-17-3] eliminated 1 variables 0% in round 3 in 12984 steps
c [elim-17-3] backward subsumption/strengthening limit 12900
c [elim-17-3-1] backward checking 10 touched variables 0%
c [elim-17-3-1] incomplete backward checking 0 remain 0%
c [elim-17-3] subsumed 1 and strengthened 0 clauses in 12901 steps
c [elim-17] incomplete 2 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 586 = 2% variables out of 36159 scheduled
c [bca-14] limit of 10000000 steps and 397503 added (scaled 2)
c [bca-14] 51692 out of 71148 literals actually usable 73%
c [bca-14] added 33 blocked clauses in 136824 steps
c [sweep-12] limit 5212363 penalty 0 = 0 + 0
c [sweep-12-1] 1734 pos 10.2% + 15337 neg 89.8% = 17071 sched 48.0% ret 18502
c [sweep-12-1] 5334683 steps 131 queries 1271.15 avg class size
c [sweep-12-1] 1946 decisions 121 SAT calls 95.42 avg env size
c [sweep-12-1] 16247 variables remain 46% (19324 retained 54%)
c [decomp-43] removed 24 variables
c [sweep-12-1] removed 24 vars (0 failed, 12 eqs, 16 impls)
c [sweep-12] 24 < 1/1000 * 35573 = 35 considered unsuccessful
c [sweep-12] removed 24 vars in TOTAL (1 rounds, 130 queries)
c [phase-count-18] 197664 negative 99.7% of 198218 except 554 0.3%
c [phase-count-18] 144815 positive 73.1% of 198218 except 53403 26.9%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 5 positive 100%, 0 negative 0%
c [sort-queue-18] sorted 35549 enqueued variables after 71430 conflicts
c [score-dist-18] active 0 (0%), one 25385 (71%), zero 10164 (29%)
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 999 variables 2.7% (35549 remain 11%)
c [simplification-18] removed 6020 irredundant clauses 2.9% (198218 remain 14%)
c [simplification-18] maximum reduction of 3% = max (3%, 3%)
c [simplification-18] geometric conflict interval increment 5583 = 22332 / 4
c [simplification-18] new conflict interval 27915
c [simplification-18] penalized conflict interval 27915 = 1 * 27915
c [simplification-18] hard conflict limit 113302 (soft 99345 + delta 13957)
c [simplification-18] new conflict limit 99345 (hard 113302)
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  163.5   35548   198218     72084   25516   7636 188229   32   110   43  29%      5   21   23   18  127%
c i  166.6   35547   198218     76800   29934   7685 188269   34   104   44  33%     53   13   34   19  174%
c i  167.2   35546   198218     77770   30835   7697 188277   35   104   44  33%     22   14   41   20  208%
c i  168.8   35539   198218     80285   33176   7725 188304   35   100   46  35%     21    9   36   20  176%
c i  168.8   35538   198218     80286   33176   7725 188304   35   100   46  35%     21    9   36   20  176%
c i  170.2   35536   198218     82398   35127   7744 188317   35    96   48  36%     16    5   45   21  218%
c i  171.6   35530   198218     84285   36887   7764 188331   37   100   48  37%     13    8   37   21  172%
c i  172.3   35529   198218     85700   38195   7793 188354   31    91   52  34%      8   -0   17   21   78%
c i  172.7   35525   198218     86256   38717   7797 188363   29    84   52  35%      4   -7   14   21   67%
c i  175.0   35524   198218     89598   41867   7845 188390   31    89   53  35%     30   -3   33   22  154%
c i  175.3   35520   198218     90108   42339   7855 188397   32    91   53  35%     17   -0   33   22  150%
c i  177.3   35517   198218     93120   45121   7905 188423   31    89   54  35%     25   -2   35   22  157%
c i  177.9   35514   198218     93961   45919   7915 188436   30    90   54  34%     10   -2   22   22  101%
c i  179.4   35506   198218     96343   48121   7943 188458   29    80   55  37%     16  -10   30   22  133%
c i  179.9   35505   198218     96975   48725   7945 188463   30    82   57  36%      7   -9   30   23  135%
c i  181.9   35504   198218    100199   51801   7971 188491   28    72   57  39%     27  -18   39   23  172%
c i  184.4   35499   198218    103580   54958   8014 188521   30    77   64  39%     29  -13   25   23  107%
c i  184.6   35476   198218    104007   55369   8015 188523   29    78   64  38%     17  -12   22   23   93%
c i  186.3   35474   198218    106760   57921   8049 188554   28    77   67  37%     19  -12   24   23  102%
c i  188.8   35473   198218    109823   60768   8085 188575   34    87   71  39%     23   -1   51   24  211%
c 
c [simplification-19] limit 99355 conflicts (hard 113302) hit after 109856 conflicts
c [quatres-15] found 15141 quaternary clauses 49% in total
c [quatres-15-2] added 34 quaternary resolvents
c [ternres-15] limit 24379203 with penalty 0 = 0 + 0
c [ternres-15] all 35471 free variables schedulable
c [ternres-15] 736 ternary resolvents (6 bin, 730 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 304740 penalty 4 = 4 + 0
c [gauss-5] extracted 15 xors of average arity 2.6
c [gauss-5] connected 39 occurrences of 39 variables (average 1.0)
c [gauss-5] limit 304740 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-44] removed 22 variables
c [treelook-7] limit 1218960 penalty 1 = 1 + 0 boost 1
c [treelook-7] scheduled 49019 literals 69%
c [treelook-7] scheduling used 822679 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 1218960 penalty 1 = 1 + 0 boost 1
c [treelook-7] used 1238532 steps
c [treelook-7] 48944 literals remain 69%
c [treelook-7] 9042 variables remain to probed next time 26%
c [treelook-7] removed 20 variables, found 5655 hbrs
c [unhide-19] limit 2437920 with penalty 1 = 0 + 1
c [unhide-19-28] 3 units, 35 failed, 7314 tauts, 0 hbrs, 295790 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 271 transitive binary clauses
c [transred-15] found 2 units
c [cce-10] limit of 60948009 steps penalty 1 = 1 + 0
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 33
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 32
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 30
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 29
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 28
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 27
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 26
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 24
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 23
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 22
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 21
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 20
c [cce-10-1] eliminated 3 clauses out of 6 (50%) of length 19
c [cce-10-1] eliminated 3 clauses out of 7 (43%) of length 18
c [cce-10-1] eliminated 3 clauses out of 8 (38%) of length 17
c [cce-10-1] eliminated 3 clauses out of 7 (43%) of length 16
c [cce-10-1] eliminated 3 clauses out of 8 (38%) of length 15
c [cce-10-1] eliminated 3 clauses out of 6 (50%) of length 14
c [cce-10-1] eliminated 3 clauses out of 6 (50%) of length 13
c [cce-10-1] eliminated 3 clauses out of 8 (38%) of length 12
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 11
c [cce-10-1] eliminated 5 clauses out of 13 (38%) of length 10
c [cce-10-1] eliminated 2 clauses out of 9 (22%) of length 9
c [cce-10-1] eliminated 5 clauses out of 19 (26%) of length 8
c [cce-10-1] eliminated 5 clauses out of 37 (14%) of length 7
c [cce-10-1] eliminated 10 clauses out of 936 (1%) of length 6
c [cce-10-1] eliminated 33 clauses out of 6293 (1%) of length 5
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 107 large clauses in 60948012 steps
c [cce-10-1] allowing another 30474006 steps for small clauses
c [cce-10-1] scheduling 132320 clauses = 106349 binary + 25971 ternary
c [cce-10-1] tried to eliminate 2694 small clauses 2%
c [cce-10-1] eliminated 399 binary clauses 0%
c [cce-10-1] eliminated 111 ternary clauses 0%
c [cce-10-1] eliminated 510 small clauses 0%
c [cce-10-1] eliminated 1545 small clauses in 60948015 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 1652 covered clauses in round 1
c [cce-10] eliminated 1652 covered clauses in TOTAL during 1 rounds
c [cce-10] 1652 < 1/100 * 196252 = 1962 considered unsuccessful
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 35271 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 9751681580 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 317 variables 1% in round 1 in 13891338 steps
c [elim-18-1] backward subsumption/strengthening limit 13891300
c [elim-18-1-1] backward checking 2090 touched variables 6%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 19 and strengthened 19 clauses in 461342 steps
c [elim-18-1] rescheduled 109 variables 0% by backward subsumption
c [elim-18-2] eliminated 2 variables 0% in round 2 in 55089 steps
c [elim-18-2] backward subsumption/strengthening limit 55000
c [elim-18-2-1] backward checking 27 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 3 and strengthened 0 clauses in 54373 steps
c [elim-18-2] rescheduled 7 variables 0% by backward subsumption
c [elim-18-3] no variable eliminated in round 3 in 3181 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 321 = 1% variables out of 35271 scheduled
c [elim-18] 321 < 1/100 * 35271 = 352 considered unsuccessful
c [bca-15] limit of 10000000 steps and 388866 added (scaled 2)
c [bca-15] 47978 out of 69902 literals actually usable 69%
c [bca-15] added 28 blocked clauses in 161367 steps
c [phase-count-19] 193399 negative 99.7% of 193956 except 557 0.3%
c [phase-count-19] 141439 positive 72.9% of 193956 except 52517 27.1%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-19] sorted 34950 enqueued variables after 109856 conflicts
c [score-dist-19] active 0 (0%), one 25420 (73%), zero 9530 (27%)
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 521 variables 1.5% (34950 remain 11%)
c [simplification-19] removed 4262 irredundant clauses 2.2% (193956 remain 14%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 9305 = 27915 / 3
c [simplification-19] new conflict interval 37220
c [simplification-19] penalized conflict interval 37220 = 1 * 37220
c [simplification-19] hard conflict limit 165686 (soft 147076 + delta 18610)
c [simplification-19] new conflict limit 147076 (hard 165686)
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 -  198.7   34950   193956    113634   25813   8415 183491   30    75   38  40%     33  -13   23   24   96%
c i  198.7   34949   193956    113872   26044   8418 183493   29    73   42  39%     36  -15   16   24   68%
c i  199.0   34948   193956    114330   26456   8423 183495   32    80   43  40%     20   -8   48   24  196%
c i  201.9   34947   193956    119862   31568   8483 183533   25    62   45  39%     56  -25   17   24   70%
c i  201.9   34943   193956    119863   31568   8483 183533   25    62   45  39%     56  -25   17   24   70%
c i  203.8   34941   193956    123928   35307   8545 183579   24    65   48  36%     33  -20   24   24   97%
c i  203.8   34939   193956    123977   35355   8545 183579   24    65   48  36%     31  -21   22   24   89%
c i  207.7   34938   193956    131116   41957   8626 183662   24    65   54  37%     76  -19   23   24   94%
c i  207.7   34936   193956    131117   41957   8626 183662   24    65   54  37%     76  -19   23   24   94%
c i  212.8   34934   193956    139948   50256   8698 183697   24    59   63  41%     97  -21   39   24  160%
c i  213.5   34933   193956    140757   51007   8711 183702   27    65   63  41%     33  -15   35   24  144%
c i  213.6   34929   193956    140906   51131   8716 183703   26    64   63  41%     25  -16   24   24   99%
c i  213.6   34928   193956    140939   51160   8717 183703   26    64   63  41%     24  -16   26   24  105%
c i  216.0   34926   193956    144206   54208   8760 183735   30    76   63  39%     12   -3   21   25   86%
c i  219.7   34925   193956    149990   59613   8793 183756   27    61   66  43%     47  -17   18   25   74%
c i  220.0   34924   193956    150400   59984   8799 183763   27    62   66  43%     24  -16   31   25  123%
c i  220.0   34922   193956    150401   59984   8799 183763   27    62   66  43%     24  -16   31   25  123%
c i  220.0   34918   193956    150404   59985   8799 183764   27    62   66  43%     23  -16   30   25  121%
c i  223.2   34912   193956    155439   64690   8829 183790   25    60   70  41%     35  -17   31   25  125%
c i  223.2   34911   193956    155445   64693   8830 183791   24    60   70  41%     35  -17   30   25  122%
c i  223.2   34893   193956    155448   64695   8830 183791   24    60   70  41%     34  -17   30   25  121%
c -  223.4   34868   193956    155622   34274   8831 183791   25    61   41  40%     25  -16   30   25  122%
c i  226.3   34867   193956    160433   38629   8882 183823   29    66   48  43%     34   -9   36   25  145%
c 
c [simplification-20] limit 147113 conflicts (hard 165686) hit after 165686 conflicts
c [quatres-16] found 15493 quaternary clauses 46% in total
c [quatres-16-1] removed 3 duplicate quaternary clauses
c [quatres-16-2] added 5 single-self-subsuming ternary resolvents
c [quatres-16-2] added 6 quaternary resolvents
c [ternres-16] limit 33707700 with penalty 0 = 0 + 0
c [ternres-16] all 34865 free variables schedulable
c [ternres-16] 463 ternary resolvents (2 bin, 461 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-46] removed 104 variables
c [basicprobe-7] limit 168538504 penalty 0 = 0 + 0
c [basicprobe-7-0] 6079 sched 18%, 679 failed, 110 lifted, 97886 hbrs
c [decomp-47] removed 2039 variables
c [basicprobe-7-1] 5079 probes remain 16% after last round
c [basicprobe-7-1] 999 units = 880 failed (88%) + 119 lifted (12%)
c [basicprobe-7-1] removed 2493 variables, found 126849 hbrs
c [bate-5] eliminated 529 asymmetric tautologies during probing
c [unhide-20] limit 6741540 with penalty 0 = 0 + 0
c [unhide-20-32] 4 units, 110 failed, 37505 tauts, 0 hbrs, 194007 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 291 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 32235 variables 100%
c [block-6] limit of 21067313 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 100 blocked clauses
c [block-6] 100 < 1/100 * 171326 = 1713 considered unsuccessful
c [bca-16] limit of 10000000 steps and 343420 added (scaled 2)
c [bca-16] 43762 out of 64464 literals actually usable 68%
c [bca-16] added 37 blocked clauses in 136327 steps
c [sweep-13] limit 5056155 penalty 1 = 1 + 0
c [sweep-13-1] 1878 pos 12.2% + 13499 neg 87.8% = 15377 sched 47.7% ret 16854
c [sweep-13-1] 5083678 steps 135 queries 1102.73 avg class size
c [sweep-13-1] 1798 decisions 120 SAT calls 79.98 avg env size
c [sweep-13-1] 14516 variables remain 45% (17658 retained 55%)
c [decomp-48] removed 283 variables
c [sweep-13-1] removed 283 vars (0 failed, 16 eqs, 21 impls)
c [sweep-13] removed 283 vars in TOTAL (1 rounds, 134 queries)
c [sort-queue-20] sorted 31948 enqueued variables after 165686 conflicts
c [score-dist-20] active 0 (0%), one 25040 (78%), zero 6908 (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 2917 variables 8.4% (31948 remain 10%)
c [simplification-20] removed 23467 irredundant clauses 12.1% (170489 remain 12%)
c [simplification-20] maximum reduction of 12% = max (8%, 12%)
c [simplification-20] large reduction 12% >= 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 177686 (soft 167686 + delta 10000)
c [simplification-20] new conflict limit 167686 (hard 177686)
c 
c [simplification-21] limit 167686 conflicts (hard 177686) hit after 177688 conflicts
c [quatres-17] found 13757 quaternary clauses 42% in total
c [quatres-17-1] removed 11 duplicate quaternary clauses
c [quatres-17-2] added 4 single-self-subsuming ternary resolvents
c [quatres-17-2] added 3 quaternary resolvents
c [ternres-17] limit 35378686 with penalty 0 = 0 + 0
c [ternres-17] all 31948 free variables schedulable
c [ternres-17] 334 ternary resolvents (1 bin, 333 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1105583 penalty 4 = 4 + 0
c [card-6] found 2169 at-most-one constraints of average size 3.9
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1105583 for elimination
c [card-6] 2169 out of 2169 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-49] removed 1 variables
c [simpleprobe-8] all 31947 free variables schedulable
c [simpleprobe-8] limit 141514744 penalty 0 = 0 + 0
c [decomp-50] removed 383 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 383 variables, found 54225 hbrs, 58 units
c [unhide-21] limit 7075737 with penalty 0 = 0 + 0
c [unhide-21-36] 0 units, 74 failed, 51795 tauts, 0 hbrs, 317263 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 462 transitive binary clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 31497 variables 100%
c [elim-19] limit of 353786860 steps penalty 1 = 1 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 1189 variables 4% in round 1 in 12038632 steps
c [elim-19-1] backward subsumption/strengthening limit 12038600
c [elim-19-1-1] backward checking 5679 touched variables 18%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 52 and strengthened 54 clauses in 967235 steps
c [elim-19-1] rescheduled 296 variables 1% by backward subsumption
c [elim-19-2] eliminated 11 variables 0% in round 2 in 460848 steps
c [elim-19-2] backward subsumption/strengthening limit 460800
c [elim-19-2-1] backward checking 146 touched variables 0%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 8 and strengthened 9 clauses in 85929 steps
c [elim-19-2] rescheduled 43 variables 0% by backward subsumption
c [elim-19-3] eliminated 1 variables 0% in round 3 in 36641 steps
c [elim-19-3] backward subsumption/strengthening limit 36600
c [elim-19-3-1] backward checking 17 touched variables 0%
c [elim-19-3-1] fully completed backward checking in 1 rounds
c [elim-19-3] subsumed 0 and strengthened 1 clauses in 32729 steps
c [elim-19] incomplete 4 not tried 0% in round 3
c [elim-19] transition to [ all 1 rem 1 ] state
c [elim-19] eliminated 1201 = 4% variables out of 31497 scheduled
c [bca-17] limit of 10000000 steps and 331836 added (scaled 2)
c [bca-17] 40124 out of 60594 literals actually usable 66%
c [bca-17] added 45 blocked clauses in 137102 steps
c [sweep-14] limit 10613605 penalty 0 = 0 + 0
c [sweep-14-1] 1682 pos 12.2% + 12148 neg 87.8% = 13830 sched 45.6% ret 16466
c [sweep-14-1] 10660634 steps 242 queries 499.73 avg class size
c [sweep-14-1] 3589 decisions 216 SAT calls 81.83 avg env size
c [sweep-14-1] 12361 variables remain 41% (17784 retained 59%)
c [decomp-51] removed 216 variables
c [sweep-14-1] removed 216 vars (0 failed, 33 eqs, 41 impls)
c [sweep-14] removed 216 vars in TOTAL (1 rounds, 241 queries)
c [sort-queue-21] sorted 30080 enqueued variables after 177688 conflicts
c [score-dist-21] active 0 (0%), one 24439 (81%), zero 5641 (19%)
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 1868 variables 5.8% (30080 remain 10%)
c [simplification-21] removed 6257 irredundant clauses 3.7% (164232 remain 12%)
c [simplification-21] maximum reduction of 6% = max (6%, 4%)
c [simplification-21] large reduction 6% >= 5% limit
c [simplification-21] next conflict interval 2000 = 2000/1
c [simplification-21] penalized conflict interval 2000 = 1 * 2000
c [simplification-21] hard conflict limit 189688 (soft 179688 + delta 10000)
c [simplification-21] new conflict limit 179688 (hard 189688)
c 
c [simplification-22] limit 179688 conflicts (hard 189688) hit after 189690 conflicts
c [quatres-18] found 14242 quaternary clauses 43% in total
c [quatres-18-1] removed 7 duplicate quaternary clauses
c [quatres-18-2] added 3 single-self-subsuming ternary resolvents
c [quatres-18-2] added 4 quaternary resolvents
c [ternres-18] limit 37210673 with penalty 0 = 0 + 0
c [ternres-18] all 30080 free variables schedulable
c [ternres-18] 569 ternary resolvents (2 bin, 567 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-52] removed 1 variables
c [treelook-8] limit 3721067 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 41838 literals 70%
c [treelook-8] scheduling used 795996 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 3721067 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 3734651 steps
c [treelook-8] 41713 literals remain 69%
c [treelook-8] 8465 variables remain to probed next time 28%
c [decomp-53] removed 4 variables
c [treelook-8] removed 7 variables, found 21002 hbrs
c [unhide-22] limit 7442134 with penalty 0 = 0 + 0
c [unhide-22-40] 0 units, 14 failed, 30792 tauts, 0 hbrs, 284467 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 334 transitive binary clauses
c [cce-11] limit of 46513341 steps penalty 2 = 2 + 0
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 47
c [cce-11-1] eliminated 1 clauses out of 1 (100%) of length 46
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-11-1] eliminated 1 clauses out of 3 (33%) of length 24
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 23
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 22
c [cce-11-1] eliminated 2 clauses out of 6 (33%) of length 21
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 20
c [cce-11-1] eliminated 2 clauses out of 6 (33%) of length 19
c [cce-11-1] eliminated 3 clauses out of 6 (50%) of length 18
c [cce-11-1] eliminated 4 clauses out of 10 (40%) of length 17
c [cce-11-1] eliminated 3 clauses out of 8 (38%) of length 16
c [cce-11-1] eliminated 3 clauses out of 9 (33%) of length 15
c [cce-11-1] eliminated 4 clauses out of 8 (50%) of length 14
c [cce-11-1] eliminated 3 clauses out of 9 (33%) of length 13
c [cce-11-1] eliminated 3 clauses out of 9 (33%) of length 12
c [cce-11-1] eliminated 5 clauses out of 11 (45%) of length 11
c [cce-11-1] eliminated 5 clauses out of 10 (50%) of length 10
c [cce-11-1] eliminated 5 clauses out of 16 (31%) of length 9
c [cce-11-1] eliminated 6 clauses out of 24 (25%) of length 8
c [cce-11-1] eliminated 9 clauses out of 48 (19%) of length 7
c [cce-11-1] eliminated 13 clauses out of 911 (1%) of length 6
c [cce-11-1] eliminated 87 clauses out of 6071 (1%) of length 5
c [cce-11-1] eliminated 2 clauses out of 11645 (0%) of length 4
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 167 large clauses in 46513345 steps
c [cce-11-1] allowing another 23256672 steps for small clauses
c [cce-11-1] scheduling 113799 clauses = 93886 binary + 19913 ternary
c [cce-11-1] tried to eliminate 3737 small clauses 3%
c [cce-11-1] eliminated 582 binary clauses 1%
c [cce-11-1] eliminated 179 ternary clauses 1%
c [cce-11-1] eliminated 761 small clauses 1%
c [cce-11-1] eliminated 777 small clauses in 46513342 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 944 covered clauses in round 1
c [cce-11] eliminated 944 covered clauses in TOTAL during 1 rounds
c [cce-11] 944 < 1/100 * 162827 = 1628 considered unsuccessful
c [elim-20] no untried remaining variables left
c [elim-20] scheduled 30031 variables 100%
c [elim-20] limit of 744213471 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 377 variables 1% in round 1 in 11566235 steps
c [elim-20-1] backward subsumption/strengthening limit 11566200
c [elim-20-1-1] backward checking 2495 touched variables 8%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 14 and strengthened 17 clauses in 540039 steps
c [elim-20-1] rescheduled 78 variables 0% by backward subsumption
c [elim-20-2] eliminated 6 variables 0% in round 2 in 56670 steps
c [elim-20-2] backward subsumption/strengthening limit 56600
c [elim-20-2-1] backward checking 93 touched variables 0%
c [elim-20-2-1] incomplete backward checking 0 remain 0%
c [elim-20-2] subsumed 4 and strengthened 1 clauses in 56601 steps
c [elim-20-2] rescheduled 13 variables 0% by backward subsumption
c [elim-20-3] eliminated 1 variables 0% in round 3 in 17835 steps
c [elim-20-3] backward subsumption/strengthening limit 17800
c [elim-20-3-1] backward checking 26 touched variables 0%
c [elim-20-3-1] incomplete backward checking 0 remain 0%
c [elim-20-3] subsumed 2 and strengthened 0 clauses in 17801 steps
c [elim-20] incomplete 5 not tried 0% in round 3
c [elim-20] transition to [ all 1 rem 1 ] state
c [elim-20] eliminated 384 = 1% variables out of 30031 scheduled
c [bca-18] limit of 10000000 steps and 323585 added (scaled 2)
c [bca-18] 38547 out of 59296 literals actually usable 65%
c [bca-18] added 37 blocked clauses in 144310 steps
c [sweep-15] limit 11163202 penalty 0 = 0 + 0
c [sweep-15-1] 1608 pos 13.2% + 10556 neg 86.8% = 12164 sched 41.0% ret 17483
c [sweep-15-1] 11193032 steps 273 queries 322.83 avg class size
c [sweep-15-1] 5393 decisions 254 SAT calls 110.00 avg env size
c [sweep-15-1] 10615 variables remain 36% (18998 retained 64%)
c [decomp-54] removed 74 variables
c [sweep-15-1] removed 74 vars (0 failed, 18 eqs, 40 impls)
c [sweep-15] removed 74 vars in TOTAL (1 rounds, 272 queries)
c [sort-queue-22] sorted 29573 enqueued variables after 189690 conflicts
c [score-dist-22] active 0 (0%), one 24261 (82%), zero 5312 (18%)
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 507 variables 1.7% (29573 remain 9%)
c [simplification-22] removed 3146 irredundant clauses 1.9% (161086 remain 12%)
c [simplification-22] maximum reduction of 2% = max (2%, 2%)
c [simplification-22] geometric conflict interval increment 12406 = 37220 / 3
c [simplification-22] new conflict interval 49626
c [simplification-22] penalized conflict interval 49626 = 1 * 49626
c [simplification-22] hard conflict limit 264129 (soft 239316 + delta 24813)
c [simplification-22] new conflict limit 239316 (hard 264129)
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  266.0   29572   161086    189877   60764   7988 235756   23    52   64  45%    341  -17   22   25   91%
c i  267.2   29571   161086    191695   62498   7995 235764   19    41   65  46%    -16  -27    8   24   33%
c -  269.6   29559   161086    195802   36524   8031 235779   21    51   40  41%    -52  -16   13   24   53%
c i  270.4   29558   161086    197757   38316   8042 235780   20    46   46  44%    -22  -21   21   24   86%
c i  276.5   29530   161086    209095   48867   8133 235822   25    54   51  46%     63  -10   28   24  117%
c i  276.5   29527   161086    209097   48868   8133 235822   25    54   51  46%     63  -10   28   24  117%
c i  277.8   29493   161086    211477   51127   8141 235838   22    48   53  47%    -59  -15   23   24   97%
c i  290.0   29486   161086    231706   69438   8291 235922   22    41   64  53%    188  -17   13   23   54%
c -  290.2   29463   161086    232052   38029   8293 235929   21    41   40  52%    102  -17   14   23   60%
c i  295.5   29462   161086    242204   47089   8363 235969   23    45   48  52%     38  -12   26   23  111%
c i  297.9   29430   161086    246748   51113   8389 235999   19    33   50  57%    -49  -22   18   23   79%
c i  298.0   26021   161086    246784   51134   8393 236004   19    33   50  57%    -51  -22   16   23   71%
c 0  298.0   25900   161086    246784   51134   8393 236004   19    33   50  57%    -51  -22   16   23   71%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 1649 basic ate = 1501 trn 91% + 148 lrg 9% in 5 updates
c bcas: 18 count, 1055 added (1382 skipped), 4360259 steps
c bkwd: tried 819396 clauses, 1636741 lits, 2.00 lits/clause
c bkwd: checked 17717286 occs, 21.62 occs/clause, 10.82 occs/lit
c bkwd: subsumed 118 binary, 1167 ternary, 193 large
c bkwd: strengthened 31 binary, 2 ternary (100% self), 1534 large (0% self)
c blkd: 6 bces, 8856 removed, 7229633 resolutions, 20070591 steps
c blkd: 10584 blocking literals 2%, 21 pure
c bump: 247819 bumped seen, 65449000 lits 264.1 on average
c card: 6 count, 0 units, 0 am1, 37839657 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 74172 subsumed
c card: 18447 at-most-one constraints found, average size 4.75
c card: 18447 at-most-one constraints used 100%, average size 4.75
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: 11 cces, 38424 eliminated, 38094 ate 99%, 330 abce 1%
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: 4660063 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 175 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 54 decompositions, 14343 equivalent 4%
c deco: 3954 decision-only clauses 2%, 56% reduction
c decs: 2387808 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 20 elims, 152884 eliminated 47%, 126 pure 0%
c elms: 63 rounds, 3.1 rounds/bve
c elms: 138882 small 91%, 13855 large 9%
c elms: 544986 tried small, 138888 succeeded 25%, 406098 failed 75%
c elms: 51326 subsumed, 72724 strengthened, 546 blocked
c elms: 23140671 copies, 20698497 resolutions, 23136119 ipos
c elms: 3037497 subchks, 2417681 strchks
c gaus: 5 extractions, 1255 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8156048 steps, 4078024 extr 50%, 166546 elim 2%
c glue: 25.0 orig avg, 25.0 real avg, 3.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 706617 = 216332 simple 31% + 469430 trn 66% + 20855 lrg 3%, 4161 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 247819 clauses, 106.1 length
c lrnd: 26282834 lits = 41630718 orig - 15347884 removed 37%
c lrnd: 106727 uips 43%, 119570 flips 48%
c mins: 233621 mins 95%, 3114 bin 1%, 6258 size 3%
c mins: 82210481 poisoned searches, 17472847 hits, 21% hit rate
c mins: 103753698 used twice searches, 3814860 hits, 4% hit rate
c move: moved 28998, 15009 bin 52%, 13989 trn 48%
c otfs: 617 driving 24%, 1942 restarting 76%
c otfs: str 2559, 2427 red 95%, 132 irr 5%
c otfs: str 2559, 0 bin 0%, 133 trn 5%, 2426 lrg 95%
c otfs: sub 8, 7 red 88%, 1 irr 12%
c otfs: sub 8, 0 bin 0%, 2 trn 25%, 6 lrg 75%
c phas: 19 computed, 216589 set, 31 pos (0%), 216558 neg (100%)
c prbs: 7 basic, 37873 probed, 2370 failed, 141 lifted
c prbs: 8 simple, 1243368 probed, 1160 failed, 3627 eqs
c prbs: 8 treelook, 295 probed, 19 failed, 0 lifted
c prom: 29239 locked 6% out of 487771 tried
c prps: 671921859 props, 264 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 18 count, 395 quat, 131 self1, 2 self2, 1266 dup
c queu: 22 sorted, 2387808 next (3 steps 0.00)
c queu: 67191848 enq (0 steps 0.00), 65449000 deq 97%
c redc: 8324 clauses 27%, 30328 tried 12%, 183 sat 1%
c redc: 18050 lits 6%, 328111 tried 1%, 183 sat 0%
c redc: 1034 times jump level reduced, 19.5 levels on average
c reds: 4 count, 61696.0 conflicts per reduce
c reds: 0 memlim 0%, 4 arith 100%
c reds: 103009 collected 81%, 24375 retired 19%
c rmbd: 57267 removed, 13283 red 23%
c rsts: 8805 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: 247819 count (225739 tried 0.9), 11943 sub out of 238249 (5.0%)
c swps: 15 count, 15 rounds, 2258 queries (150.5/round)
c swps: 1964 sat calls, 72 unsat (0.8% success rate)
c swps: 28994 decisions 14.8, 1652 conflicts 0.8
c swps; 1743.2 avg class size, 85.2 avg environment size
c swps: 0 failed, 464 impls, 352 equivs
c swp0: 747 type 0 queries, 303 unsat (40.6%), 663 sat (88.8%)
c swp1: 1511 type 1 queries, 966 unsat (63.9%), 1243 sat (82.3%)
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: 5272172 calls to obtain time
c tops: 131589 fixed 41%, 488 its, 505.70 confs/it
c trds: 18 transitive reductions, 3903 removed, 18 failed
c trds: 29133 nodes, 74924 edges, 33778676 steps
c trim: 519784 words, 2.0 MB
c trnr: 18 count, 67 bin, 17672 trn, 87804406 steps
c unhd: 22 count, 40 rounds, 91586402 steps
c unhd: 5502 non-trivial sccs of average size 2.5
c unhd: 255 units, 253 bin, 2 trn, 0 lrg
c unhd: 9417 failed, 9328 stamp, 0 lits, 35 bin, 27 trn, 0 lrg
c unhd: 346317 tauts, 7294 bin 2%, 24066 trn 7%, 1761 lrg 1%
c unhd: 346317 tauts, 313196 stamp 90%, 278926 red 81%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1639567 str, 253 bin 0%, 12678 trn 1%, 1626636 lrg 99%, 1578399 red 96%
c vars: 25900 remaining 8% and 298816 removed 92% out of 324716
c vars: 131589 fixed 41%, 152884 eliminated 47%, 14343 equivalent 4%
c vsts: 4932435327 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 7.3 search visits per propagation, 18534.2 per conflict
c wchs: 807199328 pushed, 50048180 enlarged, 251 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         238644        103009         24375      11770218       1759234         99979
c 
c  0 0         29779  12      2762   3         0   0   7372291  63    827340  47     33827  34     1.8
c  1 5         11674   5      3066   3      1101   5    869851   7<   161377   9      9585  10     1.0
c  2 6         36684  15     16400  16      3390  14   1210873  10    237063  13<    15838  16     3.1
c  3 9         45556  19     24377  24      4657  19    807709   7    165654   9     11553  12<    4.6
c  4 14        28241  12<    14825  14<     3251  13    484006   4     97814   6      7285   7     3.8
c  5 21        22830  10     12107  12      2714  11<   380754   3     87100   5      6821   7     3.0
c  6 30        19260   8      9810  10      2379  10    258819   2     68187   4      5242   5     2.4
c  7 41        15815   7      8043   8      2069   8    193790   2     55549   3      4076   4     2.2
c  8 54        10684   4      5275   5      1635   7    106302   1     28892   2      2320   2     1.8
c  9 69         6525   3      2997   3      1128   5     35848   0     12616   1      1446   1     1.3
c 10 86         5646   2      2274   2      1003   4     34998   0     10871   1      1204   1     1.2
c 11 126        4658   2       916   1       834   3     13079   0      5697   0       627   1     1.0
c 12 230        1275   1       157   0       214   1      1875   0      1061   0       155   0     0.5
c 13 534          17   0         0   0         0   0        23   0        13   0         0   0     0.0
c 
c avg                  3.9           4.3           5.0           1.2           1.9           2.5
c std                  2.8           2.4           2.7           2.0           2.4           2.7
c 
c   29.679  10% cce
c   28.725  10% elim
c   21.943   7% unhide
c   20.137   7% probe
c    8.583   3% sweep
c    5.507   2% bump
c    2.554   1% bca
c    2.032   1% block
c    1.968   1% transred
c    1.504   1% decide
c 
c    3.152 < 1% rest (below)
c 
c    1.182   0% gauss
c    0.802   0% ternres
c    0.787   0% quatres
c    0.381   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    6.410   2% preprocessing     5%
c  122.011  41% inprocessing     95%
c ==================================
c  128.422  43% simplifying
c  169.535  57% search
c ==================================
c  297.962 100% all
c 
c        246784 conflicts,         828.2 confs/sec
c          4568 ternaries,          54.0 confs/ternary
c          4084 binaries,           60.4 confs/binary
c           488 iterations,        505.7 confs/iteration
c 
c             4 reductions,          0.0 redus/sec,  61696.0 confs/reduction
c          8805 restarts,           29.6 rests/sec,     28.0 confs/restart
c       2387808 decisions,        8013.8 decis/sec,      9.7 decis/conflict
c     671921859 propagations,  2255055.6 props/sec,    281.4 props/decision
c 
c 298.0 seconds, 125.0 MB
c launch: done
