c launch: /data/cnf/sc2014/app/atco_enc1_opt2_10_14.cnf.bz2
c host: atom10
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=3
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] SUM (--score=3)
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 1001 conflicts
c [decomp-3] removed 5 variables
c [simpleprobe-2] 4160 schedulable variables 71%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 5 variables
c [simpleprobe-2] 3504 variables remain 60% (2352 retained 40%)
c [simpleprobe-2] removed 5 variables, found 263 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 9896 literals 84%
c [treelook-1] scheduling used 300003 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 304874 steps
c [treelook-1] 9859 literals remain 84%
c [treelook-1] 5823 variables remain to probed next time 99%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 230 hbrs
c [basicprobe-1] limit 1055704 based on 131963 irredundant clauses
c [basicprobe-1-0] 460 probes remain 8% after last round
c [basicprobe-1-0] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 12 variables, found 2159 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 2 failed, 999 tauts, 0 hbrs, 587 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 5841 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 1203 blocked clauses
c [block-1] 1203 < 1/100 * 131918 = 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 364 clauses out of 561 (65%) of length 13
c [cce-1-1] eliminated 116 clauses out of 827 (14%) of length 12
c [cce-1-1] eliminated 97 clauses out of 168 (58%) 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 1096 (4%) of length 9
c [cce-1-1] eliminated 43 clauses out of 3022 (1%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 703 large clauses in 30000141 steps
c [cce-1-1] allowing another 15000070 steps for small clauses
c [cce-1-1] scheduling 13963 clauses = 12194 binary + 1769 ternary
c [cce-1-1] tried to eliminate 3768 small clauses 27%
c [cce-1-1] eliminated 407 binary clauses 3%
c [cce-1-1] eliminated 12 ternary clauses 1%
c [cce-1-1] eliminated 419 small clauses 3%
c [cce-1-1] eliminated 419 small clauses in 30000296 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1122 covered clauses in round 1
c [cce-1] eliminated 1122 covered clauses in TOTAL during 1 rounds
c [cce-1] 1122 < 1/100 * 130708 = 1307 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5841 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 47 variables 1% in round 1 in 15430840 steps
c [elim-2-1] backward subsumption/strengthening limit 4569160
c [elim-2-1-1] backward checking 860 touched variables 15%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 68 clauses in 3012107 steps
c [elim-2-1] rescheduled 78 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 259085 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 47 = 1% variables out of 5841 scheduled
c [elim-2] 47 < 1/100 * 5841 = 58 considered unsuccessful
c [bca-1] limit of 10000000 steps and 259106 added (scaled 2)
c [bca-1] 11120 out of 11590 literals actually usable 96%
c [bca-1] added 103 blocked clauses in 28722 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2069 pos 35.7% + 3725 neg 64.3% = 5794 sched 100.0% ret 0
c [sweep-1-1] 1090891 steps 56 queries 805.61 avg class size
c [sweep-1-1] 1825 decisions 51 SAT calls 60.06 avg env size
c [sweep-1-1] 5282 variables remain 91% (512 retained 9%)
c [decomp-6] removed 255 variables
c [sweep-1-1] removed 255 vars (0 failed, 5 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 255 vars in TOTAL (1 rounds, 55 queries)
c [phase-count-2] 117428 negative 91.0% of 129019 except 11591 9.0%
c [phase-count-2] 120973 positive 93.8% of 129019 except 8046 6.2%
c [phase-2] phase bias: 18 positive 38%, 29 negative 62%
c [sort-queue-2] sorted 4487 enqueued variables after 1001 conflicts
c [score-dist-2] active 1052 (19%), one 0 (0%), zero 4487 (81%)
c [score-dist-2] max exp 520, different 20 (4%)
c [score-dist-2] median active exp 514, avg 513.6
c [simplification-2] removed 327 variables 5.6% (5539 remain 60%)
c [simplification-2] removed 2967 irredundant clauses 2.2% (129019 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 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 25557 quaternary clauses 30% in total
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [quatres-1-2] added 15 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 5539 free variables schedulable
c [ternres-1] 24 ternary resolvents (0 bin, 24 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 860 at-most-one constraints of average size 3.1
c [card-2] found 90 at-most-two constraints of average size 4.6
c [card-2] using previous limit 1000000 for elimination
c [card-2] 950 out of 950 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 443 xors of average arity 3.0
c [gauss-1] connected 1324 occurrences of 548 variables (average 2.4)
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 2 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 9960 literals 90%
c [treelook-2] scheduling used 300036 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 303272 steps
c [treelook-2] 9931 literals remain 90%
c [treelook-2] 5460 variables remain to probed next time 99%
c [decomp-8] removed 2 variables
c [treelook-2] removed 2 variables, found 168 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 852 tauts, 0 hbrs, 269 literals
c [transred-1] limit 128028 based on 128028 irredundant clauses
c [transred-1] removed 346 transitive binary clauses
c [bca-2] limit of 10000000 steps and 256453 added (scaled 2)
c [bca-2] 10234 out of 11072 literals actually usable 92%
c [bca-2] added 17 blocked clauses in 28269 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2115 pos 41.9% + 2928 neg 58.1% = 5043 sched 91.1% ret 492
c [sweep-2-1] 1019620 steps 109 queries 397.27 avg class size
c [sweep-2-1] 2577 decisions 104 SAT calls 50.45 avg env size
c [sweep-2-1] 4013 variables remain 73% (1520 retained 27%)
c [decomp-9] removed 49 variables
c [sweep-2-1] removed 49 vars (0 failed, 4 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 49 vars in TOTAL (1 rounds, 108 queries)
c [phase-count-3] 116060 negative 90.8% of 127847 except 11787 9.2%
c [phase-count-3] 119615 positive 93.6% of 127847 except 8232 6.4%
c [phase-3] phase bias: 8 positive 44%, 10 negative 56%
c [sort-queue-3] sorted 4136 enqueued variables after 3001 conflicts
c [score-dist-3] active 1350 (25%), one 0 (0%), zero 4136 (75%)
c [score-dist-3] max exp 523, different 22 (4%)
c [score-dist-3] median active exp 515, avg 515.0
c [simplification-3] removed 53 variables 1.0% (5486 remain 60%)
c [simplification-3] removed 1172 irredundant clauses 0.9% (127847 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  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.3    5485   127847      7294    6836    997  2373    9    13   12  69%     93   12   11    1 1023%
c 
c [simplification-4] limit 13001 conflicts (hard 23001) hit after 13002 conflicts
c [quatres-2] found 25581 quaternary clauses 30% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 15 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5485 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 74 variables remain 1% (5411 retained 99%)
c [decomp-10] removed 3 variables
c [basicprobe-2] limit 2457843 penalty 0 = 0 + 0
c [basicprobe-2-0] 414 sched 8%, 8 failed, 0 lifted, 1077 hbrs
c [decomp-11] removed 88 variables
c [basicprobe-2-1] 1086 sched 20%, 4 failed, 0 lifted, 379 hbrs
c [decomp-12] removed 10 variables
c [basicprobe-2-2] 829 probes remain 15% after last round
c [basicprobe-2-2] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 98 variables, found 1468 hbrs
c [bate-1] eliminated 152 asymmetric tautologies during probing
c [transred-2] limit 491568 with penalty 0 = 0 + 0
c [transred-2] removed 929 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5385 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 21 blocked clauses
c [block-2] 21 < 1/100 * 127187 = 1271 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 1 clauses out of 249 (0%) of length 13
c [cce-2-1] eliminated 9 clauses out of 699 (1%) of length 12
c [cce-2-1] eliminated 5 clauses out of 96 (5%) of length 11
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 19 large clauses in 15000082 steps
c [cce-2-1] allowing another 7500041 steps for small clauses
c [cce-2-1] scheduling 41090 clauses = 10625 binary + 30465 ternary
c [cce-2-1] tried to eliminate 1925 small clauses 5%
c [cce-2-1] eliminated 21 binary clauses 0%
c [cce-2-1] eliminated 77 ternary clauses 0%
c [cce-2-1] eliminated 98 small clauses 0%
c [cce-2-1] eliminated 98 small clauses in 15000491 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 117 covered clauses in round 1
c [cce-2] eliminated 117 covered clauses in TOTAL during 1 rounds
c [cce-2] 117 < 1/100 * 127166 = 1271 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5385 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 785 not tried 15% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 40 = 1% variables out of 5385 scheduled
c [elim-3] 40 < 1/100 * 5385 = 53 considered unsuccessful
c [bca-3] limit of 10000000 steps and 254418 added (scaled 2)
c [bca-3] 9510 out of 10692 literals actually usable 89%
c [bca-3] added 7 blocked clauses in 36300 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1866 pos 47.6% + 2058 neg 52.4% = 3924 sched 73.4% ret 1421
c [sweep-3-1] 1056806 steps 24 queries 893.08 avg class size
c [sweep-3-1] 887 decisions 23 SAT calls 77.48 avg env size
c [sweep-3-1] 3763 variables remain 70% (1582 retained 30%)
c [decomp-13] removed 2 variables
c [sweep-3-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 2 vars in TOTAL (1 rounds, 23 queries)
c [phase-count-4] 114336 negative 90.1% of 126929 except 12593 9.9%
c [phase-count-4] 117968 positive 92.9% of 126929 except 8961 7.1%
c [phase-4] phase bias: 1 positive 9%, 10 negative 91%
c [sort-queue-4] sorted 4019 enqueued variables after 13002 conflicts
c [score-dist-4] active 1324 (25%), one 0 (0%), zero 4019 (75%)
c [score-dist-4] max exp 527, different 25 (5%)
c [score-dist-4] median active exp 515, avg 516.4
c [simplification-4] removed 142 variables 2.6% (5343 remain 58%)
c [simplification-4] removed 918 irredundant clauses 0.7% (126929 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 38002 (soft 28002 + delta 10000)
c [simplification-4] new conflict limit 28002 (hard 38002)
c 
c [simplification-5] limit 28002 conflicts (hard 38002) hit after 28004 conflicts
c [quatres-3] found 25599 quaternary clauses 30% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 228 xors of average arity 3.0
c [gauss-2] connected 684 occurrences of 426 variables (average 1.6)
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 [simpleprobe-3] 3199 schedulable variables 60%
c [simpleprobe-3] limit 5210742 penalty 0 = 0 + 0
c [decomp-15] removed 6 variables
c [simpleprobe-3] 3345 variables remain 63% (1992 retained 37%)
c [simpleprobe-3] removed 6 variables, found 471 hbrs, 0 units
c [unhide-4] limit 130268 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 1 failed, 447 tauts, 0 hbrs, 7769 literals
c [transred-3] limit 1302685 with penalty 0 = 0 + 0
c [transred-3] removed 333 transitive binary clauses
c [bca-4] limit of 10000000 steps and 254313 added (scaled 2)
c [bca-4] 9445 out of 10674 literals actually usable 88%
c [bca-4] added 0 blocked clauses in 48494 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1779 pos 47.3% + 1979 neg 52.7% = 3758 sched 70.4% ret 1578
c [sweep-4-1] 1001901 steps 37 queries 579.86 avg class size
c [sweep-4-1] 1028 decisions 36 SAT calls 66.78 avg env size
c [sweep-4-1] 3613 variables remain 68% (1723 retained 32%)
c [decomp-16] removed 7 variables
c [sweep-4-1] removed 7 vars (0 failed, 2 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 7 vars in TOTAL (1 rounds, 36 queries)
c [phase-count-5] 114265 negative 90.1% of 126875 except 12610 9.9%
c [phase-count-5] 117916 positive 92.9% of 126875 except 8959 7.1%
c [phase-5] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-5] sorted 3959 enqueued variables after 28004 conflicts
c [score-dist-5] active 1370 (26%), one 0 (0%), zero 3959 (74%)
c [score-dist-5] max exp 530, different 28 (5%)
c [score-dist-5] median active exp 516, avg 517.2
c [simplification-5] removed 14 variables 0.3% (5329 remain 58%)
c [simplification-5] removed 54 irredundant clauses 0.0% (126875 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 35000
c [simplification-5] penalized conflict interval 35000 = 1 * 35000
c [simplification-5] hard conflict limit 80504 (soft 63004 + delta 17500)
c [simplification-5] new conflict limit 63004 (hard 80504)
c 
c [simplification-6] limit 63004 conflicts (hard 80504) hit after 63004 conflicts
c [quatres-4] found 25701 quaternary clauses 30% in total
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [ternres-3] limit 2147932 with penalty 1 = 1 + 0
c [ternres-3] 73 schedulable variables 1%
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 536983 penalty 2 = 2 + 0
c [card-3] found 625 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 536983 for elimination
c [card-3] 625 out of 625 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 429586 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 10603 literals 99%
c [treelook-3] scheduling used 429588 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 429586 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 431940 steps
c [treelook-3] 10499 literals remain 99%
c [treelook-3] 5252 variables remain to probed next time 99%
c [treelook-3] removed 0 variables, found 98 hbrs
c [unhide-5] limit 859172 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 160 tauts, 0 hbrs, 6996 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 148 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12887590 penalty 0 = 0 + 0
c [sweep-5-1] 1727 pos 47.8% + 1884 neg 52.2% = 3611 sched 67.8% ret 1718
c [sweep-5-1] 13714668 steps 428 queries 59.19 avg class size
c [sweep-5-1] 11195 decisions 408 SAT calls 54.24 avg env size
c [sweep-5-1] 1067 variables remain 20% (4258 retained 80%)
c [decomp-19] removed 38 variables
c [sweep-5-1] removed 38 vars (0 failed, 25 eqs, 7 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 38 vars in TOTAL (1 rounds, 427 queries)
c [phase-count-6] 113953 negative 90.0% of 126596 except 12643 10.0%
c [phase-count-6] 117610 positive 92.9% of 126596 except 8986 7.1%
c [phase-6] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-6] sorted 3295 enqueued variables after 63004 conflicts
c [score-dist-6] active 1996 (38%), one 0 (0%), zero 3295 (62%)
c [score-dist-6] max exp 532, different 29 (5%)
c [score-dist-6] median active exp 520, avg 520.4
c [simplification-6] removed 38 variables 0.7% (5291 remain 58%)
c [simplification-6] removed 279 irredundant clauses 0.2% (126596 remain 90%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 17500 = 35000 / 2
c [simplification-6] new conflict interval 52500
c [simplification-6] penalized conflict interval 52500 = 1 * 52500
c [simplification-6] hard conflict limit 141754 (soft 115504 + delta 26250)
c [simplification-6] new conflict limit 115504 (hard 141754)
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 -   11.4    5291   126596     63004   26892   1052  2530   10    12   11  82%    577    5   10    6  148%
c -   15.2    5291   126596     99503   28468   1059  2531   10    12   15  81%    768    3    9    8  111%
c 
c [simplification-7] limit 115504 conflicts (hard 141754) hit after 115504 conflicts
c [quatres-5] found 25791 quaternary clauses 30% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 47 quaternary resolvents
c [decomp-20] removed 2 variables
c [basicprobe-3] limit 43162397 penalty 0 = 0 + 0
c [basicprobe-3-0] 825 sched 16%, 2 failed, 0 lifted, 211 hbrs
c [decomp-21] removed 2 variables
c [basicprobe-3-1] 1068 sched 20%, 3 failed, 0 lifted, 164 hbrs
c [decomp-22] removed 3 variables
c [basicprobe-3-2] 1068 sched 20%, 1 failed, 0 lifted, 60 hbrs
c [decomp-23] removed 1 variables
c [basicprobe-3-3] 1068 sched 20%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-4] 1068 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 6 variables, found 438 hbrs
c [bate-2] eliminated 92 asymmetric tautologies during probing
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 228 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5283 variables 100%
c [block-3] limit of 21581198 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 15 blocked clauses
c [block-3] 15 < 1/100 * 126369 = 1263 considered unsuccessful
c [cce-3] limit of 10790599 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 38 clauses out of 244 (16%) of length 13
c [cce-3-1] eliminated 40 clauses out of 687 (6%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 78 large clauses in 10790614 steps
c [cce-3-1] allowing another 5395307 steps for small clauses
c [cce-3-1] scheduling 40562 clauses = 10465 binary + 30097 ternary
c [cce-3-1] tried to eliminate 1320 small clauses 3%
c [cce-3-1] eliminated 42 binary clauses 0%
c [cce-3-1] eliminated 178 ternary clauses 1%
c [cce-3-1] eliminated 220 small clauses 1%
c [cce-3-1] eliminated 220 small clauses in 10790599 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 298 covered clauses in round 1
c [cce-3] eliminated 298 covered clauses in TOTAL during 1 rounds
c [cce-3] 298 < 1/100 * 126354 = 1263 considered unsuccessful
c [elim-4] 779 variables 15% will be scheduled this time
c [elim-4] scheduled 779 variables 15%
c [elim-4] boosting limit by 20
c [elim-4] limit of 863247955 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 115312311 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 779 scheduled
c [bca-5] limit of 10000000 steps and 251559 added (scaled 2)
c [bca-5] 8072 out of 10568 literals actually usable 76%
c [bca-5] added 15 blocked clauses in 61038 steps
c [sweep-6] limit 2589743 penalty 0 = 0 + 0
c [sweep-6-1] 514 pos 48.7% + 542 neg 51.3% = 1056 sched 20.0% ret 4227
c [sweep-6-1] 2710490 steps 210 queries 41.72 avg class size
c [sweep-6-1] 5300 decisions 202 SAT calls 56.52 avg env size
c [sweep-6-1] 506 variables remain 10% (4777 retained 90%)
c [decomp-25] removed 5 variables
c [sweep-6-1] removed 5 vars (0 failed, 8 eqs, 0 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 5 vars in TOTAL (1 rounds, 209 queries)
c [phase-count-7] 112906 negative 90.0% of 125494 except 12588 10.0%
c [phase-count-7] 116593 positive 92.9% of 125494 except 8901 7.1%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 2663 enqueued variables after 115504 conflicts
c [score-dist-7] active 2615 (50%), one 0 (0%), zero 2663 (50%)
c [score-dist-7] max exp 534, different 29 (5%)
c [score-dist-7] median active exp 522, avg 522.2
c [simplification-7] removed 13 variables 0.2% (5278 remain 58%)
c [simplification-7] removed 1102 irredundant clauses 0.9% (125494 remain 89%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 26250 = 52500 / 2
c [simplification-7] new conflict interval 78750
c [simplification-7] penalized conflict interval 78750 = 1 * 78750
c [simplification-7] hard conflict limit 233629 (soft 194254 + delta 39375)
c [simplification-7] new conflict limit 194254 (hard 233629)
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 -   21.8    5278   125494    130501   29340   1306  2753   30    56   15  53%    864   38   33   13  257%
c -   29.0    5278   125494    160641   27194   1330  2759   46    62   15  74%    923   27   53   23  230%
c 
c [simplification-8] limit 194254 conflicts (hard 233629) hit after 194255 conflicts
c [quatres-6] found 25885 quaternary clauses 30% in total
c [quatres-6-2] added 21 quaternary resolvents
c [gauss-3] limit 801348 penalty 2 = 2 + 0
c [gauss-3] extracted 171 xors of average arity 3.0
c [gauss-3] connected 510 occurrences of 309 variables (average 1.7)
c [gauss-3] limit 801348 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 3 variables
c [simpleprobe-4] 3316 schedulable variables 63%
c [simpleprobe-4] limit 64107858 penalty 0 = 0 + 0
c [decomp-27] removed 70 variables
c [simpleprobe-4] 2115 variables remain 41% (3090 retained 59%)
c [simpleprobe-4] removed 70 variables, found 2355 hbrs, 0 units
c [unhide-6] limit 1602696 with penalty 1 = 1 + 0
c [unhide-6-7] 0 units, 0 failed, 1684 tauts, 0 hbrs, 92776 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 616 transitive binary clauses
c [bca-6] limit of 10000000 steps and 251193 added (scaled 2)
c [bca-6] 7544 out of 10412 literals actually usable 72%
c [bca-6] added 0 blocked clauses in 74991 steps
c [sweep-7] limit 4808089 penalty 0 = 0 + 0
c [sweep-7-1] 247 pos 48.9% + 258 neg 51.1% = 505 sched 9.7% ret 4700
c [sweep-7-1] 2905323 steps 305 queries 12.83 avg class size
c [sweep-7-1] 7593 decisions 288 SAT calls 62.28 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-28] removed 20 variables
c [sweep-7-1] removed 20 vars (0 failed, 18 eqs, 12 impls)
c [sweep-7-2] 2949 pos 56.9% + 2236 neg 43.1% = 5185 sched 100.0% ret 0
c [sweep-7-2] 1932244 steps 41 queries 477.44 avg class size
c [sweep-7-2] 1767 decisions 43 SAT calls 110.44 avg env size
c [sweep-7-2] 4479 variables remain 86% (706 retained 14%)
c [decomp-29] removed 5 variables
c [sweep-7-2] removed 5 vars (0 failed, 2 eqs, 0 impls)
c [sweep-7] removed 25 vars in TOTAL (2 rounds, 344 queries)
c [phase-count-8] 111990 negative 89.4% of 125295 except 13305 10.6%
c [phase-count-8] 115794 positive 92.4% of 125295 except 9501 7.6%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-8] sorted 2403 enqueued variables after 194255 conflicts
c [score-dist-8] active 2777 (54%), one 0 (0%), zero 2403 (46%)
c [score-dist-8] max exp 535, different 30 (6%)
c [score-dist-8] median active exp 525, avg 525.1
c [simplification-8] removed 98 variables 1.9% (5180 remain 57%)
c [simplification-8] removed 199 irredundant clauses 0.2% (125295 remain 89%)
c [simplification-8] maximum reduction of 2% = max (2%, 0%)
c [simplification-8] geometric conflict interval increment 26250 = 78750 / 3
c [simplification-8] new conflict interval 105000
c [simplification-8] penalized conflict interval 105000 = 1 * 105000
c [simplification-8] hard conflict limit 351755 (soft 299255 + delta 52500)
c [simplification-8] new conflict limit 299255 (hard 351755)
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 -   39.2    5180   125295    195404   27452   1310  2942   38    50   16  76%    965    7   36   30  120%
c -   46.8    5180   125295    231407   27387   1357  2943   31    50   16  62%    990    4   25   32   78%
c -   54.9    5180   125295    268294   30524   1380  2946   34    44   17  77%   1004   -2   34   33  102%
c 
c [simplification-9] limit 299255 conflicts (hard 351755) hit after 299256 conflicts
c [quatres-7] found 26047 quaternary clauses 30% in total
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 14 quaternary resolvents
c [ternres-4] limit 6663743 with penalty 2 = 2 + 0
c [ternres-4] all 5180 free variables schedulable
c [ternres-4] 42 ternary resolvents (4 bin, 38 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-30] removed 1 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 186 transitive binary clauses
c [transred-7] found 1 units
c [sweep-8] limit 7996492 penalty 0 = 0 + 0
c [sweep-8-1] 2531 pos 56.6% + 1944 neg 43.4% = 4475 sched 86.4% ret 703
c [sweep-8-1] 8015640 steps 344 queries 46.93 avg class size
c [sweep-8-1] 12528 decisions 360 SAT calls 81.61 avg env size
c [sweep-8-1] 1243 variables remain 24% (3935 retained 76%)
c [decomp-31] removed 34 variables
c [sweep-8-1] removed 34 vars (0 failed, 33 eqs, 4 impls)
c [sweep-8] removed 34 vars in TOTAL (1 rounds, 343 queries)
c [sort-queue-9] sorted 2183 enqueued variables after 299256 conflicts
c [score-dist-9] active 2961 (58%), one 0 (0%), zero 2183 (42%)
c [score-dist-9] max exp 537, different 32 (6%)
c [score-dist-9] median active exp 528, avg 526.5
c [simplification-9] removed 36 variables 0.7% (5144 remain 56%)
c [simplification-9] removed 45 irredundant clauses 0.0% (125250 remain 89%)
c [simplification-9] maximum reduction of 1% = max (1%, 0%)
c [simplification-9] geometric conflict interval increment 52500 = 105000 / 2
c [simplification-9] new conflict interval 157500
c [simplification-9] penalized conflict interval 157500 = 1 * 157500
c [simplification-9] hard conflict limit 535506 (soft 456756 + delta 78750)
c [simplification-9] new conflict limit 456756 (hard 535506)
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 -   63.5    5144   125250    303243   31403   1449  2853   34    46   17  74%   1013   -1   34   34  100%
c -   70.7    5144   125250    339127   32364   1470  2854   29    42   17  69%   1017   -6   29   33   90%
c -   78.7    5144   125250    375683   33934   1476  2855   25    50   17  49%   1020    5   22   31   72%
c -   87.0    5144   125250    412547   34108   1488  2859   31    40   26  76%   1022   -3   33   30  108%
c -   95.4    5144   125250    451619   34749   1515  2860   31    41   26  75%   1023    0   35   30  116%
c 
c [simplification-10] limit 456756 conflicts (hard 535506) hit after 459497 conflicts
c [quatres-8] found 26231 quaternary clauses 29% in total
c [quatres-8-2] added 10 single-self-subsuming ternary resolvents
c [quatres-8-2] added 5 quaternary resolvents
c [card-4] limit 2691956 penalty 3 = 3 + 0
c [card-4] found 629 at-most-one constraints of average size 3.2
c [card-4] found 99 at-most-two constraints of average size 4.6
c [card-4] using previous limit 2691956 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 [treelook-4] limit 2153564 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 10258 literals 100%
c [treelook-4] scheduling used 421347 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2153564 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 2171153 steps
c [treelook-4] 9965 literals remain 97%
c [treelook-4] 5065 variables remain to probed next time 98%
c [decomp-33] removed 2 variables
c [treelook-4] removed 2 variables, found 537 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 408 transitive binary clauses
c [bca-7] limit of 10000000 steps and 250737 added (scaled 2)
c [bca-7] 7021 out of 10286 literals actually usable 68%
c [bca-7] added 0 blocked clauses in 57469 steps
c [sweep-9] limit 12921389 penalty 0 = 0 + 0
c [sweep-9-1] 663 pos 53.5% + 576 neg 46.5% = 1239 sched 24.1% ret 3903
c [sweep-9-1] 4245031 steps 544 queries 17.87 avg class size
c [sweep-9-1] 14179 decisions 551 SAT calls 58.80 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-34] removed 21 variables
c [sweep-9-1] removed 21 vars (0 failed, 26 eqs, 4 impls)
c [sweep-9-2] 2875 pos 56.1% + 2246 neg 43.9% = 5121 sched 100.0% ret 0
c [sweep-9-2] 8680945 steps 496 queries 29.90 avg class size
c [sweep-9-2] 15930 decisions 506 SAT calls 66.23 avg env size
c [sweep-9-2] 751 variables remain 15% (4370 retained 85%)
c [decomp-35] removed 16 variables
c [sweep-9-2] removed 16 vars (0 failed, 20 eqs, 2 impls)
c [sweep-9] removed 37 vars in TOTAL (2 rounds, 1038 queries)
c [sort-queue-10] sorted 1982 enqueued variables after 459497 conflicts
c [score-dist-10] active 3123 (61%), one 0 (0%), zero 1982 (39%)
c [score-dist-10] max exp 538, different 33 (6%)
c [score-dist-10] median active exp 529, avg 527.7
c [simplification-10] removed 39 variables 0.8% (5105 remain 56%)
c [simplification-10] removed 172 irredundant clauses 0.1% (125078 remain 89%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 78750 = 157500 / 2
c [simplification-10] new conflict interval 236250
c [simplification-10] penalized conflict interval 236250 = 1 * 236250
c [simplification-10] hard conflict limit 813872 (soft 695747 + delta 118125)
c [simplification-10] new conflict limit 695747 (hard 813872)
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 -  105.5    5105   125078    490462   36000   1580  3132   28    35   16  80%   1023   -5   28   30   93%
c -  113.8    5105   125078    531311   36428   1593  3133   27    34   24  81%   1024   -3   29   29  100%
c -  122.4    5105   125078    573569   37106   1636  3134   24    39   24  61%   1024    3   28   27  100%
c -  129.8    5105   125078    614615   37352   1661  3134   26    32   24  80%   1024   -4   26   25  101%
c -  137.6    5105   125078    656429   38203   1666  3134   25    39   24  64%   1024    3   19   26   74%
c 
c [simplification-11] limit 695747 conflicts (hard 813872) hit after 695747 conflicts
c [quatres-9] found 26362 quaternary clauses 29% in total
c [quatres-9-2] added 13 single-self-subsuming ternary resolvents
c [quatres-9-2] added 18 quaternary resolvents
c [ternres-5] limit 33091804 with penalty 1 = 1 + 0
c [ternres-5] all 5105 free variables schedulable
c [ternres-5] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-5] fully completed ternary resolution
c [basicprobe-4] limit 330918045 penalty 0 = 0 + 0
c [basicprobe-4-0] 998 sched 20%, 3 failed, 0 lifted, 214 hbrs
c [decomp-37] removed 3 variables
c [basicprobe-4-1] 998 sched 20%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-4-2] 998 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-2] fully completed probing
c [basicprobe-4-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-4-2] removed 3 variables, found 224 hbrs
c [bate-3] eliminated 59 asymmetric tautologies during probing
c [unhide-7] limit 3309180 with penalty 2 = 2 + 0
c [unhide-7-9] 0 units, 0 failed, 485 tauts, 0 hbrs, 82189 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 106 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 5102 variables 100%
c [block-4] limit of 82729511 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 642 blocked clauses
c [block-4] 642 < 1/100 * 124599 = 1245 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 413647556 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 3 clauses out of 645 (0%) of length 12
c [cce-4-1] eliminated 9 clauses out of 100 (9%) of length 11
c [cce-4-1] eliminated 7 clauses out of 233 (3%) of length 10
c [cce-4-1] eliminated 6 clauses out of 1051 (1%) of length 9
c [cce-4-1] eliminated 109 clauses out of 2980 (4%) of length 8
c [cce-4-1] eliminated 430 clauses out of 7718 (6%) of length 7
c [cce-4-1] eliminated 914 clauses out of 17311 (5%) of length 6
c [cce-4-1] eliminated 767 clauses out of 26592 (3%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 2245 large clauses in 413647783 steps
c [cce-4-1] allowing another 206823891 steps for small clauses
c [cce-4-1] scheduling 39268 clauses = 10064 binary + 29204 ternary
c [cce-4-1] tried to eliminate 39268 small clauses 100%
c [cce-4-1] eliminated 302 binary clauses 3%
c [cce-4-1] eliminated 1542 ternary clauses 5%
c [cce-4-1] eliminated 1844 small clauses 5%
c [cce-4-1] eliminated 1844 small clauses in 350972439 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 4089 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 31337653 steps for small clauses
c [cce-4-2] scheduling 37425 clauses = 9762 binary + 27663 ternary
c [cce-4-2] tried to eliminate 7933 small clauses 21%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 4089 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5086 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 180 not tried 4% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 54 = 1% variables out of 5086 scheduled
c [sweep-10] limit 19855082 penalty 0 = 0 + 0
c [sweep-10-1] 420 pos 56.3% + 326 neg 43.7% = 746 sched 14.8% ret 4286
c [sweep-10-1] 3962789 steps 371 queries 16.95 avg class size
c [sweep-10-1] 10021 decisions 372 SAT calls 61.69 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-39] removed 12 variables
c [sweep-10-1] removed 12 vars (0 failed, 14 eqs, 1 impls)
c [sweep-10-2] 2804 pos 55.9% + 2216 neg 44.1% = 5020 sched 100.0% ret 0
c [sweep-10-2] 13739854 steps 829 queries 28.50 avg class size
c [sweep-10-2] 23219 decisions 834 SAT calls 61.19 avg env size
c [sweep-10-2] fully completed sweeping round
c [decomp-40] removed 29 variables
c [sweep-10-2] removed 29 vars (0 failed, 35 eqs, 6 impls)
c [sweep-10-3] 2786 pos 55.8% + 2205 neg 44.2% = 4991 sched 100.0% ret 0
c [sweep-10-3] 2290770 steps 47 queries 348.32 avg class size
c [sweep-10-3] 2259 decisions 48 SAT calls 125.85 avg env size
c [sweep-10-3] 4054 variables remain 81% (937 retained 19%)
c [decomp-41] removed 4 variables
c [sweep-10-3] removed 4 vars (0 failed, 3 eqs, 0 impls)
c [sweep-10] removed 45 vars in TOTAL (3 rounds, 1244 queries)
c [sort-queue-11] sorted 1750 enqueued variables after 695747 conflicts
c [score-dist-11] active 3237 (65%), one 0 (0%), zero 1750 (35%)
c [score-dist-11] max exp 539, different 33 (6%)
c [score-dist-11] median active exp 529, avg 528.2
c [simplification-11] removed 118 variables 2.3% (4987 remain 54%)
c [simplification-11] removed 6464 irredundant clauses 5.2% (118614 remain 84%)
c [simplification-11] maximum reduction of 5% = max (2%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 6957 = min (695747/100, 236250)
c [simplification-11] penalized conflict interval 6957 = 1 * 6957
c [simplification-11] hard conflict limit 712704 (soft 702704 + delta 10000)
c [simplification-11] new conflict limit 702704 (hard 712704)
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 -  154.7    4987   118614    698442   38191   2992  3105   32    40   17  81%   1024    2   29   28  105%
c 
c [simplification-12] limit 702704 conflicts (hard 712704) hit after 702704 conflicts
c [quatres-10] found 25337 quaternary clauses 29% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-2] added 8 single-self-subsuming ternary resolvents
c [quatres-10-2] added 5 quaternary resolvents
c [ternres-6] limit 66932060 with penalty 0 = 0 + 0
c [ternres-6] all 4987 free variables schedulable
c [ternres-6] 26 ternary resolvents (0 bin, 26 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-4] limit 1673301 penalty 3 = 3 + 0
c [gauss-4] extracted 254 xors of average arity 3.0
c [gauss-4] connected 759 occurrences of 396 variables (average 1.9)
c [gauss-4] limit 1673301 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] 1991 schedulable variables 40%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-43] removed 19 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 19 variables, found 2636 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1489 transitive binary clauses
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 200796180 penalty 0 = 0 + 0
c [sweep-11-1] 2213 pos 54.8% + 1822 neg 45.2% = 4035 sched 81.2% ret 933
c [sweep-11-1] 10085094 steps 814 queries 29.35 avg class size
c [sweep-11-1] 22302 decisions 831 SAT calls 62.04 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-44] removed 31 variables
c [sweep-11-1] removed 31 vars (0 failed, 35 eqs, 4 impls)
c [sweep-11-2] 2744 pos 55.6% + 2193 neg 44.4% = 4937 sched 100.0% ret 0
c [sweep-11-2] 9497236 steps 813 queries 33.95 avg class size
c [sweep-11-2] 21141 decisions 827 SAT calls 59.25 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-45] removed 24 variables
c [sweep-11-2] removed 24 vars (0 failed, 29 eqs, 2 impls)
c [sweep-11-3] 2727 pos 55.5% + 2186 neg 44.5% = 4913 sched 100.0% ret 0
c [sweep-11-3] 11585049 steps 817 queries 28.01 avg class size
c [sweep-11-3] 21917 decisions 834 SAT calls 61.15 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-46] removed 23 variables
c [sweep-11-3] removed 23 vars (0 failed, 30 eqs, 0 impls)
c [sweep-11] removed 78 vars in TOTAL (3 rounds, 2441 queries)
c [sort-queue-12] sorted 1540 enqueued variables after 702704 conflicts
c [score-dist-12] active 3350 (69%), one 0 (0%), zero 1540 (31%)
c [score-dist-12] max exp 539, different 33 (6%)
c [score-dist-12] median active exp 528, avg 528.3
c [simplification-12] removed 97 variables 1.9% (4890 remain 53%)
c [simplification-12] removed 349 irredundant clauses 0.3% (118265 remain 84%)
c [simplification-12] maximum reduction of 2% = max (2%, 0%)
c [simplification-12] geometric conflict interval increment 78750 = 236250 / 3
c [simplification-12] new conflict interval 315000
c [simplification-12] penalized conflict interval 315000 = 1 * 315000
c [simplification-12] hard conflict limit 1175204 (soft 1017704 + delta 157500)
c [simplification-12] new conflict limit 1017704 (hard 1175204)
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 -  165.1    4890   118265    738678   40087   3080  4427   25    36   16  69%   1024   -2   27   27   98%
c -  174.1    4890   118265    782807   41175   3089  4427   24    33   24  73%   1024   -3   29   26  110%
c -  183.8    4890   118265    828897   41425   3092  4428   25    31   25  80%   1024   -3   25   25  100%
c -  193.0    4890   118265    873350   41529   3110  4430   23    29   25  79%   1024   -3   23   24   96%
c -  202.8    4890   118265    919508   43415   3140  4432   22    29   25  75%   1024   -1   23   22  101%
c -  212.7    4890   118265    963417   44264   3164  4432   23    30   25  75%   1024   -3   22   23   95%
c -  222.4    4890   118265   1008692   45002   3168  4436   25    30   25  82%   1024   -2   25   24  107%
c 
c [simplification-13] limit 1017704 conflicts (hard 1175204) hit after 1033058 conflicts
c [quatres-11] found 25480 quaternary clauses 28% in total
c [quatres-11-1] removed 12 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 20 single-self-subsuming ternary resolvents
c [quatres-11-2] added 16 quaternary resolvents
c [ternres-7] limit 101530160 with penalty 0 = 0 + 0
c [ternres-7] all 4890 free variables schedulable
c [ternres-7] 53 ternary resolvents (1 bin, 52 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-5] limit 10153016 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 9743 literals 100%
c [treelook-5] scheduling used 462949 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 10153016 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 10155567 steps
c [treelook-5] 7360 literals remain 75%
c [treelook-5] 4586 variables remain to probed next time 94%
c [treelook-5] removed 2 variables, found 903 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1094 transitive binary clauses
c [cce-5] limit of 126912700 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 285 (26%) of length 13
c [cce-5-1] eliminated 23 clauses out of 648 (4%) of length 12
c [cce-5-1] eliminated 17 clauses out of 94 (18%) of length 11
c [cce-5-1] eliminated 50 clauses out of 226 (22%) of length 10
c [cce-5-1] eliminated 162 clauses out of 1051 (15%) of length 9
c [cce-5-1] eliminated 40 clauses out of 2875 (1%) of length 8
c [cce-5-1] eliminated 913 clauses out of 7284 (13%) of length 7
c [cce-5-1] eliminated 12 clauses out of 16306 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1375 large clauses in 126913107 steps
c [cce-5-1] allowing another 63456553 steps for small clauses
c [cce-5-1] scheduling 35815 clauses = 9395 binary + 26420 ternary
c [cce-5-1] tried to eliminate 17229 small clauses 48%
c [cce-5-1] eliminated 191 binary clauses 2%
c [cce-5-1] eliminated 1256 ternary clauses 5%
c [cce-5-1] eliminated 1447 small clauses 4%
c [cce-5-1] eliminated 1447 small clauses in 126912717 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2822 covered clauses in round 1
c [cce-5] eliminated 2822 covered clauses in TOTAL during 1 rounds
c [elim-6] 179 variables 4% will be scheduled this time
c [elim-6] scheduled 179 variables 4%
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 179721713 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 179 scheduled
c [bca-8] limit of 10000000 steps and 227985 added (scaled 2)
c [bca-8] 6043 out of 9778 literals actually usable 62%
c [bca-8] added 2 blocked clauses in 79984 steps
c [sweep-12] limit 30459048 penalty 0 = 0 + 0
c [sweep-12-1] 2756 pos 56.4% + 2132 neg 43.6% = 4888 sched 100.0% ret 0
c [sweep-12-1] 14694255 steps 756 queries 22.70 avg class size
c [sweep-12-1] 23624 decisions 773 SAT calls 66.62 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-49] removed 29 variables
c [sweep-12-1] removed 29 vars (0 failed, 35 eqs, 1 impls)
c [sweep-12-2] 2734 pos 56.3% + 2125 neg 43.7% = 4859 sched 100.0% ret 0
c [sweep-12-2] 13148907 steps 735 queries 24.40 avg class size
c [sweep-12-2] 21697 decisions 751 SAT calls 63.74 avg env size
c [sweep-12-2] fully completed sweeping round
c [decomp-50] removed 25 variables
c [sweep-12-2] removed 25 vars (0 failed, 36 eqs, 1 impls)
c [sweep-12-3] 2718 pos 56.2% + 2116 neg 43.8% = 4834 sched 100.0% ret 0
c [sweep-12-3] 2693155 steps 64 queries 249.08 avg class size
c [sweep-12-3] 2837 decisions 63 SAT calls 105.95 avg env size
c [sweep-12-3] 3405 variables remain 70% (1429 retained 30%)
c [sweep-12-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 54 vars in TOTAL (3 rounds, 1552 queries)
c [sort-queue-13] sorted 1396 enqueued variables after 1033058 conflicts
c [score-dist-13] active 3438 (71%), one 0 (0%), zero 1396 (29%)
c [score-dist-13] max exp 540, different 34 (6%)
c [score-dist-13] median active exp 529, avg 529.1
c [simplification-13] removed 56 variables 1.1% (4834 remain 53%)
c [simplification-13] removed 4561 irredundant clauses 3.9% (113704 remain 81%)
c [simplification-13] maximum reduction of 4% = max (1%, 4%)
c [simplification-13] geometric conflict interval increment 63000 = 315000 / 5
c [simplification-13] new conflict interval 378000
c [simplification-13] penalized conflict interval 378000 = 1 * 378000
c [simplification-13] hard conflict limit 1600058 (soft 1411058 + delta 189000)
c [simplification-13] new conflict limit 1411058 (hard 1600058)
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 -  237.4    4834   113704   1052745   45619   4482  4513   23    36   18  66%   1024    3   24   24   98%
c -  247.9    4834   113704   1102171   46986   4493  4513   24    31   18  78%   1024   -1   25   25   98%
c -  257.7    4834   113704   1148212   47493   4506  4515   25    39   18  65%   1024    6   31   25  127%
c -  269.3    4834   113704   1197322   47402   4518  4515   24    28   27  83%   1024   -6   23   25   93%
c -  281.2    4834   113704   1247707   48112   4524  4515   25    28   27  88%   1024   -5   22   25   88%
c -  293.0    4834   113704   1300610   49198   4531  4515   26    31   27  84%   1024   -2   23   26   90%
c -  305.6    4834   113704   1357334   49653   4536  4515   25    35   27  71%   1024    3   25   26   97%
c 
c [simplification-14] limit 1411058 conflicts (hard 1600058) hit after 1411061 conflicts
c [quatres-12] found 25053 quaternary clauses 28% in total
c [quatres-12-1] removed 5 duplicate quaternary clauses
c [quatres-12-2] added 14 single-self-subsuming ternary resolvents
c [quatres-12-2] added 20 quaternary resolvents
c [ternres-8] limit 144000265 with penalty 0 = 0 + 0
c [ternres-8] all 4834 free variables schedulable
c [ternres-8] 31 ternary resolvents (3 bin, 28 trn)
c [ternres-8] fully completed ternary resolution
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 932 sched 19%, 2 failed, 0 lifted, 79 hbrs
c [decomp-53] removed 2 variables
c [basicprobe-5-1] 934 sched 19%, 1 failed, 0 lifted, 33 hbrs
c [decomp-54] removed 1 variables
c [basicprobe-5-2] 934 sched 19%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-5-3] 934 sched 19%, 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 3 variables, found 120 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 602 transitive binary clauses
c [cce-6] limit of 360000664 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 623 (0%) of length 12
c [cce-6-1] eliminated 3 clauses out of 80 (4%) of length 11
c [cce-6-1] eliminated 633 clauses out of 15997 (4%) of length 6
c [cce-6-1] eliminated 1236 clauses out of 25707 (5%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1873 large clauses in 360001187 steps
c [cce-6-1] allowing another 180000593 steps for small clauses
c [cce-6-1] scheduling 12778 clauses = 9155 binary + 3623 ternary
c [cce-6-1] tried to eliminate 12778 small clauses 100%
c [cce-6-1] eliminated 5 binary clauses 0%
c [cce-6-1] eliminated 119 ternary clauses 3%
c [cce-6-1] eliminated 124 small clauses 1%
c [cce-6-1] eliminated 124 small clauses in 228041385 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 1997 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 65979660 steps for small clauses
c [cce-6-2] scheduling 12654 clauses = 9150 binary + 3504 ternary
c [cce-6-2] tried to eliminate 12654 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 1997 covered clauses in TOTAL during 2 rounds
c [sweep-13] limit 43200079 penalty 0 = 0 + 0
c [sweep-13-1] 1868 pos 54.9% + 1537 neg 45.1% = 3405 sched 70.5% ret 1426
c [sweep-13-1] 15112640 steps 734 queries 29.05 avg class size
c [sweep-13-1] 21407 decisions 745 SAT calls 62.34 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-56] removed 26 variables
c [sweep-13-1] removed 26 vars (0 failed, 33 eqs, 1 impls)
c [sweep-13-2] 2694 pos 56.1% + 2111 neg 43.9% = 4805 sched 100.0% ret 0
c [sweep-13-2] 15867644 steps 753 queries 33.92 avg class size
c [sweep-13-2] 21822 decisions 768 SAT calls 63.25 avg env size
c [sweep-13-2] fully completed sweeping round
c [decomp-57] removed 17 variables
c [sweep-13-2] removed 17 vars (0 failed, 33 eqs, 1 impls)
c [sweep-13-3] 2681 pos 56.0% + 2107 neg 44.0% = 4788 sched 100.0% ret 0
c [sweep-13-3] 12410417 steps 304 queries 85.00 avg class size
c [sweep-13-3] 11059 decisions 307 SAT calls 81.19 avg env size
c [sweep-13-3] 1276 variables remain 27% (3512 retained 73%)
c [decomp-58] removed 7 variables
c [sweep-13-3] removed 7 vars (0 failed, 11 eqs, 0 impls)
c [sweep-13] removed 50 vars in TOTAL (3 rounds, 1788 queries)
c [sort-queue-14] sorted 1299 enqueued variables after 1411061 conflicts
c [score-dist-14] active 3482 (73%), one 0 (0%), zero 1299 (27%)
c [score-dist-14] max exp 541, different 35 (6%)
c [score-dist-14] median active exp 530, avg 529.7
c [simplification-14] removed 53 variables 1.1% (4781 remain 52%)
c [simplification-14] removed 2956 irredundant clauses 2.6% (110748 remain 79%)
c [simplification-14] maximum reduction of 3% = max (1%, 3%)
c [simplification-14] geometric conflict interval increment 94500 = 378000 / 4
c [simplification-14] new conflict interval 472500
c [simplification-14] penalized conflict interval 472500 = 1 * 472500
c [simplification-14] hard conflict limit 2119811 (soft 1883561 + delta 236250)
c [simplification-14] new conflict limit 1883561 (hard 2119811)
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 -  324.2    4781   110748   1411061   51880   4698  4093   25    35   14  70%   1024    3   26   25  102%
c -  335.4    4781   110748   1463253   51679   4703  4093   23    33   19  71%   1024    0   24   25   96%
c -  347.8    4781   110748   1516455   52516   4709  4094   25    32   20  79%   1024   -2   25   25  100%
c -  361.0    4781   110748   1573122   51177   4716  4094   24    29   19  82%   1024   -3   22   24   91%
c -  374.8    4781   110748   1632026   54532   4722  4094   22    30   29  73%   1024    1   22   23   96%
c -  387.8    4781   110748   1689358   54899   4726  4095   22    25   29  88%   1024   -3   22   22   98%
c -  399.7    4781   110748   1743497   55476   4735  4095   21    28   29  76%   1024   -0   21   22   95%
c -  413.0    4781   110748   1799301   55804   4750  4098   22    29   30  77%   1024    1   23   22  108%
c -  426.5    4781   110748   1858492   56684   4757  4101   23    29   30  79%   1024    1   24   22  109%
c 
c [simplification-15] limit 1883561 conflicts (hard 2119811) hit after 1904200 conflicts
c [quatres-13] found 24533 quaternary clauses 28% in total
c [quatres-13-1] removed 3 duplicate quaternary clauses
c [quatres-13-2] added 22 single-self-subsuming ternary resolvents
c [quatres-13-2] added 34 quaternary resolvents
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 4781 free variables schedulable
c [ternres-9] 29 ternary resolvents (0 bin, 29 trn)
c [ternres-9] fully completed ternary resolution
c [card-5] limit 6339258 penalty 4 = 4 + 0
c [card-5] found 613 at-most-one constraints of average size 3.2
c [card-5] found 98 at-most-two constraints of average size 4.6
c [card-5] using previous limit 6339258 for elimination
c [card-5] 711 out of 711 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [simpleprobe-6] all 4781 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-60] removed 12 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 12 variables, found 1976 hbrs, 0 units
c [unhide-8] limit 2500000 with penalty 3 = 3 + 0
c [unhide-8-11] 0 units, 0 failed, 2150 tauts, 0 hbrs, 104324 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 736 transitive binary clauses
c [cce-7] limit of 1014281393 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 30 clauses out of 6370 (0%) of length 7
c [cce-7-1] eliminated 4528 clauses out of 15313 (30%) of length 6
c [cce-7-1] eliminated 9563 clauses out of 24448 (39%) of length 5
c [cce-7-1] eliminated 8404 clauses out of 21700 (39%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 22525 large clauses in 501736822 steps
c [cce-7-1] allowing another 250868411 steps for small clauses
c [cce-7-1] scheduling 33677 clauses = 9083 binary + 24594 ternary
c [cce-7-1] tried to eliminate 33677 small clauses 100%
c [cce-7-1] eliminated 206 binary clauses 2%
c [cce-7-1] eliminated 1229 ternary clauses 5%
c [cce-7-1] eliminated 1435 small clauses 4%
c [cce-7-1] eliminated 1435 small clauses in 341046015 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 23960 covered clauses in round 1
c [cce-7-2] eliminated 3 clauses out of 2836 (0%) of length 8
c [cce-7-2] eliminated 59 clauses out of 6340 (1%) of length 7
c [cce-7-2] eliminated 83 clauses out of 10785 (1%) of length 6
c [cce-7-2] eliminated 99 clauses out of 14885 (1%) of length 5
c [cce-7-2] eliminated 11 clauses out of 13296 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 255 large clauses in 294561490 steps
c [cce-7-2] allowing another 147280745 steps for small clauses
c [cce-7-2] scheduling 32242 clauses = 8877 binary + 23365 ternary
c [cce-7-2] tried to eliminate 32242 small clauses 100%
c [cce-7-2] eliminated 21 binary clauses 0%
c [cce-7-2] eliminated 44 ternary clauses 0%
c [cce-7-2] eliminated 65 small clauses 0%
c [cce-7-2] eliminated 65 small clauses in 230363561 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 320 covered clauses in round 2
c [cce-7-3] eliminated 27 clauses out of 6281 (0%) of length 7
c [cce-7-3] eliminated 37 clauses out of 10702 (0%) of length 6
c [cce-7-3] eliminated 10 clauses out of 14786 (0%) of length 5
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] eliminated 74 large clauses in 290973160 steps
c [cce-7-3] allowing another 145486580 steps for small clauses
c [cce-7-3] scheduling 32177 clauses = 8856 binary + 23321 ternary
c [cce-7-3] tried to eliminate 32177 small clauses 100%
c [cce-7-3] eliminated 5 binary clauses 0%
c [cce-7-3] eliminated 6 ternary clauses 0%
c [cce-7-3] eliminated 11 small clauses 0%
c [cce-7-3] eliminated 11 small clauses in 227902894 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 85 covered clauses in round 3
c [cce-7] eliminated 24365 covered clauses in TOTAL during 3 rounds
c [bca-9] limit of 10000000 steps and 171842 added (scaled 2)
c [bca-9] 5547 out of 9540 literals actually usable 58%
c [bca-9] added 0 blocked clauses in 107887 steps
c [sweep-14] limit 60856883 penalty 0 = 0 + 0
c [sweep-14-1] 644 pos 50.8% + 623 neg 49.2% = 1267 sched 26.6% ret 3502
c [sweep-14-1] 6156386 steps 460 queries 14.34 avg class size
c [sweep-14-1] 11668 decisions 461 SAT calls 59.48 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-61] removed 2 variables
c [sweep-14-1] removed 2 vars (0 failed, 2 eqs, 0 impls)
c [sweep-14-2] 2660 pos 55.8% + 2107 neg 44.2% = 4767 sched 100.0% ret 0
c [sweep-14-2] 16629566 steps 766 queries 31.59 avg class size
c [sweep-14-2] 20669 decisions 769 SAT calls 62.35 avg env size
c [sweep-14-2] fully completed sweeping round
c [sweep-14-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-14-3] 2660 pos 55.8% + 2107 neg 44.2% = 4767 sched 100.0% ret 0
c [sweep-14-3] 15845746 steps 725 queries 27.24 avg class size
c [sweep-14-3] 20220 decisions 725 SAT calls 63.56 avg env size
c [sweep-14-3] fully completed sweeping round
c [decomp-63] removed 5 variables
c [sweep-14-3] removed 5 vars (0 failed, 4 eqs, 0 impls)
c [sweep-14] removed 7 vars in TOTAL (3 rounds, 1948 queries)
c [sort-queue-15] sorted 1197 enqueued variables after 1904200 conflicts
c [score-dist-15] active 3565 (75%), one 0 (0%), zero 1197 (25%)
c [score-dist-15] max exp 542, different 34 (6%)
c [score-dist-15] median active exp 530, avg 530.1
c [simplification-15] removed 19 variables 0.4% (4762 remain 52%)
c [simplification-15] removed 25125 irredundant clauses 22.7% (85623 remain 61%)
c [simplification-15] maximum reduction of 23% = max (0%, 23%)
c [simplification-15] large reduction 23% >= 5% limit
c [simplification-15] next conflict interval 19042 = min (1904200/100, 472500)
c [simplification-15] penalized conflict interval 19042 = 1 * 19042
c [simplification-15] hard conflict limit 1933242 (soft 1923242 + delta 10000)
c [simplification-15] new conflict limit 1923242 (hard 1933242)
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 -  454.5    4762    85623   1913995   57141   5959  3773   22    25   19  88%   1024   -2   22   22   99%
c 
c [simplification-16] limit 1923242 conflicts (hard 1933242) hit after 1923441 conflicts
c [quatres-14] found 15673 quaternary clauses 24% in total
c [quatres-14-1] removed 4 duplicate quaternary clauses
c [quatres-14-1] added 1 double-self-subsuming ternary resolvents
c [quatres-14-2] added 23 single-self-subsuming ternary resolvents
c [quatres-14-2] added 52 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 4762 free variables schedulable
c [ternres-10] 37 ternary resolvents (1 bin, 36 trn)
c [ternres-10] fully completed ternary resolution
c [treelook-6] limit 20508974 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 9413 literals 99%
c [treelook-6] scheduling used 394840 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 20508974 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 11732891 steps
c [treelook-6] fully completed tree based probing
c [treelook-6] removed 0 variables, found 303 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 395 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 4762 variables 100%
c [block-5] limit of 50000000 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 1 blocked clauses
c [block-5] 1 < 1/100 * 85612 = 856 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 10254487100 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 8 clauses out of 2833 (0%) of length 8
c [cce-8-1] eliminated 3 clauses out of 6252 (0%) of length 7
c [cce-8-1] eliminated 5 clauses out of 10663 (0%) of length 6
c [cce-8-1] eliminated 10 clauses out of 14770 (0%) of length 5
c [cce-8-1] eliminated 6 clauses out of 13289 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 32 large clauses in 280183636 steps
c [cce-8-1] allowing another 140091818 steps for small clauses
c [cce-8-1] scheduling 12537 clauses = 8856 binary + 3681 ternary
c [cce-8-1] tried to eliminate 12537 small clauses 100%
c [cce-8-1] eliminated 4 ternary clauses 0%
c [cce-8-1] eliminated 4 small clauses 0%
c [cce-8-1] eliminated 4 small clauses in 173561471 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 36 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 139971482 steps for small clauses
c [cce-8-2] scheduling 12533 clauses = 8856 binary + 3677 ternary
c [cce-8-2] tried to eliminate 12533 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 36 covered clauses in TOTAL during 2 rounds
c [cce-8] 36 < 1/100 * 85611 = 856 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 4752 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 53 not tried 1% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 70 = 1% variables out of 4752 scheduled
c [sweep-15] limit 61526922 penalty 0 = 0 + 0
c [sweep-15-1] 2640 pos 56.4% + 2042 neg 43.6% = 4682 sched 100.0% ret 0
c [sweep-15-1] 11393548 steps 726 queries 21.97 avg class size
c [sweep-15-1] 18957 decisions 727 SAT calls 58.32 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-66] removed 1 variables
c [sweep-15-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-15-2] 2640 pos 56.4% + 2041 neg 43.6% = 4681 sched 100.0% ret 0
c [sweep-15-2] 10314121 steps 712 queries 33.68 avg class size
c [sweep-15-2] 18709 decisions 713 SAT calls 59.35 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-67] removed 2 variables
c [sweep-15-2] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-15-3] 2638 pos 56.4% + 2041 neg 43.6% = 4679 sched 100.0% ret 0
c [sweep-15-3] 12235262 steps 724 queries 34.23 avg class size
c [sweep-15-3] 19047 decisions 724 SAT calls 58.70 avg env size
c [sweep-15-3] fully completed sweeping round
c [sweep-15-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15] 3 < 1/1000 * 4682 = 4 considered unsuccessful
c [sweep-15] removed 3 vars in TOTAL (3 rounds, 2159 queries)
c [sort-queue-16] sorted 1094 enqueued variables after 1923441 conflicts
c [score-dist-16] active 3585 (77%), one 0 (0%), zero 1094 (23%)
c [score-dist-16] max exp 542, different 34 (6%)
c [score-dist-16] median active exp 529, avg 530.1
c [simplification-16] removed 83 variables 1.7% (4679 remain 51%)
c [simplification-16] removed 767 irredundant clauses 0.9% (84856 remain 60%)
c [simplification-16] maximum reduction of 2% = max (2%, 1%)
c [simplification-16] geometric conflict interval increment 157500 = 472500 / 3
c [simplification-16] new conflict interval 630000
c [simplification-16] penalized conflict interval 630000 = 1 * 630000
c [simplification-16] hard conflict limit 2868441 (soft 2553441 + delta 315000)
c [simplification-16] new conflict limit 2553441 (hard 2868441)
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 -  477.0    4679    84856   1984474   56598   5693  3518   23    30   24  77%   1024    1   22   22  101%
c -  489.8    4679    84856   2046887   57539   5698  3518   25    30   24  83%   1024    1   27   23  118%
c -  503.7    4679    84856   2113014   57467   5699  3518   22    26   24  85%   1024   -1   22   23   96%
c -  519.5    4679    84856   2184165   57557   5700  3520   21    25   24  81%   1024   -1   19   22   84%
c -  534.1    4679    84856   2252616   59069   5705  3521   22    24   24  90%   1024   -2   22   22  103%
c -  548.9    4679    84856   2320051   60389   5705  3521   22    24   24  90%   1024   -1   22   22  103%
c -  563.1    4679    84856   2386758   60180   5709  3521   23    27   24  83%   1024    2   23   22  109%
c -  579.0    4679    84856   2455268   60807   5713  3521   20    25   24  80%   1024    1   21   21  102%
c -  594.6    4679    84856   2524072   61371   5725  3521   21    25   24  86%   1024   -1   21   21   98%
c 
c [simplification-17] limit 2553441 conflicts (hard 2868441) hit after 2594212 conflicts
c [quatres-15] found 15615 quaternary clauses 24% in total
c [quatres-15-1] added 2 double-self-subsuming ternary resolvents
c [quatres-15-2] added 19 single-self-subsuming ternary resolvents
c [quatres-15-2] added 41 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 4679 free variables schedulable
c [ternres-11] 60 ternary resolvents (1 bin, 59 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] extracted 392 xors of average arity 3.0
c [gauss-5] connected 1176 occurrences of 381 variables (average 3.1)
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 916 sched 20%, 2 failed, 0 lifted, 65 hbrs
c [decomp-70] removed 2 variables
c [basicprobe-6-1] 914 sched 20%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-2] 914 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-2] fully completed probing
c [basicprobe-6-2] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-6-2] removed 2 variables, found 66 hbrs
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 176 transitive binary clauses
c [sort-queue-17] sorted 1094 enqueued variables after 2594212 conflicts
c [score-dist-17] active 3583 (77%), one 0 (0%), zero 1094 (23%)
c [score-dist-17] max exp 543, different 35 (6%)
c [score-dist-17] median active exp 529, avg 530.3
c [simplification-17] removed 2 variables 0.0% (4677 remain 51%)
c [simplification-17] removed 17 irredundant clauses 0.0% (84839 remain 60%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 630000
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] hard conflict limit 4094212 (soft 3594212 + delta 500000)
c [simplification-17] new conflict limit 3594212 (hard 4094212)
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 -  611.8    4677    84839   2596747   62482   5805  3380   21    27   19  77%   1024    3   20   21   97%
c -  629.2    4677    84839   2667195   61810   5809  3380   19    23   20  85%   1024   -2   19   21   93%
c -  643.3    4677    84839   2732934   63513   5822  3380   22    26   20  86%   1024   -1   22   22  101%
c -  658.1    4677    84839   2800134   64165   5831  3380   21    25   29  86%   1024   -1   21   21   97%
c -  673.1    4677    84839   2867297   65352   5834  3380   21    26   29  82%   1024    0   19   21   90%
c -  688.9    4677    84839   2934936   65080   5840  3381   19    21   29  89%   1024   -3   19   20   94%
c -  705.0    4677    84839   3003778   66934   5861  3381   19    25   29  78%   1024   -0   17   20   83%
c -  719.5    4677    84839   3070346   68504   5898  3381   20    26   29  79%   1024   -1   21   20  104%
c -  734.3    4677    84839   3135025   69375   5942  3381   23    36   29  64%   1024    7   23   21  112%
c -  751.2    4677    84839   3202471   69689   5957  3381   24    31   29  77%   1024    2   24   22  112%
c -  767.1    4677    84839   3268719   69410   5973  3381   22    26   29  83%   1024   -4   22   22  101%
c -  784.0    4677    84839   3338458   70437   5982  3381   21    25   30  84%   1024   -3   20   22   93%
c -  800.4    4677    84839   3409955   71202   5989  3382   22    28   30  78%   1024    1   21   22   96%
c -  817.0    4677    84839   3480544   72365   5992  3383   23    29   30  79%   1024    1   23   22  104%
c -  833.5    4677    84839   3553147   70944   5996  3385   19    30   30  66%   1024    3   19   21   90%
c 
c [simplification-18] limit 3594212 conflicts (hard 4094212) hit after 3629184 conflicts
c [quatres-16] found 16108 quaternary clauses 23% in total
c [quatres-16-1] added 1 double-self-subsuming ternary resolvents
c [quatres-16-2] added 14 single-self-subsuming ternary resolvents
c [quatres-16-2] added 10 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 4677 free variables schedulable
c [ternres-12] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-12] fully completed ternary resolution
c [simpleprobe-7] all 4677 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 0 variables, found 1963 hbrs, 0 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1232 transitive binary clauses
c [cce-9] limit of 1059731709 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 622 (0%) of length 12
c [cce-9-1] eliminated 1 clauses out of 78 (1%) of length 11
c [cce-9-1] eliminated 1 clauses out of 2824 (0%) of length 8
c [cce-9-1] eliminated 8 clauses out of 6258 (0%) of length 7
c [cce-9-1] eliminated 29 clauses out of 10698 (0%) of length 6
c [cce-9-1] eliminated 9 clauses out of 15375 (0%) of length 5
c [cce-9-1] eliminated 18 clauses out of 13010 (0%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 67 large clauses in 292150507 steps
c [cce-9-1] allowing another 146075253 steps for small clauses
c [cce-9-1] scheduling 12175 clauses = 8778 binary + 3397 ternary
c [cce-9-1] tried to eliminate 12175 small clauses 100%
c [cce-9-1] eliminated 6 binary clauses 0%
c [cce-9-1] eliminated 530 ternary clauses 16%
c [cce-9-1] eliminated 536 small clauses 4%
c [cce-9-1] eliminated 536 small clauses in 178976469 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 603 covered clauses in round 1
c [cce-9-2] eliminated 29 clauses out of 6250 (0%) of length 7
c [cce-9-2] eliminated 37 clauses out of 10669 (0%) of length 6
c [cce-9-2] eliminated 10 clauses out of 15366 (0%) of length 5
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 76 large clauses in 289691085 steps
c [cce-9-2] allowing another 144845542 steps for small clauses
c [cce-9-2] scheduling 11639 clauses = 8772 binary + 2867 ternary
c [cce-9-2] tried to eliminate 11639 small clauses 100%
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 76 covered clauses in round 2
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] allowing another 144311825 steps for small clauses
c [cce-9-3] scheduling 11639 clauses = 8772 binary + 2867 ternary
c [cce-9-3] tried to eliminate 11639 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 0 covered clauses in round 3
c [cce-9] eliminated 679 covered clauses in TOTAL during 3 rounds
c [cce-9] 679 < 1/100 * 84839 = 848 considered unsuccessful
c [elim-8] 53 variables 1% will be scheduled this time
c [elim-8] scheduled 53 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 47634689 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 53 scheduled
c [bca-10] limit of 10000000 steps and 168892 added (scaled 2)
c [bca-10] 5252 out of 9356 literals actually usable 56%
c [bca-10] added 0 blocked clauses in 146382 steps
c [sweep-16] limit 63583902 penalty 1 = 1 + 0
c [sweep-16-1] 2609 pos 55.8% + 2068 neg 44.2% = 4677 sched 100.0% ret 0
c [sweep-16-1] 24762895 steps 705 queries 20.45 avg class size
c [sweep-16-1] 20352 decisions 705 SAT calls 64.77 avg env size
c [sweep-16-1] fully completed sweeping round
c [sweep-16-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-16-2] 2609 pos 55.8% + 2068 neg 44.2% = 4677 sched 100.0% ret 0
c [sweep-16-2] 22590811 steps 719 queries 17.95 avg class size
c [sweep-16-2] 20570 decisions 718 SAT calls 62.92 avg env size
c [sweep-16-2] fully completed sweeping round
c [sweep-16-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-16-3] 2609 pos 55.8% + 2068 neg 44.2% = 4677 sched 100.0% ret 0
c [sweep-16-3] 16231634 steps 396 queries 51.01 avg class size
c [sweep-16-3] 12679 decisions 396 SAT calls 68.69 avg env size
c [sweep-16-3] 750 variables remain 16% (3927 retained 84%)
c [sweep-16-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-16] removed 0 vars in TOTAL (3 rounds, 1817 queries)
c [sort-queue-18] sorted 1054 enqueued variables after 3629184 conflicts
c [score-dist-18] active 3623 (77%), one 0 (0%), zero 1054 (23%)
c [score-dist-18] max exp 544, different 36 (7%)
c [score-dist-18] median active exp 530, avg 530.9
c [simplification-18] removed 0 variables 0.0% (4677 remain 51%)
c [simplification-18] removed 679 irredundant clauses 0.8% (84160 remain 60%)
c [simplification-18] maximum reduction of 1% = max (0%, 1%)
c [simplification-18] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] hard conflict limit 5129184 (soft 4629184 + delta 500000)
c [simplification-18] new conflict limit 4629184 (hard 5129184)
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 -  864.8    4677    84160   3629184   73724   6603  4160   22    26   16  85%   1024    0   22   21  106%
c -  884.5    4677    84160   3708298   74514   6610  4160   20    23   22  88%   1024   -1   21   20  104%
c -  903.3    4677    84160   3785824   74736   6618  4160   21    24   33  88%   1024   -1   21   21   98%
c -  922.9    4677    84160   3866701   74026   6621  4160   19    27   33  72%   1024    3   20   20   99%
c -  944.7    4677    84160   3951086   75779   6628  4160   18    23   33  79%   1024   -1   18   19   92%
c -  962.8    4677    84160   4029396   75703   6633  4160   20    23   33  88%   1024   -1   20   20  100%
c -  984.8    4677    84160   4114868   76862   6635  4160   20    24   33  83%   1024    1   19   20   97%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 303 basic ate = 107 trn 35% + 196 lrg 65% in 3 updates
c bcas: 10 count, 144 added (257 skipped), 669536 steps
c bkwd: tried 37199 clauses, 74029 lits, 1.99 lits/clause
c bkwd: checked 5644542 occs, 151.74 occs/clause, 76.25 occs/lit
c bkwd: subsumed 0 binary, 4 ternary, 162 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 272 large (0% self)
c blkd: 5 bces, 1882 removed, 2803716 resolutions, 9014885 steps
c blkd: 3038 blocking literals 16%, 26 pure
c bump: 4216568 bumped seen, 403867116 lits 95.8 on average
c card: 5 count, 0 units, 0 am1, 19578024 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 13009 subsumed
c card: 4534 at-most-one constraints found, average size 3.10
c card: 4534 at-most-one constraints used 100%, average size 3.10
c card: 357 at-most-two constraints found, average size 4.67
c card: 357 at-most-two constraints used 100%, average size 4.67
c cces: 9 cces, 35525 eliminated, 10331 ate 29%, 25194 abce 71%
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: 94 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 76 decompositions, 1711 equivalent 18%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 6469906 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 2527 eliminated 26%, 447 pure 18%
c elms: 11 rounds, 1.4 rounds/bve
c elms: 1571 small 62%, 483 large 19%
c elms: 3296 tried small, 1571 succeeded 48%, 1725 failed 52%
c elms: 3471 subsumed, 659 strengthened, 427 blocked
c elms: 1849522 copies, 2465622 resolutions, 114449 ipos
c elms: 5556656 subchks, 861827 strchks
c gaus: 5 extractions, 1488 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 17206166 steps, 8603083 extr 50%, 84737 elim 0%
c glue: 22.8 orig avg, 22.8 real avg, 4.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 20323 = 12071 simple 59% + 7106 trn 35% + 1146 lrg 6%, 447 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4216568 clauses, 39.7 length
c lrnd: 167529226 lits = 269435137 orig - 101905911 removed 38%
c lrnd: 1024685 uips 24%, 2653729 flips 63%
c mins: 4210049 mins 100%, 331 bin 0%, 6188 size 0%
c mins: 157936746 poisoned searches, 28673127 hits, 18% hit rate
c mins: 394449343 used twice searches, 59996350 hits, 15% hit rate
c move: moved 7581, 1277 bin 17%, 6304 trn 83%
c otfs: 6977 driving 23%, 22733 restarting 77%
c otfs: str 29710, 29415 red 99%, 295 irr 1%
c otfs: str 29710, 0 bin 0%, 308 trn 1%, 29402 lrg 99%
c otfs: sub 333, 333 red 100%, 0 irr 0%
c otfs: sub 333, 0 bin 0%, 24 trn 7%, 309 lrg 93%
c phas: 8 computed, 5945 set, 3368 pos (57%), 2577 neg (43%)
c prbs: 6 basic, 34683 probed, 37 failed, 0 lifted
c prbs: 7 simple, 49278 probed, 13 failed, 326 eqs
c prbs: 6 treelook, 12256 probed, 2 failed, 0 lifted
c prom: 308105 locked 6% out of 4992440 tried
c prps: 1397737734 props, 215 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 16 count, 314 quat, 151 self1, 6 self2, 2717 dup
c queu: 18 sorted, 6469906 next (494141 steps 0.08)
c queu: 403922102 enq (504046355 steps 1.25), 403867116 deq 100%
c redc: 4132 clauses 6%, 70026 tried 2%, 4 sat 0%
c redc: 4630 lits 1%, 744652 tried 0%, 4 sat 0%
c redc: 183 times jump level reduced, 4.8 levels on average
c reds: 73 count, 57281.4 conflicts per reduce
c reds: 0 memlim 0%, 73 arith 100%
c reds: 3142511 collected 92%, 282965 retired 8%
c rmbd: 738 removed, 304 red 41%
c rsts: 16581 restarts 98%, 314 skipped 2%
c rsts: 314 saturating 100%, 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: 18 count, 18 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 4216568 count (4172225 tried 1.0), 636231 sub out of 4212896 (15.1%)
c swps: 16 count, 32 rounds, 15532 queries (485.4/round)
c swps: 15663 sat calls, 583 unsat (2.7% success rate)
c swps: 440985 decisions 28.2, 42003 conflicts 2.7
c swps; 41.0 avg class size, 63.1 avg environment size
c swps: 0 failed, 55 impls, 445 equivs
c swp0: 5168 type 0 queries, 2154 unsat (41.7%), 5054 sat (97.8%)
c swp1: 10364 type 1 queries, 5162 unsat (49.8%), 10033 sat (96.8%)
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: 21373345 calls to obtain time
c tops: 654 fixed 7%, 1 its, 4181542.00 confs/it
c trds: 16 transitive reductions, 9024 removed, 1 failed
c trds: 154632 nodes, 200506 edges, 4655645 steps
c trim: 2927289 words, 11.2 MB
c trnr: 12 count, 10 bin, 321 trn, 64420863 steps
c unhd: 8 count, 11 rounds, 18565935 steps
c unhd: 464 non-trivial sccs of average size 2.0
c unhd: 3 units, 3 bin, 0 trn, 0 lrg
c unhd: 20 failed, 20 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 7824 tauts, 723 bin 9%, 654 trn 8%, 1230 lrg 16%
c unhd: 7824 tauts, 5217 stamp 67%, 6129 red 78%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 294927 str, 3 bin 0%, 204 trn 0%, 294720 lrg 100%, 294680 red 100%
c vars: 4677 remaining 49% and 4892 removed 51% out of 9569
c vars: 654 fixed 7%, 2527 eliminated 26%, 1711 equivalent 18%
c vsts: 50691841122 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 36.3 search visits per propagation, 12045.6 per conflict
c wchs: 10659423541 pushed, 13561741 enlarged, 188 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4213210       3142511        282965     139529476      50019803       2473365
c 
c  0 0         28857   1       876   0         0   0  62724361  45  14918217  30    492387  20     0.8
c  1 5         18943   0      3823   0     10810   4  12670301   9   3819287   8    150736   6     0.1
c  2 6         96929   2     42811   1     37687  13  23716610  17<  8030064  16<   383894  16     1.0
c  3 9        323561   8    236283   8     44245  16  20022677  14   9406747  19    590445  24<    2.6
c  4 14      1086565  26    865597  28     69518  25< 12988206   9   8255134  17    551714  22     7.7
c  5 21      1994866  47<  1470131  47<    96957  34   5930267   4   4452934   9    246277  10     9.7
c  6 30       548968  13    427546  14     19845   7   1204551   1    945218   2     48042   2     6.1
c  7 41        99163   2     82427   3      3431   1    239457   0    170187   0      8879   0     5.2
c  8 54        15079   0     12784   0       463   0     32437   0     21696   0       980   0     2.4
c  9 69          278   0       232   0         9   0       606   0       318   0        11   0     0.1
c 10 86            1   0         1   0         0   0         3   0         1   0         0   0     0.0
c 
c avg                  4.7           4.7           4.0           1.5           2.2           2.6
c std                  1.1           1.0           1.3           1.7           1.8           1.7
c 
c   38.037   4% bump
c   33.932   3% cce
c   15.229   2% sweep
c    6.366   1% probe
c    6.325   1% elim
c 
c   11.948 < 1% rest (below)
c 
c    3.787   0% decide
c    3.596   0% unhide
c    1.886   0% quatres
c    0.650   0% block
c    0.609   0% bca
c    0.434   0% transred
c    0.377   0% gauss
c    0.367   0% ternres
c    0.241   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.806   0% preprocessing     1%
c   71.511   7% inprocessing     99%
c ==================================
c   72.316   7% simplifying
c  927.651  93% search
c ==================================
c  999.967 100% all
c 
c       4181542 conflicts,        4181.7 confs/sec
c          1006 ternaries,        4156.6 confs/ternary
c            84 binaries,        49780.3 confs/binary
c             1 iterations,    4181542.0 confs/iteration
c 
c            73 reductions,          0.1 redus/sec,  57281.4 confs/reduction
c         16581 restarts,           16.6 rests/sec,    252.2 confs/restart
c       6469906 decisions,        6470.1 decis/sec,      1.5 decis/conflict
c    1397737734 propagations,  1397783.7 props/sec,    216.0 props/decision
c 
c 1000.0 seconds, 53.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
