c launch: /data/cnf/sc2014/app/q_query_3_l46_lambda.cnf.bz2
c host: atom23
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/q_query_3_l46_lambda.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/q_query_3_l46_lambda.cnf.bz2
c no embedded options
c found 'p cnf 33090 165828' header
c read 33090 variables, 165828 clauses, 478271 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=5
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 28241 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   28241   155258         0       0      0     0    0     0   12   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 712 at-most-one constraints of average size 4.5
c [card-1] found 5 at-most-two constraints of average size 4.2
c [card-1] using previous limit 2000000 for elimination
c [card-1] 717 out of 717 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 11782 variables
c [simpleprobe-1] all 21308 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 7379 variables
c [simpleprobe-1] 793 variables remain 6% (13136 retained 94%)
c [simpleprobe-1] removed 7379 variables, found 29218 hbrs, 28 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 1269 tauts, 0 hbrs, 309 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13929 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 7958 variables 57% in round 1 in 4970067 steps
c [elim-1-1] backward subsumption/strengthening limit 4970000
c [elim-1-1-1] backward checking 9731 touched variables 70%
c [elim-1-1-1] incomplete backward checking 7145 remain 73%
c [elim-1-1] subsumed 70 and strengthened 618 clauses in 4970108 steps
c [elim-1-1] rescheduled 918 variables 7% by backward subsumption
c [elim-1-2] eliminated 4 variables 0% in round 2 in 1470517 steps
c [elim-1-2] backward subsumption/strengthening limit 1470500
c [elim-1-2-1] backward checking 7339 touched variables 53%
c [elim-1-2-1] incomplete backward checking 6964 remain 95%
c [elim-1-2] subsumed 24 and strengthened 68 clauses in 1470502 steps
c [elim-1-2] rescheduled 131 variables 1% by backward subsumption
c [elim-1-3] eliminated 4 variables 0% in round 3 in 72477 steps
c [elim-1-3] backward subsumption/strengthening limit 72400
c [elim-1-3-1] backward checking 7021 touched variables 50%
c [elim-1-3-1] incomplete backward checking 6976 remain 99%
c [elim-1-3] subsumed 12 and strengthened 3 clauses in 72487 steps
c [elim-1] incomplete 24 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 7966 = 57% variables out of 13929 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 56924 negative 96.6% of 58899 except 1975 3.4%
c [phase-count-1] 45129 positive 76.6% of 58899 except 13770 23.4%
c [phase-count-1] less non-negative clauses 1975 than limit 5800 (10.0%)
c [phase-count-1] non-pos/non-neg = 13770/1975 = 6.97 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 5963 negative 100%
c [sort-queue-1] sorted 5963 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5963 (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 21954 variables 78.6% (5963 remain 21%)
c [simplification-1] removed 96359 irredundant clauses 62.1% (58899 remain 38%)
c [simplification-1] maximum reduction of 79% = max (79%, 62%)
c [simplification-1] large reduction 79% >= 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    0.8    5962    58899        30      29      0  1305    0     1    6   6%      0    1    1    0 23969%
c i    0.8    5961    58899       113      97      8  1306    0     1    7  11%      0    1    2    0 20446%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 4 variables
c [simpleprobe-2] 330 schedulable variables 6%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 340 variables remain 6% (5618 retained 94%)
c [simpleprobe-2] removed 1 variables, found 177 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 11916 literals 100%
c [treelook-1] scheduling used 248193 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 301681 steps
c [treelook-1] 11437 literals remain 96%
c [treelook-1] 5943 variables remain to probed next time 100%
c [decomp-5] removed 3 variables
c [treelook-1] removed 6 variables, found 968 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2983 sched 51%, 39 failed, 2 lifted, 3441 hbrs
c [decomp-6] removed 48 variables
c [basicprobe-1-1] 1976 probes remain 33% after last round
c [basicprobe-1-1] 46 units = 44 failed (96%) + 2 lifted (4%)
c [basicprobe-1-1] removed 53 variables, found 3551 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 5899 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 24 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 72 = 1% variables out of 5899 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 55068 negative 96.6% of 57017 except 1949 3.4%
c [phase-count-2] 42698 positive 74.9% of 57017 except 14319 25.1%
c [phase-count-2] less non-negative clauses 1949 than limit 5700 (10.0%)
c [phase-count-2] non-pos/non-neg = 14319/1949 = 7.35 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 2054 negative 100%
c [sort-queue-2] sorted 4364 enqueued variables after 1001 conflicts
c [score-dist-2] active 1463 (25%), one 0 (0%), zero 4364 (75%)
c [score-dist-2] max exp 762, different 193 (25%)
c [score-dist-2] median active exp 700, avg 679.3
c [simplification-2] removed 134 variables 2.2% (5827 remain 21%)
c [simplification-2] removed 1878 irredundant clauses 3.2% (57017 remain 37%)
c [simplification-2] maximum reduction of 3% = max (2%, 3%)
c [simplification-2] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-2] new conflict interval 5000
c [simplification-2] penalized conflict interval 5000 = 1 * 5000
c [simplification-2] hard conflict limit 16001 (soft 6001 + delta 10000)
c [simplification-2] new conflict limit 6001 (hard 16001)
c 
c [simplification-3] limit 6001 conflicts (hard 16001) hit after 6002 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1013 at-most-one constraints of average size 3.5
c [card-2] found 16 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1029 out of 1029 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 11645 literals 100%
c [treelook-2] scheduling used 250675 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 327366 steps
c [treelook-2] 11478 literals remain 99%
c [treelook-2] 5813 variables remain to probed next time 100%
c [treelook-2] removed 2 variables, found 915 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 1 failed, 575 tauts, 0 hbrs, 2326 literals
c [elim-3] 24 variables 0% will be scheduled this time
c [elim-3] scheduled 24 variables 0%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 2048551 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 24 scheduled
c [phase-count-3] 54989 negative 96.6% of 56939 except 1950 3.4%
c [phase-count-3] 42594 positive 74.8% of 56939 except 14345 25.2%
c [phase-count-3] less non-negative clauses 1950 than limit 5600 (10.0%)
c [phase-count-3] non-pos/non-neg = 14345/1950 = 7.36 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1966 negative 100%
c [sort-queue-3] sorted 4440 enqueued variables after 6002 conflicts
c [score-dist-3] active 1383 (24%), one 577 (10%), zero 3863 (66%)
c [score-dist-3] max exp 562, different 263 (47%)
c [score-dist-3] median active exp 515, avg 440.6
c [simplification-3] removed 4 variables 0.1% (5823 remain 21%)
c [simplification-3] removed 78 irredundant clauses 0.1% (56939 remain 37%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 25000
c [simplification-3] penalized conflict interval 25000 = 1 * 25000
c [simplification-3] hard conflict limit 43502 (soft 31002 + delta 12500)
c [simplification-3] new conflict limit 31002 (hard 43502)
c 
c [simplification-4] limit 31002 conflicts (hard 43502) hit after 31003 conflicts
c [basicprobe-2] limit 5111850 penalty 0 = 0 + 0
c [basicprobe-2-0] 1943 sched 34%, 32 failed, 0 lifted, 828 hbrs
c [decomp-10] removed 37 variables
c [basicprobe-2-1] 2513 sched 44%, 21 failed, 0 lifted, 301 hbrs
c [decomp-11] removed 21 variables
c [basicprobe-2-2] 2571 sched 45%, 3 failed, 0 lifted, 56 hbrs
c [decomp-12] removed 3 variables
c [basicprobe-2-3] 2574 sched 45%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-2-4] 2574 sched 45%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-4] fully completed probing
c [basicprobe-2-4] 56 units = 56 failed (100%) + 0 lifted (0%)
c [basicprobe-2-4] removed 61 variables, found 1199 hbrs
c [unhide-3] limit 204474 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 739 tauts, 0 hbrs, 10698 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 5762 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 49 blocked clauses
c [block-1] 49 < 1/100 * 55409 = 554 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 347 (1%) of length 8
c [cce-1-1] eliminated 195 clauses out of 381 (51%) of length 7
c [cce-1-1] eliminated 119 clauses out of 4662 (3%) of length 6
c [cce-1-1] eliminated 1643 clauses out of 3454 (48%) of length 5
c [cce-1-1] eliminated 923 clauses out of 4410 (21%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2883 large clauses in 9378921 steps
c [cce-1-1] allowing another 4689460 steps for small clauses
c [cce-1-1] scheduling 22448 clauses = 8052 binary + 14396 ternary
c [cce-1-1] tried to eliminate 22448 small clauses 100%
c [cce-1-1] eliminated 2385 binary clauses 30%
c [cce-1-1] eliminated 2715 ternary clauses 19%
c [cce-1-1] eliminated 5100 small clauses 23%
c [cce-1-1] eliminated 5100 small clauses in 18349856 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7983 covered clauses in round 1
c [cce-1-2] eliminated 1 clauses out of 4543 (0%) of length 6
c [cce-1-2] eliminated 1 clauses out of 1811 (0%) of length 5
c [cce-1-2] eliminated 20 clauses out of 3487 (1%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 22 large clauses in 6252446 steps
c [cce-1-2] allowing another 3126223 steps for small clauses
c [cce-1-2] scheduling 17348 clauses = 5667 binary + 11681 ternary
c [cce-1-2] tried to eliminate 17348 small clauses 100%
c [cce-1-2] eliminated 381 binary clauses 7%
c [cce-1-2] eliminated 481 ternary clauses 4%
c [cce-1-2] eliminated 862 small clauses 5%
c [cce-1-2] eliminated 862 small clauses in 11175723 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 884 covered clauses in round 2
c [cce-1-3] incomplete large round (ACCE)
c [cce-1-3] allowing another 237220 steps for small clauses
c [cce-1-3] scheduling 16486 clauses = 5286 binary + 11200 ternary
c [cce-1-3] tried to eliminate 587 small clauses 4%
c [cce-1-3] eliminated 18 binary clauses 0%
c [cce-1-3] eliminated 9 ternary clauses 0%
c [cce-1-3] eliminated 27 small clauses 0%
c [cce-1-3] eliminated 27 small clauses in 474427 steps
c [cce-1-3] incomplete small round (ACCE)
c [cce-1-3] eliminated 27 covered clauses in round 3
c [cce-1] eliminated 8894 covered clauses in TOTAL during 3 rounds
c [bca-1] limit of 10000000 steps and 93432 added (scaled 2)
c [bca-1] 8622 out of 11526 literals actually usable 75%
c [bca-1] added 0 blocked clauses in 46154 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1886 pos 32.7% + 3876 neg 67.3% = 5762 sched 100.0% ret 0
c [sweep-1-1] 1131195 steps 29 queries 683.66 avg class size
c [sweep-1-1] 903 decisions 29 SAT calls 68.66 avg env size
c [sweep-1-1] 5226 variables remain 91% (536 retained 9%)
c [decomp-14] removed 2 variables
c [sweep-1-1] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 2 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-4] 44644 negative 96.1% of 46465 except 1821 3.9%
c [phase-count-4] 35109 positive 75.6% of 46465 except 11356 24.4%
c [phase-count-4] less non-negative clauses 1821 than limit 4600 (10.0%)
c [phase-count-4] non-pos/non-neg = 11356/1821 = 6.24 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1862 negative 100%
c [sort-queue-4] sorted 3914 enqueued variables after 31003 conflicts
c [score-dist-4] active 1846 (32%), one 758 (13%), zero 3156 (55%)
c [score-dist-4] max exp 655, different 362 (55%)
c [score-dist-4] median active exp 584, avg 504.3
c [simplification-4] removed 63 variables 1.1% (5760 remain 20%)
c [simplification-4] removed 10474 irredundant clauses 18.4% (46465 remain 30%)
c [simplification-4] maximum reduction of 18% = max (1%, 18%)
c [simplification-4] large reduction 18% >= 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 43003 (soft 33003 + delta 10000)
c [simplification-4] new conflict limit 33003 (hard 43003)
c 
c [simplification-5] limit 33003 conflicts (hard 43003) hit after 33003 conflicts
c [quatres-1] found 4668 quaternary clauses 26% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 28 single-self-subsuming ternary resolvents
c [quatres-1-2] added 526 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 5760 free variables schedulable
c [ternres-1] 7501 ternary resolvents (21 bin, 7480 trn)
c [ternres-1] 1 variables remain 0% (5759 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 60 xors of average arity 3.0
c [gauss-1] connected 180 occurrences of 18 variables (average 10.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 323 schedulable variables 6%
c [simpleprobe-3] limit 4440548 penalty 0 = 0 + 0
c [decomp-16] removed 1 variables
c [simpleprobe-3] 507 variables remain 9% (5252 retained 91%)
c [simpleprobe-3] removed 1 variables, found 1365 hbrs, 0 units
c [transred-1] limit 1110137 with penalty 0 = 0 + 0
c [transred-1] removed 1330 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 186 (1%) of length 7
c [cce-2-1] eliminated 2 clauses out of 4542 (0%) of length 6
c [cce-2-1] eliminated 1 clauses out of 3466 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 5 large clauses in 6131092 steps
c [cce-2-1] allowing another 3065546 steps for small clauses
c [cce-2-1] scheduling 24758 clauses = 5272 binary + 19486 ternary
c [cce-2-1] tried to eliminate 24758 small clauses 100%
c [cce-2-1] eliminated 18 binary clauses 0%
c [cce-2-1] eliminated 4767 ternary clauses 24%
c [cce-2-1] eliminated 4785 small clauses 19%
c [cce-2-1] eliminated 4785 small clauses in 13860442 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 4790 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 2929318 steps for small clauses
c [cce-2-2] scheduling 19973 clauses = 5254 binary + 14719 ternary
c [cce-2-2] tried to eliminate 19973 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 4790 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5759 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 222027430 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 738 variables 13% in round 1 in 13962323 steps
c [elim-4-1] backward subsumption/strengthening limit 13962300
c [elim-4-1-1] backward checking 2206 touched variables 38%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 1 clauses in 1753668 steps
c [elim-4-1] rescheduled 5 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 53268 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 738 = 13% variables out of 5759 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1627 pos 35.6% + 2941 neg 64.4% = 4568 sched 91.0% ret 453
c [sweep-2-1] 1009527 steps 28 queries 593.18 avg class size
c [sweep-2-1] 1145 decisions 24 SAT calls 126.88 avg env size
c [sweep-2-1] 4226 variables remain 84% (795 retained 16%)
c [decomp-17] removed 3 variables
c [sweep-2-1] removed 3 vars (0 failed, 3 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 3 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-5] 38693 negative 96.1% of 40272 except 1579 3.9%
c [phase-count-5] 28963 positive 71.9% of 40272 except 11309 28.1%
c [phase-count-5] less non-negative clauses 1579 than limit 4000 (10.0%)
c [phase-count-5] non-pos/non-neg = 11309/1579 = 7.16 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1424 negative 100%
c [sort-queue-5] sorted 3101 enqueued variables after 33003 conflicts
c [score-dist-5] active 1917 (38%), one 602 (12%), zero 2499 (50%)
c [score-dist-5] max exp 721, different 358 (50%)
c [score-dist-5] median active exp 666, avg 577.7
c [simplification-5] removed 742 variables 12.9% (5018 remain 18%)
c [simplification-5] removed 6193 irredundant clauses 13.3% (40272 remain 26%)
c [simplification-5] maximum reduction of 13% = max (13%, 13%)
c [simplification-5] large reduction 13% >= 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 45003 (soft 35003 + delta 10000)
c [simplification-5] new conflict limit 35003 (hard 45003)
c 
c [simplification-6] limit 35003 conflicts (hard 45003) hit after 35003 conflicts
c [quatres-2] found 4837 quaternary clauses 27% in total
c [quatres-2-2] added 60 single-self-subsuming ternary resolvents
c [quatres-2-2] added 159 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 474 ternary resolvents (3 bin, 471 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 459 at-most-one constraints of average size 3.6
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 459 out of 459 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 9440 literals 94%
c [treelook-3] scheduling used 300323 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 300030 steps
c [treelook-3] 9400 literals remain 94%
c [treelook-3] 5004 variables remain to probed next time 100%
c [treelook-3] removed 1 variables, found 490 hbrs
c [unhide-4] limit 120103 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 933 tauts, 0 hbrs, 14327 literals
c [transred-2] limit 1201034 with penalty 0 = 0 + 0
c [transred-2] removed 275 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5017 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 27 blocked clauses
c [block-2] 27 < 1/100 * 40259 = 402 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-3-1] eliminated 7 clauses out of 158 (4%) of length 9
c [cce-3-1] eliminated 13 clauses out of 382 (3%) of length 8
c [cce-3-1] eliminated 21 clauses out of 172 (12%) of length 7
c [cce-3-1] eliminated 12 clauses out of 4566 (0%) of length 6
c [cce-3-1] eliminated 216 clauses out of 1864 (12%) of length 5
c [cce-3-1] eliminated 369 clauses out of 3198 (12%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 640 large clauses in 7216973 steps
c [cce-3-1] allowing another 3608486 steps for small clauses
c [cce-3-1] scheduling 15617 clauses = 4389 binary + 11228 ternary
c [cce-3-1] tried to eliminate 15617 small clauses 100%
c [cce-3-1] eliminated 167 binary clauses 4%
c [cce-3-1] eliminated 526 ternary clauses 5%
c [cce-3-1] eliminated 693 small clauses 4%
c [cce-3-1] eliminated 693 small clauses in 11290082 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 1333 covered clauses in round 1
c [cce-3-2] eliminated 15 clauses out of 1648 (1%) of length 5
c [cce-3-2] eliminated 36 clauses out of 2829 (1%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 51 large clauses in 6399647 steps
c [cce-3-2] allowing another 3199823 steps for small clauses
c [cce-3-2] scheduling 14925 clauses = 4222 binary + 10703 ternary
c [cce-3-2] tried to eliminate 14925 small clauses 100%
c [cce-3-2] eliminated 8 binary clauses 0%
c [cce-3-2] eliminated 12 ternary clauses 0%
c [cce-3-2] eliminated 20 small clauses 0%
c [cce-3-2] eliminated 20 small clauses in 10295088 steps
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 71 covered clauses in round 2
c [cce-3-3] eliminated 1 clauses out of 1633 (0%) of length 5
c [cce-3-3] eliminated 3 clauses out of 2793 (0%) of length 4
c [cce-3-3] completed large round (ACCE)
c [cce-3-3] eliminated 4 large clauses in 6358673 steps
c [cce-3-3] allowing another 3179336 steps for small clauses
c [cce-3-3] scheduling 14905 clauses = 4214 binary + 10691 ternary
c [cce-3-3] tried to eliminate 11220 small clauses 75%
c [cce-3-3] incomplete small round (ACCE)
c [cce-3-3] eliminated 4 covered clauses in round 3
c [cce-3] eliminated 1408 covered clauses in TOTAL during 3 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5017 variables 100%
c [elim-5] limit of 24020683 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 81 variables 2% in round 1 in 12985596 steps
c [elim-5-1] backward subsumption/strengthening limit 11035087
c [elim-5-1-1] backward checking 515 touched variables 10%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 7 and strengthened 1 clauses in 494497 steps
c [elim-5-1] rescheduled 19 variables 0% by backward subsumption
c [elim-5-2] eliminated 8 variables 0% in round 2 in 132420 steps
c [elim-5-2] backward subsumption/strengthening limit 132400
c [elim-5-2-1] backward checking 55 touched variables 1%
c [elim-5-2-1] incomplete backward checking 0 remain 0%
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 132401 steps
c [elim-5-2] fully rescheduled 4928 variables 98%
c [elim-5] incomplete 47 not tried 1% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 120 = 2% variables out of 5017 scheduled
c [bca-2] limit of 10000000 steps and 77656 added (scaled 2)
c [bca-2] 6610 out of 9796 literals actually usable 67%
c [bca-2] added 0 blocked clauses in 46125 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1469 pos 35.6% + 2654 neg 64.4% = 4123 sched 84.2% ret 774
c [sweep-3-1] 1011591 steps 93 queries 211.23 avg class size
c [sweep-3-1] 1650 decisions 80 SAT calls 51.36 avg env size
c [sweep-3-1] 3306 variables remain 68% (1591 retained 32%)
c [decomp-20] removed 12 variables
c [sweep-3-1] removed 12 vars (0 failed, 12 eqs, 24 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 12 vars in TOTAL (1 rounds, 92 queries)
c [phase-count-6] 37032 negative 96.0% of 38578 except 1546 4.0%
c [phase-count-6] 27565 positive 71.5% of 38578 except 11013 28.5%
c [phase-count-6] less non-negative clauses 1546 than limit 3800 (10.0%)
c [phase-count-6] non-pos/non-neg = 11013/1546 = 7.12 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 974 negative 100%
c [sort-queue-6] sorted 2873 enqueued variables after 35003 conflicts
c [score-dist-6] active 2012 (41%), one 605 (12%), zero 2268 (46%)
c [score-dist-6] max exp 779, different 387 (50%)
c [score-dist-6] median active exp 723, avg 599.8
c [simplification-6] removed 133 variables 2.7% (4885 remain 17%)
c [simplification-6] removed 1694 irredundant clauses 4.2% (38578 remain 25%)
c [simplification-6] maximum reduction of 4% = max (3%, 4%)
c [simplification-6] geometric conflict interval increment 5000 = 25000 / 5
c [simplification-6] new conflict interval 30000
c [simplification-6] penalized conflict interval 30000 = 1 * 30000
c [simplification-6] hard conflict limit 80003 (soft 65003 + delta 15000)
c [simplification-6] new conflict limit 65003 (hard 80003)
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    8.8    4884    38578     38430   35039  14551  4199    8    20   12  41%    444   12    8    3  254%
c 
c [simplification-7] limit 65003 conflicts (hard 80003) hit after 65006 conflicts
c [quatres-3] found 4547 quaternary clauses 23% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 23 single-self-subsuming ternary resolvents
c [quatres-3-2] added 72 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 4879 free variables schedulable
c [ternres-3] 515 ternary resolvents (0 bin, 515 trn)
c [ternres-3] 2012 variables remain 41% (2867 retained 59%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 57 xors of average arity 3.0
c [gauss-2] connected 171 occurrences of 29 variables (average 5.9)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 14563820 penalty 0 = 0 + 0
c [basicprobe-3-0] 2455 sched 51%, 21 failed, 0 lifted, 1298 hbrs
c [decomp-22] removed 24 variables
c [basicprobe-3-1] 2718 sched 56%, 6 failed, 0 lifted, 195 hbrs
c [decomp-23] removed 6 variables
c [basicprobe-3-2] 2745 sched 57%, 1 failed, 0 lifted, 76 hbrs
c [decomp-24] removed 1 variables
c [basicprobe-3-3] 2713 sched 56%, 2 failed, 0 lifted, 54 hbrs
c [decomp-25] removed 2 variables
c [basicprobe-3-4] 2689 sched 56%, 1 failed, 0 lifted, 48 hbrs
c [decomp-26] removed 1 variables
c [basicprobe-3-5] 2713 sched 56%, 1 failed, 0 lifted, 13 hbrs
c [decomp-27] removed 1 variables
c [basicprobe-3-6] 2705 sched 56%, 1 failed, 0 lifted, 17 hbrs
c [decomp-28] removed 1 variables
c [basicprobe-3-7] 2700 sched 56%, 0 failed, 0 lifted, 26 hbrs
c [basicprobe-3-8] 2706 sched 56%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 33 units = 33 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 36 variables, found 1729 hbrs
c [bate-1] eliminated 26 asymmetric tautologies during probing
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 322 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 98 (1%) of length 9
c [cce-4-1] eliminated 1 clauses out of 424 (0%) of length 8
c [cce-4-1] eliminated 8 clauses out of 117 (7%) of length 7
c [cce-4-1] eliminated 14 clauses out of 4593 (0%) of length 6
c [cce-4-1] eliminated 7 clauses out of 1495 (0%) of length 5
c [cce-4-1] eliminated 68 clauses out of 2764 (2%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 99 large clauses in 5020480 steps
c [cce-4-1] allowing another 2510240 steps for small clauses
c [cce-4-1] scheduling 14196 clauses = 4172 binary + 10024 ternary
c [cce-4-1] tried to eliminate 14196 small clauses 100%
c [cce-4-1] eliminated 70 binary clauses 2%
c [cce-4-1] eliminated 20 ternary clauses 0%
c [cce-4-1] eliminated 90 small clauses 1%
c [cce-4-1] eliminated 90 small clauses in 8035605 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 189 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2498616 steps for small clauses
c [cce-4-2] scheduling 14107 clauses = 4102 binary + 10005 ternary
c [cce-4-2] tried to eliminate 14107 small clauses 100%
c [cce-4-2] eliminated 1 ternary clauses 0%
c [cce-4-2] eliminated 1 small clauses 0%
c [cce-4-2] eliminated 1 small clauses in 7833947 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 1 covered clauses in round 2
c [cce-4-3] completed large round (ATE)
c [cce-4-3] allowing another 2502129 steps for small clauses
c [cce-4-3] scheduling 14106 clauses = 4102 binary + 10004 ternary
c [cce-4-3] tried to eliminate 14106 small clauses 100%
c [cce-4-3] completed small round (ATE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 190 covered clauses in TOTAL during 3 rounds
c [cce-4] 190 < 1/100 * 37275 = 372 considered unsuccessful
c [elim-6] 47 variables 1% will be scheduled this time
c [elim-6] scheduled 47 variables 1%
c [elim-6] limit of 58255281 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 2571715 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 47 scheduled
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1221 pos 37.2% + 2062 neg 62.8% = 3283 sched 67.8% ret 1560
c [sweep-4-1] 1193603 steps 94 queries 571.20 avg class size
c [sweep-4-1] 1219 decisions 87 SAT calls 33.59 avg env size
c [sweep-4-1] 2733 variables remain 56% (2110 retained 44%)
c [decomp-30] removed 7 variables
c [sweep-4-1] removed 7 vars (0 failed, 7 eqs, 14 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 7 vars in TOTAL (1 rounds, 93 queries)
c [phase-count-7] 35540 negative 95.8% of 37085 except 1545 4.2%
c [phase-count-7] 26803 positive 72.3% of 37085 except 10282 27.7%
c [phase-count-7] less non-negative clauses 1545 than limit 3700 (10.0%)
c [phase-count-7] non-pos/non-neg = 10282/1545 = 6.66 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 460 negative 100%
c [sort-queue-7] sorted 2825 enqueued variables after 65006 conflicts
c [score-dist-7] active 2011 (42%), one 897 (19%), zero 1928 (40%)
c [score-dist-7] max exp 686, different 373 (54%)
c [score-dist-7] median active exp 636, avg 549.4
c [simplification-7] removed 43 variables 0.9% (4836 remain 17%)
c [simplification-7] removed 1493 irredundant clauses 3.9% (37085 remain 24%)
c [simplification-7] maximum reduction of 4% = max (1%, 4%)
c [simplification-7] geometric conflict interval increment 6000 = 30000 / 5
c [simplification-7] new conflict interval 36000
c [simplification-7] penalized conflict interval 36000 = 1 * 36000
c [simplification-7] hard conflict limit 119006 (soft 101006 + delta 18000)
c [simplification-7] new conflict limit 101006 (hard 119006)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   15.0    4836    37085     66246   21485  14012  4548    9    20   11  44%    247    8    9    5  178%
c 
c [simplification-8] limit 101006 conflicts (hard 119006) hit after 101006 conflicts
c [quatres-4] found 4951 quaternary clauses 21% in total
c [quatres-4-1] removed 12 duplicate quaternary clauses
c [quatres-4-2] added 28 single-self-subsuming ternary resolvents
c [quatres-4-2] added 93 quaternary resolvents
c [ternres-4] limit 4814213 with penalty 0 = 0 + 0
c [ternres-4] 1996 schedulable variables 41%
c [ternres-4] 991 ternary resolvents (3 bin, 988 trn)
c [ternres-4] 225 variables remain 5% (4611 retained 95%)
c [simpleprobe-4] 400 schedulable variables 8%
c [simpleprobe-4] limit 19256852 penalty 0 = 0 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 2103 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 736 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 14442630 penalty 0 = 0 + 0
c [sweep-5-1] 1256 pos 46.0% + 1477 neg 54.0% = 2733 sched 56.5% ret 2103
c [sweep-5-1] 5865106 steps 579 queries 83.94 avg class size
c [sweep-5-1] 6165 decisions 521 SAT calls 25.00 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-33] removed 58 variables
c [sweep-5-1] removed 58 vars (0 failed, 59 eqs, 109 impls)
c [sweep-5-2] 1879 pos 39.3% + 2899 neg 60.7% = 4778 sched 100.0% ret 0
c [sweep-5-2] 6241672 steps 544 queries 64.61 avg class size
c [sweep-5-2] 6938 decisions 539 SAT calls 33.01 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-34] removed 9 variables
c [sweep-5-2] removed 9 vars (0 failed, 9 eqs, 16 impls)
c [sweep-5-3] 1875 pos 39.3% + 2894 neg 60.7% = 4769 sched 100.0% ret 0
c [sweep-5-3] 2753558 steps 38 queries 635.29 avg class size
c [sweep-5-3] 1546 decisions 38 SAT calls 118.39 avg env size
c [sweep-5-3] 3869 variables remain 81% (900 retained 19%)
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 67 vars in TOTAL (3 rounds, 1158 queries)
c [sort-queue-8] sorted 2110 enqueued variables after 101006 conflicts
c [score-dist-8] active 2659 (56%), one 1099 (23%), zero 1011 (21%)
c [score-dist-8] max exp 557, different 386 (69%)
c [score-dist-8] median active exp 431, avg 390.2
c [simplification-8] removed 67 variables 1.4% (4769 remain 17%)
c [simplification-8] removed 10 irredundant clauses 0.0% (37075 remain 24%)
c [simplification-8] maximum reduction of 1% = max (1%, 0%)
c [simplification-8] geometric conflict interval increment 18000 = 36000 / 2
c [simplification-8] new conflict interval 54000
c [simplification-8] penalized conflict interval 54000 = 1 * 54000
c [simplification-8] hard conflict limit 182006 (soft 155006 + delta 27000)
c [simplification-8] new conflict limit 155006 (hard 182006)
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 -   22.3    4769    37075    111229   28759  13333  6054   10    21   11  47%    633    4   10    7  144%
c 
c [simplification-9] limit 155006 conflicts (hard 182006) hit after 155545 conflicts
c [quatres-5] found 5366 quaternary clauses 19% in total
c [quatres-5-2] added 35 single-self-subsuming ternary resolvents
c [quatres-5-2] added 50 quaternary resolvents
c [ternres-5] limit 7866754 with penalty 0 = 0 + 0
c [ternres-5] 217 schedulable variables 5%
c [ternres-5] 1137 ternary resolvents (4 bin, 1133 trn)
c [ternres-5] 19 variables remain 0% (4750 retained 100%)
c [treelook-4] limit 786675 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 9527 literals 100%
c [treelook-4] scheduling used 396098 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 786675 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 794419 steps
c [treelook-4] 9132 literals remain 96%
c [treelook-4] 4757 variables remain to probed next time 100%
c [treelook-4] removed 0 variables, found 718 hbrs
c [unhide-5] limit 393337 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 112 tauts, 0 hbrs, 16025 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 599 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 4769 variables 100%
c [block-3] limit of 19666885 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 4 blocked clauses
c [block-3] 4 < 1/100 * 37052 = 370 considered unsuccessful
c [cce-5] limit of 19666885 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 4 clauses out of 87 (5%) of length 7
c [cce-5-1] eliminated 146 clauses out of 4603 (3%) of length 6
c [cce-5-1] eliminated 5 clauses out of 1458 (0%) of length 5
c [cce-5-1] eliminated 29 clauses out of 2712 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 184 large clauses in 6351527 steps
c [cce-5-1] allowing another 3175763 steps for small clauses
c [cce-5-1] scheduling 14210 clauses = 4346 binary + 9864 ternary
c [cce-5-1] tried to eliminate 14210 small clauses 100%
c [cce-5-1] eliminated 318 binary clauses 7%
c [cce-5-1] eliminated 70 ternary clauses 1%
c [cce-5-1] eliminated 388 small clauses 3%
c [cce-5-1] eliminated 388 small clauses in 10159827 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 572 covered clauses in round 1
c [cce-5-2] eliminated 1 clauses out of 1453 (0%) of length 5
c [cce-5-2] eliminated 1 clauses out of 2683 (0%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 2 large clauses in 5987372 steps
c [cce-5-2] allowing another 2993686 steps for small clauses
c [cce-5-2] scheduling 13831 clauses = 4028 binary + 9803 ternary
c [cce-5-2] tried to eliminate 13831 small clauses 100%
c [cce-5-2] eliminated 5 binary clauses 0%
c [cce-5-2] eliminated 10 ternary clauses 0%
c [cce-5-2] eliminated 15 small clauses 0%
c [cce-5-2] eliminated 15 small clauses in 8676944 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 17 covered clauses in round 2
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] allowing another 415058 steps for small clauses
c [cce-5-3] scheduling 13816 clauses = 4023 binary + 9793 ternary
c [cce-5-3] tried to eliminate 1012 small clauses 7%
c [cce-5-3] incomplete small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 589 covered clauses in TOTAL during 3 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 4769 variables 100%
c [elim-7] limit of 78667541 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 64 variables 1% in round 1 in 11733243 steps
c [elim-7-1] backward subsumption/strengthening limit 11733200
c [elim-7-1-1] backward checking 339 touched variables 7%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 6 clauses in 358240 steps
c [elim-7-1] rescheduled 20 variables 0% by backward subsumption
c [elim-7-2] no variable eliminated in round 2 in 501129 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 64 = 1% variables out of 4769 scheduled
c [bca-3] limit of 10000000 steps and 72580 added (scaled 2)
c [bca-3] 5303 out of 9412 literals actually usable 56%
c [bca-3] added 0 blocked clauses in 81959 steps
c [sweep-6] limit 2360026 penalty 0 = 0 + 0
c [sweep-6-1] 1530 pos 40.0% + 2294 neg 60.0% = 3824 sched 81.3% ret 881
c [sweep-6-1] 2376393 steps 74 queries 311.20 avg class size
c [sweep-6-1] 1744 decisions 74 SAT calls 61.28 avg env size
c [sweep-6-1] 2703 variables remain 57% (2002 retained 43%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 73 queries)
c [sort-queue-9] sorted 2490 enqueued variables after 155545 conflicts
c [score-dist-9] active 2215 (47%), one 1663 (35%), zero 827 (18%)
c [score-dist-9] max exp 909, different 471 (52%)
c [score-dist-9] median active exp 824, avg 706.1
c [simplification-9] removed 64 variables 1.3% (4705 remain 17%)
c [simplification-9] removed 1035 irredundant clauses 2.8% (36040 remain 23%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 13500 = 54000 / 4
c [simplification-9] new conflict interval 67500
c [simplification-9] penalized conflict interval 67500 = 1 * 67500
c [simplification-9] hard conflict limit 256795 (soft 223045 + delta 33750)
c [simplification-9] new conflict limit 223045 (hard 256795)
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 -   29.7    4705    36040    155890   35782  14275  6462    9    18   12  51%    826    0   10    8  122%
c i   34.2    4704    36040    193919   71980  14357  6473    8    17   19  50%    913   -2    5    9   63%
c -   34.8    4704    36040    198040   43653  14362  6474    9    17   13  51%  -1354   -1    9    9  105%
c -   39.4    4704    36040    236687   49629  14412  6478    9    17   19  53%   -319   -2    8    9   89%
c 
c [simplification-10] limit 223045 conflicts (hard 256795) hit after 256796 conflicts
c [quatres-6] found 5231 quaternary clauses 15% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-2] added 21 single-self-subsuming ternary resolvents
c [quatres-6-2] added 180 quaternary resolvents
c [ternres-6] limit 13082545 with penalty 0 = 0 + 0
c [ternres-6] 19 schedulable variables 0%
c [ternres-6] 1430 ternary resolvents (5 bin, 1425 trn)
c [ternres-6] 3 variables remain 0% (4701 retained 100%)
c [card-4] limit 817659 penalty 3 = 3 + 0
c [card-4] found 543 at-most-one constraints of average size 3.6
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 817659 for elimination
c [card-4] 543 out of 543 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 654127 penalty 2 = 2 + 0
c [gauss-3] extracted 57 xors of average arity 3.0
c [gauss-3] connected 171 occurrences of 43 variables (average 4.0)
c [gauss-3] limit 654127 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-4] limit 65412727 penalty 0 = 0 + 0
c [basicprobe-4-0] 2704 sched 57%, 1 failed, 0 lifted, 421 hbrs
c [decomp-40] removed 1 variables
c [basicprobe-4-1] 2736 sched 58%, 1 failed, 0 lifted, 52 hbrs
c [decomp-41] removed 1 variables
c [basicprobe-4-2] 2684 sched 57%, 1 failed, 0 lifted, 82 hbrs
c [decomp-42] removed 1 variables
c [basicprobe-4-3] 2699 sched 57%, 1 failed, 0 lifted, 31 hbrs
c [decomp-43] removed 1 variables
c [basicprobe-4-4] 2681 sched 57%, 1 failed, 0 lifted, 25 hbrs
c [decomp-44] removed 1 variables
c [basicprobe-4-5] 2662 sched 57%, 1 failed, 0 lifted, 26 hbrs
c [decomp-45] removed 1 variables
c [basicprobe-4-6] 2629 sched 56%, 1 failed, 0 lifted, 64 hbrs
c [decomp-46] removed 1 variables
c [basicprobe-4-7] 2572 sched 55%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-4-8] 2575 sched 55%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 7 variables, found 713 hbrs
c [bate-2] eliminated 6 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 361 transitive binary clauses
c [cce-6] limit of 65412727 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 1192 (0%) of length 5
c [cce-6-1] eliminated 22 clauses out of 2718 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 23 large clauses in 4489916 steps
c [cce-6-1] allowing another 2244958 steps for small clauses
c [cce-6-1] scheduling 13388 clauses = 3915 binary + 9473 ternary
c [cce-6-1] tried to eliminate 13388 small clauses 100%
c [cce-6-1] eliminated 62 binary clauses 2%
c [cce-6-1] eliminated 15 ternary clauses 0%
c [cce-6-1] eliminated 77 small clauses 1%
c [cce-6-1] eliminated 77 small clauses in 6392148 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 100 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 2250713 steps for small clauses
c [cce-6-2] scheduling 13311 clauses = 3853 binary + 9458 ternary
c [cce-6-2] tried to eliminate 13311 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 100 covered clauses in TOTAL during 2 rounds
c [cce-6] 100 < 1/100 * 35622 = 356 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 4697 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5233018220 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 50 variables 1% in round 1 in 11540691 steps
c [elim-8-1] backward subsumption/strengthening limit 11540600
c [elim-8-1-1] backward checking 650 touched variables 14%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 4 clauses in 587846 steps
c [elim-8-1] rescheduled 23 variables 0% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 228369 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 50 = 1% variables out of 4697 scheduled
c [sort-queue-10] sorted 3034 enqueued variables after 256796 conflicts
c [score-dist-10] active 1613 (35%), one 2296 (49%), zero 738 (16%)
c [score-dist-10] max exp 949, different 388 (41%)
c [score-dist-10] median active exp 860, avg 744.5
c [simplification-10] removed 57 variables 1.2% (4647 remain 16%)
c [simplification-10] removed 548 irredundant clauses 1.5% (35492 remain 23%)
c [simplification-10] maximum reduction of 2% = max (1%, 2%)
c [simplification-10] geometric conflict interval increment 22500 = 67500 / 3
c [simplification-10] new conflict interval 90000
c [simplification-10] penalized conflict interval 90000 = 1 * 90000
c [simplification-10] hard conflict limit 391796 (soft 346796 + delta 45000)
c [simplification-10] new conflict limit 346796 (hard 391796)
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 -   46.1    4647    35492    274529   51326  15298  5666   10    18   13  53%    270    1    9    9  104%
c -   51.1    4647    35492    312720   55844  15339  5672    9    14   19  61%    603   -2    9    9  107%
c 
c [simplification-11] limit 346796 conflicts (hard 391796) hit after 346796 conflicts
c [quatres-7] found 5736 quaternary clauses 14% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-2] added 51 single-self-subsuming ternary resolvents
c [quatres-7-2] added 81 quaternary resolvents
c [ternres-7] limit 18666515 with penalty 0 = 0 + 0
c [ternres-7] 3 schedulable variables 0%
c [ternres-7] 1706 ternary resolvents (7 bin, 1699 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 191 transitive binary clauses
c [transred-7] found 3 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 4639 variables 100%
c [elim-9] limit of 373330317 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 116 variables 3% in round 1 in 10958065 steps
c [elim-9-1] backward subsumption/strengthening limit 10958000
c [elim-9-1-1] backward checking 1062 touched variables 23%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 13 and strengthened 62 clauses in 832200 steps
c [elim-9-1] rescheduled 447 variables 10% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 1128410 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 116 = 3% variables out of 4639 scheduled
c [sweep-7] limit 2799977 penalty 1 = 1 + 0
c [sweep-7-1] 950 pos 36.5% + 1653 neg 63.5% = 2603 sched 57.6% ret 1920
c [sweep-7-1] 2857575 steps 202 queries 153.37 avg class size
c [sweep-7-1] 2622 decisions 199 SAT calls 32.28 avg env size
c [sweep-7-1] 999 variables remain 22% (3524 retained 78%)
c [decomp-49] removed 4 variables
c [sweep-7-1] removed 4 vars (0 failed, 3 eqs, 7 impls)
c [sweep-7] removed 4 vars in TOTAL (1 rounds, 201 queries)
c [sort-queue-11] sorted 2610 enqueued variables after 346796 conflicts
c [score-dist-11] active 1909 (42%), one 2058 (46%), zero 552 (12%)
c [score-dist-11] max exp 606, different 312 (51%)
c [score-dist-11] median active exp 558, avg 513.5
c [simplification-11] removed 128 variables 2.8% (4519 remain 16%)
c [simplification-11] removed 1249 irredundant clauses 3.5% (34243 remain 22%)
c [simplification-11] maximum reduction of 4% = max (3%, 4%)
c [simplification-11] geometric conflict interval increment 18000 = 90000 / 5
c [simplification-11] new conflict interval 108000
c [simplification-11] penalized conflict interval 108000 = 1 * 108000
c [simplification-11] hard conflict limit 508796 (soft 454796 + delta 54000)
c [simplification-11] new conflict limit 454796 (hard 508796)
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 -   57.1    4519    34243    349172   55802  15882  5403   10    19   14  52%    783    3   11    9  116%
c -   62.7    4519    34243    388212   60149  15912  5407    9    17   14  57%    891   -1   10    9  106%
c i   66.8    4518    34243    417547   86680  15964  5421    7    10   21  71%    939   -6    6    9   65%
c -   68.5    4513    34243    428779   64957  15970  5421    9    15   22  60%  -2038   -0   10    9  106%
c -   74.2    4513    34243    467777   68527  15996  5422    9    15   22  62%   -665   -2    8    9   92%
c 
c [simplification-12] limit 454796 conflicts (hard 508796) hit after 505795 conflicts
c [quatres-8] found 4345 quaternary clauses 10% in total
c [quatres-8-1] removed 9 duplicate quaternary clauses
c [quatres-8-2] added 87 single-self-subsuming ternary resolvents
c [quatres-8-2] added 48 quaternary resolvents
c [ternres-8] limit 29722305 with penalty 0 = 0 + 0
c [ternres-8] all 4513 free variables schedulable
c [ternres-8] 4466 ternary resolvents (45 bin, 4421 trn)
c [ternres-8] 36 variables remain 1% (4477 retained 99%)
c [decomp-50] removed 6 variables
c [simpleprobe-5] all 4513 free variables schedulable
c [simpleprobe-5] limit 59444611 penalty 1 = 1 + 0
c [decomp-51] removed 3 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 3 variables, found 2761 hbrs, 2 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1115 transitive binary clauses
c [cce-7] limit of 74305764 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 9 clauses out of 80 (11%) of length 9
c [cce-7-1] eliminated 1 clauses out of 333 (0%) of length 8
c [cce-7-1] eliminated 8 clauses out of 4461 (0%) of length 6
c [cce-7-1] eliminated 21 clauses out of 485 (4%) of length 5
c [cce-7-1] eliminated 234 clauses out of 1723 (14%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 273 large clauses in 3579417 steps
c [cce-7-1] allowing another 1789708 steps for small clauses
c [cce-7-1] scheduling 13102 clauses = 3752 binary + 9350 ternary
c [cce-7-1] tried to eliminate 13102 small clauses 100%
c [cce-7-1] eliminated 114 binary clauses 3%
c [cce-7-1] eliminated 169 ternary clauses 2%
c [cce-7-1] eliminated 283 small clauses 2%
c [cce-7-1] eliminated 283 small clauses in 5568331 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 556 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 184 (1%) of length 7
c [cce-7-2] eliminated 7 clauses out of 1489 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 8 large clauses in 3511357 steps
c [cce-7-2] allowing another 1755678 steps for small clauses
c [cce-7-2] scheduling 12819 clauses = 3638 binary + 9181 ternary
c [cce-7-2] tried to eliminate 12819 small clauses 100%
c [cce-7-2] eliminated 1 ternary clauses 0%
c [cce-7-2] eliminated 1 small clauses 0%
c [cce-7-2] eliminated 1 small clauses in 5348977 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 9 covered clauses in round 2
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] allowing another 1756749 steps for small clauses
c [cce-7-3] scheduling 12818 clauses = 3638 binary + 9180 ternary
c [cce-7-3] tried to eliminate 12818 small clauses 100%
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 0 covered clauses in round 3
c [cce-7] eliminated 565 covered clauses in TOTAL during 3 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 4510 variables 100%
c [elim-10] limit of 594446116 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 21 variables 0% in round 1 in 10344694 steps
c [elim-10-1] backward subsumption/strengthening limit 10344600
c [elim-10-1-1] backward checking 559 touched variables 12%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 1 and strengthened 11 clauses in 546006 steps
c [elim-10-1] rescheduled 72 variables 2% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 253824 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 21 = 0% variables out of 4510 scheduled
c [elim-10] 21 < 1/100 * 4510 = 45 considered unsuccessful
c [sweep-8] limit 8916691 penalty 0 = 0 + 0
c [sweep-8-1] 558 pos 55.9% + 441 neg 44.1% = 999 sched 22.3% ret 3490
c [sweep-8-1] 4889510 steps 300 queries 39.02 avg class size
c [sweep-8-1] 3774 decisions 297 SAT calls 26.82 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-52] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 2 eqs, 7 impls)
c [sweep-8-2] 1864 pos 41.5% + 2623 neg 58.5% = 4487 sched 100.0% ret 0
c [sweep-8-2] 4054444 steps 53 queries 298.15 avg class size
c [sweep-8-2] 1637 decisions 52 SAT calls 70.29 avg env size
c [sweep-8-2] 2961 variables remain 66% (1526 retained 34%)
c [sweep-8-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-8] 2 < 1/1000 * 4489 = 4 considered unsuccessful
c [sweep-8] removed 2 vars in TOTAL (2 rounds, 351 queries)
c [sort-queue-12] sorted 2268 enqueued variables after 505795 conflicts
c [score-dist-12] active 2219 (49%), one 1819 (41%), zero 449 (10%)
c [score-dist-12] max exp 945, different 465 (49%)
c [score-dist-12] median active exp 833, avg 738.1
c [simplification-12] removed 26 variables 0.6% (4487 remain 16%)
c [simplification-12] removed 1060 irredundant clauses 3.1% (33183 remain 21%)
c [simplification-12] maximum reduction of 3% = max (1%, 3%)
c [simplification-12] geometric conflict interval increment 27000 = 108000 / 4
c [simplification-12] new conflict interval 135000
c [simplification-12] penalized conflict interval 135000 = 1 * 135000
c [simplification-12] hard conflict limit 708295 (soft 640795 + delta 67500)
c [simplification-12] new conflict limit 640795 (hard 708295)
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 -   82.4    4487    33183    509727   69165  19987  6649    9    15   15  58%    134   -0    9    9  103%
c -   88.9    4487    33183    549769   72646  20017  6654    9    15   16  60%    541   -0   10    9  109%
c -   96.3    4487    33183    590644   76082  20026  6657    9    13   24  66%    765   -2    8    9   87%
c -  104.2    4487    33183    631751   78700  20040  6661    9    16   24  59%    886    0    8    9   90%
c 
c [simplification-13] limit 640795 conflicts (hard 708295) hit after 640795 conflicts
c [quatres-9] found 4756 quaternary clauses 8% in total
c [quatres-9-1] removed 15 duplicate quaternary clauses
c [quatres-9-1] added 3 double-self-subsuming ternary resolvents
c [quatres-9-2] added 91 single-self-subsuming ternary resolvents
c [quatres-9-2] added 140 quaternary resolvents
c [ternres-9] limit 40946646 with penalty 0 = 0 + 0
c [ternres-9] 36 schedulable variables 1%
c [ternres-9] 5221 ternary resolvents (77 bin, 5144 trn)
c [ternres-9] 4 variables remain 0% (4483 retained 100%)
c [unhide-6] limit 1023666 with penalty 3 = 3 + 0
c [unhide-6-6] 0 units, 1 failed, 3410 tauts, 0 hbrs, 24851 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 537 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4486 variables 100%
c [block-4] limit of 51183308 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 2 blocked clauses
c [block-4] 2 < 1/100 * 33174 = 331 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 2047332340 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 273 (0%) of length 8
c [cce-8-1] eliminated 9 clauses out of 4484 (0%) of length 6
c [cce-8-1] eliminated 5 clauses out of 343 (1%) of length 5
c [cce-8-1] eliminated 13 clauses out of 1585 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 28 large clauses in 3073460 steps
c [cce-8-1] allowing another 1536730 steps for small clauses
c [cce-8-1] scheduling 17033 clauses = 3663 binary + 13370 ternary
c [cce-8-1] tried to eliminate 17033 small clauses 100%
c [cce-8-1] eliminated 40 binary clauses 1%
c [cce-8-1] eliminated 459 ternary clauses 3%
c [cce-8-1] eliminated 499 small clauses 3%
c [cce-8-1] eliminated 499 small clauses in 5317385 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 527 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1548511 steps for small clauses
c [cce-8-2] scheduling 16534 clauses = 3623 binary + 12911 ternary
c [cce-8-2] tried to eliminate 16534 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 527 covered clauses in TOTAL during 2 rounds
c [bca-4] limit of 10000000 steps and 65772 added (scaled 2)
c [bca-4] 4663 out of 8974 literals actually usable 52%
c [bca-4] added 4 blocked clauses in 96226 steps
c [sort-queue-13] sorted 2975 enqueued variables after 640795 conflicts
c [score-dist-13] active 1511 (34%), one 2532 (56%), zero 443 (10%)
c [score-dist-13] max exp 821, different 379 (46%)
c [score-dist-13] median active exp 685, avg 591.6
c [simplification-13] removed 1 variables 0.0% (4486 remain 16%)
c [simplification-13] removed 547 irredundant clauses 1.6% (32636 remain 21%)
c [simplification-13] maximum reduction of 2% = max (0%, 2%)
c [simplification-13] geometric conflict interval increment 45000 = 135000 / 3
c [simplification-13] new conflict interval 180000
c [simplification-13] penalized conflict interval 180000 = 1 * 180000
c [simplification-13] hard conflict limit 910795 (soft 820795 + delta 90000)
c [simplification-13] new conflict limit 820795 (hard 910795)
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 -  113.4    4486    32636    675067   82687  23937  5518    9    15   23  62%    953   -0    9    9  104%
c -  122.1    4486    32636    717445   85488  23960  5520    9    14   23  65%    987   -0    9    9   99%
c i  124.8    4485    32636    731545   98257  23979  5524    9    13   29  67%    994   -2    6    9   66%
c -  130.5    4485    32636    761282   89052  23999  5527    8    12   24  65%  -2161   -2    9    9  101%
c i  131.0    4484    32636    764478   91882  24019  5536    8    12   28  66%  -2010   -2    5    9   63%
c i  132.0    4471    32636    770511   97454  24020  5537    9    13   28  64%  -2218   -1    8    9   90%
c i  132.3    4470    32636    771971   98680  24035  5544    8    12   28  66%  -2218   -2    6    9   70%
c i  132.8    4464    32636    774874  101341  24046  5547    8    11   29  67%  -2120   -3    5    9   57%
c i  133.2    4461    32636    776921  103123  24060  5554    7    10   29  69%  -2064   -3    5    9   64%
c i  133.2    4457    32636    777198  103336  24070  5560    7    10   29  70%  -2060   -4    6    9   68%
c i  133.3    4455    32636    777935  103970  24079  5564    7    10   29  70%  -2043   -4    6    9   66%
c i  133.3    4452    32636    777956  103989  24079  5564    7    10   29  70%  -2042   -4    6    9   70%
c i  133.3    4448    32636    777957  103989  24079  5564    7    10   29  70%  -2042   -4    6    9   69%
c i  133.4    4439    32636    778518  104444  24082  5570    7    10   29  71%  -2028   -4    6    9   74%
c i  133.4    4435    32636    778556  104455  24082  5571    7    10   29  71%  -2027   -4    6    9   70%
c i  133.5    4349    32636    778761  104583  24096  5579    7     9   29  71%  -2022   -4    5    9   57%
c i  133.5    4339    32636    778889  104681  24099  5579    7     9   29  71%  -2018   -4    5    9   54%
c i  133.5    4291    32636    778934  104709  24101  5583    7     9   29  71%  -2017   -4    4    9   52%
c i  133.5    4131    32636    778960  104723  24105  5584    7     9   29  71%  -2017   -4    4    9   50%
c i  133.5    4039    32636    778961  104723  24105  5584    7     9   29  71%  -2017   -4    4    9   49%
c 0  133.5    3978    32636    778961  104723  24105  5584    7     9   29  71%  -2017   -4    4    9   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: 32 basic ate = 30 trn 94% + 2 lrg 6% in 2 updates
c bcas: 4 count, 4 added (584 skipped), 270464 steps
c bkwd: tried 124039 clauses, 247253 lits, 1.99 lits/clause
c bkwd: checked 8026656 occs, 64.71 occs/clause, 32.46 occs/lit
c bkwd: subsumed 3 binary, 105 ternary, 20 large
c bkwd: strengthened 0 binary, 116 ternary (100% self), 658 large (0% self)
c blkd: 4 bces, 82 removed, 671223 resolutions, 1897005 steps
c blkd: 1474 blocking literals 2%, 0 pure
c bump: 779475 bumped seen, 36827906 lits 47.2 on average
c card: 4 count, 0 units, 0 am1, 11867908 steps
c card: 106 rescheduled, 90 eliminated, 163 resolved, 14471 subsumed
c card: 2727 at-most-one constraints found, average size 3.81
c card: 2727 at-most-one constraints used 100%, average size 3.81
c card: 21 at-most-two constraints found, average size 4.19
c card: 21 at-most-two constraints used 100%, average size 4.19
c cces: 8 cces, 17063 eliminated, 15500 ate 91%, 1563 abce 9%
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: 644099 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 93 gcs, 0 rescored clauses, 410 rescored vars
c dcps: 54 decompositions, 13826 equivalent 42%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1419992 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 9147 eliminated 28%, 46 pure 1%
c elms: 20 rounds, 2.0 rounds/bve
c elms: 8849 small 97%, 252 large 3%
c elms: 9593 tried small, 8849 succeeded 92%, 744 failed 8%
c elms: 2280 subsumed, 6318 strengthened, 79 blocked
c elms: 1590611 copies, 1916733 resolutions, 120413 ipos
c elms: 1769840 subchks, 526446 strchks
c gaus: 3 extractions, 174 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7309782 steps, 3654891 extr 50%, 1411 elim 0%
c glue: 8.9 orig avg, 8.9 real avg, 2.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 46699 = 35624 simple 76% + 10418 trn 22% + 657 lrg 1%, 2144 sub 5%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 779475 clauses, 21.5 length
c lrnd: 16776679 lits = 24408889 orig - 7632210 removed 31%
c lrnd: 132758 uips 17%, 559501 flips 72%
c mins: 774377 mins 99%, 78 bin 0%, 5020 size 1%
c mins: 19981635 poisoned searches, 3088424 hits, 15% hit rate
c mins: 40501294 used twice searches, 3068483 hits, 8% hit rate
c move: moved 13147, 3628 bin 28%, 9519 trn 72%
c otfs: 3083 driving 24%, 9879 restarting 76%
c otfs: str 12962, 12917 red 100%, 45 irr 0%
c otfs: str 12962, 0 bin 0%, 64 trn 0%, 12898 lrg 100%
c otfs: sub 27, 23 red 85%, 4 irr 15%
c otfs: sub 27, 0 bin 0%, 5 trn 19%, 22 lrg 81%
c phas: 7 computed, 14703 set, 0 pos (0%), 14703 neg (100%)
c prbs: 4 basic, 127530 probed, 140 failed, 2 lifted
c prbs: 5 simple, 61335 probed, 30 failed, 28728 eqs
c prbs: 4 treelook, 1074 probed, 5 failed, 0 lifted
c prom: 231001 locked 16% out of 1451772 tried
c prps: 110605607 props, 77 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 9 count, 1349 quat, 424 self1, 4 self2, 70 dup
c queu: 13 sorted, 1419992 next (653660 steps 0.46)
c queu: 37615744 enq (38261187 steps 1.02), 36827906 deq 98%
c redc: 25142 clauses 12%, 214782 tried 28%, 3 sat 0%
c redc: 31372 lits 1%, 2891540 tried 12%, 3 sat 0%
c redc: 553 times jump level reduced, 1.8 levels on average
c reds: 18 count, 43275.6 conflicts per reduce
c reds: 0 memlim 0%, 18 arith 100%
c reds: 526539 collected 86%, 86559 retired 14%
c rmbd: 8638 removed, 7815 red 90%
c rsts: 17246 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 779475 count (245716 tried 0.3), 45472 sub out of 777058 (5.9%)
c swps: 8 count, 11 rounds, 2023 queries (183.9/round)
c swps: 1940 sat calls, 13 unsat (1.9% success rate)
c swps: 29343 decisions 15.1, 3597 conflicts 1.9
c swps; 147.9 avg class size, 36.1 avg environment size
c swps: 0 failed, 184 impls, 96 equivs
c swp0: 671 type 0 queries, 32 unsat (4.8%), 658 sat (98.1%)
c swp1: 1352 type 1 queries, 224 unsat (16.6%), 1269 sat (93.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 4400031 calls to obtain time
c tops: 6139 fixed 19%, 22 its, 35407.32 confs/it
c trds: 9 transitive reductions, 5466 removed, 3 failed
c trds: 86779 nodes, 78361 edges, 1343871 steps
c trim: 294367 words, 1.1 MB
c trnr: 9 count, 165 bin, 23276 trn, 143098982 steps
c unhd: 6 count, 6 rounds, 4275243 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 2 failed, 2 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 7038 tauts, 113 bin 2%, 2666 trn 38%, 826 lrg 12%
c unhd: 7038 tauts, 3433 stamp 49%, 5339 red 76%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 68536 str, 0 bin 0%, 1366 trn 2%, 67170 lrg 98%, 66818 red 97%
c vars: 3978 remaining 12% and 29112 removed 88% out of 33090
c vars: 6139 fixed 19%, 9147 eliminated 28%, 13826 equivalent 42%
c vsts: 5457539882 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 49.7 search visits per propagation, 6936.6 per conflict
c wchs: 1611296844 pushed, 4006882 enlarged, 160 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         778407        526539         86559      14455077       5841793        436399
c 
c  0 0         84563  11     14185   3         0   0   8905562  62   2973738  51    189749  43     2.7
c  1 5         67229   9     44346   8      8928  10   1923689  13<   821938  14<    59905  14<    0.7
c  2 6        242765  31<   180787  34     27952  32   2624735  18   1360390  23    122603  28     2.1
c  3 9        290785  37    222176  42<    33690  39<   865358   6    586467  10     56740  13     2.2
c  4 14        88176  11     62144  12     14579  17    129500   1     95337   2      7136   2     0.8
c  5 21         4814   1      2862   1      1386   2      6140   0      3865   0       262   0     0.1
c  6 30           75   0        39   0        24   0        93   0        58   0         4   0     0.0
c 
c avg                  2.3           2.5           2.7           0.7           1.0           1.2
c std                  1.1           0.9           0.9           1.0           1.1           1.2
c 
c    3.377   3% cce
c    3.029   2% probe
c    2.851   2% bump
c    2.029   2% elim
c    1.842   1% sweep
c    1.073   1% ternres
c    0.793   1% decide
c 
c    1.814 < 1% rest (below)
c 
c    0.573   0% unhide
c    0.281   0% quatres
c    0.215   0% block
c    0.198   0% gauss
c    0.185   0% rescore
c    0.126   0% bca
c    0.122   0% card
c    0.114   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.818   1% preprocessing     6%
c   13.221  10% inprocessing     94%
c ==================================
c   14.039  11% simplifying
c  119.487  89% search
c ==================================
c  133.529 100% all
c 
c        778961 conflicts,        5833.7 confs/sec
c          1926 ternaries,         404.4 confs/ternary
c           222 binaries,         3508.8 confs/binary
c            22 iterations,      35407.3 confs/iteration
c 
c            18 reductions,          0.1 redus/sec,  43275.6 confs/reduction
c         17246 restarts,          129.2 rests/sec,     45.2 confs/restart
c       1419992 decisions,       10634.3 decis/sec,      1.8 decis/conflict
c     110605607 propagations,   828327.6 props/sec,     77.9 props/decision
c 
c 133.5 seconds, 36.3 MB
c launch: done
