c launch: /data/cnf/sc2014/app/velev-vliw-uns-4.0-9-i1.cnf.bz2
c host: atom17
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/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 --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=4
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 [score-type] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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 [sort-queue-1] sorted 149180 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 149180 (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 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 5000 conflicts (hard 15000) hit after 5000 conflicts
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] 127356 variables remain 85% (21823 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 106024 literals 36%
c [treelook-1] scheduling used 809497 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 799863 based on 3199453 irredundant clauses
c [treelook-1] used 836045 steps
c [treelook-1] 105134 literals remain 35%
c [treelook-1] 104373 variables remain to probed next time 70%
c [treelook-1] removed 875 variables, found 86 hbrs
c [basicprobe-1] limit 25435224 based on 3179403 irredundant clauses
c [basicprobe-1-0] 141743 probes remain 96% after last round
c [basicprobe-1-0] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 31 variables, found 20415 hbrs
c [unhide-2] limit 198712 based on 3179403 irredundant clauses
c [unhide-2-2] 48 units, 1 failed, 119 tauts, 0 hbrs, 47923 literals
c [elim-2] 147999 variables 100% will be scheduled this time
c [elim-2] scheduled 147999 variables 100%
c [elim-2] limit of 15296562 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 138698 not tried 94% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 6437 = 4% variables out of 147999 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 121025 enqueued variables after 5000 conflicts
c [score-dist-2] active 20762 (15%), one 0 (0%), zero 121025 (85%)
c [score-dist-2] max exp 511, different 28 (5%)
c [score-dist-2] median active exp 500, avg 498.5
c [simplification-2] removed 7393 variables 5.0% (141787 remain 92%)
c [simplification-2] removed 35437 irredundant clauses 1.1% (3164018 remain 98%)
c [simplification-2] maximum reduction of 5% = max (5%, 1%)
c [simplification-2] large reduction 5% >= 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 17000 (soft 7000 + delta 10000)
c [simplification-2] new conflict limit 7000 (hard 17000)
c 
c [simplification-3] limit 7000 conflicts (hard 17000) hit after 7000 conflicts
c [card-2] limit 791004 based on 3164018 irredundant clauses
c [card-2] found 12 at-most-one constraints of average size 3.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 791004 for elimination
c [card-2] 12 out of 12 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 3 variables
c [treelook-2] limit 791003 based on 3164012 irredundant clauses
c [treelook-2] scheduled 105244 literals 37%
c [treelook-2] scheduling used 791206 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 791003 based on 3164012 irredundant clauses
c [treelook-2] used 1823370 steps
c [treelook-2] 105239 literals remain 37%
c [treelook-2] 96930 variables remain to probed next time 68%
c [treelook-2] removed 0 variables, found 423 hbrs
c [unhide-3] limit 197750 based on 3164012 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 365 tauts, 0 hbrs, 7196 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 141783 variables 100%
c [elim-3] limit of 23283535 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 128846 not tried 91% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 4229 = 3% variables out of 141783 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 114560 enqueued variables after 7000 conflicts
c [score-dist-3] active 22994 (17%), one 0 (0%), zero 114560 (83%)
c [score-dist-3] max exp 510, different 35 (7%)
c [score-dist-3] median active exp 497, avg 495.5
c [simplification-3] removed 4233 variables 3.0% (137554 remain 89%)
c [simplification-3] removed 8739 irredundant clauses 0.3% (3155279 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 27000 (soft 17000 + delta 10000)
c [simplification-3] new conflict limit 17000 (hard 27000)
c 
c [simplification-4] limit 17000 conflicts (hard 27000) hit after 17001 conflicts
c [basicprobe-2] limit 25242232 based on 3155279 irredundant clauses
c [basicprobe-2-0] 126720 probes remain 92% after last round
c [basicprobe-2-0] 28 units = 28 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 28 variables, found 13878 hbrs
c [unhide-4] limit 254403 with penalty 3 = 0 + 3
c [unhide-4-4] 36 units, 1 failed, 98 tauts, 0 hbrs, 35366 literals
c [elim-4] 128662 variables 94% will be scheduled this time
c [elim-4] scheduled 128662 variables 94%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1017612700 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 1611 not tried 1% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 6997 = 5% variables out of 128662 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 100530 enqueued variables after 17001 conflicts
c [score-dist-4] active 29962 (23%), one 0 (0%), zero 100530 (77%)
c [score-dist-4] max exp 510, different 74 (14%)
c [score-dist-4] median active exp 496, avg 482.9
c [simplification-4] removed 7062 variables 5.1% (130492 remain 85%)
c [simplification-4] removed 19010 irredundant clauses 0.6% (3136269 remain 97%)
c [simplification-4] maximum reduction of 5% = max (5%, 1%)
c [simplification-4] large reduction 5% >= 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 29001 (soft 19001 + delta 10000)
c [simplification-4] new conflict limit 19001 (hard 29001)
c 
c [simplification-5] limit 19001 conflicts (hard 29001) hit after 19002 conflicts
c [quatres-1] found 31913 quaternary clauses 20% in total
c [quatres-1-2] added 1180 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3431 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 13974580 with penalty 2 = 0 + 2
c [ternres-1] all 130492 free variables schedulable
c [ternres-1] 2864 ternary resolvents (3 bin, 2861 trn)
c [ternres-1] 126030 variables remain 97% (4462 retained 3%)
c [gauss-1] limit 1568134 based on 3136269 irredundant clauses
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1 variables
c [unhide-5] limit 279491 with penalty 3 = 0 + 3
c [unhide-5-5] 11 units, 1 failed, 7439 tauts, 0 hbrs, 13143 literals
c [transred-1] limit 3129148 based on 3129148 irredundant clauses
c [transred-1] removed 1 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 130479 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 279491615 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 143224 blocked clauses
c [cce-1] limit of 27949161 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 3 clauses out of 6 (50%) of length 2206
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 793
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 755
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 754
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 752
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 750
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 643
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 607
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 557
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 547
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 508
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 485
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 425
c [cce-1-1] eliminated 11 clauses out of 11 (100%) of length 409
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 389
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 367
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 339
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 315
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 33 large clauses in 27949227 steps
c [cce-1-1] allowing another 13974613 steps for small clauses
c [cce-1-1] scheduling 1760231 clauses = 1708705 binary + 51526 ternary
c [cce-1-1] tried to eliminate 92 small clauses 0%
c [cce-1-1] eliminated 11 binary clauses 0%
c [cce-1-1] eliminated 11 small clauses 0%
c [cce-1-1] eliminated 11 small clauses in 27949162 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 44 covered clauses in round 1
c [cce-1] eliminated 44 covered clauses in TOTAL during 1 rounds
c [cce-1] 44 < 1/100 * 2985606 = 29856 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 130421 variables 100%
c [elim-5] limit of 111796646 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 42693 not tried 33% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 8804 = 7% variables out of 130421 scheduled
c [bca-1] limit of 10000000 steps and 5950874 added (scaled 2)
c [bca-1] 222463 out of 243236 literals actually usable 91%
c [bca-1] added 274588 blocked clauses in 973844 steps
c [sweep-1] limit 5950374 based on 2975187 irredundant clauses
c [sweep-1-1] 2287 pos 1.9% + 119330 neg 98.1% = 121617 sched 100.0% ret 0
c [sweep-1-1] 5970517 steps 25 queries 14434.00 avg class size
c [sweep-1-1] 1052 decisions 23 SAT calls 644.57 avg env size
c [sweep-1-1] 121319 variables remain 100% (298 retained 0%)
c [decomp-10] removed 6 variables
c [sweep-1-1] removed 6 vars (0 failed, 1 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 6 vars in TOTAL (1 rounds, 24 queries)
c [sort-queue-5] sorted 95810 enqueued variables after 19002 conflicts
c [score-dist-5] active 25801 (21%), one 0 (0%), zero 95810 (79%)
c [score-dist-5] max exp 510, different 82 (16%)
c [score-dist-5] median active exp 493, avg 483.4
c [simplification-5] removed 8881 variables 6.8% (121611 remain 79%)
c [simplification-5] removed 161142 irredundant clauses 5.1% (2975127 remain 92%)
c [simplification-5] maximum reduction of 7% = max (7%, 5%)
c [simplification-5] large reduction 7% >= 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 31002 (soft 21002 + delta 10000)
c [simplification-5] new conflict limit 21002 (hard 31002)
c 
c [simplification-6] limit 21002 conflicts (hard 31002) hit after 21002 conflicts
c [quatres-2] found 32359 quaternary clauses 20% in total
c [quatres-2-2] added 131 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1274 quaternary resolvents
c [ternres-2] limit 11900508 based on 2975127 irredundant clauses
c [ternres-2] 117460 schedulable variables 97%
c [ternres-2] 1273 ternary resolvents (0 bin, 1273 trn)
c [ternres-2] 113769 variables remain 94% (7842 retained 6%)
c [card-3] limit 750180 penalty 3 = 2 + 1
c [card-3] found 7 at-most-one constraints of average size 4.7
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 750180 for elimination
c [card-3] 7 out of 7 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 103736 schedulable variables 85%
c [simpleprobe-3] limit 12002890 penalty 2 = 1 + 1
c [decomp-12] removed 24 variables
c [simpleprobe-3] 106138 variables remain 87% (15449 retained 13%)
c [simpleprobe-3] removed 24 variables, found 45816 hbrs, 24 units
c [unhide-6] limit 300072 with penalty 3 = 0 + 3
c [unhide-6-6] 20 units, 2 failed, 304 tauts, 0 hbrs, 21578 literals
c [transred-2] limit 2974875 based on 2974875 irredundant clauses
c [transred-2] removed 22 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 121565 variables 100%
c [block-2] limit of 60014451 steps penalty 1 = 0 + 1
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 3026 blocked clauses
c [block-2] 3026 < 1/100 * 2974875 = 29748 considered unsuccessful
c [elim-6] 1609 variables 1% will be scheduled this time
c [elim-6] scheduled 1609 variables 1%
c [elim-6] limit of 120028902 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 902 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 1609 scheduled
c [bca-2] limit of 10000000 steps and 6077846 added (scaled 2)
c [bca-2] 221342 out of 243132 literals actually usable 91%
c [bca-2] added 138746 blocked clauses in 1108302 steps
c [sweep-2] limit 5940052 based on 2970026 irredundant clauses
c [sweep-2-1] 2157 pos 1.8% + 119111 neg 98.2% = 121268 sched 99.8% ret 297
c [sweep-2-1] 6046774 steps 26 queries 15864.88 avg class size
c [sweep-2-1] 1038 decisions 25 SAT calls 163.60 avg env size
c [sweep-2-1] 120953 variables remain 99% (612 retained 1%)
c [decomp-13] removed 8 variables
c [sweep-2-1] removed 8 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 8 vars in TOTAL (1 rounds, 25 queries)
c [sort-queue-6] sorted 95672 enqueued variables after 21002 conflicts
c [score-dist-6] active 25885 (21%), one 0 (0%), zero 95672 (79%)
c [score-dist-6] max exp 509, different 89 (17%)
c [score-dist-6] median active exp 487, avg 479.4
c [simplification-6] removed 54 variables 0.0% (121557 remain 79%)
c [simplification-6] removed 5472 irredundant clauses 0.2% (2969655 remain 92%)
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 66002 (soft 51002 + delta 15000)
c [simplification-6] new conflict limit 51002 (hard 66002)
c 
c [simplification-7] limit 51002 conflicts (hard 66002) hit after 51002 conflicts
c [quatres-3] found 33242 quaternary clauses 20% in total
c [quatres-3-1] added 3 double-self-subsuming ternary resolvents
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1152 quaternary resolvents
c [ternres-3] limit 13337812 with penalty 1 = 0 + 1
c [ternres-3] 113716 schedulable variables 94%
c [ternres-3] 1643 ternary resolvents (0 bin, 1643 trn)
c [ternres-3] 109584 variables remain 90% (11973 retained 10%)
c [gauss-2] limit 1484823 based on 2969647 irredundant clauses
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-7] limit 333445 with penalty 4 = 0 + 4
c [unhide-7-7] 12 units, 1 failed, 2968 tauts, 0 hbrs, 35303 literals
c [transred-3] limit 2966791 based on 2966791 irredundant clauses
c [transred-3] removed 15 transitive binary clauses
c [cce-2] limit of 33344531 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 2422
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 2308
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 2283
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 2043
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 2022
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1779
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 884
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 880
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 748
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 747
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 744
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 742
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 738
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 732
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 715
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 680
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 559
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 533
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 528
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 527
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 516
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 497
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 495
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 478
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 475
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 457
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 446
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 418
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 408
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 397
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 394
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 383
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 381
c [cce-2-1] eliminated 7 clauses out of 7 (100%) of length 379
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 378
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 375
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 370
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 362
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 351
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 329
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 328
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 53 large clauses in 33344699 steps
c [cce-2-1] allowing another 16672349 steps for small clauses
c [cce-2-1] scheduling 2757913 clauses = 1684186 binary + 1073727 ternary
c [cce-2-1] tried to eliminate 241 small clauses 0%
c [cce-2-1] eliminated 1 binary clauses 0%
c [cce-2-1] eliminated 1 small clauses 0%
c [cce-2-1] eliminated 229 small clauses in 33350912 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 282 covered clauses in round 1
c [cce-2] eliminated 282 covered clauses in TOTAL during 1 rounds
c [cce-2] 282 < 1/100 * 2966791 = 29667 considered unsuccessful
c [bca-3] limit of 10000000 steps and 6140185 added (scaled 2)
c [bca-3] 202788 out of 243090 literals actually usable 83%
c [bca-3] added 30 blocked clauses in 1018647 steps
c [sweep-3] limit 5933018 based on 2966509 irredundant clauses
c [sweep-3-1] 2273 pos 1.9% + 118659 neg 98.1% = 120932 sched 99.5% ret 612
c [sweep-3-1] 6053763 steps 22 queries 14054.73 avg class size
c [sweep-3-1] 949 decisions 19 SAT calls 200.84 avg env size
c [sweep-3-1] 120771 variables remain 99% (773 retained 1%)
c [decomp-15] removed 2 variables
c [sweep-3-1] removed 2 vars (0 failed, 2 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 2 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-7] sorted 78026 enqueued variables after 51002 conflicts
c [score-dist-7] active 43516 (36%), one 0 (0%), zero 78026 (64%)
c [score-dist-7] max exp 509, different 204 (40%)
c [score-dist-7] median active exp 487, avg 469.2
c [simplification-7] removed 15 variables 0.0% (121542 remain 79%)
c [simplification-7] removed 3138 irredundant clauses 0.1% (2966509 remain 92%)
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 141002 (soft 111002 + delta 30000)
c [simplification-7] new conflict limit 111002 (hard 141002)
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 -  215.0  121542  2966509     66609   23603   8158 480431  124   282  160  44%    648   35  106   49  217%
c -  236.2  121542  2966507    109750   28676   8189 480456  149   281  161  53%    829   20  174   71  246%
c 
c [simplification-8] limit 111002 conflicts (hard 141002) hit after 111002 conflicts
c [quatres-4] found 34216 quaternary clauses 21% in total
c [quatres-4-2] added 8 single-self-subsuming ternary resolvents
c [quatres-4-2] added 772 quaternary resolvents
c [ternres-4] limit 18726192 with penalty 1 = 0 + 1
c [ternres-4] 109569 schedulable variables 90%
c [ternres-4] 2339 ternary resolvents (2 bin, 2337 trn)
c [ternres-4] 103777 variables remain 85% (17765 retained 15%)
c [treelook-3] limit 936309 penalty 2 = 1 + 1 boost 1
c [treelook-3] scheduled 90501 literals 37%
c [treelook-3] scheduling used 936343 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 936309 penalty 2 = 1 + 1 boost 1
c [treelook-3] used 1102490 steps
c [treelook-3] 90498 literals remain 37%
c [treelook-3] 79306 variables remain to probed next time 65%
c [treelook-3] removed 1 variables, found 5 hbrs
c [unhide-8] limit 936309 with penalty 3 = 0 + 3
c [unhide-8-8] 85 units, 1 failed, 146 tauts, 0 hbrs, 41158 literals
c [transred-4] limit 2966477 based on 2966477 irredundant clauses
c [transred-4] removed 22 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 121455 variables 100%
c [block-3] limit of 93630961 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 414 blocked clauses
c [block-3] 414 < 1/100 * 2966477 = 29664 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 121455 variables 100%
c [elim-7] limit of 187261922 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 15232 not tried 13% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 517 = 0% variables out of 121455 scheduled
c [elim-7] 517 < 1/100 * 121455 = 1214 considered unsuccessful
c [bca-4] limit of 10000000 steps and 6129192 added (scaled 2)
c [bca-4] 208071 out of 241878 literals actually usable 86%
c [bca-4] added 639 blocked clauses in 1000265 steps
c [sweep-4] limit 5922010 based on 2961005 irredundant clauses
c [sweep-4-1] 2164 pos 1.8% + 118006 neg 98.2% = 120170 sched 99.4% ret 768
c [sweep-4-1] 6452323 steps 17 queries 13206.88 avg class size
c [sweep-4-1] 635 decisions 15 SAT calls 271.27 avg env size
c [sweep-4-1] 120040 variables remain 99% (898 retained 1%)
c [sweep-4-1] removed 0 vars (0 failed, 1 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-8] sorted 76126 enqueued variables after 111002 conflicts
c [score-dist-8] active 44812 (37%), one 0 (0%), zero 76126 (63%)
c [score-dist-8] max exp 510, different 426 (83%)
c [score-dist-8] median active exp 446, avg 367.1
c [simplification-8] removed 604 variables 0.5% (120938 remain 78%)
c [simplification-8] removed 5502 irredundant clauses 0.2% (2961005 remain 92%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 60000
c [simplification-8] new conflict interval 120000
c [simplification-8] penalized conflict interval 120000 = 1 * 120000
c [simplification-8] hard conflict limit 291002 (soft 231002 + delta 60000)
c [simplification-8] new conflict limit 231002 (hard 291002)
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 -  299.8  120938  2961004    151042   30464   9629 470490  126   249  160  50%    920  -11   89   86  104%
c -  312.5  120938  2960996    188830   30621   9645 470508   58   178  160  33%    966  -69   54   84   64%
c -  317.7  120938  2960996    223195   32463   9646 470508   56   172  161  33%    989  -46   60   73   82%
c 
c [simplification-9] limit 231002 conflicts (hard 291002) hit after 251362 conflicts
c [quatres-5] found 35880 quaternary clauses 22% in total
c [quatres-5-2] added 191 single-self-subsuming ternary resolvents
c [quatres-5-2] added 672 quaternary resolvents
c [ternres-5] limit 24143517 with penalty 1 = 0 + 1
c [ternres-5] 103253 schedulable variables 85%
c [ternres-5] 3956 ternary resolvents (0 bin, 3956 trn)
c [ternres-5] 95990 variables remain 79% (24948 retained 21%)
c [basicprobe-3] limit 120717589 penalty 1 = 0 + 1
c [basicprobe-3-0] 107997 probes remain 90% after last round
c [basicprobe-3-0] 128 units = 128 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1221 variables, found 39774 hbrs
c [bate-1] eliminated 4 asymmetric tautologies during probing
c [unhide-9] limit 603587 with penalty 4 = 0 + 4
c [unhide-9-9] 20 units, 0 failed, 4907 tauts, 0 hbrs, 23801 literals
c [transred-5] limit 2934537 based on 2934537 irredundant clauses
c [transred-5] removed 40 transitive binary clauses
c [transred-5] found 1 units
c [bca-5] limit of 10000000 steps and 6075819 added (scaled 2)
c [bca-5] 207690 out of 239394 literals actually usable 87%
c [bca-5] added 604 blocked clauses in 1016328 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 72430550 penalty 1 = 0 + 1
c [sweep-5-1] 2272 pos 1.9% + 116553 neg 98.1% = 118825 sched 99.3% ret 871
c [sweep-5-1] 72851951 steps 240 queries 2041.07 avg class size
c [sweep-5-1] 6733 decisions 195 SAT calls 288.95 avg env size
c [sweep-5-1] 98850 variables remain 83% (20846 retained 17%)
c [decomp-20] removed 281 variables
c [sweep-5-1] removed 281 vars (0 failed, 44 eqs, 102 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 281 vars in TOTAL (1 rounds, 239 queries)
c [sort-queue-9] sorted 93122 enqueued variables after 251362 conflicts
c [score-dist-9] active 26293 (22%), one 18278 (15%), zero 74844 (63%)
c [score-dist-9] max exp 510, different 346 (68%)
c [score-dist-9] median active exp 182, avg 234.0
c [simplification-9] removed 1523 variables 1.3% (119415 remain 77%)
c [simplification-9] removed 27492 irredundant clauses 0.9% (2933504 remain 91%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 60000 = 120000 / 2
c [simplification-9] new conflict interval 180000
c [simplification-9] penalized conflict interval 180000 = 1 * 180000
c [simplification-9] hard conflict limit 521362 (soft 431362 + delta 90000)
c [simplification-9] new conflict limit 431362 (hard 521362)
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 -  337.8  119415  2933503    256705   32008  13388 510500   55   458  162  12%   1003  243   51   66   78%
c -  343.2  119415  2933503    291631   32713  13391 510500   52   364  162  14%   1012   91   53   61   86%
c -  360.3  119415  2933503    330689   31395  13418 510526   87   201  162  44%   1017  -76  106   67  157%
c -  372.4  119415  2933500    370667   32735  13427 510543   80   191  162  42%   1020  -75   65   67   97%
c -  393.5  119415  2933494    422798   33026  13431 510572   69   110  163  62%   1022  -90   58   75   77%
c 
c [simplification-10] limit 431362 conflicts (hard 521362) hit after 463780 conflicts
c [quatres-6] found 33670 quaternary clauses 21% in total
c [quatres-6-2] added 814 quaternary resolvents
c [ternres-6] limit 33989934 with penalty 1 = 0 + 1
c [ternres-6] 94737 schedulable variables 79%
c [ternres-6] 6530 ternary resolvents (1 bin, 6529 trn)
c [ternres-6] 84717 variables remain 71% (34698 retained 29%)
c [card-4] limit 2124370 penalty 4 = 3 + 1
c [card-4] found 21 at-most-one constraints of average size 5.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2124370 for elimination
c [card-4] 21 out of 21 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1699496 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 [simpleprobe-4] 104239 schedulable variables 87%
c [simpleprobe-4] limit 100000000 penalty 1 = 0 + 1
c [decomp-22] removed 278 variables
c [simpleprobe-4] 80000 variables remain 67% (39137 retained 33%)
c [simpleprobe-4] removed 278 variables, found 67374 hbrs, 277 units
c [unhide-10] limit 849748 with penalty 4 = 0 + 4
c [unhide-10-10] 164 units, 5 failed, 1847 tauts, 0 hbrs, 80117 literals
c [transred-6] limit 2929963 based on 2929963 irredundant clauses
c [transred-6] removed 33 transitive binary clauses
c [cce-3] limit of 42487417 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 3081
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 3080
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 3075
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2979
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2778
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2414
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 2392
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2337
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 2304
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2293
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2254
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2240
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2231
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2230
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2228
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 2224
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2211
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2199
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 2150
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 2149
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2134
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2100
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 2039
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 2009
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1989
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1943
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1789
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 1759
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 1757
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1710
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1690
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1570
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1168
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1086
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 810
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 800
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 731
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 692
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 676
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 618
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 602
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 596
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 593
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 560
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 552
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 489
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 480
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 468
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 467
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 460
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 454
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 448
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 444
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 439
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 414
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 413
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 412
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 410
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 394
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 382
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 375
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 371
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 369
c [cce-3-1] eliminated 2 clauses out of 5 (40%) of length 368
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 363
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 362
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 357
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 346
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 339
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 334
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 325
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 315
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 312
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 305
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 304
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 297
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 291
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 289
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 283
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 278
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 105 large clauses in 42487420 steps
c [cce-3-1] allowing another 21243710 steps for small clauses
c [cce-3-1] scheduling 2726463 clauses = 1652435 binary + 1074028 ternary
c [cce-3-1] tried to eliminate 194 small clauses 0%
c [cce-3-1] eliminated 12 binary clauses 0%
c [cce-3-1] eliminated 12 small clauses 0%
c [cce-3-1] eliminated 1730 small clauses in 42487524 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1835 covered clauses in round 1
c [cce-3] eliminated 1835 covered clauses in TOTAL during 1 rounds
c [cce-3] 1835 < 1/100 * 2929961 = 29299 considered unsuccessful
c [bca-6] limit of 10000000 steps and 6064055 added (scaled 2)
c [bca-6] 208141 out of 237940 literals actually usable 87%
c [bca-6] added 2716 blocked clauses in 832057 steps
c [sweep-6] limit 10196980 penalty 1 = 0 + 1
c [sweep-6-1] 1970 pos 2.0% + 96290 neg 98.0% = 98260 sched 82.6% ret 20709
c [sweep-6-1] 10777451 steps 41 queries 7438.00 avg class size
c [sweep-6-1] 1120 decisions 38 SAT calls 162.97 avg env size
c [sweep-6-1] 97894 variables remain 82% (21075 retained 18%)
c [decomp-23] removed 4 variables
c [sweep-6-1] removed 4 vars (0 failed, 3 eqs, 4 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 4 vars in TOTAL (1 rounds, 40 queries)
c [sort-queue-10] sorted 101319 enqueued variables after 463780 conflicts
c [score-dist-10] active 17646 (15%), one 27064 (23%), zero 74255 (62%)
c [score-dist-10] max exp 510, different 425 (83%)
c [score-dist-10] median active exp 491, avg 401.8
c [simplification-10] removed 450 variables 0.4% (118965 remain 77%)
c [simplification-10] removed 5389 irredundant clauses 0.2% (2928105 remain 91%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 180000
c [simplification-10] new conflict interval 360000
c [simplification-10] penalized conflict interval 360000 = 1 * 360000
c [simplification-10] hard conflict limit 1003780 (soft 823780 + delta 180000)
c [simplification-10] new conflict limit 823780 (hard 1003780)
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 -  424.3  118965  2928105    474661   34329  19417 578344   80   111  164  72%   1023  -54   81   78  103%
c -  433.6  118965  2928105    513227   35825  19425 578375   74   104  166  71%   1024  -37   73   77   94%
c -  441.3  118965  2928105    550204   36467  19431 578383   73    85  167  86%   1024  -35   75   76   98%
c -  449.2  118965  2928105    587912   36421  19435 578397   79    85  167  93%   1024  -22   79   77  102%
c -  457.0  118965  2928105    627176   37156  19436 578403   76    83  169  91%   1024  -15   77   78   98%
c -  464.7  118965  2928105    666419   37768  19439 578409   75    82  169  91%   1024  -13   73   77   95%
c -  472.3  118965  2928105    705395   38668  19442 578411   74    83  170  89%   1024   -7   74   75   99%
c -  480.0  118965  2928105    744718   39642  19443 578412   73    79  170  92%   1024   -8   73   74   99%
c -  487.5  118965  2928105    784702   40115  19443 578416   72    79  170  91%   1024   -8   70   73   96%
c -  494.8  118965  2928105    824256   40585  19443 578416   70    79  170  89%   1024   -4   59   73   81%
c 
c [simplification-11] limit 823780 conflicts (hard 1003780) hit after 860933 conflicts
c [quatres-7] found 34626 quaternary clauses 21% in total
c [quatres-7-2] added 52 single-self-subsuming ternary resolvents
c [quatres-7-2] added 455 quaternary resolvents
c [ternres-7] limit 43179949 with penalty 1 = 0 + 1
c [ternres-7] 84402 schedulable variables 71%
c [ternres-7] 5880 ternary resolvents (0 bin, 5880 trn)
c [ternres-7] 73358 variables remain 62% (45607 retained 38%)
c [treelook-4] limit 4317994 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 136682 literals 57%
c [treelook-4] scheduling used 4318121 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 4317994 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 5560886 steps
c [treelook-4] 136676 literals remain 57%
c [treelook-4] 77026 variables remain to probed next time 65%
c [treelook-4] removed 2 variables, found 369 hbrs
c [unhide-11] limit 1079498 with penalty 4 = 0 + 4
c [unhide-11-11] 0 units, 1 failed, 3513 tauts, 0 hbrs, 26257 literals
c [transred-7] limit 2925062 based on 2925062 irredundant clauses
c [transred-7] removed 22 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 118962 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 128508 blocked clauses
c [elim-8] 875 variables 1% will be scheduled this time
c [elim-8] scheduled 875 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2000000000 steps penalty 3 = 2 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 4 variables 0% in round 1 in 362476040 steps
c [elim-8-1] backward subsumption/strengthening limit 362476000
c [elim-8-1-1] backward checking 12289 touched variables 10%
c [elim-8-1-1] incomplete backward checking 13351 remain 109%
c [elim-8-1] subsumed 0 and strengthened 2 clauses in 362485625 steps
c [elim-8-1] rescheduled 1065 variables 1% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 4816440 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 4 = 0% variables out of 875 scheduled
c [elim-8] 4 < 1/100 * 875 = 8 considered unsuccessful
c [bca-7] limit of 10000000 steps and 5796659 added (scaled 2)
c [bca-7] 216803 out of 237656 literals actually usable 91%
c [bca-7] added 199353 blocked clauses in 1136824 steps
c [sweep-7] limit 12953984 penalty 1 = 0 + 1
c [sweep-7-1] 1820 pos 1.9% + 95958 neg 98.1% = 97778 sched 82.3% ret 21049
c [sweep-7-1] 12993497 steps 50 queries 6659.88 avg class size
c [sweep-7-1] 1125 decisions 45 SAT calls 128.82 avg env size
c [sweep-7-1] 97315 variables remain 82% (21512 retained 18%)
c [decomp-26] removed 13 variables
c [sweep-7-1] removed 13 vars (0 failed, 4 eqs, 12 impls)
c [sweep-7] 13 < 1/1000 * 118827 = 118 considered unsuccessful
c [sweep-7] removed 13 vars in TOTAL (1 rounds, 49 queries)
c [sort-queue-11] sorted 110765 enqueued variables after 860933 conflicts
c [score-dist-11] active 8049 (7%), one 36786 (31%), zero 73979 (62%)
c [score-dist-11] max exp 509, different 284 (56%)
c [score-dist-11] median active exp 497, avg 407.1
c [simplification-11] removed 151 variables 0.1% (118814 remain 77%)
c [simplification-11] removed 134378 irredundant clauses 4.6% (2793727 remain 86%)
c [simplification-11] maximum reduction of 5% = max (0%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 8609 = min (860933/100, 360000)
c [simplification-11] penalized conflict interval 8609 = 1 * 8609
c [simplification-11] hard conflict limit 879542 (soft 869542 + delta 10000)
c [simplification-11] new conflict limit 869542 (hard 879542)
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 -  542.2  118814  2793726    865026   41116  25674 739995   61   609  173  10%   1024  511   73   71  102%
c 
c [simplification-12] limit 869542 conflicts (hard 879542) hit after 869543 conflicts
c [quatres-8] found 34178 quaternary clauses 21% in total
c [quatres-8-2] added 182 quaternary resolvents
c [ternres-8] limit 43665535 with penalty 1 = 0 + 1
c [ternres-8] 73264 schedulable variables 62%
c [ternres-8] 5019 ternary resolvents (0 bin, 5019 trn)
c [ternres-8] 59818 variables remain 50% (58996 retained 50%)
c [basicprobe-4] limit 200000000 penalty 1 = 0 + 1
c [basicprobe-4-0] 105084 probes remain 89% after last round
c [basicprobe-4-0] 205 units = 205 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 205 variables, found 52401 hbrs
c [bate-2] eliminated 3 asymmetric tautologies during probing
c [unhide-12] limit 2183276 with penalty 3 = 0 + 3
c [unhide-12-12] 195 units, 7 failed, 7873 tauts, 0 hbrs, 40325 literals
c [transred-8] limit 2790855 based on 2790855 irredundant clauses
c [transred-8] removed 5 transitive binary clauses
c [bca-8] limit of 10000000 steps and 5882892 added (scaled 2)
c [bca-8] 209359 out of 236824 literals actually usable 88%
c [bca-8] added 147 blocked clauses in 1060962 steps
c [sort-queue-12] sorted 94711 enqueued variables after 869543 conflicts
c [score-dist-12] active 23700 (20%), one 21442 (18%), zero 73269 (62%)
c [score-dist-12] max exp 510, different 234 (46%)
c [score-dist-12] median active exp 495, avg 476.9
c [simplification-12] removed 403 variables 0.3% (118411 remain 77%)
c [simplification-12] removed 6699 irredundant clauses 0.2% (2787027 remain 86%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 360000
c [simplification-12] new conflict interval 720000
c [simplification-12] penalized conflict interval 720000 = 1 * 720000
c [simplification-12] hard conflict limit 1949543 (soft 1589543 + delta 360000)
c [simplification-12] new conflict limit 1589543 (hard 1949543)
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 -  575.6  118411  2787025    926048   38175  30319 770145  121   149  170  82%   1024  -92  122   86  142%
c -  617.1  118411  2787025   1090788   36544  30338 770179  123   130  171  95%   1024  -14  128  117  110%
c 
c [simplification-13] limit of 524 binary hit after 524 binaries
c [quatres-9] found 34586 quaternary clauses 21% in total
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 197 quaternary resolvents
c [ternres-9] limit 50873215 with penalty 1 = 0 + 1
c [ternres-9] 59617 schedulable variables 50%
c [ternres-9] 5970 ternary resolvents (5 bin, 5965 trn)
c [ternres-9] 44862 variables remain 38% (73549 retained 62%)
c [decomp-28] removed 2 variables
c [simpleprobe-5] 79485 schedulable variables 67%
c [simpleprobe-5] limit 100000000 penalty 1 = 0 + 1
c [decomp-29] removed 155 variables
c [simpleprobe-5] 69114 variables remain 58% (49140 retained 42%)
c [simpleprobe-5] removed 155 variables, found 47352 hbrs, 152 units
c [unhide-13] limit 2500000 with penalty 3 = 0 + 3
c [unhide-13-13] 0 units, 3 failed, 3687 tauts, 0 hbrs, 17575 literals
c [transred-9] limit 2783468 based on 2783468 irredundant clauses
c [transred-9] removed 27 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 118252 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 830 blocked clauses
c [block-5] 830 < 1/100 * 2783467 = 27834 considered unsuccessful
c [bca-9] limit of 10000000 steps and 5874105 added (scaled 2)
c [bca-9] 204969 out of 236400 literals actually usable 87%
c [bca-9] added 127 blocked clauses in 1021870 steps
c [sweep-8] limit 7630982 penalty 2 = 1 + 1
c [sweep-8-1] 2131 pos 2.2% + 94762 neg 97.8% = 96893 sched 82.0% ret 21306
c [sweep-8-1] 7750091 steps 39 queries 9843.31 avg class size
c [sweep-8-1] 1474 decisions 37 SAT calls 110.89 avg env size
c [sweep-8-1] 96535 variables remain 82% (21664 retained 18%)
c [decomp-30] removed 1 variables
c [sweep-8-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-8] 1 < 1/1000 * 118199 = 118 considered unsuccessful
c [sweep-8] removed 1 vars in TOTAL (1 rounds, 38 queries)
c [sort-queue-13] sorted 101869 enqueued variables after 1090983 conflicts
c [score-dist-13] active 16329 (14%), one 29127 (25%), zero 72742 (62%)
c [score-dist-13] max exp 510, different 316 (62%)
c [score-dist-13] median active exp 421, avg 353.6
c [simplification-13] removed 213 variables 0.2% (118198 remain 77%)
c [simplification-13] removed 4430 irredundant clauses 0.2% (2782595 remain 86%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] forced so keeping old conflict interval 720000
c [simplification-13] conflict limit remains at 1589543 (hard 1949543)
c [simplification-13] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  673.2  118198  2782595   1237224   34871  36226 815369  111   133  171  84%   1024   -2   86  110   78%
c -  702.0  118198  2782595   1375723   35164  36228 815378   93   113  174  83%   1024   -3   99  105   94%
c -  719.8  118198  2782595   1445175   42346  36266 815469   93   131  175  71%   1024  -60   97   90  108%
c -  735.7  118198  2782595   1514230   43233  36277 815501   90   101  176  89%   1024  -42   88   93   95%
c -  748.4  118198  2782595   1565871   45612  36289 815519   88    95  178  93%   1024  -30   90   90  100%
c -  760.1  118198  2782595   1612708   44952  36290 815528   89    98  178  91%   1024  -14   96   89  109%
c 
c [simplification-14] limit 1589543 conflicts (hard 1949543) hit after 1622602 conflicts
c [quatres-10] found 34795 quaternary clauses 21% in total
c [quatres-10-2] added 5 single-self-subsuming ternary resolvents
c [quatres-10-2] added 169 quaternary resolvents
c [ternres-10] limit 63477561 with penalty 1 = 0 + 1
c [ternres-10] 44787 schedulable variables 38%
c [ternres-10] 7752 ternary resolvents (0 bin, 7752 trn)
c [ternres-10] 25821 variables remain 22% (92377 retained 78%)
c [gauss-4] limit 1586939 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-31] removed 1 variables
c [treelook-5] limit 6347756 penalty 1 = 0 + 1 boost 1
c [treelook-5] scheduled 159448 literals 67%
c [treelook-5] scheduling used 6347978 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 6347756 penalty 1 = 0 + 1 boost 1
c [treelook-5] used 8009125 steps
c [treelook-5] 159437 literals remain 67%
c [treelook-5] 76322 variables remain to probed next time 65%
c [treelook-5] removed 1 variables, found 377 hbrs
c [unhide-14] limit 1250000 with penalty 4 = 0 + 4
c [unhide-14-14] 65 units, 3 failed, 1857 tauts, 0 hbrs, 73729 literals
c [transred-10] limit 2782581 based on 2782581 irredundant clauses
c [transred-10] removed 18 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 396734761 steps penalty 4 = 3 + 1
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 755
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 728
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 270
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 268
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 248
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 245
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 243
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 232
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 225
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 224
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 221
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 209
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 199
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 198
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 192
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 177
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 173
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 172
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 169
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 168
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 144
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 139
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 137
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 108
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 103
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 102
c [cce-4-1] eliminated 2 clauses out of 8 (25%) of length 101
c [cce-4-1] eliminated 2 clauses out of 9 (22%) of length 99
c [cce-4-1] eliminated 1 clauses out of 19 (5%) of length 94
c [cce-4-1] eliminated 1 clauses out of 31 (3%) of length 88
c [cce-4-1] eliminated 2 clauses out of 44 (5%) of length 85
c [cce-4-1] eliminated 1 clauses out of 86 (1%) of length 81
c [cce-4-1] eliminated 1 clauses out of 94 (1%) of length 78
c [cce-4-1] eliminated 5 clauses out of 65 (8%) of length 76
c [cce-4-1] eliminated 3 clauses out of 97 (3%) of length 75
c [cce-4-1] eliminated 7 clauses out of 65 (11%) of length 74
c [cce-4-1] eliminated 1 clauses out of 93 (1%) of length 73
c [cce-4-1] eliminated 1 clauses out of 86 (1%) of length 72
c [cce-4-1] eliminated 2 clauses out of 104 (2%) of length 71
c [cce-4-1] eliminated 8 clauses out of 130 (6%) of length 69
c [cce-4-1] eliminated 13 clauses out of 194 (7%) of length 68
c [cce-4-1] eliminated 1 clauses out of 139 (1%) of length 67
c [cce-4-1] eliminated 1 clauses out of 85 (1%) of length 64
c [cce-4-1] eliminated 5 clauses out of 236 (2%) of length 63
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 91 large clauses in 396736157 steps
c [cce-4-1] allowing another 198368078 steps for small clauses
c [cce-4-1] scheduling 2578501 clauses = 1504501 binary + 1074000 ternary
c [cce-4-1] tried to eliminate 1500 small clauses 0%
c [cce-4-1] eliminated 221 binary clauses 0%
c [cce-4-1] eliminated 221 small clauses 0%
c [cce-4-1] eliminated 927 small clauses in 396739248 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 1018 covered clauses in round 1
c [cce-4] eliminated 1018 covered clauses in TOTAL during 1 rounds
c [cce-4] 1018 < 1/100 * 2782581 = 27825 considered unsuccessful
c [bca-10] limit of 10000000 steps and 5872101 added (scaled 2)
c [bca-10] 203679 out of 236258 literals actually usable 86%
c [bca-10] added 1303 blocked clauses in 1011404 steps
c [sort-queue-14] sorted 102221 enqueued variables after 1622602 conflicts
c [score-dist-14] active 15907 (13%), one 31072 (26%), zero 71149 (60%)
c [score-dist-14] max exp 510, different 354 (69%)
c [score-dist-14] median active exp 498, avg 391.6
c [simplification-14] removed 70 variables 0.1% (118128 remain 77%)
c [simplification-14] removed 1032 irredundant clauses 0.0% (2781563 remain 86%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 720000
c [simplification-14] conflict interval soft limit 1000000 reached
c [simplification-14] new conflict interval 1000000
c [simplification-14] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-14] hard conflict limit 3122602 (soft 2622602 + delta 500000)
c [simplification-14] new conflict limit 2622602 (hard 3122602)
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 -  795.4  118128  2781563   1676548   44447  43731 815391   94   106  176  89%   1024   -8   91   92   99%
c -  808.6  118128  2781563   1730326   45802  43765 815423   72   333  175  22%   1024   40   73   83   88%
c -  824.7  118128  2781563   1789790   47853  43773 815456   73   177  175  41%   1024  -72   70   82   86%
c -  852.7  118128  2781563   1882742   43899  43782 815500  130   135  175  96%   1024  -57  131  111  118%
c -  897.6  118128  2781563   2043745   26476  43782 815505  130   131  168  99%   1024   -8  127  128   99%
c -  950.2  118128  2781563   2235056   26861  43794 815540  122   140  170  87%   1024    0  107  126   85%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 7 basic ate = 4 trn 57% + 3 lrg 43% in 2 updates
c bcas: 10 count, 618253 added (86011 skipped), 10180503 steps
c bkwd: tried 22181 clauses, 44362 lits, 2.00 lits/clause
c bkwd: checked 328205587 occs, 14796.70 occs/clause, 7398.35 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 2 large (0% self)
c blkd: 5 bces, 276002 removed, 64677362 resolutions, 279830038 steps
c blkd: 19779 blocking literals 6%, 242 pure
c bump: 2357118 bumped seen, 712663829 lits 302.3 on average
c card: 4 count, 0 units, 0 am1, 156694239 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 221 subsumed
c card: 42 at-most-one constraints found, average size 4.62
c card: 42 at-most-one constraints used 100%, average size 4.62
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, 527 eliminated, 493 ate 94%, 34 abce 6%
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: 72 gcs, 0 rescored clauses, 9216 rescored vars
c dcps: 32 decompositions, 325 equivalent 0%
c deco: 1025094 decision-only clauses 43%, 61% reduction
c decs: 25579099 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 30959 eliminated 20%, 2 pure 0%
c elms: 9 rounds, 1.1 rounds/bve
c elms: 15968 small 52%, 14747 large 48%
c elms: 19732 tried small, 15968 succeeded 81%, 3764 failed 19%
c elms: 10135 subsumed, 83780 strengthened, 0 blocked
c elms: 10576594 copies, 16694452 resolutions, 453642 ipos
c elms: 64479753 subchks, 34681481 strchks
c gaus: 4 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12685336 steps, 6342668 extr 50%, 0 elim 0%
c glue: 96.6 orig avg, 96.6 real avg, 9.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 316865 = 164543 simple 52% + 151886 trn 48% + 436 lrg 0%, 1399 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2357118 clauses, 122.4 length
c lrnd: 288490298 lits = 578336690 orig - 289846392 removed 50%
c lrnd: 994618 uips 42%, 987421 flips 42%
c mins: 1327237 mins 56%, 133 bin 0%, 3360 size 0%
c mins: 220623855 poisoned searches, 25196452 hits, 11% hit rate
c mins: 419569571 used twice searches, 65763681 hits, 16% hit rate
c move: moved 271945, 264261 bin 97%, 7684 trn 3%
c otfs: 57908 driving 52%, 54242 restarting 48%
c otfs: str 112150, 111803 red 100%, 347 irr 0%
c otfs: str 112150, 0 bin 0%, 24 trn 0%, 112126 lrg 100%
c otfs: sub 3576, 3544 red 99%, 32 irr 1%
c otfs: sub 3576, 0 bin 0%, 0 trn 0%, 3576 lrg 100%
c phas: 1 computed, 149180 set, 0 pos (0%), 149180 neg (100%)
c prbs: 4 basic, 4089 probed, 392 failed, 0 lifted
c prbs: 5 simple, 258136 probed, 468 failed, 2 eqs
c prbs: 5 treelook, 32 probed, 879 failed, 0 lifted
c prom: 38568 locked 1% out of 4284942 tried
c prps: 2168600401 props, 82 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 10 count, 9118 quat, 1571 self1, 3 self2, 0 dup
c queu: 14 sorted, 25579099 next (958488 steps 0.04)
c queu: 899944237 enq (1068223983 steps 1.19), 712663829 deq 79%
c redc: 2256 clauses 32%, 6949 tried 0%, 339 sat 5%
c redc: 12597 lits 16%, 76355 tried 0%, 339 sat 0%
c redc: 371 times jump level reduced, 109.9 levels on average
c reds: 35 count, 68998.5 conflicts per reduce
c reds: 0 memlim 0%, 35 arith 100%
c reds: 1172607 collected 85%, 200774 retired 15%
c rmbd: 3238 removed, 2338 red 72%
c rsts: 12735 restarts 92%, 1164 skipped 8%
c rsts: 1164 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: 14 count, 13 confs 93%, 0 vars 0%
c simp: 0 its 0%, 1 bin 7%, 0 trns 0%
c subl: 2357118 count (5493185 tried 2.3), 888822 sub out of 2355458 (37.7%)
c swps: 8 count, 8 rounds, 452 queries (56.5/round)
c swps: 397 sat calls, 1 unsat (0.2% success rate)
c swps: 14126 decisions 35.6, 79 conflicts 0.2
c swps; 6236.2 avg class size, 250.0 avg environment size
c swps: 0 failed, 132 impls, 56 equivs
c swp0: 148 type 0 queries, 37 unsat (25.0%), 136 sat (91.9%)
c swp1: 304 type 1 queries, 115 unsat (37.8%), 260 sat (85.5%)
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: 55891146 calls to obtain time
c tops: 4897 fixed 3%, 0 its, 0.00 confs/it
c trds: 10 transitive reductions, 205 removed, 2 failed
c trds: 1069 nodes, 9248 edges, 29230151 steps
c trim: 14606299 words, 55.7 MB
c trnr: 10 count, 11 bin, 43215 trn, 317268811 steps
c unhd: 14 count, 14 rounds, 82462849 steps
c unhd: 416 non-trivial sccs of average size 2.0
c unhd: 2035 units, 2035 bin, 0 trn, 0 lrg
c unhd: 29 failed, 18 stamp, 0 lits, 1 bin, 1 trn, 0 lrg
c unhd: 37805 tauts, 1796 bin 5%, 3157 trn 8%, 4688 lrg 12%
c unhd: 37805 tauts, 28164 stamp 74%, 15327 red 41%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 472253 str, 2035 bin 0%, 2974 trn 1%, 467244 lrg 99%, 314061 red 67%
c vars: 118128 remaining 77% and 36181 removed 23% out of 154309
c vars: 4897 fixed 3%, 30959 eliminated 20%, 325 equivalent 0%
c vsts: 20256739058 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 9.4 search visits per propagation, 8248.9 per conflict
c wchs: 1660138938 pushed, 95448285 enlarged, 118 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2364576       1172607        200774     106627115      61401660       1631991
c 
c  0 0         12435   1       210   0         0   0  11087353  10   1481647   2     20149   1     0.3
c  1 5          3330   0       256   0      2339   1   5716486   5   1371713   2     12609   1     0.1
c  2 6         12948   1      2402   0      7193   4  16649455  16   7620149  12     81985   5     0.3
c  3 9         28677   1     10387   1     12393   6  20916126  20  13477144  22    112838   7     1.1
c  4 14        49754   2     25294   2     16581   8  23755991  22< 19925496  32<   149342   9     2.2
c  5 21        54892   2     34014   3     13312   7   8701750   8   6777392  11    123886   8     1.8
c  6 30        62780   3     45193   4      9507   5   3636624   3   2345555   4    100539   6     2.1
c  7 41       101295   4     80955   7      9038   5   3466105   3   1889959   3    106238   7<    3.2
c  8 54       203651   9    175771  15     10537   5<  4483879   4   2133630   3    172190  11     6.7
c  9 69       429622  18<   390056  33<    11677   6   3578688   3   1831002   3    268451  16    18.5
c 10 86       770513  33    339852  29     44268  22   3282098   3   1931572   3    396109  24    58.5
c 11 126      621628  26     66499   6     62214  31   1331245   1    605166   1     86769   5    77.2
c 12 230       13007   1      1711   0      1696   1     21244   0     11210   0       886   0     3.3
c 13 534          44   0         7   0        19   0        71   0        25   0         0   0     0.1
c 
c avg                  9.2           8.7           8.2           3.8           4.2           7.2
c std                  2.0           1.6           3.1           2.6           2.2           2.9
c 
c  106.237  11% bump
c   90.275   9% block
c   69.439   7% elim
c   54.200   5% probe
c   38.588   4% rescore
c   17.617   2% unhide
c   17.263   2% decide
c   11.954   1% sweep
c   11.812   1% bca
c   11.029   1% quatres
c 
c   16.827 < 1% rest (below)
c 
c   10.948   1% cce
c    2.984   0% ternres
c    2.133   0% gauss
c    0.618   0% transred
c    0.143   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    9.000   1% preprocessing     3%
c  293.156  29% inprocessing     97%
c ==================================
c  302.156  30% simplifying
c  695.927  70% search
c ==================================
c  998.086 100% all
c 
c       2414948 conflicts,        2419.6 confs/sec
c           740 ternaries,        3263.4 confs/ternary
c           890 binaries,         2713.4 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            35 reductions,          0.0 redus/sec,  68998.5 confs/reduction
c         12735 restarts,           12.8 rests/sec,    189.6 confs/restart
c      25579099 decisions,       25628.2 decis/sec,     10.6 decis/conflict
c    2168600401 propagations,  2172759.4 props/sec,     84.8 props/decision
c 
c 998.1 seconds, 321.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
