c launch: /data/cnf/sc2014/app/manol-pipe-c8nidw.cnf.bz2
c host: atom14
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/manol-pipe-c8nidw.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-c8nidw.cnf.bz2
c no embedded options
c found 'p cnf 269048 799867' header
c read 269048 variables, 799867 clauses, 1866355 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
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 269047 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
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  269047   799866         0       0      0     0    0     0   44   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 6 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] 6 out of 6 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 269047 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 864 variables
c [simpleprobe-1] 50622 variables remain 19% (217561 retained 81%)
c [simpleprobe-1] removed 864 variables, found 1325 hbrs, 21 units
c [unhide-1] limit 50000 with penalty 1 = 0 + 1
c [unhide-1-1] 2 units, 7 failed, 118 tauts, 0 hbrs, 98 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 267970 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 53809 not tried 20% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 214096 = 80% variables out of 267970 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 315609 negative 97.3% of 324383 except 8774 2.7%
c [phase-count-1] 309428 positive 95.4% of 324383 except 14955 4.6%
c [phase-1] phase bias: 15056 positive 28%, 38818 negative 72%
c [sort-queue-1] sorted 53874 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 53874 (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 215173 variables 80.0% (53874 remain 20%)
c [simplification-1] removed 475483 irredundant clauses 59.4% (324383 remain 41%)
c [simplification-1] maximum reduction of 80% = max (80%, 59%)
c [simplification-1] large reduction 80% >= 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    5.8   53873   324383        24      15      2    26    0     1   40   3%      0    1    0    0 24781%
c i    5.8   53872   324383        37      24      4    27    0     1   40   5%      0    1    1    0 24160%
c i    5.8   53860   324383        94      63     12    31    0     2   40   6%      0    2    1    0 21491%
c i    5.8   53846   324383       104      72     12    31    0     2   40   7%      0    2    1    0 21268%
c 
c [simplification-2] limit 1001 conflicts (hard 11000) hit after 1002 conflicts
c [decomp-3] removed 129 variables
c [simpleprobe-2] 10134 schedulable variables 19%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 7 variables
c [simpleprobe-2] 10208 variables remain 19% (43530 retained 81%)
c [simpleprobe-2] removed 7 variables, found 26 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 31636 literals 29%
c [treelook-1] scheduling used 300017 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 308914 steps
c [treelook-1] 31529 literals remain 29%
c [treelook-1] 27443 variables remain to probed next time 51%
c [treelook-1] removed 10 variables, found 421 hbrs
c [basicprobe-1] limit 2583488 based on 322936 irredundant clauses
c [basicprobe-1-0] 22616 probes remain 43% after last round
c [basicprobe-1-0] 102 units = 102 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 713 variables, found 3619 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 4 units, 14 failed, 276 tauts, 0 hbrs, 2688 literals
c [elim-2] 52920 variables 100% will be scheduled this time
c [elim-2] scheduled 52920 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 5817 not tried 11% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 15025 = 28% variables out of 52920 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 275674 negative 97.0% of 284096 except 8422 3.0%
c [phase-count-2] 275581 positive 97.0% of 284096 except 8515 3.0%
c [phase-2] phase bias: 30 positive 35%, 56 negative 65%
c [sort-queue-2] sorted 33524 enqueued variables after 1002 conflicts
c [score-dist-2] active 4436 (12%), one 0 (0%), zero 33524 (88%)
c [score-dist-2] max exp 511, different 10 (2%)
c [score-dist-2] median active exp 510, avg 509.7
c [simplification-2] removed 15886 variables 29.5% (37960 remain 14%)
c [simplification-2] removed 40287 irredundant clauses 12.4% (284096 remain 36%)
c [simplification-2] maximum reduction of 30% = max (30%, 12%)
c [simplification-2] large reduction 30% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13002 (soft 3002 + delta 10000)
c [simplification-2] new conflict limit 3002 (hard 13002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.4   37959   284092      1723     829     76   822    3    50   40   5%     12   50    9    0 4653%
c 
c [simplification-3] limit 3002 conflicts (hard 13002) hit after 3003 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 53 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] 53 out of 53 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 45 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 20346 literals 27%
c [treelook-2] scheduling used 300123 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 359441 steps
c [treelook-2] 20193 literals remain 27%
c [treelook-2] 13105 variables remain to probed next time 35%
c [decomp-7] removed 2 variables
c [treelook-2] removed 13 variables, found 158 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 5 failed, 705 tauts, 0 hbrs, 3939 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 37898 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 4143 not tried 11% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 445 = 1% variables out of 37898 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 29056 enqueued variables after 3003 conflicts
c [score-dist-3] active 8397 (22%), one 0 (0%), zero 29056 (78%)
c [score-dist-3] max exp 513, different 12 (2%)
c [score-dist-3] median active exp 512, avg 511.4
c [simplification-3] removed 505 variables 1.3% (37453 remain 14%)
c [simplification-3] removed 2490 irredundant clauses 0.9% (281602 remain 35%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23003 (soft 13003 + delta 10000)
c [simplification-3] new conflict limit 13003 (hard 23003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.2   37452   281602      3170    1785    169   805    4   102   40   4%     13   99   10    0 2689%
c i   12.5   37400   281601      4127    2444    226   825    5   112   41   5%     10  109    9    0 1882%
c i   13.1   37395   281601      5367    3331    280   830    6   120   41   5%     11  115    9    1 1455%
c i   14.0   37391   281601      7573    4887    358   843    7   150   41   5%     21  140   10    1 1101%
c i   14.3   37390   281601      8533    5579    396   853    8   150   41   5%     12  139    9    1  948%
c i   14.3   37384   281601      8564    5593    402   856    8   149   41   5%     12  138    9    1  881%
c i   14.7   37378   281599     10316    6802    493   881    8   137   41   6%     15  123    8    1  710%
c 
c [simplification-4] limit 13003 conflicts (hard 23003) hit after 13004 conflicts
c [decomp-8] removed 129 variables
c [basicprobe-2] limit 6303114 penalty 0 = 0 + 0
c [basicprobe-2-0] 14903 sched 41%, 135 failed, 17 lifted, 1806 hbrs
c [decomp-9] removed 657 variables
c [basicprobe-2-1] 19775 sched 54%, 46 failed, 11 lifted, 543 hbrs
c [decomp-10] removed 177 variables
c [basicprobe-2-2] 10449 probes remain 29% after last round
c [basicprobe-2-2] 220 units = 192 failed (87%) + 28 lifted (13%)
c [basicprobe-2-2] removed 855 variables, found 2500 hbrs
c [unhide-4] limit 252124 with penalty 0 = 0 + 0
c [unhide-4-4] 4 units, 2 failed, 206 tauts, 0 hbrs, 4748 literals
c [elim-4] 3846 variables 11% will be scheduled this time
c [elim-4] scheduled 3846 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 504249140 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 125677845 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 3 = 0% variables out of 3846 scheduled
c [elim-4] 3 < 1/100 * 3846 = 38 considered unsuccessful
c [sort-queue-4] sorted 23699 enqueued variables after 13004 conflicts
c [score-dist-4] active 12762 (35%), one 0 (0%), zero 23699 (65%)
c [score-dist-4] max exp 515, different 12 (2%)
c [score-dist-4] median active exp 514, avg 513.4
c [simplification-4] removed 907 variables 2.4% (36461 remain 14%)
c [simplification-4] removed 14570 irredundant clauses 5.2% (267029 remain 33%)
c [simplification-4] maximum reduction of 5% = max (2%, 5%)
c [simplification-4] large reduction 5% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 25004 (soft 15004 + delta 10000)
c [simplification-4] new conflict limit 15004 (hard 25004)
c 
c [simplification-5] limit 15004 conflicts (hard 25004) hit after 15005 conflicts
c [quatres-1] found 29159 quaternary clauses 22% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 5 double-self-subsuming ternary resolvents
c [quatres-1-2] added 557 single-self-subsuming ternary resolvents
c [quatres-1-2] added 5450 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 36461 free variables schedulable
c [ternres-1] 10598 ternary resolvents (352 bin, 10246 trn)
c [ternres-1] 19 variables remain 0% (36442 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 17520 xors of average arity 3.0
c [gauss-1] connected 52510 occurrences of 7400 variables (average 7.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 44 variables
c [simpleprobe-3] 6822 schedulable variables 19%
c [simpleprobe-3] limit 5706613 penalty 0 = 0 + 0
c [simpleprobe-3] 6160 variables remain 17% (30257 retained 83%)
c [simpleprobe-3] removed 0 variables, found 89 hbrs, 0 units
c [unhide-5] limit 285330 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 1 failed, 543 tauts, 0 hbrs, 2023 literals
c [transred-1] limit 1426653 with penalty 0 = 0 + 0
c [transred-1] removed 165 transitive binary clauses
c [transred-1] found 1 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 36409 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 8481 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 10 (10%) of length 26
c [cce-1-1] eliminated 1 clauses out of 33 (3%) of length 25
c [cce-1-1] eliminated 5 clauses out of 112 (4%) of length 23
c [cce-1-1] eliminated 3 clauses out of 105 (3%) of length 22
c [cce-1-1] eliminated 8 clauses out of 194 (4%) of length 21
c [cce-1-1] eliminated 9 clauses out of 163 (6%) of length 20
c [cce-1-1] eliminated 15 clauses out of 168 (9%) of length 19
c [cce-1-1] eliminated 22 clauses out of 196 (11%) of length 18
c [cce-1-1] eliminated 20 clauses out of 254 (8%) of length 17
c [cce-1-1] eliminated 22 clauses out of 417 (5%) of length 16
c [cce-1-1] eliminated 66 clauses out of 541 (12%) of length 15
c [cce-1-1] eliminated 95 clauses out of 630 (15%) of length 14
c [cce-1-1] eliminated 117 clauses out of 873 (13%) of length 13
c [cce-1-1] eliminated 153 clauses out of 1098 (14%) of length 12
c [cce-1-1] eliminated 223 clauses out of 1730 (13%) of length 11
c [cce-1-1] eliminated 386 clauses out of 2866 (13%) of length 10
c [cce-1-1] eliminated 439 clauses out of 4783 (9%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1585 large clauses in 30000061 steps
c [cce-1-1] allowing another 15000030 steps for small clauses
c [cce-1-1] scheduling 110629 clauses = 33001 binary + 77628 ternary
c [cce-1-1] tried to eliminate 18416 small clauses 17%
c [cce-1-1] eliminated 91 binary clauses 0%
c [cce-1-1] eliminated 191 ternary clauses 0%
c [cce-1-1] eliminated 282 small clauses 0%
c [cce-1-1] eliminated 282 small clauses in 30000065 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1867 covered clauses in round 1
c [cce-1] eliminated 1867 covered clauses in TOTAL during 1 rounds
c [cce-1] 1867 < 1/100 * 257884 = 2578 considered unsuccessful
c [bca-1] limit of 10000000 steps and 512534 added (scaled 2)
c [bca-1] 54943 out of 71552 literals actually usable 77%
c [bca-1] added 15 blocked clauses in 178388 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 13304 pos 37.2% + 22471 neg 62.8% = 35775 sched 100.0% ret 0
c [sweep-1-1] 1004103 steps 98 queries 7715.28 avg class size
c [sweep-1-1] 3648 decisions 97 SAT calls 55.45 avg env size
c [sweep-1-1] 33948 variables remain 95% (1827 retained 5%)
c [decomp-13] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 97 queries)
c [sort-queue-5] sorted 22411 enqueued variables after 15005 conflicts
c [score-dist-5] active 13361 (37%), one 0 (0%), zero 22411 (63%)
c [score-dist-5] max exp 515, different 12 (2%)
c [score-dist-5] median active exp 515, avg 513.8
c [simplification-5] removed 689 variables 1.9% (35772 remain 13%)
c [simplification-5] removed 11014 irredundant clauses 4.1% (256013 remain 32%)
c [simplification-5] maximum reduction of 4% = max (2%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 14000
c [simplification-5] penalized conflict interval 14000 = 1 * 14000
c [simplification-5] hard conflict limit 39005 (soft 29005 + delta 10000)
c [simplification-5] new conflict limit 29005 (hard 39005)
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   22.3   35771   256013     17193   16790  13088  2673    9   145   41   6%     86  120    8    2  409%
c i   25.3   35755   256013     27470   24354  13544  2735    9   120   42   7%    129   81    8    3  307%
c 
c [simplification-6] limit 29005 conflicts (hard 39005) hit after 29005 conflicts
c [quatres-2] found 33600 quaternary clauses 25% in total
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 225 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2141 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 19 schedulable variables 0%
c [ternres-2] 3391 ternary resolvents (57 bin, 3334 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 84 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] 84 out of 84 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 40 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15988 literals 22%
c [treelook-3] scheduling used 300006 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 317158 steps
c [treelook-3] 15893 literals remain 22%
c [treelook-3] 8910 variables remain to probed next time 25%
c [decomp-15] removed 5 variables
c [treelook-3] removed 38 variables, found 405 hbrs
c [unhide-6] limit 550851 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 3 failed, 1116 tauts, 0 hbrs, 7546 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 124 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 35690 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 1271 blocked clauses
c [block-2] 1271 < 1/100 * 255248 = 2552 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 35361 variables 100%
c [elim-5] limit of 27542561 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 2895 not tried 8% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1889 = 5% variables out of 35361 scheduled
c [bca-2] limit of 10000000 steps and 501097 added (scaled 2)
c [bca-2] 48999 out of 66946 literals actually usable 73%
c [bca-2] added 52 blocked clauses in 173555 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 12412 pos 39.1% + 19310 neg 60.9% = 31722 sched 94.8% ret 1750
c [sweep-2-1] 1003508 steps 111 queries 5636.44 avg class size
c [sweep-2-1] 3116 decisions 109 SAT calls 43.60 avg env size
c [sweep-2-1] 30425 variables remain 91% (3033 retained 9%)
c [decomp-16] removed 27 variables
c [sweep-2-1] removed 27 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 27 vars in TOTAL (1 rounds, 110 queries)
c [sort-queue-6] sorted 18933 enqueued variables after 29005 conflicts
c [score-dist-6] active 14512 (43%), one 0 (0%), zero 18933 (57%)
c [score-dist-6] max exp 516, different 13 (3%)
c [score-dist-6] median active exp 516, avg 514.8
c [simplification-6] removed 2308 variables 6.5% (33445 remain 12%)
c [simplification-6] removed 6157 irredundant clauses 2.4% (249856 remain 31%)
c [simplification-6] maximum reduction of 6% = max (6%, 2%)
c [simplification-6] large reduction 6% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 41005 (soft 31005 + delta 10000)
c [simplification-6] new conflict limit 31005 (hard 41005)
c 
c [simplification-7] limit 31005 conflicts (hard 41005) hit after 31005 conflicts
c [quatres-3] found 33912 quaternary clauses 25% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 75 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2085 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 33445 free variables schedulable
c [ternres-3] 533 ternary resolvents (18 bin, 515 trn)
c [ternres-3] 21658 variables remain 65% (11787 retained 35%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 8041 xors of average arity 3.0
c [gauss-2] connected 24122 occurrences of 5043 variables (average 4.8)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 14519171 penalty 0 = 0 + 0
c [basicprobe-3-0] 9776 sched 29%, 21 failed, 0 lifted, 1015 hbrs
c [decomp-18] removed 61 variables
c [basicprobe-3-1] 17869 sched 54%, 17 failed, 0 lifted, 689 hbrs
c [decomp-19] removed 54 variables
c [basicprobe-3-2] 17821 sched 53%, 0 failed, 0 lifted, 54 hbrs
c [basicprobe-3-3] 17815 sched 53%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-3-4] 17813 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 38 units = 38 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 115 variables, found 1762 hbrs
c [bate-1] eliminated 260 asymmetric tautologies during probing
c [unhide-7] limit 580766 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 496 tauts, 0 hbrs, 2593 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 176 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 11 (9%) of length 26
c [cce-2-1] eliminated 1 clauses out of 27 (4%) of length 25
c [cce-2-1] eliminated 1 clauses out of 83 (1%) of length 24
c [cce-2-1] eliminated 2 clauses out of 109 (2%) of length 23
c [cce-2-1] eliminated 1 clauses out of 105 (1%) of length 22
c [cce-2-1] eliminated 1 clauses out of 192 (1%) of length 21
c [cce-2-1] eliminated 2 clauses out of 171 (1%) of length 20
c [cce-2-1] eliminated 7 clauses out of 182 (4%) of length 19
c [cce-2-1] eliminated 12 clauses out of 186 (6%) of length 18
c [cce-2-1] eliminated 16 clauses out of 295 (5%) of length 17
c [cce-2-1] eliminated 25 clauses out of 420 (6%) of length 16
c [cce-2-1] eliminated 35 clauses out of 531 (7%) of length 15
c [cce-2-1] eliminated 53 clauses out of 684 (8%) of length 14
c [cce-2-1] eliminated 43 clauses out of 935 (5%) of length 13
c [cce-2-1] eliminated 89 clauses out of 1203 (7%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 289 large clauses in 15000036 steps
c [cce-2-1] allowing another 7500018 steps for small clauses
c [cce-2-1] scheduling 50020 clauses = 30307 binary + 19713 ternary
c [cce-2-1] tried to eliminate 7167 small clauses 14%
c [cce-2-1] eliminated 67 binary clauses 0%
c [cce-2-1] eliminated 67 ternary clauses 0%
c [cce-2-1] eliminated 134 small clauses 0%
c [cce-2-1] eliminated 134 small clauses in 15000025 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 423 covered clauses in round 1
c [cce-2] eliminated 423 covered clauses in TOTAL during 1 rounds
c [cce-2] 423 < 1/100 * 247529 = 2475 considered unsuccessful
c [elim-6] 2869 variables 9% will be scheduled this time
c [elim-6] scheduled 2869 variables 9%
c [elim-6] limit of 58076686 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 698 not tried 2% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 2869 scheduled
c [bca-3] limit of 10000000 steps and 494405 added (scaled 2)
c [bca-3] 48073 out of 66662 literals actually usable 72%
c [bca-3] added 2 blocked clauses in 173715 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 13373 pos 44.1% + 16952 neg 55.9% = 30325 sched 91.0% ret 3005
c [sweep-3-1] 1020442 steps 82 queries 7675.38 avg class size
c [sweep-3-1] 2456 decisions 80 SAT calls 54.52 avg env size
c [sweep-3-1] 29218 variables remain 88% (4112 retained 12%)
c [decomp-22] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 81 queries)
c [sort-queue-7] sorted 18791 enqueued variables after 31005 conflicts
c [score-dist-7] active 14538 (44%), one 0 (0%), zero 18791 (56%)
c [score-dist-7] max exp 516, different 13 (3%)
c [score-dist-7] median active exp 516, avg 514.9
c [simplification-7] removed 116 variables 0.3% (33329 remain 12%)
c [simplification-7] removed 2921 irredundant clauses 1.2% (246935 remain 31%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 24000
c [simplification-7] penalized conflict interval 24000 = 1 * 24000
c [simplification-7] hard conflict limit 67005 (soft 55005 + delta 12000)
c [simplification-7] new conflict limit 55005 (hard 67005)
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.8   33328   246935     33979   30513  12553  3257    8   105   43   8%     66   60    8    3  256%
c i   34.4   33288   246935     35892   31970  12621  3268    9   102   43   8%      9   55    9    3  264%
c i   38.4   33281   246935     48454   41748  13065  3302    8   106   43   8%    148   50    8    4  177%
c 
c [simplification-8] limit 55005 conflicts (hard 67005) hit after 55006 conflicts
c [quatres-4] found 36087 quaternary clauses 26% in total
c [quatres-4-1] added 4 double-self-subsuming ternary resolvents
c [quatres-4-2] added 208 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1171 quaternary resolvents
c [ternres-4] limit 5238835 with penalty 0 = 0 + 0
c [ternres-4] 21546 schedulable variables 65%
c [ternres-4] 1096 ternary resolvents (29 bin, 1067 trn)
c [ternres-4] 8245 variables remain 25% (25034 retained 75%)
c [decomp-23] removed 124 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 148 transitive binary clauses
c [transred-4] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 33197 variables 100%
c [block-3] limit of 26194175 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 2220 blocked clauses
c [block-3] 2220 < 1/100 * 245677 = 2456 considered unsuccessful
c [bca-4] limit of 10000000 steps and 487356 added (scaled 2)
c [bca-4] 44868 out of 65958 literals actually usable 68%
c [bca-4] added 26 blocked clauses in 181948 steps
c [sweep-4] limit 1571650 penalty 0 = 0 + 0
c [sweep-4-1] 13194 pos 45.7% + 15705 neg 54.3% = 28899 sched 87.6% ret 4079
c [sweep-4-1] 1600699 steps 105 queries 6545.70 avg class size
c [sweep-4-1] 2982 decisions 102 SAT calls 46.65 avg env size
c [sweep-4-1] 27195 variables remain 82% (5783 retained 18%)
c [decomp-24] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 2 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2 vars in TOTAL (1 rounds, 104 queries)
c [sort-queue-8] sorted 17244 enqueued variables after 55006 conflicts
c [score-dist-8] active 15732 (48%), one 0 (0%), zero 17244 (52%)
c [score-dist-8] max exp 517, different 14 (3%)
c [score-dist-8] median active exp 517, avg 515.8
c [simplification-8] removed 303 variables 0.9% (32976 remain 12%)
c [simplification-8] removed 3524 irredundant clauses 1.4% (243411 remain 30%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 12000 = 24000 / 2
c [simplification-8] new conflict interval 36000
c [simplification-8] penalized conflict interval 36000 = 1 * 36000
c [simplification-8] hard conflict limit 109006 (soft 91006 + delta 18000)
c [simplification-8] new conflict limit 91006 (hard 109006)
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.5   32975   243411     66625   56346  14907  3464    9    98   46   9%    209   31    9    5  160%
c i   51.0   32972   243411     84060   70754  15377  3484    9    78   46  12%    178    6    9    6  149%
c 
c [simplification-9] limit 91006 conflicts (hard 109006) hit after 91006 conflicts
c [quatres-5] found 38249 quaternary clauses 26% in total
c [quatres-5-1] removed 3 duplicate quaternary clauses
c [quatres-5-2] added 41 single-self-subsuming ternary resolvents
c [quatres-5-2] added 632 quaternary resolvents
c [ternres-5] limit 8881228 with penalty 0 = 0 + 0
c [ternres-5] 8171 schedulable variables 25%
c [ternres-5] 3880 ternary resolvents (189 bin, 3691 trn)
c [ternres-5] 16 variables remain 0% (32950 retained 100%)
c [decomp-25] removed 21 variables
c [simpleprobe-4] 5578 schedulable variables 17%
c [simpleprobe-4] limit 17762456 penalty 1 = 1 + 0
c [decomp-26] removed 10 variables
c [simpleprobe-4] 3733 variables remain 11% (29212 retained 89%)
c [simpleprobe-4] removed 10 variables, found 263 hbrs, 1 units
c [unhide-8] limit 888122 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 20 failed, 2023 tauts, 0 hbrs, 34913 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 210 transitive binary clauses
c [transred-5] found 2 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 32930 variables 100%
c [elim-7] limit of 88812284 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 591 not tried 2% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 573 = 2% variables out of 32930 scheduled
c [bca-5] limit of 10000000 steps and 483045 added (scaled 2)
c [bca-5] 42601 out of 64716 literals actually usable 66%
c [bca-5] added 15 blocked clauses in 203977 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 26643680 penalty 0 = 0 + 0
c [sweep-5-1] 11892 pos 44.6% + 14785 neg 55.4% = 26677 sched 82.4% ret 5680
c [sweep-5-1] 26645541 steps 4274 queries 413.42 avg class size
c [sweep-5-1] 75653 decisions 4230 SAT calls 26.29 avg env size
c [sweep-5-1] 1275 variables remain 4% (31056 retained 96%)
c [decomp-27] removed 147 variables
c [sweep-5-1] removed 147 vars (0 failed, 102 eqs, 64 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 147 vars in TOTAL (1 rounds, 4273 queries)
c [sort-queue-9] sorted 15557 enqueued variables after 91006 conflicts
c [score-dist-9] active 16653 (52%), one 0 (0%), zero 15557 (48%)
c [score-dist-9] max exp 518, different 15 (3%)
c [score-dist-9] median active exp 518, avg 516.7
c [simplification-9] removed 756 variables 2.3% (32210 remain 12%)
c [simplification-9] removed 3364 irredundant clauses 1.4% (240047 remain 30%)
c [simplification-9] maximum reduction of 2% = max (2%, 1%)
c [simplification-9] geometric conflict interval increment 12000 = 36000 / 3
c [simplification-9] new conflict interval 48000
c [simplification-9] penalized conflict interval 48000 = 1 * 48000
c [simplification-9] hard conflict limit 163006 (soft 139006 + delta 24000)
c [simplification-9] new conflict limit 139006 (hard 163006)
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   60.0   32209   240047     92651   76903  15873  3322    9    98   51   9%     39   25    9    6  132%
c -   60.7   32207   240047     94421   34986  15924  3325    9   100   43   9%    -43   26    9    7  144%
c i   68.1   32206   240047    126009   61570  16512  3353    8    73   47  10%    350   -5    7    7   98%
c i   68.9   32122   240047    128952   63876  16594  3361    8   100   47   8%    -97   22   12    7  161%
c i   69.6   32115   240047    131608   65877  16685  3377    8   123   47   7%   -120   43    9    7  117%
c i   69.7   32107   240047    131850   66069  16691  3379    8   123   47   7%   -126   43   10    7  142%
c i   69.7   32105   240047    131860   66077  16691  3380    8   122   47   7%   -126   42   10    7  141%
c i   70.3   32103   240047    133562   67398  16752  3396    8   128   47   6%   -129   48    9    7  126%
c i   72.2   32094   240047    139022   71763  16891  3410    9   118   47   7%    -69   33    7    7   97%
c i   73.2   32091   240047    142694   74779  16996  3422    8    96   48   9%    -89    9    8    7  105%
c i   74.1   32087   240047    145202   76792  17071  3430    9   119   48   7%   -100   32    9    8  119%
c 
c [simplification-10] limit 139007 conflicts (hard 163006) hit after 153893 conflicts
c [quatres-6] found 38933 quaternary clauses 26% in total
c [quatres-6-1] removed 18 duplicate quaternary clauses
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 204 single-self-subsuming ternary resolvents
c [quatres-6-2] added 762 quaternary resolvents
c [ternres-6] limit 14107421 with penalty 0 = 0 + 0
c [ternres-6] 14 schedulable variables 0%
c [ternres-6] 3792 ternary resolvents (102 bin, 3690 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 881713 penalty 3 = 3 + 0
c [card-4] found 191 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 881713 for elimination
c [card-4] 191 out of 191 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 705371 penalty 2 = 2 + 0
c [gauss-3] extracted 5626 xors of average arity 3.0
c [gauss-3] connected 16734 occurrences of 4048 variables (average 4.1)
c [gauss-3] limit 705371 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 341 variables
c [treelook-4] limit 1410742 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 24977 literals 39%
c [treelook-4] scheduling used 797026 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1410742 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1431203 steps
c [treelook-4] 24706 literals remain 39%
c [treelook-4] 7691 variables remain to probed next time 24%
c [decomp-29] removed 3 variables
c [treelook-4] removed 22 variables, found 1571 hbrs
c [unhide-9] limit 2821484 with penalty 0 = 0 + 0
c [unhide-9-9] 1 units, 0 failed, 1838 tauts, 0 hbrs, 29005 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 368 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 17634276 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 29
c [cce-3-1] eliminated 4 clauses out of 26 (15%) of length 25
c [cce-3-1] eliminated 1 clauses out of 83 (1%) of length 24
c [cce-3-1] eliminated 1 clauses out of 105 (1%) of length 23
c [cce-3-1] eliminated 4 clauses out of 102 (4%) of length 22
c [cce-3-1] eliminated 6 clauses out of 184 (3%) of length 21
c [cce-3-1] eliminated 20 clauses out of 167 (12%) of length 20
c [cce-3-1] eliminated 22 clauses out of 168 (13%) of length 19
c [cce-3-1] eliminated 26 clauses out of 175 (15%) of length 18
c [cce-3-1] eliminated 45 clauses out of 291 (15%) of length 17
c [cce-3-1] eliminated 49 clauses out of 420 (12%) of length 16
c [cce-3-1] eliminated 34 clauses out of 468 (7%) of length 15
c [cce-3-1] eliminated 48 clauses out of 604 (8%) of length 14
c [cce-3-1] eliminated 58 clauses out of 802 (7%) of length 13
c [cce-3-1] eliminated 56 clauses out of 975 (6%) of length 12
c [cce-3-1] eliminated 12 clauses out of 1666 (1%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 387 large clauses in 17634419 steps
c [cce-3-1] allowing another 8817209 steps for small clauses
c [cce-3-1] scheduling 50005 clauses = 28696 binary + 21309 ternary
c [cce-3-1] tried to eliminate 6908 small clauses 14%
c [cce-3-1] eliminated 267 binary clauses 1%
c [cce-3-1] eliminated 180 ternary clauses 1%
c [cce-3-1] eliminated 447 small clauses 1%
c [cce-3-1] eliminated 574 small clauses in 17636175 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 961 covered clauses in round 1
c [cce-3] eliminated 961 covered clauses in TOTAL during 1 rounds
c [cce-3] 961 < 1/100 * 234278 = 2342 considered unsuccessful
c [elim-8] 516 variables 2% will be scheduled this time
c [elim-8] scheduled 516 variables 2%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5642968480 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1 variables 0% in round 1 in 92305300 steps
c [elim-8-1] backward subsumption/strengthening limit 92305300
c [elim-8-1-1] backward checking 1250 touched variables 4%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 138 and strengthened 37 clauses in 2858678 steps
c [elim-8-1] rescheduled 146 variables 0% by backward subsumption
c [elim-8-2] eliminated 25 variables 0% in round 2 in 7891226 steps
c [elim-8-2] backward subsumption/strengthening limit 7891200
c [elim-8-2-1] backward checking 117 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 77 and strengthened 17 clauses in 1824815 steps
c [elim-8-2] rescheduled 57 variables 0% by backward subsumption
c [elim-8-3] eliminated 13 variables 0% in round 3 in 1316888 steps
c [elim-8-3] backward subsumption/strengthening limit 1316800
c [elim-8-3-1] backward checking 44 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 0 and strengthened 2 clauses in 494941 steps
c [elim-8] incomplete 13 not tried 0% in round 3
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 39 = 8% variables out of 516 scheduled
c [elim-8] 39 < 1/100 * 516 = 5 considered unsuccessful
c [bca-6] limit of 10000000 steps and 463253 added (scaled 2)
c [bca-6] 41496 out of 63352 literals actually usable 66%
c [bca-6] added 4 blocked clauses in 197916 steps
c [sweep-6] limit 4232226 penalty 0 = 0 + 0
c [sweep-6-1] 588 pos 46.7% + 670 neg 53.3% = 1258 sched 4.0% ret 30417
c [sweep-6-1] 1769816 steps 757 queries 214.06 avg class size
c [sweep-6-1] 9267 decisions 754 SAT calls 17.05 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-30] removed 45 variables
c [sweep-6-1] removed 45 vars (0 failed, 3 eqs, 3 impls)
c [sweep-6-2] 13543 pos 42.8% + 18087 neg 57.2% = 31630 sched 100.0% ret 0
c [sweep-6-2] 2472074 steps 144 queries 4481.80 avg class size
c [sweep-6-2] 5102 decisions 146 SAT calls 70.39 avg env size
c [sweep-6-2] 28441 variables remain 90% (3189 retained 10%)
c [decomp-31] removed 12 variables
c [sweep-6-2] removed 12 vars (0 failed, 5 eqs, 5 impls)
c [sweep-6] removed 57 vars in TOTAL (2 rounds, 899 queries)
c [sort-queue-10] sorted 14577 enqueued variables after 153893 conflicts
c [score-dist-10] active 17041 (54%), one 0 (0%), zero 14577 (46%)
c [score-dist-10] max exp 519, different 16 (3%)
c [score-dist-10] median active exp 518, avg 517.5
c [simplification-10] removed 468 variables 1.5% (31618 remain 12%)
c [simplification-10] removed 9150 irredundant clauses 3.8% (230897 remain 29%)
c [simplification-10] maximum reduction of 4% = max (1%, 4%)
c [simplification-10] geometric conflict interval increment 9600 = 48000 / 5
c [simplification-10] new conflict interval 57600
c [simplification-10] penalized conflict interval 57600 = 1 * 57600
c [simplification-10] hard conflict limit 240293 (soft 211493 + delta 28800)
c [simplification-10] new conflict limit 211493 (hard 240293)
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   81.0   31617   230897    157714   74431  17535  4798    8   122   49   7%     58   31    9    8  120%
c i   84.3   31616   230896    169464   84001  17878  4828    9   126   49   7%     51   31    9    8  115%
c -   87.8   31616   230896    183227   57345  18248  4864    8   100   43   8%     84    3    7    8   86%
c i   88.0   31615   230896    185139   59047  18270  4867    8    69   45  11%    111  -27    5    8   62%
c i   89.3   31613   230896    192280   64744  18412  4883    7   108   46   7%    -18   11    6    8   79%
c i   89.5   31602   230896    193706   65871  18442  4890    8   109   46   7%    -78   12    8    8  102%
c i   91.1   31600   230895    200833   71654  18555  4907    8   109   46   7%    -10    8    6    8   78%
c i   92.6   31592   230895    206386   76334  18662  4919    9   149   47   6%    -30   45    9    8  117%
c 
c [simplification-11] limit 211493 conflicts (hard 240293) hit after 213550 conflicts
c [quatres-7] found 40668 quaternary clauses 25% in total
c [quatres-7-1] removed 59 duplicate quaternary clauses
c [quatres-7-1] added 2 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1329 single-self-subsuming ternary resolvents
c [quatres-7-2] added 515 quaternary resolvents
c [ternres-7] limit 18451200 with penalty 0 = 0 + 0
c [ternres-7] all 31590 free variables schedulable
c [ternres-7] 6890 ternary resolvents (854 bin, 6036 trn)
c [ternres-7] 81 variables remain 0% (31509 retained 100%)
c [decomp-32] removed 169 variables
c [basicprobe-4] limit 92256004 penalty 0 = 0 + 0
c [basicprobe-4-0] 16553 sched 53%, 52 failed, 8 lifted, 2157 hbrs
c [decomp-33] removed 182 variables
c [basicprobe-4-1] 16451 sched 53%, 7 failed, 0 lifted, 154 hbrs
c [decomp-34] removed 17 variables
c [basicprobe-4-2] 16448 sched 53%, 0 failed, 0 lifted, 62 hbrs
c [decomp-35] removed 3 variables
c [basicprobe-4-3] 16441 sched 53%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-4-4] 16436 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-4] fully completed probing
c [basicprobe-4-4] 67 units = 59 failed (88%) + 8 lifted (12%)
c [basicprobe-4-4] removed 202 variables, found 2390 hbrs
c [bate-2] eliminated 542 asymmetric tautologies during probing
c [unhide-10] limit 3690240 with penalty 0 = 0 + 0
c [unhide-10-11] 0 units, 0 failed, 5978 tauts, 0 hbrs, 41945 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 420 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 31247 variables 100%
c [block-4] limit of 46128002 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 10580 blocked clauses
c [bca-7] limit of 10000000 steps and 434081 added (scaled 2)
c [bca-7] 39400 out of 60126 literals actually usable 66%
c [bca-7] added 184 blocked clauses in 191208 steps
c [sweep-7] limit 5535360 penalty 0 = 0 + 0
c [sweep-7-1] 14179 pos 52.3% + 12924 neg 47.7% = 27103 sched 90.2% ret 2959
c [sweep-7-1] 5550378 steps 298 queries 3269.24 avg class size
c [sweep-7-1] 8425 decisions 294 SAT calls 50.33 avg env size
c [sweep-7-1] 21127 variables remain 70% (8935 retained 30%)
c [decomp-37] removed 31 variables
c [sweep-7-1] removed 31 vars (0 failed, 10 eqs, 6 impls)
c [sweep-7] removed 31 vars in TOTAL (1 rounds, 297 queries)
c [sort-queue-11] sorted 13693 enqueued variables after 213550 conflicts
c [score-dist-11] active 16338 (54%), one 0 (0%), zero 13693 (46%)
c [score-dist-11] max exp 519, different 16 (3%)
c [score-dist-11] median active exp 519, avg 517.8
c [simplification-11] removed 1559 variables 4.9% (30031 remain 11%)
c [simplification-11] removed 14167 irredundant clauses 6.1% (216728 remain 27%)
c [simplification-11] maximum reduction of 6% = max (5%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] next conflict interval 2135 = min (213550/100, 57600)
c [simplification-11] penalized conflict interval 2135 = 1 * 2135
c [simplification-11] hard conflict limit 225685 (soft 215685 + delta 10000)
c [simplification-11] new conflict limit 215685 (hard 225685)
c 
c [simplification-12] limit 215685 conflicts (hard 225685) hit after 215687 conflicts
c [quatres-8] found 37370 quaternary clauses 25% in total
c [quatres-8-1] removed 70 duplicate quaternary clauses
c [quatres-8-1] added 5 double-self-subsuming ternary resolvents
c [quatres-8-2] added 133 single-self-subsuming ternary resolvents
c [quatres-8-2] added 272 quaternary resolvents
c [ternres-8] limit 18587700 with penalty 0 = 0 + 0
c [ternres-8] 78 schedulable variables 0%
c [ternres-8] 6615 ternary resolvents (569 bin, 6046 trn)
c [ternres-8] 1 variables remain 0% (30030 retained 100%)
c [decomp-38] removed 54 variables
c [simpleprobe-5] 3337 schedulable variables 11%
c [simpleprobe-5] limit 74350803 penalty 0 = 0 + 0
c [decomp-39] removed 44 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 44 variables, found 2892 hbrs, 10 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 860 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 29933 variables 100%
c [elim-9] limit of 185877007 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1634 variables 5% in round 1 in 154525018 steps
c [elim-9-1] backward subsumption/strengthening limit 31351989
c [elim-9-1-1] backward checking 4650 touched variables 16%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 9 and strengthened 12 clauses in 8056578 steps
c [elim-9-1] rescheduled 74 variables 0% by backward subsumption
c [elim-9-2] eliminated 3 variables 0% in round 2 in 13316363 steps
c [elim-9-2] backward subsumption/strengthening limit 9979048
c [elim-9-2-1] backward checking 10 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 459410 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1637 = 5% variables out of 29933 scheduled
c [bca-8] limit of 10000000 steps and 421279 added (scaled 2)
c [bca-8] 37649 out of 56594 literals actually usable 67%
c [bca-8] added 70 blocked clauses in 182323 steps
c [sweep-8] limit 5576310 penalty 0 = 0 + 0
c [sweep-8-1] 8802 pos 44.2% + 11091 neg 55.8% = 19893 sched 70.3% ret 8403
c [sweep-8-1] 5579314 steps 557 queries 1826.32 avg class size
c [sweep-8-1] 12554 decisions 550 SAT calls 35.20 avg env size
c [sweep-8-1] 14473 variables remain 51% (13813 retained 49%)
c [decomp-40] removed 38 variables
c [sweep-8-1] removed 38 vars (0 failed, 21 eqs, 15 impls)
c [sweep-8] removed 38 vars in TOTAL (1 rounds, 556 queries)
c [sort-queue-12] sorted 12967 enqueued variables after 215687 conflicts
c [score-dist-12] active 15291 (54%), one 0 (0%), zero 12967 (46%)
c [score-dist-12] max exp 519, different 16 (3%)
c [score-dist-12] median active exp 519, avg 517.8
c [simplification-12] removed 1773 variables 5.9% (28258 remain 11%)
c [simplification-12] removed 6669 irredundant clauses 3.1% (210059 remain 26%)
c [simplification-12] maximum reduction of 6% = max (6%, 3%)
c [simplification-12] large reduction 6% >= 5% limit
c [simplification-12] next conflict interval 2156 = min (215687/100, 57600)
c [simplification-12] penalized conflict interval 2156 = 1 * 2156
c [simplification-12] hard conflict limit 227843 (soft 217843 + delta 10000)
c [simplification-12] new conflict limit 217843 (hard 227843)
c 
c [simplification-13] limit 217843 conflicts (hard 227843) hit after 217843 conflicts
c [quatres-9] found 32299 quaternary clauses 23% in total
c [quatres-9-1] removed 26 duplicate quaternary clauses
c [quatres-9-2] added 56 single-self-subsuming ternary resolvents
c [quatres-9-2] added 643 quaternary resolvents
c [ternres-9] limit 18732203 with penalty 0 = 0 + 0
c [ternres-9] 1 schedulable variables 0%
c [ternres-9] 3858 ternary resolvents (162 bin, 3696 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-41] removed 4 variables
c [treelook-5] limit 1873220 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 22572 literals 40%
c [treelook-5] scheduling used 736513 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1873220 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1899652 steps
c [treelook-5] 22060 literals remain 39%
c [treelook-5] 6780 variables remain to probed next time 24%
c [treelook-5] removed 6 variables, found 478 hbrs
c [unhide-11] limit 1873220 with penalty 1 = 1 + 0
c [unhide-11-12] 0 units, 0 failed, 628 tauts, 0 hbrs, 5948 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 459 transitive binary clauses
c [transred-9] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 28247 variables 100%
c [block-5] limit of 93661015 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2099 blocked clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 27987 variables 100%
c [elim-10] limit of 374644060 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 172 variables 1% in round 1 in 144142731 steps
c [elim-10-1] backward subsumption/strengthening limit 144142700
c [elim-10-1-1] backward checking 965 touched variables 3%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 2 and strengthened 7 clauses in 3847901 steps
c [elim-10-1] rescheduled 14 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 14154918 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 172 = 1% variables out of 27987 scheduled
c [elim-10] 172 < 1/100 * 27987 = 279 considered unsuccessful
c [bca-9] limit of 10000000 steps and 415118 added (scaled 2)
c [bca-9] 36476 out of 55632 literals actually usable 66%
c [bca-9] added 48 blocked clauses in 179959 steps
c [sweep-9] limit 5619660 penalty 0 = 0 + 0
c [sweep-9-1] 6831 pos 47.9% + 7436 neg 52.1% = 14267 sched 51.3% ret 13548
c [sweep-9-1] 5621913 steps 682 queries 1785.75 avg class size
c [sweep-9-1] 14317 decisions 677 SAT calls 32.03 avg env size
c [sweep-9-1] 10974 variables remain 39% (16835 retained 61%)
c [decomp-43] removed 36 variables
c [sweep-9-1] removed 36 vars (0 failed, 25 eqs, 17 impls)
c [sweep-9] removed 36 vars in TOTAL (1 rounds, 681 queries)
c [sort-queue-13] sorted 12577 enqueued variables after 217843 conflicts
c [score-dist-13] active 15202 (55%), one 0 (0%), zero 12577 (45%)
c [score-dist-13] max exp 519, different 16 (3%)
c [score-dist-13] median active exp 519, avg 518.0
c [simplification-13] removed 479 variables 1.7% (27779 remain 10%)
c [simplification-13] removed 3004 irredundant clauses 1.4% (207055 remain 26%)
c [simplification-13] maximum reduction of 2% = max (2%, 1%)
c [simplification-13] geometric conflict interval increment 19200 = 57600 / 3
c [simplification-13] new conflict interval 76800
c [simplification-13] penalized conflict interval 76800 = 1 * 76800
c [simplification-13] hard conflict limit 333043 (soft 294643 + delta 38400)
c [simplification-13] new conflict limit 294643 (hard 333043)
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  115.3   27778   207055    252169   94815  22690  5610    8    89   49   9%    456  -17    8    8   93%
c -  115.9   27776   207055    254776   62034  22741  5614    9   100   43   9%   -163   -6   10    8  117%
c 
c [simplification-14] limit 294643 conflicts (hard 333043) hit after 294643 conflicts
c [quatres-10] found 34353 quaternary clauses 22% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 131 single-self-subsuming ternary resolvents
c [quatres-10-2] added 329 quaternary resolvents
c [ternres-10] limit 23237594 with penalty 0 = 0 + 0
c [ternres-10] all 27776 free variables schedulable
c [ternres-10] 3706 ternary resolvents (298 bin, 3408 trn)
c [ternres-10] 2 variables remain 0% (27774 retained 100%)
c [gauss-4] limit 580939 penalty 3 = 3 + 0
c [gauss-4] extracted 3448 xors of average arity 3.0
c [gauss-4] connected 10339 occurrences of 2829 variables (average 3.7)
c [gauss-4] limit 580939 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-44] removed 32 variables
c [basicprobe-5] limit 116187973 penalty 0 = 0 + 0
c [basicprobe-5-0] 14656 sched 53%, 27 failed, 0 lifted, 643 hbrs
c [decomp-45] removed 64 variables
c [basicprobe-5-1] 14605 sched 53%, 4 failed, 0 lifted, 43 hbrs
c [decomp-46] removed 7 variables
c [basicprobe-5-2] 14599 sched 53%, 0 failed, 0 lifted, 19 hbrs
c [decomp-47] removed 2 variables
c [basicprobe-5-3] 14601 sched 53%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-5-4] 14601 sched 53%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-5-5] 14601 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-5] fully completed probing
c [basicprobe-5-5] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-5-5] removed 73 variables, found 715 hbrs
c [bate-3] eliminated 118 asymmetric tautologies during probing
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 451 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 27671 variables 100%
c [block-6] limit of 232375946 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 460 blocked clauses
c [block-6] 460 < 1/100 * 206004 = 2060 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 145234966 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 159 (3%) of length 19
c [cce-4-1] eliminated 2 clauses out of 168 (1%) of length 18
c [cce-4-1] eliminated 1 clauses out of 227 (0%) of length 17
c [cce-4-1] eliminated 4 clauses out of 393 (1%) of length 16
c [cce-4-1] eliminated 12 clauses out of 464 (3%) of length 15
c [cce-4-1] eliminated 20 clauses out of 556 (4%) of length 14
c [cce-4-1] eliminated 23 clauses out of 725 (3%) of length 13
c [cce-4-1] eliminated 23 clauses out of 885 (3%) of length 12
c [cce-4-1] eliminated 137 clauses out of 1575 (9%) of length 11
c [cce-4-1] eliminated 203 clauses out of 2324 (9%) of length 10
c [cce-4-1] eliminated 389 clauses out of 4138 (9%) of length 9
c [cce-4-1] eliminated 1080 clauses out of 7168 (15%) of length 8
c [cce-4-1] eliminated 1624 clauses out of 14416 (11%) of length 7
c [cce-4-1] eliminated 1387 clauses out of 30363 (5%) of length 6
c [cce-4-1] eliminated 938 clauses out of 18587 (5%) of length 5
c [cce-4-1] eliminated 583 clauses out of 20037 (3%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 6430 large clauses in 124497050 steps
c [cce-4-1] allowing another 62248525 steps for small clauses
c [cce-4-1] scheduling 42203 clauses = 24495 binary + 17708 ternary
c [cce-4-1] tried to eliminate 42203 small clauses 100%
c [cce-4-1] eliminated 247 binary clauses 1%
c [cce-4-1] eliminated 494 ternary clauses 3%
c [cce-4-1] eliminated 741 small clauses 2%
c [cce-4-1] eliminated 741 small clauses in 91497193 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 7171 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 26868934 steps for small clauses
c [cce-4-2] scheduling 41466 clauses = 24248 binary + 17218 ternary
c [cce-4-2] tried to eliminate 41394 small clauses 100%
c [cce-4-2] eliminated 4 ternary clauses 0%
c [cce-4-2] eliminated 4 small clauses 0%
c [cce-4-2] eliminated 4 small clauses in 53737838 steps
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 4 covered clauses in round 2
c [cce-4] eliminated 7175 covered clauses in TOTAL during 2 rounds
c [bca-10] limit of 10000000 steps and 397446 added (scaled 2)
c [bca-10] 35466 out of 55258 literals actually usable 64%
c [bca-10] added 7 blocked clauses in 205649 steps
c [sweep-10] limit 6971278 penalty 0 = 0 + 0
c [sweep-10-1] 4877 pos 44.7% + 6045 neg 55.3% = 10922 sched 39.5% ret 16706
c [sweep-10-1] 6987466 steps 799 queries 1673.91 avg class size
c [sweep-10-1] 16905 decisions 796 SAT calls 31.62 avg env size
c [sweep-10-1] 8251 variables remain 30% (19377 retained 70%)
c [decomp-50] removed 24 variables
c [sweep-10-1] removed 24 vars (0 failed, 23 eqs, 10 impls)
c [sweep-10] 24 < 1/1000 * 27628 = 27 considered unsuccessful
c [sweep-10] removed 24 vars in TOTAL (1 rounds, 798 queries)
c [sort-queue-14] sorted 12196 enqueued variables after 294643 conflicts
c [score-dist-14] active 15408 (56%), one 0 (0%), zero 12196 (44%)
c [score-dist-14] max exp 520, different 17 (3%)
c [score-dist-14] median active exp 519, avg 518.6
c [simplification-14] removed 172 variables 0.6% (27604 remain 10%)
c [simplification-14] removed 8764 irredundant clauses 4.2% (198291 remain 25%)
c [simplification-14] maximum reduction of 4% = max (1%, 4%)
c [simplification-14] geometric conflict interval increment 15360 = 76800 / 5
c [simplification-14] new conflict interval 92160
c [simplification-14] penalized conflict interval 92160 = 1 * 92160
c [simplification-14] hard conflict limit 432883 (soft 386803 + delta 46080)
c [simplification-14] new conflict limit 386803 (hard 432883)
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 -  132.8   27604   198291    308094   73325  26119  5943    9    58   44  16%    472  -43    8    9   98%
c -  141.4   27604   198291    358406   83739  26861  5963    8   105   44   8%    768   17    9    9  102%
c i  148.2   27603   198291    390427  111964  27357  5996    9    21   52  42%    867  -53    7    9   75%
c i  150.1   27388   198291    398442  119145  27471  6009    8    43   52  20%  -1056  -28    8    9   90%
c i  151.0   27387   198291    402440  122585  27504  6012    8    27   52  29%  -1051  -42    6    9   70%
c -  151.7   27385   198291    405080   91612  27518  6014    8    19   45  40%  -1027  -48    7    9   77%
c i  152.0   27384   198291    406545   92848  27542  6024    7    16   49  44%   -986  -50    6    9   65%
c i  152.3   27333   198291    408051   94155  27551  6026    7    15   49  48%   -990  -49    8    9   97%
c i  152.6   27309   198291    409558   95377  27571  6032    7    14   49  51%   -973  -49    6    9   74%
c i  152.7   26818   198291    410216   95925  27577  6033    7    13   49  53%   -968  -50    6    8   65%
c i  152.8   26504   198291    410342   96025  27583  6033    7    13   49  53%   -968  -50    5    8   60%
c i  152.9   26489   198291    411235   96776  27592  6039    7    13   49  55%   -956  -50    6    8   67%
c i  153.0   26488   198291    411773   97187  27604  6048    7    12   49  56%   -950  -50    6    8   66%
c i  153.0   26391   198291    411813   97198  27609  6053    7    12   49  57%   -950  -50    5    8   63%
c i  153.0   26082   198291    411814   97198  27609  6053    7    12   49  57%   -950  -50    5    8   62%
c i  153.0   26037   198291    411842   97205  27616  6056    7    12   49  57%   -949  -50    5    8   60%
c i  153.0   25914   198291    411845   97205  27617  6057    7    12   49  57%   -949  -50    5    8   59%
c i  153.0   25786   198291    411847   97205  27617  6058    7    12   49  57%   -949  -50    5    8   59%
c 0  153.0   25736   198291    411847   97205  27617  6058    7    12   49  57%   -949  -50    5    8   59%
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: 920 basic ate = 142 trn 15% + 778 lrg 85% in 3 updates
c bcas: 10 count, 423 added (1757 skipped), 1868638 steps
c bkwd: tried 106472 clauses, 212685 lits, 2.00 lits/clause
c bkwd: checked 10221676 occs, 96.00 occs/clause, 48.06 occs/lit
c bkwd: subsumed 1 binary, 194 ternary, 31 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 74 large (0% self)
c blkd: 6 bces, 25111 removed, 9687619 resolutions, 24966541 steps
c blkd: 7003 blocking literals 1%, 2670 pure
c bump: 390851 bumped seen, 15625984 lits 40.0 on average
c card: 4 count, 0 units, 0 am1, 14323752 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 2383 subsumed
c card: 334 at-most-one constraints found, average size 3.02
c card: 334 at-most-one constraints used 100%, average size 3.02
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: 4 cces, 10299 eliminated, 10040 ate 97%, 259 abce 3%
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: 2666222 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 94 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 50 decompositions, 2135 equivalent 1%
c deco: 1 decision-only clauses 0%, 34% reduction
c decs: 5744528 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 236545 eliminated 88%, 104 pure 0%
c elms: 16 rounds, 1.6 rounds/bve
c elms: 222845 small 94%, 10926 large 5%
c elms: 298537 tried small, 222845 succeeded 75%, 75692 failed 25%
c elms: 7243 subsumed, 5941 strengthened, 473 blocked
c elms: 8525872 copies, 15025741 resolutions, 5753204 ipos
c elms: 6469931 subchks, 5800595 strchks
c gaus: 4 extractions, 34635 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8576106 steps, 4288053 extr 50%, 4328644 elim 50%
c glue: 8.6 orig avg, 8.6 real avg, 2.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 20318 = 4595 simple 23% + 14434 trn 71% + 1289 lrg 6%, 1577 sub 8%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 390851 clauses, 18.9 length
c lrnd: 7382516 lits = 10188819 orig - 2806303 removed 28%
c lrnd: 127704 uips 33%, 149379 flips 38%
c mins: 374222 mins 96%, 329 bin 0%, 16299 size 4%
c mins: 9765156 poisoned searches, 1455052 hits, 15% hit rate
c mins: 18019044 used twice searches, 1590827 hits, 9% hit rate
c move: moved 16539, 3968 bin 24%, 12571 trn 76%
c otfs: 23928 driving 51%, 22570 restarting 49%
c otfs: str 46498, 46316 red 100%, 182 irr 0%
c otfs: str 46498, 0 bin 0%, 376 trn 1%, 46122 lrg 99%
c otfs: sub 593, 581 red 98%, 12 irr 2%
c otfs: sub 593, 0 bin 0%, 72 trn 12%, 521 lrg 88%
c phas: 2 computed, 53960 set, 15086 pos (28%), 38874 neg (72%)
c prbs: 5 basic, 605990 probed, 422 failed, 36 lifted
c prbs: 5 simple, 509560 probed, 33 failed, 290 eqs
c prbs: 5 treelook, 1024 probed, 22 failed, 0 lifted
c prom: 42735 locked 12% out of 345878 tried
c prps: 232548539 props, 39 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 10 count, 14000 quat, 2959 self1, 24 self2, 402 dup
c queu: 14 sorted, 5744528 next (83121 steps 0.01)
c queu: 16194131 enq (368540699 steps 22.76), 15625984 deq 96%
c redc: 14287 clauses 9%, 162187 tried 39%, 9 sat 0%
c redc: 18740 lits 1%, 1494485 tried 15%, 9 sat 0%
c redc: 399 times jump level reduced, 9.4 levels on average
c reds: 6 count, 68641.2 conflicts per reduce
c reds: 0 memlim 0%, 6 arith 100%
c reds: 157583 collected 73%, 59707 retired 27%
c rmbd: 1223 removed, 703 red 57%
c rsts: 16402 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 14 count, 14 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 390851 count (161246 tried 0.4), 35414 sub out of 385237 (9.2%)
c swps: 10 count, 11 rounds, 7896 queries (717.8/round)
c swps: 7835 sat calls, 134 unsat (0.4% success rate)
c swps: 154425 decisions 19.7, 2932 conflicts 0.4
c swps; 1243.6 avg class size, 29.9 avg environment size
c swps: 0 failed, 124 impls, 193 equivs
c swp0: 2629 type 0 queries, 257 unsat (9.8%), 2592 sat (98.6%)
c swp1: 5267 type 1 queries, 1353 unsat (25.7%), 5111 sat (97.0%)
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: 12271083 calls to obtain time
c tops: 4632 fixed 2%, 52 its, 7920.13 confs/it
c trds: 10 transitive reductions, 3381 removed, 8 failed
c trds: 630601 nodes, 322475 edges, 4211178 steps
c trim: 450165 words, 1.7 MB
c trnr: 10 count, 2630 bin, 41729 trn, 135236187 steps
c unhd: 11 count, 12 rounds, 29547608 steps
c unhd: 436 non-trivial sccs of average size 2.1
c unhd: 14 units, 14 bin, 0 trn, 0 lrg
c unhd: 52 failed, 50 stamp, 0 lits, 2 bin, 0 trn, 0 lrg
c unhd: 13927 tauts, 147 bin 1%, 7516 trn 54%, 4487 lrg 32%
c unhd: 13927 tauts, 1777 stamp 13%, 11661 red 84%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 135446 str, 14 bin 0%, 1248 trn 1%, 134184 lrg 99%, 118499 red 87%
c vars: 25736 remaining 10% and 243312 removed 90% out of 269048
c vars: 4632 fixed 2%, 236545 eliminated 88%, 2135 equivalent 1%
c vsts: 3164943538 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 13.6 search visits per propagation, 7430.3 per conflict
c wchs: 663846028 pushed, 29235481 enlarged, 158 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         399237        157583         59707      17243626       1840458        180146
c 
c  0 0        112088  28      3255   2         0   0  12948810  75<  1034321  56     91590  51     2.3
c  1 5         40327  10     16462  10      6740  11   1716002  10    230248  13<    25279  14<    0.6
c  2 6         94496  24<    51181  32     16670  28   1695424  10    325409  18     35620  20     1.5
c  3 9         91096  23     52862  34<    18823  32<   683048   4    181240  10     20222  11     1.9
c  4 14        43039  11     24705  16     11204  19    161433   1     53711   3      5830   3     1.0
c  5 21        13391   3      7000   4      4328   7     31257   0     12165   1      1261   1     0.5
c  6 30         3467   1      1615   1      1353   2      5690   0      2511   0       266   0     0.2
c  7 41          942   0       383   0       419   1      1445   0       646   0        56   0     0.1
c  8 54          242   0        75   0       104   0       325   0       128   0        16   0     0.0
c  9 69          106   0        34   0        47   0       136   0        59   0         3   0     0.0
c 10 86           41   0        11   0        17   0        53   0        20   0         3   0     0.0
c 11 126           1   0         0   0         1   0         2   0         0   0         0   0     0.0
c 12 230           1   0         0   0         1   0         1   0         0   0         0   0     0.0
c 
c avg                  1.9           2.7           2.9           0.5           0.9           1.0
c std                  1.6           1.2           1.3           0.9           1.2           1.3
c 
c   17.991  12% elim
c   10.074   7% probe
c    6.472   4% sweep
c    5.867   4% bump
c    4.184   3% decide
c    4.058   3% cce
c    2.908   2% unhide
c    2.468   2% block
c    1.678   1% quatres
c    1.449   1% bca
c    1.300   1% ternres
c 
c    1.741 < 1% rest (below)
c 
c    0.994   1% gauss
c    0.379   0% card
c    0.368   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.742   4% preprocessing    11%
c   48.383  32% inprocessing     89%
c ==================================
c   54.125  35% simplifying
c   98.906  65% search
c ==================================
c  153.036 100% all
c 
c        411847 conflicts,        2691.2 confs/sec
c          4329 ternaries,          95.1 confs/ternary
c           569 binaries,          723.8 confs/binary
c            52 iterations,       7920.1 confs/iteration
c 
c             6 reductions,          0.0 redus/sec,  68641.2 confs/reduction
c         16402 restarts,          107.2 rests/sec,     25.1 confs/restart
c       5744528 decisions,       37537.1 decis/sec,     13.9 decis/conflict
c     232548539 propagations,  1519565.6 props/sec,     40.5 props/decision
c 
c 153.0 seconds, 84.0 MB
c launch: done
