c launch: /data/cnf/sc2014/app/bob12m09-opt.cnf.bz2
c host: atom04
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/bob12m09-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/bob12m09-opt.cnf.bz2
c no embedded options
c found 'p cnf 51144 152446' header
c read 51144 variables, 152446 clauses, 355706 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 51143 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   51143   152445         0       0      0     0    0     0    9   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 85 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 85 out of 85 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 77 at-most-one constraints, 77 used 100%
c [card-1] exported 77 binary clauses, 1.0 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 51143 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 1885 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1885 variables, found 4240 hbrs, 80 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 56 units, 149 failed, 643 tauts, 0 hbrs, 57 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 49181 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 36771 variables 75% in round 1 in 10682146 steps
c [elim-1-1] backward subsumption/strengthening limit 9317854
c [elim-1-1-1] backward checking 36086 touched variables 73%
c [elim-1-1-1] incomplete backward checking 35999 remain 100%
c [elim-1-1] subsumed 42 and strengthened 76 clauses in 9318852 steps
c [elim-1] incomplete 286 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 36782 = 75% variables out of 49181 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 66441 negative 90.3% of 73595 except 7154 9.7%
c [phase-count-1] 61615 positive 83.7% of 73595 except 11980 16.3%
c [phase-1] phase bias: 3377 positive 27%, 9022 negative 73%
c [sort-queue-1] sorted 12399 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 12399 (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 38744 variables 75.8% (12399 remain 24%)
c [simplification-1] removed 78850 irredundant clauses 51.7% (73595 remain 48%)
c [simplification-1] maximum reduction of 76% = max (76%, 52%)
c [simplification-1] large reduction 76% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    1.7   12398    73582       329     175     36   135    0     5    7   5%      1    5    3    0 15081%
c i    1.7   12397    73582       332     175     37   135    0     5    7   5%      1    5    3    0 14981%
c i    1.7   12394    73577       355     179     38   135    0     6    7   5%      1    6    3    0 14763%
c i    1.8   12393    73574       708     414     80   152    1    12    7   5%      1   12    4    0 9371%
c i    1.8   12388    73573       712     413     81   153    1    12    7   5%      1   12    4    0 9310%
c 
c [simplification-2] limit 1005 conflicts (hard 11000) hit after 1006 conflicts
c [decomp-3] removed 29 variables
c [simpleprobe-2] all 12370 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 10617 variables remain 86% (1753 retained 14%)
c [simpleprobe-2] removed 0 variables, found 698 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 24740 literals 100%
c [treelook-1] scheduling used 273794 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 310028 steps
c [treelook-1] 24730 literals remain 100%
c [treelook-1] 12370 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 907 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 7634 probes remain 62% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 9628 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 721 tauts, 0 hbrs, 1143 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 12369 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 262 variables 2% in round 1 in 10395264 steps
c [elim-2-1] backward subsumption/strengthening limit 9604736
c [elim-2-1-1] backward checking 2075 touched variables 17%
c [elim-2-1-1] incomplete backward checking 1554 remain 75%
c [elim-2-1] subsumed 10 and strengthened 352 clauses in 9605780 steps
c [elim-2] incomplete 492 not tried 4% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 262 = 2% variables out of 12369 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 12107 enqueued variables after 1006 conflicts
c [score-dist-2] active 0 (0%), one 3106 (26%), zero 9001 (74%)
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 281 variables 2.3% (12107 remain 24%)
c [simplification-2] removed 904 irredundant clauses 1.2% (72669 remain 48%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17672 (soft 7672 + delta 10000)
c [simplification-2] new conflict limit 7672 (hard 17672)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    2.8   12106    72669      1674    1148    142  9763    2    23    8   7%      6   23    5    0 4391%
c i    3.1   12105    72669      2351    1662    196  9792    2    30    8   7%      6   29    5    0 2733%
c i    3.8   12092    72669      5392    4207    359  9830    4    38    8  11%     32   36    6    0 1421%
c 
c [simplification-3] limit of 133 binary hit after 133 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 40 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 40 out of 40 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 13 at-most-one constraints, 12 used 92%
c [card-2] exported 12 binary clauses, 1.0 per/constraint
c [decomp-6] removed 32 variables
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 12075 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 21 not tried 0% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 67 = 1% variables out of 12075 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 12008 enqueued variables after 5710 conflicts
c [score-dist-3] active 0 (0%), one 8259 (69%), zero 3749 (31%)
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 84 variables 0.7% (12008 remain 23%)
c [simplification-3] removed 331 irredundant clauses 0.5% (72338 remain 47%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] forced so keeping old conflict interval 6666
c [simplification-3] conflict limit remains at 7672 (hard 17672)
c [simplification-3] 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    4.5   12007    72338      6040    4709    376  9810    5    40    8  12%     19   38    8    1 1461%
c i    4.5   12006    72338      6041    4709    376  9810    5    40    8  12%     19   38    8    1 1455%
c i    4.5   12005    72338      6043    4710    376  9810    5    40    8  12%     19   38    8    1 1447%
c i    4.5   12004    72338      6079    4740    378  9811    5    40    8  12%     18   38    7    1 1405%
c i    4.5   12003    72338      6084    4743    379  9811    5    40    8  12%     18   38    7    1 1389%
c i    4.5   12002    72338      6087    4744    379  9811    5    40    8  12%     18   38    7    1 1380%
c i    4.5   12001    72338      6089    4745    379  9811    5    40    8  12%     18   38    7    1 1372%
c i    4.6   12000    72338      6464    5050    404  9823    5    42    8  12%     13   39    7    1 1170%
c 
c [simplification-4] limit 7697 conflicts (hard 17672) hit after 7698 conflicts
c [decomp-7] removed 19 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 14468 literals 60%
c [treelook-2] scheduling used 150011 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 386391 steps
c [treelook-2] 14462 literals remain 60%
c [treelook-2] 10345 variables remain to probed next time 86%
c [treelook-2] removed 0 variables, found 1614 hbrs
c [unhide-3] limit 71683 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 115 tauts, 0 hbrs, 3267 literals
c [elim-4] 21 variables 0% will be scheduled this time
c [elim-4] scheduled 21 variables 0%
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] no variable eliminated in round 1 in 11427339 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 21 scheduled
c [sort-queue-4] sorted 11989 enqueued variables after 7698 conflicts
c [score-dist-4] active 0 (0%), one 9298 (78%), zero 2691 (22%)
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 5 variables 0.0% (11989 remain 23%)
c [simplification-4] removed 161 irredundant clauses 0.2% (72177 remain 47%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 26666
c [simplification-4] penalized conflict interval 26666 = 1 * 26666
c [simplification-4] hard conflict limit 47697 (soft 34364 + delta 13333)
c [simplification-4] new conflict limit 34364 (hard 47697)
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    5.3   11988    72177      8341    6648    488 11436    6    45    9  13%     17   41    7    1  976%
c i    5.3   11987    72177      8364    6670    488 11436    6    45    9  12%     16   42    7    1  959%
c i    5.8   11986    72177     10174    8257    577 11442    6    46    9  14%     16   41    6    1  655%
c i    5.8   11974    72177     10367    8417    592 11448    6    47    9  13%     13   41    6    1  637%
c i    5.8   11973    72177     10382    8428    595 11448    6    46    9  14%     13   41    6    1  619%
c i    6.3   11972    72177     12539   10325    708 11468    7    46    9  15%     19   39    7    1  597%
c i    6.4   11971    72177     12628   10404    711 11468    7    46    9  15%     18   39    7    1  575%
c i    7.7   11968    72177     17957   15249    909 11502    8    48   10  16%     63   38    8    2  471%
c i    7.7   11967    72177     17958   15249    909 11502    8    48   10  16%     63   38    8    2  469%
c i    8.9   11966    72177     23667   20487   1064 11543    8    45   11  18%     66   33    8    2  356%
c 
c [simplification-5] limit of 26 iterations hit after 26 iterations
c [quatres-1] found 16212 quaternary clauses 47% in total
c [quatres-1-1] added 3 double-self-subsuming ternary resolvents
c [quatres-1-2] added 117 single-self-subsuming ternary resolvents
c [quatres-1-2] added 530 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 11966 free variables schedulable
c [ternres-1] 9845 ternary resolvents (58 bin, 9787 trn)
c [ternres-1] 1 variables remain 0% (11965 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 2579 xors of average arity 2.9
c [gauss-1] connected 7593 occurrences of 646 variables (average 11.8)
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 34 variables
c [basicprobe-2] limit 9628458 penalty 0 = 0 + 0
c [basicprobe-2-0] 3060 probes remain 26% after last round
c [basicprobe-2-0] 25 units = 23 failed (92%) + 2 lifted (8%)
c [basicprobe-2-0] removed 25 variables, found 33428 hbrs
c [bate-1] eliminated 53 asymmetric tautologies during probing
c [transred-1] limit 1925691 with penalty 0 = 0 + 0
c [transred-1] removed 1577 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 11907 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 773 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 27
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-1-1] eliminated 1 clauses out of 4 (25%) of length 23
c [cce-1-1] eliminated 1 clauses out of 4 (25%) of length 22
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-1-1] eliminated 1 clauses out of 10 (10%) of length 16
c [cce-1-1] eliminated 1 clauses out of 12 (8%) of length 14
c [cce-1-1] eliminated 2 clauses out of 23 (9%) of length 13
c [cce-1-1] eliminated 5 clauses out of 29 (17%) of length 12
c [cce-1-1] eliminated 9 clauses out of 44 (20%) of length 11
c [cce-1-1] eliminated 19 clauses out of 93 (20%) of length 10
c [cce-1-1] eliminated 43 clauses out of 227 (19%) of length 9
c [cce-1-1] eliminated 122 clauses out of 728 (17%) of length 8
c [cce-1-1] eliminated 215 clauses out of 1561 (14%) of length 7
c [cce-1-1] eliminated 5 clauses out of 3430 (0%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 430 large clauses in 30000024 steps
c [cce-1-1] allowing another 15000012 steps for small clauses
c [cce-1-1] scheduling 30249 clauses = 18000 binary + 12249 ternary
c [cce-1-1] tried to eliminate 3597 small clauses 12%
c [cce-1-1] eliminated 42 binary clauses 0%
c [cce-1-1] eliminated 92 ternary clauses 1%
c [cce-1-1] eliminated 134 small clauses 0%
c [cce-1-1] eliminated 134 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 564 covered clauses in round 1
c [cce-1] eliminated 564 covered clauses in TOTAL during 1 rounds
c [cce-1] 564 < 1/100 * 71008 = 710 considered unsuccessful
c [bca-1] limit of 10000000 steps and 141388 added (scaled 2)
c [bca-1] 9430 out of 23814 literals actually usable 40%
c [bca-1] added 0 blocked clauses in 43308 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4505 pos 37.8% + 7401 neg 62.2% = 11906 sched 100.0% ret 0
c [sweep-1-1] 1050655 steps 41 queries 1322.73 avg class size
c [sweep-1-1] 559 decisions 40 SAT calls 38.83 avg env size
c [sweep-1-1] 10716 variables remain 90% (1189 retained 10%)
c [decomp-10] removed 28 variables
c [sweep-1-1] removed 28 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 28 vars in TOTAL (1 rounds, 40 queries)
c [sort-queue-5] sorted 11878 enqueued variables after 23667 conflicts
c [score-dist-5] active 0 (0%), one 11717 (99%), zero 161 (1%)
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 88 variables 0.7% (11878 remain 23%)
c [simplification-5] removed 1768 irredundant clauses 2.4% (70409 remain 46%)
c [simplification-5] maximum reduction of 2% = max (1%, 2%)
c [simplification-5] forced so keeping old conflict interval 26666
c [simplification-5] conflict limit remains at 34374 (hard 47697)
c [simplification-5] 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.1   11877    70409     25247   22341  10929 43365    8    48   13  17%     19   34    9    2  375%
c i   11.1   11876    70409     25274   22361  10931 43367    8    48   13  17%     18   34    8    2  358%
c i   11.3   11871    70409     26096   23127  10955 43372    8    47   13  17%      7   33    9    2  355%
c i   11.5   11870    70409     26709   23710  10965 43372    8    47   13  17%      2   33    8    2  333%
c i   11.5   11869    70409     26729   23725  10969 43372    8    47   13  17%      2   33    8    2  317%
c i   12.2   11867    70409     29561   26335  11035 43388    8    45   13  18%     21   30    7    3  269%
c i   12.4   11866    70409     30268   26977  11060 43395    8    45   13  18%      9   29    9    3  331%
c i   12.5   11865    70409     30944   27599  11077 43399    8    45   13  18%      3   29    9    3  321%
c i   13.1   11862    70409     33166   29701  11117 43406    9    44   13  20%     12   27    9    3  293%
c i   13.3   11861    70409     33831   30344  11125 43407    9    43   13  21%      5   25   10    3  314%
c i   13.3   11841    70409     33896   30390  11130 43411    9    43   13  21%      4   25    9    3  277%
c i   13.3   11840    70409     34107   30587  11133 43412    9    42   13  21%      2   25    9    3  297%
c i   13.4   11837    70409     34275   30739  11139 43413    9    42   13  21%      0   24    8    3  267%
c i   13.6   11836    70409     35175   31606  11147 43420    9    43   13  20%     -1   25    8    3  242%
c i   13.8   11835    70409     35993   32372  11166 43424    9    43   13  20%     -2   25    9    3  272%
c i   13.9   11831    70409     36430   32778  11177 43425    9    43   13  20%     -3   24    7    3  218%
c i   14.0   11830    70409     36537   32882  11178 43426    9    42   14  21%     -4   24    8    3  248%
c i   14.0   11829    70409     36558   32897  11180 43427    9    42   14  21%     -4   24    8    3  235%
c i   14.2   11816    70409     37409   33702  11203 43431    9    44   14  20%     -3   25    9    3  264%
c i   14.5   11815    70409     38378   34624  11222 43436    9    45   14  20%     -1   26    8    3  243%
c i   14.8   11806    70409     39419   35596  11254 43440    9    45   15  19%     -0   26    9    4  242%
c 
c [simplification-6] limit 34374 conflicts (hard 47697) hit after 40468 conflicts
c [quatres-2] found 16765 quaternary clauses 45% in total
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 69 single-self-subsuming ternary resolvents
c [quatres-2-2] added 299 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 508 ternary resolvents (0 bin, 508 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 74 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 74 out of 74 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 111 variables
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 1007 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 11766 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 55 blocked clauses
c [block-2] 55 < 1/100 * 69788 = 697 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 11765 variables 100%
c [elim-5] limit of 34517604 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 6 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 306 = 3% variables out of 11765 scheduled
c [sweep-2] limit 1035528 penalty 0 = 0 + 0
c [sweep-2-1] 3964 pos 38.5% + 6330 neg 61.5% = 10294 sched 89.8% ret 1165
c [sweep-2-1] 1379996 steps 35 queries 1154.34 avg class size
c [sweep-2-1] 436 decisions 30 SAT calls 39.47 avg env size
c [sweep-2-1] 9816 variables remain 86% (1636 retained 14%)
c [decomp-12] removed 23 variables
c [sweep-2-1] removed 23 vars (0 failed, 7 eqs, 4 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 23 vars in TOTAL (1 rounds, 34 queries)
c [sort-queue-6] sorted 11436 enqueued variables after 40468 conflicts
c [score-dist-6] active 0 (0%), one 11416 (100%), zero 20 (0%)
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 367 variables 3.1% (11436 remain 22%)
c [simplification-6] removed 1568 irredundant clauses 2.2% (68841 remain 45%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 26666 / 4
c [simplification-6] new conflict interval 33332
c [simplification-6] penalized conflict interval 33332 = 1 * 33332
c [simplification-6] hard conflict limit 90466 (soft 73800 + delta 16666)
c [simplification-6] new conflict limit 73800 (hard 90466)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.3   11435    68841     40594   32096  11024 41377    9    46   15  20%      1   26    9    4  252%
c i   16.3   11434    68841     40787   32246  11035 41383    9    45   15  20%     -1   25    8    4  208%
c i   17.1   11433    68840     43461   34747  11077 41395    9    44   15  21%     18   23    8    4  210%
c i   17.8   11399    68840     46243   37377  11128 41409    9    44   15  21%     20   22    9    4  219%
c i   17.8   11398    68840     46350   37477  11131 41409    9    44   15  21%     17   22    9    4  226%
c i   18.3   11395    68840     48060   39081  11170 41418    9    43   15  22%      9   20    8    4  194%
c i   18.6   11394    68840     48967   39939  11183 41424    9    42   15  22%      2   19    9    4  215%
c i   18.6   11387    68840     49179   40134  11188 41427    9    42   15  22%      0   19    9    4  199%
c i   18.7   11386    68840     49265   40210  11192 41427    9    43   15  22%     -1   20    9    4  200%
c i   18.7   11385    68840     49310   40242  11196 41429    9    43   15  22%     -1   20    9    4  211%
c i   18.8   11382    68840     49792   40708  11204 41430    9    43   15  22%     -3   20   10    4  221%
c i   18.9   11380    68840     50040   40943  11209 41431    9    43   15  21%     -4   20    9    4  202%
c i   19.2   11379    68840     51045   41878  11230 41439    9    42   15  22%     -2   19    9    5  195%
c i   19.2   11352    68840     51046   41878  11230 41439    9    42   15  22%     -2   19    9    5  194%
c i   19.2   11351    68840     51048   41877  11230 41440    9    42   15  22%     -2   19    9    5  193%
c i   19.9   11345    68840     53411   44116  11262 41448    9    43   15  21%     13   19    9    5  184%
c i   19.9   11339    68840     53412   44116  11262 41448    9    43   15  21%     13   19    9    5  184%
c i   20.2   11337    68840     54431   45076  11281 41452    9    44   15  21%      4   19    9    5  197%
c i   20.2   11336    68840     54561   45194  11283 41453    9    43   15  21%      2   19    9    5  193%
c i   20.3   11335    68840     54734   45360  11283 41453    9    44   15  21%      1   19    9    5  199%
c i   20.6   11333    68840     55676   46233  11302 41460    9    44   16  21%     -1   19    9    5  193%
c i   20.6   11331    68840     55922   46457  11311 41462    9    44   16  20%     -2   19    8    5  172%
c i   20.7   11268    68840     56289   46806  11317 41463    9    45   16  20%     -4   19    8    5  173%
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   21.0   11267    68840     56991   47462  11326 41466    9    45   16  21%     -4   20   11    5  218%
c i   21.1   11266    68840     57439   47892  11329 41469    9    45   16  21%     -5   19    9    5  188%
c i   21.2   11265    68840     57648   48078  11338 41476    9    44   16  21%     -6   19    8    5  170%
c i   21.4   11264    68840     58257   48661  11346 41481    9    44   16  21%     -5   19    9    5  189%
c i   21.5   11258    68840     58770   49137  11357 41485    9    45   16  21%     -5   19    9    5  181%
c i   21.6   11256    68840     59128   49462  11371 41486    9    44   16  21%     -6   18    9    5  169%
c i   24.3   11255    68840     67420   57347  11508 41524    9    44   18  21%     98   16   10    6  176%
c i   24.6   11215    68840     68263   58152  11519 41529    9    45   18  21%     38   17    8    6  150%
c i   24.6   11214    68840     68264   58152  11519 41529    9    45   18  21%     38   17    8    6  149%
c i   25.2   11211    68840     69914   59747  11535 41534    9    45   19  21%      7   16    9    6  158%
c 
c [simplification-7] limit 73835 conflicts (hard 90466) hit after 73835 conflicts
c [quatres-3] found 17155 quaternary clauses 41% in total
c [quatres-3-1] removed 6 duplicate quaternary clauses
c [quatres-3-2] added 65 single-self-subsuming ternary resolvents
c [quatres-3-2] added 317 quaternary resolvents
c [ternres-3] limit 6812956 with penalty 0 = 0 + 0
c [ternres-3] all 11211 free variables schedulable
c [ternres-3] 383 ternary resolvents (3 bin, 380 trn)
c [ternres-3] 565 variables remain 5% (10646 retained 95%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 627 xors of average arity 2.8
c [gauss-2] connected 1776 occurrences of 381 variables (average 4.7)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [decomp-13] removed 59 variables
c [gauss-2] exported 2 unary, 10 binary and 0 ternary equations
c [decomp-14] removed 1 variables
c [simpleprobe-3] 9581 schedulable variables 86%
c [simpleprobe-3] limit 13625912 penalty 1 = 1 + 0
c [decomp-15] removed 37 variables
c [simpleprobe-3] 3409 variables remain 31% (7705 retained 69%)
c [simpleprobe-3] removed 37 variables, found 3785 hbrs, 16 units
c [unhide-4] limit 340647 with penalty 2 = 2 + 0
c [unhide-4-4] 6 units, 16 failed, 3680 tauts, 0 hbrs, 82406 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 451 transitive binary clauses
c [transred-3] found 2 units
c [cce-2] limit of 17032390 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 10 (20%) of length 15
c [cce-2-1] eliminated 1 clauses out of 18 (6%) of length 13
c [cce-2-1] eliminated 5 clauses out of 24 (21%) of length 12
c [cce-2-1] eliminated 5 clauses out of 48 (10%) of length 11
c [cce-2-1] eliminated 17 clauses out of 97 (18%) of length 10
c [cce-2-1] eliminated 13 clauses out of 228 (6%) of length 9
c [cce-2-1] eliminated 6 clauses out of 630 (1%) of length 8
c [cce-2-1] eliminated 2 clauses out of 1409 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 51 large clauses in 17032390 steps
c [cce-2-1] allowing another 8516195 steps for small clauses
c [cce-2-1] scheduling 28441 clauses = 16759 binary + 11682 ternary
c [cce-2-1] tried to eliminate 2437 small clauses 9%
c [cce-2-1] eliminated 59 binary clauses 0%
c [cce-2-1] eliminated 79 ternary clauses 1%
c [cce-2-1] eliminated 138 small clauses 0%
c [cce-2-1] eliminated 228 small clauses in 17032411 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 279 covered clauses in round 1
c [cce-2] eliminated 279 covered clauses in TOTAL during 1 rounds
c [cce-2] 279 < 1/100 * 67076 = 670 considered unsuccessful
c [elim-6] 6 variables 0% will be scheduled this time
c [elim-6] scheduled 6 variables 0%
c [elim-6] limit of 136259125 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 18255603 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 6 scheduled
c [bca-2] limit of 10000000 steps and 134090 added (scaled 2)
c [bca-2] 4757 out of 22200 literals actually usable 21%
c [bca-2] added 4 blocked clauses in 73055 steps
c [sweep-3] limit 2043886 penalty 0 = 0 + 0
c [sweep-3-1] 3759 pos 39.0% + 5875 neg 61.0% = 9634 sched 86.8% ret 1465
c [sweep-3-1] 2189411 steps 44 queries 620.68 avg class size
c [sweep-3-1] 1146 decisions 43 SAT calls 84.53 avg env size
c [sweep-3-1] 6585 variables remain 59% (4514 retained 41%)
c [decomp-16] removed 15 variables
c [sweep-3-1] removed 15 vars (0 failed, 1 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 15 vars in TOTAL (1 rounds, 43 queries)
c [sort-queue-7] sorted 11084 enqueued variables after 73835 conflicts
c [score-dist-7] active 0 (0%), one 11082 (100%), zero 2 (0%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 127 variables 1.1% (11084 remain 22%)
c [simplification-7] removed 2073 irredundant clauses 3.0% (66767 remain 44%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 8333 = 33332 / 4
c [simplification-7] new conflict interval 41665
c [simplification-7] penalized conflict interval 41665 = 1 * 41665
c [simplification-7] hard conflict limit 136332 (soft 115500 + delta 20832)
c [simplification-7] new conflict limit 115500 (hard 136332)
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   29.0   11083    66767     75046   63859  11662 35954   10    44   21  23%     47   14   10    6  163%
c i   29.0   11082    66767     75047   63859  11662 35954   10    44   21  23%     47   14   10    6  162%
c -   29.2   11078    66767     75459   27405  11672 35954   10    44   13  23%     26   14   10    6  159%
c i   29.4   11077    66767     76082   27990  11681 35958   10    44   14  22%     11   13    8    6  126%
c i   29.9   11075    66767     78140   29961  11708 35965    9    44   14  22%      4   13    9    6  144%
c i   30.1   11074    66767     78935   30697  11715 35970    9    44   14  21%     -4   13    9    6  144%
c i   30.6   11072    66767     80728   32429  11734 35975    9    43   14  21%     -1   12    9    6  140%
c i   30.7   11070    66767     80912   32607  11737 35975    9    44   14  21%     -3   13    9    6  143%
c i   30.9   11069    66767     81627   33283  11750 35979    9    44   14  21%     -7   12    9    6  140%
c i   31.0   11059    66767     82159   33791  11762 35979    9    44   14  21%    -10   13    9    6  145%
c i   31.5   11056    66767     83661   35229  11778 35982    9    44   15  21%     -4   13    8    6  132%
c i   31.8   11052    66767     84755   36277  11791 35986    9    44   15  21%     -6   12    9    6  143%
c i   33.5   11050    66767     90735   42007  11843 35992   10    43   14  23%     59   10    9    7  139%
c i   38.1   11049    66767    106041   56630  11953 36017   10    42   17  23%    184    8    9    7  126%
c i   40.3   11048    66767    112082   62459  11993 36023   10    43   18  24%     37    7    9    8  124%
c i   40.3   11047    66767    112083   62459  11993 36023   10    43   18  24%     37    7    9    8  124%
c 
c [simplification-8] limit 115520 conflicts (hard 136332) hit after 115552 conflicts
c [quatres-4] found 17378 quaternary clauses 38% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-2] added 86 single-self-subsuming ternary resolvents
c [quatres-4-2] added 232 quaternary resolvents
c [ternres-4] limit 10960715 with penalty 0 = 0 + 0
c [ternres-4] 539 schedulable variables 5%
c [ternres-4] 1661 ternary resolvents (21 bin, 1640 trn)
c [ternres-4] 18 variables remain 0% (11027 retained 100%)
c [gauss-3] limit 2192143 penalty 0 = 0 + 0
c [gauss-3] extracted 1288 xors of average arity 2.9
c [gauss-3] connected 3738 occurrences of 340 variables (average 11.0)
c [gauss-3] limit 2192143 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [decomp-17] removed 34 variables
c [gauss-3] exported 0 unary, 11 binary and 1 ternary equations
c [decomp-18] removed 1 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 436 transitive binary clauses
c [transred-4] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 10994 variables 100%
c [block-3] limit of 54803576 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 158 blocked clauses
c [block-3] 158 < 1/100 * 66087 = 660 considered unsuccessful
c [bca-3] limit of 10000000 steps and 132154 added (scaled 2)
c [bca-3] 4889 out of 21978 literals actually usable 22%
c [bca-3] added 1 blocked clauses in 76253 steps
c [sweep-4] limit 3288214 penalty 0 = 0 + 0
c [sweep-4-1] 2522 pos 38.9% + 3966 neg 61.1% = 6488 sched 59.0% ret 4500
c [sweep-4-1] 3992518 steps 55 queries 228.65 avg class size
c [sweep-4-1] 1406 decisions 53 SAT calls 147.55 avg env size
c [sweep-4-1] 5256 variables remain 48% (5732 retained 52%)
c [decomp-19] removed 9 variables
c [sweep-4-1] removed 9 vars (0 failed, 5 eqs, 5 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 9 vars in TOTAL (1 rounds, 54 queries)
c [sort-queue-8] sorted 10979 enqueued variables after 115552 conflicts
c [score-dist-8] active 0 (0%), one 10978 (100%), zero 1 (0%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 66 variables 0.6% (10979 remain 21%)
c [simplification-8] removed 947 irredundant clauses 1.4% (65820 remain 43%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 20832 = 41665 / 2
c [simplification-8] new conflict interval 62497
c [simplification-8] penalized conflict interval 62497 = 1 * 62497
c [simplification-8] hard conflict limit 209297 (soft 178049 + delta 31248)
c [simplification-8] new conflict limit 178049 (hard 209297)
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.0   10978    65820    116648   66813  13710 35775   10    43   21  24%     15    7    9    8  120%
c i   43.0   10977    65820    116649   66813  13710 35775   10    43   21  24%     15    7    9    8  119%
c i   43.0   10976    65820    116650   66813  13710 35775   10    43   21  24%     15    7    9    8  119%
c -   44.7   10976    65820    121590   36448  13731 35779   10    43   13  23%     21    7   11    8  134%
c i   46.6   10975    65820    129265   43719  13770 35786    8    50   15  17%    131   12    9    8  118%
c i   50.5   10972    65820    154022   65783  13894 35814    6    34   17  18%    275   -5    8    7  116%
c i   52.4   10971    65820    159403   70928  13909 35818    9    37   24  24%    -26   -1    9    8  125%
c -   56.4   10971    65820    170587   50140  13956 35824   10    38   15  27%     65   -0   10    8  127%
c 
c [simplification-9] limit 178069 conflicts (hard 209297) hit after 178071 conflicts
c [quatres-5] found 18331 quaternary clauses 33% in total
c [quatres-5-1] removed 5 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 116 single-self-subsuming ternary resolvents
c [quatres-5-2] added 122 quaternary resolvents
c [ternres-5] limit 16179448 with penalty 0 = 0 + 0
c [ternres-5] 18 schedulable variables 0%
c [ternres-5] 1319 ternary resolvents (10 bin, 1309 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 3235889 penalty 0 = 0 + 0
c [gauss-4] extracted 1622 xors of average arity 3.1
c [gauss-4] connected 5028 occurrences of 420 variables (average 12.0)
c [gauss-4] limit 3235889 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-20] removed 17 variables
c [unhide-5] limit 1617944 with penalty 1 = 1 + 0
c [unhide-5-6] 14 units, 17 failed, 3779 tauts, 0 hbrs, 28926 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 329 transitive binary clauses
c [transred-5] found 4 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 10903 variables 100%
c [elim-7] limit of 161794489 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 329 variables 3% in round 1 in 52670861 steps
c [elim-7-1] backward subsumption/strengthening limit 52670800
c [elim-7-1-1] backward checking 1578 touched variables 14%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 8 and strengthened 36 clauses in 6701367 steps
c [elim-7-1] rescheduled 121 variables 1% by backward subsumption
c [elim-7-2] eliminated 4 variables 0% in round 2 in 5091752 steps
c [elim-7-2] backward subsumption/strengthening limit 5091700
c [elim-7-2-1] backward checking 46 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 5 and strengthened 2 clauses in 1415720 steps
c [elim-7-2] rescheduled 14 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 3481466 steps
c [elim-7] fully completed in 3 rounds
c [gc-52] reconnected 34266 binary clauses (produced 0 empty 1 units)
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 337 = 3% variables out of 10903 scheduled
c [bca-4] limit of 10000000 steps and 128860 added (scaled 2)
c [bca-4] 5653 out of 21134 literals actually usable 27%
c [bca-4] added 6 blocked clauses in 60508 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 48538340 penalty 0 = 0 + 0
c [sweep-5-1] 2047 pos 41.3% + 2909 neg 58.7% = 4956 sched 46.9% ret 5610
c [sweep-5-1] 30191338 steps 928 queries 26.01 avg class size
c [sweep-5-1] 10358 decisions 721 SAT calls 52.95 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-21] removed 576 variables
c [sweep-5-1] removed 576 vars (0 failed, 437 eqs, 350 impls)
c [sweep-5-2] 3733 pos 37.4% + 6257 neg 62.6% = 9990 sched 100.0% ret 0
c [sweep-5-2] 18369571 steps 348 queries 82.07 avg class size
c [sweep-5-2] 5896 decisions 306 SAT calls 69.56 avg env size
c [sweep-5-2] 1340 variables remain 13% (8639 retained 87%)
c [decomp-22] removed 87 variables
c [sweep-5-2] removed 87 vars (0 failed, 74 eqs, 71 impls)
c [sweep-5] removed 663 vars in TOTAL (2 rounds, 1274 queries)
c [sort-queue-9] sorted 9903 enqueued variables after 178071 conflicts
c [score-dist-9] active 0 (0%), one 9902 (100%), zero 1 (0%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 1068 variables 9.7% (9903 remain 19%)
c [simplification-9] removed 3521 irredundant clauses 5.3% (62299 remain 41%)
c [simplification-9] maximum reduction of 10% = max (10%, 5%)
c [simplification-9] large reduction 10% >= 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 190071 (soft 180071 + delta 10000)
c [simplification-9] new conflict limit 180071 (hard 190071)
c 
c [simplification-10] limit 180071 conflicts (hard 190071) hit after 180071 conflicts
c [quatres-6] found 17716 quaternary clauses 35% in total
c [quatres-6-1] removed 28 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 116 single-self-subsuming ternary resolvents
c [quatres-6-2] added 241 quaternary resolvents
c [ternres-6] limit 16353597 with penalty 0 = 0 + 0
c [ternres-6] all 9903 free variables schedulable
c [ternres-6] 2259 ternary resolvents (20 bin, 2239 trn)
c [ternres-6] 17 variables remain 0% (9886 retained 100%)
c [card-4] limit 1022099 penalty 3 = 3 + 0
c [card-4] found 117 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1022099 for elimination
c [card-4] 117 out of 117 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 3270719 penalty 0 = 0 + 0
c [gauss-5] extracted 1524 xors of average arity 3.1
c [gauss-5] connected 4725 occurrences of 387 variables (average 12.2)
c [gauss-5] limit 3270719 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 1 variables
c [treelook-3] limit 408839 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 18439 literals 93%
c [treelook-3] scheduling used 408953 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 408839 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 432616 steps
c [treelook-3] 18423 literals remain 93%
c [treelook-3] 8709 variables remain to probed next time 88%
c [treelook-3] removed 0 variables, found 664 hbrs
c [unhide-6] limit 3270719 with penalty 0 = 0 + 0
c [unhide-6-9] 3 units, 29 failed, 4218 tauts, 0 hbrs, 17580 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 307 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 20441997 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 14
c [cce-3-1] eliminated 1 clauses out of 6 (17%) of length 13
c [cce-3-1] eliminated 1 clauses out of 15 (7%) of length 12
c [cce-3-1] eliminated 5 clauses out of 39 (13%) of length 11
c [cce-3-1] eliminated 13 clauses out of 95 (14%) of length 10
c [cce-3-1] eliminated 24 clauses out of 206 (12%) of length 9
c [cce-3-1] eliminated 48 clauses out of 610 (8%) of length 8
c [cce-3-1] eliminated 13 clauses out of 1295 (1%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 106 large clauses in 20442010 steps
c [cce-3-1] allowing another 10221005 steps for small clauses
c [cce-3-1] scheduling 24999 clauses = 14668 binary + 10331 ternary
c [cce-3-1] tried to eliminate 1461 small clauses 6%
c [cce-3-1] eliminated 50 binary clauses 0%
c [cce-3-1] eliminated 115 ternary clauses 1%
c [cce-3-1] eliminated 165 small clauses 1%
c [cce-3-1] eliminated 188 small clauses in 20442102 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 294 covered clauses in round 1
c [cce-3] eliminated 294 covered clauses in TOTAL during 1 rounds
c [cce-3] 294 < 1/100 * 61721 = 617 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 9888 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 6541439160 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 399 variables 4% in round 1 in 52478856 steps
c [elim-8-1] backward subsumption/strengthening limit 52478800
c [elim-8-1-1] backward checking 1310 touched variables 13%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 4 and strengthened 7 clauses in 6187168 steps
c [elim-8-1] rescheduled 46 variables 0% by backward subsumption
c [elim-8-2] eliminated 3 variables 0% in round 2 in 560552 steps
c [elim-8-2] backward subsumption/strengthening limit 560500
c [elim-8-2-1] backward checking 21 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 189654 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 402 = 4% variables out of 9888 scheduled
c [bca-5] limit of 10000000 steps and 119371 added (scaled 2)
c [bca-5] 4857 out of 18974 literals actually usable 26%
c [bca-5] added 9 blocked clauses in 57102 steps
c [sweep-6] limit 4906079 penalty 0 = 0 + 0
c [sweep-6-1] 421 pos 37.1% + 713 neg 62.9% = 1134 sched 12.0% ret 8352
c [sweep-6-1] 4913130 steps 150 queries 38.05 avg class size
c [sweep-6-1] 1947 decisions 113 SAT calls 63.52 avg env size
c [sweep-6-1] 628 variables remain 7% (8858 retained 93%)
c [decomp-25] removed 61 variables
c [sweep-6-1] removed 61 vars (0 failed, 55 eqs, 57 impls)
c [sweep-6] removed 61 vars in TOTAL (1 rounds, 149 queries)
c [sort-queue-10] sorted 9425 enqueued variables after 180071 conflicts
c [score-dist-10] active 0 (0%), one 9424 (100%), zero 1 (0%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 478 variables 4.8% (9425 remain 18%)
c [simplification-10] removed 2873 irredundant clauses 4.6% (59425 remain 39%)
c [simplification-10] maximum reduction of 5% = max (5%, 5%)
c [simplification-10] large reduction 5% >= 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 192071 (soft 182071 + delta 10000)
c [simplification-10] new conflict limit 182071 (hard 192071)
c 
c [simplification-11] limit 182071 conflicts (hard 192071) hit after 192071 conflicts
c [quatres-7] found 17266 quaternary clauses 35% in total
c [quatres-7-1] removed 17 duplicate quaternary clauses
c [quatres-7-2] added 63 single-self-subsuming ternary resolvents
c [quatres-7-2] added 192 quaternary resolvents
c [ternres-7] limit 17259271 with penalty 0 = 0 + 0
c [ternres-7] 15 schedulable variables 0%
c [ternres-7] 1505 ternary resolvents (23 bin, 1482 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 5 variables
c [basicprobe-3] limit 86296359 penalty 0 = 0 + 0
c [basicprobe-3-0] 2186 sched 23%, 8 failed, 0 lifted, 17633 hbrs
c [decomp-27] removed 31 variables
c [basicprobe-3-1] 4490 sched 48%, 6 failed, 0 lifted, 7328 hbrs
c [decomp-28] removed 30 variables
c [basicprobe-3-2] 4406 sched 47%, 0 failed, 0 lifted, 478 hbrs
c [basicprobe-3-3] 4399 sched 47%, 0 failed, 0 lifted, 95 hbrs
c [basicprobe-3-4] 1145 probes remain 12% after last round
c [basicprobe-3-4] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 61 variables, found 25567 hbrs
c [bate-2] eliminated 50 asymmetric tautologies during probing
c [unhide-7] limit 3451854 with penalty 0 = 0 + 0
c [unhide-7-12] 0 units, 0 failed, 4194 tauts, 0 hbrs, 23040 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 469 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 9359 variables 100%
c [block-4] limit of 43148179 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 273 blocked clauses
c [block-4] 273 < 1/100 * 59023 = 590 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 9329 variables 100%
c [elim-9] limit of 345185438 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 116 variables 1% in round 1 in 52453294 steps
c [elim-9-1] backward subsumption/strengthening limit 52453200
c [elim-9-1-1] backward checking 654 touched variables 7%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 4 and strengthened 2 clauses in 5800711 steps
c [elim-9-1] rescheduled 21 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 123307 steps
c [elim-9-2] backward subsumption/strengthening limit 123300
c [elim-9-2-1] backward checking 14 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 29312 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 117 = 1% variables out of 9329 scheduled
c [bca-6] limit of 10000000 steps and 117360 added (scaled 2)
c [bca-6] 4286 out of 18426 literals actually usable 23%
c [bca-6] added 8 blocked clauses in 64920 steps
c [sweep-7] limit 5177781 penalty 0 = 0 + 0
c [sweep-7-1] 213 pos 38.0% + 348 neg 62.0% = 561 sched 6.1% ret 8651
c [sweep-7-1] 5822816 steps 87 queries 30.07 avg class size
c [sweep-7-1] 1373 decisions 76 SAT calls 82.62 avg env size
c [sweep-7-1] 333 variables remain 4% (8879 retained 96%)
c [decomp-31] removed 20 variables
c [sweep-7-1] removed 20 vars (0 failed, 20 eqs, 11 impls)
c [sweep-7] removed 20 vars in TOTAL (1 rounds, 86 queries)
c [sort-queue-11] sorted 9192 enqueued variables after 192071 conflicts
c [score-dist-11] active 0 (0%), one 9191 (100%), zero 1 (0%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 233 variables 2.5% (9192 remain 18%)
c [simplification-11] removed 1011 irredundant clauses 1.7% (58414 remain 38%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 20832 = 62497 / 3
c [simplification-11] new conflict interval 83329
c [simplification-11] penalized conflict interval 83329 = 1 * 83329
c [simplification-11] hard conflict limit 317064 (soft 275400 + delta 41664)
c [simplification-11] new conflict limit 275400 (hard 317064)
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 -   79.9    9192    58414    216858   45188  13622 49536   11    33   14  34%    551   -5   11    9  120%
c -   88.8    9192    58414    255991   51200  13702 49540   11    34   23  33%    763   -5   12    9  127%
c -   99.4    9192    58414    292703   54154  13743 49543   10    29   15  34%    875   -8    8   10   81%
c 
c [simplification-12] limit 275400 conflicts (hard 317064) hit after 317064 conflicts
c [quatres-8] found 17711 quaternary clauses 32% in total
c [quatres-8-1] removed 4 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 70 single-self-subsuming ternary resolvents
c [quatres-8-2] added 163 quaternary resolvents
c [ternres-8] limit 30829375 with penalty 0 = 0 + 0
c [ternres-8] all 9192 free variables schedulable
c [ternres-8] 1267 ternary resolvents (19 bin, 1248 trn)
c [ternres-8] 4 variables remain 0% (9188 retained 100%)
c [gauss-6] limit 3082937 penalty 1 = 1 + 0
c [gauss-6] extracted 1362 xors of average arity 3.0
c [gauss-6] connected 4148 occurrences of 347 variables (average 12.0)
c [gauss-6] limit 3082937 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-32] removed 5 variables
c [simpleprobe-4] 2940 schedulable variables 32%
c [simpleprobe-4] limit 123317501 penalty 0 = 0 + 0
c [decomp-33] removed 113 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 113 variables, found 8022 hbrs, 2 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 665 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 9074 variables 100%
c [elim-10] limit of 616587509 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 15 variables 0% in round 1 in 56476707 steps
c [elim-10-1] backward subsumption/strengthening limit 56476700
c [elim-10-1-1] backward checking 216 touched variables 2%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 2 and strengthened 3 clauses in 332491 steps
c [elim-10-1] rescheduled 11 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 8364 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 15 = 0% variables out of 9074 scheduled
c [elim-10] 15 < 1/100 * 9074 = 90 considered unsuccessful
c [bca-7] limit of 10000000 steps and 116416 added (scaled 2)
c [bca-7] 3964 out of 18120 literals actually usable 22%
c [bca-7] added 1 blocked clauses in 81630 steps
c [sweep-8] limit 9248812 penalty 0 = 0 + 0
c [sweep-8-1] 123 pos 37.8% + 202 neg 62.2% = 325 sched 3.6% ret 8734
c [sweep-8-1] 4359556 steps 148 queries 8.26 avg class size
c [sweep-8-1] 1860 decisions 144 SAT calls 59.99 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-34] removed 41 variables
c [sweep-8-1] removed 41 vars (0 failed, 43 eqs, 32 impls)
c [sweep-8-2] 3373 pos 37.4% + 5645 neg 62.6% = 9018 sched 100.0% ret 0
c [sweep-8-2] 5469994 steps 26 queries 1259.15 avg class size
c [sweep-8-2] 868 decisions 24 SAT calls 104.04 avg env size
c [sweep-8-2] 8755 variables remain 97% (263 retained 3%)
c [decomp-35] removed 4 variables
c [sweep-8-2] removed 4 vars (0 failed, 3 eqs, 3 impls)
c [sweep-8] removed 45 vars in TOTAL (2 rounds, 172 queries)
c [sort-queue-12] sorted 9014 enqueued variables after 317064 conflicts
c [score-dist-12] active 0 (0%), one 9014 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 178 variables 1.9% (9014 remain 18%)
c [simplification-12] removed 473 irredundant clauses 0.8% (57941 remain 38%)
c [simplification-12] maximum reduction of 2% = max (2%, 1%)
c [simplification-12] geometric conflict interval increment 27776 = 83329 / 3
c [simplification-12] new conflict interval 111105
c [simplification-12] penalized conflict interval 111105 = 1 * 111105
c [simplification-12] hard conflict limit 483721 (soft 428169 + delta 55552)
c [simplification-12] new conflict limit 428169 (hard 483721)
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 -  112.9    9014    57941    332389   55705  14688 56296   10    34   15  30%    943   -1   12    9  124%
c -  125.7    9014    57941    369286   57740  14719 56297    9    29   24  32%    978   -4   10    9  108%
c -  138.7    9014    57941    406035   59198  14739 56298   11    27   17  41%    998   -4   12    9  131%
c i  139.1    9013    57941    407273   60383  14741 56298   11    27   19  42%    998   -4   11    9  121%
c -  151.0    9013    57941    443070   59020  14767 56301   10    32   16  31%  -1270    1   10   10  105%
c 
c [simplification-13] limit 428169 conflicts (hard 483721) hit after 483721 conflicts
c [quatres-9] found 17984 quaternary clauses 29% in total
c [quatres-9-1] removed 12 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 58 single-self-subsuming ternary resolvents
c [quatres-9-2] added 141 quaternary resolvents
c [ternres-9] limit 56006309 with penalty 0 = 0 + 0
c [ternres-9] 4 schedulable variables 0%
c [ternres-9] 442 ternary resolvents (8 bin, 434 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-7] limit 11201261 penalty 0 = 0 + 0
c [gauss-7] extracted 1359 xors of average arity 3.2
c [gauss-7] connected 4281 occurrences of 340 variables (average 12.6)
c [gauss-7] limit 11201261 penalty 0 = 0 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 1 variables
c [unhide-8] limit 5600630 with penalty 1 = 1 + 0
c [unhide-8-16] 0 units, 4 failed, 6419 tauts, 0 hbrs, 106033 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 422 transitive binary clauses
c [bca-8] limit of 10000000 steps and 116096 added (scaled 2)
c [bca-8] 3757 out of 18020 literals actually usable 21%
c [bca-8] added 30 blocked clauses in 102925 steps
c [sweep-9] limit 16801892 penalty 0 = 0 + 0
c [sweep-9-1] 3248 pos 37.1% + 5501 neg 62.9% = 8749 sched 97.1% ret 260
c [sweep-9-1] 16810900 steps 136 queries 155.79 avg class size
c [sweep-9-1] 2624 decisions 131 SAT calls 94.50 avg env size
c [sweep-9-1] 3230 variables remain 36% (5779 retained 64%)
c [decomp-37] removed 20 variables
c [sweep-9-1] removed 20 vars (0 failed, 18 eqs, 11 impls)
c [sweep-9] removed 20 vars in TOTAL (1 rounds, 135 queries)
c [sort-queue-13] sorted 8989 enqueued variables after 483721 conflicts
c [score-dist-13] active 0 (0%), one 8989 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 24 variables 0.3% (8989 remain 18%)
c [simplification-13] removed 152 irredundant clauses 0.3% (57789 remain 38%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 111105
c [simplification-13] new conflict interval 222210
c [simplification-13] penalized conflict interval 222210 = 1 * 222210
c [simplification-13] hard conflict limit 817036 (soft 705931 + delta 111105)
c [simplification-13] new conflict limit 705931 (hard 817036)
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 -  168.3    8989    57789    485409   63183  14718 50664   10    23   16  41%   -178   -7   10   10  105%
c -  175.2    8989    57789    523926   67017  14740 50666    9    11   17  74%    356  -11    9    9   95%
c -  182.8    8989    57789    565046   69244  14767 50668    8     9   17  82%    667   -8   10    9  111%
c i  184.3    8988    57789    575702   78506  14772 50669    8    10   21  77%    721   -6    6    9   73%
c i  186.1    8979    57789    585424   87542  14805 50681    7    10   21  71%  -1542   -6    5    8   62%
c i  190.4    8978    57789    606618  105641  14838 50686    8    10   33  73%   -945   -4    7    8   87%
c -  190.4    8978    57789    606934   71881  14839 50686    8    11   26  73%  -1023   -3    9    8  104%
c i  190.6    8977    57789    608249   72916  14839 50687    8    10   29  75%  -1156   -4    7    8   83%
c i  191.8    8954    57789    614975   78458  14873 50690    7    10   29  73%  -1028   -4    6    8   74%
c i  192.0    8927    57789    616608   79847  14897 50696    7    11   29  62%  -1061   -2    6    8   70%
c i  192.0    8926    57789    616611   79849  14897 50696    7    11   29  62%  -1061   -2    6    8   70%
c i  192.0    8925    57789    616645   79864  14898 50701    7    11   29  62%  -1061   -2    5    8   67%
c i  192.0    8834    57789    616646   79864  14898 50701    7    11   29  62%  -1061   -2    5    8   67%
c -  205.8    8780    57789    646462   71610  14940 50723   11    16   26  71%   -328    1   11    9  122%
c i  206.8    8779    57787    651049   75407  14956 50729    9    37   19  25%   -237   22    7    9   71%
c i  206.9    8773    57787    651224   75568  14957 50732    9    36   19  25%   -318   21    5    9   58%
c 0  206.9    8734    57787    651224   75568  14957 50732    9    36   19  25%   -318   21    5    9   58%
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: 103 basic ate = 68 trn 66% + 35 lrg 34% in 2 updates
c bcas: 8 count, 59 added (53 skipped), 559701 steps
c bkwd: tried 132482 clauses, 264511 lits, 2.00 lits/clause
c bkwd: checked 25563118 occs, 192.96 occs/clause, 96.64 occs/lit
c bkwd: subsumed 3 binary, 17 ternary, 55 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 478 large (0% self)
c blkd: 4 bces, 1259 removed, 1418919 resolutions, 3566814 steps
c blkd: 580 blocking literals 1%, 38 pure
c bump: 656657 bumped seen, 66409658 lits 101.1 on average
c card: 4 count, 0 units, 89 am1, 10826783 steps
c card: 29 rescheduled, 269 eliminated, 8839 resolved, 4389 subsumed
c card: 316 at-most-one constraints found, average size 3.01
c card: 316 at-most-one constraints used 100%, average size 3.01
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: 3 cces, 1024 eliminated, 982 ate 96%, 42 abce 4%
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: 508152 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 82 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 37 decompositions, 2905 equivalent 6%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2213737 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 38310 eliminated 75%, 15 pure 0%
c elms: 19 rounds, 1.9 rounds/bve
c elms: 36822 small 96%, 1435 large 4%
c elms: 47779 tried small, 36823 succeeded 77%, 10956 failed 23%
c elms: 2276 subsumed, 4873 strengthened, 276 blocked
c elms: 2581004 copies, 3382560 resolutions, 944431 ipos
c elms: 3817983 subchks, 3732254 strchks
c gaus: 7 extractions, 10361 extracted, 3.0 size, 4 max
c gaus: exported 2 units, 21 binary and 3 ternary equations
c gaus: 0 gc, 36027280 steps, 18013640 extr 50%, 298747 elim 1%
c glue: 9.1 orig avg, 9.1 real avg, 2.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 98111 = 16745 simple 17% + 79894 trn 81% + 1472 lrg 2%, 808 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 656657 clauses, 23.5 length
c lrnd: 15449729 lits = 35311079 orig - 19861350 removed 56%
c lrnd: 124425 uips 19%, 491187 flips 75%
c mins: 648080 mins 99%, 592 bin 0%, 7985 size 1%
c mins: 61221049 poisoned searches, 3884805 hits, 6% hit rate
c mins: 91958237 used twice searches, 2149474 hits, 2% hit rate
c move: moved 1899, 468 bin 25%, 1431 trn 75%
c otfs: 1808 driving 31%, 4107 restarting 69%
c otfs: str 5915, 5633 red 95%, 282 irr 5%
c otfs: str 5915, 0 bin 0%, 279 trn 5%, 5636 lrg 95%
c otfs: sub 122, 91 red 75%, 31 irr 25%
c otfs: sub 122, 0 bin 0%, 28 trn 23%, 94 lrg 77%
c phas: 1 computed, 12399 set, 3377 pos (27%), 9022 neg (73%)
c prbs: 3 basic, 45643 probed, 38 failed, 2 lifted
c prbs: 4 simple, 154714 probed, 98 failed, 3894 eqs
c prbs: 3 treelook, 32 probed, 0 failed, 0 lifted
c prom: 150987 locked 8% out of 1931766 tried
c prps: 389157430 props, 171 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 9 count, 2237 quat, 760 self1, 10 self2, 137 dup
c queu: 13 sorted, 2213737 next (184 steps 0.00)
c queu: 66601205 enq (0 steps 0.00), 66409658 deq 100%
c redc: 22132 clauses 14%, 161526 tried 25%, 11 sat 0%
c redc: 33419 lits 2%, 1970285 tried 6%, 11 sat 0%
c redc: 798 times jump level reduced, 3.8 levels on average
c reds: 15 count, 43414.9 conflicts per reduce
c reds: 0 memlim 0%, 15 arith 100%
c reds: 427524 collected 86%, 68756 retired 14%
c rmbd: 13823 removed, 13243 red 96%
c rsts: 25535 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 13 count, 11 confs 85%, 0 vars 0%
c simp: 1 its 8%, 1 bin 8%, 0 trns 0%
c subl: 656657 count (271102 tried 0.4), 51870 sub out of 651574 (8.0%)
c swps: 9 count, 11 rounds, 1987 queries (180.6/round)
c swps: 1681 sat calls, 374 unsat (4.3% success rate)
c swps: 28473 decisions 16.9, 7241 conflicts 4.3
c swps; 126.2 avg class size, 65.8 avg environment size
c swps: 0 failed, 546 impls, 663 equivs
c swp0: 659 type 0 queries, 383 unsat (58.1%), 489 sat (74.2%)
c swp1: 1328 type 1 queries, 1147 unsat (86.4%), 835 sat (62.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 5741146 calls to obtain time
c tops: 1195 fixed 2%, 113 its, 5763.04 confs/it
c trds: 9 transitive reductions, 5663 removed, 14 failed
c trds: 52392 nodes, 102101 edges, 17928871 steps
c trim: 305640 words, 1.2 MB
c trnr: 9 count, 162 bin, 19027 trn, 178401674 steps
c unhd: 8 count, 16 rounds, 20411363 steps
c unhd: 150 non-trivial sccs of average size 2.0
c unhd: 79 units, 77 bin, 1 trn, 1 lrg
c unhd: 215 failed, 212 stamp, 0 lits, 0 bin, 2 trn, 1 lrg
c unhd: 23769 tauts, 131 bin 1%, 3491 trn 15%, 5376 lrg 23%
c unhd: 23769 tauts, 14771 stamp 62%, 22787 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 262452 str, 77 bin 0%, 702 trn 0%, 261673 lrg 100%, 258457 red 98%
c vars: 8734 remaining 17% and 42410 removed 83% out of 51144
c vars: 1195 fixed 2%, 38310 eliminated 75%, 2905 equivalent 6%
c vsts: 7595527702 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 19.7 search visits per propagation, 11420.1 per conflict
c wchs: 1877281247 pushed, 13580632 enlarged, 146 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         653811        427524         68756      26276785       8285713        336201
c 
c  0 0         70449  11      8340   2         0   0  18218614  69   4759400  57    144199  43     1.7
c  1 5         49087   8     26534   6      6965  10   3545247  13<  1264610  15<    54117  16<    0.7
c  2 6        203459  31<   146913  34     17992  26   3522869  13   1635740  20     84815  25     2.4
c  3 9        244069  37    187836  44<    24083  35<   850864   3    530753   6     42293  13     2.6
c  4 14        74097  11     50603  12     15775  23    121541   0     84852   1      9708   3     1.3
c  5 21        11687   2      6782   2      3613   5     16373   0      9672   0      1017   0     0.4
c  6 30          890   0       468   0       313   0      1181   0       619   0        44   0     0.1
c  7 41           67   0        44   0        13   0        89   0        63   0         8   0     0.0
c  8 54            5   0         3   0         2   0         5   0         3   0         0   0     0.0
c  9 69            1   0         1   0         0   0         2   0         1   0         0   0     0.0
c 
c avg                  2.4           2.6           2.9           0.5           0.8           1.2
c std                  1.2           0.9           1.1           0.9           1.0           1.2
c 
c    5.954   3% elim
c    4.257   2% probe
c    3.671   2% sweep
c    3.460   2% bump
c    2.786   1% unhide
c    1.901   1% cce
c    1.467   1% decide
c    1.245   1% transred
c    1.106   1% ternres
c 
c    2.638 < 1% rest (below)
c 
c    0.988   0% gauss
c    0.701   0% quatres
c    0.428   0% block
c    0.385   0% bca
c    0.137   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.554   1% preprocessing     6%
c   23.250  11% inprocessing     94%
c ==================================
c   24.804  12% simplifying
c  182.047  88% search
c ==================================
c  206.852 100% all
c 
c        651224 conflicts,        3148.3 confs/sec
c          3177 ternaries,         205.0 confs/ternary
c           671 binaries,          970.5 confs/binary
c           113 iterations,       5763.0 confs/iteration
c 
c            15 reductions,          0.1 redus/sec,  43414.9 confs/reduction
c         25535 restarts,          123.4 rests/sec,     25.5 confs/restart
c       2213737 decisions,       10702.0 decis/sec,      3.4 decis/conflict
c     389157430 propagations,  1881332.1 props/sec,    175.8 props/decision
c 
c 206.9 seconds, 40.6 MB
c launch: done
