c launch: /data/cnf/sc2014/app/total-10-13-u.cnf.bz2
c host: atom19
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/total-10-13-u.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/total-10-13-u.cnf.bz2
c no embedded options
c found 'p cnf 226208 1021181' header
c read 226208 variables, 1021181 clauses, 2332626 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=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 216656 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] INC (--score=1)
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  216656  1002109         0       0      0     0    0     0   39   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 10462 at-most-one constraints of average size 5.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 10462 out of 10462 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 116406 variables
c [simpleprobe-1] all 109802 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 69992 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 69992 variables, found 11070 hbrs, 947 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 2 units, 763 failed, 9374 tauts, 0 hbrs, 751 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 38583 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 12726 variables 33% in round 1 in 16209356 steps
c [elim-1-1] backward subsumption/strengthening limit 3790644
c [elim-1-1-1] backward checking 24666 touched variables 64%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 62 and strengthened 213 clauses in 3342031 steps
c [elim-1-1] rescheduled 597 variables 2% by backward subsumption
c [elim-1-2] eliminated 141 variables 0% in round 2 in 306153 steps
c [elim-1-2] backward subsumption/strengthening limit 142460
c [elim-1-2-1] backward checking 667 touched variables 2%
c [elim-1-2-1] incomplete backward checking 41 remain 6%
c [elim-1-2] subsumed 71 and strengthened 57 clauses in 142461 steps
c [elim-1] incomplete 223 not tried 1% in round 2
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 12970 = 34% variables out of 38583 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 188499 negative 99.2% of 189983 except 1484 0.8%
c [phase-count-1] 158642 positive 83.5% of 189983 except 31341 16.5%
c [phase-count-1] less non-negative clauses 1484 than limit 18900 (10.0%)
c [phase-count-1] non-pos/non-neg = 31341/1484 = 21.12 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 25613 negative 100%
c [sort-queue-1] sorted 25613 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 25613 (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 140872 variables 84.6% (25613 remain 12%)
c [simplification-1] removed 812126 irredundant clauses 81.0% (189983 remain 19%)
c [simplification-1] maximum reduction of 85% = max (85%, 81%)
c [simplification-1] large reduction 85% >= 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    2.1   25612   189983         1       0      0  6540    0     0   17   0%      0    0    0    0    0%
c i    2.1   25481   189983        10       5      1  6542    0     0   17  13%      0    0    0    0 25267%
c i    2.2   25480   189983       221     121     11  6578    1     2   17  62%      0    2   13    0 16418%
c i    2.3   24608   189983       356     241     14  6584    2     5   17  34%      0    5   14    0 12957%
c i    2.6   24607   189983       780     562     34  6598    5    14   17  35%      1   14   32    0 9614%
c i    2.6   24606   189983       783     562     34  6600    5    14   17  35%      1   14   32    0 9504%
c 
c [simplification-2] limit 1014 conflicts (hard 11000) hit after 1014 conflicts
c [decomp-3] removed 1120 variables
c [simpleprobe-2] all 24493 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 731 variables
c [simpleprobe-2] 13556 variables remain 57% (10206 retained 43%)
c [simpleprobe-2] removed 731 variables, found 3158 hbrs, 272 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 35642 literals 75%
c [treelook-1] scheduling used 300033 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 310384 steps
c [treelook-1] 35613 literals remain 75%
c [treelook-1] 23510 variables remain to probed next time 99%
c [decomp-5] removed 18 variables
c [treelook-1] removed 21 variables, found 3281 hbrs
c [basicprobe-1] limit 1366096 based on 170762 irredundant clauses
c [basicprobe-1-0] 2909 probes remain 12% after last round
c [basicprobe-1-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 55 variables, found 6057 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 507 failed, 4133 tauts, 0 hbrs, 3573 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 23220 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 1090 variables 5% in round 1 in 12470709 steps
c [elim-2-1] backward subsumption/strengthening limit 7529291
c [elim-2-1-1] backward checking 4374 touched variables 19%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 72 and strengthened 51 clauses in 861461 steps
c [elim-2-1] rescheduled 240 variables 1% by backward subsumption
c [elim-2-2] eliminated 66 variables 0% in round 2 in 126226 steps
c [elim-2-2] backward subsumption/strengthening limit 126200
c [elim-2-2-1] backward checking 289 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 54 and strengthened 10 clauses in 83509 steps
c [elim-2-2] rescheduled 91 variables 0% by backward subsumption
c [elim-2-3] eliminated 41 variables 0% in round 3 in 43109 steps
c [elim-2-3] backward subsumption/strengthening limit 43100
c [elim-2-3-1] backward checking 136 touched variables 1%
c [elim-2-3-1] incomplete backward checking 0 remain 0%
c [elim-2-3] subsumed 29 and strengthened 2 clauses in 43101 steps
c [elim-2] incomplete 57 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 1288 = 6% variables out of 23220 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 159867 negative 99.2% of 161097 except 1230 0.8%
c [phase-count-2] 130265 positive 80.9% of 161097 except 30832 19.1%
c [phase-count-2] less non-negative clauses 1230 than limit 16100 (10.0%)
c [phase-count-2] non-pos/non-neg = 30832/1230 = 25.07 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 335 negative 100%
c [sort-queue-2] sorted 14260 enqueued variables after 1014 conflicts
c [score-dist-2] active 7672 (35%), one 0 (0%), zero 14260 (65%)
c [score-dist-2] max exp 510, different 10 (2%)
c [score-dist-2] median active exp 506, avg 505.6
c [simplification-2] removed 2673 variables 10.9% (21932 remain 10%)
c [simplification-2] removed 28886 irredundant clauses 15.2% (161097 remain 16%)
c [simplification-2] maximum reduction of 15% = max (11%, 15%)
c [simplification-2] large reduction 15% >= 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 13014 (soft 3014 + delta 10000)
c [simplification-2] new conflict limit 3014 (hard 13014)
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    4.6   21931   161097      1691    1135     24 10281   30    61   16  49%      5   60  113    2 5329%
c i    4.6   21930   161097      1693    1135     24 10282   30    61   16  49%      5   61  112    2 5288%
c i    4.6   21926   161097      1696    1137     24 10282   30    61   16  49%      5   61  111    2 5227%
c i    5.3   21924   161097      2756    1913     25 10282   43    86   18  50%      8   84  130    3 3827%
c i    5.3   21923   161097      2757    1913     25 10282   43    86   18  50%      8   84  130    3 3812%
c i    5.3   21921   161097      2758    1913     25 10282   43    86   18  50%      8   84  129    3 3798%
c i    5.5   21920   161097      3010    2056     25 10283   48    92   19  52%      7   90  127    4 3290%
c 
c [simplification-3] limit 3042 conflicts (hard 13014) hit after 3042 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 5918 at-most-one constraints of average size 3.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5918 out of 5918 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 36 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 34180 literals 78%
c [treelook-2] scheduling used 300029 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 349662 steps
c [treelook-2] 34158 literals remain 78%
c [treelook-2] 21665 variables remain to probed next time 99%
c [treelook-2] removed 10 variables, found 1585 hbrs
c [unhide-3] limit 163703 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 257 failed, 8588 tauts, 0 hbrs, 13691 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 21690 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 480 variables 2% in round 1 in 11254238 steps
c [elim-3-1] backward subsumption/strengthening limit 8745762
c [elim-3-1-1] backward checking 2781 touched variables 13%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 39 and strengthened 22 clauses in 535418 steps
c [elim-3-1] rescheduled 151 variables 1% by backward subsumption
c [elim-3-2] eliminated 38 variables 0% in round 2 in 81310 steps
c [elim-3-2] backward subsumption/strengthening limit 81300
c [elim-3-2-1] backward checking 178 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 23 and strengthened 1 clauses in 54975 steps
c [elim-3-2] rescheduled 49 variables 0% by backward subsumption
c [elim-3-3] eliminated 20 variables 0% in round 3 in 26844 steps
c [elim-3-3] backward subsumption/strengthening limit 26800
c [elim-3-3-1] backward checking 84 touched variables 0%
c [elim-3-3-1] incomplete backward checking 0 remain 0%
c [elim-3-3] subsumed 13 and strengthened 7 clauses in 26801 steps
c [elim-3] incomplete 26 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 596 = 3% variables out of 21690 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 147823 negative 99.2% of 148974 except 1151 0.8%
c [phase-count-3] 122842 positive 82.5% of 148974 except 26132 17.5%
c [phase-count-3] less non-negative clauses 1151 than limit 14800 (10.0%)
c [phase-count-3] non-pos/non-neg = 26132/1151 = 22.70 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 119 negative 100%
c [sort-queue-3] sorted 12273 enqueued variables after 3042 conflicts
c [score-dist-3] active 8821 (42%), one 0 (0%), zero 12273 (58%)
c [score-dist-3] max exp 512, different 12 (2%)
c [score-dist-3] median active exp 507, avg 506.8
c [simplification-3] removed 824 variables 3.8% (21094 remain 10%)
c [simplification-3] removed 12123 irredundant clauses 7.5% (148974 remain 15%)
c [simplification-3] maximum reduction of 8% = max (4%, 8%)
c [simplification-3] large reduction 8% >= 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 15042 (soft 5042 + delta 10000)
c [simplification-3] new conflict limit 5042 (hard 15042)
c 
c [simplification-4] limit 5042 conflicts (hard 15042) hit after 5043 conflicts
c [decomp-8] removed 17 variables
c [basicprobe-2] limit 6239397 penalty 0 = 0 + 0
c [basicprobe-2-0] 2952 probes remain 14% after last round
c [basicprobe-2-0] 56 units = 56 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 135 variables, found 25425 hbrs
c [unhide-4] limit 249575 with penalty 0 = 0 + 0
c [unhide-4-4] 5 units, 156 failed, 3644 tauts, 0 hbrs, 3767 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 20741 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 499151820 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 264 variables 1% in round 1 in 10658521 steps
c [elim-4-1] backward subsumption/strengthening limit 10658500
c [elim-4-1-1] backward checking 1280 touched variables 6%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 21 and strengthened 3 clauses in 246521 steps
c [elim-4-1] rescheduled 48 variables 0% by backward subsumption
c [elim-4-2] eliminated 5 variables 0% in round 2 in 28487 steps
c [elim-4-2] backward subsumption/strengthening limit 28400
c [elim-4-2-1] backward checking 46 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 10 and strengthened 1 clauses in 26557 steps
c [elim-4-2] rescheduled 14 variables 0% by backward subsumption
c [elim-4-3] eliminated 7 variables 0% in round 3 in 6445 steps
c [elim-4-3] backward subsumption/strengthening limit 6400
c [elim-4-3-1] backward checking 43 touched variables 0%
c [elim-4-3-1] incomplete backward checking 12 remain 28%
c [elim-4-3] subsumed 7 and strengthened 0 clauses in 6421 steps
c [elim-4] incomplete 12 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 304 = 1% variables out of 20741 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 143274 negative 99.2% of 144357 except 1083 0.8%
c [phase-count-4] 118279 positive 81.9% of 144357 except 26078 18.1%
c [phase-count-4] less non-negative clauses 1083 than limit 14400 (10.0%)
c [phase-count-4] non-pos/non-neg = 26078/1083 = 24.08 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 91 negative 100%
c [sort-queue-4] sorted 11353 enqueued variables after 5043 conflicts
c [score-dist-4] active 9084 (44%), one 0 (0%), zero 11353 (56%)
c [score-dist-4] max exp 513, different 13 (3%)
c [score-dist-4] median active exp 507, avg 507.2
c [simplification-4] removed 657 variables 3.1% (20437 remain 9%)
c [simplification-4] removed 4617 irredundant clauses 3.1% (144357 remain 14%)
c [simplification-4] maximum reduction of 3% = max (3%, 3%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 5000
c [simplification-4] penalized conflict interval 5000 = 1 * 5000
c [simplification-4] hard conflict limit 20043 (soft 10043 + delta 10000)
c [simplification-4] new conflict limit 10043 (hard 20043)
c 
c [simplification-5] limit 10043 conflicts (hard 20043) hit after 10044 conflicts
c [quatres-1] found 9236 quaternary clauses 73% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 11 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 20437 free variables schedulable
c [ternres-1] 264 ternary resolvents (1 bin, 263 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 140 xors of average arity 2.8
c [gauss-1] connected 388 occurrences of 229 variables (average 1.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 14 variables
c [simpleprobe-3] 11552 schedulable variables 57%
c [simpleprobe-3] limit 9142345 penalty 0 = 0 + 0
c [decomp-10] removed 321 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 321 variables, found 9450 hbrs, 113 units
c [unhide-5] limit 457117 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 71 failed, 4102 tauts, 0 hbrs, 3255 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 460 transitive binary clauses
c [transred-1] found 15 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 20007 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 800 blocked clauses
c [block-1] 800 < 1/100 * 139207 = 1392 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 61 (2%) of length 7
c [cce-1-1] eliminated 82 clauses out of 929 (9%) of length 6
c [cce-1-1] eliminated 257 clauses out of 1829 (14%) of length 5
c [cce-1-1] eliminated 637 clauses out of 8301 (8%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 977 large clauses in 30000009 steps
c [cce-1-1] allowing another 15000004 steps for small clauses
c [cce-1-1] scheduling 99402 clauses = 75876 binary + 23526 ternary
c [cce-1-1] tried to eliminate 775 small clauses 1%
c [cce-1-1] eliminated 248 binary clauses 0%
c [cce-1-1] eliminated 31 ternary clauses 0%
c [cce-1-1] eliminated 279 small clauses 0%
c [cce-1-1] eliminated 279 small clauses in 30000005 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1256 covered clauses in round 1
c [cce-1] eliminated 1256 covered clauses in TOTAL during 1 rounds
c [cce-1] 1256 < 1/100 * 137546 = 1375 considered unsuccessful
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 20006 variables 100%
c [elim-5] limit of 45711729 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 628 variables 3% in round 1 in 9740670 steps
c [elim-5-1] backward subsumption/strengthening limit 9740600
c [elim-5-1-1] backward checking 2653 touched variables 13%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 33 and strengthened 15 clauses in 492514 steps
c [elim-5-1] rescheduled 112 variables 1% by backward subsumption
c [elim-5-2] eliminated 6 variables 0% in round 2 in 63982 steps
c [elim-5-2] backward subsumption/strengthening limit 63900
c [elim-5-2-1] backward checking 39 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 3 and strengthened 3 clauses in 25494 steps
c [elim-5-2] rescheduled 9 variables 0% by backward subsumption
c [elim-5-3] eliminated 3 variables 0% in round 3 in 4388 steps
c [elim-5-3] backward subsumption/strengthening limit 4300
c [elim-5-3-1] backward checking 7 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 3 and strengthened 1 clauses in 4301 steps
c [elim-5] incomplete 9 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 642 = 3% variables out of 20006 scheduled
c [bca-1] limit of 10000000 steps and 269452 added (scaled 2)
c [bca-1] 35064 out of 38730 literals actually usable 91%
c [bca-1] added 9 blocked clauses in 76172 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3204 pos 16.5% + 16160 neg 83.5% = 19364 sched 100.0% ret 0
c [sweep-1-1] 1080099 steps 22 queries 3490.00 avg class size
c [sweep-1-1] 205 decisions 17 SAT calls 101.24 avg env size
c [sweep-1-1] 19056 variables remain 98% (297 retained 2%)
c [decomp-11] removed 24 variables
c [sweep-1-1] removed 24 vars (0 failed, 4 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 24 vars in TOTAL (1 rounds, 21 queries)
c [phase-count-5] 133590 negative 99.4% of 134357 except 767 0.6%
c [phase-count-5] 110236 positive 82.0% of 134357 except 24121 18.0%
c [phase-count-5] less non-negative clauses 767 than limit 13400 (10.0%)
c [phase-count-5] non-pos/non-neg = 24121/767 = 31.45 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 45 negative 100%
c [sort-queue-5] sorted 9969 enqueued variables after 10044 conflicts
c [score-dist-5] active 9371 (48%), one 0 (0%), zero 9969 (52%)
c [score-dist-5] max exp 515, different 15 (3%)
c [score-dist-5] median active exp 507, avg 507.5
c [simplification-5] removed 1097 variables 5.4% (19340 remain 9%)
c [simplification-5] removed 10000 irredundant clauses 6.9% (134357 remain 13%)
c [simplification-5] maximum reduction of 7% = max (5%, 7%)
c [simplification-5] large reduction 7% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 22044 (soft 12044 + delta 10000)
c [simplification-5] new conflict limit 12044 (hard 22044)
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   15.4   19339   134357     11914    3710    363 34757  122   152   20  81%    116  131  109   21  510%
c 
c [simplification-6] limit 12044 conflicts (hard 22044) hit after 12044 conflicts
c [quatres-2] found 7422 quaternary clauses 72% in total
c [quatres-2-2] added 2 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 19339 free variables schedulable
c [ternres-2] 92 ternary resolvents (0 bin, 92 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2440 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2440 out of 2440 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 32093 literals 83%
c [treelook-3] scheduling used 300040 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 305688 steps
c [treelook-3] 32087 literals remain 83%
c [treelook-3] 19224 variables remain to probed next time 99%
c [treelook-3] removed 1 variables, found 2688 hbrs
c [unhide-6] limit 537091 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 98 failed, 4287 tauts, 0 hbrs, 5289 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 394 transitive binary clauses
c [transred-2] found 14 units
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 19258 variables 100%
c [elim-6] limit of 53709196 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 92 variables 0% in round 1 in 9511959 steps
c [elim-6-1] backward subsumption/strengthening limit 9511900
c [elim-6-1-1] backward checking 528 touched variables 3%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 6 and strengthened 9 clauses in 105466 steps
c [elim-6-1] rescheduled 32 variables 0% by backward subsumption
c [elim-6-2] eliminated 10 variables 0% in round 2 in 13332 steps
c [elim-6-2] backward subsumption/strengthening limit 13300
c [elim-6-2-1] backward checking 35 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 8 and strengthened 4 clauses in 13301 steps
c [elim-6-2] rescheduled 13 variables 0% by backward subsumption
c [elim-6-3] eliminated 2 variables 0% in round 3 in 7977 steps
c [elim-6-3] backward subsumption/strengthening limit 7900
c [elim-6-3-1] backward checking 7 touched variables 0%
c [elim-6-3-1] incomplete backward checking 0 remain 0%
c [elim-6-3] subsumed 0 and strengthened 0 clauses in 7901 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 113 = 1% variables out of 19258 scheduled
c [elim-6] 113 < 1/100 * 19258 = 192 considered unsuccessful
c [bca-2] limit of 10000000 steps and 266220 added (scaled 2)
c [bca-2] 34451 out of 38292 literals actually usable 90%
c [bca-2] added 3 blocked clauses in 75513 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3152 pos 16.7% + 15709 neg 83.3% = 18861 sched 98.5% ret 284
c [sweep-2-1] 1198641 steps 16 queries 3808.62 avg class size
c [sweep-2-1] 169 decisions 13 SAT calls 188.38 avg env size
c [sweep-2-1] 18747 variables remain 98% (393 retained 2%)
c [decomp-14] removed 8 variables
c [sweep-2-1] removed 8 vars (0 failed, 2 eqs, 6 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 8 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-6] 132033 negative 99.4% of 132792 except 759 0.6%
c [phase-count-6] 109015 positive 82.1% of 132792 except 23777 17.9%
c [phase-count-6] less non-negative clauses 759 than limit 13200 (10.0%)
c [phase-count-6] non-pos/non-neg = 23777/759 = 31.33 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 44 negative 100%
c [sort-queue-6] sorted 9572 enqueued variables after 12044 conflicts
c [score-dist-6] active 9565 (50%), one 0 (0%), zero 9572 (50%)
c [score-dist-6] max exp 515, different 15 (3%)
c [score-dist-6] median active exp 507, avg 507.5
c [simplification-6] removed 202 variables 1.0% (19137 remain 9%)
c [simplification-6] removed 1565 irredundant clauses 1.2% (132792 remain 13%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 15000
c [simplification-6] penalized conflict interval 15000 = 1 * 15000
c [simplification-6] hard conflict limit 37044 (soft 27044 + delta 10000)
c [simplification-6] new conflict limit 27044 (hard 37044)
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   18.1   19136   132792     13936    5230    408 35025  108   147   21  74%     26  123   68   23  291%
c i   23.7   19135   132792     22002   12851    408 35025   62    82   27  76%     96   47   43   28  157%
c i   25.8   19131   132792     24931   15551    412 35029   51    70   33  73%     21   33   35   28  124%
c 
c [simplification-7] limit 27044 conflicts (hard 37044) hit after 27046 conflicts
c [quatres-3] found 7193 quaternary clauses 71% in total
c [ternres-3] limit 5756858 with penalty 0 = 0 + 0
c [ternres-3] all 19131 free variables schedulable
c [ternres-3] 40 ternary resolvents (0 bin, 40 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 36 xors of average arity 2.9
c [gauss-2] connected 106 occurrences of 91 variables (average 1.2)
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 [decomp-15] removed 2 variables
c [basicprobe-3] limit 28784292 penalty 0 = 0 + 0
c [basicprobe-3-0] 1405 probes remain 9% after last round
c [basicprobe-3-0] 490 units = 408 failed (83%) + 82 lifted (17%)
c [basicprobe-3-0] removed 3760 variables, found 53915 hbrs
c [bate-1] eliminated 199 asymmetric tautologies during probing
c [unhide-7] limit 1151371 with penalty 0 = 0 + 0
c [unhide-7-8] 11 units, 466 failed, 10346 tauts, 0 hbrs, 47739 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 448 transitive binary clauses
c [transred-3] found 17 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 15024 variables 100%
c [block-2] limit of 28784292 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 267 blocked clauses
c [block-2] 267 < 1/100 * 88706 = 887 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 8
c [cce-2-1] eliminated 1 clauses out of 32 (3%) of length 7
c [cce-2-1] eliminated 4 clauses out of 274 (1%) of length 6
c [cce-2-1] eliminated 29 clauses out of 833 (3%) of length 5
c [cce-2-1] eliminated 478 clauses out of 4095 (12%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 513 large clauses in 15000003 steps
c [cce-2-1] allowing another 7500001 steps for small clauses
c [cce-2-1] scheduling 67722 clauses = 52645 binary + 15077 ternary
c [cce-2-1] tried to eliminate 693 small clauses 1%
c [cce-2-1] eliminated 208 binary clauses 0%
c [cce-2-1] eliminated 21 ternary clauses 0%
c [cce-2-1] eliminated 229 small clauses 0%
c [cce-2-1] eliminated 229 small clauses in 15000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 742 covered clauses in round 1
c [cce-2] eliminated 742 covered clauses in TOTAL during 1 rounds
c [cce-2] 742 < 1/100 * 87370 = 873 considered unsuccessful
c [bca-3] limit of 10000000 steps and 173762 added (scaled 2)
c [bca-3] 26808 out of 30040 literals actually usable 89%
c [bca-3] added 14 blocked clauses in 68725 steps
c [sweep-3] limit 1727057 penalty 0 = 0 + 0
c [sweep-3-1] 2922 pos 19.7% + 11932 neg 80.3% = 14854 sched 98.9% ret 165
c [sweep-3-1] 1903527 steps 29 queries 1404.79 avg class size
c [sweep-3-1] 237 decisions 23 SAT calls 81.26 avg env size
c [sweep-3-1] 14519 variables remain 97% (481 retained 3%)
c [decomp-16] removed 685 variables
c [sweep-3-1] removed 685 vars (0 failed, 6 eqs, 7 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 685 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-7] 84539 negative 99.2% of 85211 except 672 0.8%
c [phase-count-7] 69905 positive 82.0% of 85211 except 15306 18.0%
c [phase-count-7] less non-negative clauses 672 than limit 8500 (10.0%)
c [phase-count-7] non-pos/non-neg = 15306/672 = 22.78 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 32 negative 100%
c [sort-queue-7] sorted 6122 enqueued variables after 27046 conflicts
c [score-dist-7] active 8212 (57%), one 0 (0%), zero 6122 (43%)
c [score-dist-7] max exp 516, different 16 (3%)
c [score-dist-7] median active exp 508, avg 508.3
c [simplification-7] removed 4797 variables 25.1% (14334 remain 7%)
c [simplification-7] removed 47581 irredundant clauses 35.8% (85211 remain 9%)
c [simplification-7] maximum reduction of 36% = max (25%, 36%)
c [simplification-7] large reduction 36% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 39046 (soft 29046 + delta 10000)
c [simplification-7] new conflict limit 29046 (hard 39046)
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   30.6   14333    85211     27141   15350    436 35661   45    68   24  66%      9   31   41   28  143%
c i   31.2   14331    85211     28356   16495    436 35661   43    64   26  68%     -1   26   34   29  120%
c 
c [simplification-8] limit 29046 conflicts (hard 39046) hit after 30000 conflicts
c [ternres-4] limit 6070092 with penalty 0 = 0 + 0
c [ternres-4] all 14331 free variables schedulable
c [ternres-4] 117 ternary resolvents (0 bin, 117 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 6 variables
c [simpleprobe-4] all 14328 free variables schedulable
c [simpleprobe-4] limit 24280371 penalty 0 = 0 + 0
c [decomp-18] removed 376 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 376 variables, found 4883 hbrs, 78 units
c [unhide-8] limit 1214018 with penalty 0 = 0 + 0
c [unhide-8-10] 3 units, 87 failed, 5946 tauts, 0 hbrs, 21310 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 455 transitive binary clauses
c [transred-4] found 12 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 13832 variables 100%
c [elim-7] limit of 60700927 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1853 variables 13% in round 1 in 5570234 steps
c [elim-7-1] backward subsumption/strengthening limit 5570200
c [elim-7-1-1] backward checking 5516 touched variables 40%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 10 and strengthened 28 clauses in 802676 steps
c [elim-7-1] rescheduled 117 variables 1% by backward subsumption
c [elim-7-2] eliminated 8 variables 0% in round 2 in 213611 steps
c [elim-7-2] backward subsumption/strengthening limit 213600
c [elim-7-2-1] backward checking 79 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 1 and strengthened 0 clauses in 36146 steps
c [elim-7-2] rescheduled 2 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 5601 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1866 = 13% variables out of 13832 scheduled
c [bca-4] limit of 10000000 steps and 156919 added (scaled 2)
c [bca-4] 21231 out of 23934 literals actually usable 89%
c [bca-4] added 15 blocked clauses in 47916 steps
c [sweep-4] limit 1821027 penalty 0 = 0 + 0
c [sweep-4-1] 2254 pos 19.4% + 9354 neg 80.6% = 11608 sched 97.0% ret 358
c [sweep-4-1] 1840054 steps 39 queries 578.44 avg class size
c [sweep-4-1] 508 decisions 33 SAT calls 102.79 avg env size
c [sweep-4-1] 9536 variables remain 81% (2217 retained 19%)
c [decomp-19] removed 264 variables
c [sweep-4-1] removed 264 vars (0 failed, 6 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 264 vars in TOTAL (1 rounds, 38 queries)
c [phase-count-8] 75423 negative 99.4% of 75881 except 458 0.6%
c [phase-count-8] 60621 positive 79.9% of 75881 except 15260 20.1%
c [phase-count-8] less non-negative clauses 458 than limit 7500 (10.0%)
c [phase-count-8] non-pos/non-neg = 15260/458 = 33.32 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 23 negative 100%
c [sort-queue-8] sorted 4862 enqueued variables after 30000 conflicts
c [score-dist-8] active 6840 (58%), one 0 (0%), zero 4862 (42%)
c [score-dist-8] max exp 516, different 16 (3%)
c [score-dist-8] median active exp 509, avg 508.7
c [simplification-8] removed 2629 variables 18.3% (11702 remain 5%)
c [simplification-8] removed 9330 irredundant clauses 10.9% (75881 remain 8%)
c [simplification-8] maximum reduction of 18% = max (18%, 11%)
c [simplification-8] large reduction 18% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 42000 (soft 32000 + delta 10000)
c [simplification-8] new conflict limit 32000 (hard 42000)
c 
c [simplification-9] limit 32000 conflicts (hard 42000) hit after 32000 conflicts
c [quatres-4] found 3956 quaternary clauses 69% in total
c [quatres-4-2] added 2 quaternary resolvents
c [ternres-5] limit 6233108 with penalty 0 = 0 + 0
c [ternres-5] all 11702 free variables schedulable
c [ternres-5] 199 ternary resolvents (0 bin, 199 trn)
c [ternres-5] fully completed ternary resolution
c [treelook-4] limit 623310 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 23396 literals 100%
c [treelook-4] scheduling used 306875 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 623310 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 628641 steps
c [treelook-4] 23348 literals remain 100%
c [treelook-4] 11654 variables remain to probed next time 100%
c [decomp-21] removed 1 variables
c [treelook-4] removed 15 variables, found 5213 hbrs
c [unhide-9] limit 1246621 with penalty 0 = 0 + 0
c [unhide-9-13] 33 units, 261 failed, 4100 tauts, 0 hbrs, 36725 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 276 transitive binary clauses
c [transred-5] found 15 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 11529 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2493243500 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 338 variables 3% in round 1 in 4868289 steps
c [elim-8-1] backward subsumption/strengthening limit 4868200
c [elim-8-1-1] backward checking 1702 touched variables 15%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 12 and strengthened 9 clauses in 301303 steps
c [elim-8-1] rescheduled 58 variables 1% by backward subsumption
c [elim-8-2] eliminated 6 variables 0% in round 2 in 56618 steps
c [elim-8-2] backward subsumption/strengthening limit 56600
c [elim-8-2-1] backward checking 26 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 2 and strengthened 0 clauses in 15283 steps
c [elim-8-2] rescheduled 5 variables 0% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 1993 steps
c [elim-8-3] backward subsumption/strengthening limit 1900
c [elim-8-3-1] backward checking 7 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 1901 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 349 = 3% variables out of 11529 scheduled
c [bca-5] limit of 10000000 steps and 143368 added (scaled 2)
c [bca-5] 19593 out of 22362 literals actually usable 88%
c [bca-5] added 12 blocked clauses in 45212 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 18699320 penalty 0 = 0 + 0
c [sweep-5-1] 1924 pos 21.1% + 7208 neg 78.9% = 9132 sched 81.7% ret 2048
c [sweep-5-1] 18736330 steps 535 queries 57.00 avg class size
c [sweep-5-1] 3689 decisions 479 SAT calls 50.48 avg env size
c [sweep-5-1] 3188 variables remain 30% (7594 retained 70%)
c [decomp-22] removed 523 variables
c [sweep-5-1] removed 523 vars (0 failed, 81 eqs, 93 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 523 vars in TOTAL (1 rounds, 534 queries)
c [phase-count-9] 66836 negative 99.4% of 67264 except 428 0.6%
c [phase-count-9] 54258 positive 80.7% of 67264 except 13006 19.3%
c [phase-count-9] less non-negative clauses 428 than limit 6700 (10.0%)
c [phase-count-9] non-pos/non-neg = 13006/428 = 30.39 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 16 negative 100%
c [sort-queue-9] sorted 4129 enqueued variables after 32000 conflicts
c [score-dist-9] active 6528 (61%), one 0 (0%), zero 4129 (39%)
c [score-dist-9] max exp 516, different 16 (3%)
c [score-dist-9] median active exp 509, avg 508.9
c [simplification-9] removed 1045 variables 8.9% (10657 remain 5%)
c [simplification-9] removed 8617 irredundant clauses 11.4% (67264 remain 7%)
c [simplification-9] maximum reduction of 11% = max (9%, 11%)
c [simplification-9] large reduction 11% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 44000 (soft 34000 + delta 10000)
c [simplification-9] new conflict limit 34000 (hard 44000)
c 
c [simplification-10] limit 34000 conflicts (hard 44000) hit after 34000 conflicts
c [quatres-5] found 3537 quaternary clauses 68% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [ternres-6] limit 6421916 with penalty 0 = 0 + 0
c [ternres-6] all 10657 free variables schedulable
c [ternres-6] 74 ternary resolvents (0 bin, 74 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 401369 penalty 3 = 3 + 0
c [card-4] found 1691 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 401369 for elimination
c [card-4] 1691 out of 1691 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 33 xors of average arity 2.8
c [gauss-3] connected 94 occurrences of 69 variables (average 1.4)
c [gauss-3] limit 500000 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 32109582 penalty 0 = 0 + 0
c [basicprobe-4-0] 1507 sched 16%, 717 failed, 100 lifted, 53666 hbrs
c [decomp-24] removed 1500 variables
c [basicprobe-4-1] 1338 probes remain 15% after last round
c [basicprobe-4-1] 827 units = 727 failed (88%) + 100 lifted (12%)
c [basicprobe-4-1] removed 1513 variables, found 55302 hbrs
c [bate-2] eliminated 245 asymmetric tautologies during probing
c [unhide-10] limit 1284383 with penalty 0 = 0 + 0
c [unhide-10-16] 19 units, 160 failed, 11631 tauts, 0 hbrs, 15897 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 482 transitive binary clauses
c [transred-6] found 10 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 8938 variables 100%
c [block-3] limit of 16054791 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 173 blocked clauses
c [block-3] 173 < 1/100 * 49822 = 498 considered unsuccessful
c [cce-3] limit of 8027395 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 9
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 8
c [cce-3-1] eliminated 1 clauses out of 18 (6%) of length 7
c [cce-3-1] eliminated 4 clauses out of 134 (3%) of length 6
c [cce-3-1] eliminated 23 clauses out of 475 (5%) of length 5
c [cce-3-1] eliminated 277 clauses out of 2405 (12%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 308 large clauses in 7225569 steps
c [cce-3-1] allowing another 3612784 steps for small clauses
c [cce-3-1] scheduling 38482 clauses = 31250 binary + 7232 ternary
c [cce-3-1] tried to eliminate 692 small clauses 2%
c [cce-3-1] eliminated 197 binary clauses 1%
c [cce-3-1] eliminated 10 ternary clauses 0%
c [cce-3-1] eliminated 207 small clauses 1%
c [cce-3-1] eliminated 207 small clauses in 8027399 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 515 covered clauses in round 1
c [cce-3] eliminated 515 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8929 variables 100%
c [elim-9] limit of 128438330 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1389 variables 16% in round 1 in 3160626 steps
c [elim-9-1] backward subsumption/strengthening limit 3160600
c [elim-9-1-1] backward checking 4178 touched variables 47%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 6 and strengthened 21 clauses in 551474 steps
c [elim-9-1] rescheduled 90 variables 1% by backward subsumption
c [elim-9-2] eliminated 7 variables 0% in round 2 in 42058 steps
c [elim-9-2] backward subsumption/strengthening limit 42000
c [elim-9-2-1] backward checking 50 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 1 clauses in 21697 steps
c [elim-9-2] rescheduled 5 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 6663 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1406 = 16% variables out of 8929 scheduled
c [bca-6] limit of 10000000 steps and 94522 added (scaled 2)
c [bca-6] 13079 out of 15048 literals actually usable 87%
c [bca-6] added 27 blocked clauses in 32185 steps
c [sweep-6] limit 1926574 penalty 0 = 0 + 0
c [sweep-6-1] 884 pos 39.2% + 1372 neg 60.8% = 2256 sched 30.0% ret 5267
c [sweep-6-1] 1931894 steps 89 queries 76.52 avg class size
c [sweep-6-1] 481 decisions 85 SAT calls 30.09 avg env size
c [sweep-6-1] 1969 variables remain 26% (5541 retained 74%)
c [decomp-25] removed 29 variables
c [sweep-6-1] removed 29 vars (0 failed, 9 eqs, 8 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 29 vars in TOTAL (1 rounds, 88 queries)
c [phase-count-10] 46473 negative 99.4% of 46764 except 291 0.6%
c [phase-count-10] 36846 positive 78.8% of 46764 except 9918 21.2%
c [phase-count-10] less non-negative clauses 291 than limit 4600 (10.0%)
c [phase-count-10] non-pos/non-neg = 9918/291 = 34.08 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 3 negative 100%
c [sort-queue-10] sorted 2772 enqueued variables after 34000 conflicts
c [score-dist-10] active 4722 (63%), one 0 (0%), zero 2772 (37%)
c [score-dist-10] max exp 516, different 16 (3%)
c [score-dist-10] median active exp 509, avg 509.0
c [simplification-10] removed 3163 variables 29.7% (7494 remain 3%)
c [simplification-10] removed 20500 irredundant clauses 30.5% (46764 remain 5%)
c [simplification-10] maximum reduction of 30% = max (30%, 30%)
c [simplification-10] large reduction 30% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 46000 (soft 36000 + delta 10000)
c [simplification-10] new conflict limit 36000 (hard 46000)
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   39.6    7493    46764     34177    5002    291 35469   35    71   14  48%     57   31   31   29  108%
c 
c [simplification-11] limit 36000 conflicts (hard 46000) hit after 36001 conflicts
c [quatres-6] found 2468 quaternary clauses 66% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [ternres-7] limit 6514524 with penalty 0 = 0 + 0
c [ternres-7] all 7492 free variables schedulable
c [ternres-7] 171 ternary resolvents (0 bin, 171 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 2 variables
c [simpleprobe-5] all 7492 free variables schedulable
c [simpleprobe-5] limit 26058096 penalty 0 = 0 + 0
c [decomp-27] removed 89 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 89 variables, found 4514 hbrs, 46 units
c [unhide-11] limit 1302904 with penalty 0 = 0 + 0
c [unhide-11-20] 3 units, 128 failed, 5679 tauts, 0 hbrs, 11412 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 503 transitive binary clauses
c [transred-7] found 8 units
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 7365 variables 100%
c [elim-10] limit of 130290483 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 196 variables 3% in round 1 in 2860042 steps
c [elim-10-1] backward subsumption/strengthening limit 2860000
c [elim-10-1-1] backward checking 1122 touched variables 15%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 6 clauses in 180247 steps
c [elim-10-1] rescheduled 22 variables 0% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 9496 steps
c [elim-10-2] backward subsumption/strengthening limit 9400
c [elim-10-2-1] backward checking 22 touched variables 0%
c [elim-10-2-1] incomplete backward checking 20 remain 91%
c [elim-10-2] subsumed 11 and strengthened 1 clauses in 9408 steps
c [elim-10-2] rescheduled 14 variables 0% by backward subsumption
c [elim-10-3] eliminated 3 variables 0% in round 3 in 7305 steps
c [elim-10-3] backward subsumption/strengthening limit 7300
c [elim-10-3-1] backward checking 29 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 7301 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 203 = 3% variables out of 7365 scheduled
c [bca-7] limit of 10000000 steps and 88668 added (scaled 2)
c [bca-7] 12137 out of 14326 literals actually usable 85%
c [bca-7] added 14 blocked clauses in 31107 steps
c [sweep-7] limit 1954357 penalty 0 = 0 + 0
c [sweep-7-1] 780 pos 41.6% + 1097 neg 58.4% = 1877 sched 26.2% ret 5285
c [sweep-7-1] 1970766 steps 122 queries 71.05 avg class size
c [sweep-7-1] 539 decisions 114 SAT calls 21.81 avg env size
c [sweep-7-1] 1555 variables remain 22% (5582 retained 78%)
c [decomp-28] removed 78 variables
c [sweep-7-1] removed 78 vars (0 failed, 14 eqs, 16 impls)
c [sweep-7] removed 78 vars in TOTAL (1 rounds, 121 queries)
c [phase-count-11] 43367 negative 99.3% of 43657 except 290 0.7%
c [phase-count-11] 34472 positive 79.0% of 43657 except 9185 21.0%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 2506 enqueued variables after 36001 conflicts
c [score-dist-11] active 4578 (65%), one 0 (0%), zero 2506 (35%)
c [score-dist-11] max exp 516, different 16 (3%)
c [score-dist-11] median active exp 509, avg 509.2
c [simplification-11] removed 408 variables 5.4% (7084 remain 3%)
c [simplification-11] removed 3107 irredundant clauses 6.6% (43657 remain 4%)
c [simplification-11] maximum reduction of 7% = max (5%, 7%)
c [simplification-11] large reduction 7% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 48001 (soft 38001 + delta 10000)
c [simplification-11] new conflict limit 38001 (hard 48001)
c 
c [simplification-12] limit 38001 conflicts (hard 48001) hit after 38002 conflicts
c [ternres-8] limit 6593297 with penalty 0 = 0 + 0
c [ternres-8] all 7084 free variables schedulable
c [ternres-8] 43 ternary resolvents (0 bin, 43 trn)
c [ternres-8] fully completed ternary resolution
c [treelook-5] limit 659329 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 14166 literals 100%
c [treelook-5] scheduling used 215290 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 659329 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 664636 steps
c [treelook-5] 14091 literals remain 100%
c [treelook-5] 7052 variables remain to probed next time 100%
c [treelook-5] removed 16 variables, found 2515 hbrs
c [unhide-12] limit 1318659 with penalty 0 = 0 + 0
c [unhide-12-24] 15 units, 202 failed, 2949 tauts, 0 hbrs, 15371 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 333 transitive binary clauses
c [transred-8] found 7 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 164832430 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-4-1] eliminated 2 clauses out of 14 (14%) of length 8
c [cce-4-1] eliminated 1 clauses out of 54 (2%) of length 7
c [cce-4-1] eliminated 4 clauses out of 183 (2%) of length 6
c [cce-4-1] eliminated 32 clauses out of 645 (5%) of length 5
c [cce-4-1] eliminated 240 clauses out of 2131 (11%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 280 large clauses in 9508965 steps
c [cce-4-1] allowing another 4754482 steps for small clauses
c [cce-4-1] scheduling 31898 clauses = 25720 binary + 6178 ternary
c [cce-4-1] tried to eliminate 26674 small clauses 84%
c [cce-4-1] eliminated 5228 binary clauses 20%
c [cce-4-1] eliminated 874 ternary clauses 14%
c [cce-4-1] eliminated 6102 small clauses 19%
c [cce-4-1] eliminated 6388 small clauses in 164832430 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 6668 covered clauses in round 1
c [cce-4] eliminated 6668 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 6926 variables 100%
c [elim-11] limit of 131865944 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 816 variables 12% in round 1 in 2134092 steps
c [elim-11-1] backward subsumption/strengthening limit 2134000
c [elim-11-1-1] backward checking 2845 touched variables 41%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 13 and strengthened 31 clauses in 307866 steps
c [elim-11-1] rescheduled 198 variables 3% by backward subsumption
c [elim-11-2] eliminated 23 variables 0% in round 2 in 65317 steps
c [elim-11-2] backward subsumption/strengthening limit 65300
c [elim-11-2-1] backward checking 134 touched variables 2%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 7 and strengthened 4 clauses in 29539 steps
c [elim-11-2] rescheduled 42 variables 1% by backward subsumption
c [elim-11-3] eliminated 5 variables 0% in round 3 in 12982 steps
c [elim-11-3] backward subsumption/strengthening limit 12900
c [elim-11-3-1] backward checking 24 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 1 and strengthened 1 clauses in 12901 steps
c [elim-11] incomplete 11 not tried 0% in round 3
c [gc-94] reconnected 33174 binary clauses (produced 0 empty 1 units)
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 862 = 12% variables out of 6926 scheduled
c [bca-8] limit of 10000000 steps and 67837 added (scaled 2)
c [bca-8] 10415 out of 12130 literals actually usable 86%
c [bca-8] added 17 blocked clauses in 24542 steps
c [sweep-8] limit 1977989 penalty 0 = 0 + 0
c [sweep-8-1] 483 pos 40.0% + 726 neg 60.0% = 1209 sched 19.9% ret 4855
c [sweep-8-1] 2004278 steps 178 queries 40.51 avg class size
c [sweep-8-1] 624 decisions 171 SAT calls 18.85 avg env size
c [sweep-8-1] 820 variables remain 14% (5232 retained 86%)
c [decomp-31] removed 28 variables
c [sweep-8-1] removed 28 vars (0 failed, 7 eqs, 11 impls)
c [sweep-8] removed 28 vars in TOTAL (1 rounds, 177 queries)
c [phase-count-12] 33273 negative 99.3% of 33515 except 242 0.7%
c [phase-count-12] 26965 positive 80.5% of 33515 except 6550 19.5%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-12] sorted 2223 enqueued variables after 38002 conflicts
c [score-dist-12] active 3813 (63%), one 0 (0%), zero 2223 (37%)
c [score-dist-12] max exp 516, different 16 (3%)
c [score-dist-12] median active exp 510, avg 509.4
c [simplification-12] removed 1048 variables 14.8% (6036 remain 3%)
c [simplification-12] removed 10142 irredundant clauses 23.2% (33515 remain 3%)
c [simplification-12] maximum reduction of 23% = max (15%, 23%)
c [simplification-12] large reduction 23% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 50002 (soft 40002 + delta 10000)
c [simplification-12] new conflict limit 40002 (hard 50002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   46.2    6035    33515     38208    2459    934 30043   28    65   12  43%     30   23   29   28  103%
c i   46.3    6032    33515     38871    3094    935 30044   29    69   13  42%      9   26   37   29  131%
c i   46.6    6031    33515     39707    3871    938 30045   31    72   13  44%     -3   29   43   29  151%
c 
c [simplification-13] limit 40002 conflicts (hard 50002) hit after 41625 conflicts
c [quatres-7] found 1572 quaternary clauses 54% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [ternres-9] limit 6808003 with penalty 0 = 0 + 0
c [ternres-9] all 6031 free variables schedulable
c [ternres-9] 48 ternary resolvents (0 bin, 48 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-32] removed 6 variables
c [basicprobe-5] limit 34040019 penalty 0 = 0 + 0
c [basicprobe-5-0] 1345 sched 25%, 364 failed, 31 lifted, 27538 hbrs
c [decomp-33] removed 673 variables
c [basicprobe-5-1] 1104 sched 22%, 219 failed, 10 lifted, 19288 hbrs
c [decomp-34] removed 452 variables
c [basicprobe-5-2] 656 probes remain 14% after last round
c [basicprobe-5-2] 682 units = 636 failed (93%) + 46 lifted (7%)
c [basicprobe-5-2] removed 1203 variables, found 52616 hbrs
c [bate-3] eliminated 118 asymmetric tautologies during probing
c [unhide-13] limit 1361600 with penalty 0 = 0 + 0
c [unhide-13-30] 1 units, 22 failed, 8754 tauts, 0 hbrs, 14228 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 490 transitive binary clauses
c [transred-9] found 2 units
c [cce-5] limit of 34040019 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 11
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 9
c [cce-5-1] eliminated 4 clauses out of 13 (31%) of length 8
c [cce-5-1] eliminated 9 clauses out of 45 (20%) of length 7
c [cce-5-1] eliminated 12 clauses out of 191 (6%) of length 6
c [cce-5-1] eliminated 56 clauses out of 415 (13%) of length 5
c [cce-5-1] eliminated 112 clauses out of 1100 (10%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 198 large clauses in 3930903 steps
c [cce-5-1] allowing another 1965451 steps for small clauses
c [cce-5-1] scheduling 19783 clauses = 16438 binary + 3345 ternary
c [cce-5-1] tried to eliminate 7835 small clauses 40%
c [cce-5-1] eliminated 1089 binary clauses 7%
c [cce-5-1] eliminated 108 ternary clauses 3%
c [cce-5-1] eliminated 1197 small clauses 6%
c [cce-5-1] eliminated 1216 small clauses in 34040020 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1414 covered clauses in round 1
c [cce-5] eliminated 1414 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 4788 variables 100%
c [elim-12] limit of 136160077 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 725 variables 15% in round 1 in 1400818 steps
c [elim-12-1] backward subsumption/strengthening limit 1400800
c [elim-12-1-1] backward checking 2245 touched variables 47%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 4 clauses in 241989 steps
c [elim-12-1] rescheduled 23 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 10508 steps
c [elim-12-2] backward subsumption/strengthening limit 10500
c [elim-12-2-1] backward checking 21 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 3 and strengthened 0 clauses in 9863 steps
c [elim-12-2] rescheduled 10 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 8024 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 726 = 15% variables out of 4788 scheduled
c [bca-9] limit of 10000000 steps and 45427 added (scaled 2)
c [bca-9] 6905 out of 8126 literals actually usable 85%
c [bca-9] added 46 blocked clauses in 18090 steps
c [sweep-9] limit 2042401 penalty 0 = 0 + 0
c [sweep-9-1] 162 pos 28.4% + 408 neg 71.6% = 570 sched 14.0% ret 3492
c [sweep-9-1] 1395044 steps 303 queries 13.47 avg class size
c [sweep-9-1] 1358 decisions 297 SAT calls 19.09 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-35] removed 6 variables
c [sweep-9-1] removed 6 vars (0 failed, 7 eqs, 15 impls)
c [sweep-9-2] 737 pos 18.2% + 3319 neg 81.8% = 4056 sched 100.0% ret 0
c [sweep-9-2] 647593 steps 43 queries 244.77 avg class size
c [sweep-9-2] 982 decisions 41 SAT calls 97.12 avg env size
c [sweep-9-2] 2596 variables remain 64% (1460 retained 36%)
c [decomp-36] removed 1 variables
c [sweep-9-2] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-9] removed 7 vars in TOTAL (2 rounds, 344 queries)
c [sort-queue-13] sorted 1324 enqueued variables after 41625 conflicts
c [score-dist-13] active 2731 (67%), one 0 (0%), zero 1324 (33%)
c [score-dist-13] max exp 516, different 16 (3%)
c [score-dist-13] median active exp 510, avg 509.5
c [simplification-13] removed 1976 variables 32.8% (4055 remain 2%)
c [simplification-13] removed 11108 irredundant clauses 33.1% (22407 remain 2%)
c [simplification-13] maximum reduction of 33% = max (33%, 33%)
c [simplification-13] large reduction 33% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 53625 (soft 43625 + delta 10000)
c [simplification-13] new conflict limit 43625 (hard 53625)
c 
c [simplification-14] limit 43625 conflicts (hard 53625) hit after 43627 conflicts
c [ternres-10] limit 6894424 with penalty 0 = 0 + 0
c [ternres-10] all 4055 free variables schedulable
c [ternres-10] 75 ternary resolvents (0 bin, 75 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 7 xors of average arity 3.0
c [gauss-4] connected 21 occurrences of 15 variables (average 1.4)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 4055 free variables schedulable
c [simpleprobe-6] limit 27577696 penalty 0 = 0 + 0
c [decomp-38] removed 10 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 10 variables, found 2705 hbrs, 6 units
c [unhide-14] limit 1378884 with penalty 0 = 0 + 0
c [unhide-14-37] 0 units, 18 failed, 4064 tauts, 0 hbrs, 10669 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 437 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4042 variables 100%
c [block-4] limit of 8618030 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 99 blocked clauses
c [block-4] 99 < 1/100 * 22068 = 220 considered unsuccessful
c [cce-6] limit of 34472120 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-6-1] eliminated 1 clauses out of 8 (12%) of length 10
c [cce-6-1] eliminated 4 clauses out of 188 (2%) of length 6
c [cce-6-1] eliminated 9 clauses out of 466 (2%) of length 5
c [cce-6-1] eliminated 55 clauses out of 1083 (5%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 71 large clauses in 5135711 steps
c [cce-6-1] allowing another 2567855 steps for small clauses
c [cce-6-1] scheduling 17061 clauses = 13894 binary + 3167 ternary
c [cce-6-1] tried to eliminate 8125 small clauses 48%
c [cce-6-1] eliminated 408 binary clauses 3%
c [cce-6-1] eliminated 71 ternary clauses 2%
c [cce-6-1] eliminated 479 small clauses 3%
c [cce-6-1] eliminated 479 small clauses in 34472120 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 550 covered clauses in round 1
c [cce-6] eliminated 550 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 4042 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 113 variables 3% in round 1 in 1244927 steps
c [elim-13-1] backward subsumption/strengthening limit 1244900
c [elim-13-1-1] backward checking 675 touched variables 17%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 79846 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 113 = 3% variables out of 4042 scheduled
c [bca-10] limit of 10000000 steps and 43044 added (scaled 2)
c [bca-10] 6559 out of 7860 literals actually usable 83%
c [bca-10] added 23 blocked clauses in 18409 steps
c [sweep-10] limit 2068327 penalty 0 = 0 + 0
c [sweep-10-1] 632 pos 25.3% + 1865 neg 74.7% = 2497 sched 63.6% ret 1432
c [sweep-10-1] 2075879 steps 288 queries 30.74 avg class size
c [sweep-10-1] 2454 decisions 284 SAT calls 36.18 avg env size
c [sweep-10-1] 842 variables remain 21% (3084 retained 79%)
c [decomp-39] removed 7 variables
c [sweep-10-1] removed 7 vars (0 failed, 4 eqs, 7 impls)
c [sweep-10] removed 7 vars in TOTAL (1 rounds, 287 queries)
c [sort-queue-14] sorted 1262 enqueued variables after 43627 conflicts
c [score-dist-14] active 2660 (68%), one 0 (0%), zero 1262 (32%)
c [score-dist-14] max exp 516, different 16 (3%)
c [score-dist-14] median active exp 510, avg 509.4
c [simplification-14] removed 133 variables 3.3% (3922 remain 2%)
c [simplification-14] removed 1200 irredundant clauses 5.4% (21207 remain 2%)
c [simplification-14] maximum reduction of 5% = max (3%, 5%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 55627 (soft 45627 + delta 10000)
c [simplification-14] new conflict limit 45627 (hard 55627)
c 
c [simplification-15] limit 45627 conflicts (hard 55627) hit after 45627 conflicts
c [ternres-11] limit 6985042 with penalty 0 = 0 + 0
c [ternres-11] all 3922 free variables schedulable
c [ternres-11] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 218282 penalty 4 = 4 + 0
c [card-5] found 654 at-most-one constraints of average size 3.4
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 218282 for elimination
c [card-5] 654 out of 654 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [treelook-6] limit 698504 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 7844 literals 100%
c [treelook-6] scheduling used 132028 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 698504 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 699786 steps
c [treelook-6] 7800 literals remain 99%
c [treelook-6] 3918 variables remain to probed next time 100%
c [treelook-6] removed 0 variables, found 6061 hbrs
c [unhide-15] limit 1397008 with penalty 0 = 0 + 0
c [unhide-15-44] 1 units, 10 failed, 3226 tauts, 0 hbrs, 4773 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 330 transitive binary clauses
c [transred-11] found 3 units
c [cce-7] limit of 34925210 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 11
c [cce-7-1] eliminated 3 clauses out of 23 (13%) of length 8
c [cce-7-1] eliminated 2 clauses out of 44 (5%) of length 7
c [cce-7-1] eliminated 6 clauses out of 183 (3%) of length 6
c [cce-7-1] eliminated 12 clauses out of 423 (3%) of length 5
c [cce-7-1] eliminated 56 clauses out of 1013 (6%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 84 large clauses in 4896337 steps
c [cce-7-1] allowing another 2448168 steps for small clauses
c [cce-7-1] scheduling 16329 clauses = 13300 binary + 3029 ternary
c [cce-7-1] tried to eliminate 8447 small clauses 52%
c [cce-7-1] eliminated 555 binary clauses 4%
c [cce-7-1] eliminated 142 ternary clauses 5%
c [cce-7-1] eliminated 697 small clauses 4%
c [cce-7-1] eliminated 719 small clauses in 34925213 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 803 covered clauses in round 1
c [cce-7] eliminated 803 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 3911 variables 100%
c [elim-14] limit of 139700841 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 115 variables 3% in round 1 in 1157639 steps
c [elim-14-1] backward subsumption/strengthening limit 1157600
c [elim-14-1-1] backward checking 653 touched variables 17%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 0 clauses in 73388 steps
c [elim-14-1] rescheduled 4 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 1494 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 115 = 3% variables out of 3911 scheduled
c [bca-11] limit of 10000000 steps and 40794 added (scaled 2)
c [bca-11] 6387 out of 7594 literals actually usable 84%
c [bca-11] added 25 blocked clauses in 17267 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 20955120 penalty 0 = 0 + 0
c [sweep-11-1] 255 pos 31.6% + 553 neg 68.4% = 808 sched 21.3% ret 2988
c [sweep-11-1] 2046265 steps 459 queries 11.49 avg class size
c [sweep-11-1] 2064 decisions 457 SAT calls 17.99 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-42] removed 3 variables
c [sweep-11-1] removed 3 vars (0 failed, 3 eqs, 5 impls)
c [sweep-11-2] 636 pos 16.8% + 3157 neg 83.2% = 3793 sched 100.0% ret 0
c [sweep-11-2] 4615356 steps 688 queries 15.01 avg class size
c [sweep-11-2] 4207 decisions 677 SAT calls 27.45 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-43] removed 20 variables
c [sweep-11-2] removed 20 vars (0 failed, 20 eqs, 22 impls)
c [sweep-11-3] 630 pos 16.7% + 3143 neg 83.3% = 3773 sched 100.0% ret 0
c [sweep-11-3] 4255878 steps 624 queries 21.74 avg class size
c [sweep-11-3] 3536 decisions 604 SAT calls 28.95 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-44] removed 47 variables
c [sweep-11-3] removed 47 vars (0 failed, 20 eqs, 20 impls)
c [sweep-11] removed 70 vars in TOTAL (3 rounds, 1768 queries)
c [sort-queue-15] sorted 1140 enqueued variables after 45627 conflicts
c [score-dist-15] active 2586 (69%), one 0 (0%), zero 1140 (31%)
c [score-dist-15] max exp 516, different 16 (3%)
c [score-dist-15] median active exp 510, avg 509.3
c [simplification-15] removed 196 variables 5.0% (3726 remain 2%)
c [simplification-15] removed 1368 irredundant clauses 6.5% (19839 remain 2%)
c [simplification-15] maximum reduction of 6% = max (5%, 6%)
c [simplification-15] large reduction 6% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 57627 (soft 47627 + delta 10000)
c [simplification-15] new conflict limit 47627 (hard 57627)
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   54.8    3725    19839     46097    3369    449 28630   49    89   12  55%     63   42   58   31  187%
c i   54.9    3723    19839     46517    3752    449 28630   50    89   12  56%     35   42   57   31  182%
c 
c [simplification-16] limit 47627 conflicts (hard 57627) hit after 47636 conflicts
c [quatres-8] found 977 quaternary clauses 55% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [ternres-12] limit 7060467 with penalty 0 = 0 + 0
c [ternres-12] all 3723 free variables schedulable
c [ternres-12] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-45] removed 3 variables
c [basicprobe-6] limit 35302338 penalty 0 = 0 + 0
c [basicprobe-6-0] 777 sched 21%, 92 failed, 8 lifted, 6656 hbrs
c [decomp-46] removed 123 variables
c [basicprobe-6-1] 938 sched 27%, 101 failed, 3 lifted, 5790 hbrs
c [decomp-47] removed 160 variables
c [basicprobe-6-2] 835 sched 25%, 35 failed, 0 lifted, 6905 hbrs
c [decomp-48] removed 51 variables
c [basicprobe-6-3] 812 sched 24%, 58 failed, 3 lifted, 1289 hbrs
c [decomp-49] removed 100 variables
c [basicprobe-6-4] 764 sched 23%, 23 failed, 0 lifted, 2269 hbrs
c [decomp-50] removed 44 variables
c [basicprobe-6-5] 126 probes remain 4% after last round
c [basicprobe-6-5] 329 units = 315 failed (96%) + 14 lifted (4%)
c [basicprobe-6-5] removed 484 variables, found 23715 hbrs
c [bate-4] eliminated 112 asymmetric tautologies during probing
c [unhide-16] limit 1412093 with penalty 0 = 0 + 0
c [unhide-16-53] 0 units, 0 failed, 4603 tauts, 0 hbrs, 8313 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 458 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 353023380 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 8
c [cce-8-1] eliminated 2 clauses out of 73 (3%) of length 6
c [cce-8-1] eliminated 8 clauses out of 273 (3%) of length 5
c [cce-8-1] eliminated 38 clauses out of 714 (5%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 52 large clauses in 2598146 steps
c [cce-8-1] allowing another 1299073 steps for small clauses
c [cce-8-1] scheduling 12672 clauses = 10237 binary + 2435 ternary
c [cce-8-1] tried to eliminate 12672 small clauses 100%
c [cce-8-1] eliminated 531 binary clauses 5%
c [cce-8-1] eliminated 88 ternary clauses 4%
c [cce-8-1] eliminated 619 small clauses 5%
c [cce-8-1] eliminated 619 small clauses in 36096031 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 671 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1228486 steps for small clauses
c [cce-8-2] scheduling 12053 clauses = 9706 binary + 2347 ternary
c [cce-8-2] tried to eliminate 12053 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 671 covered clauses in TOTAL during 2 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 3239 variables 100%
c [elim-15] limit of 141209352 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 441 variables 14% in round 1 in 881070 steps
c [elim-15-1] backward subsumption/strengthening limit 881000
c [elim-15-1-1] backward checking 1227 touched variables 38%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 1 and strengthened 21 clauses in 149318 steps
c [elim-15-1] rescheduled 43 variables 1% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 18189 steps
c [elim-15-2] backward subsumption/strengthening limit 18100
c [elim-15-2-1] backward checking 16 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 1 and strengthened 1 clauses in 7522 steps
c [elim-15-2] rescheduled 12 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 3918 steps
c [elim-15-3] backward subsumption/strengthening limit 3900
c [elim-15-3-1] backward checking 16 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 0 and strengthened 0 clauses in 3901 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 444 = 14% variables out of 3239 scheduled
c [bca-12] limit of 10000000 steps and 29962 added (scaled 2)
c [bca-12] 4822 out of 5592 literals actually usable 86%
c [bca-12] added 39 blocked clauses in 12207 steps
c [sweep-12] limit 2118140 penalty 0 = 0 + 0
c [sweep-12-1] 451 pos 16.1% + 2344 neg 83.9% = 2795 sched 100.0% ret 0
c [sweep-12-1] 1897709 steps 543 queries 13.39 avg class size
c [sweep-12-1] 3072 decisions 529 SAT calls 24.21 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-51] removed 11 variables
c [sweep-12-1] removed 11 vars (0 failed, 14 eqs, 22 impls)
c [sweep-12-2] 448 pos 16.1% + 2336 neg 83.9% = 2784 sched 100.0% ret 0
c [sweep-12-2] 225704 steps 37 queries 191.22 avg class size
c [sweep-12-2] 597 decisions 35 SAT calls 56.49 avg env size
c [sweep-12-2] 1854 variables remain 67% (930 retained 33%)
c [sweep-12-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 11 vars in TOTAL (2 rounds, 578 queries)
c [sort-queue-16] sorted 927 enqueued variables after 47636 conflicts
c [score-dist-16] active 1857 (67%), one 0 (0%), zero 927 (33%)
c [score-dist-16] max exp 516, different 16 (3%)
c [score-dist-16] median active exp 509, avg 509.0
c [simplification-16] removed 939 variables 25.2% (2784 remain 1%)
c [simplification-16] removed 5161 irredundant clauses 26.0% (14678 remain 1%)
c [simplification-16] maximum reduction of 26% = max (25%, 26%)
c [simplification-16] large reduction 26% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 59636 (soft 49636 + delta 10000)
c [simplification-16] new conflict limit 49636 (hard 59636)
c 
c [simplification-17] limit 49636 conflicts (hard 59636) hit after 49636 conflicts
c [ternres-13] limit 7126162 with penalty 0 = 0 + 0
c [ternres-13] all 2784 free variables schedulable
c [ternres-13] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-7] all 2784 free variables schedulable
c [simpleprobe-7] limit 28504650 penalty 0 = 0 + 0
c [decomp-54] removed 2 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 2 variables, found 1017 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 651 transitive binary clauses
c [cce-9] limit of 35630812 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 48
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 11
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 10
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 9
c [cce-9-1] eliminated 2 clauses out of 8 (25%) of length 8
c [cce-9-1] eliminated 2 clauses out of 22 (9%) of length 7
c [cce-9-1] eliminated 4 clauses out of 76 (5%) of length 6
c [cce-9-1] eliminated 5 clauses out of 298 (2%) of length 5
c [cce-9-1] eliminated 42 clauses out of 736 (6%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 69 large clauses in 3340110 steps
c [cce-9-1] allowing another 1670055 steps for small clauses
c [cce-9-1] scheduling 11343 clauses = 9044 binary + 2299 ternary
c [cce-9-1] tried to eliminate 11343 small clauses 100%
c [cce-9-1] eliminated 590 binary clauses 7%
c [cce-9-1] eliminated 103 ternary clauses 4%
c [cce-9-1] eliminated 693 small clauses 6%
c [cce-9-1] eliminated 693 small clauses in 33416272 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 762 covered clauses in round 1
c [cce-9-2] eliminated 3 clauses out of 72 (4%) of length 6
c [cce-9-2] eliminated 4 clauses out of 694 (1%) of length 4
c [cce-9-2] incomplete large round (ACCE)
c [cce-9-2] eliminated 7 large clauses in 2214541 steps
c [cce-9-2] allowing another 1107270 steps for small clauses
c [cce-9-2] scheduling 10650 clauses = 8454 binary + 2196 ternary
c [cce-9-2] tried to eliminate 405 small clauses 4%
c [cce-9-2] eliminated 1 binary clauses 0%
c [cce-9-2] eliminated 1 small clauses 0%
c [cce-9-2] eliminated 1 small clauses in 2214544 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 8 covered clauses in round 2
c [cce-9] eliminated 770 covered clauses in TOTAL during 2 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2782 variables 100%
c [elim-16] limit of 142523251 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 138 variables 5% in round 1 in 786996 steps
c [elim-16-1] backward subsumption/strengthening limit 786900
c [elim-16-1-1] backward checking 591 touched variables 21%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 58667 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 138 = 5% variables out of 2782 scheduled
c [bca-13] limit of 10000000 steps and 28016 added (scaled 2)
c [bca-13] 4414 out of 5290 literals actually usable 83%
c [bca-13] added 19 blocked clauses in 12859 steps
c [sweep-13] limit 2137848 penalty 0 = 0 + 0
c [sweep-13-1] 330 pos 19.0% + 1405 neg 81.0% = 1735 sched 65.6% ret 909
c [sweep-13-1] 2137977 steps 403 queries 14.68 avg class size
c [sweep-13-1] 3250 decisions 402 SAT calls 28.27 avg env size
c [sweep-13-1] 102 variables remain 4% (2542 retained 96%)
c [sweep-13-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-13] removed 0 vars in TOTAL (1 rounds, 402 queries)
c [sort-queue-17] sorted 871 enqueued variables after 49636 conflicts
c [score-dist-17] active 1773 (67%), one 0 (0%), zero 871 (33%)
c [score-dist-17] max exp 516, different 16 (3%)
c [score-dist-17] median active exp 510, avg 509.2
c [simplification-17] removed 140 variables 5.0% (2644 remain 1%)
c [simplification-17] removed 981 irredundant clauses 6.7% (13697 remain 1%)
c [simplification-17] maximum reduction of 7% = max (5%, 7%)
c [simplification-17] large reduction 7% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 61636 (soft 51636 + delta 10000)
c [simplification-17] new conflict limit 51636 (hard 61636)
c 
c [simplification-18] limit 51636 conflicts (hard 61636) hit after 51639 conflicts
c [ternres-14] limit 7190161 with penalty 0 = 0 + 0
c [ternres-14] all 2644 free variables schedulable
c [ternres-14] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-14] fully completed ternary resolution
c [unhide-17] limit 719016 with penalty 1 = 1 + 0
c [unhide-17-59] 0 units, 0 failed, 993 tauts, 0 hbrs, 7613 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 270 transitive binary clauses
c [cce-10] limit of 35950809 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-10-1] eliminated 2 clauses out of 70 (3%) of length 6
c [cce-10-1] eliminated 1 clauses out of 295 (0%) of length 5
c [cce-10-1] eliminated 3 clauses out of 681 (0%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 7 large clauses in 2884715 steps
c [cce-10-1] allowing another 1442357 steps for small clauses
c [cce-10-1] scheduling 10482 clauses = 8292 binary + 2190 ternary
c [cce-10-1] tried to eliminate 10482 small clauses 100%
c [cce-10-1] eliminated 28 binary clauses 0%
c [cce-10-1] eliminated 1 ternary clauses 0%
c [cce-10-1] eliminated 29 small clauses 0%
c [cce-10-1] eliminated 29 small clauses in 29530674 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 36 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 1438035 steps for small clauses
c [cce-10-2] scheduling 10453 clauses = 8264 binary + 2189 ternary
c [cce-10-2] tried to eliminate 1824 small clauses 17%
c [cce-10-2] incomplete small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 36 covered clauses in TOTAL during 2 rounds
c [cce-10] 36 < 1/100 * 13681 = 136 considered unsuccessful
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 2644 variables 100%
c [elim-17] limit of 143803236 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 5 variables 0% in round 1 in 770824 steps
c [elim-17-1] backward subsumption/strengthening limit 770800
c [elim-17-1-1] backward checking 51 touched variables 2%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 6109 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 5 = 0% variables out of 2644 scheduled
c [elim-17] 5 < 1/100 * 2644 = 26 considered unsuccessful
c [bca-14] limit of 10000000 steps and 27897 added (scaled 2)
c [bca-14] 4345 out of 5280 literals actually usable 82%
c [bca-14] added 21 blocked clauses in 14275 steps
c [sort-queue-18] sorted 864 enqueued variables after 51639 conflicts
c [score-dist-18] active 1775 (67%), one 0 (0%), zero 864 (33%)
c [score-dist-18] max exp 516, different 16 (3%)
c [score-dist-18] median active exp 510, avg 509.3
c [simplification-18] removed 5 variables 0.2% (2639 remain 1%)
c [simplification-18] removed 64 irredundant clauses 0.5% (13633 remain 1%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 20000
c [simplification-18] new conflict interval 35000
c [simplification-18] penalized conflict interval 35000 = 1 * 35000
c [simplification-18] hard conflict limit 104139 (soft 86639 + delta 17500)
c [simplification-18] new conflict limit 86639 (hard 104139)
c 
c [simplification-19] limit 86639 conflicts (hard 104139) hit after 104140 conflicts
c [gauss-5] limit 126905 penalty 4 = 4 + 0
c [gauss-5] extracted 1 xors of average arity 3.0
c [gauss-5] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-5] limit 126905 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-7] limit 507623 penalty 1 = 1 + 0 boost 1
c [treelook-7] scheduled 5278 literals 100%
c [treelook-7] scheduling used 188684 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 507623 penalty 1 = 1 + 0 boost 1
c [treelook-7] used 515722 steps
c [treelook-7] 5216 literals remain 99%
c [treelook-7] 2637 variables remain to probed next time 100%
c [treelook-7] removed 0 variables, found 2972 hbrs
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 303 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 2639 variables 100%
c [block-5] limit of 6345294 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 12 blocked clauses
c [block-5] 12 < 1/100 * 13632 = 136 considered unsuccessful
c [bca-15] limit of 10000000 steps and 27882 added (scaled 2)
c [bca-15] 3992 out of 5280 literals actually usable 76%
c [bca-15] added 3 blocked clauses in 59963 steps
c [sweep-14] limit 1522870 penalty 1 = 1 + 0
c [sweep-14-1] 46 pos 45.5% + 55 neg 54.5% = 101 sched 3.8% ret 2538
c [sweep-14-1] 717038 steps 75 queries 7.35 avg class size
c [sweep-14-1] 445 decisions 74 SAT calls 18.32 avg env size
c [sweep-14-1] fully completed sweeping round
c [sweep-14-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14-2] 412 pos 15.6% + 2227 neg 84.4% = 2639 sched 100.0% ret 0
c [sweep-14-2] 906321 steps 13 queries 300.15 avg class size
c [sweep-14-2] 726 decisions 12 SAT calls 202.42 avg env size
c [sweep-14-2] 2484 variables remain 94% (155 retained 6%)
c [sweep-14-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14] removed 0 vars in TOTAL (2 rounds, 86 queries)
c [sort-queue-19] sorted 791 enqueued variables after 104140 conflicts
c [score-dist-19] active 1848 (70%), one 0 (0%), zero 791 (30%)
c [score-dist-19] max exp 518, different 18 (3%)
c [score-dist-19] median active exp 511, avg 510.0
c [simplification-19] removed 0 variables 0.0% (2639 remain 1%)
c [simplification-19] removed 13 irredundant clauses 0.1% (13620 remain 1%)
c [simplification-19] maximum reduction of 0% = max (0%, 0%)
c [simplification-19] full geometric conflict interval increment 35000
c [simplification-19] new conflict interval 70000
c [simplification-19] penalized conflict interval 70000 = 1 * 70000
c [simplification-19] hard conflict limit 209140 (soft 174140 + delta 35000)
c [simplification-19] new conflict limit 174140 (hard 209140)
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 -   71.5    2639    13620    104421   24106    302 18152   29    38   17  78%    585  -13   28   34   84%
c -   77.2    2639    13620    136835   25185    302 18152   31    39   19  80%    756   -9   29   34   86%
c -   83.0    2639    13620    169445   25916    302 18152   38    46   19  83%    861   -0   31   35   90%
c -   88.5    2639    13620    202931   24311    302 18152   32    38   19  84%    926   -5   32   34   94%
c 
c [simplification-20] limit 174140 conflicts (hard 209140) hit after 209141 conflicts
c [quatres-9] found 701 quaternary clauses 38% in total
c [ternres-15] limit 8247910 with penalty 1 = 1 + 0
c [ternres-15] all 2639 free variables schedulable
c [ternres-15] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-15] fully completed ternary resolution
c [basicprobe-7] limit 82479107 penalty 0 = 0 + 0
c [basicprobe-7-0] 212 sched 8%, 4 failed, 0 lifted, 465 hbrs
c [decomp-62] removed 11 variables
c [basicprobe-7-1] 769 sched 29%, 1 failed, 0 lifted, 1133 hbrs
c [decomp-63] removed 1 variables
c [basicprobe-7-2] 766 sched 29%, 1 failed, 0 lifted, 65 hbrs
c [decomp-64] removed 1 variables
c [basicprobe-7-3] 766 sched 29%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-7-4] 766 sched 29%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-7-5] 766 sched 29%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-7-6] 766 sched 29%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-7] 766 sched 29%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-7-8] 766 sched 29%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-7-8] round limit 8 hit
c [basicprobe-7-8] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-7-8] removed 13 variables, found 1694 hbrs
c [bate-5] eliminated 11 asymmetric tautologies during probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 300 transitive binary clauses
c [cce-11] limit of 41239553 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-11-1] eliminated 2 clauses out of 286 (1%) of length 5
c [cce-11-1] eliminated 4 clauses out of 655 (1%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 9 large clauses in 2746555 steps
c [cce-11-1] allowing another 1373277 steps for small clauses
c [cce-11-1] scheduling 10361 clauses = 8316 binary + 2045 ternary
c [cce-11-1] tried to eliminate 10361 small clauses 100%
c [cce-11-1] eliminated 122 binary clauses 1%
c [cce-11-1] eliminated 129 ternary clauses 6%
c [cce-11-1] eliminated 251 small clauses 2%
c [cce-11-1] eliminated 251 small clauses in 28658400 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 260 covered clauses in round 1
c [cce-11-2] eliminated 2 clauses out of 651 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 2 large clauses in 2664533 steps
c [cce-11-2] allowing another 1332266 steps for small clauses
c [cce-11-2] scheduling 10110 clauses = 8194 binary + 1916 ternary
c [cce-11-2] tried to eliminate 4299 small clauses 43%
c [cce-11-2] eliminated 5 binary clauses 0%
c [cce-11-2] eliminated 3 ternary clauses 0%
c [cce-11-2] eliminated 8 small clauses 0%
c [cce-11-2] eliminated 8 small clauses in 12581154 steps
c [cce-11-2] incomplete small round (ACCE)
c [cce-11-2] eliminated 10 covered clauses in round 2
c [cce-11] eliminated 270 covered clauses in TOTAL during 2 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2626 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 3299164310 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 35 variables 1% in round 1 in 739369 steps
c [elim-18-1] backward subsumption/strengthening limit 739300
c [elim-18-1-1] backward checking 245 touched variables 9%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 1 and strengthened 1 clauses in 22584 steps
c [elim-18-1] rescheduled 20 variables 1% by backward subsumption
c [elim-18-2] no variable eliminated in round 2 in 8745 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 35 = 1% variables out of 2626 scheduled
c [bca-16] limit of 10000000 steps and 27059 added (scaled 2)
c [bca-16] 3835 out of 5184 literals actually usable 74%
c [bca-16] added 7 blocked clauses in 39189 steps
c [sort-queue-20] sorted 681 enqueued variables after 209141 conflicts
c [score-dist-20] active 1910 (74%), one 0 (0%), zero 681 (26%)
c [score-dist-20] max exp 519, different 19 (4%)
c [score-dist-20] median active exp 512, avg 510.6
c [simplification-20] removed 48 variables 1.8% (2591 remain 1%)
c [simplification-20] removed 412 irredundant clauses 3.0% (13208 remain 1%)
c [simplification-20] maximum reduction of 3% = max (2%, 3%)
c [simplification-20] geometric conflict interval increment 17500 = 70000 / 4
c [simplification-20] new conflict interval 87500
c [simplification-20] penalized conflict interval 87500 = 1 * 87500
c [simplification-20] hard conflict limit 340391 (soft 296641 + delta 43750)
c [simplification-20] new conflict limit 296641 (hard 340391)
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 -   97.2    2591    13208    238326   25894    398 18483   35    46   17  76%    967    4   45   33  135%
c -  103.2    2591    13208    274020   26177    399 18483   33    40   17  83%    991   -4   31   35   88%
c 
c [simplification-21] limit 296641 conflicts (hard 340391) hit after 299704 conflicts
c [ternres-16] limit 21894940 with penalty 0 = 0 + 0
c [ternres-16] all 2591 free variables schedulable
c [ternres-16] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 684216 penalty 4 = 4 + 0
c [card-6] found 1020 at-most-one constraints of average size 3.6
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 684216 for elimination
c [card-6] 1020 out of 1020 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 890 at-most-one constraints, 823 used 92%
c [card-6] exported 6388 binary clauses, 7.8 per/constraint
c [simpleprobe-8] all 2591 free variables schedulable
c [simpleprobe-8] limit 87579761 penalty 0 = 0 + 0
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 0 variables, found 1741 hbrs, 0 units
c [unhide-18] limit 1094747 with penalty 2 = 2 + 0
c [unhide-18-61] 0 units, 0 failed, 4040 tauts, 0 hbrs, 25775 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 451 transitive binary clauses
c [cce-12] limit of 109474701 steps penalty 0 = 0 + 0
c [cce-12-1] completed large round (ATE)
c [cce-12-1] allowing another 1368782 steps for small clauses
c [cce-12-1] scheduling 10033 clauses = 8125 binary + 1908 ternary
c [cce-12-1] tried to eliminate 10033 small clauses 100%
c [cce-12-1] eliminated 5 binary clauses 0%
c [cce-12-1] eliminated 1 ternary clauses 0%
c [cce-12-1] eliminated 6 small clauses 0%
c [cce-12-1] eliminated 6 small clauses in 26805234 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 6 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1367929 steps for small clauses
c [cce-12-2] scheduling 10027 clauses = 8120 binary + 1907 ternary
c [cce-12-2] tried to eliminate 10027 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 6 covered clauses in TOTAL during 2 rounds
c [cce-12] 6 < 1/100 * 13208 = 132 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2591 variables 100%
c [elim-19] limit of 437898806 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] no variable eliminated in round 1 in 736038 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 0 = 0% variables out of 2591 scheduled
c [bca-17] limit of 10000000 steps and 27051 added (scaled 2)
c [bca-17] 3795 out of 5184 literals actually usable 73%
c [bca-17] added 14 blocked clauses in 56591 steps
c [sort-queue-21] sorted 663 enqueued variables after 299704 conflicts
c [score-dist-21] active 1928 (74%), one 0 (0%), zero 663 (26%)
c [score-dist-21] max exp 519, different 19 (4%)
c [score-dist-21] median active exp 512, avg 511.1
c [simplification-21] removed 0 variables 0.0% (2591 remain 1%)
c [simplification-21] removed 6 irredundant clauses 0.0% (13202 remain 1%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 87500
c [simplification-21] new conflict interval 175000
c [simplification-21] penalized conflict interval 175000 = 1 * 175000
c [simplification-21] hard conflict limit 562204 (soft 474704 + delta 87500)
c [simplification-21] new conflict limit 474704 (hard 562204)
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 -  111.5    2591    13202    312008   26335    404 21995   32    40   19  79%   1006   -3   30   34   87%
c -  118.3    2591    13202    352728   27877    420 21996   36    43   19  83%   1014    0   37   34  107%
c -  125.2    2591    13202    394554   28650    422 21996   34    44   19  78%   1019    1   38   34  110%
c -  131.4    2591    13202    434825   29084    422 21997   27    38   25  72%   1021   -4   22   32   71%
c -  137.9    2591    13202    473804   29534    423 21998   28    37   25  76%   1022   -3   33   30  109%
c 
c [simplification-22] limit 474704 conflicts (hard 562204) hit after 482655 conflicts
c [ternres-17] limit 34217356 with penalty 0 = 0 + 0
c [ternres-17] all 2591 free variables schedulable
c [ternres-17] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-17] fully completed ternary resolution
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 347 transitive binary clauses
c [bca-18] limit of 10000000 steps and 27058 added (scaled 2)
c [bca-18] 3847 out of 5184 literals actually usable 74%
c [bca-18] added 10 blocked clauses in 46360 steps
c [sweep-15] limit 2566301 penalty 2 = 2 + 0
c [sweep-15-1] 361 pos 14.8% + 2076 neg 85.2% = 2437 sched 94.1% ret 154
c [sweep-15-1] 2627598 steps 52 queries 69.33 avg class size
c [sweep-15-1] 1851 decisions 52 SAT calls 111.04 avg env size
c [sweep-15-1] 1257 variables remain 49% (1333 retained 51%)
c [decomp-73] removed 1 variables
c [sweep-15-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15] 1 < 1/1000 * 2591 = 2 considered unsuccessful
c [sweep-15] removed 1 vars in TOTAL (1 rounds, 51 queries)
c [sort-queue-22] sorted 653 enqueued variables after 482655 conflicts
c [score-dist-22] active 1937 (75%), one 0 (0%), zero 653 (25%)
c [score-dist-22] max exp 520, different 20 (4%)
c [score-dist-22] median active exp 512, avg 511.5
c [simplification-22] removed 1 variables 0.0% (2590 remain 1%)
c [simplification-22] removed 11 irredundant clauses 0.1% (13191 remain 1%)
c [simplification-22] maximum reduction of 0% = max (0%, 0%)
c [simplification-22] full geometric conflict interval increment 175000
c [simplification-22] new conflict interval 350000
c [simplification-22] penalized conflict interval 350000 = 1 * 350000
c [simplification-22] hard conflict limit 1007655 (soft 832655 + delta 175000)
c [simplification-22] new conflict limit 832655 (hard 1007655)
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.7    2590    13191    516083   30159    423 21670   29    36   18  81%   1023   -2   31   29  106%
c -  153.4    2590    13191    560992   31063    423 21670   31    39   18  78%   1024    2   29   29  101%
c -  160.9    2590    13191    605055   31670    425 21671   45    53   24  86%   1024   12   40   34  117%
c -  168.7    2590    13191    650724   31962    426 21671   29    38   24  75%   1024   -3   23   33   69%
c -  176.0    2590    13191    696634   31662    431 21671   33    42   24  79%   1024    3   33   31  106%
c -  182.9    2590    13191    742525   33628    433 21671   23    35   24  67%   1024   -2   21   28   72%
c -  190.4    2590    13191    787390   34256    434 21671   31    36   24  84%   1024   -1   30   29  103%
c 
c [simplification-23] limit 832655 conflicts (hard 1007655) hit after 832657 conflicts
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 313 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 1450861625 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-13-1] eliminated 6 clauses out of 687 (1%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 7 large clauses in 2795149 steps
c [cce-13-1] allowing another 1397574 steps for small clauses
c [cce-13-1] scheduling 10186 clauses = 8113 binary + 2073 ternary
c [cce-13-1] tried to eliminate 10186 small clauses 100%
c [cce-13-1] eliminated 20 binary clauses 0%
c [cce-13-1] eliminated 32 ternary clauses 2%
c [cce-13-1] eliminated 52 small clauses 1%
c [cce-13-1] eliminated 52 small clauses in 27912810 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 59 covered clauses in round 1
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] allowing another 1376779 steps for small clauses
c [cce-13-2] scheduling 10134 clauses = 8093 binary + 2041 ternary
c [cce-13-2] tried to eliminate 10134 small clauses 100%
c [cce-13-2] eliminated 2 binary clauses 0%
c [cce-13-2] eliminated 2 ternary clauses 0%
c [cce-13-2] eliminated 4 small clauses 0%
c [cce-13-2] eliminated 4 small clauses in 27618331 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 4 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 1376207 steps for small clauses
c [cce-13-3] scheduling 10130 clauses = 8091 binary + 2039 ternary
c [cce-13-3] tried to eliminate 10130 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 0 covered clauses in round 3
c [cce-13] eliminated 63 covered clauses in TOTAL during 3 rounds
c [cce-13] 63 < 1/100 * 13191 = 131 considered unsuccessful
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 2590 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 8 variables 0% in round 1 in 732486 steps
c [elim-20-1] backward subsumption/strengthening limit 732400
c [elim-20-1-1] backward checking 63 touched variables 2%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 6867 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 8 = 0% variables out of 2590 scheduled
c [elim-20] 8 < 1/100 * 2590 = 25 considered unsuccessful
c [bca-19] limit of 10000000 steps and 26899 added (scaled 2)
c [bca-19] 3772 out of 5166 literals actually usable 73%
c [bca-19] added 6 blocked clauses in 80518 steps
c [sort-queue-23] sorted 606 enqueued variables after 832657 conflicts
c [score-dist-23] active 1976 (77%), one 0 (0%), zero 606 (23%)
c [score-dist-23] max exp 521, different 21 (4%)
c [score-dist-23] median active exp 513, avg 511.9
c [simplification-23] removed 8 variables 0.3% (2582 remain 1%)
c [simplification-23] removed 71 irredundant clauses 0.5% (13120 remain 1%)
c [simplification-23] maximum reduction of 1% = max (0%, 1%)
c [simplification-23] geometric conflict interval increment 175000 = 350000 / 2
c [simplification-23] new conflict interval 525000
c [simplification-23] penalized conflict interval 525000 = 1 * 525000
c [simplification-23] hard conflict limit 1620157 (soft 1357657 + delta 262500)
c [simplification-23] new conflict limit 1357657 (hard 1620157)
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 -  200.5    2582    13120    833593   34613    463 21282   38    46   18  82%   1024    8   40   30  132%
c -  209.4    2582    13120    881252   35107    463 21283   25    33   22  75%   1024   -6   25   30   83%
c -  218.1    2582    13120    930988   35390    466 21283   27    34   22  80%   1024   -2   22   28   77%
c -  227.6    2582    13120    986122   36331    471 21283   24    28   22  86%   1024   -4   22   26   83%
c -  236.5    2582    13120   1038342   36979    472 21283   30    36   22  85%   1024    4   25   27   93%
c -  245.7    2582    13120   1089216   37696    471 21284   34    42   31  80%   1024    9   32   27  118%
c -  256.0    2582    13120   1140476   37349    471 21284   27    31   31  85%   1024   -3   27   29   96%
c -  266.9    2582    13120   1195566   37782    471 21284   24    30   31  78%   1024   -3   25   28   88%
c -  277.6    2582    13120   1253124   38383    471 21284   25    28   31  87%   1024   -3   29   26  112%
c -  287.3    2582    13120   1311388   39519    472 21284   22    28   32  79%   1024   -3   17   25   70%
c 
c [simplification-24] limit 1357657 conflicts (hard 1620157) hit after 1364758 conflicts
c [ternres-18] limit 49504158 with penalty 1 = 1 + 0
c [ternres-18] all 2582 free variables schedulable
c [ternres-18] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-18] fully completed ternary resolution
c [treelook-8] limit 2475207 penalty 2 = 2 + 0 boost 1
c [treelook-8] scheduled 5164 literals 100%
c [treelook-8] scheduling used 270423 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 2475207 penalty 2 = 2 + 0 boost 1
c [treelook-8] used 2477821 steps
c [treelook-8] 4776 literals remain 92%
c [treelook-8] 2580 variables remain to probed next time 100%
c [treelook-8] removed 0 variables, found 14215 hbrs
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 424 transitive binary clauses
c [bca-20] limit of 10000000 steps and 26902 added (scaled 2)
c [bca-20] 3771 out of 5166 literals actually usable 73%
c [bca-20] added 6 blocked clauses in 90072 steps
c [sort-queue-24] sorted 603 enqueued variables after 1364758 conflicts
c [score-dist-24] active 1979 (77%), one 0 (0%), zero 603 (23%)
c [score-dist-24] max exp 522, different 22 (4%)
c [score-dist-24] median active exp 514, avg 512.4
c [simplification-24] removed 0 variables 0.0% (2582 remain 1%)
c [simplification-24] removed 0 irredundant clauses 0.0% (13120 remain 1%)
c [simplification-24] maximum reduction of 0% = max (0%, 0%)
c [simplification-24] full geometric conflict interval increment 525000
c [simplification-24] new conflict interval 1050000
c [simplification-24] penalized conflict interval 1050000 = 1 * 1050000
c [simplification-24] hard conflict limit 2939758 (soft 2414758 + delta 525000)
c [simplification-24] new conflict limit 2414758 (hard 2939758)
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 -  298.3    2582    13120   1366895   40236    474 35081   25    31   19  82%   1024   -0   22   25   90%
c -  308.9    2582    13120   1425504   40711    475 35081   20    25   24  80%   1024   -3   20   23   87%
c -  320.0    2582    13120   1485134   41194    475 35081   20    24   24  82%   1024   -4   22   23   97%
c -  330.8    2582    13120   1543188   42294    477 35081   26    33   24  81%   1024    3   27   24  109%
c -  341.0    2582    13120   1598534   42881    477 35081   37    43   24  86%   1024   10   36   28  128%
c -  352.1    2582    13120   1656285   41875    478 35081   35    42   24  83%   1024    9   38   27  141%
c -  363.7    2582    13120   1717247   43158    478 35081   36    43   34  83%   1024   10   41   28  149%
c -  375.4    2582    13120   1778039   44152    478 35081   24    33   34  74%   1024   -2   28   28  101%
c -  387.1    2582    13120   1841134   44094    479 35081   23    30   34  75%   1024   -4   18   27   68%
c -  399.1    2582    13120   1906632   45802    479 35081   28    35   34  80%   1024    1   41   27  154%
c -  410.8    2582    13120   1970776   47480    479 35081   23    30   34  77%   1024   -4   21   27   78%
c -  422.0    2582    13120   2030440   47873    480 35081   27    31   35  85%   1024   -4   33   29  114%
c -  434.4    2582    13120   2099093   48086    480 35081   24    29   34  84%   1024   -3   27   26  105%
c -  446.3    2582    13120   2164709   48339    482 35082   30    35   35  86%   1024    3   26   26   99%
c -  459.1    2582    13120   2229802   49097    483 35082   26    32   35  81%   1024   -1   22   28   77%
c -  472.7    2582    13120   2299497   48400    488 35083   29    34   35  86%   1024    3   35   26  132%
c -  486.6    2582    13120   2373884   50275    495 35085   25    29   35  85%   1024    1   31   24  131%
c 
c [simplification-25] limit 2414758 conflicts (hard 2939758) hit after 2422105 conflicts
c [quatres-10] found 1224 quaternary clauses 13% in total
c [quatres-10-2] added 40 single-self-subsuming ternary resolvents
c [quatres-10-2] added 10 quaternary resolvents
c [ternres-19] limit 187864517 with penalty 0 = 0 + 0
c [ternres-19] all 2582 free variables schedulable
c [ternres-19] 22 ternary resolvents (4 bin, 18 trn)
c [ternres-19] fully completed ternary resolution
c [gauss-6] limit 2348306 penalty 4 = 4 + 0
c [gauss-6] extracted 9 xors of average arity 3.0
c [gauss-6] connected 27 occurrences of 9 variables (average 3.0)
c [gauss-6] limit 2348306 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 763 sched 30%, 20 failed, 0 lifted, 2078 hbrs
c [decomp-78] removed 43 variables
c [basicprobe-8-1] 749 sched 30%, 9 failed, 0 lifted, 329 hbrs
c [decomp-79] removed 12 variables
c [basicprobe-8-2] 749 sched 30%, 5 failed, 0 lifted, 77 hbrs
c [decomp-80] removed 5 variables
c [basicprobe-8-3] 747 sched 30%, 3 failed, 0 lifted, 228 hbrs
c [decomp-81] removed 3 variables
c [basicprobe-8-4] 745 sched 30%, 2 failed, 0 lifted, 131 hbrs
c [decomp-82] removed 4 variables
c [basicprobe-8-5] 743 sched 30%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-8-6] 743 sched 30%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-8-7] 743 sched 30%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-8-8] 743 sched 30%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-8-8] round limit 8 hit
c [basicprobe-8-8] 39 units = 39 failed (100%) + 0 lifted (0%)
c [basicprobe-8-8] removed 67 variables, found 2857 hbrs
c [bate-6] eliminated 33 asymmetric tautologies during probing
c [unhide-19] limit 2500000 with penalty 3 = 3 + 0
c [unhide-19-64] 0 units, 0 failed, 34367 tauts, 0 hbrs, 68649 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 383 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 2515 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 7 blocked clauses
c [block-6] 7 < 1/100 * 12523 = 125 considered unsuccessful
c [bca-21] limit of 10000000 steps and 25697 added (scaled 2)
c [bca-21] 3671 out of 5032 literals actually usable 73%
c [bca-21] added 7 blocked clauses in 60656 steps
c [sort-queue-25] sorted 524 enqueued variables after 2422105 conflicts
c [score-dist-25] active 1991 (79%), one 0 (0%), zero 524 (21%)
c [score-dist-25] max exp 522, different 22 (4%)
c [score-dist-25] median active exp 514, avg 512.9
c [simplification-25] removed 67 variables 2.6% (2515 remain 1%)
c [simplification-25] removed 604 irredundant clauses 4.6% (12516 remain 1%)
c [simplification-25] maximum reduction of 5% = max (3%, 5%)
c [simplification-25] large reduction 5% >= 5% limit
c [simplification-25] next conflict interval 24221 = min (2422105/100, 1050000)
c [simplification-25] penalized conflict interval 24221 = 1 * 24221
c [simplification-25] hard conflict limit 2458436 (soft 2446326 + delta 12110)
c [simplification-25] new conflict limit 2446326 (hard 2458436)
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  499.9    2514    12516   2425503   53486    499 32293   22    26   27  85%   1024   -1   14   22   63%
c 
c [simplification-26] limit 2446326 conflicts (hard 2458436) hit after 2458436 conflicts
c [ternres-20] limit 190591322 with penalty 0 = 0 + 0
c [ternres-20] all 2511 free variables schedulable
c [ternres-20] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-86] removed 4 variables
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 323 transitive binary clauses
c [cce-14] limit of 238239153 steps penalty 2 = 2 + 0
c [cce-14-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-14-1] eliminated 4 clauses out of 627 (1%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 5 large clauses in 2515798 steps
c [cce-14-1] allowing another 1257899 steps for small clauses
c [cce-14-1] scheduling 9888 clauses = 8186 binary + 1702 ternary
c [cce-14-1] tried to eliminate 9888 small clauses 100%
c [cce-14-1] eliminated 195 binary clauses 2%
c [cce-14-1] eliminated 13 ternary clauses 1%
c [cce-14-1] eliminated 208 small clauses 2%
c [cce-14-1] eliminated 208 small clauses in 26909522 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 213 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1248028 steps for small clauses
c [cce-14-2] scheduling 9680 clauses = 7991 binary + 1689 ternary
c [cce-14-2] tried to eliminate 9680 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 213 covered clauses in TOTAL during 2 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 2511 variables 100%
c [elim-21] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 46 variables 2% in round 1 in 675377 steps
c [elim-21-1] backward subsumption/strengthening limit 675300
c [elim-21-1-1] backward checking 300 touched variables 12%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 25058 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 46 = 2% variables out of 2511 scheduled
c [bca-22] limit of 10000000 steps and 25124 added (scaled 2)
c [bca-22] 3543 out of 4932 literals actually usable 72%
c [bca-22] added 3 blocked clauses in 62903 steps
c [sweep-16] limit 7147174 penalty 3 = 3 + 0
c [sweep-16-1] 258 pos 21.2% + 960 neg 78.8% = 1218 sched 49.4% ret 1247
c [sweep-16-1] 7276655 steps 154 queries 19.73 avg class size
c [sweep-16-1] 3797 decisions 152 SAT calls 68.14 avg env size
c [sweep-16-1] 509 variables remain 21% (1954 retained 79%)
c [decomp-87] removed 3 variables
c [sweep-16-1] removed 3 vars (0 failed, 1 eqs, 1 impls)
c [sweep-16] removed 3 vars in TOTAL (1 rounds, 153 queries)
c [sort-queue-26] sorted 475 enqueued variables after 2458436 conflicts
c [score-dist-26] active 1987 (81%), one 0 (0%), zero 475 (19%)
c [score-dist-26] max exp 522, different 22 (4%)
c [score-dist-26] median active exp 514, avg 512.9
c [simplification-26] removed 49 variables 2.0% (2462 remain 1%)
c [simplification-26] removed 303 irredundant clauses 2.4% (12213 remain 1%)
c [simplification-26] maximum reduction of 2% = max (2%, 2%)
c [simplification-26] geometric conflict interval increment 350000 = 1050000 / 3
c [simplification-26] conflict interval soft limit 1000000 reached
c [simplification-26] new conflict interval 1000000
c [simplification-26] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-26] hard conflict limit 3958436 (soft 3458436 + delta 500000)
c [simplification-26] new conflict limit 3458436 (hard 3958436)
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 -  518.0    2462    12213   2519111   52510    402 29637   23    29   30  79%  -8027    1   25   23  108%
c -  529.6    2462    12213   2580927   53877    402 29638   27    33   30  81%  -2500   -0   22   27   82%
c -  540.6    2462    12213   2644940   54383    403 29638   28    32   30  86%   -303    1   21   26   81%
c -  551.9    2462    12213   2708491   53202    404 29638   31    40   30  78%    521    6   37   27  135%
c -  563.6    2462    12213   2769964   54304    404 29638   41    51   30  81%    827    7   33   35   93%
c -  575.7    2462    12213   2833489   52720    404 29638   28    37   43  75%    949   -5   21   32   66%
c -  588.0    2462    12213   2901836   53135    404 29638   23    30   42  76%    998   -7   22   28   77%
c -  598.9    2462    12213   2969891   55588    405 29638   34    41   43  83%   1015    8   39   27  142%
c -  611.8    2462    12213   3039272   56522    405 29638   27    31   43  85%   1021   -4   24   28   86%
c -  625.4    2462    12213   3111543   56627    407 29639   30    36   43  84%   1023    4   40   26  155%
c i  640.1    2461    12213   3189039  112051    438 29652   24    29   67  82%   1024   -2   18   25   73%
c -  640.8    2446    12213   3192433   56750    439 29652   26    33   43  81% -10045    2   23   25   92%
c -  654.5    2446    12213   3269793   59280    446 29654   26    30   44  86%  -2511    0   29   25  116%
c -  667.3    2446    12213   3341249   59974    453 29654   38    50   45  77%   -164   18   51   27  190%
c -  680.6    2446    12213   3409387   58222    453 29654   39    47   44  83%    604    6   39   34  117%
c -  695.2    2446    12213   3482444   58199    453 29654   23    30   44  79%    886   -9   21   30   69%
c 
c [simplification-27] limit 3458436 conflicts (hard 3958436) hit after 3507555 conflicts
c [decomp-88] removed 17 variables
c [simpleprobe-9] all 2445 free variables schedulable
c [simpleprobe-9] limit 100000000 penalty 1 = 1 + 0
c [decomp-89] removed 2 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 2 variables, found 1353 hbrs, 2 units
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 578 transitive binary clauses
c [transred-23] found 2 units
c [bca-23] limit of 10000000 steps and 24778 added (scaled 2)
c [bca-23] 3465 out of 4880 literals actually usable 71%
c [bca-23] added 2 blocked clauses in 79181 steps
c [sort-queue-27] sorted 436 enqueued variables after 3507555 conflicts
c [score-dist-27] active 2003 (82%), one 0 (0%), zero 436 (18%)
c [score-dist-27] max exp 523, different 23 (4%)
c [score-dist-27] median active exp 514, avg 513.2
c [simplification-27] removed 7 variables 0.3% (2439 remain 1%)
c [simplification-27] removed 159 irredundant clauses 1.3% (12054 remain 1%)
c [simplification-27] maximum reduction of 1% = max (0%, 1%)
c [simplification-27] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-27] conflict interval soft limit 1000000 reached
c [simplification-27] new conflict interval 1000000
c [simplification-27] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-27] hard conflict limit 5007555 (soft 4507555 + delta 500000)
c [simplification-27] new conflict limit 4507555 (hard 5007555)
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 -  709.4    2439    12054   3558867   52592    367 30230   24    32   24  74%    981   -5   25   29   87%
c -  723.7    2439    12054   3634983   54944    367 30230   28    33   33  85%   1011   -2   22   28   80%
c -  739.4    2439    12054   3717004   56022    376 30231   28    34   33  84%   1020    2   38   26  145%
c i  748.8    2438    12054   3768584   94000    379 30234   22    27   49  84%   1022   -5   15   26   59%
c -  755.5    2438    12054   3802332   57066    379 30234   26    31   33  86%  -4474    0   32   25  126%
c i  757.8    2437    12054   3815575   66123    389 30241   20    25   40  79%  -3468   -5   15   25   60%
c i  759.2    2143    12054   3824382   72129    400 30249   20    24   40  81%  -3555   -5   15   24   62%
c i  760.8    2142    12054   3833476   78417    406 30255   23    28   43  82%  -3083   -1   20   24   81%
c i  762.2    2141    12054   3842248   84214    417 30261   23    29   44  82%  -2695   -1   18   24   74%
c i  763.3    2140    12054   3847976   88157    421 30266   21    25   44  83%  -2511   -4   13   24   53%
c i  763.6    2138    12054   3850155   89663    430 30270   19    23   44  82%  -2473   -6   12   24   52%
c i  764.0    2137    12054   3852557   91433    431 30272   18    22   48  82%  -2387   -7   14   24   58%
c i  767.9    2134    12054   3875247  108605    432 30274   22    27   50  81%  -1419   -3   18   24   74%
c i  768.0    2034    12054   3875681  108916    435 30274   22    27   50  81%  -1525   -3   21   24   85%
c i  769.5    2033    12054   3883589  114296    439 30276   22    26   50  84%  -1450   -4   17   24   70%
c i  769.5    1826    12054   3883677  114330    441 30277   22    26   50  84%  -1457   -4   19   24   80%
c i  769.5    1706    12054   3883685  114332    443 30277   22    26   50  84%  -1457   -4   19   24   78%
c i  769.5    1692    12054   3883691  114332    444 30278   22    26   50  84%  -1458   -4   18   24   76%
c i  769.5    1682    12054   3883723  114343    446 30279   22    26   50  84%  -1460   -4   18   24   73%
c i  769.5    1664    12054   3883729  114342    446 30281   22    26   50  84%  -1460   -4   17   24   72%
c i  769.5    1662    12054   3883731  114343    446 30281   22    26   50  84%  -1460   -4   17   24   71%
c i  769.6    1647    12054   3883876  114409    450 30285   21    26   50  84%  -1469   -4   17   24   72%
c i  769.6    1218    12054   3883877  114409    450 30285   21    26   50  84%  -1469   -4   17   24   72%
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  769.6    1150    12054   3883878  114409    450 30285   21    26   50  84%  -1470   -4   17   24   71%
c i  769.6    1099    12054   3883879  114409    450 30285   21    26   50  84%  -1470   -4   17   24   71%
c 0  769.6     947    12054   3883879  114409    450 30285   21    26   50  84%  -1470   -4   17   24   71%
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: 718 basic ate = 610 trn 85% + 108 lrg 15% in 6 updates
c bcas: 23 count, 342 added (729 skipped), 1069912 steps
c bkwd: tried 282182 clauses, 563741 lits, 2.00 lits/clause
c bkwd: checked 6422661 occs, 22.76 occs/clause, 11.39 occs/lit
c bkwd: subsumed 51 binary, 242 ternary, 233 large
c bkwd: strengthened 39 binary, 4 ternary (100% self), 485 large (0% self)
c blkd: 6 bces, 1358 removed, 993544 resolutions, 2709652 steps
c blkd: 2667 blocking literals 1%, 15 pure
c bump: 3882651 bumped seen, 496734809 lits 127.9 on average
c card: 6 count, 0 units, 6388 am1, 15128196 steps
c card: 44 rescheduled, 430 eliminated, 3649 resolved, 72105 subsumed
c card: 22185 at-most-one constraints found, average size 4.35
c card: 22185 at-most-one constraints used 100%, average size 4.35
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 14 cces, 13650 eliminated, 12213 ate 89%, 1437 abce 11%
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: 3353807 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 205 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 89 decompositions, 67261 equivalent 30%
c deco: 7662 decision-only clauses 0%, 67% reduction
c decs: 6284390 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 21 elims, 21913 eliminated 10%, 111 pure 1%
c elms: 63 rounds, 3.0 rounds/bve
c elms: 20889 small 95%, 898 large 4%
c elms: 82188 tried small, 20889 succeeded 25%, 61299 failed 75%
c elms: 6351 subsumed, 9594 strengthened, 745 blocked
c elms: 5067151 copies, 4578784 resolutions, 2652842 ipos
c elms: 975939 subchks, 633703 strchks
c gaus: 6 extractions, 226 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9080990 steps, 4540495 extr 50%, 4328 elim 0%
c glue: 28.5 orig avg, 28.5 real avg, 5.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 344945 = 39891 simple 12% + 284820 trn 83% + 20234 lrg 6%, 2725 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3882651 clauses, 53.3 length
c lrnd: 206876022 lits = 303358989 orig - 96482967 removed 32%
c lrnd: 1351562 uips 35%, 2372951 flips 61%
c mins: 3871715 mins 100%, 151 bin 0%, 2658 size 0%
c mins: 411986066 poisoned searches, 53282691 hits, 13% hit rate
c mins: 654030352 used twice searches, 73728153 hits, 11% hit rate
c move: moved 13248, 9820 bin 74%, 3428 trn 26%
c otfs: 3402 driving 28%, 8826 restarting 72%
c otfs: str 12228, 12189 red 100%, 39 irr 0%
c otfs: str 12228, 0 bin 0%, 34 trn 0%, 12194 lrg 100%
c otfs: sub 71, 71 red 100%, 0 irr 0%
c otfs: sub 71, 0 bin 0%, 0 trn 0%, 71 lrg 100%
c phas: 12 computed, 26324 set, 2 pos (0%), 26322 neg (100%)
c prbs: 8 basic, 44444 probed, 2196 failed, 242 lifted
c prbs: 9 simple, 387029 probed, 1464 failed, 26225 eqs
c prbs: 8 treelook, 601 probed, 25 failed, 0 lifted
c prom: 131979 locked 7% out of 1917410 tried
c prps: 1245516756 props, 194 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 10 count, 25 quat, 41 self1, 0 self2, 14 dup
c queu: 27 sorted, 6284390 next (178004 steps 0.03)
c queu: 497078491 enq (640322272 steps 1.29), 496734809 deq 100%
c redc: 1897 clauses 4%, 53227 tried 1%, 3 sat 0%
c redc: 5449 lits 1%, 590525 tried 0%, 3 sat 0%
c redc: 149 times jump level reduced, 10.1 levels on average
c reds: 64 count, 60685.6 conflicts per reduce
c reds: 0 memlim 0%, 64 arith 100%
c reds: 2608171 collected 92%, 225372 retired 8%
c rmbd: 7701 removed, 2191 red 28%
c rsts: 14528 restarts 93%, 1100 skipped 7%
c rsts: 1100 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: 27 count, 27 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3882651 count (3671037 tried 0.9), 828744 sub out of 3881701 (21.4%)
c swps: 16 count, 21 rounds, 4691 queries (223.4/round)
c swps: 4551 sat calls, 82 unsat (0.5% success rate)
c swps: 34791 decisions 7.6, 2174 conflicts 0.5
c swps; 72.1 avg class size, 33.4 avg environment size
c swps: 0 failed, 253 impls, 199 equivs
c swp0: 1558 type 0 queries, 689 unsat (44.2%), 1504 sat (96.5%)
c swp1: 3133 type 1 queries, 1611 unsat (51.4%), 2988 sat (95.4%)
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: 20334678 calls to obtain time
c tops: 136087 fixed 60%, 48 its, 80914.15 confs/it
c trds: 23 transitive reductions, 9409 removed, 105 failed
c trds: 60201 nodes, 163509 edges, 46008572 steps
c trim: 11684259 words, 44.6 MB
c trnr: 20 count, 5 bin, 1159 trn, 23991755 steps
c unhd: 19 count, 64 rounds, 24569791 steps
c unhd: 3142 non-trivial sccs of average size 2.2
c unhd: 100 units, 97 bin, 3 trn, 0 lrg
c unhd: 3206 failed, 3160 stamp, 0 lits, 29 bin, 8 trn, 0 lrg
c unhd: 134826 tauts, 6997 bin 5%, 2054 trn 2%, 30875 lrg 23%
c unhd: 134826 tauts, 94900 stamp 70%, 105210 red 78%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 318800 str, 97 bin 0%, 1304 trn 0%, 317399 lrg 100%, 313579 red 98%
c vars: 947 remaining 0% and 225261 removed 100% out of 226208
c vars: 136087 fixed 60%, 21913 eliminated 10%, 67261 equivalent 30%
c vsts: 32372405383 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 26.4 search visits per propagation, 8278.6 per conflict
c wchs: 7326634779 pushed, 15866190 enlarged, 321 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3881726       2608171        225372      78657311      28124785       1727330
c 
c  0 0         18311   0      1918   0         0   0  25037389  32   6651540  24    161747   9     0.4
c  1 5         18258   0      8655   0      4676   2   6288701   8   1930270   7     59073   3     0.2
c  2 6         90245   2     52795   2     17779   8  11062825  14<  3674885  13    176588  10     0.7
c  3 9        290764   7    191088   7     40170  18  12756194  16   4717889  17<   312341  18     1.9
c  4 14       716081  18    481572  18     68520  30< 12840298  16   5239458  19    490000  28<    5.2
c  5 21      1097426  28<   748595  29<    53945  24   6195025   8   3223179  11    343379  20     7.2
c  6 30      1027982  26    705213  27     28323  13   2977886   4   1811160   6    136640   8     7.2
c  7 41       490142  13    339388  13      9984   4   1090034   1    677334   2     37161   2     6.6
c  8 54       108046   3     73423   3      1837   1    244936   0    147536   1      7398   0     3.2
c  9 69        11139   0      5166   0       133   0     92387   0     23743   0      1600   0     1.6
c 10 86         5384   0       358   0         5   0     48745   0     17698   0       837   0     2.5
c 11 126        7601   0         0   0         0   0     20250   0      8973   0       266   0     2.8
c 12 230         347   0         0   0         0   0      2641   0      1120   0       300   0     0.4
c 
c avg                  5.2           5.2           4.3           2.3           2.8           3.6
c std                  1.4           1.3           1.4           2.0           2.1           1.7
c 
c   54.180   7% bump
c   15.803   2% cce
c   12.333   2% probe
c    9.174   1% unhide
c    4.774   1% elim
c    3.665   0% decide
c 
c    8.019 < 1% rest (below)
c 
c    3.349   0% sweep
c    2.661   0% transred
c    0.744   0% bca
c    0.383   0% block
c    0.368   0% gauss
c    0.301   0% card
c    0.164   0% ternres
c    0.050   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    2.103   0% preprocessing     4%
c   50.878   7% inprocessing     96%
c ==================================
c   52.981   7% simplifying
c  716.592  93% search
c ==================================
c  769.576 100% all
c 
c       3883879 conflicts,        5046.8 confs/sec
c           370 ternaries,       10497.0 confs/ternary
c           200 binaries,        19419.4 confs/binary
c            48 iterations,      80914.1 confs/iteration
c 
c            64 reductions,          0.1 redus/sec,  60685.6 confs/reduction
c         14528 restarts,           18.9 rests/sec,    267.3 confs/restart
c       6284390 decisions,        8166.0 decis/sec,      1.6 decis/conflict
c    1245516756 propagations,  1618444.5 props/sec,    198.2 props/decision
c 
c 769.6 seconds, 75.4 MB
c launch: done
