c launch: /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c host: atom08
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/manol-pipe-g10bid_i.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c no embedded options
c found 'p cnf 266405 792175' header
c read 266405 variables, 792175 clauses, 1848407 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 266404 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  266404   792174         0       0      0     0    0     0   44   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 1 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 1 out of 1 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 1 at-most-one constraints, 1 used 100%
c [card-1] exported 1 binary clauses, 1.0 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 266404 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 7402 variables
c [simpleprobe-1] 91801 variables remain 35% (167201 retained 65%)
c [simpleprobe-1] removed 7402 variables, found 953 hbrs, 86 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 83 failed, 201 tauts, 0 hbrs, 171 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 257663 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 64530 not tried 25% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 193123 = 75% variables out of 257663 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 313684 negative 95.8% of 327495 except 13811 4.2%
c [phase-count-1] 311324 positive 95.1% of 327495 except 16171 4.9%
c [phase-1] phase bias: 23065 positive 36%, 41475 negative 64%
c [sort-queue-1] sorted 64540 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 64540 (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 201864 variables 75.8% (64540 remain 24%)
c [simplification-1] removed 464679 irredundant clauses 58.7% (327495 remain 41%)
c [simplification-1] maximum reduction of 76% = max (76%, 59%)
c [simplification-1] large reduction 76% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  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    5.2   64539   327495        20      13      1    55    0     0   38   4%      0    0    0    0 24505%
c i    5.2   64527   327495        24      13      2    57    0     0   38   4%      0    0    0    0 24185%
c i    5.2   64524   327495        25      13      2    57    0     0   38   4%      0    0    0    0 24091%
c i    5.2   64516   327495        26      13      2    57    0     0   38   4%      0    0    0    0 23997%
c i    5.3   64514   327495        43      27      4    57    0     0   38   7%      0    0    0    0 23534%
c i    5.3   64507   327495        44      27      4    57    0     0   38   7%      0    0    0    0 23443%
c i    5.3   64502   327495        48      27      6    58    0     0   38   7%      0    0    0    0 23154%
c i    5.3   64495   327495        50      28      6    58    0     0   38   7%      0    0    0    0 23072%
c i    5.4   64490   327495       228     167     22    64    0     6   38   4%      0    6    3    0 18438%
c 
c [simplification-2] limit 1039 conflicts (hard 11000) hit after 1040 conflicts
c [decomp-3] removed 266 variables
c [simpleprobe-2] 22527 schedulable variables 35%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 2 variables
c [simpleprobe-2] 22546 variables remain 35% (41726 retained 65%)
c [simpleprobe-2] removed 2 variables, found 18 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 37858 literals 29%
c [treelook-1] scheduling used 300032 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 341768 steps
c [treelook-1] 37508 literals remain 29%
c [treelook-1] 32479 variables remain to probed next time 51%
c [decomp-5] removed 57 variables
c [treelook-1] removed 95 variables, found 354 hbrs
c [basicprobe-1] limit 2602720 based on 325340 irredundant clauses
c [basicprobe-1-0] 36557 probes remain 58% after last round
c [basicprobe-1-0] 76 units = 76 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 723 variables, found 5301 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 2 units, 25 failed, 192 tauts, 0 hbrs, 1830 literals
c [elim-2] 63333 variables 100% will be scheduled this time
c [elim-2] scheduled 63333 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 17112 not tried 27% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 26221 = 41% variables out of 63333 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 264606 negative 97.2% of 272264 except 7658 2.8%
c [phase-count-2] 261591 positive 96.1% of 272264 except 10673 3.9%
c [phase-2] phase bias: 0 positive 0%, 18 negative 100%
c [sort-queue-2] sorted 31813 enqueued variables after 1040 conflicts
c [score-dist-2] active 5314 (14%), one 0 (0%), zero 31813 (86%)
c [score-dist-2] max exp 506, different 10 (2%)
c [score-dist-2] median active exp 501, avg 500.9
c [simplification-2] removed 27352 variables 42.4% (37127 remain 14%)
c [simplification-2] removed 55231 irredundant clauses 16.9% (272264 remain 34%)
c [simplification-2] maximum reduction of 42% = max (42%, 17%)
c [simplification-2] large reduction 42% >= 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 13040 (soft 3040 + delta 10000)
c [simplification-2] new conflict limit 3040 (hard 13040)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.5   37126   272264      2579    1319     66  1013    5    94   38   5%     22   92   10    0 2720%
c i    9.5   37123   272264      2599    1333     67  1014    5    93   38   5%     22   92   11    0 2817%
c 
c [simplification-3] limit 3040 conflicts (hard 13040) hit after 3040 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 44 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 44 out of 44 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 46 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 20655 literals 28%
c [treelook-2] scheduling used 300011 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 347733 steps
c [treelook-2] 20501 literals remain 28%
c [treelook-2] 12859 variables remain to probed next time 35%
c [decomp-7] removed 25 variables
c [treelook-2] removed 86 variables, found 157 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 46 failed, 1041 tauts, 0 hbrs, 3615 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 36845 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 4544 not tried 12% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1856 = 5% variables out of 36845 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 26214 enqueued variables after 3040 conflicts
c [score-dist-3] active 8775 (25%), one 0 (0%), zero 26214 (75%)
c [score-dist-3] max exp 507, different 17 (3%)
c [score-dist-3] median active exp 500, avg 499.3
c [simplification-3] removed 2132 variables 5.7% (34989 remain 13%)
c [simplification-3] removed 9944 irredundant clauses 3.7% (262320 remain 33%)
c [simplification-3] maximum reduction of 6% = max (6%, 4%)
c [simplification-3] large reduction 6% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15040 (soft 5040 + delta 10000)
c [simplification-3] new conflict limit 5040 (hard 15040)
c 
c [simplification-4] limit 5040 conflicts (hard 15040) hit after 5041 conflicts
c [decomp-8] removed 22 variables
c [basicprobe-2] limit 3108624 penalty 0 = 0 + 0
c [basicprobe-2-0] 2319 probes remain 7% after last round
c [basicprobe-2-0] 242 units = 225 failed (93%) + 17 lifted (7%)
c [basicprobe-2-0] removed 908 variables, found 2508 hbrs
c [unhide-4] limit 124344 with penalty 0 = 0 + 0
c [unhide-4-4] 7 units, 20 failed, 206 tauts, 0 hbrs, 5475 literals
c [elim-4] 4253 variables 13% will be scheduled this time
c [elim-4] scheduled 4253 variables 13%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 99965472 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 4253 scheduled
c [elim-4] 2 < 1/100 * 4253 = 42 considered unsuccessful
c [sort-queue-4] sorted 23828 enqueued variables after 5041 conflicts
c [score-dist-4] active 10178 (30%), one 0 (0%), zero 23828 (70%)
c [score-dist-4] max exp 508, different 24 (5%)
c [score-dist-4] median active exp 498, avg 497.0
c [simplification-4] removed 983 variables 2.8% (34006 remain 13%)
c [simplification-4] removed 17663 irredundant clauses 6.7% (244657 remain 31%)
c [simplification-4] maximum reduction of 7% = max (3%, 7%)
c [simplification-4] large reduction 7% >= 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 17041 (soft 7041 + delta 10000)
c [simplification-4] new conflict limit 7041 (hard 17041)
c 
c [simplification-5] limit 7041 conflicts (hard 17041) hit after 7041 conflicts
c [quatres-1] found 29653 quaternary clauses 24% in total
c [quatres-1-1] added 3 double-self-subsuming ternary resolvents
c [quatres-1-2] added 355 single-self-subsuming ternary resolvents
c [quatres-1-2] added 8867 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 34006 free variables schedulable
c [ternres-1] 9486 ternary resolvents (173 bin, 9313 trn)
c [ternres-1] 1 variables remain 0% (34005 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 19930 xors of average arity 3.0
c [gauss-1] connected 59613 occurrences of 7365 variables (average 8.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 134 variables
c [simpleprobe-3] 11916 schedulable variables 35%
c [simpleprobe-3] limit 3347692 penalty 0 = 0 + 0
c [decomp-10] removed 7 variables
c [simpleprobe-3] 11967 variables remain 35% (21898 retained 65%)
c [simpleprobe-3] removed 7 variables, found 65 hbrs, 3 units
c [unhide-5] limit 167384 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 8 failed, 412 tauts, 0 hbrs, 2037 literals
c [transred-1] limit 836923 with penalty 0 = 0 + 0
c [transred-1] removed 162 transitive binary clauses
c [transred-1] found 1 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 33855 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 7281 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 28 (7%) of length 23
c [cce-1-1] eliminated 17 clauses out of 94 (18%) of length 21
c [cce-1-1] eliminated 15 clauses out of 137 (11%) of length 20
c [cce-1-1] eliminated 6 clauses out of 171 (4%) of length 19
c [cce-1-1] eliminated 18 clauses out of 237 (8%) of length 18
c [cce-1-1] eliminated 26 clauses out of 323 (8%) of length 17
c [cce-1-1] eliminated 53 clauses out of 394 (13%) of length 16
c [cce-1-1] eliminated 55 clauses out of 379 (15%) of length 15
c [cce-1-1] eliminated 92 clauses out of 568 (16%) of length 14
c [cce-1-1] eliminated 109 clauses out of 640 (17%) of length 13
c [cce-1-1] eliminated 143 clauses out of 969 (15%) of length 12
c [cce-1-1] eliminated 256 clauses out of 1848 (14%) of length 11
c [cce-1-1] eliminated 407 clauses out of 2400 (17%) of length 10
c [cce-1-1] eliminated 769 clauses out of 4269 (18%) of length 9
c [cce-1-1] eliminated 7 clauses out of 7498 (0%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1975 large clauses in 30000061 steps
c [cce-1-1] allowing another 15000030 steps for small clauses
c [cce-1-1] scheduling 106718 clauses = 29355 binary + 77363 ternary
c [cce-1-1] tried to eliminate 14465 small clauses 14%
c [cce-1-1] eliminated 130 binary clauses 0%
c [cce-1-1] eliminated 176 ternary clauses 0%
c [cce-1-1] eliminated 306 small clauses 0%
c [cce-1-1] eliminated 306 small clauses in 30000033 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2281 covered clauses in round 1
c [cce-1] eliminated 2281 covered clauses in TOTAL during 1 rounds
c [cce-1] 2281 < 1/100 * 236233 = 2362 considered unsuccessful
c [bca-1] limit of 10000000 steps and 468404 added (scaled 2)
c [bca-1] 51303 out of 66948 literals actually usable 77%
c [bca-1] added 107 blocked clauses in 164790 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 13349 pos 39.9% + 20124 neg 60.1% = 33473 sched 100.0% ret 0
c [sweep-1-1] 1005890 steps 71 queries 6942.34 avg class size
c [sweep-1-1] 2045 decisions 73 SAT calls 43.52 avg env size
c [sweep-1-1] 32555 variables remain 97% (905 retained 3%)
c [decomp-11] removed 54 variables
c [sweep-1-1] removed 54 vars (0 failed, 3 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 54 vars in TOTAL (1 rounds, 70 queries)
c [sort-queue-5] sorted 21030 enqueued variables after 7041 conflicts
c [score-dist-5] active 12389 (37%), one 0 (0%), zero 21030 (63%)
c [score-dist-5] max exp 507, different 31 (6%)
c [score-dist-5] median active exp 497, avg 495.1
c [simplification-5] removed 587 variables 1.7% (33419 remain 13%)
c [simplification-5] removed 11141 irredundant clauses 4.6% (233516 remain 29%)
c [simplification-5] maximum reduction of 5% = max (2%, 5%)
c [simplification-5] large reduction 5% >= 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 19041 (soft 9041 + delta 10000)
c [simplification-5] new conflict limit 9041 (hard 19041)
c 
c [simplification-6] limit 9041 conflicts (hard 19041) hit after 9041 conflicts
c [quatres-2] found 37378 quaternary clauses 29% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 194 single-self-subsuming ternary resolvents
c [quatres-2-2] added 4064 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 256 ternary resolvents (2 bin, 254 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 80 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 80 out of 80 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 1 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 16516 literals 25%
c [treelook-3] scheduling used 300484 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 303317 steps
c [treelook-3] 16445 literals remain 25%
c [treelook-3] 8872 variables remain to probed next time 27%
c [decomp-13] removed 2 variables
c [treelook-3] removed 18 variables, found 330 hbrs
c [unhide-6] limit 207039 with penalty 0 = 0 + 0
c [unhide-6-6] 2 units, 22 failed, 560 tauts, 0 hbrs, 2329 literals
c [transred-2] limit 1035197 with penalty 0 = 0 + 0
c [transred-2] removed 101 transitive binary clauses
c [transred-2] found 7 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 33276 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1562 blocked clauses
c [block-2] 1562 < 1/100 * 233058 = 2330 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 32878 variables 100%
c [elim-5] limit of 10351973 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 6926 not tried 21% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2414 = 7% variables out of 32878 scheduled
c [bca-2] limit of 10000000 steps and 451131 added (scaled 2)
c [bca-2] 45963 out of 60930 literals actually usable 75%
c [bca-2] added 40 blocked clauses in 153937 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 11193 pos 37.7% + 18478 neg 62.3% = 29671 sched 97.4% ret 793
c [sweep-2-1] 1001527 steps 149 queries 4095.54 avg class size
c [sweep-2-1] 3937 decisions 146 SAT calls 41.41 avg env size
c [sweep-2-1] 27334 variables remain 90% (3128 retained 10%)
c [decomp-14] removed 10 variables
c [sweep-2-1] removed 10 vars (0 failed, 2 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 10 vars in TOTAL (1 rounds, 148 queries)
c [sort-queue-6] sorted 18095 enqueued variables after 9041 conflicts
c [score-dist-6] active 12359 (41%), one 0 (0%), zero 18095 (59%)
c [score-dist-6] max exp 508, different 40 (8%)
c [score-dist-6] median active exp 492, avg 491.4
c [simplification-6] removed 2965 variables 8.9% (30454 remain 11%)
c [simplification-6] removed 8328 irredundant clauses 3.6% (225188 remain 28%)
c [simplification-6] maximum reduction of 9% = max (9%, 4%)
c [simplification-6] large reduction 9% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21041 (soft 11041 + delta 10000)
c [simplification-6] new conflict limit 11041 (hard 21041)
c 
c [simplification-7] limit 11041 conflicts (hard 21041) hit after 11041 conflicts
c [quatres-3] found 35708 quaternary clauses 28% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 95 single-self-subsuming ternary resolvents
c [quatres-3-2] added 3323 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 30454 free variables schedulable
c [ternres-3] 377 ternary resolvents (3 bin, 374 trn)
c [ternres-3] 17984 variables remain 59% (12470 retained 41%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 9696 xors of average arity 3.0
c [gauss-2] connected 29088 occurrences of 5233 variables (average 5.6)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 5958157 penalty 0 = 0 + 0
c [basicprobe-3-0] 2623 sched 9%, 30 failed, 6 lifted, 497 hbrs
c [decomp-16] removed 123 variables
c [basicprobe-3-1] 16160 sched 53%, 46 failed, 0 lifted, 707 hbrs
c [decomp-17] removed 100 variables
c [basicprobe-3-2] 16031 sched 53%, 7 failed, 0 lifted, 74 hbrs
c [decomp-18] removed 25 variables
c [basicprobe-3-3] 4354 probes remain 14% after last round
c [basicprobe-3-3] 113 units = 100 failed (88%) + 13 lifted (12%)
c [basicprobe-3-3] removed 274 variables, found 1349 hbrs
c [bate-1] eliminated 755 asymmetric tautologies during probing
c [unhide-7] limit 238326 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 2 failed, 265 tauts, 0 hbrs, 1504 literals
c [transred-3] limit 1191631 with penalty 0 = 0 + 0
c [transred-3] removed 125 transitive binary clauses
c [transred-3] found 2 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 29
c [cce-2-1] eliminated 1 clauses out of 25 (4%) of length 23
c [cce-2-1] eliminated 1 clauses out of 65 (2%) of length 22
c [cce-2-1] eliminated 1 clauses out of 67 (1%) of length 21
c [cce-2-1] eliminated 2 clauses out of 107 (2%) of length 20
c [cce-2-1] eliminated 7 clauses out of 159 (4%) of length 19
c [cce-2-1] eliminated 5 clauses out of 244 (2%) of length 18
c [cce-2-1] eliminated 3 clauses out of 307 (1%) of length 17
c [cce-2-1] eliminated 20 clauses out of 403 (5%) of length 16
c [cce-2-1] eliminated 29 clauses out of 434 (7%) of length 15
c [cce-2-1] eliminated 31 clauses out of 642 (5%) of length 14
c [cce-2-1] eliminated 48 clauses out of 727 (7%) of length 13
c [cce-2-1] eliminated 99 clauses out of 1152 (9%) of length 12
c [cce-2-1] eliminated 140 clauses out of 2019 (7%) of length 11
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 388 large clauses in 15001211 steps
c [cce-2-1] allowing another 7500605 steps for small clauses
c [cce-2-1] scheduling 97611 clauses = 25633 binary + 71978 ternary
c [cce-2-1] tried to eliminate 6075 small clauses 6%
c [cce-2-1] eliminated 25 binary clauses 0%
c [cce-2-1] eliminated 51 ternary clauses 0%
c [cce-2-1] eliminated 76 small clauses 0%
c [cce-2-1] eliminated 128 small clauses in 15002405 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 516 covered clauses in round 1
c [cce-2] eliminated 516 covered clauses in TOTAL during 1 rounds
c [cce-2] 516 < 1/100 * 220038 = 2200 considered unsuccessful
c [elim-6] 6790 variables 23% will be scheduled this time
c [elim-6] scheduled 6790 variables 23%
c [elim-6] limit of 23832631 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 2088 not tried 7% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 14 = 0% variables out of 6790 scheduled
c [elim-6] 14 < 1/100 * 6790 = 67 considered unsuccessful
c [bca-3] limit of 10000000 steps and 439047 added (scaled 2)
c [bca-3] 44018 out of 60326 literals actually usable 73%
c [bca-3] added 9 blocked clauses in 150712 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 10362 pos 38.3% + 16727 neg 61.7% = 27089 sched 89.8% ret 3073
c [sweep-3-1] 1003968 steps 150 queries 4444.59 avg class size
c [sweep-3-1] 4109 decisions 150 SAT calls 39.57 avg env size
c [sweep-3-1] 25133 variables remain 83% (5029 retained 17%)
c [decomp-19] removed 24 variables
c [sweep-3-1] removed 24 vars (0 failed, 3 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 24 vars in TOTAL (1 rounds, 149 queries)
c [sort-queue-7] sorted 17455 enqueued variables after 11041 conflicts
c [score-dist-7] active 12683 (42%), one 0 (0%), zero 17455 (58%)
c [score-dist-7] max exp 508, different 47 (9%)
c [score-dist-7] median active exp 489, avg 488.4
c [simplification-7] removed 316 variables 1.0% (30138 remain 11%)
c [simplification-7] removed 6010 irredundant clauses 2.7% (219178 remain 28%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 5000
c [simplification-7] penalized conflict interval 5000 = 1 * 5000
c [simplification-7] hard conflict limit 26041 (soft 16041 + delta 10000)
c [simplification-7] new conflict limit 16041 (hard 26041)
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   25.0   30137   219178     13582   21189   8439  2454   12   156   38   8%    144  134   11    2  540%
c 
c [simplification-8] limit 16041 conflicts (hard 26041) hit after 16042 conflicts
c [quatres-4] found 38210 quaternary clauses 30% in total
c [quatres-4-2] added 77 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1792 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 17793 schedulable variables 59%
c [ternres-4] 795 ternary resolvents (9 bin, 786 trn)
c [ternres-4] 5000 variables remain 17% (25137 retained 83%)
c [decomp-20] removed 27 variables
c [simpleprobe-4] 10637 schedulable variables 35%
c [simpleprobe-4] limit 6515275 penalty 0 = 0 + 0
c [simpleprobe-4] 7672 variables remain 25% (22439 retained 75%)
c [simpleprobe-4] removed 0 variables, found 77 hbrs, 0 units
c [unhide-8] limit 325763 with penalty 0 = 0 + 0
c [unhide-8-8] 6 units, 5 failed, 359 tauts, 0 hbrs, 3790 literals
c [transred-4] limit 1628818 with penalty 0 = 0 + 0
c [transred-4] removed 76 transitive binary clauses
c [transred-4] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 30097 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1183 blocked clauses
c [block-3] 1183 < 1/100 * 218962 = 2189 considered unsuccessful
c [bca-4] limit of 10000000 steps and 435910 added (scaled 2)
c [bca-4] 41489 out of 59872 literals actually usable 69%
c [bca-4] added 0 blocked clauses in 147782 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 9661 pos 38.7% + 15285 neg 61.3% = 24946 sched 83.3% ret 4989
c [sweep-4-1] 1003912 steps 161 queries 4944.75 avg class size
c [sweep-4-1] 3999 decisions 156 SAT calls 35.65 avg env size
c [sweep-4-1] 23408 variables remain 78% (6527 retained 22%)
c [decomp-22] removed 21 variables
c [sweep-4-1] removed 21 vars (0 failed, 4 eqs, 5 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 21 vars in TOTAL (1 rounds, 160 queries)
c [sort-queue-8] sorted 15596 enqueued variables after 16042 conflicts
c [score-dist-8] active 14318 (48%), one 0 (0%), zero 15596 (52%)
c [score-dist-8] max exp 508, different 64 (13%)
c [score-dist-8] median active exp 492, avg 485.0
c [simplification-8] removed 223 variables 0.7% (29914 remain 11%)
c [simplification-8] removed 1556 irredundant clauses 0.7% (217622 remain 27%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-8] new conflict interval 15000
c [simplification-8] penalized conflict interval 15000 = 1 * 15000
c [simplification-8] hard conflict limit 41042 (soft 31042 + delta 10000)
c [simplification-8] new conflict limit 31042 (hard 41042)
c 
c [simplification-9] limit 31042 conflicts (hard 41042) hit after 31043 conflicts
c [quatres-5] found 40336 quaternary clauses 31% in total
c [quatres-5-1] added 3 double-self-subsuming ternary resolvents
c [quatres-5-2] added 55 single-self-subsuming ternary resolvents
c [quatres-5-2] added 1018 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] 4963 schedulable variables 17%
c [ternres-5] 1784 ternary resolvents (78 bin, 1706 trn)
c [ternres-5] 13 variables remain 0% (29901 retained 100%)
c [decomp-23] removed 8 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 13187 literals 22%
c [treelook-4] scheduling used 300027 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 324674 steps
c [treelook-4] 13053 literals remain 22%
c [treelook-4] 6287 variables remain to probed next time 21%
c [treelook-4] removed 0 variables, found 211 hbrs
c [unhide-9] limit 545915 with penalty 0 = 0 + 0
c [unhide-9-9] 0 units, 1 failed, 322 tauts, 0 hbrs, 8849 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 80 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 29904 variables 100%
c [elim-7] limit of 27295780 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 2356 not tried 8% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 565 = 2% variables out of 29904 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 10922 pos 47.7% + 11955 neg 52.3% = 22877 sched 78.0% ret 6462
c [sweep-5-1] 10002428 steps 1597 queries 984.41 avg class size
c [sweep-5-1] 34691 decisions 1581 SAT calls 31.02 avg env size
c [sweep-5-1] 9184 variables remain 31% (20106 retained 69%)
c [decomp-25] removed 105 variables
c [sweep-5-1] removed 105 vars (0 failed, 32 eqs, 23 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 105 vars in TOTAL (1 rounds, 1596 queries)
c [sort-queue-9] sorted 13506 enqueued variables after 31043 conflicts
c [score-dist-9] active 15728 (54%), one 0 (0%), zero 13506 (46%)
c [score-dist-9] max exp 508, different 119 (23%)
c [score-dist-9] median active exp 481, avg 466.3
c [simplification-9] removed 680 variables 2.3% (29234 remain 11%)
c [simplification-9] removed 2606 irredundant clauses 1.2% (215016 remain 27%)
c [simplification-9] maximum reduction of 2% = max (2%, 1%)
c [simplification-9] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-9] new conflict interval 21666
c [simplification-9] penalized conflict interval 21666 = 1 * 21666
c [simplification-9] hard conflict limit 63542 (soft 52709 + delta 10833)
c [simplification-9] new conflict limit 52709 (hard 63542)
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   34.5   29233   215016     32299   36114  10331  2337   16   127   41  12%    231   77   13    5  279%
c 
c [simplification-10] limit 52709 conflicts (hard 63542) hit after 52710 conflicts
c [quatres-6] found 39544 quaternary clauses 30% in total
c [quatres-6-1] removed 13 duplicate quaternary clauses
c [quatres-6-2] added 691 single-self-subsuming ternary resolvents
c [quatres-6-2] added 481 quaternary resolvents
c [ternres-6] limit 4024908 with penalty 0 = 0 + 0
c [ternres-6] 13 schedulable variables 0%
c [ternres-6] 1416 ternary resolvents (52 bin, 1364 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 251556 penalty 3 = 3 + 0
c [card-4] found 72 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 251556 for elimination
c [card-4] 72 out of 72 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 4400 xors of average arity 3.0
c [gauss-3] connected 13195 occurrences of 3361 variables (average 3.9)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 5 variables
c [basicprobe-4] limit 20124541 penalty 0 = 0 + 0
c [basicprobe-4-0] 4362 sched 15%, 13 failed, 0 lifted, 301 hbrs
c [decomp-27] removed 39 variables
c [basicprobe-4-1] 15409 sched 53%, 14 failed, 0 lifted, 353 hbrs
c [decomp-28] removed 42 variables
c [basicprobe-4-2] 15381 sched 53%, 4 failed, 0 lifted, 50 hbrs
c [decomp-29] removed 10 variables
c [basicprobe-4-3] 15380 sched 53%, 0 failed, 0 lifted, 12 hbrs
c [decomp-30] removed 1 variables
c [basicprobe-4-4] 15379 sched 53%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-4-5] 15379 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-5] fully completed probing
c [basicprobe-4-5] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-4-5] removed 92 variables, found 729 hbrs
c [bate-2] eliminated 562 asymmetric tautologies during probing
c [unhide-10] limit 804981 with penalty 0 = 0 + 0
c [unhide-10-10] 0 units, 0 failed, 1237 tauts, 0 hbrs, 22978 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 122 transitive binary clauses
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 31
c [cce-3-1] eliminated 3 clauses out of 9 (33%) of length 29
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-3-1] eliminated 2 clauses out of 8 (25%) of length 27
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 26
c [cce-3-1] eliminated 2 clauses out of 13 (15%) of length 25
c [cce-3-1] eliminated 8 clauses out of 33 (24%) of length 23
c [cce-3-1] eliminated 5 clauses out of 64 (8%) of length 21
c [cce-3-1] eliminated 1 clauses out of 131 (1%) of length 20
c [cce-3-1] eliminated 8 clauses out of 177 (5%) of length 19
c [cce-3-1] eliminated 6 clauses out of 283 (2%) of length 18
c [cce-3-1] eliminated 23 clauses out of 367 (6%) of length 17
c [cce-3-1] eliminated 22 clauses out of 397 (6%) of length 16
c [cce-3-1] eliminated 21 clauses out of 489 (4%) of length 15
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 104 large clauses in 7500583 steps
c [cce-3-1] allowing another 3750291 steps for small clauses
c [cce-3-1] scheduling 33976 clauses = 24543 binary + 9433 ternary
c [cce-3-1] tried to eliminate 2670 small clauses 8%
c [cce-3-1] eliminated 63 binary clauses 0%
c [cce-3-1] eliminated 53 ternary clauses 1%
c [cce-3-1] eliminated 116 small clauses 0%
c [cce-3-1] eliminated 116 small clauses in 7500175 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 220 covered clauses in round 1
c [cce-3] eliminated 220 covered clauses in TOTAL during 1 rounds
c [cce-3] 220 < 1/100 * 212996 = 2129 considered unsuccessful
c [elim-8] 2057 variables 7% will be scheduled this time
c [elim-8] scheduled 2057 variables 7%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1609963300 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 116239083 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 2057 scheduled
c [bca-5] limit of 10000000 steps and 423950 added (scaled 2)
c [bca-5] 36336 out of 58270 literals actually usable 62%
c [bca-5] added 5 blocked clauses in 160783 steps
c [sweep-6] limit 1207472 penalty 0 = 0 + 0
c [sweep-6-1] 4151 pos 45.4% + 4995 neg 54.6% = 9146 sched 31.4% ret 19988
c [sweep-6-1] 1209063 steps 307 queries 2283.69 avg class size
c [sweep-6-1] 5243 decisions 293 SAT calls 25.27 avg env size
c [sweep-6-1] 8447 variables remain 29% (20683 retained 71%)
c [decomp-32] removed 19 variables
c [sweep-6-1] removed 19 vars (0 failed, 19 eqs, 13 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 19 vars in TOTAL (1 rounds, 306 queries)
c [sort-queue-10] sorted 13262 enqueued variables after 52710 conflicts
c [score-dist-10] active 15853 (54%), one 0 (0%), zero 13262 (46%)
c [score-dist-10] max exp 508, different 195 (38%)
c [score-dist-10] median active exp 404, avg 413.5
c [simplification-10] removed 116 variables 0.4% (29115 remain 11%)
c [simplification-10] removed 3434 irredundant clauses 1.6% (211582 remain 27%)
c [simplification-10] maximum reduction of 2% = max (0%, 2%)
c [simplification-10] geometric conflict interval increment 7222 = 21666 / 3
c [simplification-10] new conflict interval 28888
c [simplification-10] penalized conflict interval 28888 = 1 * 28888
c [simplification-10] hard conflict limit 96042 (soft 81598 + delta 14444)
c [simplification-10] new conflict limit 81598 (hard 96042)
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 -   47.6   29115   211582     79319   38042  12046  2451   21   104   39  20%    492   25   21   12  179%
c 
c [simplification-11] limit 81598 conflicts (hard 96042) hit after 81598 conflicts
c [quatres-7] found 39784 quaternary clauses 30% in total
c [quatres-7-1] removed 43 duplicate quaternary clauses
c [quatres-7-1] added 3 double-self-subsuming ternary resolvents
c [quatres-7-2] added 113 single-self-subsuming ternary resolvents
c [quatres-7-2] added 293 quaternary resolvents
c [ternres-7] limit 5767842 with penalty 0 = 0 + 0
c [ternres-7] all 29115 free variables schedulable
c [ternres-7] 501 ternary resolvents (16 bin, 485 trn)
c [ternres-7] 12197 variables remain 42% (16918 retained 58%)
c [decomp-33] removed 1 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 91 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 29114 variables 100%
c [block-4] limit of 14419605 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 999 blocked clauses
c [block-4] 999 < 1/100 * 211525 = 2115 considered unsuccessful
c [bca-6] limit of 10000000 steps and 421632 added (scaled 2)
c [bca-6] 38727 out of 57872 literals actually usable 67%
c [bca-6] added 1 blocked clauses in 157624 steps
c [sweep-7] limit 1730352 penalty 0 = 0 + 0
c [sweep-7-1] 3893 pos 46.6% + 4459 neg 53.4% = 8352 sched 28.9% ret 20583
c [sweep-7-1] 1735644 steps 459 queries 1910.77 avg class size
c [sweep-7-1] 8356 decisions 457 SAT calls 24.81 avg env size
c [sweep-7-1] 7249 variables remain 25% (21683 retained 75%)
c [decomp-34] removed 4 variables
c [sweep-7-1] removed 4 vars (0 failed, 2 eqs, 0 impls)
c [sweep-7] 4 < 1/1000 * 28935 = 28 considered unsuccessful
c [sweep-7] removed 4 vars in TOTAL (1 rounds, 458 queries)
c [sort-queue-11] sorted 12905 enqueued variables after 81598 conflicts
c [score-dist-11] active 16026 (55%), one 0 (0%), zero 12905 (45%)
c [score-dist-11] max exp 509, different 285 (56%)
c [score-dist-11] median active exp 301, avg 346.9
c [simplification-11] removed 184 variables 0.6% (28931 remain 11%)
c [simplification-11] removed 1114 irredundant clauses 0.5% (210468 remain 27%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 14444 = 28888 / 2
c [simplification-11] new conflict interval 43332
c [simplification-11] penalized conflict interval 43332 = 1 * 43332
c [simplification-11] hard conflict limit 146596 (soft 124930 + delta 21666)
c [simplification-11] new conflict limit 124930 (hard 146596)
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 -   56.5   28931   210468    129550   49901  13120  2356   18    74   39  24%    777  -20   27   15  179%
c 
c [simplification-12] limit 124930 conflicts (hard 146596) hit after 146596 conflicts
c [quatres-8] found 40801 quaternary clauses 29% in total
c [quatres-8-1] removed 28 duplicate quaternary clauses
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 40 single-self-subsuming ternary resolvents
c [quatres-8-2] added 99 quaternary resolvents
c [ternres-8] limit 8602583 with penalty 0 = 0 + 0
c [ternres-8] 12120 schedulable variables 42%
c [ternres-8] 1382 ternary resolvents (76 bin, 1306 trn)
c [ternres-8] 3 variables remain 0% (28928 retained 100%)
c [decomp-35] removed 11 variables
c [simpleprobe-5] 7327 schedulable variables 25%
c [simpleprobe-5] limit 17205167 penalty 1 = 1 + 0
c [decomp-36] removed 5 variables
c [simpleprobe-5] 3269 variables remain 11% (25646 retained 89%)
c [simpleprobe-5] removed 5 variables, found 163 hbrs, 0 units
c [unhide-11] limit 860258 with penalty 1 = 1 + 0
c [unhide-11-11] 0 units, 0 failed, 220 tauts, 0 hbrs, 44886 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 140 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 28915 variables 100%
c [elim-9] limit of 86025836 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 284 not tried 1% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 536 = 2% variables out of 28915 scheduled
c [bca-7] limit of 10000000 steps and 419037 added (scaled 2)
c [bca-7] 37532 out of 56760 literals actually usable 66%
c [bca-7] added 12 blocked clauses in 177006 steps
c [sort-queue-12] sorted 14613 enqueued variables after 146596 conflicts
c [score-dist-12] active 13766 (49%), one 2421 (9%), zero 12192 (43%)
c [score-dist-12] max exp 510, different 367 (72%)
c [score-dist-12] median active exp 286, avg 269.1
c [simplification-12] removed 552 variables 1.9% (28379 remain 11%)
c [simplification-12] removed 1240 irredundant clauses 0.6% (209228 remain 26%)
c [simplification-12] maximum reduction of 2% = max (2%, 1%)
c [simplification-12] geometric conflict interval increment 14444 = 43332 / 3
c [simplification-12] new conflict interval 57776
c [simplification-12] penalized conflict interval 57776 = 1 * 57776
c [simplification-12] hard conflict limit 233260 (soft 204372 + delta 28888)
c [simplification-12] new conflict limit 204372 (hard 233260)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   64.1   28379   209228    176812   58695  13178  1985    8   186   40   4%    904   25    8   13   61%
c -   68.9   28379   209228    217459   61937  13473  1996   10    32   41  31%    959  -91    9   12   70%
c 
c [simplification-13] limit 204372 conflicts (hard 233260) hit after 233260 conflicts
c [quatres-9] found 40397 quaternary clauses 27% in total
c [quatres-9-1] added 3 double-self-subsuming ternary resolvents
c [quatres-9-2] added 38 single-self-subsuming ternary resolvents
c [quatres-9-2] added 187 quaternary resolvents
c [ternres-9] limit 11459593 with penalty 0 = 0 + 0
c [ternres-9] 3 schedulable variables 0%
c [ternres-9] 831 ternary resolvents (24 bin, 807 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-37] removed 2 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 80 transitive binary clauses
c [elim-10] 283 variables 1% will be scheduled this time
c [elim-10] scheduled 283 variables 1%
c [elim-10] limit of 229191860 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 138680113 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 0 = 0% variables out of 283 scheduled
c [bca-8] limit of 10000000 steps and 417321 added (scaled 2)
c [bca-8] 36766 out of 56756 literals actually usable 65%
c [bca-8] added 9 blocked clauses in 189054 steps
c [sweep-8] limit 1718938 penalty 1 = 1 + 0
c [sweep-8-1] 3198 pos 45.0% + 3911 neg 55.0% = 7109 sched 25.1% ret 21268
c [sweep-8-1] 1720066 steps 521 queries 1638.92 avg class size
c [sweep-8-1] 8642 decisions 520 SAT calls 22.98 avg env size
c [sweep-8-1] 5962 variables remain 21% (22415 retained 79%)
c [decomp-38] removed 1 variables
c [sweep-8-1] removed 1 vars (0 failed, 2 eqs, 3 impls)
c [sweep-8] 1 < 1/1000 * 28377 = 28 considered unsuccessful
c [sweep-8] removed 1 vars in TOTAL (1 rounds, 520 queries)
c [sort-queue-13] sorted 16263 enqueued variables after 233260 conflicts
c [score-dist-13] active 12113 (43%), one 4907 (17%), zero 11356 (40%)
c [score-dist-13] max exp 509, different 321 (63%)
c [score-dist-13] median active exp 312, avg 340.8
c [simplification-13] removed 3 variables 0.0% (28376 remain 11%)
c [simplification-13] removed 861 irredundant clauses 0.4% (208367 remain 26%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 57776
c [simplification-13] new conflict interval 115552
c [simplification-13] penalized conflict interval 115552 = 1 * 115552
c [simplification-13] hard conflict limit 406588 (soft 348812 + delta 57776)
c [simplification-13] new conflict limit 348812 (hard 406588)
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   75.8   28375   208367    254207   94176  14492  1977   10   289   48   3%    987  185   11   12   91%
c i   76.7   28307   208367    258261   97376  14571  1985   12   208   48   6%  -2255   95   14   12  117%
c -   77.1   28307   208367    260648   66697  14645  1988   11   173   41   6%  -2251   58   11   12   89%
c i   77.7   28306   208367    265832   70818  14756  1990   10   108   44   9%  -2014   -9   13   12  112%
c i   77.7   28299   208367    266062   71020  14753  1992   10   106   44  10%  -2027  -10   13   12  110%
c i   80.0   28298   208367    287286   89060  15064  2010   11    65   46  16%  -1255  -50   11   11  102%
c -   83.5   28298   208367    311892   75332  15367  2029   10   207   42   5%   -773   81    9   11   83%
c i   85.9   28297   208367    328495   89054  15572  2042   10   145   46   7%   -371   -7    7   11   68%
c i   89.0   28296   208367    343899  101624  15720  2051    9   167   62   6%   -596   11   12   10  116%
c i   90.8   28294   208367    350567  107103  15853  2064   13   142   63   9%   -660  -14   13   11  120%
c i   90.9   28290   208367    350908  107338  15867  2065   13   138   63  10%   -680  -18   12   11  110%
c i   90.9   28284   208367    351283  107674  15871  2066   13   130   63  10%   -695  -25   10   11   92%
c i   90.9   28278   208367    351307  107691  15874  2068   13   129   63  10%   -696  -26    9   11   88%
c i   91.0   28271   208367    351501  107828  15883  2068   13   124   63  10%   -701  -31    7   11   65%
c -   93.4   28247   208367    363252   82719  16104  2087   13   139   56   9%   -463  -17   17   11  155%
c i   97.2   28246   208367    385517  101398  16371  2112   10   162   61   6%    -35  -19   14   11  131%
c i   99.6   28243   208367    396927  110862  16589  2125   11   149   62   7%   -319  -29   11   11  107%
c i  100.0   28241   208367    398811  112354  16627  2131   11   164   62   6%   -428  -14    9   11   88%
c 
c [simplification-14] limit 348812 conflicts (hard 406588) hit after 406589 conflicts
c [quatres-10] found 40548 quaternary clauses 25% in total
c [quatres-10-1] added 8 double-self-subsuming ternary resolvents
c [quatres-10-2] added 2322 single-self-subsuming ternary resolvents
c [quatres-10-2] added 292 quaternary resolvents
c [ternres-10] limit 20308637 with penalty 0 = 0 + 0
c [ternres-10] all 28235 free variables schedulable
c [ternres-10] 3315 ternary resolvents (41 bin, 3274 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 507715 penalty 3 = 3 + 0
c [gauss-4] extracted 3986 xors of average arity 3.0
c [gauss-4] connected 11851 occurrences of 3177 variables (average 3.7)
c [gauss-4] limit 507715 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-39] removed 339 variables
c [treelook-5] limit 1015431 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 19552 literals 35%
c [treelook-5] scheduling used 771972 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1015431 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 1026759 steps
c [treelook-5] 19138 literals remain 34%
c [treelook-5] 5753 variables remain to probed next time 21%
c [decomp-40] removed 58 variables
c [treelook-5] removed 77 variables, found 627 hbrs
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 233 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 126928985 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 5 clauses out of 177 (3%) of length 19
c [cce-4-1] eliminated 9 clauses out of 272 (3%) of length 18
c [cce-4-1] eliminated 20 clauses out of 326 (6%) of length 17
c [cce-4-1] eliminated 15 clauses out of 342 (4%) of length 16
c [cce-4-1] eliminated 19 clauses out of 401 (5%) of length 15
c [cce-4-1] eliminated 38 clauses out of 575 (7%) of length 14
c [cce-4-1] eliminated 34 clauses out of 656 (5%) of length 13
c [cce-4-1] eliminated 46 clauses out of 1021 (5%) of length 12
c [cce-4-1] eliminated 55 clauses out of 1601 (3%) of length 11
c [cce-4-1] eliminated 201 clauses out of 2239 (9%) of length 10
c [cce-4-1] eliminated 310 clauses out of 3471 (9%) of length 9
c [cce-4-1] eliminated 1076 clauses out of 6847 (16%) of length 8
c [cce-4-1] eliminated 1937 clauses out of 14263 (14%) of length 7
c [cce-4-1] eliminated 1955 clauses out of 29619 (7%) of length 6
c [cce-4-1] eliminated 1450 clauses out of 18567 (8%) of length 5
c [cce-4-1] eliminated 891 clauses out of 20802 (4%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 8061 large clauses in 126928985 steps
c [cce-4-1] allowing another 63464492 steps for small clauses
c [cce-4-1] scheduling 92064 clauses = 23631 binary + 68433 ternary
c [cce-4-1] tried to eliminate 83791 small clauses 91%
c [cce-4-1] eliminated 254 binary clauses 1%
c [cce-4-1] eliminated 701 ternary clauses 1%
c [cce-4-1] eliminated 955 small clauses 1%
c [cce-4-1] eliminated 955 small clauses in 126930092 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 9016 covered clauses in round 1
c [cce-4] eliminated 9016 covered clauses in TOTAL during 1 rounds
c [bca-9] limit of 10000000 steps and 389231 added (scaled 2)
c [bca-9] 30777 out of 55640 literals actually usable 55%
c [bca-9] added 14 blocked clauses in 205770 steps
c [sort-queue-14] sorted 13708 enqueued variables after 406589 conflicts
c [score-dist-14] active 14111 (51%), one 3621 (13%), zero 10087 (36%)
c [score-dist-14] max exp 509, different 381 (75%)
c [score-dist-14] median active exp 463, avg 429.6
c [simplification-14] removed 416 variables 1.5% (27819 remain 10%)
c [simplification-14] removed 14047 irredundant clauses 6.7% (194320 remain 25%)
c [simplification-14] maximum reduction of 7% = max (1%, 7%)
c [simplification-14] large reduction 7% >= 5% limit
c [simplification-14] next conflict interval 4065 = min (406589/100, 115552)
c [simplification-14] penalized conflict interval 4065 = 1 * 4065
c [simplification-14] hard conflict limit 420654 (soft 410654 + delta 10000)
c [simplification-14] new conflict limit 410654 (hard 420654)
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  105.3   27818   194319    408999  113269  21437  2784   10    90   52  11%   -270  -78   11   10  108%
c i  107.4   27817   194319    417987  121112  21550  2794   15   110   53  13%   -245  -50   11   11   97%
c -  107.7   27812   194319    419248   86734  21575  2794   14   119   43  12%   -319  -40   11   11  104%
c 
c [simplification-15] limit 410654 conflicts (hard 420654) hit after 420654 conflicts
c [quatres-11] found 38829 quaternary clauses 25% in total
c [quatres-11-1] removed 53 duplicate quaternary clauses
c [quatres-11-1] added 3 double-self-subsuming ternary resolvents
c [quatres-11-2] added 179 single-self-subsuming ternary resolvents
c [quatres-11-2] added 149 quaternary resolvents
c [ternres-11] limit 21401818 with penalty 0 = 0 + 0
c [ternres-11] all 27812 free variables schedulable
c [ternres-11] 8179 ternary resolvents (1072 bin, 7107 trn)
c [ternres-11] 14 variables remain 0% (27798 retained 100%)
c [card-5] limit 668806 penalty 4 = 4 + 0
c [card-5] found 107 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 668806 for elimination
c [card-5] 107 out of 107 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-41] removed 107 variables
c [basicprobe-5] limit 107009094 penalty 0 = 0 + 0
c [basicprobe-5-0] 14523 sched 53%, 42 failed, 3 lifted, 1413 hbrs
c [decomp-42] removed 162 variables
c [basicprobe-5-1] 14395 sched 52%, 6 failed, 0 lifted, 252 hbrs
c [decomp-43] removed 18 variables
c [basicprobe-5-2] 14364 sched 52%, 1 failed, 0 lifted, 42 hbrs
c [decomp-44] removed 7 variables
c [basicprobe-5-3] 14361 sched 52%, 1 failed, 0 lifted, 7 hbrs
c [decomp-45] removed 3 variables
c [basicprobe-5-4] 14362 sched 52%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-5] 14362 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-5] fully completed probing
c [basicprobe-5-5] 53 units = 50 failed (94%) + 3 lifted (6%)
c [basicprobe-5-5] removed 190 variables, found 1715 hbrs
c [bate-3] eliminated 96 asymmetric tautologies during probing
c [unhide-12] limit 1070090 with penalty 2 = 2 + 0
c [unhide-12-12] 0 units, 0 failed, 4757 tauts, 0 hbrs, 19392 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 312 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 27522 variables 100%
c [block-5] limit of 26752273 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 14221 blocked clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 25796 variables 100%
c [elim-11] limit of 214018189 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 2451 variables 10% in round 1 in 111530903 steps
c [elim-11-1] backward subsumption/strengthening limit 102487286
c [elim-11-1-1] backward checking 6866 touched variables 27%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 5 clauses in 6095832 steps
c [elim-11-1] rescheduled 17 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 9358809 steps
c [elim-11-2] backward subsumption/strengthening limit 9358800
c [elim-11-2-1] backward checking 13 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 327208 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 2452 = 10% variables out of 25796 scheduled
c [bca-10] limit of 10000000 steps and 343798 added (scaled 2)
c [bca-10] 27688 out of 46690 literals actually usable 59%
c [bca-10] added 41 blocked clauses in 154637 steps
c [sort-queue-15] sorted 10467 enqueued variables after 420654 conflicts
c [score-dist-15] active 12877 (55%), one 2544 (11%), zero 7923 (34%)
c [score-dist-15] max exp 508, different 376 (74%)
c [score-dist-15] median active exp 488, avg 445.2
c [simplification-15] removed 4468 variables 16.1% (23344 remain 9%)
c [simplification-15] removed 22719 irredundant clauses 11.7% (171600 remain 22%)
c [simplification-15] maximum reduction of 16% = max (16%, 12%)
c [simplification-15] large reduction 16% >= 5% limit
c [simplification-15] next conflict interval 4206 = min (420654/100, 115552)
c [simplification-15] penalized conflict interval 4206 = 1 * 4206
c [simplification-15] hard conflict limit 434860 (soft 424860 + delta 10000)
c [simplification-15] new conflict limit 424860 (hard 434860)
c 
c [simplification-16] limit 424860 conflicts (hard 434860) hit after 434860 conflicts
c [quatres-12] found 29048 quaternary clauses 21% in total
c [quatres-12-1] removed 21 duplicate quaternary clauses
c [quatres-12-1] added 5 double-self-subsuming ternary resolvents
c [quatres-12-2] added 164 single-self-subsuming ternary resolvents
c [quatres-12-2] added 318 quaternary resolvents
c [ternres-12] limit 22069947 with penalty 0 = 0 + 0
c [ternres-12] 14 schedulable variables 0%
c [ternres-12] 3532 ternary resolvents (128 bin, 3404 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-47] removed 28 variables
c [simpleprobe-6] 2631 schedulable variables 11%
c [simpleprobe-6] limit 88279789 penalty 0 = 0 + 0
c [decomp-48] removed 42 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 42 variables, found 793 hbrs, 8 units
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 301 transitive binary clauses
c [cce-5] limit of 27587434 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-5-1] eliminated 2 clauses out of 17 (12%) of length 26
c [cce-5-1] eliminated 8 clauses out of 21 (38%) of length 25
c [cce-5-1] eliminated 2 clauses out of 18 (11%) of length 24
c [cce-5-1] eliminated 1 clauses out of 25 (4%) of length 23
c [cce-5-1] eliminated 2 clauses out of 61 (3%) of length 22
c [cce-5-1] eliminated 4 clauses out of 65 (6%) of length 21
c [cce-5-1] eliminated 3 clauses out of 147 (2%) of length 20
c [cce-5-1] eliminated 9 clauses out of 191 (5%) of length 19
c [cce-5-1] eliminated 8 clauses out of 298 (3%) of length 18
c [cce-5-1] eliminated 11 clauses out of 326 (3%) of length 17
c [cce-5-1] eliminated 19 clauses out of 360 (5%) of length 16
c [cce-5-1] eliminated 16 clauses out of 438 (4%) of length 15
c [cce-5-1] eliminated 18 clauses out of 564 (3%) of length 14
c [cce-5-1] eliminated 22 clauses out of 684 (3%) of length 13
c [cce-5-1] eliminated 66 clauses out of 1091 (6%) of length 12
c [cce-5-1] eliminated 56 clauses out of 1544 (4%) of length 11
c [cce-5-1] eliminated 77 clauses out of 2122 (4%) of length 10
c [cce-5-1] eliminated 35 clauses out of 3483 (1%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 360 large clauses in 27587481 steps
c [cce-5-1] allowing another 13793740 steps for small clauses
c [cce-5-1] scheduling 76385 clauses = 19501 binary + 56884 ternary
c [cce-5-1] tried to eliminate 17957 small clauses 24%
c [cce-5-1] eliminated 85 binary clauses 0%
c [cce-5-1] eliminated 399 ternary clauses 1%
c [cce-5-1] eliminated 484 small clauses 1%
c [cce-5-1] eliminated 484 small clauses in 27587454 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 844 covered clauses in round 1
c [cce-5] eliminated 844 covered clauses in TOTAL during 1 rounds
c [cce-5] 844 < 1/100 * 171315 = 1713 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 23274 variables 100%
c [elim-12] limit of 441398946 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 702 variables 3% in round 1 in 102777005 steps
c [elim-12-1] backward subsumption/strengthening limit 102777000
c [elim-12-1-1] backward checking 1474 touched variables 6%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 1 clauses in 2977265 steps
c [elim-12-1] rescheduled 10 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 1407755 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 702 = 3% variables out of 23274 scheduled
c [bca-11] limit of 10000000 steps and 335043 added (scaled 2)
c [bca-11] 26311 out of 45146 literals actually usable 58%
c [bca-11] added 225 blocked clauses in 161581 steps
c [sweep-9] limit 1655246 penalty 2 = 2 + 0
c [sweep-9-1] 2222 pos 49.5% + 2263 neg 50.5% = 4485 sched 19.9% ret 18087
c [sweep-9-1] 1661049 steps 393 queries 991.01 avg class size
c [sweep-9-1] 7778 decisions 389 SAT calls 27.78 avg env size
c [sweep-9-1] 3546 variables remain 16% (19023 retained 84%)
c [decomp-49] removed 15 variables
c [sweep-9-1] removed 15 vars (0 failed, 4 eqs, 5 impls)
c [sweep-9] 15 < 1/1000 * 22572 = 22 considered unsuccessful
c [sweep-9] removed 15 vars in TOTAL (1 rounds, 392 queries)
c [sort-queue-16] sorted 10057 enqueued variables after 434860 conflicts
c [score-dist-16] active 12500 (55%), one 2462 (11%), zero 7595 (34%)
c [score-dist-16] max exp 508, different 378 (74%)
c [score-dist-16] median active exp 465, avg 435.7
c [simplification-16] removed 787 variables 3.4% (22557 remain 8%)
c [simplification-16] removed 4411 irredundant clauses 2.6% (167189 remain 21%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 28888 = 115552 / 4
c [simplification-16] new conflict interval 144440
c [simplification-16] penalized conflict interval 144440 = 1 * 144440
c [simplification-16] hard conflict limit 651520 (soft 579300 + delta 72220)
c [simplification-16] new conflict limit 579300 (hard 651520)
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  121.1   22556   167189    449267   88884  17378  3354   11   279   44   4%    148  107   12   11  106%
c i  121.5   22555   167189    453116   92160  17417  3359   10   177   45   5%   -258    4   12   11  111%
c i  122.5   22552   167189    456265   94854  17463  3360   13   154   46   8%   -264  -18   18   11  164%
c -  125.4   22550   167189    479843   78174  17714  3375   12   143   40   8%     88  -34    9   11   84%
c i  130.8   22549   167189    514732  106935  18137  3396   12   123   46  10%    474  -72   13   11  123%
c -  133.4   22549   167189    532651   85809  18300  3409   11   109   53  10%   -100  -79    8   11   79%
c 
c [simplification-17] limit 579300 conflicts (hard 651520) hit after 579940 conflicts
c [quatres-13] found 30579 quaternary clauses 20% in total
c [quatres-13-1] removed 12 duplicate quaternary clauses
c [quatres-13-1] added 10 double-self-subsuming ternary resolvents
c [quatres-13-2] added 91 single-self-subsuming ternary resolvents
c [quatres-13-2] added 206 quaternary resolvents
c [ternres-13] limit 29246003 with penalty 0 = 0 + 0
c [ternres-13] all 22549 free variables schedulable
c [ternres-13] 2228 ternary resolvents (232 bin, 1996 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-50] removed 57 variables
c [treelook-6] limit 2924600 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 15824 literals 35%
c [treelook-6] scheduling used 681126 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2924600 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2966439 steps
c [treelook-6] 14905 literals remain 33%
c [treelook-6] 4505 variables remain to probed next time 20%
c [decomp-51] removed 7 variables
c [treelook-6] removed 22 variables, found 1588 hbrs
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 422 transitive binary clauses
c [transred-13] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 22477 variables 100%
c [block-6] limit of 73115008 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 653 blocked clauses
c [block-6] 653 < 1/100 * 166927 = 1669 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 22445 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 73 variables 0% in round 1 in 102096864 steps
c [elim-13-1] backward subsumption/strengthening limit 102096800
c [elim-13-1-1] backward checking 581 touched variables 3%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 2 clauses in 1204631 steps
c [elim-13-1] rescheduled 7 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 69805 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 73 = 0% variables out of 22445 scheduled
c [elim-13] 73 < 1/100 * 22445 = 224 considered unsuccessful
c [bca-12] limit of 10000000 steps and 332479 added (scaled 2)
c [bca-12] 24536 out of 44746 literals actually usable 55%
c [bca-12] added 39 blocked clauses in 203883 steps
c [sort-queue-17] sorted 10544 enqueued variables after 579940 conflicts
c [score-dist-17] active 11828 (53%), one 3339 (15%), zero 7205 (32%)
c [score-dist-17] max exp 510, different 398 (78%)
c [score-dist-17] median active exp 473, avg 415.2
c [simplification-17] removed 177 variables 0.8% (22372 remain 8%)
c [simplification-17] removed 1315 irredundant clauses 0.8% (165874 remain 21%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 72220 = 144440 / 2
c [simplification-17] new conflict interval 216660
c [simplification-17] penalized conflict interval 216660 = 1 * 216660
c [simplification-17] hard conflict limit 904930 (soft 796600 + delta 108330)
c [simplification-17] new conflict limit 796600 (hard 904930)
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 -  145.4   22372   165874    585287   93091  20581  4746   11   132   42   9%    520  -38   12   11  110%
c i  147.0   22371   165874    592411   99310  20708  4751   11    96   46  12%    572  -67   16   11  148%
c i  149.3   22364   165874    606309  110935  20860  4759   14   143   48  10%   -339  -19   17   11  150%
c i  153.9   22359   165874    628556  130277  21162  4772   12   174   52   7%   -104   15   13   11  115%
c -  154.8   22349   165874    637560   99600  21221  4772   11   223   43   5%   -267   56   10   11   95%
c -  161.7   22349   165874    689134  108100  21572  4792    9   129   44   7%    436  -33    8   10   77%
c -  173.6   22349   165874    739735  112647  22247  4817   13   102   59  13%    753  -29   13   11  118%
c i  175.5   22348   165874    751266  122623  22305  4818   10   229   64   4%    796   96   13   11  117%
c i  179.4   22347   165874    767681  136650  22482  4839   11    77   65  15%   -669  -54   11   11  102%
c -  185.6   22346   165874    794611  120645  22804  4849   11    69   59  17%   -272  -42   15   11  134%
c 
c [simplification-18] limit 796600 conflicts (hard 904930) hit after 830613 conflicts
c [quatres-14] found 34143 quaternary clauses 19% in total
c [quatres-14-1] removed 5 duplicate quaternary clauses
c [quatres-14-1] added 4 double-self-subsuming ternary resolvents
c [quatres-14-2] added 147 single-self-subsuming ternary resolvents
c [quatres-14-2] added 200 quaternary resolvents
c [ternres-14] limit 47060001 with penalty 0 = 0 + 0
c [ternres-14] all 22346 free variables schedulable
c [ternres-14] 2104 ternary resolvents (168 bin, 1936 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-52] removed 107 variables
c [basicprobe-6] limit 235300009 penalty 0 = 0 + 0
c [basicprobe-6-0] 11649 sched 52%, 17 failed, 0 lifted, 936 hbrs
c [decomp-53] removed 66 variables
c [basicprobe-6-1] 11627 sched 52%, 1 failed, 0 lifted, 179 hbrs
c [decomp-54] removed 5 variables
c [basicprobe-6-2] 11631 sched 52%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-6-3] 11630 sched 52%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-6-4] 11630 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-4] fully completed probing
c [basicprobe-6-4] 18 units = 18 failed (100%) + 0 lifted (0%)
c [basicprobe-6-4] removed 71 variables, found 1148 hbrs
c [bate-4] eliminated 223 asymmetric tautologies during probing
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 443 transitive binary clauses
c [bca-13] limit of 10000000 steps and 329591 added (scaled 2)
c [bca-13] 24030 out of 44390 literals actually usable 54%
c [bca-13] added 6 blocked clauses in 228907 steps
c [sort-queue-18] sorted 11054 enqueued variables after 830613 conflicts
c [score-dist-18] active 11140 (50%), one 4098 (18%), zero 6956 (31%)
c [score-dist-18] max exp 509, different 403 (79%)
c [score-dist-18] median active exp 481, avg 414.0
c [simplification-18] removed 152 variables 0.7% (22194 remain 8%)
c [simplification-18] removed 1454 irredundant clauses 0.9% (164420 remain 21%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 108330 = 216660 / 2
c [simplification-18] new conflict interval 324990
c [simplification-18] penalized conflict interval 324990 = 1 * 324990
c [simplification-18] hard conflict limit 1318098 (soft 1155603 + delta 162495)
c [simplification-18] new conflict limit 1155603 (hard 1318098)
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 -  202.6   22194   164420    848220  127079  24248  5285   19    54   45  34%    452  -35   24   13  180%
c -  214.0   22194   164420    900945  135947  24583  5295   10    94   46  11%    768   21    8   12   65%
c -  225.6   22194   164420    946754  138474  24803  5305   17    35   46  48%    897  -23   19   13  141%
c -  234.5   22194   164420    999420  145143  25103  5317   11   158   63   7%    967   61   11   12   89%
c -  244.5   22194   164420   1048488  149309  25325  5324   11    78   63  14%    997  -21    8   12   67%
c -  258.0   22194   164420   1095795  152055  25464  5332   16    27   63  61%   1011  -44   15   14  105%
c -  270.7   22194   164420   1142340  154005  25517  5334   16    22   64  76%   1018  -24   22   15  149%
c -  284.3   22194   164420   1190848  155111  25525  5334   12    15   64  84%   1021  -16   11   14   80%
c -  296.4   22194   164420   1240913  155391  25544  5337   11    13   64  84%   1023  -10   13   13  104%
c 
c [simplification-19] limit 1155603 conflicts (hard 1318098) hit after 1283339 conflicts
c [quatres-15] found 36929 quaternary clauses 18% in total
c [quatres-15-1] removed 18 duplicate quaternary clauses
c [quatres-15-1] added 8 double-self-subsuming ternary resolvents
c [quatres-15-2] added 107 single-self-subsuming ternary resolvents
c [quatres-15-2] added 233 quaternary resolvents
c [ternres-15] limit 87596478 with penalty 0 = 0 + 0
c [ternres-15] all 22194 free variables schedulable
c [ternres-15] 2973 ternary resolvents (244 bin, 2729 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 1094955 penalty 4 = 4 + 0
c [gauss-5] extracted 8066 xors of average arity 3.0
c [gauss-5] connected 24177 occurrences of 3534 variables (average 6.8)
c [gauss-5] limit 1094955 penalty 4 = 4 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-57] removed 23 variables
c [simpleprobe-7] all 22171 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-58] removed 83 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 83 variables, found 3190 hbrs, 3 units
c [unhide-13] limit 2189911 with penalty 3 = 3 + 0
c [unhide-13-13] 0 units, 0 failed, 930 tauts, 0 hbrs, 53003 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 837 transitive binary clauses
c [cce-6] limit of 54747799 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 2 clauses out of 61 (3%) of length 21
c [cce-6-1] eliminated 2 clauses out of 167 (1%) of length 20
c [cce-6-1] eliminated 10 clauses out of 189 (5%) of length 19
c [cce-6-1] eliminated 13 clauses out of 276 (5%) of length 18
c [cce-6-1] eliminated 1 clauses out of 303 (0%) of length 17
c [cce-6-1] eliminated 9 clauses out of 322 (3%) of length 16
c [cce-6-1] eliminated 7 clauses out of 408 (2%) of length 15
c [cce-6-1] eliminated 11 clauses out of 520 (2%) of length 14
c [cce-6-1] eliminated 12 clauses out of 634 (2%) of length 13
c [cce-6-1] eliminated 24 clauses out of 892 (3%) of length 12
c [cce-6-1] eliminated 18 clauses out of 1435 (1%) of length 11
c [cce-6-1] eliminated 63 clauses out of 1994 (3%) of length 10
c [cce-6-1] eliminated 171 clauses out of 3425 (5%) of length 9
c [cce-6-1] eliminated 340 clauses out of 5707 (6%) of length 8
c [cce-6-1] eliminated 492 clauses out of 11391 (4%) of length 7
c [cce-6-1] eliminated 108 clauses out of 25049 (0%) of length 6
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1283 large clauses in 54747806 steps
c [cce-6-1] allowing another 27373903 steps for small clauses
c [cce-6-1] scheduling 71851 clauses = 18608 binary + 53243 ternary
c [cce-6-1] tried to eliminate 51916 small clauses 72%
c [cce-6-1] eliminated 43 binary clauses 0%
c [cce-6-1] eliminated 299 ternary clauses 1%
c [cce-6-1] eliminated 342 small clauses 0%
c [cce-6-1] eliminated 342 small clauses in 54747829 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1625 covered clauses in round 1
c [cce-6] eliminated 1625 covered clauses in TOTAL during 1 rounds
c [cce-6] 1625 < 1/100 * 163307 = 1633 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 22088 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 555 variables 3% in round 1 in 96249590 steps
c [elim-14-1] backward subsumption/strengthening limit 96249500
c [elim-14-1-1] backward checking 1981 touched variables 9%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 2 clauses in 2915710 steps
c [elim-14-1] rescheduled 8 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 109725 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 555 = 3% variables out of 22088 scheduled
c [bca-14] limit of 10000000 steps and 317028 added (scaled 2)
c [bca-14] 23663 out of 43068 literals actually usable 55%
c [bca-14] added 61 blocked clauses in 259866 steps
c [sort-queue-19] sorted 16140 enqueued variables after 1283339 conflicts
c [score-dist-19] active 5393 (25%), one 9487 (44%), zero 6653 (31%)
c [score-dist-19] max exp 509, different 306 (60%)
c [score-dist-19] median active exp 498, avg 429.9
c [simplification-19] removed 661 variables 3.0% (21533 remain 8%)
c [simplification-19] removed 6283 irredundant clauses 3.8% (158137 remain 20%)
c [simplification-19] maximum reduction of 4% = max (3%, 4%)
c [simplification-19] geometric conflict interval increment 64998 = 324990 / 5
c [simplification-19] new conflict interval 389988
c [simplification-19] penalized conflict interval 389988 = 1 * 389988
c [simplification-19] hard conflict limit 1868321 (soft 1673327 + delta 194994)
c [simplification-19] new conflict limit 1673327 (hard 1868321)
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 -  316.4   21533   158137   1295875  153016  27093  6889   12    18   48  67%   1023   -1   11   13   86%
c -  330.8   21533   158137   1349713  153701  27119  6893   12    17   49  74%   1024   -1   10   12   83%
c -  345.9   21533   158137   1404872  154641  27181  6895   13    19   49  72%   1024   -2   13   12  108%
c -  361.3   21533   158137   1461723  156411  27203  6903   10    12   50  85%   1024   -5   10   11   92%
c i  364.0   21532   158137   1472116  163273  27254  6916    8     9   57  86%   1024   -6    5   11   50%
c i  365.8   21459   158137   1480282  170449  27312  6927   10   142   57   7%  -8844  120    8   11   78%
c -  376.5   21457   158137   1521411  160750  27633  6940   11    77   68  14%  -4315   22    9   11   79%
c -  392.0   21457   158137   1581691  167303  27961  6966   11    95   68  12%  -1104   18   12   12   98%
c i  400.4   21456   158137   1627441  208109  28064  6971   14    63   82  23%    -35  -21   13   12  102%
c -  403.7   21453   158137   1639313  173831  28090  6972   16    66   68  25%  -1808  -14   21   13  167%
c -  418.6   21453   158137   1692188  175505  28250  6981   18    45   68  39%   -240  -22   15   14  103%
c i  426.4   21452   158137   1723014  203026  28287  6985   15    34   81  43%    234  -28   18   14  129%
c -  434.2   21452   158137   1747530  178449  28308  6985   11    20   68  57%   -563  -30   11   14   77%
c -  452.0   21452   158137   1806719  180668  28339  6989   15    26   69  57%    381   -6   12   13   92%
c 
c [simplification-20] limit 1673327 conflicts (hard 1868321) hit after 1811565 conflicts
c [quatres-16] found 36922 quaternary clauses 18% in total
c [quatres-16-1] removed 88 duplicate quaternary clauses
c [quatres-16-1] added 14 double-self-subsuming ternary resolvents
c [quatres-16-2] added 212 single-self-subsuming ternary resolvents
c [quatres-16-2] added 442 quaternary resolvents
c [ternres-16] limit 141438829 with penalty 0 = 0 + 0
c [ternres-16] all 21452 free variables schedulable
c [ternres-16] 2850 ternary resolvents (174 bin, 2676 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-59] removed 287 variables
c [treelook-7] limit 14143882 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 15516 literals 37%
c [treelook-7] scheduling used 759901 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 14143882 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 9826721 steps
c [treelook-7] fully completed tree based probing
c [decomp-60] removed 85 variables
c [treelook-7] removed 114 variables, found 3361 hbrs
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 993 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 21132 variables 100%
c [block-7] limit of 100000000 steps penalty 3 = 3 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 3665 blocked clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 20676 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 421 variables 2% in round 1 in 94270236 steps
c [elim-15-1] backward subsumption/strengthening limit 94270200
c [elim-15-1-1] backward checking 2057 touched variables 10%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 53 clauses in 3811496 steps
c [elim-15-1] rescheduled 56 variables 0% by backward subsumption
c [elim-15-2] no variable eliminated in round 2 in 1456069 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 421 = 2% variables out of 20676 scheduled
c [bca-15] limit of 10000000 steps and 300784 added (scaled 2)
c [bca-15] 22147 out of 40512 literals actually usable 55%
c [bca-15] added 69 blocked clauses in 243014 steps
c [sweep-10] limit 5303956 penalty 3 = 3 + 0
c [sweep-10-1] 1598 pos 50.8% + 1550 neg 49.2% = 3148 sched 15.5% ret 17107
c [sweep-10-1] 5331907 steps 796 queries 412.69 avg class size
c [sweep-10-1] 16555 decisions 805 SAT calls 29.25 avg env size
c [sweep-10-1] 1261 variables remain 6% (18970 retained 94%)
c [decomp-61] removed 86 variables
c [sweep-10-1] removed 86 vars (0 failed, 8 eqs, 1 impls)
c [sweep-10] removed 86 vars in TOTAL (1 rounds, 795 queries)
c [sort-queue-20] sorted 12417 enqueued variables after 1811565 conflicts
c [score-dist-20] active 7752 (38%), one 6439 (32%), zero 5978 (30%)
c [score-dist-20] max exp 510, different 333 (65%)
c [score-dist-20] median active exp 497, avg 420.1
c [simplification-20] removed 1283 variables 6.0% (20169 remain 8%)
c [simplification-20] removed 8880 irredundant clauses 5.6% (149257 remain 19%)
c [simplification-20] maximum reduction of 6% = max (6%, 6%)
c [simplification-20] large reduction 6% >= 5% limit
c [simplification-20] next conflict interval 18115 = min (1811565/100, 389988)
c [simplification-20] penalized conflict interval 18115 = 1 * 18115
c [simplification-20] hard conflict limit 1839680 (soft 1829680 + delta 10000)
c [simplification-20] new conflict limit 1829680 (hard 1839680)
c 
c [simplification-21] limit 1829680 conflicts (hard 1839680) hit after 1839680 conflicts
c [quatres-17] found 35707 quaternary clauses 17% in total
c [quatres-17-1] removed 39 duplicate quaternary clauses
c [quatres-17-1] added 10 double-self-subsuming ternary resolvents
c [quatres-17-2] added 323 single-self-subsuming ternary resolvents
c [quatres-17-2] added 649 quaternary resolvents
c [ternres-17] limit 144710190 with penalty 0 = 0 + 0
c [ternres-17] all 20169 free variables schedulable
c [ternres-17] 8969 ternary resolvents (739 bin, 8230 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 4522193 penalty 4 = 4 + 0
c [card-6] found 340 at-most-one constraints of average size 3.1
c [card-6] found 285 at-most-two constraints of average size 4.0
c [card-6] using previous limit 4522193 for elimination
c [card-6] 622 out of 625 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-62] removed 92 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 10366 sched 52%, 14 failed, 0 lifted, 299 hbrs
c [decomp-63] removed 28 variables
c [basicprobe-7-1] 10364 sched 52%, 4 failed, 0 lifted, 103 hbrs
c [decomp-64] removed 15 variables
c [basicprobe-7-2] 10343 sched 52%, 2 failed, 0 lifted, 28 hbrs
c [decomp-65] removed 4 variables
c [basicprobe-7-3] 10342 sched 52%, 2 failed, 0 lifted, 15 hbrs
c [decomp-66] removed 6 variables
c [basicprobe-7-4] 10339 sched 52%, 1 failed, 0 lifted, 19 hbrs
c [decomp-67] removed 5 variables
c [basicprobe-7-5] 10336 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-5] fully completed probing
c [basicprobe-7-5] 23 units = 23 failed (100%) + 0 lifted (0%)
c [basicprobe-7-5] removed 58 variables, found 464 hbrs
c [bate-5] eliminated 87 asymmetric tautologies during probing
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 561 transitive binary clauses
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 20019 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 331 variables 2% in round 1 in 93347956 steps
c [elim-16-1] backward subsumption/strengthening limit 93347900
c [elim-16-1-1] backward checking 936 touched variables 5%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 11 and strengthened 23 clauses in 2006234 steps
c [elim-16-1] rescheduled 49 variables 0% by backward subsumption
c [elim-16-2] eliminated 6 variables 0% in round 2 in 1217649 steps
c [elim-16-2] backward subsumption/strengthening limit 1217600
c [elim-16-2-1] backward checking 31 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 0 clauses in 138418 steps
c [elim-16] fully completed in 2 rounds
c [gc-130] reconnected 6806 binary clauses (produced 0 empty 2 units)
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 343 = 2% variables out of 20019 scheduled
c [bca-16] limit of 10000000 steps and 293653 added (scaled 2)
c [bca-16] 21234 out of 39354 literals actually usable 54%
c [bca-16] added 21 blocked clauses in 260821 steps
c [sort-queue-21] sorted 12054 enqueued variables after 1839680 conflicts
c [score-dist-21] active 7622 (39%), one 6286 (32%), zero 5768 (29%)
c [score-dist-21] max exp 510, different 295 (58%)
c [score-dist-21] median active exp 421, avg 414.1
c [simplification-21] removed 493 variables 2.4% (19676 remain 7%)
c [simplification-21] removed 2840 irredundant clauses 1.9% (146417 remain 18%)
c [simplification-21] maximum reduction of 2% = max (2%, 2%)
c [simplification-21] geometric conflict interval increment 129996 = 389988 / 3
c [simplification-21] new conflict interval 519984
c [simplification-21] penalized conflict interval 519984 = 1 * 519984
c [simplification-21] hard conflict limit 2619656 (soft 2359664 + delta 259992)
c [simplification-21] new conflict limit 2359664 (hard 2619656)
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 -  480.7   19676   146417   1866977  166938  28366  6550   11    13   48  80%    768  -15   11   12   91%
c -  499.3   19676   146417   1927658  168514  28410  6556   11    13   50  85%    922  -12   11   12   92%
c -  515.4   19676   146417   1985816  169975  28485  6562   11    13   50  85%    982  -14   11   12   91%
c i  523.3   19675   146417   2013948  192382  28523  6563    8    19   60  44%    997   -6    6   11   54%
c i  526.4   19674   146417   2024721  199984  28573  6575    8     9   62  81%  -2917  -14    5   11   45%
c i  527.0   19473   146417   2028470  203219  28614  6584    9    69   62  13%  -2855   44   10   11   95%
c -  532.5   19473   146417   2049046  172355  28706  6599   15    53   50  29%  -1856   16   17   11  146%
c -  550.9   19473   146417   2110117  174657  28762  6615   10    13   68  77%   -110  -14   10   11   83%
c -  567.6   19473   146417   2173761  177900  28812  6623    8    10   68  83%    594  -15    8   11   76%
c i  568.9   19472   146417   2179077  181506  28840  6629    8     9   76  86%    628  -15    6   10   54%
c i  568.9   19255   146417   2179137  181530  28849  6634    8     9   76  86%    494  -15    5   10   49%
c 0  568.9   19248   146417   2179137  181530  28849  6634    8     9   76  86%    492  -15    5   10   49%
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: 1723 basic ate = 217 trn 13% + 1506 lrg 87% in 5 updates
c bcas: 16 count, 659 added (1410 skipped), 3020167 steps
c bkwd: tried 131776 clauses, 263486 lits, 2.00 lits/clause
c bkwd: checked 11006126 occs, 83.52 occs/clause, 41.77 occs/lit
c bkwd: subsumed 0 binary, 4 ternary, 18 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 86 large (0% self)
c blkd: 7 bces, 29564 removed, 9734990 resolutions, 26100874 steps
c blkd: 9206 blocking literals 2%, 3335 pure
c bump: 2129713 bumped seen, 158637798 lits 74.5 on average
c card: 6 count, 0 units, 1 am1, 20772021 steps
c card: 1 rescheduled, 2 eliminated, 8 resolved, 5195 subsumed
c card: 644 at-most-one constraints found, average size 3.08
c card: 644 at-most-one constraints used 100%, average size 3.08
c card: 285 at-most-two constraints found, average size 4.05
c card: 282 at-most-two constraints used 99%, average size 4.05
c cces: 6 cces, 14450 eliminated, 13987 ate 97%, 463 abce 3%
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: 2640582 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 132 gcs, 0 rescored clauses, 8320 rescored vars
c dcps: 67 decompositions, 6483 equivalent 2%
c deco: 220 decision-only clauses 0%, 47% reduction
c decs: 14789115 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 232548 eliminated 87%, 284 pure 0%
c elms: 24 rounds, 1.5 rounds/bve
c elms: 217036 small 93%, 11893 large 5%
c elms: 325028 tried small, 217036 succeeded 67%, 107992 failed 33%
c elms: 10662 subsumed, 8205 strengthened, 2069 blocked
c elms: 11752355 copies, 20702721 resolutions, 7093485 ipos
c elms: 9411125 subchks, 8479720 strchks
c gaus: 5 extractions, 46078 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10207962 steps, 5103981 extr 50%, 5154712 elim 50%
c glue: 12.2 orig avg, 12.2 real avg, 2.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 25917 = 5259 simple 20% + 18508 trn 71% + 2150 lrg 8%, 1418 sub 5%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2129713 clauses, 27.7 length
c lrnd: 58967271 lits = 105064143 orig - 46096872 removed 44%
c lrnd: 588999 uips 28%, 1006259 flips 47%
c mins: 2104177 mins 99%, 258 bin 0%, 25058 size 1%
c mins: 102900150 poisoned searches, 11299863 hits, 11% hit rate
c mins: 194336572 used twice searches, 11009177 hits, 6% hit rate
c move: moved 20095, 4338 bin 22%, 15757 trn 78%
c otfs: 50888 driving 45%, 61058 restarting 55%
c otfs: str 111946, 111819 red 100%, 127 irr 0%
c otfs: str 111946, 0 bin 0%, 393 trn 0%, 111553 lrg 100%
c otfs: sub 2420, 2419 red 100%, 1 irr 0%
c otfs: sub 2420, 0 bin 0%, 87 trn 4%, 2333 lrg 96%
c phas: 2 computed, 64558 set, 23065 pos (36%), 41493 neg (64%)
c prbs: 7 basic, 705728 probed, 523 failed, 33 lifted
c prbs: 7 simple, 512018 probed, 100 failed, 384 eqs
c prbs: 7 treelook, 17314 probed, 59 failed, 0 lifted
c prom: 432361 locked 8% out of 5213724 tried
c prps: 918595471 props, 62 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 17 count, 22613 quat, 5203 self1, 79 self2, 431 dup
c queu: 21 sorted, 14789115 next (890264 steps 0.06)
c queu: 244123542 enq (336419334 steps 1.38), 158637798 deq 65%
c redc: 32559 clauses 8%, 418930 tried 19%, 8 sat 0%
c redc: 43043 lits 1%, 4771719 tried 5%, 8 sat 0%
c redc: 664 times jump level reduced, 10.0 levels on average
c reds: 40 count, 54478.4 conflicts per reduce
c reds: 0 memlim 0%, 40 arith 100%
c reds: 1390102 collected 86%, 227670 retired 14%
c rmbd: 1239 removed, 739 red 60%
c rsts: 49807 restarts 100%, 13 skipped 0%
c rsts: 13 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: 21 count, 21 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2129713 count (1328101 tried 0.6), 266735 sub out of 2124412 (12.6%)
c swps: 10 count, 10 rounds, 4594 queries (459.4/round)
c swps: 4570 sat calls, 57 unsat (0.3% success rate)
c swps: 95355 decisions 20.9, 1464 conflicts 0.3
c swps; 1586.4 avg class size, 29.5 avg environment size
c swps: 0 failed, 52 impls, 79 equivs
c swp0: 1528 type 0 queries, 77 unsat (5.0%), 1519 sat (99.4%)
c swp1: 3066 type 1 queries, 730 unsat (23.8%), 2996 sat (97.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 33854772 calls to obtain time
c tops: 8126 fixed 3%, 48 its, 45398.69 confs/it
c trds: 17 transitive reductions, 5079 removed, 13 failed
c trds: 905082 nodes, 433946 edges, 5721730 steps
c trim: 1764487 words, 6.7 MB
c trnr: 17 count, 3231 bin, 47747 trn, 315694433 steps
c unhd: 13 count, 13 rounds, 29191480 steps
c unhd: 358 non-trivial sccs of average size 2.1
c unhd: 20 units, 20 bin, 0 trn, 0 lrg
c unhd: 212 failed, 203 stamp, 0 lits, 0 bin, 7 trn, 0 lrg
c unhd: 10702 tauts, 202 bin 2%, 6490 trn 61%, 2511 lrg 23%
c unhd: 10702 tauts, 1499 stamp 14%, 8737 red 82%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 169859 str, 20 bin 0%, 1398 trn 1%, 168441 lrg 99%, 152079 red 90%
c vars: 19248 remaining 7% and 247157 removed 93% out of 266405
c vars: 8126 fixed 3%, 232548 eliminated 87%, 6483 equivalent 2%
c vsts: 18570307559 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 20.3 search visits per propagation, 8479.7 per conflict
c wchs: 3692056587 pushed, 51792948 enlarged, 220 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2147025       1390102        227670     144386882      24255117       1294824
c 
c  0 0        235347  11     19789   1         0   0 102881836  71  11945962  49    429253  33     5.2
c  1 5        117440   5     60693   4     35165  15  14740884  10<  2732809  11<   120418   9     0.7
c  2 6        416134  19    273302  20     61455  27  16812281  12   4698335  19    268853  21<    2.4
c  3 9        722031  34<   531046  38<    57280  25<  7507289   5   3464518  14    316693  24     4.7
c  4 14       420850  20    327742  24     37273  16   1813216   1   1065563   4    121064   9     3.0
c  5 21       147351   7    114586   8     19137   8    412373   0    239492   1     26548   2     1.8
c  6 30        57509   3     42534   3     10166   4    150847   0     74695   0      7964   1     1.2
c  7 41        19887   1     13636   1      4496   2     45104   0     22582   0      2685   0     0.9
c  8 54         7076   0      4682   0      1785   1     15789   0      7610   0       906   0     0.7
c  9 69         2307   0      1510   0       595   0      5127   0      2574   0       332   0     0.4
c 10 86          912   0       542   0       254   0      1839   0       864   0       106   0     0.3
c 11 126         181   0        40   0        64   0       297   0       113   0         2   0     0.0
c 
c avg                  2.8           3.2           3.0           0.6           1.2           1.8
c std                  1.5           1.3           1.6           1.0           1.4           1.5
c 
c   24.784   4% elim
c   16.461   3% bump
c   14.069   2% probe
c   12.451   2% rescore
c    9.786   2% decide
c    4.832   1% cce
c    3.964   1% sweep
c    3.527   1% quatres
c    3.014   1% unhide
c    2.580   0% ternres
c 
c    6.751 < 1% rest (below)
c 
c    2.489   0% block
c    2.113   0% bca
c    1.150   0% gauss
c    0.501   0% transred
c    0.499   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.216   1% preprocessing     8%
c   63.657  11% inprocessing     92%
c ==================================
c   68.874  12% simplifying
c  500.065  88% search
c ==================================
c  568.944 100% all
c 
c       2179137 conflicts,        3830.1 confs/sec
c          4442 ternaries,         490.6 confs/ternary
c           524 binaries,         4158.7 confs/binary
c            48 iterations,      45398.7 confs/iteration
c 
c            40 reductions,          0.1 redus/sec,  54478.4 confs/reduction
c         49807 restarts,           87.5 rests/sec,     43.8 confs/restart
c      14789115 decisions,       25994.0 decis/sec,      6.8 decis/conflict
c     918595471 propagations,  1614563.0 props/sec,     62.1 props/decision
c 
c 568.9 seconds, 98.6 MB
c launch: done
