c launch: /data/cnf/sc2014/app/velev-vliw-uns-4.0-9-i1.cnf.bz2
c host: atom30
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/velev-vliw-uns-4.0-9-i1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/velev-vliw-uns-4.0-9-i1.cnf.bz2
c no embedded options
c found 'p cnf 154309 3230738' header
c read 154309 variables, 3230738 clauses, 9429252 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 --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 --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 154308 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 [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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  154308  3230737         0       0      0     0    0     0   88   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 807684 based on 3230737 irredundant clauses
c [card-1] found 2 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 807684 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 4 variables
c [simpleprobe-1] all 154305 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 6461414 based on 3230707 irredundant clauses
c [decomp-2] removed 15 variables
c [simpleprobe-1] 133497 variables remain 87% (20793 retained 13%)
c [simpleprobe-1] removed 15 variables, found 379 hbrs, 15 units
c [unhide-1] limit 201889 based on 3230232 irredundant clauses
c [unhide-1-1] 1379 units, 2 failed, 2682 tauts, 0 hbrs, 8782 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 152909 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 148955 not tried 97% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 3729 = 2% variables out of 152909 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3198917 negative 100.0% of 3199455 except 538 0.0%
c [phase-count-1] 1874450 positive 58.6% of 3199455 except 1325005 41.4%
c [phase-count-1] less non-negative clauses 538 than limit 319900 (10.0%)
c [phase-count-1] non-pos/non-neg = 1325005/538 = 2462.83 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 149180 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 149180 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 149180 variables
c [simplification-1] removed 5125 variables 3.3% (149180 remain 97%)
c [simplification-1] removed 31282 irredundant clauses 1.0% (3199455 remain 99%)
c [simplification-1] maximum reduction of 3% = max (3%, 1%)
c [simplification-1] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-1] new conflict interval 5000
c [simplification-1] penalized conflict interval 5000 = 1 * 5000
c [simplification-1] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-1] new conflict limit 5000 (hard 15000)
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 1 variables
c [simpleprobe-2] 129070 schedulable variables 87%
c [simpleprobe-2] limit 6398906 based on 3199453 irredundant clauses
c [simpleprobe-2] 127408 variables remain 85% (21771 retained 15%)
c [simpleprobe-2] removed 0 variables, found 3622 hbrs, 0 units
c [treelook-1] limit 799863 based on 3199453 irredundant clauses
c [treelook-1] scheduled 106908 literals 36%
c [treelook-1] scheduling used 802307 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 799863 based on 3199453 irredundant clauses
c [treelook-1] used 1123460 steps
c [treelook-1] 106017 literals remain 36%
c [treelook-1] 105126 variables remain to probed next time 71%
c [treelook-1] removed 875 variables, found 115 hbrs
c [basicprobe-1] limit 25435224 based on 3179403 irredundant clauses
c [basicprobe-1-0] 141726 probes remain 96% after last round
c [basicprobe-1-0] 28 units = 28 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 28 variables, found 18821 hbrs
c [unhide-2] limit 198712 based on 3179403 irredundant clauses
c [unhide-2-2] 86 units, 1 failed, 21 tauts, 0 hbrs, 61283 literals
c [elim-2] 147964 variables 100% will be scheduled this time
c [elim-2] scheduled 147964 variables 100%
c [elim-2] limit of 11670621 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 141276 not tried 95% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 5444 = 4% variables out of 147964 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3165256 negative 100.0% of 3165792 except 536 0.0%
c [phase-count-2] 1859552 positive 58.7% of 3165792 except 1306240 41.3%
c [phase-count-2] less non-negative clauses 536 than limit 316500 (10.0%)
c [phase-count-2] non-pos/non-neg = 1306240/536 = 2437.01 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 42 negative 100%
c [score-distribution-2] 18967 pos 13.29%, 0 min 0.00%, 123778 zero 86.71%
c [score-distribution-2] 3614 different 2.53% out of total 142745 variables
c [simplification-2] removed 6435 variables 4.3% (142745 remain 93%)
c [simplification-2] removed 33663 irredundant clauses 1.1% (3165792 remain 98%)
c [simplification-2] maximum reduction of 4% = max (4%, 1%)
c [simplification-2] forced so keeping old conflict interval 5000
c [simplification-2] conflict limit remains at 5000 (hard 15000)
c [simplification-2] new binary interval 1000
c 
c [simplification-3] limit 5000 conflicts (hard 15000) hit after 5000 conflicts
c [card-2] limit 791448 based on 3165792 irredundant clauses
c [card-2] found 5 at-most-one constraints of average size 3.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 791448 for elimination
c [card-2] 5 out of 5 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 4 variables
c [treelook-2] limit 791446 based on 3165784 irredundant clauses
c [treelook-2] scheduled 106462 literals 37%
c [treelook-2] scheduling used 791601 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 791446 based on 3165784 irredundant clauses
c [treelook-2] used 3501406 steps
c [treelook-2] 106457 literals remain 37%
c [treelook-2] 98137 variables remain to probed next time 69%
c [treelook-2] removed 1 variables, found 554 hbrs
c [unhide-3] limit 197859 based on 3165757 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 547 tauts, 0 hbrs, 3683 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 142739 variables 100%
c [elim-3] limit of 18554737 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 130791 not tried 92% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 4228 = 3% variables out of 142739 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3155469 negative 100.0% of 3155996 except 527 0.0%
c [phase-count-3] 1857728 positive 58.9% of 3155996 except 1298268 41.1%
c [phase-count-3] less non-negative clauses 527 than limit 315500 (10.0%)
c [phase-count-3] non-pos/non-neg = 1298268/527 = 2463.51 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 18 negative 100%
c [score-distribution-3] 15232 pos 11.00%, 6723 min 4.85%, 116556 zero 84.15%
c [score-distribution-3] 3397 different 2.45% out of total 138511 variables
c [simplification-3] removed 4234 variables 3.0% (138511 remain 90%)
c [simplification-3] removed 9796 irredundant clauses 0.3% (3155996 remain 98%)
c [simplification-3] maximum reduction of 3% = max (3%, 0%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 25000 (soft 15000 + delta 10000)
c [simplification-3] new conflict limit 15000 (hard 25000)
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   46.5  138510  3155996     10955    8926    392 15805   14   560  144   2%    144  492   15    2  707%
c 
c [simplification-4] limit 15000 conflicts (hard 25000) hit after 15001 conflicts
c [decomp-8] removed 7 variables
c [basicprobe-2] limit 25247544 based on 3155943 irredundant clauses
c [basicprobe-2-0] 128188 probes remain 93% after last round
c [basicprobe-2-0] 34 units = 34 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 34 variables, found 9515 hbrs
c [unhide-4] limit 252904 with penalty 3 = 0 + 3
c [unhide-4-4] 2008 units, 6 failed, 308 tauts, 0 hbrs, 76965 literals
c [elim-4] 127716 variables 95% will be scheduled this time
c [elim-4] scheduled 127716 variables 95%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1011616720 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 1687 not tried 1% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 7896 = 6% variables out of 127716 scheduled
c [elim-4] considered successful since not run to completion yet
c [score-distribution-4] 18299 pos 14.39%, 14462 min 11.37%, 94436 zero 74.24%
c [score-distribution-4] 4359 different 3.43% out of total 127197 variables
c [simplification-4] removed 11313 variables 8.2% (127197 remain 82%)
c [simplification-4] removed 86260 irredundant clauses 2.7% (3069736 remain 95%)
c [simplification-4] maximum reduction of 8% = max (8%, 3%)
c [simplification-4] large reduction 8% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 27001 (soft 17001 + delta 10000)
c [simplification-4] new conflict limit 17001 (hard 27001)
c 
c [simplification-5] limit 17001 conflicts (hard 27001) hit after 17001 conflicts
c [quatres-1] found 28342 quaternary clauses 19% in total
c [quatres-1-2] added 1050 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1768 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 13938480 with penalty 2 = 0 + 2
c [ternres-1] all 127197 free variables schedulable
c [ternres-1] 1666 ternary resolvents (0 bin, 1666 trn)
c [ternres-1] 122570 variables remain 96% (4627 retained 4%)
c [gauss-1] limit 1534867 based on 3069735 irredundant clauses
c [gauss-1] extracted 5 xors of average arity 2.0
c [gauss-1] connected 10 occurrences of 10 variables (average 1.0)
c [gauss-1] limit 1534867 based on 3069735 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 216 variables
c [unhide-5] limit 278769 with penalty 3 = 0 + 3
c [unhide-5-5] 3 units, 0 failed, 16150 tauts, 0 hbrs, 12086 literals
c [transred-1] limit 3052791 based on 3052791 irredundant clauses
c [transred-1] removed 1 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 126978 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 278769622 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 173774 blocked clauses
c [cce-1] limit of 27876962 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 2904
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 2443
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 2081
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 2046
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 2028
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 1730
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 1717
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 796
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 732
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 705
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 703
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 669
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 650
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 630
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 550
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 540
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 532
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 520
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 516
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 505
c [cce-1-1] eliminated 1 clauses out of 4 (25%) of length 503
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 424
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 414
c [cce-1-1] eliminated 9 clauses out of 9 (100%) of length 399
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 394
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 385
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 382
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 357
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 341
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 334
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 329
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 320
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 314
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 307
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 294
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 272
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 260
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 258
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 250
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 236
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 231
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 227
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 226
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 222
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 58 large clauses in 27876966 steps
c [cce-1-1] allowing another 13938483 steps for small clauses
c [cce-1-1] scheduling 1666166 clauses = 1612353 binary + 53813 ternary
c [cce-1-1] tried to eliminate 77 small clauses 0%
c [cce-1-1] eliminated 15 binary clauses 0%
c [cce-1-1] eliminated 15 small clauses 0%
c [cce-1-1] eliminated 15 small clauses in 27876966 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 73 covered clauses in round 1
c [cce-1] eliminated 73 covered clauses in TOTAL during 1 rounds
c [cce-1] 73 < 1/100 * 2878888 = 28788 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 125715 variables 100%
c [elim-5] limit of 111507849 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 36623 not tried 29% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 8940 = 7% variables out of 125715 scheduled
c [bca-1] limit of 10000000 steps and 5734512 added (scaled 2)
c [bca-1] 210943 out of 233552 literals actually usable 90%
c [bca-1] added 256227 blocked clauses in 895185 steps
c [sweep-1] limit 5734012 based on 2867006 irredundant clauses
c [sweep-1-1] 2205 pos 1.9% + 114570 neg 98.1% = 116775 sched 100.0% ret 0
c [sweep-1-1] 5878930 steps 19 queries 18489.47 avg class size
c [sweep-1-1] 530 decisions 17 SAT calls 244.00 avg env size
c [sweep-1-1] 116616 variables remain 100% (146 retained 0%)
c [decomp-10] removed 46 variables
c [sweep-1-1] removed 46 vars (0 failed, 1 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 46 vars in TOTAL (1 rounds, 18 queries)
c [score-distribution-5] 12005 pos 10.28%, 16743 min 14.34%, 87981 zero 75.37%
c [score-distribution-5] 3999 different 3.43% out of total 116729 variables
c [simplification-5] removed 10468 variables 8.2% (116729 remain 76%)
c [simplification-5] removed 210141 irredundant clauses 6.8% (2859595 remain 89%)
c [simplification-5] maximum reduction of 8% = max (8%, 7%)
c [simplification-5] large reduction 8% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 29001 (soft 19001 + delta 10000)
c [simplification-5] new conflict limit 19001 (hard 29001)
c 
c [simplification-6] limit 19001 conflicts (hard 29001) hit after 19002 conflicts
c [quatres-2] found 28223 quaternary clauses 18% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 26 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1079 quaternary resolvents
c [ternres-2] limit 11438380 based on 2859595 irredundant clauses
c [ternres-2] 112484 schedulable variables 96%
c [ternres-2] 2003 ternary resolvents (0 bin, 2003 trn)
c [ternres-2] 109503 variables remain 94% (7226 retained 6%)
c [card-3] limit 771992 penalty 3 = 2 + 1
c [card-3] found 12 at-most-one constraints of average size 4.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 771992 for elimination
c [card-3] 12 out of 12 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 99628 schedulable variables 85%
c [simpleprobe-3] limit 12351887 penalty 2 = 1 + 1
c [decomp-12] removed 1 variables
c [simpleprobe-3] 100249 variables remain 86% (16479 retained 14%)
c [simpleprobe-3] removed 1 variables, found 6094 hbrs, 1 units
c [unhide-6] limit 308797 with penalty 3 = 0 + 3
c [unhide-6-6] 145 units, 9 failed, 928 tauts, 0 hbrs, 24854 literals
c [transred-2] limit 2859074 based on 2859074 irredundant clauses
c [transred-2] removed 48 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 116571 variables 100%
c [block-2] limit of 61759436 steps penalty 1 = 0 + 1
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 3102 blocked clauses
c [block-2] 3102 < 1/100 * 2859074 = 28590 considered unsuccessful
c [elim-6] 1655 variables 1% will be scheduled this time
c [elim-6] scheduled 1655 variables 1%
c [elim-6] limit of 123518872 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 882 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 1655 scheduled
c [bca-2] limit of 10000000 steps and 5828161 added (scaled 2)
c [bca-2] 208379 out of 233144 literals actually usable 89%
c [bca-2] added 220098 blocked clauses in 1097985 steps
c [sweep-2] limit 5699548 based on 2849774 irredundant clauses
c [sweep-2-1] 2811 pos 2.4% + 113615 neg 97.6% = 116426 sched 99.9% ret 145
c [sweep-2-1] 5709618 steps 24 queries 14663.50 avg class size
c [sweep-2-1] 1296 decisions 22 SAT calls 206.27 avg env size
c [sweep-2-1] 116249 variables remain 100% (322 retained 0%)
c [decomp-13] removed 5 variables
c [sweep-2-1] removed 5 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 5 vars in TOTAL (1 rounds, 23 queries)
c [score-distribution-6] 13792 pos 11.83%, 16304 min 13.99%, 86470 zero 74.18%
c [score-distribution-6] 3961 different 3.40% out of total 116566 variables
c [simplification-6] removed 163 variables 0.1% (116566 remain 76%)
c [simplification-6] removed 10045 irredundant clauses 0.4% (2849550 remain 88%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 20000
c [simplification-6] new conflict interval 30000
c [simplification-6] penalized conflict interval 30000 = 1 * 30000
c [simplification-6] hard conflict limit 64002 (soft 49002 + delta 15000)
c [simplification-6] new conflict limit 49002 (hard 64002)
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  164.8  116565  2849539     28811   24155   6231 501953   17   422  155   4%    221  251   20    6  356%
c 
c [simplification-7] limit 49002 conflicts (hard 64002) hit after 49002 conflicts
c [quatres-3] found 29443 quaternary clauses 19% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 153 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1117 quaternary resolvents
c [ternres-3] limit 14363653 with penalty 1 = 0 + 1
c [ternres-3] 109349 schedulable variables 94%
c [ternres-3] 2062 ternary resolvents (0 bin, 2062 trn)
c [ternres-3] 104878 variables remain 90% (11687 retained 10%)
c [gauss-2] limit 1436365 penalty 2 = 1 + 1
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 4 variables
c [treelook-3] limit 1436365 penalty 1 = 0 + 1 boost 1
c [treelook-3] scheduled 96789 literals 42%
c [treelook-3] scheduling used 1436503 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1436365 penalty 1 = 0 + 1 boost 1
c [treelook-3] used 1736804 steps
c [treelook-3] 96786 literals remain 42%
c [treelook-3] 76571 variables remain to probed next time 66%
c [treelook-3] removed 1 variables, found 1 hbrs
c [unhide-7] limit 718182 with penalty 3 = 0 + 3
c [unhide-7-7] 112 units, 8 failed, 6513 tauts, 0 hbrs, 21136 literals
c [transred-3] limit 2843298 based on 2843298 irredundant clauses
c [transred-3] removed 1 transitive binary clauses
c [cce-2] limit of 35909134 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 2016
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 1058
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 926
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 883
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 861
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 857
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 842
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 727
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 704
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 686
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 659
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 649
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 642
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 641
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 627
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 626
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 616
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 605
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 596
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 578
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 567
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 556
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 541
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 540
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 521
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 516
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 502
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 497
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 489
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 486
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 466
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 457
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 455
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 442
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 428
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 409
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 50 large clauses in 35923475 steps
c [cce-2-1] allowing another 17961737 steps for small clauses
c [cce-2-1] scheduling 1620263 clauses = 1567385 binary + 52878 ternary
c [cce-2-1] tried to eliminate 159 small clauses 0%
c [cce-2-1] eliminated 37 binary clauses 0%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 39 small clauses 0%
c [cce-2-1] eliminated 1707 small clauses in 35909258 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1757 covered clauses in round 1
c [cce-2] eliminated 1757 covered clauses in TOTAL during 1 rounds
c [cce-2] 1757 < 1/100 * 2843298 = 28432 considered unsuccessful
c [bca-3] limit of 10000000 steps and 5921744 added (scaled 2)
c [bca-3] 196067 out of 232884 literals actually usable 84%
c [bca-3] added 55993 blocked clauses in 1099878 steps
c [sweep-3] limit 5683082 based on 2841541 irredundant clauses
c [sweep-3-1] 2521 pos 2.2% + 113600 neg 97.8% = 116121 sched 99.7% ret 320
c [sweep-3-1] 5708562 steps 14 queries 18005.21 avg class size
c [sweep-3-1] 292 decisions 10 SAT calls 304.80 avg env size
c [sweep-3-1] 116075 variables remain 100% (366 retained 0%)
c [decomp-16] removed 12 variables
c [sweep-3-1] removed 12 vars (0 failed, 3 eqs, 7 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 12 vars in TOTAL (1 rounds, 13 queries)
c [score-distribution-7] 14449 pos 12.41%, 23535 min 20.21%, 78445 zero 67.38%
c [score-distribution-7] 3642 different 3.13% out of total 116429 variables
c [simplification-7] removed 136 variables 0.1% (116429 remain 75%)
c [simplification-7] removed 8069 irredundant clauses 0.3% (2841447 remain 88%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 30000
c [simplification-7] new conflict interval 60000
c [simplification-7] penalized conflict interval 60000 = 1 * 60000
c [simplification-7] hard conflict limit 139002 (soft 109002 + delta 30000)
c [simplification-7] new conflict limit 109002 (hard 139002)
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 -  230.7  116429  2841436     66569   19364   9113 542523   20   594  154   3%    414  301   25   11  221%
c i  257.0  116428  2841433     83333   34609   9394 542780   19   560  158   3%    551  206   19   13  143%
c 
c [simplification-8] limit of 2489 ternary hit after 2489 ternaries
c [quatres-4] found 31111 quaternary clauses 19% in total
c [quatres-4-2] added 50 single-self-subsuming ternary resolvents
c [quatres-4-2] added 747 quaternary resolvents
c [ternres-4] limit 28903751 with penalty 1 = 0 + 1
c [ternres-4] 104729 schedulable variables 90%
c [ternres-4] 3199 ternary resolvents (2 bin, 3197 trn)
c [ternres-4] 96051 variables remain 83% (20348 retained 17%)
c [decomp-17] removed 30 variables
c [basicprobe-3] limit 144518759 penalty 1 = 0 + 1
c [basicprobe-3-0] 84456 probes remain 87% after last round
c [basicprobe-3-0] 212 units = 212 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 19470 variables, found 18551 hbrs
c [bate-1] eliminated 13 asymmetric tautologies during probing
c [unhide-8] limit 1445187 with penalty 3 = 0 + 3
c [unhide-8-8] 180 units, 31 failed, 2111 tauts, 0 hbrs, 45070 literals
c [transred-4] limit 2516578 based on 2516578 irredundant clauses
c [transred-4] removed 9 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 96688 variables 100%
c [block-3] limit of 144518759 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 906 blocked clauses
c [block-3] 906 < 1/100 * 2516577 = 25165 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 96680 variables 100%
c [elim-7] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 15024 not tried 16% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2558 = 3% variables out of 96680 scheduled
c [bca-4] limit of 10000000 steps and 5254573 added (scaled 2)
c [bca-4] 145609 out of 188246 literals actually usable 77%
c [bca-4] added 1293 blocked clauses in 547051 steps
c [sweep-4] limit 8671125 penalty 1 = 0 + 1
c [sweep-4-1] 2905 pos 3.1% + 90899 neg 96.9% = 93804 sched 99.7% ret 318
c [sweep-4-1] 8882647 steps 31 queries 9763.77 avg class size
c [sweep-4-1] 1620 decisions 28 SAT calls 272.11 avg env size
c [sweep-4-1] 93398 variables remain 99% (724 retained 1%)
c [decomp-18] removed 398 variables
c [sweep-4-1] removed 398 vars (0 failed, 4 eqs, 6 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 398 vars in TOTAL (1 rounds, 30 queries)
c [score-distribution-8] 15614 pos 16.66%, 29659 min 31.65%, 48451 zero 51.70%
c [score-distribution-8] 4224 different 4.51% out of total 93724 variables
c [simplification-8] removed 22675 variables 19.5% (93724 remain 61%)
c [simplification-8] removed 348293 irredundant clauses 12.3% (2493140 remain 77%)
c [simplification-8] maximum reduction of 19% = max (19%, 12%)
c [simplification-8] forced so keeping old conflict interval 60000
c [simplification-8] conflict limit remains at 109002 (hard 139002)
c [simplification-8] new ternary interval 10000
c 
c [simplification-9] limit 109002 conflicts (hard 139002) hit after 109004 conflicts
c [quatres-5] found 29713 quaternary clauses 22% in total
c [quatres-5-1] removed 2 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 210 single-self-subsuming ternary resolvents
c [quatres-5-2] added 983 quaternary resolvents
c [ternres-5] limit 30339378 with penalty 1 = 0 + 1
c [ternres-5] 77436 schedulable variables 83%
c [ternres-5] 2240 ternary resolvents (0 bin, 2240 trn)
c [ternres-5] 71446 variables remain 76% (22278 retained 24%)
c [simpleprobe-4] 80481 schedulable variables 86%
c [simpleprobe-4] limit 100000000 penalty 1 = 0 + 1
c [decomp-20] removed 139 variables
c [simpleprobe-4] 80667 variables remain 86% (12918 retained 14%)
c [simpleprobe-4] removed 139 variables, found 49299 hbrs, 99 units
c [unhide-9] limit 1516968 with penalty 3 = 0 + 3
c [unhide-9-9] 1142 units, 17 failed, 7297 tauts, 0 hbrs, 14850 literals
c [transred-5] limit 2484057 based on 2484057 irredundant clauses
c [transred-5] removed 11 transitive binary clauses
c [transred-5] found 3 units
c [elim-8] 818 variables 1% will be scheduled this time
c [elim-8] scheduled 818 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8000000000 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2 variables 0% in round 1 in 330617756 steps
c [elim-8-1] backward subsumption/strengthening limit 330617700
c [elim-8-1-1] backward checking 6533 touched variables 7%
c [elim-8-1-1] incomplete backward checking 6798 remain 104%
c [elim-8-1] subsumed 0 and strengthened 216 clauses in 330619101 steps
c [elim-8-1] rescheduled 666 variables 1% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 24411994 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2 = 0% variables out of 818 scheduled
c [elim-8] 2 < 1/100 * 818 = 8 considered unsuccessful
c [bca-5] limit of 10000000 steps and 5195245 added (scaled 2)
c [bca-5] 138984 out of 184850 literals actually usable 75%
c [bca-5] added 509731 blocked clauses in 1068182 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 91018130 penalty 1 = 0 + 1
c [sweep-5-1] 2731 pos 3.0% + 88984 neg 97.0% = 91715 sched 99.2% ret 709
c [sweep-5-1] 91075441 steps 392 queries 1911.22 avg class size
c [sweep-5-1] 13276 decisions 309 SAT calls 203.57 avg env size
c [sweep-5-1] 78701 variables remain 85% (13718 retained 15%)
c [decomp-21] removed 97 variables
c [sweep-5-1] removed 97 vars (0 failed, 89 eqs, 183 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 97 vars in TOTAL (1 rounds, 391 queries)
c [score-distribution-9] 13571 pos 14.70%, 32697 min 35.41%, 46059 zero 49.89%
c [score-distribution-9] 3455 different 3.74% out of total 92327 variables
c [simplification-9] removed 1397 variables 1.5% (92327 remain 60%)
c [simplification-9] removed 29331 irredundant clauses 1.2% (2463808 remain 76%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 30000 = 60000 / 2
c [simplification-9] new conflict interval 90000
c [simplification-9] penalized conflict interval 90000 = 1 * 90000
c [simplification-9] hard conflict limit 244004 (soft 199004 + delta 45000)
c [simplification-9] new conflict limit 199004 (hard 244004)
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 -  349.5   92327  2463808    116262   25865  13540 697790   24   698  146   3%    214  242   24   17  144%
c -  387.5   92327  2463800    162879   33002  14084 698150   17   226  147   7%    627 -256   13   18   71%
c i  402.5   92326  2463800    184550   52568  14264 698325   21   531  155   4%    738   92   24   18  132%
c -  419.5   92326  2463800    203462   35207  14428 698470   23   611  147   4%   -394  164   15   19   77%
c i  424.9   92325  2463800    210504   41700  14493 698523   22   564  151   4%   -249  105   23   19  119%
c 
c [simplification-10] limit 199004 conflicts (hard 244004) hit after 243159 conflicts
c [quatres-6] found 30428 quaternary clauses 23% in total
c [quatres-6-2] added 115 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1136 quaternary resolvents
c [ternres-6] limit 50892484 with penalty 1 = 0 + 1
c [ternres-6] 70344 schedulable variables 76%
c [ternres-6] 5340 ternary resolvents (0 bin, 5340 trn)
c [ternres-6] 58431 variables remain 63% (33832 retained 37%)
c [card-4] limit 3180780 penalty 4 = 3 + 1
c [card-4] found 43 at-most-one constraints of average size 7.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 3180780 for elimination
c [card-4] 43 out of 43 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2544624 penalty 3 = 2 + 1
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 7 variables
c [treelook-4] limit 5089248 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 112321 literals 61%
c [treelook-4] scheduling used 5089262 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 5089248 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 8518127 steps
c [treelook-4] 112293 literals remain 61%
c [treelook-4] 54479 variables remain to probed next time 59%
c [treelook-4] removed 13 variables, found 342 hbrs
c [unhide-10] limit 2500000 with penalty 3 = 0 + 3
c [unhide-10-10] 827 units, 18 failed, 3470 tauts, 0 hbrs, 75872 literals
c [transred-6] limit 2455154 based on 2455154 irredundant clauses
c [transred-6] removed 26 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 63615605 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2222
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 2193
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2188
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2165
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 2160
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2157
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 2130
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2125
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2093
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1964
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1862
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1843
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1833
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1832
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1829
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1816
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1815
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1811
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1810
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1803
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1790
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1782
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1776
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1763
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1730
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1662
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1658
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1625
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1597
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1559
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1537
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1502
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1493
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1485
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1469
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1460
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1456
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1451
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1433
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1354
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1350
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 1296
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 1295
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 1168
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 1038
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 977
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 969
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 778
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 777
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 775
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 758
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 690
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 668
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 661
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 660
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 650
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 649
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 604
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 584
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 536
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 534
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 523
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 507
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 489
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 488
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 456
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 449
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 427
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 419
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 418
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 378
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 364
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 363
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 359
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 352
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 350
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 344
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 342
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 338
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 334
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 320
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 308
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 306
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 304
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 293
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 292
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 278
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 274
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 272
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 266
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 259
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 255
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 253
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 251
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 244
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 243
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 237
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 236
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 235
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 228
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 223
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 218
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 197
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 194
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 170
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 169
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 166
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 165
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 156
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 155
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 141
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 122
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 121
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-3-1] eliminated 1 clauses out of 16 (6%) of length 97
c [cce-3-1] eliminated 2 clauses out of 23 (9%) of length 94
c [cce-3-1] eliminated 1 clauses out of 26 (4%) of length 93
c [cce-3-1] eliminated 2 clauses out of 42 (5%) of length 92
c [cce-3-1] eliminated 1 clauses out of 30 (3%) of length 91
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 160 large clauses in 63616714 steps
c [cce-3-1] allowing another 31808357 steps for small clauses
c [cce-3-1] scheduling 1254062 clauses = 1203791 binary + 50271 ternary
c [cce-3-1] tried to eliminate 269 small clauses 0%
c [cce-3-1] eliminated 9 binary clauses 0%
c [cce-3-1] eliminated 9 small clauses 0%
c [cce-3-1] eliminated 14910 small clauses in 63615605 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 15070 covered clauses in round 1
c [cce-3] eliminated 15070 covered clauses in TOTAL during 1 rounds
c [cce-3] 15070 < 1/100 * 2455153 = 24551 considered unsuccessful
c [bca-6] limit of 10000000 steps and 5402337 added (scaled 2)
c [bca-6] 130411 out of 182768 literals actually usable 71%
c [bca-6] added 4229 blocked clauses in 531838 steps
c [sweep-6] limit 15267745 penalty 1 = 0 + 1
c [sweep-6-1] 2573 pos 3.3% + 75210 neg 96.7% = 77783 sched 85.1% ret 13600
c [sweep-6-1] 15282983 steps 72 queries 5447.75 avg class size
c [sweep-6-1] 2498 decisions 66 SAT calls 96.48 avg env size
c [sweep-6-1] 76825 variables remain 84% (14556 retained 16%)
c [decomp-24] removed 16 variables
c [sweep-6-1] removed 16 vars (0 failed, 8 eqs, 15 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 16 vars in TOTAL (1 rounds, 71 queries)
c [score-distribution-10] 18196 pos 19.92%, 33688 min 36.87%, 39483 zero 43.21%
c [score-distribution-10] 4923 different 5.39% out of total 91367 variables
c [simplification-10] removed 896 variables 1.0% (91367 remain 59%)
c [simplification-10] removed 23746 irredundant clauses 1.0% (2440054 remain 76%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 45000 = 90000 / 2
c [simplification-10] new conflict interval 135000
c [simplification-10] penalized conflict interval 135000 = 1 * 135000
c [simplification-10] hard conflict limit 445659 (soft 378159 + delta 67500)
c [simplification-10] new conflict limit 378159 (hard 445659)
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 -  467.9   91367  2440054    245449   38042  20024 654954   23   578  146   4%     35  126   23   20  115%
c -  499.0   91367  2440054    287539   39963  20393 655295   20   405  146   5%    504  -83   20   21   95%
c -  525.0   91367  2440054    329999   42367  20694 655627   24   398  147   6%    752  -83   17   23   73%
c -  540.2   91367  2440054    372065   45337  20878 655813   21   131  147  16%    881 -283   19   23   80%
c 
c [simplification-11] limit 378159 conflicts (hard 445659) hit after 387367 conflicts
c [quatres-7] found 32201 quaternary clauses 23% in total
c [quatres-7-1] removed 4 duplicate quaternary clauses
c [quatres-7-1] added 3 double-self-subsuming ternary resolvents
c [quatres-7-2] added 124 single-self-subsuming ternary resolvents
c [quatres-7-2] added 636 quaternary resolvents
c [ternres-7] limit 65109875 with penalty 1 = 0 + 1
c [ternres-7] 57873 schedulable variables 63%
c [ternres-7] 6072 ternary resolvents (2 bin, 6070 trn)
c [ternres-7] 42967 variables remain 47% (48400 retained 53%)
c [basicprobe-4] limit 200000000 penalty 1 = 0 + 1
c [basicprobe-4-0] 73934 probes remain 81% after last round
c [basicprobe-4-0] 535 units = 535 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 547 variables, found 25582 hbrs
c [bate-2] eliminated 9 asymmetric tautologies during probing
c [unhide-11] limit 2500000 with penalty 3 = 0 + 3
c [unhide-11-11] 138 units, 3 failed, 8068 tauts, 0 hbrs, 21479 literals
c [transred-7] limit 2425143 based on 2425143 irredundant clauses
c [transred-7] removed 28 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 90679 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 2 + 1
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 91005 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 90467 variables 100%
c [elim-9] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 15589 not tried 17% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 7734 = 9% variables out of 90467 scheduled
c [bca-7] limit of 10000000 steps and 5170351 added (scaled 2)
c [bca-7] 118475 out of 165468 literals actually usable 72%
c [bca-7] added 39122 blocked clauses in 684271 steps
c [sweep-7] limit 19532962 penalty 1 = 0 + 1
c [sweep-7-1] 2222 pos 3.2% + 66944 neg 96.8% = 69166 sched 83.6% ret 13567
c [sweep-7-1] 19567279 steps 129 queries 4395.78 avg class size
c [sweep-7-1] 5257 decisions 112 SAT calls 158.94 avg env size
c [sweep-7-1] 66616 variables remain 81% (16112 retained 19%)
c [decomp-26] removed 44 variables
c [sweep-7-1] removed 44 vars (0 failed, 17 eqs, 32 impls)
c [sweep-7] 44 < 1/1000 * 82733 = 82 considered unsuccessful
c [sweep-7] removed 44 vars in TOTAL (1 rounds, 128 queries)
c [score-distribution-11] 15255 pos 18.45%, 37284 min 45.09%, 30150 zero 36.46%
c [score-distribution-11] 4356 different 5.27% out of total 82689 variables
c [simplification-11] removed 8678 variables 9.5% (82689 remain 54%)
c [simplification-11] removed 117310 irredundant clauses 4.8% (2322744 remain 72%)
c [simplification-11] maximum reduction of 9% = max (9%, 5%)
c [simplification-11] large reduction 9% >= 5% limit
c [simplification-11] next conflict interval 3873 = min (387367/100, 135000)
c [simplification-11] penalized conflict interval 3873 = 1 * 3873
c [simplification-11] hard conflict limit 401240 (soft 391240 + delta 10000)
c [simplification-11] new conflict limit 391240 (hard 401240)
c 
c [simplification-12] limit 391240 conflicts (hard 401240) hit after 391240 conflicts
c [quatres-8] found 33447 quaternary clauses 22% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 2 double-self-subsuming ternary resolvents
c [quatres-8-2] added 16 single-self-subsuming ternary resolvents
c [quatres-8-2] added 322 quaternary resolvents
c [ternres-8] limit 65544520 with penalty 1 = 0 + 1
c [ternres-8] 38986 schedulable variables 47%
c [ternres-8] 6561 ternary resolvents (1 bin, 6560 trn)
c [ternres-8] 24641 variables remain 30% (58048 retained 70%)
c [simpleprobe-5] 70827 schedulable variables 86%
c [simpleprobe-5] limit 100000000 penalty 1 = 0 + 1
c [decomp-28] removed 1304 variables
c [simpleprobe-5] 49372 variables remain 61% (32013 retained 39%)
c [simpleprobe-5] removed 1304 variables, found 33482 hbrs, 1224 units
c [unhide-12] limit 2500000 with penalty 3 = 0 + 3
c [unhide-12-12] 78 units, 8 failed, 4547 tauts, 0 hbrs, 84803 literals
c [transred-8] limit 2304778 based on 2304778 irredundant clauses
c [transred-8] removed 45 transitive binary clauses
c [transred-8] found 5 units
c [elim-10] 15583 variables 19% will be scheduled this time
c [elim-10] scheduled 15583 variables 19%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 6803 not tried 8% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 1 = 0% variables out of 15583 scheduled
c [elim-10] 1 < 1/100 * 15583 = 155 considered unsuccessful
c [bca-8] limit of 10000000 steps and 5130944 added (scaled 2)
c [bca-8] 114207 out of 162588 literals actually usable 70%
c [bca-8] added 964429 blocked clauses in 1656913 steps
c [score-distribution-12] 16072 pos 19.77%, 36393 min 44.77%, 28828 zero 35.46%
c [score-distribution-12] 5050 different 6.21% out of total 81293 variables
c [simplification-12] removed 1396 variables 1.7% (81293 remain 53%)
c [simplification-12] removed 29195 irredundant clauses 1.3% (2293549 remain 71%)
c [simplification-12] maximum reduction of 2% = max (2%, 1%)
c [simplification-12] geometric conflict interval increment 45000 = 135000 / 3
c [simplification-12] new conflict interval 180000
c [simplification-12] penalized conflict interval 180000 = 1 * 180000
c [simplification-12] hard conflict limit 661240 (soft 571240 + delta 90000)
c [simplification-12] new conflict limit 571240 (hard 661240)
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 -  600.3   81293  2293549    413268   47546  32255 1374676   22   312  162   7%    948  -71   26   23  116%
c -  619.5   81293  2293549    455450   48735  32479 1374823   16   195  163   8%    984 -186   10   22   44%
c i  621.2   81292  2293549    460500   53297  32517 1374874   20   299  167   7%    987  -72   19   22   86%
c -  640.3   81292  2293549    498099   49104  32685 1375067   24   413  162   6%  -1233   27   26   22  117%
c i  656.3   81291  2293549    533241   80452  32874 1375273   23   404  176   6%   -296   27   29   22  130%
c -  662.6   81291  2293549    543801   51305  32939 1375318   22   414  163   5%  -1082   36   21   22   97%
c -  676.5   81291  2293549    589179   54161  33109 1375475   21   168  163  13%    -30 -137   22   22  100%
c 
c [simplification-13] limit 571240 conflicts (hard 661240) hit after 593205 conflicts
c [quatres-9] found 35064 quaternary clauses 23% in total
c [quatres-9-2] added 145 single-self-subsuming ternary resolvents
c [quatres-9-2] added 574 quaternary resolvents
c [ternres-9] limit 80892392 with penalty 1 = 0 + 1
c [ternres-9] 24252 schedulable variables 30%
c [ternres-9] 9458 ternary resolvents (5 bin, 9453 trn)
c [ternres-9] 6746 variables remain 8% (74545 retained 92%)
c [decomp-29] removed 5 variables
c [treelook-5] limit 8089239 penalty 1 = 0 + 1 boost 1
c [treelook-5] scheduled 112165 literals 69%
c [treelook-5] scheduling used 8089710 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 8089239 penalty 1 = 0 + 1 boost 1
c [treelook-5] used 8605649 steps
c [treelook-5] 112126 literals remain 69%
c [treelook-5] 43932 variables remain to probed next time 54%
c [treelook-5] removed 16 variables, found 51 hbrs
c [unhide-13] limit 2500000 with penalty 3 = 0 + 3
c [unhide-13-13] 71 units, 2 failed, 2606 tauts, 0 hbrs, 19778 literals
c [transred-9] limit 2290779 based on 2290779 irredundant clauses
c [transred-9] removed 37 transitive binary clauses
c [transred-9] found 7 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 81192 variables 100%
c [block-5] limit of 200000000 steps penalty 2 = 1 + 1
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 14948 blocked clauses
c [block-5] 14948 < 1/100 * 2290777 = 22907 considered unsuccessful
c [bca-9] limit of 10000000 steps and 5575881 added (scaled 2)
c [bca-9] 112362 out of 162382 literals actually usable 69%
c [bca-9] added 3727 blocked clauses in 1620065 steps
c [sweep-8] limit 12133858 penalty 2 = 1 + 1
c [sweep-8-1] 2763 pos 4.2% + 62407 neg 95.8% = 65170 sched 80.3% ret 16020
c [sweep-8-1] 12512008 steps 70 queries 8079.00 avg class size
c [sweep-8-1] 2630 decisions 62 SAT calls 116.52 avg env size
c [sweep-8-1] 64357 variables remain 79% (16830 retained 21%)
c [decomp-31] removed 14 variables
c [sweep-8-1] removed 14 vars (0 failed, 8 eqs, 16 impls)
c [sweep-8] 14 < 1/1000 * 81190 = 81 considered unsuccessful
c [sweep-8] removed 14 vars in TOTAL (1 rounds, 69 queries)
c [score-distribution-13] 12124 pos 14.94%, 41122 min 50.66%, 27930 zero 34.41%
c [score-distribution-13] 4077 different 5.02% out of total 81176 variables
c [simplification-13] removed 115 variables 0.1% (81176 remain 53%)
c [simplification-13] removed 18693 irredundant clauses 0.8% (2274856 remain 70%)
c [simplification-13] maximum reduction of 1% = max (0%, 1%)
c [simplification-13] geometric conflict interval increment 90000 = 180000 / 2
c [simplification-13] new conflict interval 270000
c [simplification-13] penalized conflict interval 270000 = 1 * 270000
c [simplification-13] hard conflict limit 998205 (soft 863205 + delta 135000)
c [simplification-13] new conflict limit 863205 (hard 998205)
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 -  707.4   81176  2274856    632855   55360  42587 1363480   19   250  163   8%    483  -24   16   22   76%
c -  726.2   81176  2274856    678582   56775  42776 1363658   22   269  164   8%    755  -14   26   21  121%
c -  741.4   81176  2274856    724192   57962  42904 1363800   22   240  164   9%    890  -17   24   21  116%
c -  759.0   81176  2274856    770689   58768  43042 1363919   21   150  164  14%    958 -103   19   21   90%
c -  777.6   81176  2274856    819673   60906  43195 1364045   17   131  164  13%    993  -99   13   19   69%
c -  799.7   81176  2274856    868040   62052  43414 1364210   22   239  164   9%   1009  -24   22   20  107%
c 
c [simplification-14] limit 863205 conflicts (hard 998205) hit after 879349 conflicts
c [quatres-10] found 36571 quaternary clauses 23% in total
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 193 single-self-subsuming ternary resolvents
c [quatres-10-2] added 427 quaternary resolvents
c [ternres-10] limit 99656376 with penalty 1 = 0 + 1
c [ternres-10] 6737 schedulable variables 8%
c [ternres-10] 26681 ternary resolvents (298 bin, 26383 trn)
c [ternres-10] 5 variables remain 0% (81171 retained 100%)
c [gauss-4] limit 2491409 penalty 4 = 3 + 1
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 2 variables
c [basicprobe-5] limit 200000000 penalty 1 = 0 + 1
c [basicprobe-5-0] 55585 probes remain 73% after last round
c [basicprobe-5-0] 726 units = 726 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 4670 variables, found 27166 hbrs
c [unhide-14] limit 2500000 with penalty 3 = 0 + 3
c [unhide-14-14] 2313 units, 10 failed, 6347 tauts, 0 hbrs, 89020 literals
c [transred-10] limit 2202599 based on 2202599 irredundant clauses
c [transred-10] removed 57 transitive binary clauses
c [transred-10] found 4 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 622852355 steps penalty 4 = 3 + 1
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 1083
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 1008
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 990
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 989
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 971
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 823
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 809
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 798
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 790
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 685
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 621
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 603
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 566
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 542
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 541
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 434
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 433
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 420
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 407
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 399
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 375
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 372
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 371
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 365
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 352
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 328
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 327
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 303
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 296
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 295
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 291
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 289
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 281
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 257
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 256
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 255
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 253
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 252
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 246
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 242
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 235
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 231
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 224
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 191
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 189
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 188
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 186
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 182
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 180
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 177
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 176
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 175
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 174
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 167
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 163
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 157
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 156
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 150
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 132
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 131
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 130
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 127
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 126
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 125
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 124
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 121
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 120
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 116
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 113
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 111
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 105
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 104
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 99
c [cce-4-1] eliminated 2 clauses out of 17 (12%) of length 98
c [cce-4-1] eliminated 2 clauses out of 15 (13%) of length 97
c [cce-4-1] eliminated 1 clauses out of 18 (6%) of length 96
c [cce-4-1] eliminated 1 clauses out of 34 (3%) of length 95
c [cce-4-1] eliminated 2 clauses out of 15 (13%) of length 94
c [cce-4-1] eliminated 1 clauses out of 23 (4%) of length 93
c [cce-4-1] eliminated 1 clauses out of 35 (3%) of length 92
c [cce-4-1] eliminated 1 clauses out of 46 (2%) of length 90
c [cce-4-1] eliminated 2 clauses out of 32 (6%) of length 88
c [cce-4-1] eliminated 1 clauses out of 47 (2%) of length 87
c [cce-4-1] eliminated 1 clauses out of 43 (2%) of length 86
c [cce-4-1] eliminated 1 clauses out of 36 (3%) of length 85
c [cce-4-1] eliminated 1 clauses out of 63 (2%) of length 79
c [cce-4-1] eliminated 1 clauses out of 114 (1%) of length 77
c [cce-4-1] eliminated 5 clauses out of 75 (7%) of length 73
c [cce-4-1] eliminated 9 clauses out of 119 (8%) of length 71
c [cce-4-1] eliminated 8 clauses out of 139 (6%) of length 69
c [cce-4-1] eliminated 14 clauses out of 146 (10%) of length 68
c [cce-4-1] eliminated 3 clauses out of 144 (2%) of length 67
c [cce-4-1] eliminated 2 clauses out of 129 (2%) of length 66
c [cce-4-1] eliminated 3 clauses out of 199 (2%) of length 65
c [cce-4-1] eliminated 4 clauses out of 112 (4%) of length 64
c [cce-4-1] eliminated 1 clauses out of 200 (0%) of length 63
c [cce-4-1] eliminated 3 clauses out of 151 (2%) of length 62
c [cce-4-1] eliminated 8 clauses out of 211 (4%) of length 61
c [cce-4-1] eliminated 8 clauses out of 181 (4%) of length 60
c [cce-4-1] eliminated 15 clauses out of 246 (6%) of length 59
c [cce-4-1] eliminated 26 clauses out of 270 (10%) of length 58
c [cce-4-1] eliminated 2 clauses out of 198 (1%) of length 57
c [cce-4-1] eliminated 6 clauses out of 156 (4%) of length 56
c [cce-4-1] eliminated 8 clauses out of 221 (4%) of length 55
c [cce-4-1] eliminated 9 clauses out of 213 (4%) of length 54
c [cce-4-1] eliminated 4 clauses out of 244 (2%) of length 53
c [cce-4-1] eliminated 8 clauses out of 211 (4%) of length 52
c [cce-4-1] eliminated 63 clauses out of 378 (17%) of length 51
c [cce-4-1] eliminated 25 clauses out of 367 (7%) of length 50
c [cce-4-1] eliminated 10 clauses out of 248 (4%) of length 49
c [cce-4-1] eliminated 13 clauses out of 239 (5%) of length 48
c [cce-4-1] eliminated 6 clauses out of 263 (2%) of length 47
c [cce-4-1] eliminated 1 clauses out of 249 (0%) of length 46
c [cce-4-1] eliminated 25 clauses out of 325 (8%) of length 45
c [cce-4-1] eliminated 1 clauses out of 215 (0%) of length 44
c [cce-4-1] eliminated 46 clauses out of 460 (10%) of length 43
c [cce-4-1] eliminated 5 clauses out of 341 (1%) of length 42
c [cce-4-1] eliminated 7 clauses out of 393 (2%) of length 41
c [cce-4-1] eliminated 18 clauses out of 261 (7%) of length 40
c [cce-4-1] eliminated 24 clauses out of 364 (7%) of length 39
c [cce-4-1] eliminated 34 clauses out of 275 (12%) of length 38
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 532 large clauses in 622852546 steps
c [cce-4-1] allowing another 311426273 steps for small clauses
c [cce-4-1] scheduling 2000086 clauses = 928504 binary + 1071582 ternary
c [cce-4-1] tried to eliminate 7779 small clauses 0%
c [cce-4-1] eliminated 513 binary clauses 0%
c [cce-4-1] eliminated 3 ternary clauses 0%
c [cce-4-1] eliminated 516 small clauses 0%
c [cce-4-1] eliminated 42727 small clauses in 622852373 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 43259 covered clauses in round 1
c [cce-4] eliminated 43259 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 74177 variables 100%
c [elim-11] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 12898 not tried 17% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 808 = 1% variables out of 74177 scheduled
c [bca-10] limit of 10000000 steps and 5328786 added (scaled 2)
c [bca-10] 95663 out of 146740 literals actually usable 65%
c [bca-10] added 25707 blocked clauses in 718233 steps
c [score-distribution-14] 14686 pos 20.02%, 38232 min 52.11%, 20451 zero 27.87%
c [score-distribution-14] 4127 different 5.62% out of total 73369 variables
c [simplification-14] removed 7807 variables 9.6% (73369 remain 48%)
c [simplification-14] removed 124425 irredundant clauses 5.5% (2150431 remain 67%)
c [simplification-14] maximum reduction of 10% = max (10%, 5%)
c [simplification-14] large reduction 10% >= 5% limit
c [simplification-14] next conflict interval 8793 = min (879349/100, 270000)
c [simplification-14] penalized conflict interval 8793 = 1 * 8793
c [simplification-14] hard conflict limit 898142 (soft 888142 + delta 10000)
c [simplification-14] new conflict limit 888142 (hard 898142)
c 
c [simplification-15] limit 888142 conflicts (hard 898142) hit after 898143 conflicts
c [quatres-11] found 38182 quaternary clauses 25% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 130 single-self-subsuming ternary resolvents
c [quatres-11-2] added 247 quaternary resolvents
c [ternres-11] limit 100000000 with penalty 1 = 0 + 1
c [ternres-11] 4 schedulable variables 0%
c [ternres-11] 25911 ternary resolvents (286 bin, 25625 trn)
c [ternres-11] 2 variables remain 0% (73367 retained 100%)
c [card-5] limit 3134470 penalty 5 = 4 + 1
c [card-5] found 24 at-most-one constraints of average size 11.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 3134470 for elimination
c [card-5] 24 out of 24 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-33] removed 20 variables
c [simpleprobe-6] 43130 schedulable variables 59%
c [simpleprobe-6] limit 100000000 penalty 1 = 0 + 1
c [decomp-34] removed 24 variables
c [simpleprobe-6] 47261 variables remain 64% (26064 retained 36%)
c [simpleprobe-6] removed 24 variables, found 41798 hbrs, 7 units
c [unhide-15] limit 2500000 with penalty 3 = 0 + 3
c [unhide-15-15] 10 units, 0 failed, 3406 tauts, 0 hbrs, 48493 literals
c [transred-11] limit 2146998 based on 2146998 irredundant clauses
c [transred-11] removed 74 transitive binary clauses
c [transred-11] found 6 units
c [elim-12] 6788 variables 9% will be scheduled this time
c [elim-12] scheduled 6788 variables 9%
c [elim-12] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 2812 not tried 4% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 0 = 0% variables out of 6788 scheduled
c [bca-11] limit of 10000000 steps and 5318982 added (scaled 2)
c [bca-11] 94895 out of 146620 literals actually usable 65%
c [bca-11] added 206036 blocked clauses in 956706 steps
c [score-distribution-15] 8616 pos 11.75%, 44282 min 60.40%, 20411 zero 27.84%
c [score-distribution-15] 2849 different 3.89% out of total 73309 variables
c [simplification-15] removed 60 variables 0.1% (73309 remain 48%)
c [simplification-15] removed 11328 irredundant clauses 0.5% (2139102 remain 66%)
c [simplification-15] maximum reduction of 1% = max (0%, 1%)
c [simplification-15] geometric conflict interval increment 135000 = 270000 / 2
c [simplification-15] new conflict interval 405000
c [simplification-15] penalized conflict interval 405000 = 1 * 405000
c [simplification-15] hard conflict limit 1505643 (soft 1303143 + delta 202500)
c [simplification-15] new conflict limit 1303143 (hard 1505643)
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 -  857.6   73309  2139101    918246   62942  91127 757578   25   426  150   6%   1017  157   24   21  117%
c -  876.6   73309  2139095    967770   65630  91205 757645   25   488  152   5%   1021  248   23   20  116%
c i  894.9   73308  2139089   1009391  103197  91321 757717   16   139  169  11%   1022 -135    9   20   44%
c -  898.1   73296  2139089   1017006   65687  91333 757732   17   174  151  10%  -5702  -94   17   20   85%
c -  921.6   73296  2139078   1068217   66399  91456 757922   20    85  152  23%  -2057 -196   18   22   80%
c i  937.0   73295  2139077   1109869  103441  91558 758007   17   207  170   8%   -608  -42   10   20   49%
c -  943.4   73084  2139077   1121809   69553  91576 758049   27   266  152  10%  -1665    7   26   22  119%
c -  956.9   73084  2139077   1174852   71818  91605 758159   17    96  152  18%   -173  -90   16   20   82%
c i  960.1   73083  2139077   1189836   85172  91647 758183   15    68  161  21%     72  -95    9   19   46%
c i  960.4   67004  2139077   1190542   85757  91655 758189   14    66  161  21%   -537  -97    9   19   48%
c i  961.8   57855  2139077   1196972   91084  91728 758201   14    69  162  20%   -977  -88    8   19   44%
c i  962.4   57090  2139077   1199750   93242  91741 758204   14    63  162  22%   -987  -90   11   19   57%
c i  962.8   57089  2139077   1201733   94961  91760 758211   13    61  162  21%   -969  -89   10   18   56%
c 0  962.8   53483  2139077   1201733   94961  91760 758211   13    61  162  21%   -969  -89   10   18   56%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 22 basic ate = 9 trn 41% + 13 lrg 59% in 2 updates
c bcas: 11 count, 2286592 added (16931 skipped), 10876307 steps
c bkwd: tried 221369 clauses, 442528 lits, 2.00 lits/clause
c bkwd: checked 321519801 occs, 1452.42 occs/clause, 726.55 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 216 large (0% self)
c blkd: 5 bces, 283735 removed, 55819216 resolutions, 221444521 steps
c blkd: 22305 blocking literals 7%, 1485 pure
c bump: 1170975 bumped seen, 123808392 lits 105.7 on average
c card: 5 count, 0 units, 0 am1, 422469184 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1220 subsumed
c card: 86 at-most-one constraints found, average size 7.42
c card: 86 at-most-one constraints used 100%, average size 7.42
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 4 cces, 1379 eliminated, 1308 ate 95%, 71 abce 5%
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: 12659990 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 93 gcs, 0 rescored clauses, 616 rescored vars
c dcps: 34 decompositions, 948 equivalent 1%
c deco: 157 decision-only clauses 0%, 48% reduction
c decs: 43689752 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 207015853 push, 206863283 pop (206863283 dec 100%)
c dsch: 3740576200 swaps, 0 down, 785216213 up
c elms: 12 elims, 42825 eliminated 28%, 12 pure 0%
c elms: 13 rounds, 1.1 rounds/bve
c elms: 20342 small 48%, 20986 large 49%
c elms: 25802 tried small, 20342 succeeded 79%, 5460 failed 21%
c elms: 34731 subsumed, 116906 strengthened, 6105 blocked
c elms: 18019455 copies, 26775301 resolutions, 573161 ipos
c elms: 97399842 subchks, 53179350 strchks
c gaus: 4 extractions, 5 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 16039940 steps, 8019970 extr 50%, 15 elim 0%
c glue: 20.8 orig avg, 20.8 real avg, 4.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 252284 = 134674 simple 53% + 117362 trn 47% + 248 lrg 0%, 2958 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1170975 clauses, 58.4 length
c lrnd: 68403199 lits = 100948996 orig - 32545797 removed 32%
c lrnd: 539599 uips 46%, 439476 flips 38%
c mins: 1147724 mins 98%, 2609 bin 0%, 20441 size 2%
c mins: 138992906 poisoned searches, 22226585 hits, 16% hit rate
c mins: 216332683 used twice searches, 11752344 hits, 5% hit rate
c move: moved 278336, 270772 bin 97%, 7564 trn 3%
c otfs: 31036 driving 24%, 100471 restarting 76%
c otfs: str 131507, 128885 red 98%, 2622 irr 2%
c otfs: str 131507, 0 bin 0%, 241 trn 0%, 131266 lrg 100%
c otfs: sub 479, 394 red 82%, 85 irr 18%
c otfs: sub 479, 0 bin 0%, 6 trn 1%, 473 lrg 99%
c phas: 3 computed, 149240 set, 0 pos (0%), 149240 neg (100%)
c prbs: 5 basic, 11455 probed, 1535 failed, 0 lifted
c prbs: 6 simple, 293957 probed, 1346 failed, 150 eqs
c prbs: 5 treelook, 50 probed, 906 failed, 0 lifted
c prom: 213415 locked 7% out of 2883835 tried
c prps: 2735448095 props, 61 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 11 count, 9036 quat, 2212 self1, 8 self2, 102 dup
c redc: 26877 clauses 36%, 75330 tried 6%, 558 sat 1%
c redc: 75550 lits 9%, 838620 tried 1%, 558 sat 0%
c redc: 2184 times jump level reduced, 76.8 levels on average
c reds: 25 count, 48069.3 conflicts per reduce
c reds: 0 memlim 0%, 25 arith 100%
c reds: 775221 collected 79%, 206093 retired 21%
c rmbd: 14165 removed, 8124 red 57%
c rsts: 23131 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 15 count, 13 confs 87%, 0 vars 0%
c simp: 0 its 0%, 1 bin 7%, 1 trns 7%
c subl: 1170975 count (1146801 tried 1.0), 77975 sub out of 1156946 (6.7%)
c swps: 8 count, 8 rounds, 743 queries (92.9/round)
c swps: 626 sat calls, 16 unsat (0.4% success rate)
c swps: 27399 decisions 43.8, 278 conflicts 0.4
c swps; 4753.7 avg class size, 181.5 avg environment size
c swps: 0 failed, 265 impls, 131 equivs
c swp0: 245 type 0 queries, 122 unsat (49.8%), 189 sat (77.1%)
c swp1: 498 type 1 queries, 201 unsat (40.4%), 423 sat (84.9%)
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: 89722997 calls to obtain time
c tops: 57053 fixed 37%, 14 its, 85838.07 confs/it
c trds: 11 transitive reductions, 337 removed, 28 failed
c trds: 2587 nodes, 15936 edges, 27631346 steps
c trim: 5482046 words, 20.9 MB
c trnr: 11 count, 594 bin, 90599 trn, 561079295 steps
c unhd: 15 count, 15 rounds, 78581655 steps
c unhd: 980 non-trivial sccs of average size 2.9
c unhd: 8492 units, 8491 bin, 1 trn, 0 lrg
c unhd: 116 failed, 108 stamp, 0 lits, 3 bin, 0 trn, 0 lrg
c unhd: 65001 tauts, 1789 bin 3%, 5455 trn 8%, 10616 lrg 16%
c unhd: 65001 tauts, 47141 stamp 73%, 21669 red 33%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 608154 str, 8491 bin 1%, 5613 trn 1%, 594050 lrg 98%, 323859 red 53%
c vars: 53483 remaining 35% and 100826 removed 65% out of 154309
c vars: 57053 fixed 37%, 42825 eliminated 28%, 948 equivalent 1%
c vsts: 24495117452 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 9.0 search visits per propagation, 19959.0 per conflict
c wchs: 1539837926 pushed, 128655826 enlarged, 142 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1165982        775221        206093      65057583      10187958        726468
c 
c  0 0         54264   5      5756   1         0   0  39172641  60   2527667  25     63463   9     1.4
c  1 5         27466   2     13321   2      9305   5   6052736   9<   772932   8     26143   4     0.3
c  2 6        112650  10     75523  10     19888  10   8815046  14   2079588  20<   100590  14     1.8
c  3 9        239260  21    175845  23     28448  14   5836061   9   2393484  23    195570  27<    4.0
c  4 14       270167  23<   199109  26<    40084  19   2858307   4   1337125  13    164861  23     4.4
c  5 21       211583  18    147564  19     41848  20<  1350823   2    633868   6     96526  13     4.0
c  6 30       136695  12     90173  12     32887  16    594730   1    271428   3     47351   7     2.4
c  7 41        70423   6     43841   6     19729  10    247670   0    112911   1     20361   3     1.5
c  8 54        30216   3     17481   2      9212   4     95575   0     42834   0      8392   1     0.8
c  9 69         9988   1      5122   1      3438   2     26608   0     12581   0      2420   0     0.3
c 10 86         2889   0      1315   0      1118   1      6726   0      3234   0       757   0     0.1
c 11 126         354   0       160   0       124   0       621   0       286   0        31   0     0.0
c 12 230          27   0        11   0        12   0        39   0        20   0         3   0     0.0
c 
c avg                  4.1           4.2           4.6           1.0           2.3           3.4
c std                  1.9           1.6           1.9           1.5           1.8           1.8
c 
c   91.904  10% elim
c   71.943   7% decide
c   62.914   7% block
c   47.392   5% probe
c   15.415   2% unhide
c   13.250   1% sweep
c   12.637   1% quatres
c   12.260   1% cce
c   10.704   1% bca
c    6.486   1% bump
c 
c   10.076 < 1% rest (below)
c 
c    4.948   1% ternres
c    2.676   0% gauss
c    1.654   0% rescore
c    0.599   0% transred
c    0.199   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    9.018   1% preprocessing     3%
c  285.535  30% inprocessing     97%
c ==================================
c  294.553  31% simplifying
c  668.260  69% search
c ==================================
c  962.813 100% all
c 
c       1201733 conflicts,        1248.1 confs/sec
c          7568 ternaries,         158.8 confs/ternary
c          6338 binaries,          189.6 confs/binary
c            14 iterations,      85838.1 confs/iteration
c 
c            25 reductions,          0.0 redus/sec,  48069.3 confs/reduction
c         23131 restarts,           24.0 rests/sec,     52.0 confs/restart
c      43689752 decisions,       45377.2 decis/sec,     36.4 decis/conflict
c    2735448095 propagations,  2841101.0 props/sec,     62.6 props/decision
c 
c 962.8 seconds, 256.9 MB
c launch: done
