c launch: /data/cnf/sc2014/app/manol-pipe-c10nidw.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-c10nidw.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-c10nidw.cnf.bz2
c no embedded options
c found 'p cnf 433601 1291714' header
c read 433601 variables, 1291714 clauses, 3013998 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 433600 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  433600  1291713         0       0      0     0    0     0   73   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 2 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] 2 out of 2 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 433600 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 506 variables
c [simpleprobe-1] 181013 variables remain 42% (252081 retained 58%)
c [simpleprobe-1] removed 506 variables, found 1058 hbrs, 10 units
c [unhide-1] limit 80637 based on 1290202 irredundant clauses
c [unhide-1-1] 0 units, 64 failed, 105 tauts, 0 hbrs, 114 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 431402 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 189604 not tried 44% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 241798 = 56% variables out of 431402 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 744044 negative 95.9% of 775692 except 31648 4.1%
c [phase-count-1] 716116 positive 92.3% of 775692 except 59576 7.7%
c [phase-1] phase bias: 59937 positive 32%, 129667 negative 68%
c [sort-queue-1] sorted 189604 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 189604 (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 243996 variables 56.3% (189604 remain 44%)
c [simplification-1] removed 516021 irredundant clauses 39.9% (775692 remain 60%)
c [simplification-1] maximum reduction of 56% = max (56%, 40%)
c [simplification-1] large reduction 56% >= 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    7.6  189603   775692         1       0      0   154    0     0   66   0%      0    0    0    0    0%
c i    7.6  189477   775692        22      13      3   157    0     0   67   3%      0    0    0    0 24672%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1010 conflicts
c [decomp-3] removed 500 variables
c [simpleprobe-2] 78860 schedulable variables 42%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 2 variables
c [simpleprobe-2] 78869 variables remain 42% (110233 retained 58%)
c [simpleprobe-2] removed 2 variables, found 10 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 46678 literals 12%
c [treelook-1] scheduling used 300482 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300584 steps
c [treelook-1] 46549 literals remain 12%
c [treelook-1] 45534 variables remain to probed next time 24%
c [decomp-5] removed 2 variables
c [treelook-1] removed 3 variables, found 355 hbrs
c [basicprobe-1] limit 6189336 based on 773667 irredundant clauses
c [basicprobe-1-0] 142165 probes remain 76% after last round
c [basicprobe-1-0] 373 units = 211 failed (57%) + 162 lifted (43%)
c [basicprobe-1-0] removed 2125 variables, found 6216 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 11 units, 69 failed, 422 tauts, 0 hbrs, 2263 literals
c [elim-2] 186572 variables 100% will be scheduled this time
c [elim-2] scheduled 186572 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 77079 not tried 41% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 109312 = 59% variables out of 186572 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 479795 negative 97.4% of 492474 except 12679 2.6%
c [phase-count-2] 473002 positive 96.0% of 492474 except 19472 4.0%
c [phase-2] phase bias: 13 positive 10%, 112 negative 90%
c [sort-queue-2] sorted 70744 enqueued variables after 1010 conflicts
c [score-dist-2] active 6516 (8%), one 0 (0%), zero 70744 (92%)
c [score-dist-2] max exp 511, different 11 (2%)
c [score-dist-2] median active exp 510, avg 509.8
c [simplification-2] removed 112185 variables 59.2% (77260 remain 18%)
c [simplification-2] removed 283218 irredundant clauses 36.5% (492474 remain 38%)
c [simplification-2] maximum reduction of 59% = max (59%, 37%)
c [simplification-2] large reduction 59% >= 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 13010 (soft 3010 + delta 10000)
c [simplification-2] new conflict limit 3010 (hard 13010)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.2   77259   492473      2352    1102    106  1350    3    66   60   5%     22   65   10    0 3773%
c 
c [simplification-3] limit 3010 conflicts (hard 13010) hit after 3011 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 35 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] 35 out of 35 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 115 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 20513 literals 13%
c [treelook-2] scheduling used 300034 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 448880 steps
c [treelook-2] 20404 literals remain 13%
c [treelook-2] 9853 variables remain to probed next time 13%
c [decomp-7] removed 1 variables
c [treelook-2] removed 2 variables, found 394 hbrs
c [unhide-3] limit 123474 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 8 failed, 1292 tauts, 0 hbrs, 4116 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 76985 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 22697 not tried 29% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 14518 = 19% variables out of 76985 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 449043 negative 97.3% of 461467 except 12424 2.7%
c [phase-count-3] 447042 positive 96.9% of 461467 except 14425 3.1%
c [phase-3] phase bias: 5 positive 9%, 52 negative 91%
c [sort-queue-3] sorted 52557 enqueued variables after 3011 conflicts
c [score-dist-3] active 9910 (16%), one 0 (0%), zero 52557 (84%)
c [score-dist-3] max exp 513, different 13 (3%)
c [score-dist-3] median active exp 512, avg 511.5
c [simplification-3] removed 14789 variables 19.1% (62467 remain 14%)
c [simplification-3] removed 31006 irredundant clauses 6.3% (461467 remain 36%)
c [simplification-3] maximum reduction of 19% = max (19%, 6%)
c [simplification-3] large reduction 19% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15011 (soft 5011 + delta 10000)
c [simplification-3] new conflict limit 5011 (hard 15011)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.4   62466   461467      3826    1513    146   771    5    89   60   6%     15   86   12    0 2509%
c i   19.4   62445   461467      3829    1512    147   771    5    89   60   6%     15   86   12    0 2492%
c i   19.4   62439   461467      3831    1512    147   771    5    89   60   6%     15   86   12    0 2482%
c i   19.4   62438   461467      3833    1512    147   771    5    89   60   6%     15   86   12    0 2472%
c i   19.4   62437   461466      3837    1512    147   771    5    89   60   6%     15   86   12    0 2463%
c i   19.4   62436   461466      3839    1512    147   771    5    89   60   6%     15   86   12    0 2453%
c i   19.5   62435   461465      4081    1679    162   777    6    91   60   6%     12   88   10    0 1978%
c 
c [simplification-4] limit 5031 conflicts (hard 15011) hit after 5032 conflicts
c [decomp-8] removed 114 variables
c [basicprobe-2] limit 4028904 penalty 0 = 0 + 0
c [basicprobe-2-0] 16671 probes remain 27% after last round
c [basicprobe-2-0] 174 units = 166 failed (95%) + 8 lifted (5%)
c [basicprobe-2-0] removed 1473 variables, found 2930 hbrs
c [unhide-4] limit 161156 with penalty 0 = 0 + 0
c [unhide-4-4] 5 units, 20 failed, 118 tauts, 0 hbrs, 7049 literals
c [elim-4] 22015 variables 36% will be scheduled this time
c [elim-4] scheduled 22015 variables 36%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2119 variables 3% in round 1 in 267038942 steps
c [elim-4-1] backward subsumption/strengthening limit 132961058
c [elim-4-1-1] backward checking 13996 touched variables 23%
c [elim-4-1-1] incomplete backward checking 3197 remain 23%
c [elim-4-1] subsumed 734 and strengthened 1855 clauses in 132961218 steps
c [elim-4] incomplete 1790 not tried 3% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 2133 = 10% variables out of 22015 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 419215 negative 97.1% of 431669 except 12454 2.9%
c [phase-count-4] 421633 positive 97.7% of 431669 except 10036 2.3%
c [phase-4] phase bias: 16 positive 80%, 4 negative 20%
c [sort-queue-4] sorted 47857 enqueued variables after 5032 conflicts
c [score-dist-4] active 10869 (19%), one 0 (0%), zero 47857 (81%)
c [score-dist-4] max exp 514, different 14 (3%)
c [score-dist-4] median active exp 512, avg 512.0
c [simplification-4] removed 3708 variables 5.9% (58726 remain 14%)
c [simplification-4] removed 29796 irredundant clauses 6.5% (431669 remain 33%)
c [simplification-4] maximum reduction of 6% = max (6%, 6%)
c [simplification-4] large reduction 6% >= 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 17032 (soft 7032 + delta 10000)
c [simplification-4] new conflict limit 7032 (hard 17032)
c 
c [simplification-5] limit 7032 conflicts (hard 17032) hit after 7032 conflicts
c [quatres-1] found 39993 quaternary clauses 19% in total
c [quatres-1-2] added 9 single-self-subsuming ternary resolvents
c [quatres-1-2] added 5959 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 58726 free variables schedulable
c [ternres-1] 6256 ternary resolvents (98 bin, 6158 trn)
c [ternres-1] 1127 variables remain 2% (57599 retained 98%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 17363 xors of average arity 3.0
c [gauss-1] connected 52015 occurrences of 9311 variables (average 5.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [decomp-9] removed 113 variables
c [gauss-1] exported 0 unary, 1 binary and 0 ternary equations
c [simpleprobe-3] 24351 schedulable variables 42%
c [simpleprobe-3] limit 4019181 penalty 0 = 0 + 0
c [decomp-11] removed 1 variables
c [simpleprobe-3] 24377 variables remain 42% (34235 retained 58%)
c [simpleprobe-3] removed 1 variables, found 38 hbrs, 0 units
c [unhide-5] limit 200959 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 6 failed, 287 tauts, 0 hbrs, 3286 literals
c [transred-1] limit 1004795 with penalty 0 = 0 + 0
c [transred-1] removed 171 transitive binary clauses
c [transred-1] found 4 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 58592 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 10719 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 44
c [cce-1-1] eliminated 2 clauses out of 19 (11%) of length 33
c [cce-1-1] eliminated 1 clauses out of 51 (2%) of length 30
c [cce-1-1] eliminated 2 clauses out of 95 (2%) of length 28
c [cce-1-1] eliminated 7 clauses out of 150 (5%) of length 27
c [cce-1-1] eliminated 1 clauses out of 102 (1%) of length 26
c [cce-1-1] eliminated 1 clauses out of 172 (1%) of length 25
c [cce-1-1] eliminated 20 clauses out of 241 (8%) of length 24
c [cce-1-1] eliminated 4 clauses out of 279 (1%) of length 23
c [cce-1-1] eliminated 14 clauses out of 229 (6%) of length 22
c [cce-1-1] eliminated 13 clauses out of 280 (5%) of length 21
c [cce-1-1] eliminated 5 clauses out of 325 (2%) of length 20
c [cce-1-1] eliminated 19 clauses out of 612 (3%) of length 19
c [cce-1-1] eliminated 54 clauses out of 715 (8%) of length 18
c [cce-1-1] eliminated 51 clauses out of 549 (9%) of length 17
c [cce-1-1] eliminated 82 clauses out of 969 (8%) of length 16
c [cce-1-1] eliminated 114 clauses out of 846 (13%) of length 15
c [cce-1-1] eliminated 124 clauses out of 1005 (12%) of length 14
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 515 large clauses in 30000020 steps
c [cce-1-1] allowing another 15000010 steps for small clauses
c [cce-1-1] scheduling 125221 clauses = 56024 binary + 69197 ternary
c [cce-1-1] tried to eliminate 11038 small clauses 9%
c [cce-1-1] eliminated 145 binary clauses 0%
c [cce-1-1] eliminated 67 ternary clauses 0%
c [cce-1-1] eliminated 212 small clauses 0%
c [cce-1-1] eliminated 212 small clauses in 30000157 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 727 covered clauses in round 1
c [cce-1] eliminated 727 covered clauses in TOTAL during 1 rounds
c [cce-1] 727 < 1/100 * 419933 = 4199 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 57842 variables 100%
c [elim-5] limit of 20095907 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 8011 not tried 14% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2447 = 4% variables out of 57842 scheduled
c [bca-1] limit of 10000000 steps and 827532 added (scaled 2)
c [bca-1] 96622 out of 110792 literals actually usable 87%
c [bca-1] added 521 blocked clauses in 298628 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 19617 pos 35.4% + 35778 neg 64.6% = 55395 sched 100.0% ret 0
c [sweep-1-1] 1002308 steps 88 queries 14899.77 avg class size
c [sweep-1-1] 2525 decisions 86 SAT calls 55.00 avg env size
c [sweep-1-1] 53963 variables remain 97% (1432 retained 3%)
c [decomp-12] removed 2 variables
c [sweep-1-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 2 vars in TOTAL (1 rounds, 87 queries)
c [phase-count-5] 401781 negative 97.2% of 413515 except 11734 2.8%
c [phase-count-5] 403785 positive 97.6% of 413515 except 9730 2.4%
c [phase-5] phase bias: 15 positive 100%, 0 negative 0%
c [sort-queue-5] sorted 42324 enqueued variables after 7032 conflicts
c [score-dist-5] active 13069 (24%), one 0 (0%), zero 42324 (76%)
c [score-dist-5] max exp 514, different 12 (2%)
c [score-dist-5] median active exp 513, avg 512.8
c [simplification-5] removed 3333 variables 5.7% (55393 remain 13%)
c [simplification-5] removed 18154 irredundant clauses 4.2% (413515 remain 32%)
c [simplification-5] maximum reduction of 6% = max (6%, 4%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19032 (soft 9032 + delta 10000)
c [simplification-5] new conflict limit 9032 (hard 19032)
c 
c [simplification-6] limit 9032 conflicts (hard 19032) hit after 9032 conflicts
c [quatres-2] found 42578 quaternary clauses 20% in total
c [quatres-2-1] added 14 double-self-subsuming ternary resolvents
c [quatres-2-2] added 188 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2612 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1067 schedulable variables 2%
c [ternres-2] 2817 ternary resolvents (129 bin, 2688 trn)
c [ternres-2] 514 variables remain 1% (54879 retained 99%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 110 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 110 out of 110 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 16735 xors of average arity 3.0
c [gauss-2] connected 50198 occurrences of 8800 variables (average 5.7)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 8 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 11139 literals 10%
c [treelook-3] scheduling used 300069 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 304124 steps
c [treelook-3] 11105 literals remain 10%
c [treelook-3] 4312 variables remain to probed next time 8%
c [decomp-14] removed 4 variables
c [treelook-3] removed 18 variables, found 78 hbrs
c [unhide-6] limit 238833 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 6 failed, 675 tauts, 0 hbrs, 3931 literals
c [transred-2] limit 1194165 with penalty 0 = 0 + 0
c [transred-2] removed 67 transitive binary clauses
c [transred-2] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 55349 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 725 blocked clauses
c [block-2] 725 < 1/100 * 413219 = 4132 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 55309 variables 100%
c [elim-6] limit of 23883316 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 6566 not tried 12% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 186 = 0% variables out of 55309 scheduled
c [elim-6] 186 < 1/100 * 55309 = 553 considered unsuccessful
c [bca-2] limit of 10000000 steps and 824028 added (scaled 2)
c [bca-2] 93697 out of 110248 literals actually usable 85%
c [bca-2] added 4 blocked clauses in 292376 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 18233 pos 34.0% + 35464 neg 66.0% = 53697 sched 97.4% ret 1426
c [sweep-2-1] 1014244 steps 81 queries 14201.93 avg class size
c [sweep-2-1] 2670 decisions 77 SAT calls 53.48 avg env size
c [sweep-2-1] 52798 variables remain 96% (2325 retained 4%)
c [decomp-15] removed 5 variables
c [sweep-2-1] removed 5 vars (0 failed, 3 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 5 vars in TOTAL (1 rounds, 80 queries)
c [phase-count-6] 399952 negative 97.2% of 411616 except 11664 2.8%
c [phase-count-6] 401902 positive 97.6% of 411616 except 9714 2.4%
c [phase-6] phase bias: 1 positive 50%, 1 negative 50%
c [sort-queue-6] sorted 40954 enqueued variables after 9032 conflicts
c [score-dist-6] active 14164 (26%), one 0 (0%), zero 40954 (74%)
c [score-dist-6] max exp 514, different 12 (2%)
c [score-dist-6] median active exp 514, avg 513.0
c [simplification-6] removed 275 variables 0.5% (55118 remain 13%)
c [simplification-6] removed 1898 irredundant clauses 0.5% (411616 remain 32%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 20000
c [simplification-6] new conflict interval 20000
c [simplification-6] penalized conflict interval 20000 = 1 * 20000
c [simplification-6] hard conflict limit 39032 (soft 29032 + delta 10000)
c [simplification-6] new conflict limit 29032 (hard 39032)
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.5   55117   411616     17243   18241  10145  3042   11   184   60   6%    172  158   14    2  637%
c i   43.9   55112   411616     18265   19047  10185  3044   11   181   60   6%     57  152   14    2  598%
c i   46.0   55111   411616     23654   22930  10394  3078   10   156   60   7%     48  117   10    3  362%
c i   46.0   55110   411616     23655   22930  10394  3078   10   156   60   7%     48  117   10    3  361%
c i   46.0   55104   411616     23656   22930  10394  3078   10   156   60   7%     48  117   10    3  359%
c i   46.5   55097   411616     24400   23462  10424  3087   10   173   61   6%     15  133   10    3  330%
c i   46.8   55094   411616     25058   23997  10447  3088   10   174   61   6%      1  133   12    3  397%
c i   48.8   55054   411616     28986   26931  10606  3098   10   178   61   6%     25  129    9    3  277%
c 
c [simplification-7] limit 29052 conflicts (hard 39032) hit after 29052 conflicts
c [quatres-3] found 45470 quaternary clauses 21% in total
c [quatres-3-2] added 133 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1836 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 497 schedulable variables 1%
c [ternres-3] 4874 ternary resolvents (113 bin, 4761 trn)
c [ternres-3] 53 variables remain 0% (54993 retained 100%)
c [decomp-16] removed 113 variables
c [basicprobe-3] limit 18377585 penalty 0 = 0 + 0
c [basicprobe-3-0] 15164 sched 28%, 107 failed, 2 lifted, 2306 hbrs
c [decomp-17] removed 446 variables
c [basicprobe-3-1] 29226 sched 54%, 74 failed, 0 lifted, 1354 hbrs
c [decomp-18] removed 126 variables
c [basicprobe-3-2] 29103 sched 53%, 7 failed, 0 lifted, 201 hbrs
c [decomp-19] removed 20 variables
c [basicprobe-3-3] 8986 probes remain 17% after last round
c [basicprobe-3-3] 191 units = 189 failed (99%) + 2 lifted (1%)
c [basicprobe-3-3] removed 593 variables, found 3905 hbrs
c [bate-1] eliminated 519 asymmetric tautologies during probing
c [unhide-7] limit 735103 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 655 tauts, 0 hbrs, 7063 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 285 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 124 (2%) of length 25
c [cce-2-1] eliminated 1 clauses out of 172 (1%) of length 23
c [cce-2-1] eliminated 2 clauses out of 279 (1%) of length 22
c [cce-2-1] eliminated 4 clauses out of 303 (1%) of length 20
c [cce-2-1] eliminated 6 clauses out of 449 (1%) of length 19
c [cce-2-1] eliminated 12 clauses out of 697 (2%) of length 18
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 27 large clauses in 15000065 steps
c [cce-2-1] allowing another 7500032 steps for small clauses
c [cce-2-1] scheduling 117264 clauses = 51254 binary + 66010 ternary
c [cce-2-1] tried to eliminate 6308 small clauses 5%
c [cce-2-1] eliminated 43 binary clauses 0%
c [cce-2-1] eliminated 56 ternary clauses 0%
c [cce-2-1] eliminated 99 small clauses 0%
c [cce-2-1] eliminated 99 small clauses in 15000072 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 126 covered clauses in round 1
c [cce-2] eliminated 126 covered clauses in TOTAL during 1 rounds
c [cce-2] 126 < 1/100 * 402746 = 4027 considered unsuccessful
c [bca-3] limit of 10000000 steps and 806002 added (scaled 2)
c [bca-3] 81526 out of 108826 literals actually usable 75%
c [bca-3] added 13 blocked clauses in 266387 steps
c [sweep-3] limit 1102655 penalty 0 = 0 + 0
c [sweep-3-1] 22516 pos 43.1% + 29687 neg 56.9% = 52203 sched 95.9% ret 2209
c [sweep-3-1] 1105306 steps 110 queries 13984.47 avg class size
c [sweep-3-1] 2789 decisions 109 SAT calls 40.41 avg env size
c [sweep-3-1] 50998 variables remain 94% (3414 retained 6%)
c [decomp-20] removed 2 variables
c [sweep-3-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 2 vars in TOTAL (1 rounds, 109 queries)
c [sort-queue-7] sorted 29180 enqueued variables after 29052 conflicts
c [score-dist-7] active 25230 (46%), one 0 (0%), zero 29180 (54%)
c [score-dist-7] max exp 516, different 13 (3%)
c [score-dist-7] median active exp 516, avg 515.1
c [simplification-7] removed 636 variables 1.2% (54410 remain 13%)
c [simplification-7] removed 8998 irredundant clauses 2.2% (402618 remain 31%)
c [simplification-7] maximum reduction of 2% = max (1%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 26666
c [simplification-7] penalized conflict interval 26666 = 1 * 26666
c [simplification-7] hard conflict limit 69051 (soft 55718 + delta 13333)
c [simplification-7] new conflict limit 55718 (hard 69051)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   59.0   54409   402617     41411   37472  15091  4874   10   168   62   6%    145  101    9    4  197%
c i   64.0   54406   402617     53692   46588  15543  4922    9   139   64   7%    132   60    7    5  136%
c 
c [simplification-8] limit 55718 conflicts (hard 69051) hit after 57225 conflicts
c [quatres-4] found 47750 quaternary clauses 22% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 4 double-self-subsuming ternary resolvents
c [quatres-4-2] added 78 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1072 quaternary resolvents
c [ternres-4] limit 7174829 with penalty 0 = 0 + 0
c [ternres-4] 50 schedulable variables 0%
c [ternres-4] 3955 ternary resolvents (37 bin, 3918 trn)
c [ternres-4] 5 variables remain 0% (54398 retained 100%)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 7025 xors of average arity 3.0
c [gauss-3] connected 21069 occurrences of 3422 variables (average 6.2)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-21] removed 29 variables
c [simpleprobe-4] 22677 schedulable variables 42%
c [simpleprobe-4] limit 28699319 penalty 0 = 0 + 0
c [decomp-22] removed 4 variables
c [simpleprobe-4] 20643 variables remain 38% (33727 retained 62%)
c [simpleprobe-4] removed 4 variables, found 315 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 263 transitive binary clauses
c [transred-4] found 7 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 54336 variables 100%
c [block-3] limit of 35874149 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 3392 blocked clauses
c [block-3] 3392 < 1/100 * 402429 = 4024 considered unsuccessful
c [elim-7] 6341 variables 12% will be scheduled this time
c [elim-7] scheduled 6341 variables 12%
c [elim-7] limit of 71748298 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 2165 not tried 4% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 0 = 0% variables out of 6341 scheduled
c [bca-4] limit of 10000000 steps and 797161 added (scaled 2)
c [bca-4] 75533 out of 107590 literals actually usable 70%
c [bca-4] added 3 blocked clauses in 270397 steps
c [sweep-4] limit 2152448 penalty 0 = 0 + 0
c [sweep-4-1] 20119 pos 39.9% + 30294 neg 60.1% = 50413 sched 93.7% ret 3381
c [sweep-4-1] 2291083 steps 169 queries 8722.10 avg class size
c [sweep-4-1] 4568 decisions 167 SAT calls 47.19 avg env size
c [sweep-4-1] 48306 variables remain 90% (5484 retained 10%)
c [decomp-23] removed 26 variables
c [sweep-4-1] removed 26 vars (0 failed, 3 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 26 vars in TOTAL (1 rounds, 168 queries)
c [sort-queue-8] sorted 25909 enqueued variables after 57225 conflicts
c [score-dist-8] active 27859 (52%), one 0 (0%), zero 25909 (48%)
c [score-dist-8] max exp 517, different 14 (3%)
c [score-dist-8] median active exp 516, avg 515.9
c [simplification-8] removed 635 variables 1.2% (53768 remain 12%)
c [simplification-8] removed 4611 irredundant clauses 1.1% (398006 remain 31%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-8] new conflict interval 39999
c [simplification-8] penalized conflict interval 39999 = 1 * 39999
c [simplification-8] hard conflict limit 117223 (soft 97224 + delta 19999)
c [simplification-8] new conflict limit 97224 (hard 117223)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   76.2   53767   398006     70919   60415  19300  4885   10   143   66   7%    188   53   12    6  195%
c -   86.7   53739   398006     92636   33158  19949  4933    9   126   61   7%    228   24    9    7  133%
c 
c [simplification-9] limit 97224 conflicts (hard 117223) hit after 97225 conflicts
c [quatres-5] found 49920 quaternary clauses 22% in total
c [quatres-5-1] removed 4 duplicate quaternary clauses
c [quatres-5-1] added 5 double-self-subsuming ternary resolvents
c [quatres-5-2] added 42 single-self-subsuming ternary resolvents
c [quatres-5-2] added 595 quaternary resolvents
c [ternres-5] limit 12475799 with penalty 0 = 0 + 0
c [ternres-5] 5 schedulable variables 0%
c [ternres-5] 7389 ternary resolvents (53 bin, 7336 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-24] removed 104 variables
c [treelook-4] limit 1247579 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 18323 literals 17%
c [treelook-4] scheduling used 977464 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1247579 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1301149 steps
c [treelook-4] 18272 literals remain 17%
c [treelook-4] 3858 variables remain to probed next time 7%
c [treelook-4] removed 1 variables, found 483 hbrs
c [unhide-8] limit 1247579 with penalty 1 = 1 + 0
c [unhide-8-8] 1 units, 7 failed, 1777 tauts, 0 hbrs, 9166 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 195 transitive binary clauses
c [transred-5] found 3 units
c [bca-5] limit of 10000000 steps and 793738 added (scaled 2)
c [bca-5] 83674 out of 107270 literals actually usable 78%
c [bca-5] added 20 blocked clauses in 288167 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 37427390 penalty 0 = 0 + 0
c [sweep-5-1] 18382 pos 38.1% + 29825 neg 61.9% = 48207 sched 89.9% ret 5427
c [sweep-5-1] 37428388 steps 3605 queries 1081.10 avg class size
c [sweep-5-1] 60224 decisions 3562 SAT calls 24.76 avg env size
c [sweep-5-1] 14584 variables remain 27% (39028 retained 73%)
c [decomp-26] removed 202 variables
c [sweep-5-1] removed 202 vars (0 failed, 102 eqs, 63 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 202 vars in TOTAL (1 rounds, 3604 queries)
c [sort-queue-9] sorted 24069 enqueued variables after 97225 conflicts
c [score-dist-9] active 29363 (55%), one 0 (0%), zero 24069 (45%)
c [score-dist-9] max exp 518, different 15 (3%)
c [score-dist-9] median active exp 517, avg 516.7
c [simplification-9] removed 307 variables 0.6% (53432 remain 12%)
c [simplification-9] removed 2786 irredundant clauses 0.7% (395220 remain 31%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 19999 = 39999 / 2
c [simplification-9] new conflict interval 59998
c [simplification-9] penalized conflict interval 59998 = 1 * 59998
c [simplification-9] hard conflict limit 187222 (soft 157223 + delta 29999)
c [simplification-9] new conflict limit 157223 (hard 187222)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  112.0   53431   395220    163918   92704  25294  5306    7    42   69  18%    756  -58    6    8   75%
c -  113.2   53286   395220    167129   56459  25393  5313    8    77   62  11%   -573  -22    8    8  100%
c i  114.1   53285   395220    170722   59269  25480  5319    9   129   64   7%   -547   30   11    8  140%
c i  115.0   53279   395220    173574   61510  25561  5326    9   130   64   7%   -578   31   10    8  124%
c 
c [simplification-10] limit 157223 conflicts (hard 187222) hit after 187223 conflicts
c [quatres-6] found 52712 quaternary clauses 23% in total
c [quatres-6-1] removed 15 duplicate quaternary clauses
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 239 single-self-subsuming ternary resolvents
c [quatres-6-2] added 820 quaternary resolvents
c [ternres-6] limit 19408329 with penalty 0 = 0 + 0
c [ternres-6] all 53269 free variables schedulable
c [ternres-6] 2666 ternary resolvents (23 bin, 2643 trn)
c [ternres-6] 2764 variables remain 5% (50505 retained 95%)
c [card-4] limit 1213020 penalty 3 = 3 + 0
c [card-4] found 193 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1213020 for elimination
c [card-4] 193 out of 193 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-27] removed 454 variables
c [basicprobe-4] limit 97041646 penalty 0 = 0 + 0
c [basicprobe-4-0] 8897 sched 17%, 41 failed, 0 lifted, 1688 hbrs
c [decomp-28] removed 160 variables
c [basicprobe-4-1] 28114 sched 53%, 38 failed, 1 lifted, 2079 hbrs
c [decomp-29] removed 162 variables
c [basicprobe-4-2] 28009 sched 53%, 2 failed, 0 lifted, 99 hbrs
c [decomp-30] removed 6 variables
c [basicprobe-4-3] 28007 sched 53%, 1 failed, 0 lifted, 21 hbrs
c [decomp-31] removed 3 variables
c [basicprobe-4-4] 28005 sched 53%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-4-5] 28002 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-5] fully completed probing
c [basicprobe-4-5] 83 units = 82 failed (99%) + 1 lifted (1%)
c [basicprobe-4-5] removed 331 variables, found 3891 hbrs
c [bate-2] eliminated 424 asymmetric tautologies during probing
c [unhide-9] limit 3881665 with penalty 0 = 0 + 0
c [unhide-9-9] 0 units, 0 failed, 2124 tauts, 0 hbrs, 22054 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 562 transitive binary clauses
c [cce-3] limit of 24260411 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 91 (4%) of length 27
c [cce-3-1] eliminated 19 clauses out of 128 (15%) of length 26
c [cce-3-1] eliminated 15 clauses out of 234 (6%) of length 24
c [cce-3-1] eliminated 1 clauses out of 175 (1%) of length 23
c [cce-3-1] eliminated 20 clauses out of 266 (8%) of length 22
c [cce-3-1] eliminated 21 clauses out of 258 (8%) of length 21
c [cce-3-1] eliminated 11 clauses out of 295 (4%) of length 20
c [cce-3-1] eliminated 29 clauses out of 425 (7%) of length 19
c [cce-3-1] eliminated 38 clauses out of 662 (6%) of length 18
c [cce-3-1] eliminated 28 clauses out of 530 (5%) of length 17
c [cce-3-1] eliminated 77 clauses out of 907 (8%) of length 16
c [cce-3-1] eliminated 72 clauses out of 822 (9%) of length 15
c [cce-3-1] eliminated 3 clauses out of 863 (0%) of length 14
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 338 large clauses in 24261298 steps
c [cce-3-1] allowing another 12130649 steps for small clauses
c [cce-3-1] scheduling 136339 clauses = 49734 binary + 86605 ternary
c [cce-3-1] tried to eliminate 8059 small clauses 6%
c [cce-3-1] eliminated 108 binary clauses 0%
c [cce-3-1] eliminated 236 ternary clauses 0%
c [cce-3-1] eliminated 344 small clauses 0%
c [cce-3-1] eliminated 344 small clauses in 24260450 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 682 covered clauses in round 1
c [cce-3] eliminated 682 covered clauses in TOTAL during 1 rounds
c [cce-3] 682 < 1/100 * 386047 = 3860 considered unsuccessful
c [bca-6] limit of 10000000 steps and 771510 added (scaled 2)
c [bca-6] 77890 out of 105296 literals actually usable 74%
c [bca-6] added 21 blocked clauses in 299070 steps
c [sweep-6] limit 5822498 penalty 0 = 0 + 0
c [sweep-6-1] 6880 pos 47.5% + 7594 neg 52.5% = 14474 sched 27.5% ret 38173
c [sweep-6-1] 5824207 steps 763 queries 2738.27 avg class size
c [sweep-6-1] 11208 decisions 748 SAT calls 22.33 avg env size
c [sweep-6-1] 12297 variables remain 23% (40350 retained 77%)
c [decomp-33] removed 47 variables
c [sweep-6-1] removed 47 vars (0 failed, 38 eqs, 21 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 47 vars in TOTAL (1 rounds, 762 queries)
c [sort-queue-10] sorted 23139 enqueued variables after 187223 conflicts
c [score-dist-10] active 29461 (56%), one 0 (0%), zero 23139 (44%)
c [score-dist-10] max exp 519, different 16 (3%)
c [score-dist-10] median active exp 518, avg 517.3
c [simplification-10] removed 669 variables 1.3% (52600 remain 12%)
c [simplification-10] removed 9940 irredundant clauses 2.5% (385280 remain 30%)
c [simplification-10] maximum reduction of 3% = max (1%, 3%)
c [simplification-10] geometric conflict interval increment 14999 = 59998 / 4
c [simplification-10] new conflict interval 74997
c [simplification-10] penalized conflict interval 74997 = 1 * 74997
c [simplification-10] hard conflict limit 299718 (soft 262220 + delta 37498)
c [simplification-10] new conflict limit 262220 (hard 299718)
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  125.4   52599   385279    194843   71109  25263  7178    9   209   66   4%   -172  101    9    8  111%
c i  128.7   52595   385275    210332   83279  25551  7213    8   216   67   4%   -187   82    9    8  103%
c i  130.3   52593   385274    216512   88084  25760  7233    9   163   68   5%   -301   25    8    8   97%
c i  130.3   52579   385274    216896   88407  25767  7234    9   154   68   6%   -323   15    8    8   93%
c i  130.4   52566   385274    217010   88498  25773  7236    9   151   68   6%   -329   13   10    8  116%
c i  131.5   52550   385273    220921   91310  25872  7255    9   207   68   4%   -313   67   10    8  115%
c i  131.9   52537   385272    222160   92313  25918  7268    9   190   68   5%   -331   49   10    8  119%
c i  132.8   52535   385270    228501   97247  26180  7285    7    93   68   8%   -241  -49    7    8   81%
c i  135.0   52529   385266    240502  106977  26454  7324    8   262   68   3%   -113  116   10    8  116%
c -  135.2   52524   385266    240675   72940  26462  7326    8   259   63   3%   -140  113   10    8  120%
c i  137.7   52523   385264    247303   78142  26700  7356    9   193   66   5%   -173   40   10    8  116%
c i  138.0   52502   385264    249220   79606  26785  7364    8   138   66   6%   -227  -15    6    8   75%
c i  141.3   52499   385264    257232   85803  27073  7390    9   177   67   5%   -124   23   10    9  115%
c i  142.7   52494   385263    261804   89543  27218  7403    9   134   67   7%   -164  -21    7    9   80%
c i  142.7   52493   385263    261806   89543  27218  7404    9   134   67   7%   -164  -21    7    9   80%
c i  143.8   52492   385263    263546   91008  27264  7408   10   159   67   6%   -192    5   11    9  128%
c i  143.8   52491   385263    263548   91008  27265  7408   10   159   67   6%   -192    5   11    9  127%
c i  146.6   52487   385263    271977   97745  27524  7449    9   129   68   7%    -81  -23   11    9  132%
c i  147.1   52480   385263    273389   98921  27566  7455    9   118   68   8%   -155  -34   10    9  116%
c i  147.1   52478   385263    273390   98921  27566  7455    9   118   68   8%   -155  -34   10    9  115%
c 
c [simplification-11] limit 262240 conflicts (hard 299718) hit after 285660 conflicts
c [quatres-7] found 56322 quaternary clauses 23% in total
c [quatres-7-1] removed 68 duplicate quaternary clauses
c [quatres-7-1] added 9 double-self-subsuming ternary resolvents
c [quatres-7-2] added 310 single-self-subsuming ternary resolvents
c [quatres-7-2] added 717 quaternary resolvents
c [ternres-7] limit 26978912 with penalty 0 = 0 + 0
c [ternres-7] 2662 schedulable variables 5%
c [ternres-7] 9721 ternary resolvents (1162 bin, 8559 trn)
c [ternres-7] 28 variables remain 0% (52449 retained 100%)
c [gauss-4] limit 1348945 penalty 2 = 2 + 0
c [gauss-4] extracted 10901 xors of average arity 3.0
c [gauss-4] connected 32510 occurrences of 6738 variables (average 4.8)
c [gauss-4] limit 1348945 penalty 2 = 2 + 0
c [decomp-34] removed 385 variables
c [gauss-4] exported 0 unary, 1 binary and 1 ternary equations
c [simpleprobe-5] 19739 schedulable variables 38%
c [simpleprobe-5] limit 107915650 penalty 0 = 0 + 0
c [decomp-36] removed 112 variables
c [simpleprobe-5] 492 variables remain 1% (51488 retained 99%)
c [simpleprobe-5] removed 112 variables, found 1830 hbrs, 2 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 953 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 51980 variables 100%
c [block-4] limit of 67447281 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 14145 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 50292 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2697891260 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2646 variables 5% in round 1 in 294634696 steps
c [elim-8-1] backward subsumption/strengthening limit 294634600
c [elim-8-1-1] backward checking 8221 touched variables 16%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 23 and strengthened 950 clauses in 52081868 steps
c [elim-8-1] rescheduled 1257 variables 2% by backward subsumption
c [elim-8-2] eliminated 148 variables 0% in round 2 in 51627082 steps
c [elim-8-2] backward subsumption/strengthening limit 51627000
c [elim-8-2-1] backward checking 686 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 94 clauses in 10142918 steps
c [elim-8-2] rescheduled 184 variables 0% by backward subsumption
c [elim-8-3] eliminated 3 variables 0% in round 3 in 39893471 steps
c [elim-8-3] backward subsumption/strengthening limit 39893400
c [elim-8-3-1] backward checking 36 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 1191236 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2797 = 6% variables out of 50292 scheduled
c [bca-7] limit of 10000000 steps and 711897 added (scaled 2)
c [bca-7] 66909 out of 94992 literals actually usable 70%
c [bca-7] added 270 blocked clauses in 292894 steps
c [sweep-7] limit 8093673 penalty 0 = 0 + 0
c [sweep-7-1] 4808 pos 44.1% + 6101 neg 55.9% = 10909 sched 23.0% ret 36586
c [sweep-7-1] 8097028 steps 1568 queries 1691.83 avg class size
c [sweep-7-1] 25288 decisions 1566 SAT calls 22.63 avg env size
c [sweep-7-1] 7067 variables remain 15% (40427 retained 85%)
c [decomp-37] removed 36 variables
c [sweep-7-1] removed 36 vars (0 failed, 17 eqs, 16 impls)
c [sweep-7] 36 < 1/1000 * 47495 = 47 considered unsuccessful
c [sweep-7] removed 36 vars in TOTAL (1 rounds, 1567 queries)
c [sort-queue-11] sorted 20418 enqueued variables after 285660 conflicts
c [score-dist-11] active 27041 (57%), one 0 (0%), zero 20418 (43%)
c [score-dist-11] max exp 520, different 17 (3%)
c [score-dist-11] median active exp 519, avg 517.7
c [simplification-11] removed 5018 variables 9.6% (47459 remain 11%)
c [simplification-11] removed 29824 irredundant clauses 7.7% (355439 remain 28%)
c [simplification-11] maximum reduction of 10% = max (10%, 8%)
c [simplification-11] large reduction 10% >= 5% limit
c [simplification-11] next conflict interval 2856 = min (285660/100, 74997)
c [simplification-11] penalized conflict interval 2856 = 1 * 2856
c [simplification-11] hard conflict limit 298516 (soft 288516 + delta 10000)
c [simplification-11] new conflict limit 288516 (hard 298516)
c 
c [simplification-12] limit 288516 conflicts (hard 298516) hit after 288702 conflicts
c [quatres-8] found 48624 quaternary clauses 22% in total
c [quatres-8-1] removed 32 duplicate quaternary clauses
c [quatres-8-1] added 10 double-self-subsuming ternary resolvents
c [quatres-8-2] added 697 single-self-subsuming ternary resolvents
c [quatres-8-2] added 907 quaternary resolvents
c [ternres-8] limit 27082982 with penalty 0 = 0 + 0
c [ternres-8] 24 schedulable variables 0%
c [ternres-8] 10141 ternary resolvents (796 bin, 9345 trn)
c [ternres-8] 3 variables remain 0% (47456 retained 100%)
c [decomp-38] removed 68 variables
c [treelook-5] limit 2708298 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 15991 literals 17%
c [treelook-5] scheduling used 952431 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2708298 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2708650 steps
c [treelook-5] 15285 literals remain 16%
c [treelook-5] 3237 variables remain to probed next time 7%
c [decomp-39] removed 18 variables
c [treelook-5] removed 40 variables, found 1115 hbrs
c [unhide-10] limit 2708298 with penalty 1 = 1 + 0
c [unhide-10-10] 0 units, 0 failed, 5911 tauts, 0 hbrs, 43469 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 406 transitive binary clauses
c [bca-8] limit of 10000000 steps and 711076 added (scaled 2)
c [bca-8] 66561 out of 94704 literals actually usable 70%
c [bca-8] added 11 blocked clauses in 292443 steps
c [sort-queue-12] sorted 20391 enqueued variables after 288702 conflicts
c [score-dist-12] active 26960 (57%), one 0 (0%), zero 20391 (43%)
c [score-dist-12] max exp 520, different 17 (3%)
c [score-dist-12] median active exp 519, avg 517.7
c [simplification-12] removed 108 variables 0.2% (47351 remain 11%)
c [simplification-12] removed 364 irredundant clauses 0.1% (355075 remain 27%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 74997
c [simplification-12] new conflict interval 149994
c [simplification-12] penalized conflict interval 149994 = 1 * 149994
c [simplification-12] hard conflict limit 513693 (soft 438696 + delta 74997)
c [simplification-12] new conflict limit 438696 (hard 513693)
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  168.9   47350   355075    303032  101645  30686  6614   10   171   69   6%    238   31   12    9  137%
c -  172.0   47347   355075    312353   72601  30953  6640    9   105   63   9%    -65  -36    9    9  106%
c i  173.4   47346   355075    317697   77013  31067  6649    9   143   65   7%     20    3   10    9  117%
c -  190.5   47346   355075    372133   85499  32406  6724   10   151   63   7%    485   -2   10    9  104%
c 
c [simplification-13] limit of 588 binary hit after 594 binaries
c [quatres-9] found 51531 quaternary clauses 21% in total
c [quatres-9-1] removed 153 duplicate quaternary clauses
c [quatres-9-1] added 16 double-self-subsuming ternary resolvents
c [quatres-9-2] added 373 single-self-subsuming ternary resolvents
c [quatres-9-2] added 352 quaternary resolvents
c [ternres-9] limit 35529200 with penalty 0 = 0 + 0
c [ternres-9] 2 schedulable variables 0%
c [ternres-9] 4875 ternary resolvents (306 bin, 4569 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 3552920 penalty 1 = 1 + 0
c [gauss-5] extracted 24324 xors of average arity 3.0
c [gauss-5] connected 72876 occurrences of 7316 variables (average 10.0)
c [gauss-5] limit 3552920 penalty 1 = 1 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-40] removed 91 variables
c [basicprobe-5] limit 177646000 penalty 0 = 0 + 0
c [basicprobe-5-0] 25147 sched 53%, 70 failed, 0 lifted, 1978 hbrs
c [decomp-41] removed 144 variables
c [basicprobe-5-1] 25039 sched 53%, 6 failed, 0 lifted, 165 hbrs
c [decomp-42] removed 23 variables
c [basicprobe-5-2] 25032 sched 53%, 0 failed, 0 lifted, 25 hbrs
c [decomp-43] removed 1 variables
c [basicprobe-5-3] 25027 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-4] 25027 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-4] fully completed probing
c [basicprobe-5-4] 76 units = 76 failed (100%) + 0 lifted (0%)
c [basicprobe-5-4] removed 168 variables, found 2169 hbrs
c [bate-3] eliminated 352 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 592 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 47087 variables 100%
c [block-5] limit of 177646000 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 8497 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 46018 variables 100%
c [elim-9] limit of 355292000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 718 variables 2% in round 1 in 315884872 steps
c [elim-9-1] backward subsumption/strengthening limit 39407128
c [elim-9-1-1] backward checking 3988 touched variables 9%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 45 and strengthened 18 clauses in 14460943 steps
c [elim-9-1] rescheduled 119 variables 0% by backward subsumption
c [elim-9] incomplete 1 not tried 0% in round 2
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 735 = 2% variables out of 46018 scheduled
c [bca-9] limit of 10000000 steps and 682985 added (scaled 2)
c [bca-9] 63776 out of 90568 literals actually usable 70%
c [bca-9] added 124 blocked clauses in 280339 steps
c [sweep-8] limit 5329380 penalty 1 = 1 + 0
c [sweep-8-1] 3279 pos 48.4% + 3502 neg 51.6% = 6781 sched 15.0% ret 38502
c [sweep-8-1] 5332206 steps 1291 queries 1393.72 avg class size
c [sweep-8-1] 17780 decisions 1290 SAT calls 19.19 avg env size
c [sweep-8-1] 4340 variables remain 10% (40942 retained 90%)
c [decomp-45] removed 22 variables
c [sweep-8-1] removed 22 vars (0 failed, 11 eqs, 11 impls)
c [sweep-8] 22 < 1/1000 * 45283 = 45 considered unsuccessful
c [sweep-8] removed 22 vars in TOTAL (1 rounds, 1290 queries)
c [sort-queue-13] sorted 19442 enqueued variables after 381179 conflicts
c [score-dist-13] active 25819 (57%), one 0 (0%), zero 19442 (43%)
c [score-dist-13] max exp 520, different 17 (3%)
c [score-dist-13] median active exp 520, avg 518.1
c [simplification-13] removed 2085 variables 4.4% (45261 remain 10%)
c [simplification-13] removed 14113 irredundant clauses 4.0% (340962 remain 26%)
c [simplification-13] maximum reduction of 4% = max (4%, 4%)
c [simplification-13] forced so keeping old conflict interval 149994
c [simplification-13] conflict limit remains at 438696 (hard 513693)
c [simplification-13] 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 -  214.9   45261   340962    430575   89794  31922  6518   10   144   62   7%    803  -11    8   10   89%
c 
c [simplification-14] limit 438696 conflicts (hard 513693) hit after 438696 conflicts
c [quatres-10] found 50059 quaternary clauses 21% in total
c [quatres-10-1] removed 19 duplicate quaternary clauses
c [quatres-10-1] added 9 double-self-subsuming ternary resolvents
c [quatres-10-2] added 160 single-self-subsuming ternary resolvents
c [quatres-10-2] added 781 quaternary resolvents
c [ternres-10] limit 39490510 with penalty 0 = 0 + 0
c [ternres-10] all 45261 free variables schedulable
c [ternres-10] 5988 ternary resolvents (654 bin, 5334 trn)
c [ternres-10] 9 variables remain 0% (45252 retained 100%)
c [decomp-46] removed 67 variables
c [simpleprobe-6] 327 schedulable variables 1%
c [simpleprobe-6] limit 157962043 penalty 0 = 0 + 0
c [decomp-47] removed 42 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 42 variables, found 2287 hbrs, 4 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 895 transitive binary clauses
c [transred-10] found 3 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 45149 variables 100%
c [block-6] limit of 394905109 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 1067 blocked clauses
c [block-6] 1067 < 1/100 * 340613 = 3406 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 246815692 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 70 (1%) of length 27
c [cce-4-1] eliminated 5 clauses out of 223 (2%) of length 24
c [cce-4-1] eliminated 2 clauses out of 180 (1%) of length 23
c [cce-4-1] eliminated 1 clauses out of 252 (0%) of length 22
c [cce-4-1] eliminated 4 clauses out of 252 (2%) of length 21
c [cce-4-1] eliminated 7 clauses out of 303 (2%) of length 20
c [cce-4-1] eliminated 18 clauses out of 397 (5%) of length 19
c [cce-4-1] eliminated 25 clauses out of 644 (4%) of length 18
c [cce-4-1] eliminated 19 clauses out of 482 (4%) of length 17
c [cce-4-1] eliminated 39 clauses out of 828 (5%) of length 16
c [cce-4-1] eliminated 30 clauses out of 728 (4%) of length 15
c [cce-4-1] eliminated 68 clauses out of 828 (8%) of length 14
c [cce-4-1] eliminated 184 clauses out of 1263 (15%) of length 13
c [cce-4-1] eliminated 273 clauses out of 2039 (13%) of length 12
c [cce-4-1] eliminated 434 clauses out of 2917 (15%) of length 11
c [cce-4-1] eliminated 663 clauses out of 4178 (16%) of length 10
c [cce-4-1] eliminated 941 clauses out of 6342 (15%) of length 9
c [cce-4-1] eliminated 1704 clauses out of 11431 (15%) of length 8
c [cce-4-1] eliminated 2612 clauses out of 23247 (11%) of length 7
c [cce-4-1] eliminated 2426 clauses out of 51724 (5%) of length 6
c [cce-4-1] eliminated 1391 clauses out of 27973 (5%) of length 5
c [cce-4-1] eliminated 449 clauses out of 30454 (1%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 11296 large clauses in 246815882 steps
c [cce-4-1] allowing another 123407941 steps for small clauses
c [cce-4-1] scheduling 99059 clauses = 42367 binary + 56692 ternary
c [cce-4-1] tried to eliminate 99059 small clauses 100%
c [cce-4-1] eliminated 445 binary clauses 1%
c [cce-4-1] eliminated 1235 ternary clauses 2%
c [cce-4-1] eliminated 1680 small clauses 2%
c [cce-4-1] eliminated 1680 small clauses in 217048153 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 12976 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 14883786 steps for small clauses
c [cce-4-2] scheduling 97381 clauses = 41922 binary + 55459 ternary
c [cce-4-2] tried to eliminate 19243 small clauses 20%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 12976 covered clauses in TOTAL during 2 rounds
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 45014 variables 100%
c [elim-10] limit of 789810219 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 3382 variables 8% in round 1 in 254307267 steps
c [elim-10-1] backward subsumption/strengthening limit 254307200
c [elim-10-1-1] backward checking 11932 touched variables 27%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 2 and strengthened 4 clauses in 12258113 steps
c [elim-10-1] rescheduled 24 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 15974816 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 3382 = 8% variables out of 45014 scheduled
c [bca-10] limit of 10000000 steps and 636563 added (scaled 2)
c [bca-10] 58710 out of 83266 literals actually usable 71%
c [bca-10] added 115 blocked clauses in 276064 steps
c [sort-queue-14] sorted 17581 enqueued variables after 438696 conflicts
c [score-dist-14] active 24051 (58%), one 0 (0%), zero 17581 (42%)
c [score-dist-14] max exp 520, different 17 (3%)
c [score-dist-14] median active exp 520, avg 518.2
c [simplification-14] removed 3629 variables 8.0% (41632 remain 10%)
c [simplification-14] removed 23177 irredundant clauses 6.8% (317785 remain 25%)
c [simplification-14] maximum reduction of 8% = max (8%, 7%)
c [simplification-14] large reduction 8% >= 5% limit
c [simplification-14] next conflict interval 4386 = min (438696/100, 149994)
c [simplification-14] penalized conflict interval 4386 = 1 * 4386
c [simplification-14] hard conflict limit 453082 (soft 443082 + delta 10000)
c [simplification-14] new conflict limit 443082 (hard 453082)
c 
c [simplification-15] limit 443082 conflicts (hard 453082) hit after 443082 conflicts
c [quatres-11] found 43250 quaternary clauses 19% in total
c [quatres-11-1] removed 11 duplicate quaternary clauses
c [quatres-11-1] added 4 double-self-subsuming ternary resolvents
c [quatres-11-2] added 143 single-self-subsuming ternary resolvents
c [quatres-11-2] added 323 quaternary resolvents
c [ternres-11] limit 39884057 with penalty 0 = 0 + 0
c [ternres-11] 9 schedulable variables 0%
c [ternres-11] 1022 ternary resolvents (65 bin, 957 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1246376 penalty 4 = 4 + 0
c [card-5] found 212 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1246376 for elimination
c [card-5] 212 out of 212 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-48] removed 4 variables
c [treelook-6] limit 3988405 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 13655 literals 16%
c [treelook-6] scheduling used 861616 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3988405 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 4033679 steps
c [treelook-6] 12851 literals remain 15%
c [treelook-6] 2631 variables remain to probed next time 6%
c [decomp-49] removed 1 variables
c [treelook-6] removed 15 variables, found 1325 hbrs
c [unhide-11] limit 1994202 with penalty 2 = 2 + 0
c [unhide-11-11] 0 units, 0 failed, 658 tauts, 0 hbrs, 24205 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 774 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 41613 variables 100%
c [elim-11] limit of 797681150 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 425 variables 1% in round 1 in 244258170 steps
c [elim-11-1] backward subsumption/strengthening limit 244258100
c [elim-11-1-1] backward checking 902 touched variables 2%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 5 clauses in 4572282 steps
c [elim-11-1] rescheduled 20 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 5599154 steps
c [elim-11-2] backward subsumption/strengthening limit 5599100
c [elim-11-2-1] backward checking 5 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 2 and strengthened 0 clauses in 214331 steps
c [elim-11-2] rescheduled 5 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 288359 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 426 = 1% variables out of 41613 scheduled
c [bca-11] limit of 10000000 steps and 632781 added (scaled 2)
c [bca-11] 57904 out of 82376 literals actually usable 70%
c [bca-11] added 46 blocked clauses in 276202 steps
c [sort-queue-15] sorted 17426 enqueued variables after 443082 conflicts
c [score-dist-15] active 23761 (58%), one 0 (0%), zero 17426 (42%)
c [score-dist-15] max exp 520, different 17 (3%)
c [score-dist-15] median active exp 520, avg 518.2
c [simplification-15] removed 445 variables 1.1% (41187 remain 9%)
c [simplification-15] removed 1920 irredundant clauses 0.6% (315865 remain 24%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 74997 = 149994 / 2
c [simplification-15] new conflict interval 224991
c [simplification-15] penalized conflict interval 224991 = 1 * 224991
c [simplification-15] hard conflict limit 780568 (soft 668073 + delta 112495)
c [simplification-15] new conflict limit 668073 (hard 780568)
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 -  247.3   41187   315865    484715   94569  34453  7732   10   156   62   6%    927   13    8   10   86%
c -  257.8   41187   315865    536170  104021  35114  7770    9   155   62   6%    980   10    8   10   78%
c -  270.1   41187   315865    587629  112243  35934  7821   10    68   63  14%   1004  -54   11   10  110%
c i  282.9   41186   315865    634082  152767  36571  7858   10    92   73  11%   1014   -6   12   10  117%
c -  284.9   41179   315865    640035  120096  36636  7861   10    66   63  16%  -3556  -29   10   10   97%
c i  294.2   41178   315865    671690  148490  36934  7887   10    37   93  26%  -1811  -45    7   10   69%
c -  298.9   41056   315865    691635  129182  37115  7905   10    43   86  23%  -1507  -33   11   10  118%
c i  302.8   41055   315865    703980  140264  37261  7929   10    38   91  26%  -1073  -33   11   10  116%
c i  303.2   41053   315865    705672  141793  37280  7937    9    35   91  26%  -1421  -34    7   10   69%
c i  308.3   41022   315865    722425  156738  37368  7955    9    16   94  55%   -966  -43    6    9   68%
c i  308.3   41019   315865    722515  156815  37372  7957    9    16   94  55%   -985  -44    6    9   61%
c i  308.4   41000   315865    722743  157003  37382  7961    8    16   94  53%  -1026  -43    5    9   52%
c i  308.4   40989   315865    722840  157055  37387  7965    8    15   94  54%  -1041  -44    5    9   53%
c i  308.4   40723   315865    722849  157057  37389  7968    8    15   94  54%  -1042  -44    5    9   52%
c i  308.4   40661   315865    722850  157057  37389  7968    8    15   94  54%  -1042  -44    5    9   51%
c i  308.4   40649   315865    722881  157077  37391  7968    8    15   94  54%  -1047  -44    5    9   49%
c i  308.4   40647   315865    722884  157073  37391  7970    8    15   94  54%  -1047  -44    5    9   49%
c i  308.4   40401   315865    722887  157073  37391  7971    8    15   94  54%  -1048  -44    5    9   48%
c i  308.4   40381   315865    722889  157073  37391  7971    8    15   94  54%  -1048  -44    5    9   48%
c 0  308.4   40304   315865    722889  157073  37391  7971    8    15   94  54%  -1048  -44    5    9   48%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 1295 basic ate = 256 trn 20% + 1039 lrg 80% in 3 updates
c bcas: 11 count, 1148 added (1294 skipped), 3132967 steps
c bkwd: tried 763854 clauses, 1524982 lits, 2.00 lits/clause
c bkwd: checked 152001215 occs, 198.99 occs/clause, 99.67 occs/lit
c bkwd: subsumed 0 binary, 52 ternary, 754 large
c bkwd: strengthened 3 binary, 21 ternary (100% self), 2902 large (0% self)
c blkd: 6 bces, 38545 removed, 16237791 resolutions, 43059001 steps
c blkd: 10728 blocking literals 1%, 4224 pure
c bump: 685420 bumped seen, 30461436 lits 44.4 on average
c card: 5 count, 0 units, 0 am1, 15353513 steps
c card: 1 rescheduled, 4 eliminated, 211 resolved, 4419 subsumed
c card: 552 at-most-one constraints found, average size 3.14
c card: 552 at-most-one constraints used 100%, average size 3.14
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, 14511 eliminated, 14228 ate 98%, 283 abce 2%
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: 4305712 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 99 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 49 decompositions, 2797 equivalent 1%
c deco: 5 decision-only clauses 0%, 42% reduction
c decs: 10014479 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 11 elims, 381941 eliminated 88%, 369 pure 0%
c elms: 19 rounds, 1.7 rounds/bve
c elms: 356447 small 93%, 20901 large 5%
c elms: 494388 tried small, 356447 succeeded 72%, 137941 failed 28%
c elms: 13370 subsumed, 11100 strengthened, 1379 blocked
c elms: 15187483 copies, 27125389 resolutions, 9950348 ipos
c elms: 14774724 subchks, 12936123 strchks
c gaus: 5 extractions, 76348 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 2 binary and 1 ternary equations
c gaus: 0 gc, 19810784 steps, 9905392 extr 50%, 9997256 elim 50%
c glue: 9.4 orig avg, 9.4 real avg, 2.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 29718 = 5538 simple 19% + 22312 trn 75% + 1868 lrg 6%, 2194 sub 7%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 685420 clauses, 21.8 length
c lrnd: 14919101 lits = 20119966 orig - 5200865 removed 26%
c lrnd: 223659 uips 33%, 274242 flips 40%
c mins: 658485 mins 96%, 466 bin 0%, 26464 size 4%
c mins: 20608978 poisoned searches, 3090652 hits, 15% hit rate
c mins: 36784761 used twice searches, 3041543 hits, 8% hit rate
c move: moved 25365, 5644 bin 22%, 19721 trn 78%
c otfs: 39223 driving 50%, 38801 restarting 50%
c otfs: str 78024, 77748 red 100%, 276 irr 0%
c otfs: str 78024, 0 bin 0%, 615 trn 1%, 77409 lrg 99%
c otfs: sub 1512, 1486 red 98%, 26 irr 2%
c otfs: sub 1512, 0 bin 0%, 142 trn 9%, 1370 lrg 91%
c phas: 6 computed, 189823 set, 59987 pos (32%), 129836 neg (68%)
c prbs: 5 basic, 778148 probed, 724 failed, 173 lifted
c prbs: 6 simple, 712624 probed, 16 failed, 332 eqs
c prbs: 6 treelook, 1793 probed, 46 failed, 0 lifted
c prom: 105033 locked 17% out of 614888 tried
c prps: 466309764 props, 46 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 11 count, 15974 quat, 2372 self1, 74 self2, 529 dup
c queu: 15 sorted, 10014479 next (75334 steps 0.01)
c queu: 31536632 enq (866201437 steps 27.47), 30461436 deq 97%
c redc: 22115 clauses 8%, 261331 tried 36%, 14 sat 0%
c redc: 28768 lits 1%, 2455439 tried 12%, 15 sat 0%
c redc: 588 times jump level reduced, 8.7 levels on average
c reds: 11 count, 65717.2 conflicts per reduce
c reds: 0 memlim 0%, 11 arith 100%
c reds: 302522 collected 74%, 107134 retired 26%
c rmbd: 1563 removed, 835 red 53%
c rsts: 20767 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: 15 count, 14 confs 93%, 0 vars 0%
c simp: 0 its 0%, 1 bin 7%, 0 trns 0%
c subl: 685420 count (325338 tried 0.5), 62705 sub out of 677487 (9.3%)
c swps: 8 count, 8 rounds, 7667 queries (958.4/round)
c swps: 7605 sat calls, 113 unsat (0.2% success rate)
c swps: 127052 decisions 16.7, 1754 conflicts 0.2
c swps; 2075.5 avg class size, 24.5 avg environment size
c swps: 0 failed, 120 impls, 175 equivs
c swp0: 2554 type 0 queries, 195 unsat (7.6%), 2521 sat (98.7%)
c swp1: 5113 type 1 queries, 1376 unsat (26.9%), 4971 sat (97.2%)
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: 21400147 calls to obtain time
c tops: 8559 fixed 2%, 59 its, 12252.36 confs/it
c trds: 11 transitive reductions, 5163 removed, 20 failed
c trds: 1107477 nodes, 583618 edges, 9540230 steps
c trim: 825776 words, 3.2 MB
c trnr: 11 count, 3436 bin, 56268 trn, 218653158 steps
c unhd: 11 count, 11 rounds, 40801024 steps
c unhd: 1925 non-trivial sccs of average size 2.5
c unhd: 20 units, 20 bin, 0 trn, 0 lrg
c unhd: 180 failed, 175 stamp, 0 lits, 2 bin, 3 trn, 0 lrg
c unhd: 14024 tauts, 197 bin 1%, 8702 trn 62%, 3109 lrg 22%
c unhd: 14024 tauts, 2016 stamp 14%, 11533 red 82%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 126716 str, 20 bin 0%, 1605 trn 1%, 125091 lrg 99%, 98012 red 77%
c vars: 40304 remaining 9% and 393297 removed 91% out of 433601
c vars: 8559 fixed 2%, 381941 eliminated 88%, 2797 equivalent 1%
c vsts: 6293514684 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 13.5 search visits per propagation, 8524.1 per conflict
c wchs: 1129408090 pushed, 48548785 enlarged, 163 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         693461        302522        107134      31357611       3388019        315006
c 
c  0 0        175988  25      6085   2         0   0  23846363  76<  1875925  55    157472  50     3.7
c  1 5         64600   9     30887  10     12480  12   2750379   9    386086  11<    40774  13<    0.6
c  2 6        155518  22<    90577  30     27537  26   2978398   9    589358  17     59714  19     1.6
c  3 9        164590  24     97642  32<    31566  29<  1230756   4    366151  11     38466  12     2.4
c  4 14        86777  13     51914  17     20974  20    428672   1    124614   4     13686   4     1.5
c  5 21        31304   5     18026   6      9027   8     93728   0     34123   1      3605   1     0.8
c  6 30        10658   2      5586   2      3758   4     21905   0      9062   0       988   0     0.4
c  7 41         2808   0      1272   0      1210   1      5485   0      1952   0       219   0     0.2
c  8 54          827   0       391   0       375   0      1370   0       559   0        63   0     0.1
c  9 69          228   0        79   0       118   0       311   0       115   0        11   0     0.0
c 10 86          123   0        48   0        64   0       190   0        58   0         6   0     0.0
c 11 126          37   0        15   0        22   0        51   0        16   0         2   0     0.0
c 12 230           3   0         0   0         3   0         3   0         0   0         0   0     0.0
c 
c avg                  2.1           2.8           3.1           0.5           1.0           1.1
c std                  1.6           1.2           1.4           1.0           1.3           1.4
c 
c   40.562  13% elim
c   16.974   6% probe
c   14.729   5% bump
c    8.119   3% sweep
c    6.843   2% decide
c    6.126   2% cce
c    4.244   1% block
c    4.215   1% unhide
c    3.081   1% quatres
c    2.616   1% bca
c    2.585   1% gauss
c 
c    3.208 < 1% rest (below)
c 
c    2.023   1% ternres
c    0.780   0% transred
c    0.406   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    7.566   2% preprocessing     8%
c   91.237  30% inprocessing     92%
c ==================================
c   98.803  32% simplifying
c  209.633  68% search
c ==================================
c  308.443 100% all
c 
c        722889 conflicts,        2343.7 confs/sec
c          6422 ternaries,         112.6 confs/ternary
c           853 binaries,          847.5 confs/binary
c            59 iterations,      12252.4 confs/iteration
c 
c            11 reductions,          0.0 redus/sec,  65717.2 confs/reduction
c         20767 restarts,           67.3 rests/sec,     34.8 confs/restart
c      10014479 decisions,       32467.8 decis/sec,     13.9 decis/conflict
c     466309764 propagations,  1511816.5 props/sec,     46.6 props/decision
c 
c 308.4 seconds, 119.1 MB
c launch: done
