c launch: /data/cnf/sc2014/app/atco_enc1_opt2_10_15.cnf.bz2
c host: atom16
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/atco_enc1_opt2_10_15.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt2_10_15.cnf.bz2
c no embedded options
c found 'p cnf 9590 150623' header
c read 9590 variables, 150623 clauses, 630722 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=2
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 9188 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] VMTF (--score=2)
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    9188   141098         0       0      0     0    0     0    7   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 1807 at-most-one constraints of average size 3.1
c [card-1] found 70 at-most-two constraints of average size 4.9
c [card-1] using previous limit 2000000 for elimination
c [card-1] 1877 out of 1877 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1190 variables
c [simpleprobe-1] all 8400 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 325 variables
c [simpleprobe-1] 4965 variables remain 61% (3110 retained 39%)
c [simpleprobe-1] removed 325 variables, found 2609 hbrs, 21 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 0 failed, 1070 tauts, 0 hbrs, 11 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 8074 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 2215 variables 27% in round 1 in 7790487 steps
c [elim-1-1] backward subsumption/strengthening limit 7790400
c [elim-1-1-1] backward checking 5596 touched variables 69%
c [elim-1-1-1] incomplete backward checking 2748 remain 49%
c [elim-1-1] subsumed 162 and strengthened 191 clauses in 7790453 steps
c [elim-1-1] rescheduled 189 variables 2% by backward subsumption
c [elim-1-2] eliminated 1 variables 0% in round 2 in 42744 steps
c [elim-1-2] backward subsumption/strengthening limit 42700
c [elim-1-2-1] backward checking 2754 touched variables 34%
c [elim-1-2-1] incomplete backward checking 2751 remain 100%
c [elim-1-2] subsumed 0 and strengthened 1 clauses in 43395 steps
c [elim-1-2] rescheduled 4 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 349 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2216 = 27% variables out of 8074 scheduled
c [phase-count-1] 122219 negative 92.5% of 132127 except 9908 7.5%
c [phase-count-1] 124268 positive 94.1% of 132127 except 7859 5.9%
c [phase-1] phase bias: 3329 positive 57%, 2529 negative 43%
c [sort-queue-1] sorted 5858 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5858 (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 3163 variables 35.1% (5858 remain 64%)
c [simplification-1] removed 8971 irredundant clauses 6.4% (132127 remain 94%)
c [simplification-1] maximum reduction of 35% = max (35%, 6%)
c [simplification-1] large reduction 35% >= 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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 9 variables
c [simpleprobe-2] 3832 schedulable variables 66%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 3888 variables remain 66% (1961 retained 34%)
c [simpleprobe-2] removed 0 variables, found 158 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 10271 literals 88%
c [treelook-1] scheduling used 300068 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 301058 steps
c [treelook-1] 10208 literals remain 87%
c [treelook-1] 5722 variables remain to probed next time 98%
c [decomp-5] removed 2 variables
c [treelook-1] removed 4 variables, found 199 hbrs
c [basicprobe-1] limit 1056840 based on 132105 irredundant clauses
c [basicprobe-1-0] 424 probes remain 7% after last round
c [basicprobe-1-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 12 variables, found 1984 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 1 failed, 996 tauts, 0 hbrs, 429 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 5832 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 1205 blocked clauses
c [block-1] 1205 < 1/100 * 132059 = 1320 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 7 clauses out of 7 (100%) of length 22
c [cce-1-1] eliminated 21 clauses out of 21 (100%) of length 21
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 20
c [cce-1-1] eliminated 320 clauses out of 514 (62%) of length 13
c [cce-1-1] eliminated 123 clauses out of 871 (14%) of length 12
c [cce-1-1] eliminated 97 clauses out of 181 (54%) of length 11
c [cce-1-1] eliminated 11 clauses out of 239 (5%) of length 10
c [cce-1-1] eliminated 46 clauses out of 1098 (4%) of length 9
c [cce-1-1] eliminated 38 clauses out of 3036 (1%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 666 large clauses in 30000078 steps
c [cce-1-1] allowing another 15000039 steps for small clauses
c [cce-1-1] scheduling 13913 clauses = 12164 binary + 1749 ternary
c [cce-1-1] tried to eliminate 3864 small clauses 28%
c [cce-1-1] eliminated 425 binary clauses 3%
c [cce-1-1] eliminated 18 ternary clauses 1%
c [cce-1-1] eliminated 443 small clauses 3%
c [cce-1-1] eliminated 443 small clauses in 30000150 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1109 covered clauses in round 1
c [cce-1] eliminated 1109 covered clauses in TOTAL during 1 rounds
c [cce-1] 1109 < 1/100 * 130849 = 1308 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5832 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 36 variables 1% in round 1 in 15495164 steps
c [elim-2-1] backward subsumption/strengthening limit 4504836
c [elim-2-1-1] backward checking 780 touched variables 13%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 164 and strengthened 76 clauses in 3165782 steps
c [elim-2-1] rescheduled 93 variables 2% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 583037 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 36 = 1% variables out of 5832 scheduled
c [elim-2] 36 < 1/100 * 5832 = 58 considered unsuccessful
c [bca-1] limit of 10000000 steps and 259094 added (scaled 2)
c [bca-1] 10705 out of 11594 literals actually usable 92%
c [bca-1] added 51 blocked clauses in 27870 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2147 pos 37.0% + 3649 neg 63.0% = 5796 sched 100.0% ret 0
c [sweep-1-1] 1002269 steps 129 queries 455.19 avg class size
c [sweep-1-1] 2474 decisions 105 SAT calls 53.20 avg env size
c [sweep-1-1] 4644 variables remain 80% (1150 retained 20%)
c [decomp-6] removed 284 variables
c [sweep-1-1] removed 284 vars (0 failed, 25 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 284 vars in TOTAL (1 rounds, 128 queries)
c [phase-count-2] 116767 negative 90.6% of 128931 except 12164 9.4%
c [phase-count-2] 120390 positive 93.4% of 128931 except 8541 6.6%
c [phase-2] phase bias: 16 positive 50%, 16 negative 50%
c [sort-queue-2] sorted 5512 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 1098 (20%), zero 4414 (80%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 346 variables 5.9% (5512 remain 60%)
c [simplification-2] removed 3196 irredundant clauses 2.4% (128931 remain 91%)
c [simplification-2] maximum reduction of 6% = max (6%, 2%)
c [simplification-2] large reduction 6% >= 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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [quatres-1] found 25589 quaternary clauses 30% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 3 single-self-subsuming ternary resolvents
c [quatres-1-2] added 7 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 5512 free variables schedulable
c [ternres-1] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 868 at-most-one constraints of average size 3.1
c [card-2] found 83 at-most-two constraints of average size 4.7
c [card-2] using previous limit 1000000 for elimination
c [card-2] 951 out of 951 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 414 xors of average arity 2.9
c [gauss-1] connected 1221 occurrences of 581 variables (average 2.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 7 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 10118 literals 92%
c [treelook-2] scheduling used 300197 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 303706 steps
c [treelook-2] 10080 literals remain 92%
c [treelook-2] 5361 variables remain to probed next time 97%
c [decomp-8] removed 5 variables
c [treelook-2] removed 5 variables, found 85 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 598 tauts, 0 hbrs, 677 literals
c [transred-1] limit 128269 based on 128269 irredundant clauses
c [transred-1] removed 342 transitive binary clauses
c [bca-2] limit of 10000000 steps and 256901 added (scaled 2)
c [bca-2] 9839 out of 11002 literals actually usable 89%
c [bca-2] added 4 blocked clauses in 27828 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2073 pos 47.0% + 2340 neg 53.0% = 4413 sched 80.2% ret 1087
c [sweep-2-1] 1073355 steps 95 queries 402.88 avg class size
c [sweep-2-1] 2434 decisions 88 SAT calls 57.45 avg env size
c [sweep-2-1] 3691 variables remain 67% (1809 retained 33%)
c [decomp-9] removed 30 variables
c [sweep-2-1] removed 30 vars (0 failed, 7 eqs, 4 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 30 vars in TOTAL (1 rounds, 94 queries)
c [phase-count-3] 116012 negative 90.5% of 128166 except 12154 9.5%
c [phase-count-3] 119618 positive 93.3% of 128166 except 8548 6.7%
c [phase-3] phase bias: 9 positive 82%, 2 negative 18%
c [sort-queue-3] sorted 5470 enqueued variables after 3001 conflicts
c [score-dist-3] active 0 (0%), one 1449 (26%), zero 4021 (74%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 42 variables 0.8% (5470 remain 60%)
c [simplification-3] removed 765 irredundant clauses 0.6% (128166 remain 91%)
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 23001 (soft 13001 + delta 10000)
c [simplification-3] new conflict limit 13001 (hard 23001)
c 
c [simplification-4] limit 13001 conflicts (hard 23001) hit after 13001 conflicts
c [quatres-2] found 25786 quaternary clauses 30% in total
c [quatres-2-2] added 3 single-self-subsuming ternary resolvents
c [quatres-2-2] added 20 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5470 free variables schedulable
c [ternres-2] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-2] 195 variables remain 4% (5275 retained 96%)
c [decomp-10] removed 10 variables
c [basicprobe-2] limit 2585407 penalty 0 = 0 + 0
c [basicprobe-2-0] 377 sched 7%, 6 failed, 0 lifted, 1118 hbrs
c [decomp-11] removed 74 variables
c [basicprobe-2-1] 1103 sched 21%, 6 failed, 0 lifted, 399 hbrs
c [decomp-12] removed 11 variables
c [basicprobe-2-2] 692 probes remain 13% after last round
c [basicprobe-2-2] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 85 variables, found 1560 hbrs
c [bate-1] eliminated 235 asymmetric tautologies during probing
c [transred-2] limit 517081 with penalty 0 = 0 + 0
c [transred-2] removed 837 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5375 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 26 blocked clauses
c [block-2] 26 < 1/100 * 127467 = 1274 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 22
c [cce-2-1] eliminated 3 clauses out of 249 (1%) of length 13
c [cce-2-1] eliminated 9 clauses out of 699 (1%) of length 12
c [cce-2-1] eliminated 9 clauses out of 99 (9%) of length 11
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 25 large clauses in 15000334 steps
c [cce-2-1] allowing another 7500167 steps for small clauses
c [cce-2-1] scheduling 40921 clauses = 10626 binary + 30295 ternary
c [cce-2-1] tried to eliminate 1959 small clauses 5%
c [cce-2-1] eliminated 17 binary clauses 0%
c [cce-2-1] eliminated 80 ternary clauses 0%
c [cce-2-1] eliminated 97 small clauses 0%
c [cce-2-1] eliminated 97 small clauses in 15000115 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 122 covered clauses in round 1
c [cce-2] eliminated 122 covered clauses in TOTAL during 1 rounds
c [cce-2] 122 < 1/100 * 127441 = 1274 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5375 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 799 not tried 15% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 31 = 1% variables out of 5375 scheduled
c [elim-3] 31 < 1/100 * 5375 = 53 considered unsuccessful
c [bca-3] limit of 10000000 steps and 254831 added (scaled 2)
c [bca-3] 9220 out of 10690 literals actually usable 86%
c [bca-3] added 25 blocked clauses in 36317 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1762 pos 48.8% + 1848 neg 51.2% = 3610 sched 67.6% ret 1734
c [sweep-3-1] 1006865 steps 48 queries 538.67 avg class size
c [sweep-3-1] 1585 decisions 47 SAT calls 58.21 avg env size
c [sweep-3-1] 3417 variables remain 64% (1927 retained 36%)
c [decomp-13] removed 10 variables
c [sweep-3-1] removed 10 vars (0 failed, 2 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 10 vars in TOTAL (1 rounds, 47 queries)
c [phase-count-4] 114682 negative 90.2% of 127148 except 12466 9.8%
c [phase-count-4] 118320 positive 93.1% of 127148 except 8828 6.9%
c [phase-4] phase bias: 4 positive 44%, 5 negative 56%
c [sort-queue-4] sorted 5334 enqueued variables after 13001 conflicts
c [score-dist-4] active 0 (0%), one 1651 (31%), zero 3683 (69%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 136 variables 2.5% (5334 remain 58%)
c [simplification-4] removed 1018 irredundant clauses 0.8% (127148 remain 90%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 16666
c [simplification-4] penalized conflict interval 16666 = 1 * 16666
c [simplification-4] hard conflict limit 39667 (soft 29667 + delta 10000)
c [simplification-4] new conflict limit 29667 (hard 39667)
c 
c [simplification-5] limit 29667 conflicts (hard 39667) hit after 29667 conflicts
c [quatres-3] found 26037 quaternary clauses 30% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 10 single-self-subsuming ternary resolvents
c [quatres-3-2] added 31 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 190 schedulable variables 4%
c [ternres-3] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 221 xors of average arity 3.0
c [gauss-2] connected 656 occurrences of 378 variables (average 1.7)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 5 variables
c [unhide-4] limit 151443 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 254 tauts, 0 hbrs, 11537 literals
c [transred-3] limit 1514439 with penalty 0 = 0 + 0
c [transred-3] removed 166 transitive binary clauses
c [bca-4] limit of 10000000 steps and 254698 added (scaled 2)
c [bca-4] 8878 out of 10660 literals actually usable 83%
c [bca-4] added 0 blocked clauses in 50925 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1761 pos 51.7% + 1646 neg 48.3% = 3407 sched 63.9% ret 1922
c [sweep-4-1] 1001831 steps 50 queries 377.28 avg class size
c [sweep-4-1] 1397 decisions 50 SAT calls 66.72 avg env size
c [sweep-4-1] 3169 variables remain 59% (2160 retained 41%)
c [decomp-15] removed 10 variables
c [sweep-4-1] removed 10 vars (0 failed, 1 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 10 vars in TOTAL (1 rounds, 49 queries)
c [phase-count-5] 114615 negative 90.2% of 127076 except 12461 9.8%
c [phase-count-5] 118263 positive 93.1% of 127076 except 8813 6.9%
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-5] sorted 5319 enqueued variables after 29667 conflicts
c [score-dist-5] active 0 (0%), one 1907 (36%), zero 3412 (64%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 15 variables 0.3% (5319 remain 58%)
c [simplification-5] removed 72 irredundant clauses 0.1% (127076 remain 90%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 36666
c [simplification-5] penalized conflict interval 36666 = 1 * 36666
c [simplification-5] hard conflict limit 84666 (soft 66333 + delta 18333)
c [simplification-5] new conflict limit 66333 (hard 84666)
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.0    5318   127076     35585   34358   1277  2256   11    19   14  58%    420   12   11    4  257%
c -   14.2    5318   127076     58835   17899   1377  2271   11    19   19  59%    204    8   11    6  172%
c 
c [simplification-6] limit 66333 conflicts (hard 84666) hit after 66334 conflicts
c [quatres-4] found 26493 quaternary clauses 30% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 16 single-self-subsuming ternary resolvents
c [quatres-4-2] added 23 quaternary resolvents
c [ternres-4] limit 4678951 with penalty 0 = 0 + 0
c [ternres-4] all 5318 free variables schedulable
c [ternres-4] 80 ternary resolvents (0 bin, 80 trn)
c [ternres-4] 6 variables remain 0% (5312 retained 100%)
c [card-3] limit 584868 penalty 2 = 2 + 0
c [card-3] found 666 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 584868 for elimination
c [card-3] 666 out of 666 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-16] removed 2 variables
c [simpleprobe-3] 3556 schedulable variables 67%
c [simpleprobe-3] limit 9357903 penalty 1 = 1 + 0
c [decomp-17] removed 25 variables
c [simpleprobe-3] 3405 variables remain 64% (1887 retained 36%)
c [simpleprobe-3] removed 25 variables, found 805 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 564 transitive binary clauses
c [transred-4] found 2 units
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 14036850 penalty 0 = 0 + 0
c [sweep-5-1] 1664 pos 52.8% + 1485 neg 47.2% = 3149 sched 59.5% ret 2141
c [sweep-5-1] 10787882 steps 876 queries 31.08 avg class size
c [sweep-5-1] 20939 decisions 848 SAT calls 53.32 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-18] removed 58 variables
c [sweep-5-1] removed 58 vars (0 failed, 54 eqs, 14 impls)
c [sweep-5-2] 2908 pos 55.6% + 2324 neg 44.4% = 5232 sched 100.0% ret 0
c [sweep-5-2] 3361328 steps 24 queries 1218.67 avg class size
c [sweep-5-2] 1140 decisions 23 SAT calls 109.13 avg env size
c [sweep-5-2] 4925 variables remain 94% (307 retained 6%)
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 58 vars in TOTAL (2 rounds, 898 queries)
c [phase-count-6] 114245 negative 90.0% of 126876 except 12631 10.0%
c [phase-count-6] 117932 positive 93.0% of 126876 except 8944 7.0%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-6] sorted 5232 enqueued variables after 66334 conflicts
c [score-dist-6] active 0 (0%), one 2358 (45%), zero 2874 (55%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 86 variables 1.6% (5232 remain 57%)
c [simplification-6] removed 200 irredundant clauses 0.2% (126876 remain 90%)
c [simplification-6] maximum reduction of 2% = max (2%, 0%)
c [simplification-6] geometric conflict interval increment 12222 = 36666 / 3
c [simplification-6] new conflict interval 48888
c [simplification-6] penalized conflict interval 48888 = 1 * 48888
c [simplification-6] hard conflict limit 139666 (soft 115222 + delta 24444)
c [simplification-6] new conflict limit 115222 (hard 139666)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   18.8    5231   126876     80846   40710   1548  2784   11    19   14  60%    438    6   12    8  156%
c i   18.8    5230   126876     81073   40915   1551  2785   11    19   15  60%    300    5   11    8  141%
c -   23.7    5227   126876    101662   24880   1630  2797   11    19   19  61%     72    4   11    9  127%
c 
c [simplification-7] limit 115222 conflicts (hard 139666) hit after 116186 conflicts
c [quatres-5] found 26864 quaternary clauses 29% in total
c [quatres-5-2] added 15 single-self-subsuming ternary resolvents
c [quatres-5-2] added 35 quaternary resolvents
c [ternres-5] limit 8920527 with penalty 0 = 0 + 0
c [ternres-5] 6 schedulable variables 0%
c [ternres-5] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 6 variables
c [treelook-3] limit 892052 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 10338 literals 99%
c [treelook-3] scheduling used 403077 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 892052 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 893384 steps
c [treelook-3] 10229 literals remain 98%
c [treelook-3] 5079 variables remain to probed next time 97%
c [treelook-3] removed 3 variables, found 347 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 469 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5223 variables 100%
c [block-3] limit of 22301318 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 13 blocked clauses
c [block-3] 13 < 1/100 * 126441 = 1264 considered unsuccessful
c [cce-3] limit of 11150659 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 38 clauses out of 241 (16%) of length 13
c [cce-3-1] eliminated 46 clauses out of 682 (7%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 84 large clauses in 11150739 steps
c [cce-3-1] allowing another 5575369 steps for small clauses
c [cce-3-1] scheduling 13944 clauses = 10386 binary + 3558 ternary
c [cce-3-1] tried to eliminate 1147 small clauses 8%
c [cce-3-1] eliminated 81 binary clauses 1%
c [cce-3-1] eliminated 145 ternary clauses 4%
c [cce-3-1] eliminated 226 small clauses 2%
c [cce-3-1] eliminated 226 small clauses in 11151310 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 310 covered clauses in round 1
c [cce-3] eliminated 310 covered clauses in TOTAL during 1 rounds
c [cce-3] 310 < 1/100 * 126428 = 1264 considered unsuccessful
c [elim-4] 785 variables 15% will be scheduled this time
c [elim-4] scheduled 785 variables 15%
c [elim-4] boosting limit by 20
c [elim-4] limit of 892052725 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 112740536 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 785 scheduled
c [bca-5] limit of 10000000 steps and 250706 added (scaled 2)
c [bca-5] 8078 out of 10448 literals actually usable 77%
c [bca-5] added 12 blocked clauses in 57767 steps
c [sweep-6] limit 2676158 penalty 0 = 0 + 0
c [sweep-6-1] 2745 pos 55.8% + 2173 neg 44.2% = 4918 sched 94.2% ret 305
c [sweep-6-1] 2999413 steps 101 queries 399.04 avg class size
c [sweep-6-1] 2608 decisions 98 SAT calls 67.17 avg env size
c [sweep-6-1] 3927 variables remain 75% (1296 retained 25%)
c [decomp-22] removed 6 variables
c [sweep-6-1] removed 6 vars (0 failed, 8 eqs, 3 impls)
c [sweep-6] removed 6 vars in TOTAL (1 rounds, 100 queries)
c [phase-count-7] 112522 negative 90.0% of 125083 except 12561 10.0%
c [phase-count-7] 116245 positive 92.9% of 125083 except 8838 7.1%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 5217 enqueued variables after 116186 conflicts
c [score-dist-7] active 0 (0%), one 2497 (48%), zero 2720 (52%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 10 variables 0.2% (5217 remain 57%)
c [simplification-7] removed 1793 irredundant clauses 1.4% (125083 remain 89%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 24444 = 48888 / 2
c [simplification-7] new conflict interval 73332
c [simplification-7] penalized conflict interval 73332 = 1 * 73332
c [simplification-7] hard conflict limit 226184 (soft 189518 + delta 36666)
c [simplification-7] new conflict limit 189518 (hard 226184)
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 -   32.8    5217   125083    141884   30131   1901  2777   11    25   20  47%    509    8   11   10  118%
c -   38.6    5217   125083    181087   35654   1974  2782   10    16   20  65%    741   -1   13   10  129%
c 
c [simplification-8] limit 189518 conflicts (hard 226184) hit after 191750 conflicts
c [quatres-6] found 27049 quaternary clauses 28% in total
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 16 single-self-subsuming ternary resolvents
c [quatres-6-2] added 49 quaternary resolvents
c [ternres-6] limit 15379435 with penalty 0 = 0 + 0
c [ternres-6] all 5217 free variables schedulable
c [ternres-6] 132 ternary resolvents (4 bin, 128 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 768971 penalty 2 = 2 + 0
c [gauss-3] extracted 163 xors of average arity 3.0
c [gauss-3] connected 483 occurrences of 336 variables (average 1.4)
c [gauss-3] limit 768971 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 6 variables
c [basicprobe-3] limit 76897175 penalty 0 = 0 + 0
c [basicprobe-3-0] 669 sched 13%, 3 failed, 0 lifted, 185 hbrs
c [decomp-24] removed 4 variables
c [basicprobe-3-1] 1054 sched 20%, 1 failed, 0 lifted, 101 hbrs
c [decomp-25] removed 4 variables
c [basicprobe-3-2] 1051 sched 20%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-3-3] 1051 sched 20%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-3-4] 1051 sched 20%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-5] 1051 sched 20%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-6] 1051 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-6] fully completed probing
c [basicprobe-3-6] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-3-6] removed 8 variables, found 304 hbrs
c [bate-2] eliminated 46 asymmetric tautologies during probing
c [unhide-5] limit 768971 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 229 tauts, 0 hbrs, 13435 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 196 transitive binary clauses
c [bca-6] limit of 10000000 steps and 250026 added (scaled 2)
c [bca-6] 7756 out of 10408 literals actually usable 75%
c [bca-6] added 0 blocked clauses in 63350 steps
c [sweep-7] limit 4613830 penalty 0 = 0 + 0
c [sweep-7-1] 2177 pos 55.6% + 1738 neg 44.4% = 3915 sched 75.2% ret 1288
c [sweep-7-1] 4625949 steps 221 queries 116.27 avg class size
c [sweep-7-1] 5928 decisions 227 SAT calls 55.32 avg env size
c [sweep-7-1] 2006 variables remain 39% (3197 retained 61%)
c [decomp-30] removed 13 variables
c [sweep-7-1] removed 13 vars (0 failed, 8 eqs, 0 impls)
c [sweep-7] removed 13 vars in TOTAL (1 rounds, 220 queries)
c [sort-queue-8] sorted 5190 enqueued variables after 191750 conflicts
c [score-dist-8] active 0 (0%), one 2712 (52%), zero 2478 (48%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 27 variables 0.5% (5190 remain 56%)
c [simplification-8] removed 347 irredundant clauses 0.3% (124736 remain 88%)
c [simplification-8] maximum reduction of 1% = max (1%, 0%)
c [simplification-8] geometric conflict interval increment 36666 = 73332 / 2
c [simplification-8] new conflict interval 109998
c [simplification-8] penalized conflict interval 109998 = 1 * 109998
c [simplification-8] hard conflict limit 356747 (soft 301748 + delta 54999)
c [simplification-8] new conflict limit 301748 (hard 356747)
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.0    5189   124736    214006   66955   2054  2861    8    13   18  65%    853   -3    6   10   59%
c -   45.5    5186   124736    216332   38683   2066  2863    9    14   13  66%   -961   -1    9   10   88%
c i   45.5    5185   124736    216403   38739   2068  2865    9    14   15  66%   -973   -1    8   10   83%
c i   49.5    5184   124736    241897   61854   2113  2877   10    15   24  70%   -493   -0    9   10   93%
c i   51.4    5181   124736    253657   72292   2149  2883    9    13   28  73%   -582   -2    6   10   63%
c -   51.4    5181   124736    253670   40251   2149  2883    9    13   21  73%   -584   -2    7   10   67%
c -   57.4    5181   124736    291101   42260   2205  2884   11    18   21  64%     12    2   13   10  123%
c 
c [simplification-9] limit 301748 conflicts (hard 356747) hit after 301751 conflicts
c [quatres-7] found 27460 quaternary clauses 27% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 19 single-self-subsuming ternary resolvents
c [quatres-7-2] added 17 quaternary resolvents
c [ternres-7] limit 25383702 with penalty 0 = 0 + 0
c [ternres-7] all 5181 free variables schedulable
c [ternres-7] 95 ternary resolvents (0 bin, 95 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-31] removed 13 variables
c [simpleprobe-4] 3334 schedulable variables 64%
c [simpleprobe-4] limit 101534809 penalty 0 = 0 + 0
c [decomp-32] removed 72 variables
c [simpleprobe-4] 1128 variables remain 22% (3977 retained 78%)
c [simpleprobe-4] removed 72 variables, found 2954 hbrs, 1 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1489 transitive binary clauses
c [sweep-8] limit 7615110 penalty 0 = 0 + 0
c [sweep-8-1] 1039 pos 52.6% + 936 neg 47.4% = 1975 sched 38.7% ret 3130
c [sweep-8-1] 7616551 steps 649 queries 20.93 avg class size
c [sweep-8-1] 14292 decisions 640 SAT calls 52.46 avg env size
c [sweep-8-1] 107 variables remain 2% (4998 retained 98%)
c [decomp-33] removed 20 variables
c [sweep-8-1] removed 20 vars (0 failed, 28 eqs, 4 impls)
c [sweep-8] removed 20 vars in TOTAL (1 rounds, 648 queries)
c [sort-queue-9] sorted 5085 enqueued variables after 301751 conflicts
c [score-dist-9] active 0 (0%), one 2722 (54%), zero 2363 (46%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 96 variables 1.9% (5085 remain 55%)
c [simplification-9] removed 476 irredundant clauses 0.4% (124260 remain 88%)
c [simplification-9] maximum reduction of 2% = max (2%, 0%)
c [simplification-9] geometric conflict interval increment 36666 = 109998 / 3
c [simplification-9] new conflict interval 146664
c [simplification-9] penalized conflict interval 146664 = 1 * 146664
c [simplification-9] hard conflict limit 521747 (soft 448415 + delta 73332)
c [simplification-9] new conflict limit 448415 (hard 521747)
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 -   64.7    5085   124260    329611   44837   2294  4249   10    15   22  68%    462   -0   10   10   95%
c i   64.8    5084   124260    330589   45675   2317  4253   10    15   24  69%    470   -1    8   10   74%
c -   70.7    5084   124260    367681   46980   2365  4256   10    15   22  72%     16   -1   11   10  105%
c -   76.7    5084   124260    406895   49944   2407  4266   11    15   22  71%    470    0   11   10  110%
c i   78.1    5083   124260    416316   58273   2439  4270    9    13   25  73%    544   -2    7   10   67%
c i   79.7    5082   124260    427267   67987   2467  4278   10    13   26  76%   -533   -2    9   10   94%
c -   83.4    5079   124260    446799   52051   2482  4279   10    14   22  72%   -261    0   10   10  100%
c i   86.7    5078   124260    468278   71017   2531  4290    9    11   26  79%     98   -3    6   10   62%
c -   90.3    5070   124260    488046   54678   2546  4290   10    13   23  75%   -142   -1   12   10  120%
c 
c [simplification-10] limit 448415 conflicts (hard 521747) hit after 500506 conflicts
c [quatres-8] found 27743 quaternary clauses 27% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 31 single-self-subsuming ternary resolvents
c [quatres-8-2] added 9 quaternary resolvents
c [ternres-8] limit 45420035 with penalty 0 = 0 + 0
c [ternres-8] all 5070 free variables schedulable
c [ternres-8] 70 ternary resolvents (1 bin, 69 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 2838752 penalty 3 = 3 + 0
c [card-4] found 625 at-most-one constraints of average size 3.1
c [card-4] found 109 at-most-two constraints of average size 4.6
c [card-4] using previous limit 2838752 for elimination
c [card-4] 733 out of 734 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-34] removed 15 variables
c [treelook-4] limit 4542003 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 10027 literals 99%
c [treelook-4] scheduling used 447743 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 4542003 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 4552857 steps
c [treelook-4] 9382 literals remain 93%
c [treelook-4] 4924 variables remain to probed next time 97%
c [treelook-4] removed 0 variables, found 842 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1089 transitive binary clauses
c [bca-7] limit of 10000000 steps and 248354 added (scaled 2)
c [bca-7] 7554 out of 10142 literals actually usable 74%
c [bca-7] added 0 blocked clauses in 78431 steps
c [sweep-9] limit 13626010 penalty 0 = 0 + 0
c [sweep-9-1] 41 pos 38.3% + 66 neg 61.7% = 107 sched 2.1% ret 4963
c [sweep-9-1] 412500 steps 84 queries 9.42 avg class size
c [sweep-9-1] 2406 decisions 83 SAT calls 71.20 avg env size
c [sweep-9-1] fully completed sweeping round
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9-2] 2840 pos 56.0% + 2230 neg 44.0% = 5070 sched 100.0% ret 0
c [sweep-9-2] 13234571 steps 527 queries 75.88 avg class size
c [sweep-9-2] 13257 decisions 534 SAT calls 55.56 avg env size
c [sweep-9-2] 959 variables remain 19% (4108 retained 81%)
c [decomp-37] removed 18 variables
c [sweep-9-2] removed 18 vars (0 failed, 19 eqs, 0 impls)
c [sweep-9] removed 18 vars in TOTAL (2 rounds, 609 queries)
c [sort-queue-10] sorted 5052 enqueued variables after 500506 conflicts
c [score-dist-10] active 0 (0%), one 2784 (55%), zero 2268 (45%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 18 variables 0.4% (5052 remain 55%)
c [simplification-10] removed 431 irredundant clauses 0.3% (123829 remain 88%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 146664
c [simplification-10] new conflict interval 293328
c [simplification-10] penalized conflict interval 293328 = 1 * 293328
c [simplification-10] hard conflict limit 940498 (soft 793834 + delta 146664)
c [simplification-10] new conflict limit 793834 (hard 940498)
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 -   98.9    5052   123829    530777   54983   2611  4069   10    14   14  71%    416    1    9   10   92%
c i   99.5    5051   123829    534399   58047   2637  4077    9    12   17  75%    449   -1    8   10   77%
c -  106.1    5050   123829    573116   57797   2703  4081    9    12   24  76%    124   -1    8   10   84%
c i  107.2    5049   123829    580849   64411   2727  4088    9    11   26  78%    224   -3    7   10   71%
c -  113.9    5042   123829    617835   61391   2772  4093    9    12   24  78%    150   -1   10    9  105%
c i  114.3    5041   123829    619999   63318   2778  4095    9    12   26  77%    178   -0    8    9   83%
c i  118.4    5040   123829    645948   85764   2841  4103    8    13   27  64%     37    0   10    9  105%
c i  119.5    5038   123829    652178   91036   2881  4111    8    16   29  51%   -247    3    6    9   66%
c i  119.9    5026   123829    654679   93099   2926  4123    8    15   30  52%   -287    2    5    9   54%
c i  120.0    5016   123829    655074   93384   2938  4126    7    14   30  53%   -295    1    5    9   59%
c i  120.4    5008   123829    657995   95820   2976  4138    8    21   30  39%   -272    7    8    9   86%
c i  120.6    4985   123829    659210   96945   2988  4143    9    28   30  31%   -281   14   10    9  107%
c i  120.6    4976   123829    659258   96963   2991  4154    8    27   30  31%   -282   14    9    9   95%
c i  120.7    4971   123829    659769   97398   3004  4163    9    28   30  30%   -285   15   10    9  113%
c i  120.7    4801   123829    660156   97757   3010  4167    9    29   30  30%   -286   16   10    9  114%
c i  120.8    4798   123829    661190   98723   3018  4172    9    28   31  31%   -281   14   10    9  110%
c -  121.1    4796   123829    663430   64596   3045  4175    9    28   24  32%   -259   14    9    9  105%
c i  121.2    4795   123829    664647   65733   3067  4180    9    30   27  30%   -238   15   10    9  114%
c i  121.3    4792   123829    665919   66910   3085  4185    9    33   27  29%   -252   17    9    9  105%
c i  121.9    4789   123829    672697   73306   3116  4194    9    31   28  28%   -159   15    9    9  100%
c i  121.9    4749   123829    672995   73572   3124  4196    9    31   28  28%   -181   15    9    9  103%
c i  122.4    4748   123829    677522   77830   3159  4208    9    36   28  25%   -179   18   10    9  116%
c i  122.6    4745   123829    679031   79255   3172  4211    9    36   28  26%   -206   18    9    9   95%
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  123.5    4718   123829    686601   86414   3221  4217    9    28   28  32%   -108    9   10    9  113%
c 
c [simplification-11] limit of 304 binary hit after 360 binaries
c [quatres-9] found 22441 quaternary clauses 29% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 5 single-self-subsuming ternary resolvents
c [quatres-9-2] added 13 quaternary resolvents
c [ternres-9] limit 64716402 with penalty 0 = 0 + 0
c [ternres-9] all 4715 free variables schedulable
c [ternres-9] 21 ternary resolvents (3 bin, 18 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-38] removed 378 variables
c [basicprobe-4] limit 323582010 penalty 0 = 0 + 0
c [basicprobe-4-0] 825 sched 18%, 27 failed, 5 lifted, 669 hbrs
c [decomp-39] removed 33 variables
c [basicprobe-4-1] 836 sched 18%, 12 failed, 0 lifted, 159 hbrs
c [decomp-40] removed 16 variables
c [basicprobe-4-2] 842 sched 18%, 8 failed, 0 lifted, 60 hbrs
c [decomp-41] removed 9 variables
c [basicprobe-4-3] 840 sched 18%, 3 failed, 0 lifted, 29 hbrs
c [decomp-42] removed 3 variables
c [basicprobe-4-4] 843 sched 18%, 1 failed, 0 lifted, 21 hbrs
c [decomp-43] removed 2 variables
c [basicprobe-4-5] 840 sched 18%, 1 failed, 0 lifted, 11 hbrs
c [decomp-44] removed 1 variables
c [basicprobe-4-6] 841 sched 18%, 1 failed, 0 lifted, 6 hbrs
c [decomp-45] removed 1 variables
c [basicprobe-4-7] 843 sched 18%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-8] 843 sched 18%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 58 units = 53 failed (91%) + 5 lifted (9%)
c [basicprobe-4-8] removed 65 variables, found 972 hbrs
c [bate-3] eliminated 125 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 635 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4609 variables 100%
c [block-4] limit of 80895502 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 735 blocked clauses
c [block-4] 735 < 1/100 * 110527 = 1105 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 404477512 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 582 (1%) of length 12
c [cce-4-1] eliminated 4 clauses out of 92 (4%) of length 11
c [cce-4-1] eliminated 4 clauses out of 210 (2%) of length 10
c [cce-4-1] eliminated 5 clauses out of 899 (1%) of length 9
c [cce-4-1] eliminated 145 clauses out of 2467 (6%) of length 8
c [cce-4-1] eliminated 211 clauses out of 6869 (3%) of length 7
c [cce-4-1] eliminated 627 clauses out of 15409 (4%) of length 6
c [cce-4-1] eliminated 611 clauses out of 23534 (3%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 1611 large clauses in 404477529 steps
c [cce-4-1] allowing another 202238764 steps for small clauses
c [cce-4-1] scheduling 35101 clauses = 9031 binary + 26070 ternary
c [cce-4-1] tried to eliminate 35101 small clauses 100%
c [cce-4-1] eliminated 275 binary clauses 3%
c [cce-4-1] eliminated 1553 ternary clauses 6%
c [cce-4-1] eliminated 1828 small clauses 5%
c [cce-4-1] eliminated 1828 small clauses in 320825903 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 3439 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 41826235 steps for small clauses
c [cce-4-2] scheduling 33275 clauses = 8756 binary + 24519 ternary
c [cce-4-2] tried to eliminate 12273 small clauses 37%
c [cce-4-2] eliminated 1 ternary clauses 0%
c [cce-4-2] eliminated 1 small clauses 0%
c [cce-4-2] eliminated 1 small clauses in 83651814 steps
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 1 covered clauses in round 2
c [cce-4] eliminated 3440 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 4569 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 144 not tried 3% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 122 = 3% variables out of 4569 scheduled
c [sweep-10] limit 19414920 penalty 0 = 0 + 0
c [sweep-10-1] 475 pos 53.9% + 407 neg 46.1% = 882 sched 19.8% ret 3565
c [sweep-10-1] 3597245 steps 396 queries 12.14 avg class size
c [sweep-10-1] 9644 decisions 396 SAT calls 59.98 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-47] removed 6 variables
c [sweep-10-1] removed 6 vars (0 failed, 12 eqs, 1 impls)
c [sweep-10-2] 2496 pos 56.2% + 1945 neg 43.8% = 4441 sched 100.0% ret 0
c [sweep-10-2] 9221010 steps 731 queries 31.78 avg class size
c [sweep-10-2] 20133 decisions 745 SAT calls 62.23 avg env size
c [sweep-10-2] fully completed sweeping round
c [decomp-48] removed 29 variables
c [sweep-10-2] removed 29 vars (0 failed, 37 eqs, 6 impls)
c [sweep-10-3] 2474 pos 56.1% + 1938 neg 43.9% = 4412 sched 100.0% ret 0
c [sweep-10-3] 6606916 steps 349 queries 73.14 avg class size
c [sweep-10-3] 11065 decisions 364 SAT calls 68.25 avg env size
c [sweep-10-3] 910 variables remain 21% (3502 retained 79%)
c [decomp-49] removed 14 variables
c [sweep-10-3] removed 14 vars (0 failed, 16 eqs, 0 impls)
c [sweep-10] removed 49 vars in TOTAL (3 rounds, 1473 queries)
c [sort-queue-11] sorted 4398 enqueued variables after 699773 conflicts
c [score-dist-11] active 0 (0%), one 2556 (58%), zero 1842 (42%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 317 variables 6.7% (4398 remain 48%)
c [simplification-11] removed 18204 irredundant clauses 14.7% (105625 remain 75%)
c [simplification-11] maximum reduction of 15% = max (7%, 15%)
c [simplification-11] forced so keeping old conflict interval 293328
c [simplification-11] conflict limit remains at 793834 (hard 940498)
c [simplification-11] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  134.1    4397   105625    706139   36546   2800  3474   10    25   15  38%     95    4    9    9  102%
c -  142.0    4397   105625    750560   39479   2893  3509   10    22   18  43%    395    2   11    9  115%
c i  142.9    4396   105625    756509   45170   2912  3511    9    22   21  44%    449    1   11    9  117%
c -  150.9    4396   105625    796484   46146   2965  3521    9    18   19  51%    277   -2   10    9  112%
c 
c [simplification-12] limit 793834 conflicts (hard 940498) hit after 799616 conflicts
c [quatres-10] found 22296 quaternary clauses 26% in total
c [quatres-10-1] removed 9 duplicate quaternary clauses
c [quatres-10-2] added 8 single-self-subsuming ternary resolvents
c [quatres-10-2] added 29 quaternary resolvents
c [ternres-10] limit 71867533 with penalty 0 = 0 + 0
c [ternres-10] all 4396 free variables schedulable
c [ternres-10] 91 ternary resolvents (0 bin, 91 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1796688 penalty 3 = 3 + 0
c [gauss-4] extracted 229 xors of average arity 2.9
c [gauss-4] connected 672 occurrences of 318 variables (average 2.1)
c [gauss-4] limit 1796688 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-50] removed 3 variables
c [simpleprobe-5] 918 schedulable variables 21%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-51] removed 5 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 5 variables, found 1285 hbrs, 1 units
c [unhide-6] limit 1796688 with penalty 3 = 3 + 0
c [unhide-6-7] 0 units, 0 failed, 1675 tauts, 0 hbrs, 18631 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 497 transitive binary clauses
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 215602590 penalty 0 = 0 + 0
c [sweep-11-1] 426 pos 47.0% + 481 neg 53.0% = 907 sched 20.7% ret 3481
c [sweep-11-1] 5718802 steps 399 queries 13.19 avg class size
c [sweep-11-1] 10331 decisions 399 SAT calls 58.90 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-52] removed 7 variables
c [sweep-11-1] removed 7 vars (0 failed, 13 eqs, 0 impls)
c [sweep-11-2] 2509 pos 57.3% + 1872 neg 42.7% = 4381 sched 100.0% ret 0
c [sweep-11-2] 11679899 steps 723 queries 22.50 avg class size
c [sweep-11-2] 19510 decisions 747 SAT calls 59.51 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-53] removed 33 variables
c [sweep-11-2] removed 33 vars (0 failed, 41 eqs, 1 impls)
c [sweep-11-3] 2486 pos 57.2% + 1862 neg 42.8% = 4348 sched 100.0% ret 0
c [sweep-11-3] 14974118 steps 713 queries 24.27 avg class size
c [sweep-11-3] 19812 decisions 730 SAT calls 62.06 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-54] removed 28 variables
c [sweep-11-3] removed 28 vars (0 failed, 38 eqs, 2 impls)
c [sweep-11] removed 68 vars in TOTAL (3 rounds, 1832 queries)
c [sort-queue-12] sorted 4320 enqueued variables after 799616 conflicts
c [score-dist-12] active 0 (0%), one 2702 (63%), zero 1618 (37%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 76 variables 1.7% (4320 remain 47%)
c [simplification-12] removed 838 irredundant clauses 0.8% (104787 remain 74%)
c [simplification-12] maximum reduction of 2% = max (2%, 1%)
c [simplification-12] geometric conflict interval increment 97776 = 293328 / 3
c [simplification-12] new conflict interval 391104
c [simplification-12] penalized conflict interval 391104 = 1 * 391104
c [simplification-12] hard conflict limit 1386272 (soft 1190720 + delta 195552)
c [simplification-12] new conflict limit 1190720 (hard 1386272)
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 -  161.8    4320   104787    836585   48290   3001  2939   10    18   20  57%    619   -1   10   10  105%
c -  171.6    4320   104787    879807   47867   3032  2950   10    19   20  56%    815   -1   10   10  101%
c -  181.0    4320   104787    927640   52020   3058  2959   10    16   21  65%    923   -3   10   10   95%
c -  190.9    4320   104787    974089   54137   3081  2964   11    18   21  58%    974    0   10   10   95%
c -  201.5    4320   104787   1021412   56692   3100  2973   10    15   21  64%   1000   -3   10   10   95%
c -  211.4    4320   104787   1067666   59131   3109  2977   10    13   21  75%   1012   -3   11   10  104%
c i  212.8    4319   104787   1074666   65755   3111  2979   11    17   24  66%   1013    1   12   10  120%
c -  222.9    4319   104787   1114549   59789   3118  2983   11    17   21  64%  -1730    1   11   11  100%
c -  233.3    4319   104787   1162573   62853   3133  2990   10    13   21  72%   -299   -3   11   10  102%
c 
c [simplification-13] limit 1190720 conflicts (hard 1386272) hit after 1190720 conflicts
c [quatres-11] found 22316 quaternary clauses 22% in total
c [quatres-11-1] removed 8 duplicate quaternary clauses
c [quatres-11-2] added 23 single-self-subsuming ternary resolvents
c [quatres-11-2] added 47 quaternary resolvents
c [ternres-11] limit 109163167 with penalty 0 = 0 + 0
c [ternres-11] all 4319 free variables schedulable
c [ternres-11] 47 ternary resolvents (0 bin, 47 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-55] removed 2 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 392 transitive binary clauses
c [transred-11] found 1 units
c [cce-5] limit of 136453958 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 84 clauses out of 84 (100%) of length 14
c [cce-5-1] eliminated 74 clauses out of 261 (28%) of length 13
c [cce-5-1] eliminated 13 clauses out of 582 (2%) of length 12
c [cce-5-1] eliminated 14 clauses out of 88 (16%) of length 11
c [cce-5-1] eliminated 50 clauses out of 212 (24%) of length 10
c [cce-5-1] eliminated 163 clauses out of 892 (18%) of length 9
c [cce-5-1] eliminated 46 clauses out of 2309 (2%) of length 8
c [cce-5-1] eliminated 919 clauses out of 6680 (14%) of length 7
c [cce-5-1] eliminated 42 clauses out of 14721 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1405 large clauses in 136453965 steps
c [cce-5-1] allowing another 68226982 steps for small clauses
c [cce-5-1] scheduling 11647 clauses = 8301 binary + 3346 ternary
c [cce-5-1] tried to eliminate 11647 small clauses 100%
c [cce-5-1] eliminated 411 binary clauses 5%
c [cce-5-1] eliminated 833 ternary clauses 25%
c [cce-5-1] eliminated 1244 small clauses 11%
c [cce-5-1] eliminated 1252 small clauses in 115646483 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 2657 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 10404063 steps for small clauses
c [cce-5-2] scheduling 10403 clauses = 7890 binary + 2513 ternary
c [cce-5-2] tried to eliminate 2865 small clauses 28%
c [cce-5-2] incomplete small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 2657 covered clauses in TOTAL during 2 rounds
c [elim-6] 144 variables 3% will be scheduled this time
c [elim-6] scheduled 144 variables 3%
c [elim-6] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 152931639 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 144 scheduled
c [bca-8] limit of 10000000 steps and 202086 added (scaled 2)
c [bca-8] 5681 out of 8636 literals actually usable 66%
c [bca-8] added 2 blocked clauses in 101175 steps
c [sweep-12] limit 32748950 penalty 0 = 0 + 0
c [sweep-12-1] 2455 pos 56.9% + 1862 neg 43.1% = 4317 sched 100.0% ret 0
c [sweep-12-1] 16341009 steps 704 queries 25.34 avg class size
c [sweep-12-1] 17544 decisions 707 SAT calls 57.38 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-56] removed 16 variables
c [sweep-12-1] removed 16 vars (0 failed, 34 eqs, 2 impls)
c [sweep-12-2] 2447 pos 56.9% + 1854 neg 43.1% = 4301 sched 100.0% ret 0
c [sweep-12-2] 17053606 steps 570 queries 28.32 avg class size
c [sweep-12-2] 14809 decisions 572 SAT calls 57.76 avg env size
c [sweep-12-2] 336 variables remain 8% (3965 retained 92%)
c [decomp-57] removed 15 variables
c [sweep-12-2] removed 15 vars (0 failed, 28 eqs, 1 impls)
c [sweep-12] removed 31 vars in TOTAL (2 rounds, 1272 queries)
c [sort-queue-13] sorted 4286 enqueued variables after 1190720 conflicts
c [score-dist-13] active 0 (0%), one 2840 (66%), zero 1446 (34%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 33 variables 0.8% (4286 remain 47%)
c [simplification-13] removed 4018 irredundant clauses 3.8% (100769 remain 71%)
c [simplification-13] maximum reduction of 4% = max (1%, 4%)
c [simplification-13] geometric conflict interval increment 78220 = 391104 / 5
c [simplification-13] new conflict interval 469324
c [simplification-13] penalized conflict interval 469324 = 1 * 469324
c [simplification-13] hard conflict limit 1894706 (soft 1660044 + delta 234662)
c [simplification-13] new conflict limit 1660044 (hard 1894706)
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 -  248.8    4286   100769   1208537   64077   3987  3243   10    14   15  76%    368   -2   11   11  107%
c -  260.2    4286   100769   1257836   66217   3996  3247    9    12   25  81%    715   -4    8   10   78%
c -  274.3    4286   100769   1308032   65683   4014  3257   11    18   24  61%    880    2   10   11   94%
c -  288.8    4286   100769   1363061   69754   4024  3261    9    11   25  78%    962   -4    8   10   82%
c -  302.7    4286   100769   1415497   70757   4038  3264   11    16   25  67%    996    1   13   10  124%
c -  317.8    4286   100769   1467590   71384   4047  3267   11    17   25  65%   1011    1   10   11   95%
c -  332.4    4286   100769   1523218   74385   4055  3271   11    15   25  71%   1019   -1   12   11  113%
c -  347.2    4286   100769   1577292   76505   4064  3274   10    14   25  75%   1022   -2    9   11   86%
c -  361.9    4286   100769   1635421   78249   4079  3276    9    12   25  75%   1023   -2   10   10  103%
c 
c [simplification-14] limit 1660044 conflicts (hard 1894706) hit after 1679264 conflicts
c [quatres-12] found 22338 quaternary clauses 21% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-1] added 1 double-self-subsuming ternary resolvents
c [quatres-12-2] added 31 single-self-subsuming ternary resolvents
c [quatres-12-2] added 45 quaternary resolvents
c [ternres-12] limit 170366113 with penalty 0 = 0 + 0
c [ternres-12] all 4286 free variables schedulable
c [ternres-12] 44 ternary resolvents (0 bin, 44 trn)
c [ternres-12] fully completed ternary resolution
c [treelook-5] limit 8518305 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 8501 literals 99%
c [treelook-5] scheduling used 505108 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 8518305 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 8518764 steps
c [treelook-5] 6501 literals remain 76%
c [treelook-5] 4026 variables remain to probed next time 94%
c [decomp-59] removed 2 variables
c [treelook-5] removed 2 variables, found 841 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 592 transitive binary clauses
c [cce-6] limit of 425915284 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 5 clauses out of 2263 (0%) of length 8
c [cce-6-1] eliminated 22 clauses out of 5761 (0%) of length 7
c [cce-6-1] eliminated 542 clauses out of 14401 (4%) of length 6
c [cce-6-1] eliminated 1147 clauses out of 22890 (5%) of length 5
c [cce-6-1] eliminated 220 clauses out of 19446 (1%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1936 large clauses in 425915570 steps
c [cce-6-1] allowing another 212957785 steps for small clauses
c [cce-6-1] scheduling 10391 clauses = 7875 binary + 2516 ternary
c [cce-6-1] tried to eliminate 10391 small clauses 100%
c [cce-6-1] eliminated 5 binary clauses 0%
c [cce-6-1] eliminated 3 ternary clauses 0%
c [cce-6-1] eliminated 8 small clauses 0%
c [cce-6-1] eliminated 8 small clauses in 249726639 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 1944 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 88094470 steps for small clauses
c [cce-6-2] scheduling 10383 clauses = 7870 binary + 2513 ternary
c [cce-6-2] tried to eliminate 10383 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 1944 covered clauses in TOTAL during 2 rounds
c [sweep-13] limit 51109834 penalty 0 = 0 + 0
c [sweep-13-1] 171 pos 51.2% + 163 neg 48.8% = 334 sched 7.8% ret 3950
c [sweep-13-1] 1486608 steps 197 queries 9.57 avg class size
c [sweep-13-1] 4233 decisions 188 SAT calls 57.91 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-60] removed 10 variables
c [sweep-13-1] removed 10 vars (0 failed, 8 eqs, 0 impls)
c [sweep-13-2] 2454 pos 57.4% + 1820 neg 42.6% = 4274 sched 100.0% ret 0
c [sweep-13-2] 29505708 steps 745 queries 21.56 avg class size
c [sweep-13-2] 19757 decisions 750 SAT calls 57.83 avg env size
c [sweep-13-2] fully completed sweeping round
c [decomp-61] removed 22 variables
c [sweep-13-2] removed 22 vars (0 failed, 34 eqs, 1 impls)
c [sweep-13-3] 2436 pos 57.3% + 1816 neg 42.7% = 4252 sched 100.0% ret 0
c [sweep-13-3] 20117706 steps 439 queries 45.90 avg class size
c [sweep-13-3] 12079 decisions 444 SAT calls 59.12 avg env size
c [sweep-13-3] 625 variables remain 15% (3627 retained 85%)
c [decomp-62] removed 8 variables
c [sweep-13-3] removed 8 vars (0 failed, 13 eqs, 0 impls)
c [sweep-13] removed 40 vars in TOTAL (3 rounds, 1378 queries)
c [sort-queue-14] sorted 4244 enqueued variables after 1679264 conflicts
c [score-dist-14] active 0 (0%), one 2955 (70%), zero 1289 (30%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 42 variables 1.0% (4244 remain 46%)
c [simplification-14] removed 2292 irredundant clauses 2.3% (98477 remain 70%)
c [simplification-14] maximum reduction of 2% = max (1%, 2%)
c [simplification-14] geometric conflict interval increment 156441 = 469324 / 3
c [simplification-14] new conflict interval 625765
c [simplification-14] penalized conflict interval 625765 = 1 * 625765
c [simplification-14] hard conflict limit 2617911 (soft 2305029 + delta 312882)
c [simplification-14] new conflict limit 2305029 (hard 2617911)
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 -  385.9    4244    98477   1688984   77893   4173  3625   12    18   16  64%   1024    4   10   10   92%
c i  403.0    4243    98477   1744620  127846   4184  3625   12    20   35  59%   1024    5   11   11  107%
c -  404.0    4243    98477   1747730   81036   4184  3625   11    16   27  66%  -8608    1    9   11   83%
c -  423.4    4243    98477   1806846   82178   4192  3627   11    14   28  75%  -3091   -1   10   11   97%
c -  442.7    4243    98477   1866194   84316   4223  3632   12    17   28  71%   -640    1   12   11  107%
c -  462.1    4243    98477   1925032   86815   4232  3634   12    18   28  67%    346    2   10   11   90%
c -  484.7    4243    98477   1986829   88493   4254  3636   12    17   28  72%    760    2   12   11  107%
c -  504.6    4243    98477   2049186   91354   4265  3639   10    12   29  80%    922   -2   13   11  121%
c -  526.8    4243    98477   2111367   92858   4292  3641   11    15   29  75%    985    1    9   11   87%
c i  532.6    4242    98477   2133479  111632   4317  3650    8    10   35  80%    996   -4    6   10   58%
c i  540.4    4236    98477   2159319  131798   4361  3662    8    10   37  80%  -3156   -3    6   10   62%
c i  541.8    4226    98477   2163096  134779   4384  3672    8    10   37  78%  -3299   -3    6   10   65%
c i  542.0    4189    98477   2163806  135330   4397  3678    8    10   37  77%  -3287   -3    7   10   77%
c i  542.4    4186    98477   2165403  136635   4403  3682    8    11   37  76%  -3218   -2    7   10   76%
c i  542.5    4111    98477   2165404  136635   4403  3682    8    11   37  76%  -3218   -2    7   10   76%
c i  542.5    4106    98477   2165405  136635   4403  3682    8    11   37  76%  -3218   -2    7   10   76%
c 0  542.5    3441    98477   2165405  136635   4403  3682    8    11   37  76%  -3218   -2    7   10   76%
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: 406 basic ate = 166 trn 41% + 240 lrg 59% in 3 updates
c bcas: 8 count, 94 added (246 skipped), 443663 steps
c bkwd: tried 36444 clauses, 72352 lits, 1.99 lits/clause
c bkwd: checked 5671425 occs, 155.62 occs/clause, 78.39 occs/lit
c bkwd: subsumed 0 binary, 3 ternary, 323 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 268 large (0% self)
c blkd: 4 bces, 1979 removed, 2351293 resolutions, 7549771 steps
c blkd: 2105 blocking literals 11%, 40 pure
c bump: 2179730 bumped seen, 102473138 lits 47.0 on average
c card: 4 count, 0 units, 0 am1, 11537422 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 9998 subsumed
c card: 3966 at-most-one constraints found, average size 3.08
c card: 3966 at-most-one constraints used 100%, average size 3.08
c card: 262 at-most-two constraints found, average size 4.70
c card: 261 at-most-two constraints used 100%, average size 4.70
c cces: 6 cces, 9574 eliminated, 7017 ate 73%, 2557 abce 27%
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: 781345 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 81 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 62 decompositions, 1817 equivalent 19%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 3534893 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 2445 eliminated 25%, 430 pure 18%
c elms: 9 rounds, 1.5 rounds/bve
c elms: 1531 small 63%, 444 large 18%
c elms: 2790 tried small, 1531 succeeded 55%, 1259 failed 45%
c elms: 2974 subsumed, 634 strengthened, 312 blocked
c elms: 1371386 copies, 1909136 resolutions, 87500 ipos
c elms: 3704398 subchks, 614870 strchks
c gaus: 4 extractions, 1027 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 11136162 steps, 5568081 extr 50%, 53517 elim 0%
c glue: 10.3 orig avg, 10.3 real avg, 2.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 16380 = 7811 simple 48% + 7311 trn 45% + 1258 lrg 8%, 503 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2179730 clauses, 20.8 length
c lrnd: 45256933 lits = 64696248 orig - 19439315 removed 30%
c lrnd: 538734 uips 25%, 1486035 flips 68%
c mins: 2160182 mins 99%, 422 bin 0%, 19126 size 1%
c mins: 44525474 poisoned searches, 8075155 hits, 18% hit rate
c mins: 98848641 used twice searches, 12103814 hits, 12% hit rate
c move: moved 5314, 1274 bin 24%, 4040 trn 76%
c otfs: 6359 driving 30%, 14716 restarting 70%
c otfs: str 21075, 20836 red 99%, 239 irr 1%
c otfs: str 21075, 0 bin 0%, 305 trn 1%, 20770 lrg 99%
c otfs: sub 112, 112 red 100%, 0 irr 0%
c otfs: sub 112, 0 bin 0%, 14 trn 12%, 98 lrg 88%
c phas: 7 computed, 5910 set, 3358 pos (57%), 2552 neg (43%)
c prbs: 4 basic, 34907 probed, 79 failed, 5 lifted
c prbs: 5 simple, 27487 probed, 23 failed, 411 eqs
c prbs: 5 treelook, 2844 probed, 5 failed, 0 lifted
c prom: 645778 locked 18% out of 3680575 tried
c prps: 413212160 props, 115 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 12 count, 325 quat, 180 self1, 4 self2, 1856 dup
c queu: 14 sorted, 3534893 next (3 steps 0.00)
c queu: 102553245 enq (102553216 steps 1.00), 102473138 deq 100%
c redc: 25556 clauses 7%, 366037 tried 17%, 12 sat 0%
c redc: 32326 lits 1%, 4605586 tried 7%, 12 sat 0%
c redc: 951 times jump level reduced, 2.0 levels on average
c reds: 43 count, 50358.3 conflicts per reduce
c reds: 0 memlim 0%, 43 arith 100%
c reds: 1526564 collected 87%, 231132 retired 13%
c rmbd: 673 removed, 268 red 40%
c rsts: 41022 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, 13 confs 93%, 0 vars 0%
c simp: 0 its 0%, 1 bin 7%, 0 trns 0%
c subl: 2179730 count (700305 tried 0.3), 203178 sub out of 2174762 (9.3%)
c swps: 13 count, 22 rounds, 8748 queries (397.6/round)
c swps: 8785 sat calls, 464 unsat (2.4% success rate)
c swps: 227377 decisions 25.9, 20684 conflicts 2.4
c swps; 55.2 avg class size, 58.6 avg environment size
c swps: 0 failed, 43 impls, 426 equivs
c swp0: 2907 type 0 queries, 1247 unsat (42.9%), 2810 sat (96.7%)
c swp1: 5841 type 1 queries, 3119 unsat (53.4%), 5512 sat (94.4%)
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: 11429594 calls to obtain time
c tops: 1887 fixed 20%, 42 its, 51557.26 confs/it
c trds: 12 transitive reductions, 7268 removed, 3 failed
c trds: 112224 nodes, 142353 edges, 3287546 steps
c trim: 1073544 words, 4.1 MB
c trnr: 12 count, 8 bin, 594 trn, 61925316 steps
c unhd: 6 count, 7 rounds, 9489825 steps
c unhd: 464 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 1 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 4822 tauts, 561 bin 12%, 484 trn 10%, 619 lrg 13%
c unhd: 4822 tauts, 3158 stamp 65%, 3470 red 72%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 44720 str, 1 bin 0%, 185 trn 0%, 44534 lrg 100%, 44458 red 99%
c vars: 3441 remaining 36% and 6149 removed 64% out of 9590
c vars: 1887 fixed 20%, 2445 eliminated 25%, 1817 equivalent 19%
c vsts: 24586082251 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 59.8 search visits per propagation, 11260.4 per conflict
c wchs: 9092592660 pushed, 9871577 enlarged, 157 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2175087       1526564        231132      51052166      18433899       1410682
c 
c  0 0        117136   5     17993   1         0   0  32392303  63   9708936  53    610907  43     2.4
c  1 5        114705   5     67671   4     18709   8   6403764  13<  2446837  13<   207295  15<    0.6
c  2 6        573843  26    424068  28     59719  26   8760745  17   3985379  22    386263  27     2.2
c  3 9        936769  43<   716673  47<    84466  37<  2833913   6   1816172  10    170871  12     3.1
c  4 14       386172  18    272174  18     56385  24    599002   1    435823   2     32302   2     1.4
c  5 21        44472   2     26950   2     11210   5     59898   0     39260   0      2936   0     0.3
c  6 30         1898   0      1000   0       613   0      2425   0      1427   0       101   0     0.0
c  7 41           78   0        32   0        22   0        99   0        59   0         7   0     0.0
c  8 54           10   0         2   0         5   0        12   0         5   0         0   0     0.0
c  9 69            2   0         0   0         2   0         2   0         0   0         0   0     0.0
c 10 86            2   0         1   0         1   0         3   0         1   0         0   0     0.0
c 
c avg                  2.7           2.8           2.9           0.7           1.0           1.2
c std                  1.1           0.9           1.0           1.0           1.2           1.2
c 
c   11.766   2% cce
c    7.756   1% sweep
c    4.491   1% elim
c    4.259   1% probe
c    3.656   1% bump
c 
c    6.307 < 1% rest (below)
c 
c    1.865   0% decide
c    1.595   0% quatres
c    0.847   0% unhide
c    0.516   0% block
c    0.397   0% bca
c    0.351   0% ternres
c    0.299   0% transred
c    0.284   0% gauss
c    0.153   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.814   0% preprocessing     2%
c   33.574   6% inprocessing     98%
c ==================================
c   34.389   6% simplifying
c  508.064  94% search
c ==================================
c  542.453 100% all
c 
c       2165405 conflicts,        3991.9 confs/sec
c          2684 ternaries,         806.8 confs/ternary
c           533 binaries,         4062.7 confs/binary
c            42 iterations,      51557.3 confs/iteration
c 
c            43 reductions,          0.1 redus/sec,  50358.3 confs/reduction
c         41022 restarts,           75.6 rests/sec,     52.8 confs/restart
c       3534893 decisions,        6516.5 decis/sec,      1.6 decis/conflict
c     413212160 propagations,   761747.2 props/sec,    116.9 props/decision
c 
c 542.5 seconds, 43.6 MB
c launch: done
