c launch: /data/cnf/sc2014/app/slp-synthesis-aes-top28.cnf.bz2
c host: atom31
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/slp-synthesis-aes-top28.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/slp-synthesis-aes-top28.cnf.bz2
c no embedded options
c found 'p cnf 88763 282870' header
c read 88763 variables, 282870 clauses, 691774 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=5
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 85392 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   85392   265956         0       0      0     0    0     0   17   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 56 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 56 out of 56 constraints (100%) meet size limits
c [card-1] found 1 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 4905 variables
c [simpleprobe-1] all 83858 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 800 variables
c [simpleprobe-1] 661 variables remain 1% (82397 retained 99%)
c [simpleprobe-1] removed 800 variables, found 6295 hbrs, 84 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 0 failed, 318 tauts, 0 hbrs, 105 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 83057 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 60028 variables 72% in round 1 in 13542442 steps
c [elim-1-1] backward subsumption/strengthening limit 6457558
c [elim-1-1-1] backward checking 60035 touched variables 72%
c [elim-1-1-1] incomplete backward checking 58202 remain 97%
c [elim-1-1] subsumed 860 and strengthened 1903 clauses in 6457858 steps
c [elim-1] incomplete 1714 not tried 2% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 60028 = 72% variables out of 83057 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 126170 negative 95.8% of 131734 except 5564 4.2%
c [phase-count-1] 124057 positive 94.2% of 131734 except 7677 5.8%
c [phase-1] phase bias: 3919 positive 17%, 19110 negative 83%
c [sort-queue-1] sorted 23029 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 23029 (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 62363 variables 73.0% (23029 remain 27%)
c [simplification-1] removed 134222 irredundant clauses 50.5% (131734 remain 50%)
c [simplification-1] maximum reduction of 73% = max (73%, 50%)
c [simplification-1] large reduction 73% >= 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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 37 variables
c [simpleprobe-2] 206 schedulable variables 1%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 46 variables
c [simpleprobe-2] 564 variables remain 2% (22382 retained 98%)
c [simpleprobe-2] removed 46 variables, found 379 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 26727 literals 58%
c [treelook-1] scheduling used 300009 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300426 steps
c [treelook-1] 26696 literals remain 58%
c [treelook-1] 18483 variables remain to probed next time 81%
c [decomp-5] removed 1 variables
c [treelook-1] removed 1 variables, found 360 hbrs
c [basicprobe-1] limit 1052088 based on 131511 irredundant clauses
c [basicprobe-1-0] 6814 probes remain 30% after last round
c [basicprobe-1-0] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3 variables, found 1129 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 1 failed, 44 tauts, 0 hbrs, 1739 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 22941 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 558 not tried 2% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 277 = 1% variables out of 22941 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 124016 negative 95.5% of 129819 except 5803 4.5%
c [phase-count-2] 122299 positive 94.2% of 129819 except 7520 5.8%
c [phase-2] phase bias: 6 positive 21%, 22 negative 79%
c [sort-queue-2] sorted 19021 enqueued variables after 1001 conflicts
c [score-dist-2] active 3643 (16%), one 0 (0%), zero 19021 (84%)
c [score-dist-2] max exp 761, different 169 (22%)
c [score-dist-2] median active exp 527, avg 593.2
c [simplification-2] removed 365 variables 1.6% (22664 remain 27%)
c [simplification-2] removed 1915 irredundant clauses 1.5% (129819 remain 49%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17667 (soft 7667 + delta 10000)
c [simplification-2] new conflict limit 7667 (hard 17667)
c 
c [simplification-3] limit 7667 conflicts (hard 17667) hit after 7668 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 175 at-most-one constraints of average size 3.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 175 out of 175 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 104 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 23479 literals 52%
c [treelook-2] scheduling used 300005 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 316616 steps
c [treelook-2] 23456 literals remain 52%
c [treelook-2] 16383 variables remain to probed next time 73%
c [decomp-7] removed 1 variables
c [treelook-2] removed 3 variables, found 552 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 1 failed, 69 tauts, 0 hbrs, 1545 literals
c [elim-3] 558 variables 2% will be scheduled this time
c [elim-3] scheduled 558 variables 2%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 236 not tried 1% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 558 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 123531 negative 95.6% of 129242 except 5711 4.4%
c [phase-count-3] 121808 positive 94.2% of 129242 except 7434 5.8%
c [phase-3] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-3] sorted 18434 enqueued variables after 7668 conflicts
c [score-dist-3] active 4121 (18%), one 1697 (8%), zero 16737 (74%)
c [score-dist-3] max exp 994, different 352 (35%)
c [score-dist-3] median active exp 917, avg 838.2
c [simplification-3] removed 109 variables 0.5% (22555 remain 26%)
c [simplification-3] removed 575 irredundant clauses 0.4% (129242 remain 49%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 26666
c [simplification-3] penalized conflict interval 26666 = 1 * 26666
c [simplification-3] hard conflict limit 47667 (soft 34334 + delta 13333)
c [simplification-3] new conflict limit 34334 (hard 47667)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.5   22554   129242      9616    8609    312  3563    8    45   17  19%    126   41   10    1  796%
c 
c [simplification-4] limit of 189 binary hit after 189 binaries
c [decomp-8] removed 3 variables
c [basicprobe-2] limit 3331551 penalty 0 = 0 + 0
c [basicprobe-2-0] 2071 probes remain 9% after last round
c [basicprobe-2-0] 38 units = 38 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 42 variables, found 3113 hbrs
c [unhide-4] limit 133262 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 4 failed, 82 tauts, 0 hbrs, 3073 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 22505 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 710 variables 3% in round 1 in 63786595 steps
c [elim-4-1] backward subsumption/strengthening limit 63786500
c [elim-4-1-1] backward checking 3371 touched variables 15%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 54 and strengthened 163 clauses in 7102485 steps
c [elim-4-1] rescheduled 161 variables 1% by backward subsumption
c [elim-4-2] eliminated 8 variables 0% in round 2 in 986172 steps
c [elim-4-2] backward subsumption/strengthening limit 986100
c [elim-4-2-1] backward checking 90 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 1 and strengthened 10 clauses in 352645 steps
c [elim-4-2] rescheduled 22 variables 0% by backward subsumption
c [elim-4-3] eliminated 1 variables 0% in round 3 in 483788 steps
c [elim-4-3] backward subsumption/strengthening limit 483700
c [elim-4-3-1] backward checking 16 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 132354 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 745 = 3% variables out of 22505 scheduled
c [phase-count-4] 118123 negative 95.2% of 124123 except 6000 4.8%
c [phase-count-4] 116804 positive 94.1% of 124123 except 7319 5.9%
c [phase-4] phase bias: 3 positive 15%, 17 negative 85%
c [sort-queue-4] sorted 18244 enqueued variables after 18357 conflicts
c [score-dist-4] active 3516 (16%), one 3774 (17%), zero 14470 (66%)
c [score-dist-4] max exp 778, different 359 (46%)
c [score-dist-4] median active exp 713, avg 586.5
c [simplification-4] removed 794 variables 3.5% (21760 remain 25%)
c [simplification-4] removed 5119 irredundant clauses 4.0% (124123 remain 47%)
c [simplification-4] maximum reduction of 4% = max (4%, 4%)
c [simplification-4] forced so keeping old conflict interval 26666
c [simplification-4] conflict limit remains at 34334 (hard 47667)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.2   21759   124123     22533   19979    478  5855   10    54   18  19%    161   42   10    3  350%
c i   10.0   21758   124123     26875   23651    644  6173   10    52   18  19%     27   38    9    3  268%
c i   10.2   21757   124123     28382   24877    690  6325   10    47   18  21%     -4   31    8    3  242%
c i   10.2   21741   124123     28435   24906    694  6338   10    46   18  21%     -5   31    8    3  228%
c i   10.3   21737   124123     28701   25107    708  6375   10    47   18  21%     -9   31    8    3  233%
c i   10.3   21732   124123     28702   25107    708  6375   10    47   18  21%     -9   31    8    3  232%
c i   10.3   21723   124123     28706   25108    708  6377   10    47   18  21%    -10   31    8    3  229%
c 
c [simplification-5] limit 34346 conflicts (hard 47667) hit after 34346 conflicts
c [quatres-1] found 43283 quaternary clauses 74% in total
c [quatres-1-2] added 65 single-self-subsuming ternary resolvents
c [quatres-1-2] added 34283 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 21704 free variables schedulable
c [ternres-1] 15807 ternary resolvents (65 bin, 15742 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 13658 xors of average arity 2.9
c [gauss-1] connected 39649 occurrences of 2886 variables (average 13.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [decomp-9] removed 548 variables
c [gauss-1] exported 0 unary, 26 binary and 0 ternary equations
c [simpleprobe-3] 518 schedulable variables 2%
c [simpleprobe-3] limit 6019283 penalty 0 = 0 + 0
c [decomp-11] removed 15 variables
c [simpleprobe-3] 848 variables remain 4% (20293 retained 96%)
c [simpleprobe-3] removed 15 variables, found 813 hbrs, 3 units
c [unhide-5] limit 300964 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 4 failed, 85 tauts, 0 hbrs, 2768 literals
c [transred-1] limit 1504820 with penalty 0 = 0 + 0
c [transred-1] removed 76 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 21137 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 11646 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 42
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 39
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 38
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 37
c [cce-1-1] eliminated 6 clauses out of 7 (86%) of length 36
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 35
c [cce-1-1] eliminated 7 clauses out of 8 (88%) of length 34
c [cce-1-1] eliminated 5 clauses out of 6 (83%) of length 33
c [cce-1-1] eliminated 6 clauses out of 7 (86%) of length 32
c [cce-1-1] eliminated 10 clauses out of 12 (83%) of length 31
c [cce-1-1] eliminated 6 clauses out of 10 (60%) of length 30
c [cce-1-1] eliminated 6 clauses out of 10 (60%) of length 29
c [cce-1-1] eliminated 10 clauses out of 14 (71%) of length 28
c [cce-1-1] eliminated 7 clauses out of 12 (58%) of length 27
c [cce-1-1] eliminated 5 clauses out of 25 (20%) of length 26
c [cce-1-1] eliminated 6 clauses out of 20 (30%) of length 25
c [cce-1-1] eliminated 3 clauses out of 21 (14%) of length 24
c [cce-1-1] eliminated 3 clauses out of 34 (9%) of length 23
c [cce-1-1] eliminated 5 clauses out of 45 (11%) of length 22
c [cce-1-1] eliminated 3 clauses out of 43 (7%) of length 21
c [cce-1-1] eliminated 3 clauses out of 40 (8%) of length 20
c [cce-1-1] eliminated 2 clauses out of 49 (4%) of length 19
c [cce-1-1] eliminated 4 clauses out of 45 (9%) of length 18
c [cce-1-1] eliminated 4 clauses out of 61 (7%) of length 17
c [cce-1-1] eliminated 7 clauses out of 62 (11%) of length 16
c [cce-1-1] eliminated 11 clauses out of 88 (12%) of length 15
c [cce-1-1] eliminated 10 clauses out of 89 (11%) of length 14
c [cce-1-1] eliminated 15 clauses out of 94 (16%) of length 13
c [cce-1-1] eliminated 20 clauses out of 138 (14%) of length 12
c [cce-1-1] eliminated 44 clauses out of 2735 (2%) of length 11
c [cce-1-1] eliminated 46 clauses out of 354 (13%) of length 10
c [cce-1-1] eliminated 60 clauses out of 2041 (3%) of length 9
c [cce-1-1] eliminated 160 clauses out of 961 (17%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 488 large clauses in 30000043 steps
c [cce-1-1] allowing another 15000021 steps for small clauses
c [cce-1-1] scheduling 40260 clauses = 18753 binary + 21507 ternary
c [cce-1-1] tried to eliminate 3490 small clauses 9%
c [cce-1-1] eliminated 154 binary clauses 1%
c [cce-1-1] eliminated 35 ternary clauses 0%
c [cce-1-1] eliminated 189 small clauses 0%
c [cce-1-1] eliminated 189 small clauses in 30000063 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 677 covered clauses in round 1
c [cce-1] eliminated 677 covered clauses in TOTAL during 1 rounds
c [cce-1] 677 < 1/100 * 107643 = 1076 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 21137 variables 100%
c [elim-5] limit of 30096418 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 196 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 382 = 2% variables out of 21137 scheduled
c [bca-1] limit of 10000000 steps and 213310 added (scaled 2)
c [bca-1] 16121 out of 41512 literals actually usable 39%
c [bca-1] added 414 blocked clauses in 94133 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 6388 pos 30.8% + 14367 neg 69.2% = 20755 sched 100.0% ret 0
c [sweep-1-1] 1122690 steps 73 queries 2541.86 avg class size
c [sweep-1-1] 1414 decisions 70 SAT calls 55.31 avg env size
c [sweep-1-1] 18562 variables remain 89% (2188 retained 11%)
c [decomp-12] removed 87 variables
c [sweep-1-1] removed 87 vars (0 failed, 2 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 87 vars in TOTAL (1 rounds, 72 queries)
c [phase-count-5] 100808 negative 95.3% of 105772 except 4964 4.7%
c [phase-count-5] 98818 positive 93.4% of 105772 except 6954 6.6%
c [phase-5] phase bias: 533 positive 91%, 54 negative 9%
c [sort-queue-5] sorted 13889 enqueued variables after 34346 conflicts
c [score-dist-5] active 6779 (33%), one 3436 (17%), zero 10453 (51%)
c [score-dist-5] max exp 948, different 513 (54%)
c [score-dist-5] median active exp 800, avg 715.7
c [simplification-5] removed 1036 variables 4.8% (20668 remain 24%)
c [simplification-5] removed 18351 irredundant clauses 14.8% (105772 remain 40%)
c [simplification-5] maximum reduction of 15% = max (5%, 15%)
c [simplification-5] large reduction 15% >= 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 46346 (soft 36346 + delta 10000)
c [simplification-5] new conflict limit 36346 (hard 46346)
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   14.3   20667   105772     34716   56416  23383  8404   10    48   23  20%     50   29   10    4  247%
c i   14.4   20666   105772     35436   57010  23430  8463   10    48   23  20%     13   29   10    4  235%
c i   14.5   20657   105772     35738   57233  23442  8508    9    47   23  20%      3   29    8    4  208%
c i   14.6   20656   105772     36110   57536  23478  8529    9    47   23  20%     -6   28    8    4  204%
c i   14.8   20645   105772     37538   58768  23553  8603    9    47   23  20%    -12   27    9    4  208%
c i   14.9   20634   105772     38077   59246  23567  8631    9    49   23  19%    -17   29    9    4  210%
c 
c [simplification-6] limit 36346 conflicts (hard 46346) hit after 40741 conflicts
c [quatres-2] found 73026 quaternary clauses 84% in total
c [quatres-2-1] removed 11 duplicate quaternary clauses
c [quatres-2-2] added 380 single-self-subsuming ternary resolvents
c [quatres-2-2] added 24257 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 20621 free variables schedulable
c [ternres-2] 233 ternary resolvents (0 bin, 233 trn)
c [ternres-2] 9781 variables remain 47% (10840 retained 53%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 154 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 154 out of 154 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 13946 xors of average arity 2.9
c [gauss-2] connected 40729 occurrences of 2608 variables (average 15.6)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 350 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15100 literals 37%
c [treelook-3] scheduling used 300587 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 437067 steps
c [treelook-3] 15091 literals remain 37%
c [treelook-3] 11127 variables remain to probed next time 55%
c [treelook-3] removed 0 variables, found 1245 hbrs
c [unhide-6] limit 382163 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 3 failed, 769 tauts, 0 hbrs, 3538 literals
c [transred-2] limit 1910815 with penalty 0 = 0 + 0
c [transred-2] removed 140 transitive binary clauses
c [transred-2] found 2 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 20266 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1377 blocked clauses
c [elim-6] 188 variables 1% will be scheduled this time
c [elim-6] scheduled 188 variables 1%
c [elim-6] limit of 38216318 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 14205286 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 188 scheduled
c [bca-2] limit of 10000000 steps and 200791 added (scaled 2)
c [bca-2] 14732 out of 40530 literals actually usable 36%
c [bca-2] added 80 blocked clauses in 114024 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 5252 pos 28.9% + 12934 neg 71.1% = 18186 sched 89.7% ret 2078
c [sweep-2-1] 1037133 steps 61 queries 3464.31 avg class size
c [sweep-2-1] 1453 decisions 61 SAT calls 57.25 avg env size
c [sweep-2-1] 17240 variables remain 85% (3022 retained 15%)
c [decomp-15] removed 12 variables
c [sweep-2-1] removed 12 vars (0 failed, 3 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 12 vars in TOTAL (1 rounds, 60 queries)
c [phase-count-6] 96085 negative 96.1% of 100008 except 3923 3.9%
c [phase-count-6] 93185 positive 93.2% of 100008 except 6823 6.8%
c [phase-6] phase bias: 512 positive 69%, 228 negative 31%
c [sort-queue-6] sorted 14503 enqueued variables after 40741 conflicts
c [score-dist-6] active 5749 (28%), one 4541 (22%), zero 9962 (49%)
c [score-dist-6] max exp 636, different 405 (64%)
c [score-dist-6] median active exp 570, avg 504.1
c [simplification-6] removed 369 variables 1.8% (20252 remain 24%)
c [simplification-6] removed 5764 irredundant clauses 5.4% (100008 remain 38%)
c [simplification-6] maximum reduction of 5% = max (2%, 5%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 52741 (soft 42741 + delta 10000)
c [simplification-6] new conflict limit 42741 (hard 52741)
c 
c [simplification-7] limit 42741 conflicts (hard 52741) hit after 42741 conflicts
c [quatres-3] found 96097 quaternary clauses 87% in total
c [quatres-3-1] removed 9 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 537 single-self-subsuming ternary resolvents
c [quatres-3-2] added 4460 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 9584 schedulable variables 47%
c [ternres-3] 974 ternary resolvents (0 bin, 974 trn)
c [ternres-3] 25 variables remain 0% (20227 retained 100%)
c [basicprobe-3] limit 10231159 penalty 0 = 0 + 0
c [basicprobe-3-0] 3464 sched 17%, 23 failed, 3 lifted, 3768 hbrs
c [decomp-17] removed 153 variables
c [basicprobe-3-1] 8826 sched 44%, 83 failed, 5 lifted, 7715 hbrs
c [decomp-18] removed 392 variables
c [basicprobe-3-2] 1944 probes remain 10% after last round
c [basicprobe-3-2] 149 units = 139 failed (93%) + 10 lifted (7%)
c [basicprobe-3-2] removed 586 variables, found 12449 hbrs
c [bate-1] eliminated 396 asymmetric tautologies during probing
c [unhide-7] limit 409246 with penalty 0 = 0 + 0
c [unhide-7-7] 6 units, 0 failed, 188 tauts, 0 hbrs, 1237 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 217 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 19655 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 87 blocked clauses
c [block-3] 87 < 1/100 * 95369 = 953 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 19 (11%) of length 26
c [cce-2-1] eliminated 2 clauses out of 19 (11%) of length 25
c [cce-2-1] eliminated 1 clauses out of 18 (6%) of length 24
c [cce-2-1] eliminated 2 clauses out of 49 (4%) of length 18
c [cce-2-1] eliminated 5 clauses out of 63 (8%) of length 17
c [cce-2-1] eliminated 2 clauses out of 55 (4%) of length 16
c [cce-2-1] eliminated 1 clauses out of 79 (1%) of length 15
c [cce-2-1] eliminated 2 clauses out of 74 (3%) of length 14
c [cce-2-1] eliminated 4 clauses out of 81 (5%) of length 13
c [cce-2-1] eliminated 1 clauses out of 96 (1%) of length 12
c [cce-2-1] eliminated 21 clauses out of 2501 (1%) of length 11
c [cce-2-1] eliminated 7 clauses out of 345 (2%) of length 10
c [cce-2-1] eliminated 7 clauses out of 1933 (0%) of length 9
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 57 large clauses in 15000093 steps
c [cce-2-1] allowing another 7500046 steps for small clauses
c [cce-2-1] scheduling 30931 clauses = 16810 binary + 14121 ternary
c [cce-2-1] tried to eliminate 1379 small clauses 4%
c [cce-2-1] eliminated 29 binary clauses 0%
c [cce-2-1] eliminated 14 ternary clauses 0%
c [cce-2-1] eliminated 43 small clauses 0%
c [cce-2-1] eliminated 43 small clauses in 15000073 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 100 covered clauses in round 1
c [cce-2] eliminated 100 covered clauses in TOTAL during 1 rounds
c [cce-2] 100 < 1/100 * 95232 = 952 considered unsuccessful
c [bca-3] limit of 10000000 steps and 191011 added (scaled 2)
c [bca-3] 14487 out of 39302 literals actually usable 37%
c [bca-3] added 2 blocked clauses in 115505 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 5259 pos 31.5% + 11453 neg 68.5% = 16712 sched 85.0% ret 2938
c [sweep-3-1] 1043600 steps 66 queries 3549.48 avg class size
c [sweep-3-1] 885 decisions 57 SAT calls 41.09 avg env size
c [sweep-3-1] 16155 variables remain 82% (3495 retained 18%)
c [decomp-19] removed 22 variables
c [sweep-3-1] removed 22 vars (0 failed, 8 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 22 vars in TOTAL (1 rounds, 65 queries)
c [phase-count-7] 91216 negative 95.9% of 95091 except 3875 4.1%
c [phase-count-7] 88229 positive 92.8% of 95091 except 6862 7.2%
c [phase-7] phase bias: 163 positive 40%, 246 negative 60%
c [sort-queue-7] sorted 13610 enqueued variables after 42741 conflicts
c [score-dist-7] active 6018 (31%), one 4296 (22%), zero 9314 (47%)
c [score-dist-7] max exp 685, different 456 (66%)
c [score-dist-7] median active exp 488, avg 448.4
c [simplification-7] removed 624 variables 3.1% (19628 remain 23%)
c [simplification-7] removed 4917 irredundant clauses 4.9% (95091 remain 36%)
c [simplification-7] maximum reduction of 5% = max (3%, 5%)
c [simplification-7] large reduction 5% >= 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 54741 (soft 44741 + delta 10000)
c [simplification-7] new conflict limit 44741 (hard 54741)
c 
c [simplification-8] limit 44741 conflicts (hard 54741) hit after 44742 conflicts
c [quatres-4] found 93675 quaternary clauses 87% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 846 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3171 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 23 schedulable variables 0%
c [ternres-4] 126 ternary resolvents (0 bin, 126 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 5641 xors of average arity 3.0
c [gauss-3] connected 16879 occurrences of 1839 variables (average 9.2)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 752 schedulable variables 4%
c [simpleprobe-4] limit 8758331 penalty 0 = 0 + 0
c [decomp-21] removed 40 variables
c [simpleprobe-4] 603 variables remain 3% (18985 retained 97%)
c [simpleprobe-4] removed 40 variables, found 670 hbrs, 14 units
c [unhide-8] limit 437916 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 15 failed, 1496 tauts, 0 hbrs, 5007 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 109 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 19584 variables 100%
c [elim-7] limit of 21895827 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 245 not tried 1% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 403 = 2% variables out of 19584 scheduled
c [bca-4] limit of 10000000 steps and 189624 added (scaled 2)
c [bca-4] 14114 out of 38364 literals actually usable 37%
c [bca-4] added 38 blocked clauses in 116748 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 5362 pos 34.0% + 10405 neg 66.0% = 15767 sched 82.2% ret 3414
c [sweep-4-1] 1056829 steps 39 queries 3406.36 avg class size
c [sweep-4-1] 1217 decisions 37 SAT calls 70.19 avg env size
c [sweep-4-1] 15253 variables remain 80% (3928 retained 20%)
c [decomp-22] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 2 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2 vars in TOTAL (1 rounds, 38 queries)
c [phase-count-8] 90547 negative 95.9% of 94434 except 3887 4.1%
c [phase-count-8] 87598 positive 92.8% of 94434 except 6836 7.2%
c [phase-8] phase bias: 79 positive 23%, 270 negative 77%
c [sort-queue-8] sorted 13896 enqueued variables after 44742 conflicts
c [score-dist-8] active 5283 (28%), one 5005 (26%), zero 8891 (46%)
c [score-dist-8] max exp 732, different 454 (62%)
c [score-dist-8] median active exp 627, avg 550.4
c [simplification-8] removed 449 variables 2.3% (19179 remain 22%)
c [simplification-8] removed 657 irredundant clauses 0.7% (94434 remain 36%)
c [simplification-8] maximum reduction of 2% = max (2%, 1%)
c [simplification-8] geometric conflict interval increment 8888 = 26666 / 3
c [simplification-8] new conflict interval 35554
c [simplification-8] penalized conflict interval 35554 = 1 * 35554
c [simplification-8] hard conflict limit 98073 (soft 80296 + delta 17777)
c [simplification-8] new conflict limit 80296 (hard 98073)
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   28.0   19178    94434     70078  108620  23414 18899   12    60   28  19%    368   27   12    7  181%
c i   30.3   19177    94434     78269  116313  23539 18926   12    59   29  21%     -3   24   14    7  194%
c -   31.4   19177    94434     81421   76347  23592 18930   12    62   21  20%    -73   25   13    8  171%
c 
c [simplification-9] limit 80296 conflicts (hard 98073) hit after 86270 conflicts
c [quatres-5] found 95557 quaternary clauses 84% in total
c [quatres-5-2] added 993 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3263 quaternary resolvents
c [ternres-5] limit 5411459 with penalty 0 = 0 + 0
c [ternres-5] all 19177 free variables schedulable
c [ternres-5] 641 ternary resolvents (0 bin, 641 trn)
c [ternres-5] 4308 variables remain 22% (14869 retained 78%)
c [decomp-23] removed 13 variables
c [unhide-9] limit 1082291 with penalty 0 = 0 + 0
c [unhide-9-10] 0 units, 5 failed, 564 tauts, 0 hbrs, 5917 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 62 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 19155 variables 100%
c [block-4] limit of 27057299 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 588 blocked clauses
c [block-4] 588 < 1/100 * 94024 = 940 considered unsuccessful
c [elim-8] 245 variables 1% will be scheduled this time
c [elim-8] scheduled 245 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2164583960 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 17211310 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 245 scheduled
c [bca-5] limit of 10000000 steps and 187573 added (scaled 2)
c [bca-5] 14806 out of 38208 literals actually usable 39%
c [bca-5] added 34 blocked clauses in 116483 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 16234370 penalty 0 = 0 + 0
c [sweep-5-1] 6795 pos 44.7% + 8396 neg 55.3% = 15191 sched 79.5% ret 3912
c [sweep-5-1] 16234743 steps 1279 queries 374.93 avg class size
c [sweep-5-1] 13414 decisions 1228 SAT calls 24.09 avg env size
c [sweep-5-1] 6594 variables remain 35% (12349 retained 65%)
c [decomp-24] removed 402 variables
c [sweep-5-1] removed 402 vars (0 failed, 74 eqs, 88 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 402 vars in TOTAL (1 rounds, 1278 queries)
c [phase-count-9] 86519 negative 95.7% of 90426 except 3907 4.3%
c [phase-count-9] 83553 positive 92.4% of 90426 except 6873 7.6%
c [phase-9] phase bias: 1 positive 17%, 5 negative 83%
c [sort-queue-9] sorted 11450 enqueued variables after 86270 conflicts
c [score-dist-9] active 7251 (39%), one 4423 (24%), zero 7027 (38%)
c [score-dist-9] max exp 843, different 544 (64%)
c [score-dist-9] median active exp 711, avg 636.1
c [simplification-9] removed 476 variables 2.5% (18701 remain 22%)
c [simplification-9] removed 4008 irredundant clauses 4.2% (90426 remain 34%)
c [simplification-9] maximum reduction of 4% = max (2%, 4%)
c [simplification-9] geometric conflict interval increment 7110 = 35554 / 5
c [simplification-9] new conflict interval 42664
c [simplification-9] penalized conflict interval 42664 = 1 * 42664
c [simplification-9] hard conflict limit 150266 (soft 128934 + delta 21332)
c [simplification-9] new conflict limit 128934 (hard 150266)
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   47.4   18700    90426    128733  121027  25827 20569   13    62   30  22%    488   10   13   11  120%
c 
c [simplification-10] limit 128934 conflicts (hard 150266) hit after 128936 conflicts
c [quatres-6] found 92464 quaternary clauses 81% in total
c [quatres-6-1] removed 9 duplicate quaternary clauses
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 1054 single-self-subsuming ternary resolvents
c [quatres-6-2] added 834 quaternary resolvents
c [ternres-6] limit 9192258 with penalty 0 = 0 + 0
c [ternres-6] 4190 schedulable variables 22%
c [ternres-6] 1869 ternary resolvents (12 bin, 1857 trn)
c [ternres-6] 1 variables remain 0% (18699 retained 100%)
c [card-4] limit 574516 penalty 3 = 3 + 0
c [card-4] found 112 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 574516 for elimination
c [card-4] 112 out of 112 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-25] removed 18 variables
c [treelook-4] limit 459612 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 17405 literals 47%
c [treelook-4] scheduling used 459628 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 459612 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 531937 steps
c [treelook-4] 17393 literals remain 47%
c [treelook-4] 9659 variables remain to probed next time 52%
c [decomp-26] removed 1 variables
c [treelook-4] removed 2 variables, found 1661 hbrs
c [unhide-10] limit 1838451 with penalty 0 = 0 + 0
c [unhide-10-12] 5 units, 41 failed, 1450 tauts, 0 hbrs, 34791 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 92 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 11490322 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 30
c [cce-3-1] eliminated 2 clauses out of 5 (40%) of length 27
c [cce-3-1] eliminated 1 clauses out of 32 (3%) of length 23
c [cce-3-1] eliminated 1 clauses out of 43 (2%) of length 22
c [cce-3-1] eliminated 1 clauses out of 52 (2%) of length 16
c [cce-3-1] eliminated 1 clauses out of 78 (1%) of length 15
c [cce-3-1] eliminated 1 clauses out of 70 (1%) of length 14
c [cce-3-1] eliminated 1 clauses out of 76 (1%) of length 13
c [cce-3-1] eliminated 3 clauses out of 92 (3%) of length 12
c [cce-3-1] eliminated 18 clauses out of 2407 (1%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 33 large clauses in 11490333 steps
c [cce-3-1] allowing another 5745166 steps for small clauses
c [cce-3-1] scheduling 29432 clauses = 16549 binary + 12883 ternary
c [cce-3-1] tried to eliminate 2169 small clauses 7%
c [cce-3-1] eliminated 106 binary clauses 1%
c [cce-3-1] eliminated 58 ternary clauses 0%
c [cce-3-1] eliminated 164 small clauses 1%
c [cce-3-1] eliminated 205 small clauses in 11490365 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 238 covered clauses in round 1
c [cce-3] eliminated 238 covered clauses in TOTAL during 1 rounds
c [cce-3] 238 < 1/100 * 89836 = 898 considered unsuccessful
c [bca-6] limit of 10000000 steps and 179980 added (scaled 2)
c [bca-6] 12222 out of 37316 literals actually usable 33%
c [bca-6] added 3 blocked clauses in 147728 steps
c [sweep-6] limit 2757677 penalty 0 = 0 + 0
c [sweep-6-1] 3280 pos 50.6% + 3203 neg 49.4% = 6483 sched 34.7% ret 12174
c [sweep-6-1] 2759567 steps 85 queries 1716.98 avg class size
c [sweep-6-1] 1944 decisions 72 SAT calls 68.82 avg env size
c [sweep-6-1] 6321 variables remain 34% (12323 retained 66%)
c [decomp-27] removed 70 variables
c [sweep-6-1] removed 70 vars (0 failed, 13 eqs, 14 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 70 vars in TOTAL (1 rounds, 84 queries)
c [phase-count-10] 85514 negative 95.6% of 89405 except 3891 4.4%
c [phase-count-10] 82509 positive 92.3% of 89405 except 6896 7.7%
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-10] sorted 14220 enqueued variables after 128936 conflicts
c [score-dist-10] active 4367 (23%), one 7593 (41%), zero 6627 (36%)
c [score-dist-10] max exp 562, different 337 (60%)
c [score-dist-10] median active exp 472, avg 425.0
c [simplification-10] removed 113 variables 0.6% (18587 remain 22%)
c [simplification-10] removed 1021 irredundant clauses 1.1% (89405 remain 34%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 21332 = 42664 / 2
c [simplification-10] new conflict interval 63996
c [simplification-10] penalized conflict interval 63996 = 1 * 63996
c [simplification-10] hard conflict limit 224930 (soft 192932 + delta 31998)
c [simplification-10] new conflict limit 192932 (hard 224930)
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 -   51.1   18587    89405    132255   79766  27948 21412   14    66   23  22%   -217   14   14   11  129%
c i   53.9   18586    89405    145112   91947  28066 21426   13    56   27  23%    -17    1   16   11  143%
c i   54.0   18585    89405    145692   92466  28084 21426   13    55   27  23%   -118   -0   12   11  108%
c -   66.5   18578    89405    183663   86549  28293 21450   16    72   24  22%    296   12   17   13  135%
c 
c [simplification-11] limit 192932 conflicts (hard 224930) hit after 192934 conflicts
c [quatres-7] found 91780 quaternary clauses 78% in total
c [quatres-7-1] removed 4 duplicate quaternary clauses
c [quatres-7-1] added 4 double-self-subsuming ternary resolvents
c [quatres-7-2] added 614 single-self-subsuming ternary resolvents
c [quatres-7-2] added 559 quaternary resolvents
c [ternres-7] limit 14632563 with penalty 0 = 0 + 0
c [ternres-7] 1 schedulable variables 0%
c [ternres-7] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 731628 penalty 2 = 2 + 0
c [gauss-4] extracted 4071 xors of average arity 3.0
c [gauss-4] connected 12168 occurrences of 1616 variables (average 7.5)
c [gauss-4] limit 731628 penalty 2 = 2 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 52 variables
c [basicprobe-4] limit 73162816 penalty 0 = 0 + 0
c [basicprobe-4-0] 2275 sched 12%, 71 failed, 25 lifted, 610 hbrs
c [decomp-29] removed 215 variables
c [basicprobe-4-1] 8344 sched 46%, 86 failed, 8 lifted, 1649 hbrs
c [decomp-30] removed 365 variables
c [basicprobe-4-2] 8359 sched 47%, 93 failed, 22 lifted, 677 hbrs
c [decomp-31] removed 180 variables
c [basicprobe-4-3] 8302 sched 47%, 77 failed, 12 lifted, 807 hbrs
c [decomp-32] removed 187 variables
c [basicprobe-4-4] 8261 sched 47%, 67 failed, 21 lifted, 580 hbrs
c [decomp-33] removed 122 variables
c [basicprobe-4-5] 8235 sched 47%, 50 failed, 10 lifted, 494 hbrs
c [decomp-34] removed 119 variables
c [basicprobe-4-6] 8237 sched 48%, 77 failed, 6 lifted, 573 hbrs
c [decomp-35] removed 201 variables
c [basicprobe-4-7] 8246 sched 49%, 57 failed, 9 lifted, 437 hbrs
c [decomp-36] removed 179 variables
c [basicprobe-4-8] 8237 sched 49%, 60 failed, 11 lifted, 308 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 762 units = 638 failed (84%) + 124 lifted (16%)
c [basicprobe-4-8] removed 1729 variables, found 6135 hbrs
c [bate-2] eliminated 597 asymmetric tautologies during probing
c [unhide-11] limit 2926512 with penalty 0 = 0 + 0
c [unhide-11-15] 6 units, 39 failed, 1424 tauts, 0 hbrs, 11640 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 81 transitive binary clauses
c [transred-7] found 2 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 16715 variables 100%
c [elim-9] limit of 146325632 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 520 variables 3% in round 1 in 30728274 steps
c [elim-9-1] backward subsumption/strengthening limit 30728200
c [elim-9-1-1] backward checking 2173 touched variables 13%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 32 and strengthened 70 clauses in 2553766 steps
c [elim-9-1] rescheduled 88 variables 1% by backward subsumption
c [elim-9-2] eliminated 7 variables 0% in round 2 in 601343 steps
c [elim-9-2] backward subsumption/strengthening limit 601300
c [elim-9-2-1] backward checking 49 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 3 and strengthened 6 clauses in 180351 steps
c [elim-9-2] rescheduled 15 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 145519 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 534 = 3% variables out of 16715 scheduled
c [bca-7] limit of 10000000 steps and 153231 added (scaled 2)
c [bca-7] 12755 out of 32364 literals actually usable 39%
c [bca-7] added 28 blocked clauses in 103360 steps
c [sweep-7] limit 4389768 penalty 0 = 0 + 0
c [sweep-7-1] 2700 pos 53.2% + 2378 neg 46.8% = 5078 sched 31.4% ret 11103
c [sweep-7-1] 4390831 steps 213 queries 629.01 avg class size
c [sweep-7-1] 2871 decisions 203 SAT calls 31.54 avg env size
c [sweep-7-1] 4327 variables remain 27% (11814 retained 73%)
c [decomp-37] removed 52 variables
c [sweep-7-1] removed 52 vars (0 failed, 15 eqs, 21 impls)
c [sweep-7] removed 52 vars in TOTAL (1 rounds, 212 queries)
c [phase-count-11] 71998 negative 94.8% of 75930 except 3932 5.2%
c [phase-count-11] 69058 positive 90.9% of 75930 except 6872 9.1%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 1 positive 33%, 2 negative 67%
c [sort-queue-11] sorted 9986 enqueued variables after 192934 conflicts
c [score-dist-11] active 6143 (38%), one 5665 (35%), zero 4321 (27%)
c [score-dist-11] max exp 896, different 565 (63%)
c [score-dist-11] median active exp 694, avg 647.2
c [simplification-11] removed 2449 variables 13.2% (16129 remain 19%)
c [simplification-11] removed 13475 irredundant clauses 15.1% (75930 remain 29%)
c [simplification-11] maximum reduction of 15% = max (13%, 15%)
c [simplification-11] large reduction 15% >= 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 204934 (soft 194934 + delta 10000)
c [simplification-11] new conflict limit 194934 (hard 204934)
c 
c [simplification-12] limit 194934 conflicts (hard 204934) hit after 194934 conflicts
c [quatres-8] found 64774 quaternary clauses 71% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 1632 single-self-subsuming ternary resolvents
c [quatres-8-2] added 1831 quaternary resolvents
c [simpleprobe-5] 531 schedulable variables 3%
c [simpleprobe-5] limit 59000189 penalty 0 = 0 + 0
c [decomp-39] removed 44 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 44 variables, found 3204 hbrs, 14 units
c [unhide-12] limit 2950009 with penalty 0 = 0 + 0
c [unhide-12-18] 3 units, 7 failed, 3270 tauts, 0 hbrs, 7297 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 156 transitive binary clauses
c [transred-8] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 16077 variables 100%
c [block-5] limit of 36875118 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 97 blocked clauses
c [block-5] 97 < 1/100 * 75524 = 755 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 16077 variables 100%
c [elim-10] limit of 295000945 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 118 variables 1% in round 1 in 29268748 steps
c [elim-10-1] backward subsumption/strengthening limit 29268700
c [elim-10-1-1] backward checking 1003 touched variables 6%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 5 clauses in 1530075 steps
c [elim-10-1] rescheduled 8 variables 0% by backward subsumption
c [elim-10-2] eliminated 2 variables 0% in round 2 in 31213 steps
c [elim-10-2] backward subsumption/strengthening limit 31200
c [elim-10-2-1] backward checking 9 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 2 and strengthened 1 clauses in 31201 steps
c [elim-10-2] rescheduled 7 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 69910 steps
c [elim-10-3] backward subsumption/strengthening limit 69900
c [elim-10-3-1] backward checking 12 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 1 clauses in 61569 steps
c [elim-10] incomplete 4 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 130 = 1% variables out of 16077 scheduled
c [elim-10] 130 < 1/100 * 16077 = 160 considered unsuccessful
c [bca-8] limit of 10000000 steps and 150575 added (scaled 2)
c [bca-8] 12375 out of 31896 literals actually usable 39%
c [bca-8] added 21 blocked clauses in 102747 steps
c [sweep-8] limit 4425014 penalty 0 = 0 + 0
c [sweep-8-1] 2373 pos 55.9% + 1872 neg 44.1% = 4245 sched 26.6% ret 11702
c [sweep-8-1] 4432253 steps 396 queries 383.61 avg class size
c [sweep-8-1] 4167 decisions 385 SAT calls 23.29 avg env size
c [sweep-8-1] 3142 variables remain 20% (12798 retained 80%)
c [decomp-40] removed 35 variables
c [sweep-8-1] removed 35 vars (0 failed, 23 eqs, 29 impls)
c [sweep-8] removed 35 vars in TOTAL (1 rounds, 395 queries)
c [phase-count-12] 70797 negative 94.7% of 74797 except 4000 5.3%
c [phase-count-12] 67926 positive 90.8% of 74797 except 6871 9.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 9488 enqueued variables after 194934 conflicts
c [score-dist-12] active 6424 (40%), one 5645 (35%), zero 3843 (24%)
c [score-dist-12] max exp 995, different 600 (60%)
c [score-dist-12] median active exp 802, avg 735.4
c [simplification-12] removed 217 variables 1.3% (15912 remain 19%)
c [simplification-12] removed 1133 irredundant clauses 1.5% (74797 remain 28%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 31998 = 63996 / 2
c [simplification-12] new conflict interval 95994
c [simplification-12] penalized conflict interval 95994 = 1 * 95994
c [simplification-12] hard conflict limit 338925 (soft 290928 + delta 47997)
c [simplification-12] new conflict limit 290928 (hard 338925)
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   77.9   15911    74797    202938   82034  24311 19422   14    61   24  22%    482   -1    6   13   48%
c -   87.9   15911    74797    236247   73832  24459 19439   16    72   29  23%    151    6   16   14  118%
c -  101.4   15911    74797    282354   78168  24657 19455   18    76   29  23%    592    8   18   15  117%
c 
c [simplification-13] limit 290928 conflicts (hard 338925) hit after 290928 conflicts
c [quatres-9] found 63360 quaternary clauses 66% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 773 single-self-subsuming ternary resolvents
c [quatres-9-2] added 913 quaternary resolvents
c [ternres-8] limit 11297590 with penalty 1 = 1 + 0
c [ternres-8] all 15911 free variables schedulable
c [ternres-8] 2949 ternary resolvents (16 bin, 2933 trn)
c [ternres-8] 29 variables remain 0% (15882 retained 100%)
c [decomp-41] removed 4 variables
c [treelook-5] limit 2259518 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 22237 literals 70%
c [treelook-5] scheduling used 589373 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2259518 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2284236 steps
c [treelook-5] 22154 literals remain 70%
c [treelook-5] 8798 variables remain to probed next time 55%
c [treelook-5] removed 0 variables, found 2361 hbrs
c [unhide-13] limit 4519036 with penalty 0 = 0 + 0
c [unhide-13-22] 4 units, 13 failed, 1590 tauts, 0 hbrs, 19626 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 158 transitive binary clauses
c [transred-9] found 1 units
c [bca-9] limit of 10000000 steps and 149406 added (scaled 2)
c [bca-9] 11670 out of 31734 literals actually usable 37%
c [bca-9] added 6 blocked clauses in 112702 steps
c [sweep-9] limit 6778554 penalty 0 = 0 + 0
c [sweep-9-1] 1869 pos 59.6% + 1265 neg 40.4% = 3134 sched 19.8% ret 12732
c [sweep-9-1] 6780004 steps 710 queries 144.24 avg class size
c [sweep-9-1] 5682 decisions 707 SAT calls 19.09 avg env size
c [sweep-9-1] 1144 variables remain 7% (14624 retained 93%)
c [decomp-43] removed 115 variables
c [sweep-9-1] removed 115 vars (0 failed, 11 eqs, 12 impls)
c [sweep-9] removed 115 vars in TOTAL (1 rounds, 709 queries)
c [phase-count-13] 69425 negative 94.5% of 73427 except 4002 5.5%
c [phase-count-13] 66556 positive 90.6% of 73427 except 6871 9.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 9039 enqueued variables after 290928 conflicts
c [score-dist-13] active 6712 (43%), one 5962 (38%), zero 3077 (20%)
c [score-dist-13] max exp 750, different 531 (71%)
c [score-dist-13] median active exp 624, avg 573.6
c [simplification-13] removed 160 variables 1.0% (15751 remain 18%)
c [simplification-13] removed 1370 irredundant clauses 1.8% (73427 remain 28%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 31998 = 95994 / 3
c [simplification-13] new conflict interval 127992
c [simplification-13] penalized conflict interval 127992 = 1 * 127992
c [simplification-13] hard conflict limit 482916 (soft 418920 + delta 63996)
c [simplification-13] new conflict limit 418920 (hard 482916)
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 -  117.9   15751    73427    327172   80826  28179 19912   18    89   31  20%    806   12   16   17   94%
c i  122.3   15750    73427    346096   98992  28223 19914   18    81   37  23%    861    5   20   17  118%
c -  130.1   15748    73427    371346   86094  28286 19920   18    72   32  25%   -633   -7   14   17   81%
c -  142.1   15748    73427    413489   89595  28329 19922   18    76   32  23%    153   -4   19   18  102%
c 
c [simplification-14] limit 418920 conflicts (hard 482916) hit after 418920 conflicts
c [quatres-10] found 62006 quaternary clauses 62% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 1058 single-self-subsuming ternary resolvents
c [quatres-10-2] added 446 quaternary resolvents
c [ternres-9] limit 33204951 with penalty 0 = 0 + 0
c [ternres-9] 27 schedulable variables 0%
c [ternres-9] 653 ternary resolvents (1 bin, 652 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-44] removed 4 variables
c [basicprobe-5] limit 166024759 penalty 0 = 0 + 0
c [basicprobe-5-0] 8095 sched 52%, 61 failed, 14 lifted, 625 hbrs
c [decomp-45] removed 154 variables
c [basicprobe-5-1] 8062 sched 52%, 48 failed, 9 lifted, 520 hbrs
c [decomp-46] removed 133 variables
c [basicprobe-5-2] 8039 sched 52%, 35 failed, 6 lifted, 397 hbrs
c [decomp-47] removed 76 variables
c [basicprobe-5-3] 8011 sched 52%, 46 failed, 11 lifted, 225 hbrs
c [decomp-48] removed 119 variables
c [basicprobe-5-4] 8031 sched 53%, 45 failed, 11 lifted, 378 hbrs
c [decomp-49] removed 120 variables
c [basicprobe-5-5] 8019 sched 53%, 40 failed, 13 lifted, 224 hbrs
c [decomp-50] removed 67 variables
c [basicprobe-5-6] 8016 sched 53%, 33 failed, 10 lifted, 534 hbrs
c [decomp-51] removed 80 variables
c [basicprobe-5-7] 8027 sched 54%, 37 failed, 3 lifted, 180 hbrs
c [decomp-52] removed 84 variables
c [basicprobe-5-8] 8014 sched 54%, 37 failed, 10 lifted, 182 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 469 units = 382 failed (81%) + 87 lifted (19%)
c [basicprobe-5-8] removed 909 variables, found 3265 hbrs
c [bate-3] eliminated 499 asymmetric tautologies during probing
c [unhide-14] limit 6640990 with penalty 0 = 0 + 0
c [unhide-14-27] 4 units, 20 failed, 1806 tauts, 0 hbrs, 28344 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 104 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 207530948 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 43 (2%) of length 22
c [cce-4-1] eliminated 3 clauses out of 69 (4%) of length 19
c [cce-4-1] eliminated 3 clauses out of 50 (6%) of length 18
c [cce-4-1] eliminated 2 clauses out of 77 (3%) of length 17
c [cce-4-1] eliminated 5 clauses out of 78 (6%) of length 16
c [cce-4-1] eliminated 4 clauses out of 92 (4%) of length 15
c [cce-4-1] eliminated 7 clauses out of 105 (7%) of length 14
c [cce-4-1] eliminated 8 clauses out of 106 (8%) of length 13
c [cce-4-1] eliminated 12 clauses out of 126 (10%) of length 12
c [cce-4-1] eliminated 6 clauses out of 2406 (0%) of length 11
c [cce-4-1] eliminated 15 clauses out of 381 (4%) of length 10
c [cce-4-1] eliminated 39 clauses out of 1957 (2%) of length 9
c [cce-4-1] eliminated 39 clauses out of 680 (6%) of length 8
c [cce-4-1] eliminated 61 clauses out of 825 (7%) of length 7
c [cce-4-1] eliminated 63 clauses out of 849 (7%) of length 6
c [cce-4-1] eliminated 104 clauses out of 1025 (10%) of length 5
c [cce-4-1] eliminated 2356 clauses out of 17011 (14%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 2728 large clauses in 51199306 steps
c [cce-4-1] allowing another 25599653 steps for small clauses
c [cce-4-1] scheduling 24871 clauses = 16032 binary + 8839 ternary
c [cce-4-1] tried to eliminate 24871 small clauses 100%
c [cce-4-1] eliminated 543 binary clauses 3%
c [cce-4-1] eliminated 197 ternary clauses 2%
c [cce-4-1] eliminated 740 small clauses 3%
c [cce-4-1] eliminated 829 small clauses in 68560996 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 3557 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 22442115 steps for small clauses
c [cce-4-2] scheduling 24131 clauses = 15489 binary + 8642 ternary
c [cce-4-2] tried to eliminate 24131 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 3557 covered clauses in TOTAL during 2 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 14773 variables 100%
c [elim-11] limit of 332049518 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 431 variables 3% in round 1 in 23596214 steps
c [elim-11-1] backward subsumption/strengthening limit 23596200
c [elim-11-1-1] backward checking 1671 touched variables 11%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 2 clauses in 1913429 steps
c [elim-11-1] rescheduled 5 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 29932 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 431 = 3% variables out of 14773 scheduled
c [bca-10] limit of 10000000 steps and 127237 added (scaled 2)
c [bca-10] 11884 out of 28686 literals actually usable 41%
c [bca-10] added 4 blocked clauses in 101581 steps
c [sweep-10] limit 9961485 penalty 0 = 0 + 0
c [sweep-10-1] 523 pos 52.9% + 466 neg 47.1% = 989 sched 6.9% ret 13353
c [sweep-10-1] 4278413 steps 506 queries 57.19 avg class size
c [sweep-10-1] 4293 decisions 508 SAT calls 17.49 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-53] removed 8 variables
c [sweep-10-1] removed 8 vars (0 failed, 10 eqs, 15 impls)
c [sweep-10-2] 6363 pos 44.4% + 7971 neg 55.6% = 14334 sched 100.0% ret 0
c [sweep-10-2] 5683682 steps 295 queries 501.58 avg class size
c [sweep-10-2] 5879 decisions 293 SAT calls 46.48 avg env size
c [sweep-10-2] 6523 variables remain 46% (7811 retained 54%)
c [decomp-54] removed 4 variables
c [sweep-10-2] removed 4 vars (0 failed, 4 eqs, 5 impls)
c [sweep-10] 12 < 1/1000 * 14342 = 14 considered unsuccessful
c [sweep-10] removed 12 vars in TOTAL (2 rounds, 799 queries)
c [sort-queue-14] sorted 8931 enqueued variables after 418920 conflicts
c [score-dist-14] active 5399 (38%), one 6884 (48%), zero 2047 (14%)
c [score-dist-14] max exp 957, different 368 (38%)
c [score-dist-14] median active exp 860, avg 779.4
c [simplification-14] removed 1418 variables 9.0% (14330 remain 17%)
c [simplification-14] removed 10237 irredundant clauses 13.9% (63190 remain 24%)
c [simplification-14] maximum reduction of 14% = max (9%, 14%)
c [simplification-14] large reduction 14% >= 5% limit
c [simplification-14] next conflict interval 4189 = min (418920/100, 127992)
c [simplification-14] penalized conflict interval 4189 = 1 * 4189
c [simplification-14] hard conflict limit 433109 (soft 423109 + delta 10000)
c [simplification-14] new conflict limit 423109 (hard 433109)
c 
c [simplification-15] limit 423109 conflicts (hard 433109) hit after 423109 conflicts
c [quatres-11] found 43494 quaternary clauses 54% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 589 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1652 quaternary resolvents
c [ternres-10] limit 33491987 with penalty 0 = 0 + 0
c [ternres-10] all 14330 free variables schedulable
c [ternres-10] 1518 ternary resolvents (4 bin, 1514 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 1046624 penalty 4 = 4 + 0
c [card-5] found 286 at-most-one constraints of average size 3.5
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1046624 for elimination
c [card-5] 286 out of 286 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 837299 penalty 3 = 3 + 0
c [gauss-5] extracted 5719 xors of average arity 3.0
c [gauss-5] connected 17157 occurrences of 1598 variables (average 10.7)
c [gauss-5] limit 837299 penalty 3 = 3 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 14330 free variables schedulable
c [simpleprobe-6] limit 133967950 penalty 0 = 0 + 0
c [decomp-56] removed 15 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 15 variables, found 6073 hbrs, 10 units
c [unhide-15] limit 6698397 with penalty 0 = 0 + 0
c [unhide-15-33] 0 units, 3 failed, 5251 tauts, 0 hbrs, 12154 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 214 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 14313 variables 100%
c [elim-12] limit of 669839752 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 27 variables 0% in round 1 in 23280127 steps
c [elim-12-1] backward subsumption/strengthening limit 23280100
c [elim-12-1-1] backward checking 273 touched variables 2%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 2 and strengthened 2 clauses in 548397 steps
c [elim-12-1] rescheduled 8 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 66139 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 27 = 0% variables out of 14313 scheduled
c [elim-12] 27 < 1/100 * 14313 = 143 considered unsuccessful
c [bca-11] limit of 10000000 steps and 126885 added (scaled 2)
c [bca-11] 11457 out of 28574 literals actually usable 40%
c [bca-11] added 7 blocked clauses in 104891 steps
c [sort-queue-15] sorted 10074 enqueued variables after 423109 conflicts
c [score-dist-15] active 4212 (29%), one 8040 (56%), zero 2034 (14%)
c [score-dist-15] max exp 555, different 377 (68%)
c [score-dist-15] median active exp 446, avg 411.7
c [simplification-15] removed 44 variables 0.3% (14286 remain 17%)
c [simplification-15] removed 155 irredundant clauses 0.2% (63035 remain 24%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 127992
c [simplification-15] new conflict interval 255984
c [simplification-15] penalized conflict interval 255984 = 1 * 255984
c [simplification-15] hard conflict limit 807085 (soft 679093 + delta 127992)
c [simplification-15] new conflict limit 679093 (hard 807085)
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 -  165.1   14286    63035    462630   79410  26635 19791   19    67   30  28%    613  -21   17   18   92%
c -  176.7   14286    63035    504800   83054  26726 19796   19    92   31  20%    808    4   16   19   85%
c -  190.0   14286    63035    546207   83069  26832 19802   22   112   30  20%    909   18   21   20  106%
c -  202.7   14286    63035    591041   86978  26934 19807   21    72   32  30%    966  -26   24   21  117%
c i  213.3   14285    63035    631309  125210  27011 19814   23   112   47  20%    993   25   23   20  114%
c -  214.2   14283    63035    634951   90263  27014 19815   20   119   32  17%  -3159   30   18   20   91%
c -  227.1   14283    63035    677729   92465  27076 19817   21   125   33  17%  -1221   30   22   20  110%
c -  240.7   14283    63035    721739   93494  27150 19823   20    72   52  27%   -123  -23   19   21   91%
c 
c [simplification-16] limit 679093 conflicts (hard 807085) hit after 729172 conflicts
c [quatres-12] found 45411 quaternary clauses 48% in total
c [quatres-12-1] removed 4 duplicate quaternary clauses
c [quatres-12-2] added 455 single-self-subsuming ternary resolvents
c [quatres-12-2] added 495 quaternary resolvents
c [ternres-11] limit 59072843 with penalty 0 = 0 + 0
c [ternres-11] all 14283 free variables schedulable
c [ternres-11] 1128 ternary resolvents (4 bin, 1124 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-57] removed 3 variables
c [unhide-16] limit 11814568 with penalty 0 = 0 + 0
c [unhide-16-41] 0 units, 10 failed, 1043 tauts, 0 hbrs, 41319 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 63 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 14276 variables 100%
c [block-6] limit of 73841054 steps penalty 3 = 3 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 34 blocked clauses
c [block-6] 34 < 1/100 * 62977 = 629 considered unsuccessful
c [cce-5] limit of 73841054 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 7 (29%) of length 29
c [cce-5-1] eliminated 4 clauses out of 23 (17%) of length 26
c [cce-5-1] eliminated 4 clauses out of 17 (24%) of length 25
c [cce-5-1] eliminated 4 clauses out of 21 (19%) of length 24
c [cce-5-1] eliminated 4 clauses out of 39 (10%) of length 23
c [cce-5-1] eliminated 4 clauses out of 50 (8%) of length 22
c [cce-5-1] eliminated 6 clauses out of 62 (10%) of length 21
c [cce-5-1] eliminated 3 clauses out of 42 (7%) of length 20
c [cce-5-1] eliminated 12 clauses out of 72 (17%) of length 19
c [cce-5-1] eliminated 7 clauses out of 54 (13%) of length 18
c [cce-5-1] eliminated 8 clauses out of 77 (10%) of length 17
c [cce-5-1] eliminated 12 clauses out of 65 (18%) of length 16
c [cce-5-1] eliminated 11 clauses out of 96 (11%) of length 15
c [cce-5-1] eliminated 8 clauses out of 90 (9%) of length 14
c [cce-5-1] eliminated 9 clauses out of 97 (9%) of length 13
c [cce-5-1] eliminated 17 clauses out of 122 (14%) of length 12
c [cce-5-1] eliminated 18 clauses out of 2406 (1%) of length 11
c [cce-5-1] eliminated 49 clauses out of 381 (13%) of length 10
c [cce-5-1] eliminated 119 clauses out of 1923 (6%) of length 9
c [cce-5-1] eliminated 63 clauses out of 645 (10%) of length 8
c [cce-5-1] eliminated 41 clauses out of 795 (5%) of length 7
c [cce-5-1] eliminated 79 clauses out of 839 (9%) of length 6
c [cce-5-1] eliminated 269 clauses out of 1424 (19%) of length 5
c [cce-5-1] eliminated 364 clauses out of 14251 (3%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 1117 large clauses in 49351952 steps
c [cce-5-1] allowing another 24675976 steps for small clauses
c [cce-5-1] scheduling 31380 clauses = 15506 binary + 15874 ternary
c [cce-5-1] tried to eliminate 28638 small clauses 91%
c [cce-5-1] eliminated 801 binary clauses 5%
c [cce-5-1] eliminated 404 ternary clauses 3%
c [cce-5-1] eliminated 1205 small clauses 4%
c [cce-5-1] eliminated 1205 small clauses in 73841093 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2322 covered clauses in round 1
c [cce-5] eliminated 2322 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 122060 added (scaled 2)
c [bca-12] 10912 out of 28554 literals actually usable 38%
c [bca-12] added 6 blocked clauses in 124033 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 88609265 penalty 1 = 1 + 0
c [sweep-11-1] 3591 pos 55.2% + 2912 neg 44.8% = 6503 sched 45.6% ret 7773
c [sweep-11-1] 30754399 steps 1694 queries 96.52 avg class size
c [sweep-11-1] 20288 decisions 1705 SAT calls 28.41 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-58] removed 27 variables
c [sweep-11-1] removed 27 vars (0 failed, 22 eqs, 49 impls)
c [sweep-11-2] 6448 pos 45.3% + 7801 neg 54.7% = 14249 sched 100.0% ret 0
c [sweep-11-2] 38127176 steps 1779 queries 86.62 avg class size
c [sweep-11-2] 24913 decisions 1779 SAT calls 35.07 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-59] removed 39 variables
c [sweep-11-2] removed 39 vars (0 failed, 24 eqs, 38 impls)
c [sweep-11-3] 6440 pos 45.3% + 7770 neg 54.7% = 14210 sched 100.0% ret 0
c [sweep-11-3] 19813247 steps 733 queries 147.88 avg class size
c [sweep-11-3] 14299 decisions 733 SAT calls 47.14 avg env size
c [sweep-11-3] 2829 variables remain 20% (11378 retained 80%)
c [decomp-60] removed 21 variables
c [sweep-11-3] removed 21 vars (0 failed, 6 eqs, 14 impls)
c [sweep-11] removed 87 vars in TOTAL (3 rounds, 4203 queries)
c [sort-queue-16] sorted 6304 enqueued variables after 729172 conflicts
c [score-dist-16] active 7885 (56%), one 5266 (37%), zero 1038 (7%)
c [score-dist-16] max exp 768, different 568 (74%)
c [score-dist-16] median active exp 648, avg 558.2
c [simplification-16] removed 94 variables 0.7% (14189 remain 17%)
c [simplification-16] removed 2704 irredundant clauses 4.3% (60331 remain 23%)
c [simplification-16] maximum reduction of 4% = max (1%, 4%)
c [simplification-16] geometric conflict interval increment 51196 = 255984 / 5
c [simplification-16] new conflict interval 307180
c [simplification-16] penalized conflict interval 307180 = 1 * 307180
c [simplification-16] hard conflict limit 1189942 (soft 1036352 + delta 153590)
c [simplification-16] new conflict limit 1036352 (hard 1189942)
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 -  261.5   14189    60331    764062   96580  29977 20122   25   104   33  24%    423    7   20   22   88%
c -  274.5   14189    60331    808667  100756  30020 20123   16   130   33  13%    720   24   16   21   74%
c -  288.2   14189    60331    851669  101153  30108 20132   25   104   33  24%    866   -1   23   21  106%
c -  302.1   14189    60331    897475  103514  30210 20140   18   108   53  17%    945    5   15   22   69%
c -  316.8   14189    60331    943154  105751  30328 20143   23   123   53  18%    985   19   22   22  100%
c -  332.5   14189    60331    989396  106812  30400 20148   23    95   36  25%   1005  -14   14   23   58%
c 
c [simplification-17] limit 1036352 conflicts (hard 1189942) hit after 1036352 conflicts
c [quatres-13] found 45622 quaternary clauses 44% in total
c [quatres-13-1] removed 10 duplicate quaternary clauses
c [quatres-13-1] added 5 double-self-subsuming ternary resolvents
c [quatres-13-2] added 556 single-self-subsuming ternary resolvents
c [quatres-13-2] added 512 quaternary resolvents
c [ternres-12] limit 88557308 with penalty 0 = 0 + 0
c [ternres-12] all 14189 free variables schedulable
c [ternres-12] 2401 ternary resolvents (5 bin, 2396 trn)
c [ternres-12] fully completed ternary resolution
c [treelook-6] limit 4427865 penalty 1 = 1 + 0 boost 1
c [treelook-6] scheduled 21052 literals 74%
c [treelook-6] scheduling used 690751 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 4427865 penalty 1 = 1 + 0 boost 1
c [treelook-6] used 4433503 steps
c [treelook-6] 20722 literals remain 73%
c [treelook-6] 8297 variables remain to probed next time 58%
c [treelook-6] removed 3 variables, found 3280 hbrs
c [unhide-17] limit 17711461 with penalty 0 = 0 + 0
c [unhide-17-49] 5 units, 10 failed, 2707 tauts, 0 hbrs, 209189 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 84 transitive binary clauses
c [transred-13] found 1 units
c [cce-6] limit of 221393271 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 6 clauses out of 57 (11%) of length 21
c [cce-6-1] eliminated 1 clauses out of 99 (1%) of length 12
c [cce-6-1] eliminated 2 clauses out of 1803 (0%) of length 9
c [cce-6-1] eliminated 2 clauses out of 585 (0%) of length 8
c [cce-6-1] eliminated 2 clauses out of 756 (0%) of length 7
c [cce-6-1] eliminated 4 clauses out of 743 (1%) of length 6
c [cce-6-1] eliminated 7 clauses out of 1078 (1%) of length 5
c [cce-6-1] eliminated 43 clauses out of 13311 (0%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 67 large clauses in 35428858 steps
c [cce-6-1] allowing another 17714429 steps for small clauses
c [cce-6-1] scheduling 22805 clauses = 14844 binary + 7961 ternary
c [cce-6-1] tried to eliminate 22805 small clauses 100%
c [cce-6-1] eliminated 75 binary clauses 1%
c [cce-6-1] eliminated 57 ternary clauses 1%
c [cce-6-1] eliminated 132 small clauses 1%
c [cce-6-1] eliminated 149 small clauses in 50384305 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 216 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 17558788 steps for small clauses
c [cce-6-2] scheduling 22673 clauses = 14769 binary + 7904 ternary
c [cce-6-2] tried to eliminate 22673 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 216 covered clauses in TOTAL during 2 rounds
c [cce-6] 216 < 1/100 * 60173 = 601 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 14169 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 581 variables 4% in round 1 in 21864274 steps
c [elim-13-1] backward subsumption/strengthening limit 21864200
c [elim-13-1-1] backward checking 1340 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 2 clauses in 2571501 steps
c [elim-13-1] rescheduled 11 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 333781 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 581 = 4% variables out of 14169 scheduled
c [bca-13] limit of 10000000 steps and 119435 added (scaled 2)
c [bca-13] 9317 out of 27178 literals actually usable 34%
c [bca-13] added 24 blocked clauses in 156791 steps
c [sweep-12] limit 26567192 penalty 0 = 0 + 0
c [sweep-12-1] 1781 pos 67.3% + 867 neg 32.7% = 2648 sched 19.5% ret 10940
c [sweep-12-1] 24453029 steps 981 queries 54.71 avg class size
c [sweep-12-1] 14451 decisions 989 SAT calls 40.56 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-63] removed 3 variables
c [sweep-12-1] removed 3 vars (0 failed, 4 eqs, 14 impls)
c [sweep-12-2] 6054 pos 44.6% + 7531 neg 55.4% = 13585 sched 100.0% ret 0
c [sweep-12-2] 2413384 steps 53 queries 1272.02 avg class size
c [sweep-12-2] 1850 decisions 51 SAT calls 118.53 avg env size
c [sweep-12-2] 10374 variables remain 76% (3211 retained 24%)
c [decomp-64] removed 1 variables
c [sweep-12-2] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-12] 4 < 1/1000 * 13588 = 13 considered unsuccessful
c [sweep-12] removed 4 vars in TOTAL (2 rounds, 1032 queries)
c [sort-queue-17] sorted 6393 enqueued variables after 1036352 conflicts
c [score-dist-17] active 7191 (53%), one 5659 (42%), zero 734 (5%)
c [score-dist-17] max exp 691, different 461 (67%)
c [score-dist-17] median active exp 582, avg 547.6
c [simplification-17] removed 605 variables 4.3% (13584 remain 16%)
c [simplification-17] removed 1026 irredundant clauses 1.7% (59305 remain 22%)
c [simplification-17] maximum reduction of 4% = max (4%, 2%)
c [simplification-17] geometric conflict interval increment 61436 = 307180 / 5
c [simplification-17] new conflict interval 368616
c [simplification-17] penalized conflict interval 368616 = 1 * 368616
c [simplification-17] hard conflict limit 1589276 (soft 1404968 + delta 184308)
c [simplification-17] new conflict limit 1404968 (hard 1589276)
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 -  363.0   13584    59305   1050915  106664  31497 19035   26   116   36  23%   1016    4   28   24  117%
c -  376.1   13584    59305   1099406  110957  31545 19043   23    42   37  53%   1020  -55   24   24  103%
c -  389.5   13584    59305   1146103  112399  31599 19047   25    97   37  26%   1022   13   30   23  127%
c -  405.0   13584    59305   1192971  112720  31637 19048   25   101   38  25%   1023    2   29   23  122%
c -  421.5   13584    59305   1242517  114326  31692 19053   24    94   59  25%   1024   -9   31   24  129%
c -  437.7   13584    59305   1293246  118144  31746 19054   22   109   60  20%   1024    4   26   23  115%
c -  453.5   13584    59305   1342619  118650  31803 19058   21   102   61  21%   1024   -2   27   23  116%
c -  469.7   13584    59305   1393890  121977  31839 19063   21    72   61  29%   1024  -25   19   23   85%
c 
c [simplification-18] limit 1404968 conflicts (hard 1589276) hit after 1408544 conflicts
c [quatres-14] found 44039 quaternary clauses 39% in total
c [quatres-14-1] removed 5 duplicate quaternary clauses
c [quatres-14-1] added 6 double-self-subsuming ternary resolvents
c [quatres-14-2] added 430 single-self-subsuming ternary resolvents
c [quatres-14-2] added 486 quaternary resolvents
c [ternres-13] limit 124052521 with penalty 0 = 0 + 0
c [ternres-13] all 13584 free variables schedulable
c [ternres-13] 1485 ternary resolvents (3 bin, 1482 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 7856 sched 58%, 28 failed, 5 lifted, 521 hbrs
c [decomp-66] removed 36 variables
c [basicprobe-6-1] 7815 sched 58%, 23 failed, 1 lifted, 232 hbrs
c [decomp-67] removed 31 variables
c [basicprobe-6-2] 7795 sched 58%, 15 failed, 0 lifted, 97 hbrs
c [decomp-68] removed 17 variables
c [basicprobe-6-3] 7779 sched 58%, 17 failed, 9 lifted, 144 hbrs
c [decomp-69] removed 26 variables
c [basicprobe-6-4] 7778 sched 58%, 15 failed, 3 lifted, 120 hbrs
c [decomp-70] removed 22 variables
c [basicprobe-6-5] 7769 sched 58%, 14 failed, 3 lifted, 80 hbrs
c [decomp-71] removed 15 variables
c [basicprobe-6-6] 7761 sched 58%, 10 failed, 2 lifted, 121 hbrs
c [decomp-72] removed 11 variables
c [basicprobe-6-7] 7771 sched 58%, 9 failed, 1 lifted, 46 hbrs
c [decomp-73] removed 9 variables
c [basicprobe-6-8] 7760 sched 58%, 6 failed, 0 lifted, 59 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 161 units = 137 failed (85%) + 24 lifted (15%)
c [basicprobe-6-8] removed 175 variables, found 1420 hbrs
c [bate-4] eliminated 72 asymmetric tautologies during probing
c [unhide-18] limit 20000000 with penalty 0 = 0 + 0
c [unhide-18-59] 0 units, 9 failed, 1215 tauts, 0 hbrs, 82826 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 65 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 13404 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 59 variables 0% in round 1 in 21176526 steps
c [elim-14-1] backward subsumption/strengthening limit 21176500
c [elim-14-1-1] backward checking 368 touched variables 3%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 4 and strengthened 10 clauses in 756648 steps
c [elim-14-1] rescheduled 25 variables 0% by backward subsumption
c [elim-14-2] eliminated 5 variables 0% in round 2 in 25602 steps
c [elim-14-2] backward subsumption/strengthening limit 25600
c [elim-14-2-1] backward checking 18 touched variables 0%
c [elim-14-2-1] incomplete backward checking 1 remain 6%
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 25782 steps
c [elim-14-2] fully rescheduled 13331 variables 99%
c [elim-14-3] eliminated 7 variables 0% in round 3 in 21184770 steps
c [elim-14-3] backward subsumption/strengthening limit 21184700
c [elim-14-3-1] backward checking 83 touched variables 1%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 275545 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 80 = 1% variables out of 13404 scheduled
c [elim-14] 80 < 1/100 * 13404 = 134 considered unsuccessful
c [bca-14] limit of 10000000 steps and 116883 added (scaled 2)
c [bca-14] 9446 out of 26650 literals actually usable 35%
c [bca-14] added 4 blocked clauses in 154879 steps
c [sort-queue-18] sorted 8348 enqueued variables after 1408544 conflicts
c [score-dist-18] active 4976 (37%), one 7706 (58%), zero 642 (5%)
c [score-dist-18] max exp 725, different 454 (63%)
c [score-dist-18] median active exp 619, avg 563.4
c [simplification-18] removed 260 variables 1.9% (13324 remain 16%)
c [simplification-18] removed 1280 irredundant clauses 2.2% (58025 remain 22%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 122872 = 368616 / 3
c [simplification-18] new conflict interval 491488
c [simplification-18] penalized conflict interval 491488 = 1 * 491488
c [simplification-18] hard conflict limit 2145776 (soft 1900032 + delta 245744)
c [simplification-18] new conflict limit 1900032 (hard 2145776)
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 -  497.4   13324    58025   1445049  121523  32897 17672   19    82   38  22%   1024  -17   17   22   77%
c -  517.4   13324    58025   1496860  121089  32963 17679   25   114   59  22%   1024    7   28   23  120%
c -  535.6   13324    58025   1551952  124785  33009 17683   23   116   59  20%   1024   14   15   23   67%
c -  552.5   13324    58025   1604181  132207  33013 17683   14   147   61   9%   1024   21   14   18   80%
c -  575.1   13324    58025   1652281  123229  33068 17689   26    98   59  27%   1024  -17   29   21  139%
c -  597.2   13324    58025   1712105  127950  33127 17695   26   105   41  24%   1024    1   27   22  121%
c -  618.4   13324    58025   1770007  131393  33168 17698   24    91   41  26%   1024  -11   27   23  117%
c -  635.1   13324    58025   1827966  136845  33202 17699   15   113   42  13%   1024   19   16   22   73%
c -  658.4   13324    58025   1881738  133360  33268 17703   25    79   66  31%   1024  -17   24   23  101%
c 
c [simplification-19] limit 1900032 conflicts (hard 2145776) hit after 1900032 conflicts
c [quatres-15] found 42980 quaternary clauses 35% in total
c [quatres-15-1] removed 4 duplicate quaternary clauses
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 453 single-self-subsuming ternary resolvents
c [quatres-15-2] added 452 quaternary resolvents
c [ternres-14] limit 178287068 with penalty 0 = 0 + 0
c [ternres-14] all 13324 free variables schedulable
c [ternres-14] 1086 ternary resolvents (4 bin, 1082 trn)
c [ternres-14] fully completed ternary resolution
c [simpleprobe-7] all 13324 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-75] removed 10 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 10 variables, found 6433 hbrs, 6 units
c [unhide-19] limit 20000000 with penalty 0 = 0 + 0
c [unhide-19-68] 0 units, 4 failed, 5267 tauts, 0 hbrs, 105634 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 127 transitive binary clauses
c [cce-7] limit of 222858835 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 43
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 39
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 38
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 37
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 32
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 30
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 29
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 28
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 27
c [cce-7-1] eliminated 2 clauses out of 20 (10%) of length 26
c [cce-7-1] eliminated 7 clauses out of 24 (29%) of length 25
c [cce-7-1] eliminated 10 clauses out of 27 (37%) of length 24
c [cce-7-1] eliminated 5 clauses out of 53 (9%) of length 22
c [cce-7-1] eliminated 7 clauses out of 57 (12%) of length 21
c [cce-7-1] eliminated 7 clauses out of 50 (14%) of length 20
c [cce-7-1] eliminated 5 clauses out of 60 (8%) of length 19
c [cce-7-1] eliminated 6 clauses out of 56 (11%) of length 18
c [cce-7-1] eliminated 3 clauses out of 76 (4%) of length 17
c [cce-7-1] eliminated 5 clauses out of 62 (8%) of length 16
c [cce-7-1] eliminated 9 clauses out of 93 (10%) of length 15
c [cce-7-1] eliminated 4 clauses out of 92 (4%) of length 14
c [cce-7-1] eliminated 4 clauses out of 81 (5%) of length 13
c [cce-7-1] eliminated 5 clauses out of 106 (5%) of length 12
c [cce-7-1] eliminated 10 clauses out of 2405 (0%) of length 11
c [cce-7-1] eliminated 9 clauses out of 337 (3%) of length 10
c [cce-7-1] eliminated 19 clauses out of 1775 (1%) of length 9
c [cce-7-1] eliminated 20 clauses out of 569 (4%) of length 8
c [cce-7-1] eliminated 16 clauses out of 819 (2%) of length 7
c [cce-7-1] eliminated 29 clauses out of 765 (4%) of length 6
c [cce-7-1] eliminated 41 clauses out of 1037 (4%) of length 5
c [cce-7-1] eliminated 132 clauses out of 11918 (1%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 388 large clauses in 35811039 steps
c [cce-7-1] allowing another 17905519 steps for small clauses
c [cce-7-1] scheduling 29650 clauses = 14569 binary + 15081 ternary
c [cce-7-1] tried to eliminate 29650 small clauses 100%
c [cce-7-1] eliminated 63 binary clauses 0%
c [cce-7-1] eliminated 187 ternary clauses 1%
c [cce-7-1] eliminated 250 small clauses 1%
c [cce-7-1] eliminated 250 small clauses in 61798445 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 638 covered clauses in round 1
c [cce-7-2] eliminated 2 clauses out of 43 (5%) of length 20
c [cce-7-2] eliminated 2 clauses out of 57 (4%) of length 16
c [cce-7-2] eliminated 1 clauses out of 84 (1%) of length 15
c [cce-7-2] eliminated 2 clauses out of 101 (2%) of length 12
c [cce-7-2] eliminated 1 clauses out of 2395 (0%) of length 11
c [cce-7-2] eliminated 2 clauses out of 328 (1%) of length 10
c [cce-7-2] eliminated 2 clauses out of 549 (0%) of length 8
c [cce-7-2] eliminated 4 clauses out of 803 (0%) of length 7
c [cce-7-2] eliminated 5 clauses out of 736 (1%) of length 6
c [cce-7-2] eliminated 7 clauses out of 996 (1%) of length 5
c [cce-7-2] eliminated 30 clauses out of 11786 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 58 large clauses in 33709500 steps
c [cce-7-2] allowing another 16854750 steps for small clauses
c [cce-7-2] scheduling 29400 clauses = 14506 binary + 14894 ternary
c [cce-7-2] tried to eliminate 29400 small clauses 100%
c [cce-7-2] eliminated 3 binary clauses 0%
c [cce-7-2] eliminated 6 ternary clauses 0%
c [cce-7-2] eliminated 9 small clauses 0%
c [cce-7-2] eliminated 9 small clauses in 59212182 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 67 covered clauses in round 2
c [cce-7-3] eliminated 3 clauses out of 11756 (0%) of length 4
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] eliminated 3 large clauses in 33539382 steps
c [cce-7-3] allowing another 16769691 steps for small clauses
c [cce-7-3] scheduling 29391 clauses = 14503 binary + 14888 ternary
c [cce-7-3] tried to eliminate 29391 small clauses 100%
c [cce-7-3] eliminated 1 ternary clauses 0%
c [cce-7-3] eliminated 1 small clauses 0%
c [cce-7-3] eliminated 1 small clauses in 59099426 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 4 covered clauses in round 3
c [cce-7] eliminated 709 covered clauses in TOTAL during 3 rounds
c [bca-15] limit of 10000000 steps and 115295 added (scaled 2)
c [bca-15] 8917 out of 26626 literals actually usable 33%
c [bca-15] added 4 blocked clauses in 171115 steps
c [sweep-13] limit 26743060 penalty 1 = 1 + 0
c [sweep-13-1] 4661 pos 46.0% + 5474 neg 54.0% = 10135 sched 76.1% ret 3177
c [sweep-13-1] 26777814 steps 625 queries 105.87 avg class size
c [sweep-13-1] 17931 decisions 628 SAT calls 70.71 avg env size
c [sweep-13-1] 2149 variables remain 16% (11163 retained 84%)
c [decomp-76] removed 3 variables
c [sweep-13-1] removed 3 vars (0 failed, 3 eqs, 7 impls)
c [sweep-13] 3 < 1/1000 * 13312 = 13 considered unsuccessful
c [sweep-13] removed 3 vars in TOTAL (1 rounds, 624 queries)
c [sort-queue-19] sorted 6624 enqueued variables after 1900032 conflicts
c [score-dist-19] active 6685 (50%), one 6072 (46%), zero 552 (4%)
c [score-dist-19] max exp 918, different 517 (56%)
c [score-dist-19] median active exp 823, avg 742.2
c [simplification-19] removed 15 variables 0.1% (13309 remain 16%)
c [simplification-19] removed 799 irredundant clauses 1.4% (57226 remain 22%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 245744 = 491488 / 2
c [simplification-19] new conflict interval 737232
c [simplification-19] penalized conflict interval 737232 = 1 * 737232
c [simplification-19] hard conflict limit 3005880 (soft 2637264 + delta 368616)
c [simplification-19] new conflict limit 2637264 (hard 3005880)
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 -  688.1   13309    57226   1941299  137770  34945 19093   22   102   41  21%   1024   10   13   23   56%
c -  711.1   13309    57226   2000343  138838  35031 19095   24    99   65  24%   1024    7   16   23   69%
c -  734.8   13309    57226   2060383  141915  35091 19098   14    88   65  16%   1024  -10   15   23   65%
c -  762.4   13309    57226   2119960  142478  35132 19102   28    96   65  29%   1024    2   26   22  116%
c -  789.8   13309    57226   2181236  143137  35176 19102   26   102   64  26%   1024   -7   31   24  134%
c -  814.5   13309    57226   2245374  147243  35233 19106   26   101   45  26%   1024   -5   30   26  117%
c -  838.0   13309    57226   2307325  151906  35268 19108   25   134   45  19%   1024   20   17   26   66%
c -  859.1   13309    57226   2367074  155753  35307 19108   20   127   46  16%   1024   10   20   25   80%
c -  883.3   13309    57226   2425323  154209  35360 19112   29   134   73  22%   1024   18   33   26  124%
c -  907.2   13309    57226   2487138  158148  35393 19115   27   136   74  20%   1024   12   25   26   98%
c -  929.5   13309    57226   2547513  159384  35433 19115   27   123   74  22%   1024    5   25   26   96%
c -  953.7   13309    57226   2609428  161468  35482 19119   23   128   74  18%   1024    9   28   26  107%
c 
c [simplification-20] limit 2637264 conflicts (hard 3005880) hit after 2647001 conflicts
c [quatres-16] found 44187 quaternary clauses 31% in total
c [quatres-16-1] removed 8 duplicate quaternary clauses
c [quatres-16-1] added 2 double-self-subsuming ternary resolvents
c [quatres-16-2] added 505 single-self-subsuming ternary resolvents
c [quatres-16-2] added 491 quaternary resolvents
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 13309 free variables schedulable
c [ternres-15] 1721 ternary resolvents (4 bin, 1717 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-6] limit 3125000 penalty 4 = 4 + 0
c [gauss-6] extracted 17345 xors of average arity 3.0
c [gauss-6] connected 52035 occurrences of 1900 variables (average 27.4)
c [gauss-6] limit 3125000 penalty 4 = 4 + 0
c [gauss-6] connected 18504 occurrences of 1900 variables (average 9.7)
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-7] limit 26857329 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 19998 literals 75%
c [treelook-7] scheduling used 785527 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 26857329 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 19049374 steps
c [treelook-7] fully completed tree based probing
c [decomp-78] removed 13 variables
c [treelook-7] removed 81 variables, found 5871 hbrs
c [unhide-20] limit 20000000 with penalty 0 = 0 + 0
c [unhide-20-75] 6 units, 62 failed, 3293 tauts, 0 hbrs, 245347 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 153 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 6714332350 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 1 clauses out of 103 (1%) of length 12
c [cce-8-1] eliminated 2 clauses out of 2379 (0%) of length 11
c [cce-8-1] eliminated 2 clauses out of 332 (1%) of length 10
c [cce-8-1] eliminated 3 clauses out of 1751 (0%) of length 9
c [cce-8-1] eliminated 2 clauses out of 546 (0%) of length 8
c [cce-8-1] eliminated 2 clauses out of 788 (0%) of length 7
c [cce-8-1] eliminated 2 clauses out of 736 (0%) of length 6
c [cce-8-1] eliminated 4 clauses out of 962 (0%) of length 5
c [cce-8-1] eliminated 63 clauses out of 11301 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 81 large clauses in 27998339 steps
c [cce-8-1] allowing another 13999169 steps for small clauses
c [cce-8-1] scheduling 22126 clauses = 14597 binary + 7529 ternary
c [cce-8-1] tried to eliminate 22126 small clauses 100%
c [cce-8-1] eliminated 39 binary clauses 0%
c [cce-8-1] eliminated 89 ternary clauses 1%
c [cce-8-1] eliminated 128 small clauses 1%
c [cce-8-1] eliminated 201 small clauses in 43032703 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 282 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 13773342 steps for small clauses
c [cce-8-2] scheduling 21998 clauses = 14558 binary + 7440 ternary
c [cce-8-2] tried to eliminate 21998 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 282 covered clauses in TOTAL during 2 rounds
c [cce-8] 282 < 1/100 * 56643 = 566 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 13167 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 168 variables 1% in round 1 in 20478007 steps
c [elim-15-1] backward subsumption/strengthening limit 20478000
c [elim-15-1-1] backward checking 552 touched variables 4%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 772977 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 168 = 1% variables out of 13167 scheduled
c [bca-16] limit of 10000000 steps and 113101 added (scaled 2)
c [bca-16] 8463 out of 26000 literals actually usable 33%
c [bca-16] added 6 blocked clauses in 212690 steps
c [sort-queue-20] sorted 8237 enqueued variables after 2647001 conflicts
c [score-dist-20] active 4762 (37%), one 7729 (59%), zero 508 (4%)
c [score-dist-20] max exp 675, different 443 (66%)
c [score-dist-20] median active exp 599, avg 518.2
c [simplification-20] removed 310 variables 2.3% (12999 remain 15%)
c [simplification-20] removed 1094 irredundant clauses 1.9% (56132 remain 21%)
c [simplification-20] maximum reduction of 2% = max (2%, 2%)
c [simplification-20] geometric conflict interval increment 245744 = 737232 / 3
c [simplification-20] new conflict interval 982976
c [simplification-20] penalized conflict interval 982976 = 1 * 982976
c [simplification-20] hard conflict limit 4121465 (soft 3629977 + delta 491488)
c [simplification-20] new conflict limit 3629977 (hard 4121465)
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 -  990.2   12999    56132   2673529  159166  35710 18420   31   117   45  26%   1024   -4   34   28  119%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1564 basic ate = 1041 trn 67% + 523 lrg 33% in 4 updates
c bcas: 16 count, 681 added (1471 skipped), 2049410 steps
c bkwd: tried 202093 clauses, 402011 lits, 1.99 lits/clause
c bkwd: checked 15521415 occs, 76.80 occs/clause, 38.61 occs/lit
c bkwd: subsumed 0 binary, 86 ternary, 873 large
c bkwd: strengthened 14 binary, 12 ternary (100% self), 2149 large (0% self)
c blkd: 6 bces, 13829 removed, 2775250 resolutions, 8078517 steps
c blkd: 9374 blocking literals 5%, 59 pure
c bump: 2700190 bumped seen, 258065500 lits 95.6 on average
c card: 5 count, 1 units, 0 am1, 44793470 steps
c card: 36 rescheduled, 82 eliminated, 4108 resolved, 5243 subsumed
c card: 783 at-most-one constraints found, average size 3.46
c card: 783 at-most-one constraints used 100%, average size 3.46
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: 8 cces, 7881 eliminated, 6577 ate 83%, 1304 abce 17%
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: 974644 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 189 gcs, 0 rescored clauses, 1420 rescored vars
c dcps: 78 decompositions, 4516 equivalent 5%
c deco: 1854 decision-only clauses 0%, 47% reduction
c decs: 11817168 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 63791 eliminated 72%, 331 pure 1%
c elms: 31 rounds, 2.1 rounds/bve
c elms: 61197 small 96%, 2204 large 3%
c elms: 169790 tried small, 61197 succeeded 36%, 108593 failed 64%
c elms: 6620 subsumed, 12502 strengthened, 466 blocked
c elms: 6099680 copies, 8066985 resolutions, 6320755 ipos
c elms: 5745563 subchks, 5720103 strchks
c gaus: 6 extractions, 60380 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 26 binary and 0 ternary equations
c gaus: 1 gc, 19391564 steps, 9695782 extr 50%, 8449765 elim 44%
c glue: 21.9 orig avg, 21.9 real avg, 4.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 75335 = 23867 simple 32% + 44283 trn 59% + 7185 lrg 10%, 2638 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2700190 clauses, 55.1 length
c lrnd: 148798390 lits = 191758459 orig - 42960069 removed 22%
c lrnd: 747846 uips 28%, 1657319 flips 61%
c mins: 2663674 mins 99%, 1606 bin 0%, 33055 size 1%
c mins: 171768664 poisoned searches, 40600080 hits, 24% hit rate
c mins: 319368140 used twice searches, 31590223 hits, 10% hit rate
c move: moved 13621, 2194 bin 16%, 11427 trn 84%
c otfs: 11432 driving 30%, 26501 restarting 70%
c otfs: str 37933, 37616 red 99%, 317 irr 1%
c otfs: str 37933, 0 bin 0%, 216 trn 1%, 37717 lrg 99%
c otfs: sub 122, 119 red 98%, 3 irr 2%
c otfs: sub 122, 0 bin 0%, 6 trn 5%, 116 lrg 95%
c phas: 13 computed, 25173 set, 5217 pos (21%), 19956 neg (79%)
c prbs: 6 basic, 471175 probed, 1337 failed, 245 lifted
c prbs: 7 simple, 247002 probed, 132 failed, 1627 eqs
c prbs: 7 treelook, 20446 probed, 57 failed, 0 lifted
c prom: 589444 locked 13% out of 4514647 tried
c prps: 1465503186 props, 123 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 16 count, 78105 quat, 10940 self1, 23 self2, 81 dup
c queu: 20 sorted, 11817168 next (2537877 steps 0.21)
c queu: 265253460 enq (275538207 steps 1.04), 258065500 deq 97%
c redc: 21237 clauses 8%, 273246 tried 10%, 6 sat 0%
c redc: 37174 lits 1%, 3265178 tried 2%, 6 sat 0%
c redc: 1329 times jump level reduced, 10.7 levels on average
c reds: 51 count, 52916.2 conflicts per reduce
c reds: 0 memlim 0%, 51 arith 100%
c reds: 1910977 collected 80%, 488310 retired 20%
c rmbd: 2116 removed, 1791 red 85%
c rsts: 58982 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 20 count, 19 confs 95%, 0 vars 0%
c simp: 0 its 0%, 1 bin 5%, 0 trns 0%
c subl: 2700190 count (2638603 tried 1.0), 76971 sub out of 2689614 (2.9%)
c swps: 13 count, 17 rounds, 9571 queries (563.0/round)
c swps: 9506 sat calls, 168 unsat (1.4% success rate)
c swps: 136951 decisions 14.4, 12894 conflicts 1.4
c swps; 268.3 avg class size, 35.2 avg environment size
c swps: 0 failed, 319 impls, 225 equivs
c swp0: 3185 type 0 queries, 180 unsat (5.7%), 3150 sat (98.9%)
c swp1: 6386 type 1 queries, 833 unsat (13.0%), 6196 sat (97.0%)
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: 29038026 calls to obtain time
c tops: 7457 fixed 8%, 22 its, 122669.45 confs/it
c trds: 16 transitive reductions, 1901 removed, 8 failed
c trds: 265645 nodes, 208928 edges, 31420123 steps
c trim: 841126 words, 3.2 MB
c trnr: 15 count, 118 bin, 32473 trn, 191748410 steps
c unhd: 20 count, 75 rounds, 131384042 steps
c unhd: 1090 non-trivial sccs of average size 2.1
c unhd: 42 units, 40 bin, 1 trn, 1 lrg
c unhd: 251 failed, 240 stamp, 0 lits, 9 bin, 2 trn, 1 lrg
c unhd: 31931 tauts, 378 bin 1%, 5347 trn 17%, 2882 lrg 9%
c unhd: 31931 tauts, 23324 stamp 73%, 30927 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 823096 str, 40 bin 0%, 2364 trn 0%, 820692 lrg 100%, 810780 red 99%
c vars: 12999 remaining 15% and 75764 removed 85% out of 88763
c vars: 7457 fixed 8%, 63791 eliminated 72%, 4516 equivalent 5%
c vsts: 27864034211 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 19.0 search visits per propagation, 10213.4 per conflict
c wchs: 8797361209 pushed, 26078929 enlarged, 291 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2767719       1910977        488310     152147655      29060315       1659632
c 
c  0 0        204251   7     14777   1         0   0 112817506  74  17167605  59    673127  41     4.3
c  1 5         78644   3     51047   3     17639   4  12693581   8<  2680910   9<   137090   8     0.4
c  2 6        307200  11    225009  12     61439  13  14340958   9   3670535  13    261731  16<    1.3
c  3 9        531796  19    409794  21     97362  20   5393377   4   2051899   7    190120  11     4.9
c  4 14       562936  20<   433429  23<    97348  20<  3093466   2   1425332   5    152899   9     7.1
c  5 21       453073  16    341503  18     76159  16   2082481   1   1054450   4    126419   8     5.7
c  6 30       293032  11    215283  11     55257  11    968204   1    539002   2     63791   4     5.2
c  7 41       178287   6    124488   7     39457   8    451873   0    278900   1     33375   2     3.9
c  8 54        90622   3     58475   3     23632   5    187351   0    118195   0     12773   1     2.3
c  9 69        39754   1     23385   1     11609   2     71369   0     44016   0      4845   0     1.0
c 10 86        24657   1     12633   1      7152   1     43043   0     27014   0      3309   0     0.7
c 11 126        3467   0      1154   0      1256   0      4446   0      2457   0       153   0     0.2
c 
c avg                  4.0           4.3           4.5           0.6           1.2           2.0
c std                  2.1           1.8           2.0           1.3           1.8           2.1
c 
c   26.874   3% unhide
c   24.402   2% bump
c   13.091   1% probe
c   11.812   1% elim
c   10.657   1% sweep
c    8.480   1% cce
c    7.195   1% decide
c 
c   12.324 < 1% rest (below)
c 
c    4.243   0% quatres
c    2.000   0% transred
c    1.326   0% rescore
c    1.296   0% ternres
c    1.153   0% gauss
c    1.141   0% bca
c    1.017   0% block
c    0.149   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    2.564   0% preprocessing     3%
c   82.860   8% inprocessing     97%
c ==================================
c   85.424   9% simplifying
c  914.460  91% search
c ==================================
c  999.885 100% all
c 
c       2698728 conflicts,        2699.0 confs/sec
c          6125 ternaries,         440.6 confs/ternary
c          1685 binaries,         1601.6 confs/binary
c            22 iterations,     122669.5 confs/iteration
c 
c            51 reductions,          0.1 redus/sec,  52916.2 confs/reduction
c         58982 restarts,           59.0 rests/sec,     45.8 confs/restart
c      11817168 decisions,       11818.5 decis/sec,      4.4 decis/conflict
c    1465503186 propagations,  1465671.1 props/sec,    124.0 props/decision
c 
c 999.9 seconds, 132.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
