c launch: /data/cnf/sc2014/app/atco_enc1_opt2_10_14.cnf.bz2
c host: atom19
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_14.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt2_10_14.cnf.bz2
c no embedded options
c found 'p cnf 9569 150316' header
c read 9569 variables, 150316 clauses, 629732 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 9167 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    9167   140791         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 8379 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 211 variables
c [simpleprobe-1] 5561 variables remain 68% (2607 retained 32%)
c [simpleprobe-1] removed 211 variables, found 2407 hbrs, 13 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 3 units, 17 failed, 1047 tauts, 0 hbrs, 17 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 8156 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 2289 variables 28% in round 1 in 7813266 steps
c [elim-1-1] backward subsumption/strengthening limit 7813200
c [elim-1-1-1] backward checking 5611 touched variables 69%
c [elim-1-1-1] incomplete backward checking 2745 remain 49%
c [elim-1-1] subsumed 166 and strengthened 201 clauses in 7813345 steps
c [elim-1-1] rescheduled 210 variables 3% by backward subsumption
c [elim-1-2] eliminated 1 variables 0% in round 2 in 54482 steps
c [elim-1-2] backward subsumption/strengthening limit 54400
c [elim-1-2-1] backward checking 2752 touched variables 34%
c [elim-1-2-1] incomplete backward checking 2740 remain 100%
c [elim-1-2] subsumed 0 and strengthened 3 clauses in 54409 steps
c [elim-1-2] rescheduled 12 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 775 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2290 = 28% variables out of 8156 scheduled
c [phase-count-1] 122092 negative 92.5% of 131986 except 9894 7.5%
c [phase-count-1] 124142 positive 94.1% of 131986 except 7844 5.9%
c [phase-1] phase bias: 3338 positive 57%, 2528 negative 43%
c [sort-queue-1] sorted 5866 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5866 (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 3134 variables 34.8% (5866 remain 64%)
c [simplification-1] removed 8805 irredundant clauses 6.3% (131986 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 1000 conflicts
c [decomp-3] removed 11 variables
c [simpleprobe-2] 4160 schedulable variables 71%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 4212 variables remain 72% (1640 retained 28%)
c [simpleprobe-2] removed 3 variables, found 133 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 9988 literals 85%
c [treelook-1] scheduling used 300126 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 304586 steps
c [treelook-1] 9954 literals remain 85%
c [treelook-1] 5771 variables remain to probed next time 99%
c [decomp-5] removed 6 variables
c [treelook-1] removed 7 variables, found 223 hbrs
c [basicprobe-1] limit 1055624 based on 131953 irredundant clauses
c [basicprobe-1-0] 482 probes remain 8% after last round
c [basicprobe-1-0] 8 units = 8 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 9 variables, found 2182 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 2 failed, 998 tauts, 0 hbrs, 336 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 5835 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 1206 blocked clauses
c [block-1] 1206 < 1/100 * 131915 = 1319 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 22
c [cce-1-1] eliminated 18 clauses out of 18 (100%) of length 21
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 20
c [cce-1-1] eliminated 365 clauses out of 562 (65%) of length 13
c [cce-1-1] eliminated 117 clauses out of 827 (14%) of length 12
c [cce-1-1] eliminated 94 clauses out of 167 (56%) of length 11
c [cce-1-1] eliminated 9 clauses out of 234 (4%) of length 10
c [cce-1-1] eliminated 45 clauses out of 1100 (4%) of length 9
c [cce-1-1] eliminated 36 clauses out of 3018 (1%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 695 large clauses in 30000156 steps
c [cce-1-1] allowing another 15000078 steps for small clauses
c [cce-1-1] scheduling 13932 clauses = 12163 binary + 1769 ternary
c [cce-1-1] tried to eliminate 3831 small clauses 27%
c [cce-1-1] eliminated 432 binary clauses 4%
c [cce-1-1] eliminated 12 ternary clauses 1%
c [cce-1-1] eliminated 444 small clauses 3%
c [cce-1-1] eliminated 444 small clauses in 30000085 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1139 covered clauses in round 1
c [cce-1] eliminated 1139 covered clauses in TOTAL during 1 rounds
c [cce-1] 1139 < 1/100 * 130706 = 1307 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5835 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 40 variables 1% in round 1 in 15378815 steps
c [elim-2-1] backward subsumption/strengthening limit 4621185
c [elim-2-1-1] backward checking 796 touched variables 14%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 67 clauses in 2928443 steps
c [elim-2-1] rescheduled 77 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 221561 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 40 = 1% variables out of 5835 scheduled
c [elim-2] 40 < 1/100 * 5835 = 58 considered unsuccessful
c [bca-1] limit of 10000000 steps and 259058 added (scaled 2)
c [bca-1] 10859 out of 11592 literals actually usable 94%
c [bca-1] added 85 blocked clauses in 28170 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2061 pos 35.6% + 3734 neg 64.4% = 5795 sched 100.0% ret 0
c [sweep-1-1] 1003750 steps 52 queries 816.42 avg class size
c [sweep-1-1] 1394 decisions 43 SAT calls 64.40 avg env size
c [sweep-1-1] 5347 variables remain 92% (448 retained 8%)
c [decomp-6] removed 274 variables
c [sweep-1-1] removed 274 vars (0 failed, 8 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 274 vars in TOTAL (1 rounds, 51 queries)
c [phase-count-2] 116763 negative 90.6% of 128939 except 12176 9.4%
c [phase-count-2] 120369 positive 93.4% of 128939 except 8570 6.6%
c [phase-2] phase bias: 21 positive 38%, 34 negative 62%
c [sort-queue-2] sorted 5521 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 606 (11%), zero 4915 (89%)
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 345 variables 5.9% (5521 remain 60%)
c [simplification-2] removed 3047 irredundant clauses 2.3% (128939 remain 92%)
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 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3002 conflicts
c [quatres-1] found 25571 quaternary clauses 30% in total
c [quatres-1-2] added 3 single-self-subsuming ternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 5521 free variables schedulable
c [ternres-1] 54 ternary resolvents (0 bin, 54 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 859 at-most-one constraints of average size 3.1
c [card-2] found 89 at-most-two constraints of average size 4.7
c [card-2] using previous limit 1000000 for elimination
c [card-2] 948 out of 948 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 461 xors of average arity 2.9
c [gauss-1] connected 1358 occurrences of 596 variables (average 2.3)
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 9 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 10040 literals 91%
c [treelook-2] scheduling used 300002 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 301308 steps
c [treelook-2] 10001 literals remain 91%
c [treelook-2] 5429 variables remain to probed next time 98%
c [decomp-8] removed 4 variables
c [treelook-2] removed 4 variables, found 119 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 2 failed, 445 tauts, 0 hbrs, 729 literals
c [transred-1] limit 128404 based on 128404 irredundant clauses
c [transred-1] removed 334 transitive binary clauses
c [transred-1] found 1 units
c [bca-2] limit of 10000000 steps and 257158 added (scaled 2)
c [bca-2] 10185 out of 11014 literals actually usable 92%
c [bca-2] added 0 blocked clauses in 28671 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2002 pos 39.4% + 3079 neg 60.6% = 5081 sched 92.3% ret 425
c [sweep-2-1] 1092814 steps 56 queries 589.52 avg class size
c [sweep-2-1] 1560 decisions 54 SAT calls 51.83 avg env size
c [sweep-2-1] 4702 variables remain 85% (802 retained 15%)
c [decomp-9] removed 28 variables
c [sweep-2-1] removed 28 vars (0 failed, 1 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 28 vars in TOTAL (1 rounds, 55 queries)
c [phase-count-3] 116061 negative 90.5% of 128264 except 12203 9.5%
c [phase-count-3] 119640 positive 93.3% of 128264 except 8624 6.7%
c [phase-3] phase bias: 10 positive 42%, 14 negative 58%
c [sort-queue-3] sorted 5478 enqueued variables after 3002 conflicts
c [score-dist-3] active 0 (0%), one 747 (14%), zero 4731 (86%)
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 43 variables 0.8% (5478 remain 60%)
c [simplification-3] removed 675 irredundant clauses 0.5% (128264 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 23002 (soft 13002 + delta 10000)
c [simplification-3] new conflict limit 13002 (hard 23002)
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    3.0    5477   128264      3095    3295   1029  2290    5    11    9  47%     33   10   10    0 2293%
c 
c [simplification-4] limit 13002 conflicts (hard 23002) hit after 13003 conflicts
c [quatres-2] found 25787 quaternary clauses 30% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 7 single-self-subsuming ternary resolvents
c [quatres-2-2] added 16 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5476 free variables schedulable
c [ternres-2] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-2] 53 variables remain 1% (5423 retained 99%)
c [decomp-10] removed 11 variables
c [basicprobe-2] limit 2626573 penalty 0 = 0 + 0
c [basicprobe-2-0] 418 sched 8%, 8 failed, 0 lifted, 891 hbrs
c [decomp-11] removed 72 variables
c [basicprobe-2-1] 1091 sched 20%, 9 failed, 1 lifted, 415 hbrs
c [decomp-12] removed 12 variables
c [basicprobe-2-2] 642 probes remain 12% after last round
c [basicprobe-2-2] 19 units = 18 failed (95%) + 1 lifted (5%)
c [basicprobe-2-2] removed 85 variables, found 1336 hbrs
c [bate-1] eliminated 166 asymmetric tautologies during probing
c [unhide-4] limit 105062 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 473 tauts, 0 hbrs, 4102 literals
c [transred-2] limit 525314 with penalty 0 = 0 + 0
c [transred-2] removed 532 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5382 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 25 blocked clauses
c [block-2] 25 < 1/100 * 127575 = 1275 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 7 clauses out of 692 (1%) of length 12
c [cce-2-1] eliminated 13 clauses out of 103 (13%) of length 11
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 24 large clauses in 15000000 steps
c [cce-2-1] allowing another 7500000 steps for small clauses
c [cce-2-1] scheduling 40810 clauses = 10615 binary + 30195 ternary
c [cce-2-1] tried to eliminate 1970 small clauses 5%
c [cce-2-1] eliminated 22 binary clauses 0%
c [cce-2-1] eliminated 95 ternary clauses 0%
c [cce-2-1] eliminated 117 small clauses 0%
c [cce-2-1] eliminated 117 small clauses in 15000025 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 141 covered clauses in round 1
c [cce-2] eliminated 141 covered clauses in TOTAL during 1 rounds
c [cce-2] 141 < 1/100 * 127550 = 1275 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5382 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 792 not tried 15% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 46 = 1% variables out of 5382 scheduled
c [elim-3] 46 < 1/100 * 5382 = 53 considered unsuccessful
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2115 pos 46.0% + 2480 neg 54.0% = 4595 sched 86.1% ret 741
c [sweep-3-1] 1005590 steps 44 queries 623.05 avg class size
c [sweep-3-1] 1685 decisions 43 SAT calls 72.00 avg env size
c [sweep-3-1] 4153 variables remain 78% (1183 retained 22%)
c [decomp-13] removed 3 variables
c [sweep-3-1] removed 3 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3 vars in TOTAL (1 rounds, 43 queries)
c [phase-count-4] 114716 negative 90.2% of 127212 except 12496 9.8%
c [phase-count-4] 118338 positive 93.0% of 127212 except 8874 7.0%
c [phase-4] phase bias: 3 positive 27%, 8 negative 73%
c [sort-queue-4] sorted 5333 enqueued variables after 13003 conflicts
c [score-dist-4] active 0 (0%), one 1151 (22%), zero 4182 (78%)
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 143 variables 2.6% (5333 remain 58%)
c [simplification-4] removed 1052 irredundant clauses 0.8% (127212 remain 90%)
c [simplification-4] maximum reduction of 3% = max (3%, 1%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 15000
c [simplification-4] penalized conflict interval 15000 = 1 * 15000
c [simplification-4] hard conflict limit 38003 (soft 28003 + delta 10000)
c [simplification-4] new conflict limit 28003 (hard 38003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    6.3    5332   127212     20964   20156   1179  2374   10    19   11  55%    231   15   11    3  414%
c i    7.2    5331   127212     26849   25760   1221  2378   10    18   13  56%     41   13    9    3  281%
c 
c [simplification-5] limit 28003 conflicts (hard 38003) hit after 29870 conflicts
c [quatres-3] found 25957 quaternary clauses 30% in total
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [quatres-3-2] added 7 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 51 schedulable variables 1%
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 210 xors of average arity 3.0
c [gauss-2] connected 629 occurrences of 422 variables (average 1.5)
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 1 variables
c [simpleprobe-3] 3872 schedulable variables 73%
c [simpleprobe-3] limit 6234363 penalty 0 = 0 + 0
c [decomp-15] removed 6 variables
c [simpleprobe-3] 3271 variables remain 61% (2050 retained 39%)
c [simpleprobe-3] removed 6 variables, found 530 hbrs, 0 units
c [transred-3] limit 1558590 with penalty 0 = 0 + 0
c [transred-3] removed 490 transitive binary clauses
c [bca-3] limit of 10000000 steps and 254616 added (scaled 2)
c [bca-3] 9446 out of 10644 literals actually usable 89%
c [bca-3] added 7 blocked clauses in 53285 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2050 pos 49.5% + 2093 neg 50.5% = 4143 sched 77.9% ret 1178
c [sweep-4-1] 1001151 steps 115 queries 249.90 avg class size
c [sweep-4-1] 2573 decisions 112 SAT calls 55.53 avg env size
c [sweep-4-1] 3038 variables remain 57% (2277 retained 43%)
c [decomp-16] removed 22 variables
c [sweep-4-1] removed 22 vars (0 failed, 4 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 22 vars in TOTAL (1 rounds, 114 queries)
c [phase-count-5] 114356 negative 90.1% of 126955 except 12599 9.9%
c [phase-count-5] 118046 positive 93.0% of 126955 except 8909 7.0%
c [phase-5] phase bias: 1 positive 33%, 2 negative 67%
c [sort-queue-5] sorted 5299 enqueued variables after 29870 conflicts
c [score-dist-5] active 0 (0%), one 1461 (28%), zero 3838 (72%)
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 29 variables 0.5% (5299 remain 58%)
c [simplification-5] removed 257 irredundant clauses 0.2% (126955 remain 90%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 25000
c [simplification-5] penalized conflict interval 25000 = 1 * 25000
c [simplification-5] hard conflict limit 67370 (soft 54870 + delta 12500)
c [simplification-5] new conflict limit 54870 (hard 67370)
c 
c [simplification-6] limit 54870 conflicts (hard 67370) hit after 54872 conflicts
c [quatres-4] found 26205 quaternary clauses 29% in total
c [quatres-4-2] added 8 quaternary resolvents
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 554 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 554 out of 554 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 381101 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 9653 literals 91%
c [treelook-3] scheduling used 381313 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 381101 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 389454 steps
c [treelook-3] 9617 literals remain 91%
c [treelook-3] 5197 variables remain to probed next time 98%
c [treelook-3] removed 0 variables, found 101 hbrs
c [unhide-5] limit 381101 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 449 tauts, 0 hbrs, 20240 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 235 transitive binary clauses
c [bca-4] limit of 10000000 steps and 253630 added (scaled 2)
c [bca-4] 9055 out of 10600 literals actually usable 85%
c [bca-4] added 7 blocked clauses in 75846 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 11433040 penalty 0 = 0 + 0
c [sweep-5-1] 1641 pos 54.1% + 1393 neg 45.9% = 3034 sched 57.3% ret 2265
c [sweep-5-1] 11438223 steps 510 queries 54.28 avg class size
c [sweep-5-1] 11388 decisions 488 SAT calls 53.28 avg env size
c [sweep-5-1] 615 variables remain 12% (4683 retained 88%)
c [decomp-19] removed 48 variables
c [sweep-5-1] removed 48 vars (0 failed, 38 eqs, 18 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 48 vars in TOTAL (1 rounds, 509 queries)
c [phase-count-6] 113725 negative 89.9% of 126498 except 12773 10.1%
c [phase-count-6] 117475 positive 92.9% of 126498 except 9023 7.1%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-6] sorted 5251 enqueued variables after 54872 conflicts
c [score-dist-6] active 0 (0%), one 2001 (38%), zero 3250 (62%)
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 48 variables 0.9% (5251 remain 57%)
c [simplification-6] removed 457 irredundant clauses 0.4% (126498 remain 90%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 12500 = 25000 / 2
c [simplification-6] new conflict interval 37500
c [simplification-6] penalized conflict interval 37500 = 1 * 37500
c [simplification-6] hard conflict limit 111122 (soft 92372 + delta 18750)
c [simplification-6] new conflict limit 92372 (hard 111122)
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 -   15.7    5251   126498     57760   18061   1344  2586   11    19   12  59%    352    8   11    6  182%
c i   17.5    5250   126498     69792   29604   1401  2597   11    19   14  59%    464    7   12    7  165%
c 
c [simplification-7] limit 92372 conflicts (hard 111122) hit after 92372 conflicts
c [quatres-5] found 26592 quaternary clauses 29% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 6 single-self-subsuming ternary resolvents
c [quatres-5-2] added 35 quaternary resolvents
c [ternres-4] limit 3471392 with penalty 1 = 1 + 0
c [ternres-4] all 5250 free variables schedulable
c [ternres-4] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-4] 2063 variables remain 39% (3187 retained 61%)
c [decomp-20] removed 2 variables
c [basicprobe-3] limit 34713922 penalty 0 = 0 + 0
c [basicprobe-3-0] 630 sched 12%, 2 failed, 0 lifted, 146 hbrs
c [decomp-21] removed 4 variables
c [basicprobe-3-1] 1052 sched 20%, 3 failed, 0 lifted, 139 hbrs
c [decomp-22] removed 5 variables
c [basicprobe-3-2] 1057 sched 20%, 1 failed, 0 lifted, 88 hbrs
c [decomp-23] removed 1 variables
c [basicprobe-3-3] 1056 sched 20%, 1 failed, 0 lifted, 49 hbrs
c [decomp-24] removed 1 variables
c [basicprobe-3-4] 1056 sched 20%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-3-5] 1056 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-5] fully completed probing
c [basicprobe-3-5] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 11 variables, found 429 hbrs
c [bate-2] eliminated 350 asymmetric tautologies during probing
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 321 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5238 variables 100%
c [block-3] limit of 17356961 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 42 blocked clauses
c [block-3] 42 < 1/100 * 125929 = 1259 considered unsuccessful
c [cce-3] limit of 8678480 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 37 clauses out of 241 (15%) of length 13
c [cce-3-1] eliminated 40 clauses out of 677 (6%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 77 large clauses in 8678970 steps
c [cce-3-1] allowing another 4339485 steps for small clauses
c [cce-3-1] scheduling 13710 clauses = 10370 binary + 3340 ternary
c [cce-3-1] tried to eliminate 856 small clauses 6%
c [cce-3-1] eliminated 66 binary clauses 1%
c [cce-3-1] eliminated 115 ternary clauses 3%
c [cce-3-1] eliminated 181 small clauses 1%
c [cce-3-1] eliminated 181 small clauses in 8678605 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 258 covered clauses in round 1
c [cce-3] eliminated 258 covered clauses in TOTAL during 1 rounds
c [cce-3] 258 < 1/100 * 125887 = 1258 considered unsuccessful
c [elim-4] 772 variables 15% will be scheduled this time
c [elim-4] scheduled 772 variables 15%
c [elim-4] boosting limit by 20
c [elim-4] limit of 694278440 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 111247540 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 772 scheduled
c [bca-5] limit of 10000000 steps and 250359 added (scaled 2)
c [bca-5] 8571 out of 10476 literals actually usable 82%
c [bca-5] added 18 blocked clauses in 72347 steps
c [sweep-6] limit 2082835 penalty 0 = 0 + 0
c [sweep-6-1] 306 pos 50.7% + 297 neg 49.3% = 603 sched 11.5% ret 4634
c [sweep-6-1] 2443164 steps 104 queries 36.56 avg class size
c [sweep-6-1] 2551 decisions 101 SAT calls 54.98 avg env size
c [sweep-6-1] 404 variables remain 8% (4833 retained 92%)
c [decomp-26] removed 4 variables
c [sweep-6-1] removed 4 vars (0 failed, 6 eqs, 0 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 4 vars in TOTAL (1 rounds, 103 queries)
c [phase-count-7] 112189 negative 89.8% of 124904 except 12715 10.2%
c [phase-count-7] 115940 positive 92.8% of 124904 except 8964 7.2%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 5233 enqueued variables after 92372 conflicts
c [score-dist-7] active 0 (0%), one 2226 (43%), zero 3007 (57%)
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 17 variables 0.3% (5233 remain 57%)
c [simplification-7] removed 1594 irredundant clauses 1.3% (124904 remain 89%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 18750 = 37500 / 2
c [simplification-7] new conflict interval 56250
c [simplification-7] penalized conflict interval 56250 = 1 * 56250
c [simplification-7] hard conflict limit 176747 (soft 148622 + delta 28125)
c [simplification-7] new conflict limit 148622 (hard 176747)
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 -   27.4    5233   124904    101401   24275   1630  2720   11    19   12  61%    258    4   12    9  134%
c i   34.0    5232   124904    136964   58179   1726  2730   11    19   18  59%    579    2   11   10  118%
c -   35.5    5232   124904    142746   29962   1733  2731   11    18   21  62%   -356    2   11   10  109%
c 
c [simplification-8] limit 148622 conflicts (hard 176747) hit after 174534 conflicts
c [quatres-6] found 26899 quaternary clauses 28% in total
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 10 single-self-subsuming ternary resolvents
c [quatres-6-2] added 32 quaternary resolvents
c [ternres-5] limit 14003433 with penalty 0 = 0 + 0
c [ternres-5] 2056 schedulable variables 39%
c [ternres-5] 42 ternary resolvents (0 bin, 42 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-3] limit 700171 penalty 2 = 2 + 0
c [gauss-3] extracted 127 xors of average arity 3.0
c [gauss-3] connected 379 occurrences of 228 variables (average 1.7)
c [gauss-3] limit 700171 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-27] removed 3 variables
c [simpleprobe-4] 3221 schedulable variables 62%
c [simpleprobe-4] limit 56013734 penalty 0 = 0 + 0
c [decomp-28] removed 66 variables
c [simpleprobe-4] 2141 variables remain 41% (3022 retained 59%)
c [simpleprobe-4] removed 66 variables, found 2164 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1155 transitive binary clauses
c [bca-6] limit of 10000000 steps and 250054 added (scaled 2)
c [bca-6] 7976 out of 10328 literals actually usable 77%
c [bca-6] added 0 blocked clauses in 77439 steps
c [sweep-7] limit 4201030 penalty 0 = 0 + 0
c [sweep-7-1] 180 pos 44.8% + 222 neg 55.2% = 402 sched 7.8% ret 4761
c [sweep-7-1] 3189127 steps 253 queries 13.36 avg class size
c [sweep-7-1] 6362 decisions 239 SAT calls 61.21 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-29] removed 2 variables
c [sweep-7-1] removed 2 vars (0 failed, 14 eqs, 0 impls)
c [sweep-7-2] 2890 pos 56.0% + 2271 neg 44.0% = 5161 sched 100.0% ret 0
c [sweep-7-2] 1084638 steps 6 queries 1570.83 avg class size
c [sweep-7-2] 337 decisions 5 SAT calls 129.40 avg env size
c [sweep-7-2] 5147 variables remain 100% (14 retained 0%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] 2 < 1/1000 * 5163 = 5 considered unsuccessful
c [sweep-7] removed 2 vars in TOTAL (2 rounds, 257 queries)
c [phase-count-8] 111446 negative 89.3% of 124748 except 13302 10.7%
c [phase-count-8] 115273 positive 92.4% of 124748 except 9475 7.6%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-8] sorted 5161 enqueued variables after 174534 conflicts
c [score-dist-8] active 0 (0%), one 2486 (48%), zero 2675 (52%)
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 71 variables 1.4% (5161 remain 56%)
c [simplification-8] removed 156 irredundant clauses 0.1% (124748 remain 89%)
c [simplification-8] maximum reduction of 1% = max (1%, 0%)
c [simplification-8] geometric conflict interval increment 28125 = 56250 / 2
c [simplification-8] new conflict interval 84375
c [simplification-8] penalized conflict interval 84375 = 1 * 84375
c [simplification-8] hard conflict limit 301096 (soft 258909 + delta 42187)
c [simplification-8] new conflict limit 258909 (hard 301096)
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   41.7    5160   124748    177933   62385   1889  3683   10    21   19  49%    215    5    7   10   67%
c -   42.8    5157   124748    182889   35541   1902  3683   11    19   13  60%   -324    3   11   10  113%
c -   48.9    5157   124748    220644   39289   1983  3687   10    15   13  69%    264   -1   11   10  105%
c -   54.8    5157   124748    258241   42610   2045  3692   10    19   14  54%    596    3   10   10   99%
c 
c [simplification-9] limit 258909 conflicts (hard 301096) hit after 258910 conflicts
c [quatres-7] found 27495 quaternary clauses 27% in total
c [quatres-7-2] added 16 single-self-subsuming ternary resolvents
c [quatres-7-2] added 17 quaternary resolvents
c [ternres-6] limit 21434243 with penalty 0 = 0 + 0
c [ternres-6] all 5157 free variables schedulable
c [ternres-6] 35 ternary resolvents (0 bin, 35 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-31] removed 4 variables
c [unhide-6] limit 1071712 with penalty 2 = 2 + 0
c [unhide-6-6] 0 units, 0 failed, 1390 tauts, 0 hbrs, 6946 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 342 transitive binary clauses
c [phase-count-9] 111391 negative 89.3% of 124688 except 13297 10.7%
c [phase-count-9] 115224 positive 92.4% of 124688 except 9464 7.6%
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-9] sorted 5157 enqueued variables after 258910 conflicts
c [score-dist-9] active 0 (0%), one 2519 (49%), zero 2638 (51%)
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 0 variables 0.0% (5157 remain 56%)
c [simplification-9] removed 60 irredundant clauses 0.0% (124688 remain 89%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 84375
c [simplification-9] new conflict interval 168750
c [simplification-9] penalized conflict interval 168750 = 1 * 168750
c [simplification-9] hard conflict limit 512035 (soft 427660 + delta 84375)
c [simplification-9] new conflict limit 427660 (hard 512035)
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 -   61.2    5157   124688    295446   44700   2016  2759    9    12   13  73%    781   -3    8   10   81%
c -   67.3    5157   124688    332422   46868   2049  2761    9    12   21  75%    886   -2    8   10   81%
c i   68.1    5156   124688    336952   51118   2053  2763   10    15   23  69%    895    1   11   10  115%
c i   68.1    5155   124688    336966   51130   2053  2763   10    15   23  69%    861    1   11   10  111%
c i   70.8    5154   124688    351620   64481   2102  2772   10    16   24  63%  -1097    1    8   10   80%
c -   75.0    5151   124688    371050   47418   2121  2775   11    17   21  66%   -726    3   12   10  122%
c -   83.0    5151   124688    413098   50848   2182  2778   11    15   21  71%    103    1    9   10   88%
c 
c [simplification-10] limit 427660 conflicts (hard 512035) hit after 427661 conflicts
c [quatres-8] found 27927 quaternary clauses 26% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 42 single-self-subsuming ternary resolvents
c [quatres-8-2] added 25 quaternary resolvents
c [ternres-7] limit 37915523 with penalty 0 = 0 + 0
c [ternres-7] all 5151 free variables schedulable
c [ternres-7] 58 ternary resolvents (0 bin, 58 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 2369720 penalty 3 = 3 + 0
c [card-4] found 622 at-most-one constraints of average size 3.1
c [card-4] found 106 at-most-two constraints of average size 4.6
c [card-4] using previous limit 2369720 for elimination
c [card-4] 728 out of 728 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-32] removed 6 variables
c [treelook-4] limit 1895776 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 10222 literals 99%
c [treelook-4] scheduling used 451191 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1895776 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 1896413 steps
c [treelook-4] 9964 literals remain 97%
c [treelook-4] 5049 variables remain to probed next time 98%
c [decomp-33] removed 1 variables
c [treelook-4] removed 2 variables, found 482 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 311 transitive binary clauses
c [bca-7] limit of 10000000 steps and 249634 added (scaled 2)
c [bca-7] 7811 out of 10300 literals actually usable 76%
c [bca-7] added 0 blocked clauses in 81310 steps
c [sweep-8] limit 5687328 penalty 1 = 1 + 0
c [sweep-8-1] 2859 pos 55.7% + 2276 neg 44.3% = 5135 sched 99.7% ret 14
c [sweep-8-1] 5803262 steps 36 queries 557.22 avg class size
c [sweep-8-1] 1580 decisions 35 SAT calls 96.03 avg env size
c [sweep-8-1] 4735 variables remain 92% (413 retained 8%)
c [decomp-34] removed 4 variables
c [sweep-8-1] removed 4 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] 4 < 1/1000 * 5149 = 5 considered unsuccessful
c [sweep-8] removed 4 vars in TOTAL (1 rounds, 35 queries)
c [phase-count-10] 111228 negative 89.3% of 124527 except 13299 10.7%
c [phase-count-10] 115053 positive 92.4% of 124527 except 9474 7.6%
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-10] sorted 5145 enqueued variables after 427661 conflicts
c [score-dist-10] active 0 (0%), one 2571 (50%), zero 2574 (50%)
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 6 variables 0.1% (5145 remain 56%)
c [simplification-10] removed 161 irredundant clauses 0.1% (124527 remain 88%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 168750
c [simplification-10] new conflict interval 337500
c [simplification-10] penalized conflict interval 337500 = 1 * 337500
c [simplification-10] hard conflict limit 933911 (soft 765161 + delta 168750)
c [simplification-10] new conflict limit 765161 (hard 933911)
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   87.4    5144   124527    435584   70854   2197  2921    8    11   19  74%    370   -4    7   10   73%
c -   90.7    5142   124527    453891   53772   2220  2923   10    13   14  75%   -478   -2   10   10   98%
c i   90.9    5141   124527    455507   55114   2238  2930    9    12   17  76%   -442   -3    6   10   60%
c -   98.1    5141   124527    494646   56176   2291  2938   10    14   15  71%     43   -0    7   10   74%
c i  100.8    5140   124527    512332   71398   2333  2948    8    10   18  78%    275   -4    6   10   61%
c -  105.4    5137   124527    537193   59064   2367  2953   10    14   24  70%   -106    0   11   10  115%
c i  112.1    5136   124527    572416   90366   2416  2960   10    13   30  75%    364   -1    7   10   74%
c -  113.7    5130   124527    579156   60250   2421  2961   11    16   24  65%   -431    3   12   10  117%
c i  116.6    5129   124527    596827   75613   2455  2970    9    11   27  79%    -88   -3    6   10   59%
c i  117.3    5128   124527    600782   78982   2467  2974    9    11   27  79%   -379   -3    6   10   63%
c -  122.0    5127   124527    624457   64174   2493  2977    9    11   24  80%     -3   -2    9   10   95%
c i  127.5    5126   124527    654462   90502   2543  2988    8    10   29  80%    374   -4    6   10   59%
c i  129.9    5120   124527    666280  100602   2570  2990    9    12   31  70%   -230   -1    8    9   81%
c i  130.3    5116   124527    668024  102000   2586  2995    8    11   31  75%   -346   -3    6    9   65%
c -  130.5    5104   124527    669429   67108   2594  2997    9    23   24  37%   -362   10   11    9  116%
c i  130.8    5103   124527    671822   69212   2602  3002    8    18   27  48%   -325    4    7    9   70%
c i  130.9    5094   124527    672116   69403   2616  3007    8    17   27  49%   -335    3    6    9   64%
c i  130.9    5070   124527    672121   69402   2618  3009    8    17   27  49%   -335    3    6    9   63%
c i  130.9    5052   124527    672123   69403   2618  3009    8    17   27  49%   -335    3    6    9   63%
c i  130.9    5037   124527    672297   69571   2618  3009    9    19   27  46%   -339    5   11    9  116%
c i  130.9    5036   124527    672298   69571   2618  3009    9    19   27  46%   -339    5   11    9  116%
c i  130.9    5034   124527    672300   69571   2618  3010    9    19   27  46%   -339    5   11    9  115%
c i  130.9    5024   124527    672301   69571   2618  3010    9    19   27  46%   -339    5   11    9  114%
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  130.9    4999   124527    672303   69571   2618  3011    9    19   27  46%   -339    5   11    9  114%
c i  130.9    4987   124527    672347   69586   2621  3017    9    18   27  46%   -340    5   10    9  102%
c i  131.0    4956   124527    673012   70194   2632  3020    9    22   27  40%   -347    8   10    9  103%
c i  131.3    4953   124527    676481   73419   2661  3030   10    35   27  28%   -307   20   11    9  117%
c i  131.3    4945   124527    676489   73422   2662  3033   10    34   27  28%   -307   20   11    9  114%
c i  131.6    4910   124527    679540   76322   2680  3034   10    36   28  28%   -297   20   12    9  126%
c i  131.6    4909   124527    679818   76580   2684  3035   10    36   28  27%   -304   20    9    9   92%
c i  131.7    4906   124527    680827   77521   2693  3036   10    39   28  24%   -310   23    8    9   83%
c i  131.7    4905   124527    681039   77708   2698  3037   10    40   28  24%   -312   23   10    9  102%
c i  132.4    4883   124527    688533   84779   2759  3053    9    32   28  29%   -194   14   10    9  109%
c i  132.4    4881   124527    688534   84779   2759  3053    9    32   28  29%   -194   14   10    9  108%
c i  134.4    4876   124527    704605  100011   2848  3079    9    29   32  32%    -22    8    7    9   79%
c i  135.3    4861   124527    710450  105613   2873  3089   10    30   32  33%   -165    9   11    9  115%
c i  135.4    4858   124527    710945  106071   2878  3089    9    29   32  33%   -191    8    8    9   84%
c -  136.1    4842   124527    715614   73076   2885  3092    9    22   25  39%   -168    1    8    9   86%
c 
c [simplification-11] limit of 265 binary hit after 339 binaries
c [quatres-9] found 22741 quaternary clauses 29% in total
c [quatres-9-2] added 4 single-self-subsuming ternary resolvents
c [quatres-9-2] added 12 quaternary resolvents
c [ternres-8] limit 68666529 with penalty 0 = 0 + 0
c [ternres-8] all 4842 free variables schedulable
c [ternres-8] 18 ternary resolvents (0 bin, 18 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-35] removed 351 variables
c [basicprobe-4] limit 343332648 penalty 0 = 0 + 0
c [basicprobe-4-0] 891 sched 19%, 25 failed, 0 lifted, 623 hbrs
c [decomp-36] removed 35 variables
c [basicprobe-4-1] 905 sched 19%, 21 failed, 2 lifted, 190 hbrs
c [decomp-37] removed 23 variables
c [basicprobe-4-2] 916 sched 19%, 9 failed, 0 lifted, 102 hbrs
c [decomp-38] removed 10 variables
c [basicprobe-4-3] 918 sched 19%, 4 failed, 0 lifted, 77 hbrs
c [decomp-39] removed 4 variables
c [basicprobe-4-4] 915 sched 19%, 2 failed, 0 lifted, 27 hbrs
c [decomp-40] removed 2 variables
c [basicprobe-4-5] 914 sched 19%, 2 failed, 0 lifted, 5 hbrs
c [decomp-41] removed 2 variables
c [basicprobe-4-6] 916 sched 19%, 2 failed, 0 lifted, 33 hbrs
c [decomp-42] removed 2 variables
c [basicprobe-4-7] 915 sched 19%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-8] 915 sched 19%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 67 units = 65 failed (97%) + 2 lifted (3%)
c [basicprobe-4-8] removed 78 variables, found 1063 hbrs
c [bate-3] eliminated 221 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 301 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4716 variables 100%
c [block-4] limit of 85833162 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 875 blocked clauses
c [block-4] 875 < 1/100 * 111278 = 1112 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 429165810 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 5 clauses out of 93 (5%) of length 11
c [cce-4-1] eliminated 4 clauses out of 210 (2%) of length 10
c [cce-4-1] eliminated 7 clauses out of 900 (1%) of length 9
c [cce-4-1] eliminated 130 clauses out of 2464 (5%) of length 8
c [cce-4-1] eliminated 251 clauses out of 6950 (4%) of length 7
c [cce-4-1] eliminated 366 clauses out of 15265 (2%) of length 6
c [cce-4-1] eliminated 405 clauses out of 23624 (2%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 1168 large clauses in 429165819 steps
c [cce-4-1] allowing another 214582909 steps for small clauses
c [cce-4-1] scheduling 12069 clauses = 9223 binary + 2846 ternary
c [cce-4-1] tried to eliminate 12069 small clauses 100%
c [cce-4-1] eliminated 350 binary clauses 4%
c [cce-4-1] eliminated 177 ternary clauses 6%
c [cce-4-1] eliminated 527 small clauses 4%
c [cce-4-1] eliminated 527 small clauses in 266361825 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 1695 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 81402002 steps for small clauses
c [cce-4-2] scheduling 11543 clauses = 8873 binary + 2670 ternary
c [cce-4-2] tried to eliminate 11543 small clauses 100%
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 131348913 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 1 covered clauses in round 2
c [cce-4-3] incomplete large round (ATE)
c [cce-4-3] allowing another 15727536 steps for small clauses
c [cce-4-3] scheduling 11542 clauses = 8873 binary + 2669 ternary
c [cce-4-3] tried to eliminate 3662 small clauses 32%
c [cce-4-3] incomplete small round (ATE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 1696 covered clauses in TOTAL during 3 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 4670 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 147 not tried 3% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 94 = 2% variables out of 4670 scheduled
c [phase-count-11] 96578 negative 89.4% of 108072 except 11494 10.6%
c [phase-count-11] 99076 positive 91.7% of 108072 except 8996 8.3%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 4576 enqueued variables after 725620 conflicts
c [score-dist-11] active 0 (0%), one 2324 (51%), zero 2252 (49%)
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 266 variables 5.5% (4576 remain 50%)
c [simplification-11] removed 16455 irredundant clauses 13.2% (108072 remain 77%)
c [simplification-11] maximum reduction of 13% = max (5%, 13%)
c [simplification-11] forced so keeping old conflict interval 337500
c [simplification-11] conflict limit remains at 765209 (hard 933911)
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  146.5    4575   108072    737669   34162   1656  2821    9    22   12  43%    172   -1   10    9  108%
c i  146.5    4574   108072    737700   34176   1658  2824    9    22   12  43%    160   -1    9    9   99%
c 
c [simplification-12] limit 765209 conflicts (hard 933911) hit after 767062 conflicts
c [quatres-10] found 22242 quaternary clauses 27% in total
c [quatres-10-1] removed 18 duplicate quaternary clauses
c [quatres-10-2] added 3 single-self-subsuming ternary resolvents
c [quatres-10-2] added 15 quaternary resolvents
c [ternres-9] limit 71285202 with penalty 0 = 0 + 0
c [ternres-9] all 4569 free variables schedulable
c [ternres-9] 98 ternary resolvents (1 bin, 97 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 1782130 penalty 3 = 3 + 0
c [gauss-4] extracted 372 xors of average arity 2.9
c [gauss-4] connected 1097 occurrences of 461 variables (average 2.4)
c [gauss-4] limit 1782130 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-44] removed 10 variables
c [simpleprobe-5] 1880 schedulable variables 41%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-45] removed 24 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 24 variables, found 2568 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1309 transitive binary clauses
c [phase-count-12] 96327 negative 89.3% of 107922 except 11595 10.7%
c [phase-count-12] 98820 positive 91.6% of 107922 except 9102 8.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 4535 enqueued variables after 767062 conflicts
c [score-dist-12] active 0 (0%), one 2308 (51%), zero 2227 (49%)
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 34 variables 0.7% (4535 remain 49%)
c [simplification-12] removed 150 irredundant clauses 0.1% (107922 remain 77%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 168750 = 337500 / 2
c [simplification-12] new conflict interval 506250
c [simplification-12] penalized conflict interval 506250 = 1 * 506250
c [simplification-12] hard conflict limit 1526437 (soft 1273312 + delta 253125)
c [simplification-12] new conflict limit 1273312 (hard 1526437)
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 -  156.5    4535   107922    787494   42460   1760  4021   10    20   21  47%    427   -1    9   10   97%
c -  165.5    4535   107922    832885   47759   1816  4037   10    20   22  50%    725    1   10   10  106%
c -  175.8    4535   107922    876581   49363   1845  4053   10    18   21  56%    871   -2    8   10   85%
c i  182.1    4534   107922    907337   77590   1861  4059   10    18   26  57%    928   -1   11   10  110%
c -  186.8    4534   107922    923789   52625   1878  4063   10    20   22  52%  -1145    2   11   10  115%
c i  193.1    4533   107922    951503   78759   1906  4067   11    18   26  58%   -397    0   12   10  126%
c i  193.7    4532   107922    953201   80361   1909  4068   11    19   26  57%   -911    1   12   10  119%
c i  193.8    4531   107922    953427   80563   1915  4071   11    19   26  56%   -935    1   11   10  112%
c -  197.1    4531   107922    968451   54306   1920  4073   11    25   22  42%   -639    5   10   10   96%
c -  208.5    4531   107922   1015218   56993   1941  4080   10    20   22  51%    209    1   12   10  117%
c i  211.2    4530   107922   1026786   67945   1958  4085   11    24   26  45%    341    4   11   10  111%
c -  220.9    4530   107922   1062023   57728   1984  4090   11    19   22  58%    -55   -0   11   10  111%
c -  233.1    4530   107922   1112216   61622   2001  4098   11    16   22  67%    522   -2   11   10  107%
c -  245.8    4530   107922   1161030   64287   2015  4101   11    19   22  59%    786    2   13   10  124%
c -  259.4    4530   107922   1210226   66011   2046  4109   11    21   22  54%    912    3   11   10  109%
c -  271.2    4530   107922   1259407   69933   2052  4110    9    12   22  71%    971   -4    7   10   72%
c 
c [simplification-13] limit 1273312 conflicts (hard 1526437) hit after 1279117 conflicts
c [quatres-11] found 23156 quaternary clauses 22% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 11 single-self-subsuming ternary resolvents
c [quatres-11-2] added 60 quaternary resolvents
c [ternres-10] limit 124892456 with penalty 0 = 0 + 0
c [ternres-10] all 4530 free variables schedulable
c [ternres-10] 95 ternary resolvents (0 bin, 95 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-46] removed 12 variables
c [treelook-5] limit 12489245 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 8974 literals 99%
c [treelook-5] scheduling used 466240 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 12489245 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 12493181 steps
c [treelook-5] 5423 literals remain 60%
c [treelook-5] 3817 variables remain to probed next time 84%
c [decomp-47] removed 10 variables
c [treelook-5] removed 13 variables, found 1987 hbrs
c [unhide-7] limit 2500000 with penalty 3 = 3 + 0
c [unhide-7-8] 0 units, 0 failed, 3166 tauts, 0 hbrs, 26226 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 587 transitive binary clauses
c [cce-5] limit of 156115570 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 263 (28%) of length 13
c [cce-5-1] eliminated 21 clauses out of 589 (4%) of length 12
c [cce-5-1] eliminated 15 clauses out of 90 (17%) of length 11
c [cce-5-1] eliminated 50 clauses out of 206 (24%) of length 10
c [cce-5-1] eliminated 163 clauses out of 886 (18%) of length 9
c [cce-5-1] eliminated 47 clauses out of 2292 (2%) of length 8
c [cce-5-1] eliminated 942 clauses out of 6722 (14%) of length 7
c [cce-5-1] eliminated 831 clauses out of 14864 (6%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 2227 large clauses in 156115592 steps
c [cce-5-1] allowing another 78057796 steps for small clauses
c [cce-5-1] scheduling 11242 clauses = 8612 binary + 2630 ternary
c [cce-5-1] tried to eliminate 11242 small clauses 100%
c [cce-5-1] eliminated 610 binary clauses 7%
c [cce-5-1] eliminated 842 ternary clauses 32%
c [cce-5-1] eliminated 1452 small clauses 13%
c [cce-5-1] eliminated 1452 small clauses in 125248996 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 3679 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 15433295 steps for small clauses
c [cce-5-2] scheduling 9790 clauses = 8002 binary + 1788 ternary
c [cce-5-2] tried to eliminate 4092 small clauses 42%
c [cce-5-2] eliminated 1 binary clauses 0%
c [cce-5-2] eliminated 1 small clauses 0%
c [cce-5-2] eliminated 1 small clauses in 30866684 steps
c [cce-5-2] incomplete small round (ACCE)
c [cce-5-2] eliminated 1 covered clauses in round 2
c [cce-5] eliminated 3680 covered clauses in TOTAL during 2 rounds
c [elim-6] 147 variables 3% will be scheduled this time
c [elim-6] scheduled 147 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 154707757 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 147 scheduled
c [bca-8] limit of 10000000 steps and 208720 added (scaled 2)
c [bca-8] 6191 out of 9022 literals actually usable 69%
c [bca-8] added 1 blocked clauses in 99689 steps
c [sweep-9] limit 9366934 penalty 2 = 2 + 0
c [sweep-9-1] 2489 pos 57.8% + 1820 neg 42.2% = 4309 sched 95.5% ret 201
c [sweep-9-1] 9379804 steps 121 queries 110.38 avg class size
c [sweep-9-1] 4428 decisions 124 SAT calls 80.66 avg env size
c [sweep-9-1] 2296 variables remain 51% (2214 retained 49%)
c [decomp-48] removed 14 variables
c [sweep-9-1] removed 14 vars (0 failed, 6 eqs, 0 impls)
c [sweep-9] removed 14 vars in TOTAL (1 rounds, 120 queries)
c [sort-queue-13] sorted 4496 enqueued variables after 1279117 conflicts
c [score-dist-13] active 0 (0%), one 2352 (52%), zero 2144 (48%)
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 34 variables 0.8% (4496 remain 49%)
c [simplification-13] removed 3841 irredundant clauses 3.6% (104081 remain 74%)
c [simplification-13] maximum reduction of 4% = max (1%, 4%)
c [simplification-13] geometric conflict interval increment 101250 = 506250 / 5
c [simplification-13] new conflict interval 607500
c [simplification-13] penalized conflict interval 607500 = 1 * 607500
c [simplification-13] hard conflict limit 2190367 (soft 1886617 + delta 303750)
c [simplification-13] new conflict limit 1886617 (hard 2190367)
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 -  292.8    4496   104081   1308627   68081   2843  4262   10    15   24  66%    999   -2   10   10   93%
c -  307.5    4496   104081   1361504   71684   2865  4272   11    16   24  66%   1013   -1   10   10   92%
c -  321.8    4496   104081   1414544   74501   2882  4282   10    15   25  70%   1019   -2   10   10   92%
c -  338.1    4496   104081   1467954   77994   2893  4288   11    17   25  64%   1022    1   11   10  104%
c -  354.7    4496   104081   1519714   77584   2898  4291   11    15   25  68%   1023   -1    9   10   86%
c -  371.7    4496   104081   1574370   80799   2911  4294   10    14   25  70%   1024   -2    9   11   82%
c -  389.9    4496   104081   1629601   83731   2919  4298   11    17   25  68%   1024   -0   13   10  129%
c -  407.4    4496   104081   1683303   83116   2927  4304   10    13   25  78%   1024   -4    8   11   77%
c i  417.1    4495   104081   1716558  113319   2931  4307   12    19   32  65%   1024    2   13   11  121%
c -  425.9    4495   104081   1739758   86882   2933  4307    9    13   25  72%  -6661   -3   11   11  101%
c -  445.2    4495   104081   1795700   88842   2946  4315   12    20   25  60%  -2249    4   14   11  133%
c -  465.3    4495   104081   1853192   89553   2967  4318   11    16   25  70%   -337   -0   11   11   99%
c 
c [simplification-14] limit 1886617 conflicts (hard 2190367) hit after 1911527 conflicts
c [quatres-12] found 23854 quaternary clauses 20% in total
c [quatres-12-1] removed 8 duplicate quaternary clauses
c [quatres-12-2] added 9 single-self-subsuming ternary resolvents
c [quatres-12-2] added 43 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 4495 free variables schedulable
c [ternres-11] 81 ternary resolvents (0 bin, 81 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-49] removed 1 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 796 sched 18%, 2 failed, 0 lifted, 80 hbrs
c [decomp-50] removed 2 variables
c [basicprobe-5-1] 796 sched 18%, 1 failed, 0 lifted, 2 hbrs
c [decomp-51] removed 3 variables
c [basicprobe-5-2] 795 sched 18%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-5-3] 795 sched 18%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-3] fully completed probing
c [basicprobe-5-3] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-5-3] removed 5 variables, found 84 hbrs
c [bate-4] eliminated 29 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 274 transitive binary clauses
c [cce-6] limit of 529268837 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 2237 (0%) of length 8
c [cce-6-1] eliminated 3 clauses out of 5787 (0%) of length 7
c [cce-6-1] eliminated 29 clauses out of 14026 (0%) of length 6
c [cce-6-1] eliminated 52 clauses out of 23608 (0%) of length 5
c [cce-6-1] eliminated 737 clauses out of 20948 (4%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 823 large clauses in 522643980 steps
c [cce-6-1] allowing another 261321990 steps for small clauses
c [cce-6-1] scheduling 33875 clauses = 7989 binary + 25886 ternary
c [cce-6-1] tried to eliminate 33875 small clauses 100%
c [cce-6-1] eliminated 4 binary clauses 0%
c [cce-6-1] eliminated 1159 ternary clauses 4%
c [cce-6-1] eliminated 1163 small clauses 3%
c [cce-6-1] eliminated 1163 small clauses in 361860949 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] completed small and large (ATE)
c [cce-6-1] eliminated 1986 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 83704214 steps for small clauses
c [cce-6-2] scheduling 32713 clauses = 7985 binary + 24728 ternary
c [cce-6-2] tried to eliminate 28073 small clauses 86%
c [cce-6-2] eliminated 1 ternary clauses 0%
c [cce-6-2] eliminated 1 small clauses 0%
c [cce-6-2] eliminated 1 small clauses in 167408268 steps
c [cce-6-2] incomplete small round (ATE)
c [cce-6-2] eliminated 1 covered clauses in round 2
c [cce-6] eliminated 1987 covered clauses in TOTAL during 2 rounds
c [sort-queue-14] sorted 4490 enqueued variables after 1911527 conflicts
c [score-dist-14] active 0 (0%), one 2354 (52%), zero 2136 (48%)
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 5 variables 0.1% (4490 remain 49%)
c [simplification-14] removed 2062 irredundant clauses 2.0% (102019 remain 72%)
c [simplification-14] maximum reduction of 2% = max (0%, 2%)
c [simplification-14] geometric conflict interval increment 202500 = 607500 / 3
c [simplification-14] new conflict interval 810000
c [simplification-14] penalized conflict interval 810000 = 1 * 810000
c [simplification-14] hard conflict limit 3126527 (soft 2721527 + delta 405000)
c [simplification-14] new conflict limit 2721527 (hard 3126527)
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 -  491.8    4490   102019   1912406   93148   4155  4122   12    17   19  70%    473    1   14   10  133%
c -  512.9    4490   102019   1970191   92133   4174  4123   11    16   31  68%    796    0   12   11  111%
c -  532.7    4490   102019   2031947   96217   4181  4128   10    14   31  72%    935   -1   12   11  112%
c -  553.1    4490   102019   2092347   97719   4186  4129   10    14   31  73%    989   -2   11   11  104%
c -  575.3    4490   102019   2155896   99338   4218  4131   12    17   31  69%   1011    2   12   11  110%
c -  596.8    4490   102019   2220075  102419   4242  4135   10    14   32  72%   1019    0   12   10  114%
c i  606.1    4489   102019   2248153  126993   4258  4144   10    13   39  76%   1021   -2    7   11   63%
c -  617.7    4476   102019   2281958  102753   4262  4145   10    14   32  76%  -4015   -1   14   11  129%
c i  634.7    4475   102019   2333362  147392   4294  4154    9    12   42  79%  -1276   -2    7   10   63%
c i  635.9    4472   102019   2336550  149697   4328  4163    8    10   44  79%  -2395   -4    6   10   56%
c i  637.5    4456   102019   2341329  153636   4347  4166    8    11   44  79%  -2256   -3    8   10   74%
c i  637.7    4443   102019   2342047  154250   4356  4170    8    10   44  79%  -2259   -3    6   10   59%
c i  638.1    4442   102019   2343148  155111   4367  4176    8    10   44  79%  -2236   -4    6   10   60%
c i  638.4    4435   102019   2344155  155933   4374  4184    8    10   44  77%  -2207   -3    6   10   64%
c i  638.4    4432   102019   2344191  155947   4376  4188    8    10   44  77%  -2206   -3    6   10   59%
c 0  638.4    4290   102019   2344191  155947   4376  4188    8    10   44  77%  -2206   -3    6   10   59%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 766 basic ate = 211 trn 28% + 555 lrg 72% in 4 updates
c bcas: 8 count, 118 added (242 skipped), 516757 steps
c bkwd: tried 36659 clauses, 72948 lits, 1.99 lits/clause
c bkwd: checked 5600714 occs, 152.78 occs/clause, 76.78 occs/lit
c bkwd: subsumed 0 binary, 4 ternary, 162 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 271 large (0% self)
c blkd: 4 bces, 2148 removed, 2346805 resolutions, 7560349 steps
c blkd: 2097 blocking literals 11%, 47 pure
c bump: 2342657 bumped seen, 115922796 lits 49.5 on average
c card: 4 count, 0 units, 0 am1, 10684778 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 9371 subsumed
c card: 3842 at-most-one constraints found, average size 3.09
c card: 3842 at-most-one constraints used 100%, average size 3.09
c card: 265 at-most-two constraints found, average size 4.70
c card: 265 at-most-two constraints used 100%, average size 4.70
c cces: 6 cces, 8901 eliminated, 5240 ate 59%, 3661 abce 41%
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: 780048 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 90 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 52 decompositions, 1503 equivalent 16%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 3895776 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 2517 eliminated 26%, 430 pure 17%
c elms: 9 rounds, 1.5 rounds/bve
c elms: 1591 small 63%, 449 large 18%
c elms: 2784 tried small, 1591 succeeded 57%, 1193 failed 43%
c elms: 1842 subsumed, 644 strengthened, 324 blocked
c elms: 1374675 copies, 1901248 resolutions, 84894 ipos
c elms: 3853059 subchks, 616358 strchks
c gaus: 4 extractions, 1170 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10965590 steps, 5482795 extr 50%, 73796 elim 1%
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: 16556 = 7802 simple 47% + 7324 trn 44% + 1430 lrg 9%, 472 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2342657 clauses, 21.5 length
c lrnd: 50339338 lits = 73054062 orig - 22714724 removed 31%
c lrnd: 583091 uips 25%, 1596699 flips 68%
c mins: 2324102 mins 99%, 260 bin 0%, 18295 size 1%
c mins: 53036856 poisoned searches, 9602515 hits, 18% hit rate
c mins: 114035612 used twice searches, 12674091 hits, 11% hit rate
c move: moved 5382, 1583 bin 29%, 3799 trn 71%
c otfs: 5560 driving 27%, 15011 restarting 73%
c otfs: str 20571, 20368 red 99%, 203 irr 1%
c otfs: str 20571, 0 bin 0%, 130 trn 1%, 20441 lrg 99%
c otfs: sub 77, 77 red 100%, 0 irr 0%
c otfs: sub 77, 0 bin 0%, 2 trn 3%, 75 lrg 97%
c phas: 12 computed, 5959 set, 3373 pos (57%), 2586 neg (43%)
c prbs: 5 basic, 40445 probed, 101 failed, 3 lifted
c prbs: 5 simple, 26777 probed, 13 failed, 306 eqs
c prbs: 5 treelook, 3896 probed, 5 failed, 0 lifted
c prom: 717959 locked 18% out of 4032664 tried
c prps: 516191613 props, 132 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 12 count, 270 quat, 114 self1, 1 self2, 108 dup
c queu: 14 sorted, 3895776 next (3 steps 0.00)
c queu: 116003906 enq (116003877 steps 1.00), 115922796 deq 100%
c redc: 27505 clauses 7%, 402908 tried 17%, 12 sat 0%
c redc: 34111 lits 1%, 5278288 tried 7%, 12 sat 0%
c redc: 1132 times jump level reduced, 1.9 levels on average
c reds: 46 count, 50960.7 conflicts per reduce
c reds: 0 memlim 0%, 46 arith 100%
c reds: 1667555 collected 87%, 248181 retired 13%
c rmbd: 589 removed, 190 red 32%
c rsts: 46364 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: 2342657 count (761396 tried 0.3), 203027 sub out of 2339115 (8.7%)
c swps: 9 count, 10 rounds, 1287 queries (128.7/round)
c swps: 1244 sat calls, 41 unsat (3.2% success rate)
c swps: 33858 decisions 27.2, 4026 conflicts 3.2
c swps; 162.6 avg class size, 60.3 avg environment size
c swps: 0 failed, 22 impls, 77 equivs
c swp0: 426 type 0 queries, 121 unsat (28.4%), 412 sat (96.7%)
c swp1: 861 type 1 queries, 455 unsat (52.8%), 798 sat (92.7%)
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: 12477226 calls to obtain time
c tops: 1259 fixed 13%, 56 its, 41860.55 confs/it
c trds: 12 transitive reductions, 6191 removed, 1 failed
c trds: 113863 nodes, 144829 edges, 3329809 steps
c trim: 1118516 words, 4.3 MB
c trnr: 11 count, 1 bin, 492 trn, 57968589 steps
c unhd: 7 count, 8 rounds, 11873865 steps
c unhd: 456 non-trivial sccs of average size 2.0
c unhd: 3 units, 3 bin, 0 trn, 0 lrg
c unhd: 21 failed, 21 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 7968 tauts, 682 bin 9%, 458 trn 6%, 2707 lrg 34%
c unhd: 7968 tauts, 4121 stamp 52%, 6541 red 82%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 58596 str, 3 bin 0%, 212 trn 0%, 58381 lrg 100%, 58341 red 100%
c vars: 4290 remaining 45% and 5279 removed 55% out of 9569
c vars: 1259 fixed 13%, 2517 eliminated 26%, 1503 equivalent 16%
c vsts: 28094337681 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 54.5 search visits per propagation, 11953.8 per conflict
c wchs: 10136878202 pushed, 7653530 enlarged, 156 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2339385       1667555        248181      60118091      20765387       1507987
c 
c  0 0        132954   6     25514   2         0   0  39873930  66  11496784  55    691582  46     2.8
c  1 5        128865   6     82773   5     21039   8   7326556  12<  2679382  13<   214630  14<    0.7
c  2 6        619795  26    473740  28     63662  26   9192857  15   4147036  20    385695  26     2.5
c  3 9        990789  42<   760994  46<    89683  36<  2997524   5   1922329   9    176985  12     3.3
c  4 14       414096  18    292489  18     60439  24    654824   1    472386   2     35474   2     1.4
c  5 21        50347   2     30681   2     12526   5     69092   0     45515   0      3461   0     0.3
c  6 30         2429   0      1320   0       787   0      3173   0      1885   0       155   0     0.0
c  7 41          100   0        42   0        40   0       122   0        65   0         5   0     0.0
c  8 54           10   0         2   0         5   0        13   0         5   0         0   0     0.0
c 
c avg                  2.7           2.8           2.9           0.6           0.9           1.1
c std                  1.1           0.9           1.0           1.0           1.2           1.2
c 
c   14.175   2% cce
c    5.004   1% probe
c    4.460   1% elim
c    4.232   1% bump
c    2.270   0% decide
c 
c    6.880 < 1% rest (below)
c 
c    1.904   0% sweep
c    1.718   0% quatres
c    1.182   0% unhide
c    0.512   0% block
c    0.426   0% bca
c    0.370   0% gauss
c    0.323   0% ternres
c    0.304   0% transred
c    0.142   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.799   0% preprocessing     2%
c   31.678   5% inprocessing     98%
c ==================================
c   32.476   5% simplifying
c  605.965  95% search
c ==================================
c  638.441 100% all
c 
c       2344191 conflicts,        3671.7 confs/sec
c          2669 ternaries,         878.3 confs/ternary
c           578 binaries,         4055.7 confs/binary
c            56 iterations,      41860.6 confs/iteration
c 
c            46 reductions,          0.1 redus/sec,  50960.7 confs/reduction
c         46364 restarts,           72.6 rests/sec,     50.6 confs/restart
c       3895776 decisions,        6102.0 decis/sec,      1.7 decis/conflict
c     516191613 propagations,   808518.7 props/sec,    132.5 props/decision
c 
c 638.4 seconds, 51.6 MB
c launch: done
