c launch: /data/cnf/sc2014/app/SAT_dat.k85-24_1_rule_3.cnf.bz2
c host: atom11
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/SAT_dat.k85-24_1_rule_3.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k85-24_1_rule_3.cnf.bz2
c no embedded options
c found 'p cnf 1376701 5395102' header
c read 1376701 variables, 5395102 clauses, 13543383 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 1333833 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0 1333833  5352100         0       0      0     0    0     0  276   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1338025 based on 5352100 irredundant clauses
c [card-1] found 1157 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1338025 for elimination
c [card-1] 1157 out of 1157 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 297359 variables
c [simpleprobe-1] all 1079342 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 8778580 based on 4389290 irredundant clauses
c [decomp-2] removed 5368 variables
c [simpleprobe-1] 881094 variables remain 82% (192880 retained 18%)
c [simpleprobe-1] removed 5368 variables, found 10747 hbrs, 950 units
c [unhide-1] limit 272568 based on 4361090 irredundant clauses
c [unhide-1-1] 1426 units, 1036 failed, 9528 tauts, 0 hbrs, 54975 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1067971 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 986657 not tried 92% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 81322 = 8% variables out of 1067971 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3883753 negative 95.2% of 4079881 except 196128 4.8%
c [phase-count-1] 3820819 positive 93.7% of 4079881 except 259062 6.3%
c [phase-1] phase bias: 458362 positive 46%, 528287 negative 54%
c [sort-queue-1] sorted 986649 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 986649 (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 178414 variables 15.3% (986649 remain 74%)
c [simplification-1] removed 1272219 irredundant clauses 23.8% (4079881 remain 76%)
c [simplification-1] maximum reduction of 24% = max (15%, 24%)
c [simplification-1] large reduction 24% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.4  986648  4079881         4       2     10  9268    0     0  249   1%      0    0    0    0 25376%
c i   16.5  986515  4079881        11       6     10  9270    0     0  249   1%      0    0    0    0 24972%
c i   16.5  986463  4079881        12       6     10  9270    0     0  249   1%      0    0    0    0 24874%
c i   16.7  986461  4079881        83      58     18  9277    0     1  249   6%      0    1    1    0 22169%
c i   16.8  986460  4079881       154     116     24  9281    0     2  249   9%      0    2    2    0 20509%
c i   17.0  986305  4079881       232     174     36  9284    0     3  249   9%      0    3    3    0 17426%
c i   17.1  986304  4079881       250     185     38  9288    0     3  249   9%      0    3    3    0 16634%
c i   21.1  986303  4079881       914     693    107  9354    1    22  250   5%      3   22    6    0 8235%
c 
c [simplification-2] limit 1013 conflicts (hard 11000) hit after 1014 conflicts
c [decomp-3] removed 3409 variables
c [simpleprobe-2] 806909 schedulable variables 82%
c [simpleprobe-2] limit 8141504 based on 4070752 irredundant clauses
c [decomp-4] removed 1367 variables
c [simpleprobe-2] 813544 variables remain 83% (168329 retained 17%)
c [simpleprobe-2] removed 1367 variables, found 39685 hbrs, 177 units
c [treelook-1] limit 1016310 based on 4065241 irredundant clauses
c [treelook-1] scheduled 205042 literals 10%
c [treelook-1] scheduling used 1016558 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1016310 based on 4065241 irredundant clauses
c [treelook-1] used 1032004 steps
c [treelook-1] 204886 literals remain 10%
c [treelook-1] 198893 variables remain to probed next time 20%
c [decomp-5] removed 159 variables
c [treelook-1] removed 180 variables, found 4796 hbrs
c [basicprobe-1] limit 32516568 based on 4064571 irredundant clauses
c [basicprobe-1-0] 888450 probes remain 91% after last round
c [basicprobe-1-0] 2931 units = 1768 failed (60%) + 1163 lifted (40%)
c [basicprobe-1-0] removed 8852 variables, found 211823 hbrs
c [unhide-2] limit 254035 based on 4064571 irredundant clauses
c [unhide-2-2] 865 units, 1230 failed, 12928 tauts, 0 hbrs, 36039 literals
c [elim-2] 970398 variables 100% will be scheduled this time
c [elim-2] scheduled 970398 variables 100%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 889565 not tried 92% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 80833 = 8% variables out of 970398 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3637722 negative 95.1% of 3824833 except 187111 4.9%
c [phase-count-2] 3573563 positive 93.4% of 3824833 except 251270 6.6%
c [phase-2] phase bias: 894 positive 36%, 1618 negative 64%
c [sort-queue-2] sorted 869735 enqueued variables after 1014 conflicts
c [score-dist-2] active 19830 (2%), one 0 (0%), zero 869735 (98%)
c [score-dist-2] max exp 507, different 7 (1%)
c [score-dist-2] median active exp 503, avg 503.0
c [simplification-2] removed 96738 variables 9.8% (889565 remain 67%)
c [simplification-2] removed 255048 irredundant clauses 6.3% (3824833 remain 71%)
c [simplification-2] maximum reduction of 10% = max (10%, 6%)
c [simplification-2] large reduction 10% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13014 (soft 3014 + delta 10000)
c [simplification-2] new conflict limit 3014 (hard 13014)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   47.8  889564  3824833      1427     911    144 189090    2    38  244   6%      3   37   14    0 8678%
c i   55.4  889563  3824833      2183    1500    239 189136    3    75  245   4%      5   74    7    0 2915%
c i   56.1  889562  3824833      2216    1525    244 189138    3    77  245   4%      5   76    6    0 2777%
c i   56.2  889530  3824833      2217    1525    244 189138    3    77  245   4%      5   76    6    0 2766%
c i   59.5  889467  3824833      2444    1695    275 189161    3   100  253   3%      4   98    4    0 1878%
c 
c [simplification-3] limit of 196 binary hit after 196 binaries
c [card-2] limit 956208 based on 3824833 irredundant clauses
c [card-2] found 891 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 956208 for elimination
c [card-2] 891 out of 891 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 5272 variables
c [treelook-2] limit 953987 based on 3815951 irredundant clauses
c [treelook-2] scheduled 178673 literals 10%
c [treelook-2] scheduling used 954058 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 953987 based on 3815951 irredundant clauses
c [treelook-2] used 976999 steps
c [treelook-2] 178449 literals remain 10%
c [treelook-2] 111329 variables remain to probed next time 13%
c [decomp-7] removed 88 variables
c [treelook-2] removed 110 variables, found 2974 hbrs
c [unhide-3] limit 238467 based on 3815480 irredundant clauses
c [unhide-3-3] 465 units, 721 failed, 18679 tauts, 0 hbrs, 19955 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 882805 variables 100%
c [elim-3] limit of 18326089 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 630343 not tried 71% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 252463 = 29% variables out of 882805 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3082968 negative 95.0% of 3246149 except 163181 5.0%
c [phase-count-3] 3016017 positive 92.9% of 3246149 except 230132 7.1%
c [phase-3] phase bias: 520 positive 29%, 1297 negative 71%
c [sort-queue-3] sorted 597131 enqueued variables after 2631 conflicts
c [score-dist-3] active 33211 (5%), one 0 (0%), zero 597131 (95%)
c [score-dist-3] max exp 508, different 8 (2%)
c [score-dist-3] median active exp 503, avg 503.4
c [simplification-3] removed 259125 variables 29.1% (630342 remain 47%)
c [simplification-3] removed 578684 irredundant clauses 15.1% (3246149 remain 61%)
c [simplification-3] maximum reduction of 29% = max (29%, 15%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3024 (hard 13014)
c [simplification-3] 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   82.1  630341  3246149      2814    1160    283 114892    3   134  233   2%      4  133    4    0 1715%
c i   84.2  630340  3246149      2994    1300    301 114909    3   148  233   2%      3  145    5    0 1694%
c 
c [simplification-4] limit 3024 conflicts (hard 13014) hit after 3025 conflicts
c [decomp-8] removed 778 variables
c [basicprobe-2] limit 25955888 based on 3244486 irredundant clauses
c [basicprobe-2-0] 487002 probes remain 78% after last round
c [basicprobe-2-0] 1375 units = 1298 failed (94%) + 77 lifted (6%)
c [basicprobe-2-0] removed 1808 variables, found 130701 hbrs
c [unhide-4] limit 202780 based on 3244486 irredundant clauses
c [unhide-4-4] 221 units, 483 failed, 12111 tauts, 0 hbrs, 61949 literals
c [elim-4] 627040 variables 100% will be scheduled this time
c [elim-4] scheduled 627040 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 445481390 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 3149 not tried 1% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 284018 = 45% variables out of 627040 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 2286633 negative 95.6% of 2391533 except 104900 4.4%
c [phase-count-4] 2242145 positive 93.8% of 2391533 except 149388 6.2%
c [phase-4] phase bias: 1088 positive 47%, 1247 negative 53%
c [sort-queue-4] sorted 317690 enqueued variables after 3025 conflicts
c [score-dist-4] active 25332 (7%), one 0 (0%), zero 317690 (93%)
c [score-dist-4] max exp 508, different 8 (2%)
c [score-dist-4] median active exp 503, avg 503.4
c [simplification-4] removed 287318 variables 45.6% (343022 remain 26%)
c [simplification-4] removed 854616 irredundant clauses 26.3% (2391533 remain 45%)
c [simplification-4] maximum reduction of 46% = max (46%, 26%)
c [simplification-4] large reduction 46% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15025 (soft 5025 + delta 10000)
c [simplification-4] new conflict limit 5025 (hard 15025)
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  115.3  343021  2391533      3503     983    222 78976    4   165  212   2%      4  162    6    0 1893%
c i  116.3  343020  2391533      3645    1111    225 78983    4   169  212   2%      3  165    6    0 1803%
c i  117.5  343019  2391533      3794    1249    230 78985    4   176  212   2%      3  171    6    0 1751%
c i  117.7  343018  2391533      3799    1253    230 78985    4   176  212   2%      3  171    6    0 1727%
c i  117.7  343017  2391533      3801    1254    230 78985    4   176  212   2%      3  171    6    0 1720%
c i  117.9  343016  2391533      3812    1264    230 78985    4   176  212   2%      3  172    6    0 1718%
c i  125.1  343015  2391533      4573    1935    267 79015    5   207  213   2%      5  200    9    0 1944%
c i  125.9  343014  2391533      4642    1994    274 79016    5   211  214   2%      4  204    9    0 1896%
c i  128.0  343013  2391533      4860    2156    293 79033    5   218  214   2%      4  210    8    0 1608%
c 
c [simplification-5] limit 5032 conflicts (hard 15025) hit after 5034 conflicts
c [quatres-1] found 298512 quaternary clauses 40% in total
c [quatres-1-1] removed 8 duplicate quaternary clauses
c [quatres-1-1] added 107 double-self-subsuming ternary resolvents
c [quatres-1-2] added 2182 single-self-subsuming ternary resolvents
c [quatres-1-2] added 9928 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 19207837 with penalty 1 = 0 + 1
c [ternres-1] all 343013 free variables schedulable
c [ternres-1] 79224 ternary resolvents (305 bin, 78919 trn)
c [ternres-1] 84381 variables remain 25% (258632 retained 75%)
c [gauss-1] limit 1195703 based on 2391406 irredundant clauses
c [gauss-1] extracted 6431 xors of average arity 3.0
c [gauss-1] connected 19090 occurrences of 7375 variables (average 2.6)
c [gauss-1] limit 1195679 based on 2391358 irredundant clauses
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1887 variables
c [simpleprobe-3] 283917 schedulable variables 83%
c [simpleprobe-3] limit 15366271 penalty 1 = 0 + 1
c [decomp-10] removed 660 variables
c [simpleprobe-3] 275537 variables remain 81% (64929 retained 19%)
c [simpleprobe-3] removed 660 variables, found 39325 hbrs, 125 units
c [unhide-5] limit 192078 with penalty 3 = 0 + 3
c [unhide-5-5] 316 units, 343 failed, 45859 tauts, 0 hbrs, 59170 literals
c [transred-1] limit 2341622 based on 2341622 irredundant clauses
c [transred-1] removed 1103 transitive binary clauses
c [transred-1] found 34 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 339677 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 384156785 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 26409 blocked clauses
c [cce-1] limit of 19207839 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 28
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 27
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 26
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 25
c [cce-1-1] eliminated 3 clauses out of 6 (50%) of length 24
c [cce-1-1] eliminated 4 clauses out of 9 (44%) of length 23
c [cce-1-1] eliminated 3 clauses out of 9 (33%) of length 22
c [cce-1-1] eliminated 4 clauses out of 12 (33%) of length 21
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 20
c [cce-1-1] eliminated 8 clauses out of 9 (89%) of length 19
c [cce-1-1] eliminated 24 clauses out of 795 (3%) of length 18
c [cce-1-1] eliminated 390 clauses out of 1044 (37%) of length 17
c [cce-1-1] eliminated 291 clauses out of 937 (31%) of length 16
c [cce-1-1] eliminated 273 clauses out of 1923 (14%) of length 15
c [cce-1-1] eliminated 115 clauses out of 2473 (5%) of length 14
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1125 large clauses in 19207952 steps
c [cce-1-1] allowing another 9603976 steps for small clauses
c [cce-1-1] scheduling 1312086 clauses = 1039103 binary + 272983 ternary
c [cce-1-1] tried to eliminate 4367 small clauses 0%
c [cce-1-1] eliminated 886 binary clauses 0%
c [cce-1-1] eliminated 189 ternary clauses 0%
c [cce-1-1] eliminated 1075 small clauses 0%
c [cce-1-1] eliminated 1075 small clauses in 19207841 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2200 covered clauses in round 1
c [cce-1] eliminated 2200 covered clauses in TOTAL during 1 rounds
c [cce-1] 2200 < 1/100 * 2307421 = 23074 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 339178 variables 100%
c [elim-5] limit of 76831357 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 85964 not tried 25% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 17911 = 5% variables out of 339178 scheduled
c [bca-1] limit of 10000000 steps and 4526620 added (scaled 2)
c [bca-1] 612254 out of 642536 literals actually usable 95%
c [bca-1] added 8396 blocked clauses in 1936726 steps
c [sweep-1] limit 4526120 based on 2263060 irredundant clauses
c [sweep-1-1] 128268 pos 39.9% + 192999 neg 60.1% = 321267 sched 100.0% ret 0
c [sweep-1-1] 4536454 steps 85 queries 103192.72 avg class size
c [sweep-1-1] 1374 decisions 78 SAT calls 32.90 avg env size
c [sweep-1-1] 320978 variables remain 100% (285 retained 0%)
c [decomp-11] removed 545 variables
c [sweep-1-1] removed 545 vars (0 failed, 21 eqs, 26 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 545 vars in TOTAL (1 rounds, 84 queries)
c [phase-count-5] 2161581 negative 95.6% of 2261865 except 100284 4.4%
c [phase-count-5] 2138078 positive 94.5% of 2261865 except 123787 5.5%
c [phase-5] phase bias: 111 positive 47%, 127 negative 53%
c [sort-queue-5] sorted 270868 enqueued variables after 5034 conflicts
c [score-dist-5] active 49854 (16%), one 0 (0%), zero 270868 (84%)
c [score-dist-5] max exp 509, different 9 (2%)
c [score-dist-5] median active exp 503, avg 503.5
c [simplification-5] removed 22291 variables 6.5% (320722 remain 24%)
c [simplification-5] removed 129668 irredundant clauses 5.4% (2261865 remain 42%)
c [simplification-5] maximum reduction of 6% = max (6%, 5%)
c [simplification-5] large reduction 6% >= 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 17034 (soft 7034 + delta 10000)
c [simplification-5] new conflict limit 7034 (hard 17034)
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  158.0  320721  2261865      5446   10408  61813 111362    6   233  215   2%      4  223   10    1 1696%
c i  159.6  320720  2261865      5737   10674  61824 111364    7   236  215   3%      4  226   18    1 2698%
c 
c [simplification-6] limit 7034 conflicts (hard 17034) hit after 7035 conflicts
c [quatres-2] found 304227 quaternary clauses 41% in total
c [quatres-2-1] removed 32 duplicate quaternary clauses
c [quatres-2-1] added 14 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1956 single-self-subsuming ternary resolvents
c [quatres-2-2] added 7333 quaternary resolvents
c [ternres-2] limit 9047032 based on 2261758 irredundant clauses
c [ternres-2] 78471 schedulable variables 24%
c [ternres-2] 49492 ternary resolvents (1992 bin, 47500 trn)
c [ternres-2] 41056 variables remain 13% (279664 retained 87%)
c [card-3] limit 627075 penalty 3 = 2 + 1
c [card-3] found 354 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 627075 for elimination
c [card-3] 354 out of 354 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 671 variables
c [treelook-3] limit 565266 based on 2261064 irredundant clauses
c [treelook-3] scheduled 67944 literals 11%
c [treelook-3] scheduling used 565643 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 565266 based on 2261064 irredundant clauses
c [treelook-3] used 570390 steps
c [treelook-3] 67810 literals remain 11%
c [treelook-3] 39496 variables remain to probed next time 12%
c [decomp-13] removed 13 variables
c [treelook-3] removed 19 variables, found 980 hbrs
c [unhide-6] limit 250830 with penalty 3 = 0 + 3
c [unhide-6-6] 268 units, 557 failed, 9470 tauts, 0 hbrs, 42138 literals
c [transred-2] limit 2259179 based on 2259179 irredundant clauses
c [transred-2] removed 1015 transitive binary clauses
c [transred-2] found 22 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 319298 variables 100%
c [block-2] limit of 50166076 steps penalty 1 = 0 + 1
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 9360 blocked clauses
c [block-2] 9360 < 1/100 * 2258454 = 22584 considered unsuccessful
c [elim-6] 3049 variables 1% will be scheduled this time
c [elim-6] scheduled 3049 variables 1%
c [elim-6] limit of 100332152 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1744 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 64 = 2% variables out of 3049 scheduled
c [elim-6] 64 < 1/100 * 3049 = 30 considered unsuccessful
c [bca-2] limit of 10000000 steps and 4475694 added (scaled 2)
c [bca-2] 594158 out of 638034 literals actually usable 93%
c [bca-2] added 528 blocked clauses in 1862442 steps
c [sweep-2] limit 4470996 based on 2235498 irredundant clauses
c [sweep-2-1] 127966 pos 40.1% + 190787 neg 59.9% = 318753 sched 99.9% ret 263
c [sweep-2-1] 4511249 steps 100 queries 93632.75 avg class size
c [sweep-2-1] 1212 decisions 83 SAT calls 32.83 avg env size
c [sweep-2-1] 318342 variables remain 100% (674 retained 0%)
c [decomp-14] removed 606 variables
c [sweep-2-1] removed 606 vars (0 failed, 17 eqs, 25 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 606 vars in TOTAL (1 rounds, 99 queries)
c [phase-count-6] 2133646 negative 95.5% of 2234128 except 100482 4.5%
c [phase-count-6] 2110899 positive 94.5% of 2234128 except 123229 5.5%
c [phase-6] phase bias: 17 positive 29%, 42 negative 71%
c [sort-queue-6] sorted 263048 enqueued variables after 7035 conflicts
c [score-dist-6] active 55362 (17%), one 0 (0%), zero 263048 (83%)
c [score-dist-6] max exp 511, different 11 (2%)
c [score-dist-6] median active exp 504, avg 504.1
c [simplification-6] removed 2310 variables 0.7% (318410 remain 24%)
c [simplification-6] removed 27735 irredundant clauses 1.2% (2234128 remain 42%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 10000
c [simplification-6] penalized conflict interval 10000 = 1 * 10000
c [simplification-6] hard conflict limit 27035 (soft 17035 + delta 10000)
c [simplification-6] new conflict limit 17035 (hard 27035)
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  191.8  318409  2234128      8546   19438  96306 107756   18   163  217  11%     28  145   33    2 1760%
c i  192.2  318408  2234128      8660   19533  96308 107760   18   160  217  11%     25  142   30    2 1562%
c i  227.7  318407  2234128     14717   24663  96456 107828   27   174  220  16%     75  145   19    5  396%
c 
c [simplification-7] limit 17035 conflicts (hard 27035) hit after 17035 conflicts
c [quatres-3] found 311137 quaternary clauses 43% in total
c [quatres-3-1] removed 12 duplicate quaternary clauses
c [quatres-3-1] added 20 double-self-subsuming ternary resolvents
c [quatres-3-2] added 802 single-self-subsuming ternary resolvents
c [quatres-3-2] added 3367 quaternary resolvents
c [ternres-3] limit 11539756 with penalty 1 = 0 + 1
c [ternres-3] 40428 schedulable variables 13%
c [ternres-3] 63188 ternary resolvents (2596 bin, 60592 trn)
c [ternres-3] 10949 variables remain 3% (307458 retained 97%)
c [gauss-2] limit 1153975 penalty 2 = 1 + 1
c [gauss-2] extracted 4836 xors of average arity 3.0
c [gauss-2] connected 14428 occurrences of 5590 variables (average 2.6)
c [gauss-2] limit 1153975 penalty 2 = 1 + 1
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 786 variables
c [basicprobe-3] limit 57698780 penalty 1 = 0 + 1
c [basicprobe-3-0] 163373 probes remain 52% after last round
c [basicprobe-3-0] 4328 units = 4066 failed (94%) + 262 lifted (6%)
c [basicprobe-3-0] removed 6365 variables, found 216634 hbrs
c [bate-1] eliminated 5001 asymmetric tautologies during probing
c [unhide-7] limit 576987 with penalty 3 = 0 + 3
c [unhide-7-7] 127 units, 249 failed, 30541 tauts, 0 hbrs, 34495 literals
c [transred-3] limit 2127791 based on 2127791 irredundant clauses
c [transred-3] removed 1335 transitive binary clauses
c [transred-3] found 6 units
c [cce-2] limit of 28849390 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 23
c [cce-2-1] eliminated 9 clauses out of 12 (75%) of length 22
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 19
c [cce-2-1] eliminated 1 clauses out of 720 (0%) of length 18
c [cce-2-1] eliminated 9 clauses out of 644 (1%) of length 17
c [cce-2-1] eliminated 3 clauses out of 473 (1%) of length 16
c [cce-2-1] eliminated 51 clauses out of 1250 (4%) of length 15
c [cce-2-1] eliminated 591 clauses out of 2069 (29%) of length 14
c [cce-2-1] eliminated 582 clauses out of 4716 (12%) of length 13
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1250 large clauses in 28849410 steps
c [cce-2-1] allowing another 14424705 steps for small clauses
c [cce-2-1] scheduling 1187599 clauses = 920118 binary + 267481 ternary
c [cce-2-1] tried to eliminate 5317 small clauses 0%
c [cce-2-1] eliminated 802 binary clauses 0%
c [cce-2-1] eliminated 279 ternary clauses 0%
c [cce-2-1] eliminated 1081 small clauses 0%
c [cce-2-1] eliminated 4374 small clauses in 28849394 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5624 covered clauses in round 1
c [cce-2] eliminated 5624 covered clauses in TOTAL during 1 rounds
c [cce-2] 5624 < 1/100 * 2127356 = 21273 considered unsuccessful
c [bca-3] limit of 10000000 steps and 4248426 added (scaled 2)
c [bca-3] 568973 out of 621780 literals actually usable 92%
c [bca-3] added 717 blocked clauses in 1725645 steps
c [sweep-3] limit 4243464 based on 2121732 irredundant clauses
c [sweep-3-1] 123205 pos 39.7% + 187029 neg 60.3% = 310234 sched 99.8% ret 655
c [sweep-3-1] 4271960 steps 92 queries 85619.04 avg class size
c [sweep-3-1] 1186 decisions 84 SAT calls 35.10 avg env size
c [sweep-3-1] 309756 variables remain 100% (1132 retained 0%)
c [decomp-16] removed 5685 variables
c [sweep-3-1] removed 5685 vars (0 failed, 12 eqs, 18 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 5685 vars in TOTAL (1 rounds, 91 queries)
c [phase-count-7] 2010474 negative 95.2% of 2112741 except 102267 4.8%
c [phase-count-7] 1992195 positive 94.3% of 2112741 except 120546 5.7%
c [phase-7] phase bias: 90 positive 62%, 55 negative 38%
c [sort-queue-7] sorted 241741 enqueued variables after 17035 conflicts
c [score-dist-7] active 63463 (21%), one 0 (0%), zero 241741 (79%)
c [score-dist-7] max exp 514, different 14 (3%)
c [score-dist-7] median active exp 504, avg 505.5
c [simplification-7] removed 13203 variables 4.1% (305204 remain 23%)
c [simplification-7] removed 121387 irredundant clauses 5.4% (2112741 remain 39%)
c [simplification-7] maximum reduction of 5% = max (4%, 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 29035 (soft 19035 + delta 10000)
c [simplification-7] new conflict limit 19035 (hard 29035)
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  280.8  305203  2112741     18487   29025 126383 232398  101   232  221  43%     39  194   34   13  263%
c 
c [simplification-8] limit 19035 conflicts (hard 29035) hit after 19037 conflicts
c [quatres-4] found 301904 quaternary clauses 43% in total
c [quatres-4-1] removed 21 duplicate quaternary clauses
c [quatres-4-1] added 64 double-self-subsuming ternary resolvents
c [quatres-4-2] added 1001 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3173 quaternary resolvents
c [ternres-4] limit 13366438 with penalty 1 = 0 + 1
c [ternres-4] 10299 schedulable variables 3%
c [ternres-4] 70752 ternary resolvents (2562 bin, 68190 trn)
c [ternres-4] 1215 variables remain 0% (303988 retained 100%)
c [decomp-17] removed 627 variables
c [simpleprobe-4] 246075 schedulable variables 81%
c [simpleprobe-4] limit 53465752 penalty 1 = 0 + 1
c [decomp-18] removed 3324 variables
c [simpleprobe-4] 153969 variables remain 51% (147284 retained 49%)
c [simpleprobe-4] removed 3324 variables, found 98314 hbrs, 540 units
c [unhide-8] limit 668321 with penalty 3 = 0 + 3
c [unhide-8-8] 156 units, 261 failed, 36306 tauts, 0 hbrs, 45111 literals
c [transred-4] limit 2086160 based on 2086160 irredundant clauses
c [transred-4] removed 1429 transitive binary clauses
c [transred-4] found 9 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 300828 variables 100%
c [block-3] limit of 66832190 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 13733 blocked clauses
c [block-3] 13733 < 1/100 * 2085654 = 20856 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 300601 variables 100%
c [elim-7] limit of 133664380 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 16070 not tried 5% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 17533 = 6% variables out of 300601 scheduled
c [bca-4] limit of 10000000 steps and 4014162 added (scaled 2)
c [bca-4] 515120 out of 566138 literals actually usable 91%
c [bca-4] added 1734 blocked clauses in 1608294 steps
c [sweep-4] limit 4009931 penalty 1 = 0 + 1
c [sweep-4-1] 110872 pos 39.3% + 171161 neg 60.7% = 282033 sched 99.6% ret 1035
c [sweep-4-1] 4019913 steps 95 queries 84157.26 avg class size
c [sweep-4-1] 1492 decisions 85 SAT calls 37.94 avg env size
c [sweep-4-1] 281477 variables remain 99% (1584 retained 1%)
c [decomp-19] removed 696 variables
c [sweep-4-1] removed 696 vars (0 failed, 15 eqs, 21 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 696 vars in TOTAL (1 rounds, 94 queries)
c [phase-count-8] 1905383 negative 95.1% of 2002585 except 97202 4.9%
c [phase-count-8] 1885551 positive 94.2% of 2002585 except 117034 5.8%
c [phase-8] phase bias: 62 positive 57%, 47 negative 43%
c [sort-queue-8] sorted 220378 enqueued variables after 19037 conflicts
c [score-dist-8] active 61994 (22%), one 0 (0%), zero 220378 (78%)
c [score-dist-8] max exp 514, different 14 (3%)
c [score-dist-8] median active exp 505, avg 505.7
c [simplification-8] removed 22831 variables 7.5% (282372 remain 21%)
c [simplification-8] removed 110156 irredundant clauses 5.2% (2002585 remain 37%)
c [simplification-8] maximum reduction of 7% = max (7%, 5%)
c [simplification-8] large reduction 7% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 31037 (soft 21037 + delta 10000)
c [simplification-8] new conflict limit 21037 (hard 31037)
c 
c [simplification-9] limit 21037 conflicts (hard 31037) hit after 21037 conflicts
c [quatres-5] found 301980 quaternary clauses 44% in total
c [quatres-5-1] removed 224 duplicate quaternary clauses
c [quatres-5-1] added 31 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1358 single-self-subsuming ternary resolvents
c [quatres-5-2] added 4507 quaternary resolvents
c [ternres-5] limit 15575555 with penalty 1 = 0 + 1
c [ternres-5] 1095 schedulable variables 0%
c [ternres-5] 69911 ternary resolvents (1969 bin, 67942 trn)
c [ternres-5] 156 variables remain 0% (282216 retained 100%)
c [decomp-20] removed 432 variables
c [treelook-4] limit 1557555 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 118291 literals 21%
c [treelook-4] scheduling used 1557732 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1557555 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 1558533 steps
c [treelook-4] 118142 literals remain 21%
c [treelook-4] 33120 variables remain to probed next time 12%
c [decomp-21] removed 7 variables
c [treelook-4] removed 24 variables, found 2030 hbrs
c [unhide-9] limit 778777 with penalty 3 = 0 + 3
c [unhide-9-9] 79 units, 145 failed, 19809 tauts, 0 hbrs, 22138 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1176 transitive binary clauses
c [transred-5] found 10 units
c [elim-8] 1718 variables 1% will be scheduled this time
c [elim-8] scheduled 1718 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 12460444760 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 351935158 steps
c [elim-8] fully completed in 1 rounds
c [gc-65] reconnected 248852 binary clauses (produced 0 empty 2 units)
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 25 = 1% variables out of 1718 scheduled
c [elim-8] 25 < 1/100 * 1718 = 17 considered unsuccessful
c [bca-5] limit of 10000000 steps and 3956777 added (scaled 2)
c [bca-5] 506776 out of 563338 literals actually usable 90%
c [bca-5] added 381 blocked clauses in 1579756 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 93453330 penalty 0 = 0 + 0
c [sweep-5-1] 110106 pos 39.3% + 169993 neg 60.7% = 280099 sched 99.4% ret 1569
c [sweep-5-1] 93478031 steps 1952 queries 28469.86 avg class size
c [sweep-5-1] 26096 decisions 1854 SAT calls 35.49 avg env size
c [sweep-5-1] 258217 variables remain 92% (23382 retained 8%)
c [decomp-22] removed 1380 variables
c [sweep-5-1] removed 1380 vars (0 failed, 348 eqs, 443 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1380 vars in TOTAL (1 rounds, 1951 queries)
c [phase-count-9] 1872589 negative 95.0% of 1971040 except 98451 5.0%
c [phase-count-9] 1854459 positive 94.1% of 1971040 except 116581 5.9%
c [phase-9] phase bias: 13 positive 15%, 73 negative 85%
c [sort-queue-9] sorted 212657 enqueued variables after 21037 conflicts
c [score-dist-9] active 67631 (24%), one 0 (0%), zero 212657 (76%)
c [score-dist-9] max exp 514, different 14 (3%)
c [score-dist-9] median active exp 504, avg 505.7
c [simplification-9] removed 2084 variables 0.7% (280288 remain 21%)
c [simplification-9] removed 31545 irredundant clauses 1.6% (1971040 remain 37%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-9] new conflict interval 16666
c [simplification-9] penalized conflict interval 16666 = 1 * 16666
c [simplification-9] hard conflict limit 47703 (soft 37703 + delta 10000)
c [simplification-9] new conflict limit 37703 (hard 47703)
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  411.5  280287  1971040     27673   36829 169838 256754  107   259  223  41%    114  195   49   28  173%
c i  414.3  280286  1971040     28594   37656 169878 256774   92   265  223  35%     42  198   22   29   77%
c i  416.1  280285  1971040     30192   39115 169908 256802   75   266  224  28%      9  195   49   29  170%
c i  416.3  280284  1971040     30282   39196 169910 256806   74   266  224  28%      7  194   45   29  156%
c i  417.9  280283  1971040     31491   40308 169947 256817   66   260  224  26%     -1  185   51   29  176%
c i  417.9  280281  1971040     31500   40315 169948 256817   66   260  224  26%     -1  185   50   29  173%
c i  419.8  280280  1971040     32778   41462 169980 256829   57   246  224  23%     -2  168   17   29   59%
c i  422.5  280278  1971040     34197   42777 170005 256848   47   231  225  20%     -2  149   29   29   99%
c i  423.1  280129  1971040     34529   43089 170010 256849   45   228  225  20%     -5  146   29   29  100%
c i  423.3  280128  1971040     34639   43185 170017 256853   45   229  225  20%     -6  146   25   29   88%
c i  423.8  280052  1971040     35015   43530 170019 256855   44   225  225  20%     -7  141   35   29  122%
c i  423.8  280051  1971040     35021   43533 170019 256855   44   225  225  20%     -7  141   36   29  125%
c i  424.9  280050  1971040     35739   44186 170035 256864   42   213  225  20%     -8  128   28   29   96%
c i  424.9  280049  1971040     35758   44201 170035 256866   42   212  225  20%     -8  127   27   29   95%
c i  425.6  279989  1971040     36251   44664 170046 256878   40   212  226  19%     -9  126   26   29   90%
c i  426.1  279892  1971039     36580   44973 170051 256882   39   206  226  19%    -10  120   34   29  116%
c 
c [simplification-10] limit 37705 conflicts (hard 47703) hit after 38279 conflicts
c [quatres-6] found 301977 quaternary clauses 45% in total
c [quatres-6-1] removed 49 duplicate quaternary clauses
c [quatres-6-1] added 45 double-self-subsuming ternary resolvents
c [quatres-6-2] added 528 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2176 quaternary resolvents
c [ternres-6] limit 45181744 with penalty 0 = 0 + 0
c [ternres-6] 144 schedulable variables 0%
c [ternres-6] 83788 ternary resolvents (1534 bin, 82254 trn)
c [ternres-6] 2 variables remain 0% (279890 retained 100%)
c [card-4] limit 2823859 penalty 3 = 3 + 0
c [card-4] found 1641 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2823859 for elimination
c [card-4] 1641 out of 1641 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2259087 penalty 2 = 2 + 0
c [gauss-3] extracted 5617 xors of average arity 3.0
c [gauss-3] connected 16709 occurrences of 6643 variables (average 2.5)
c [gauss-3] limit 2259087 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 560 variables
c [basicprobe-4] limit 225908724 penalty 0 = 0 + 0
c [basicprobe-4-0] 137383 sched 52%, 8207 failed, 496 lifted, 276275 hbrs
c [decomp-24] removed 23364 variables
c [basicprobe-4-1] 80439 probes remain 33% after last round
c [basicprobe-4-1] 10583 units = 9957 failed (94%) + 626 lifted (6%)
c [basicprobe-4-1] removed 31939 variables, found 324894 hbrs
c [bate-2] eliminated 10654 asymmetric tautologies during probing
c [unhide-10] limit 1129543 with penalty 3 = 0 + 3
c [unhide-10-10] 69 units, 102 failed, 47898 tauts, 0 hbrs, 64275 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1965 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 56477181 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 27
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-3-1] eliminated 6 clauses out of 7 (86%) of length 20
c [cce-3-1] eliminated 6 clauses out of 8 (75%) of length 19
c [cce-3-1] eliminated 5 clauses out of 701 (1%) of length 18
c [cce-3-1] eliminated 16 clauses out of 694 (2%) of length 17
c [cce-3-1] eliminated 19 clauses out of 467 (4%) of length 16
c [cce-3-1] eliminated 27 clauses out of 1149 (2%) of length 15
c [cce-3-1] eliminated 84 clauses out of 1289 (7%) of length 14
c [cce-3-1] eliminated 939 clauses out of 3149 (30%) of length 13
c [cce-3-1] eliminated 2466 clauses out of 5928 (42%) of length 12
c [cce-3-1] eliminated 556 clauses out of 7754 (7%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4130 large clauses in 56477203 steps
c [cce-3-1] allowing another 28238601 steps for small clauses
c [cce-3-1] scheduling 913324 clauses = 713250 binary + 200074 ternary
c [cce-3-1] tried to eliminate 11291 small clauses 1%
c [cce-3-1] eliminated 2607 binary clauses 0%
c [cce-3-1] eliminated 514 ternary clauses 0%
c [cce-3-1] eliminated 3121 small clauses 0%
c [cce-3-1] eliminated 4269 small clauses in 56477290 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 8399 covered clauses in round 1
c [cce-3] eliminated 8399 covered clauses in TOTAL during 1 rounds
c [cce-3] 8399 < 1/100 * 1701184 = 17011 considered unsuccessful
c [bca-6] limit of 10000000 steps and 3391948 added (scaled 2)
c [bca-6] 439459 out of 494484 literals actually usable 89%
c [bca-6] added 1173 blocked clauses in 1333972 steps
c [sweep-6] limit 13554523 penalty 0 = 0 + 0
c [sweep-6-1] 87783 pos 38.7% + 139169 neg 61.3% = 226952 sched 91.8% ret 20289
c [sweep-6-1] 13564103 steps 384 queries 54461.63 avg class size
c [sweep-6-1] 4929 decisions 358 SAT calls 33.63 avg env size
c [sweep-6-1] 224561 variables remain 91% (22670 retained 9%)
c [decomp-25] removed 3819 variables
c [sweep-6-1] removed 3819 vars (0 failed, 63 eqs, 78 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 3819 vars in TOTAL (1 rounds, 383 queries)
c [phase-count-10] 1592543 negative 94.6% of 1683808 except 91265 5.4%
c [phase-count-10] 1573474 positive 93.4% of 1683808 except 110334 6.6%
c [phase-10] phase bias: 86 positive 67%, 42 negative 33%
c [sort-queue-10] sorted 178347 enqueued variables after 38279 conflicts
c [score-dist-10] active 65075 (27%), one 0 (0%), zero 178347 (73%)
c [score-dist-10] max exp 515, different 15 (3%)
c [score-dist-10] median active exp 505, avg 506.0
c [simplification-10] removed 36470 variables 13.0% (243422 remain 18%)
c [simplification-10] removed 287231 irredundant clauses 14.6% (1683808 remain 31%)
c [simplification-10] maximum reduction of 15% = max (13%, 15%)
c [simplification-10] large reduction 15% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 50279 (soft 40279 + delta 10000)
c [simplification-10] new conflict limit 40279 (hard 50279)
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  460.1  243421  1683808     39082   44870 134899 338582   34   174  206  20%     10   83   22   29   75%
c 
c [simplification-11] limit 40279 conflicts (hard 50279) hit after 40279 conflicts
c [quatres-7] found 266630 quaternary clauses 46% in total
c [quatres-7-1] removed 205 duplicate quaternary clauses
c [quatres-7-1] added 169 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1480 single-self-subsuming ternary resolvents
c [quatres-7-2] added 3453 quaternary resolvents
c [ternres-7] limit 45743891 with penalty 0 = 0 + 0
c [ternres-7] 1 schedulable variables 0%
c [ternres-7] 21345 ternary resolvents (337 bin, 21008 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 208 variables
c [simpleprobe-5] 121748 schedulable variables 50%
c [simpleprobe-5] limit 182975567 penalty 0 = 0 + 0
c [decomp-27] removed 7038 variables
c [simpleprobe-5] 56935 variables remain 24% (179241 retained 76%)
c [simpleprobe-5] removed 7038 variables, found 246469 hbrs, 440 units
c [unhide-11] limit 1143597 with penalty 3 = 0 + 3
c [unhide-11-11] 24 units, 26 failed, 23206 tauts, 0 hbrs, 25993 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2791 transitive binary clauses
c [transred-7] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 236132 variables 100%
c [block-4] limit of 114359729 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 23765 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 235191 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 771 not tried 0% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 20188 = 9% variables out of 235191 scheduled
c [bca-7] limit of 10000000 steps and 3054304 added (scaled 2)
c [bca-7] 377045 out of 430008 literals actually usable 88%
c [bca-7] added 2024 blocked clauses in 1198284 steps
c [sweep-7] limit 13723167 penalty 0 = 0 + 0
c [sweep-7-1] 73754 pos 37.9% + 120877 neg 62.1% = 194631 sched 90.5% ret 20372
c [sweep-7-1] 13765209 steps 418 queries 42587.94 avg class size
c [sweep-7-1] 6059 decisions 402 SAT calls 37.31 avg env size
c [sweep-7-1] 191620 variables remain 89% (23374 retained 11%)
c [decomp-28] removed 560 variables
c [sweep-7-1] removed 560 vars (1 failed, 62 eqs, 65 impls)
c [sweep-7] removed 560 vars in TOTAL (1 rounds, 417 queries)
c [phase-count-11] 1440951 negative 94.7% of 1522356 except 81405 5.3%
c [phase-count-11] 1421585 positive 93.4% of 1522356 except 100771 6.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 51 positive 36%, 89 negative 64%
c [sort-queue-11] sorted 153449 enqueued variables after 40279 conflicts
c [score-dist-11] active 60994 (28%), one 0 (0%), zero 153449 (72%)
c [score-dist-11] max exp 515, different 15 (3%)
c [score-dist-11] median active exp 505, avg 506.1
c [simplification-11] removed 28899 variables 11.9% (214443 remain 16%)
c [simplification-11] removed 161452 irredundant clauses 9.6% (1522356 remain 28%)
c [simplification-11] maximum reduction of 12% = max (12%, 10%)
c [simplification-11] large reduction 12% >= 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 52279 (soft 42279 + delta 10000)
c [simplification-11] new conflict limit 42279 (hard 52279)
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  488.5  214442  1522356     41089   40645 115561 452870   27   199  197  14%      6  106   15   29   54%
c i  489.3  214441  1522356     41772   41280 115578 452880   26   206  197  12%     -1  111   19   28   65%
c i  489.4  214440  1522356     41777   41284 115578 452880   26   206  197  12%     -1  111   19   28   67%
c 
c [simplification-12] limit 42281 conflicts (hard 52279) hit after 43315 conflicts
c [quatres-8] found 254055 quaternary clauses 46% in total
c [quatres-8-1] removed 1610 duplicate quaternary clauses
c [quatres-8-1] added 17 double-self-subsuming ternary resolvents
c [quatres-8-2] added 340 single-self-subsuming ternary resolvents
c [quatres-8-2] added 4379 quaternary resolvents
c [ternres-8] limit 46691336 with penalty 0 = 0 + 0
c [ternres-8] all 214440 free variables schedulable
c [ternres-8] 40621 ternary resolvents (1609 bin, 39012 trn)
c [ternres-8] 1552 variables remain 1% (212888 retained 99%)
c [decomp-29] removed 280 variables
c [treelook-5] limit 4669133 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 170114 literals 40%
c [treelook-5] scheduling used 3833143 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4669133 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 4679534 steps
c [treelook-5] 169546 literals remain 40%
c [treelook-5] 24116 variables remain to probed next time 11%
c [decomp-30] removed 22 variables
c [treelook-5] removed 55 variables, found 3627 hbrs
c [unhide-12] limit 2334566 with penalty 2 = 0 + 2
c [unhide-12-12] 37 units, 253 failed, 66053 tauts, 0 hbrs, 31134 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2641 transitive binary clauses
c [transred-8] found 4 units
c [elim-10] 771 variables 0% will be scheduled this time
c [elim-10] scheduled 771 variables 0%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 141560330 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 80 = 10% variables out of 771 scheduled
c [elim-10] 80 < 1/100 * 771 = 7 considered unsuccessful
c [bca-8] limit of 10000000 steps and 3039470 added (scaled 2)
c [bca-8] 369261 out of 427582 literals actually usable 86%
c [bca-8] added 703 blocked clauses in 1156834 steps
c [sweep-8] limit 14007401 penalty 0 = 0 + 0
c [sweep-8-1] 72298 pos 37.9% + 118250 neg 62.1% = 190548 sched 89.1% ret 23242
c [sweep-8-1] 14011429 steps 351 queries 42880.34 avg class size
c [sweep-8-1] 5383 decisions 330 SAT calls 37.46 avg env size
c [sweep-8-1] 187819 variables remain 88% (25966 retained 12%)
c [decomp-31] removed 432 variables
c [sweep-8-1] removed 432 vars (0 failed, 45 eqs, 56 impls)
c [sweep-8] removed 432 vars in TOTAL (1 rounds, 350 queries)
c [phase-count-12] 1432514 negative 94.6% of 1514693 except 82179 5.4%
c [phase-count-12] 1412718 positive 93.3% of 1514693 except 101975 6.7%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 25 positive 60%, 17 negative 40%
c [sort-queue-12] sorted 150832 enqueued variables after 43315 conflicts
c [score-dist-12] active 62526 (29%), one 0 (0%), zero 150832 (71%)
c [score-dist-12] max exp 515, different 15 (3%)
c [score-dist-12] median active exp 505, avg 506.1
c [simplification-12] removed 1082 variables 0.5% (213358 remain 16%)
c [simplification-12] removed 7663 irredundant clauses 0.5% (1514693 remain 28%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-12] new conflict interval 26666
c [simplification-12] penalized conflict interval 26666 = 1 * 26666
c [simplification-12] hard conflict limit 83314 (soft 69981 + delta 13333)
c [simplification-12] new conflict limit 69981 (hard 83314)
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  533.0  213357  1514693     51123   50789 142894 391456   54   199  200  27%    109   88   25   31   80%
c i  574.3  213356  1514693     61474   55264 143119 391532  409   587  224  70%    116  431  103   83  124%
c 
c [simplification-13] limit 69981 conflicts (hard 83314) hit after 69982 conflicts
c [quatres-9] found 254310 quaternary clauses 46% in total
c [quatres-9-1] removed 33 duplicate quaternary clauses
c [quatres-9-1] added 44 double-self-subsuming ternary resolvents
c [quatres-9-2] added 811 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1151 quaternary resolvents
c [ternres-9] limit 79472507 with penalty 0 = 0 + 0
c [ternres-9] 1524 schedulable variables 1%
c [ternres-9] 40104 ternary resolvents (1832 bin, 38272 trn)
c [ternres-9] 3 variables remain 0% (213353 retained 100%)
c [decomp-32] removed 367 variables
c [basicprobe-5] limit 397362536 penalty 0 = 0 + 0
c [basicprobe-5-0] 68156 sched 32%, 1985 failed, 212 lifted, 48796 hbrs
c [decomp-33] removed 4808 variables
c [basicprobe-5-1] 136555 sched 67%, 1780 failed, 134 lifted, 40439 hbrs
c [decomp-34] removed 4543 variables
c [basicprobe-5-2] 113617 probes remain 56% after last round
c [basicprobe-5-2] 4170 units = 3823 failed (92%) + 347 lifted (8%)
c [basicprobe-5-2] removed 9519 variables, found 91958 hbrs
c [bate-3] eliminated 5688 asymmetric tautologies during probing
c [unhide-13] limit 1986812 with penalty 3 = 0 + 3
c [unhide-13-13] 9 units, 45 failed, 15606 tauts, 0 hbrs, 83255 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2699 transitive binary clauses
c [transred-9] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 203416 variables 100%
c [block-5] limit of 397362536 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 13011 blocked clauses
c [block-5] 13011 < 1/100 * 1415000 = 14150 considered unsuccessful
c [bca-9] limit of 10000000 steps and 2811400 added (scaled 2)
c [bca-9] 336594 out of 405444 literals actually usable 83%
c [bca-9] added 478 blocked clauses in 1051101 steps
c [sweep-9] limit 23841752 penalty 0 = 0 + 0
c [sweep-9-1] 66156 pos 37.1% + 112106 neg 62.9% = 178262 sched 87.9% ret 24459
c [sweep-9-1] 23865821 steps 660 queries 26535.14 avg class size
c [sweep-9-1] 9949 decisions 642 SAT calls 39.77 avg env size
c [sweep-9-1] 171557 variables remain 85% (31150 retained 15%)
c [decomp-35] removed 521 variables
c [sweep-9-1] removed 521 vars (0 failed, 70 eqs, 80 impls)
c [sweep-9] removed 521 vars in TOTAL (1 rounds, 659 queries)
c [phase-count-13] 1322970 negative 94.5% of 1399509 except 76539 5.5%
c [phase-count-13] 1301171 positive 93.0% of 1399509 except 98338 7.0%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 9 positive 30%, 21 negative 70%
c [sort-queue-13] sorted 125852 enqueued variables after 69982 conflicts
c [score-dist-13] active 76348 (38%), one 0 (0%), zero 125852 (62%)
c [score-dist-13] max exp 516, different 16 (3%)
c [score-dist-13] median active exp 507, avg 507.4
c [simplification-13] removed 11156 variables 5.2% (202200 remain 15%)
c [simplification-13] removed 115184 irredundant clauses 7.6% (1399509 remain 26%)
c [simplification-13] maximum reduction of 8% = max (5%, 8%)
c [simplification-13] large reduction 8% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 81982 (soft 71982 + delta 10000)
c [simplification-13] new conflict limit 71982 (hard 81982)
c 
c [simplification-14] limit 71982 conflicts (hard 81982) hit after 71982 conflicts
c [quatres-10] found 235885 quaternary clauses 46% in total
c [quatres-10-1] removed 183 duplicate quaternary clauses
c [quatres-10-1] added 24 double-self-subsuming ternary resolvents
c [quatres-10-2] added 805 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1356 quaternary resolvents
c [ternres-10] limit 86358461 with penalty 0 = 0 + 0
c [ternres-10] 3 schedulable variables 0%
c [ternres-10] 4070 ternary resolvents (62 bin, 4008 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 2158961 penalty 3 = 3 + 0
c [gauss-4] extracted 4546 xors of average arity 3.0
c [gauss-4] connected 13604 occurrences of 5176 variables (average 2.6)
c [gauss-4] limit 2158961 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 8 variables
c [simpleprobe-6] 46953 schedulable variables 23%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-37] removed 3329 variables
c [simpleprobe-6] 26204 variables remain 13% (172659 retained 87%)
c [simpleprobe-6] removed 3329 variables, found 141459 hbrs, 105 units
c [unhide-14] limit 2158961 with penalty 3 = 0 + 3
c [unhide-14-14] 6 units, 23 failed, 90920 tauts, 0 hbrs, 139118 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2226 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 539740383 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 655 (0%) of length 18
c [cce-4-1] eliminated 1 clauses out of 397 (0%) of length 17
c [cce-4-1] eliminated 4 clauses out of 289 (1%) of length 16
c [cce-4-1] eliminated 3 clauses out of 1284 (0%) of length 15
c [cce-4-1] eliminated 39 clauses out of 1246 (3%) of length 14
c [cce-4-1] eliminated 22 clauses out of 1777 (1%) of length 13
c [cce-4-1] eliminated 63 clauses out of 3789 (2%) of length 12
c [cce-4-1] eliminated 387 clauses out of 4454 (9%) of length 11
c [cce-4-1] eliminated 2282 clauses out of 8729 (26%) of length 10
c [cce-4-1] eliminated 5647 clauses out of 17113 (33%) of length 9
c [cce-4-1] eliminated 5083 clauses out of 24866 (20%) of length 8
c [cce-4-1] eliminated 5512 clauses out of 31015 (18%) of length 7
c [cce-4-1] eliminated 7677 clauses out of 52862 (15%) of length 6
c [cce-4-1] eliminated 21842 clauses out of 114535 (19%) of length 5
c [cce-4-1] eliminated 9208 clauses out of 208110 (4%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 57771 large clauses in 539740390 steps
c [cce-4-1] allowing another 269870195 steps for small clauses
c [cce-4-1] scheduling 733599 clauses = 553149 binary + 180450 ternary
c [cce-4-1] tried to eliminate 156804 small clauses 21%
c [cce-4-1] eliminated 17303 binary clauses 3%
c [cce-4-1] eliminated 6625 ternary clauses 4%
c [cce-4-1] eliminated 23928 small clauses 3%
c [cce-4-1] eliminated 24172 small clauses in 539740386 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 81943 covered clauses in round 1
c [cce-4] eliminated 81943 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 198825 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 22297 variables 11% in round 1 in 378095084 steps
c [elim-11-1] backward subsumption/strengthening limit 21904916
c [elim-11-1-1] backward checking 88008 touched variables 44%
c [elim-11-1-1] incomplete backward checking 76566 remain 87%
c [elim-11-1] subsumed 431 and strengthened 366 clauses in 21904947 steps
c [elim-11] incomplete 2007 not tried 1% in round 1
c [gc-108] reconnected 439134 binary clauses (produced 0 empty 5 units)
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 22311 = 11% variables out of 198825 scheduled
c [bca-10] limit of 10000000 steps and 2456969 added (scaled 2)
c [bca-10] 296637 out of 353030 literals actually usable 84%
c [bca-10] added 3635 blocked clauses in 925918 steps
c [sweep-10] limit 25907538 penalty 0 = 0 + 0
c [sweep-10-1] 54295 pos 36.4% + 94714 neg 63.6% = 149009 sched 84.4% ret 27505
c [sweep-10-1] 25928295 steps 764 queries 18023.10 avg class size
c [sweep-10-1] 10343 decisions 742 SAT calls 35.80 avg env size
c [sweep-10-1] 141416 variables remain 80% (35093 retained 20%)
c [decomp-38] removed 459 variables
c [sweep-10-1] removed 459 vars (0 failed, 91 eqs, 103 impls)
c [sweep-10] removed 459 vars in TOTAL (1 rounds, 763 queries)
c [phase-count-14] 1153283 negative 94.3% of 1223078 except 69795 5.7%
c [phase-count-14] 1137169 positive 93.0% of 1223078 except 85909 7.0%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 37 positive 60%, 25 negative 40%
c [sort-queue-14] sorted 105049 enqueued variables after 71982 conflicts
c [score-dist-14] active 71006 (40%), one 0 (0%), zero 105049 (60%)
c [score-dist-14] max exp 516, different 16 (3%)
c [score-dist-14] median active exp 507, avg 507.5
c [simplification-14] removed 26145 variables 12.9% (176055 remain 13%)
c [simplification-14] removed 176431 irredundant clauses 12.6% (1223078 remain 23%)
c [simplification-14] maximum reduction of 13% = max (13%, 13%)
c [simplification-14] large reduction 13% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 83982 (soft 73982 + delta 10000)
c [simplification-14] new conflict limit 73982 (hard 83982)
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  772.7  176054  1223078     72146   43415 131977 363648  155   251  183  62%    113   55  127   88  143%
c 
c [simplification-15] limit 73982 conflicts (hard 83982) hit after 73983 conflicts
c [quatres-11] found 217718 quaternary clauses 49% in total
c [quatres-11-1] removed 253 duplicate quaternary clauses
c [quatres-11-1] added 152 double-self-subsuming ternary resolvents
c [quatres-11-2] added 828 single-self-subsuming ternary resolvents
c [quatres-11-2] added 4356 quaternary resolvents
c [ternres-11] limit 90547987 with penalty 0 = 0 + 0
c [ternres-11] all 176054 free variables schedulable
c [ternres-11] 35489 ternary resolvents (1628 bin, 33861 trn)
c [ternres-11] 2 variables remain 0% (176052 retained 100%)
c [card-5] limit 2829624 penalty 4 = 4 + 0
c [card-5] found 1946 at-most-one constraints of average size 3.3
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2829624 for elimination
c [card-5] 1946 out of 1946 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-39] removed 153 variables
c [treelook-6] limit 9054798 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 145003 literals 41%
c [treelook-6] scheduling used 3218236 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 9054798 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 9839682 steps
c [treelook-6] 144504 literals remain 41%
c [treelook-6] 20214 variables remain to probed next time 11%
c [decomp-40] removed 77 variables
c [treelook-6] removed 88 variables, found 30881 hbrs
c [unhide-15] limit 4527399 with penalty 2 = 0 + 2
c [unhide-15-15] 3 units, 11 failed, 8011 tauts, 0 hbrs, 7895 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 2183 transitive binary clauses
c [transred-11] found 1 units
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 175795 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 3090 variables 2% in round 1 in 358251525 steps
c [elim-12-1] backward subsumption/strengthening limit 358251500
c [elim-12-1-1] backward checking 23665 touched variables 13%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 140 and strengthened 185 clauses in 31751267 steps
c [elim-12-1] rescheduled 1322 variables 1% by backward subsumption
c [elim-12-2] eliminated 91 variables 0% in round 2 in 12465820 steps
c [elim-12-2] backward subsumption/strengthening limit 12465800
c [elim-12-2-1] backward checking 660 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 36 and strengthened 48 clauses in 1673442 steps
c [elim-12-2] rescheduled 216 variables 0% by backward subsumption
c [elim-12-3] eliminated 23 variables 0% in round 3 in 2453880 steps
c [elim-12-3] backward subsumption/strengthening limit 2453800
c [elim-12-3-1] backward checking 153 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 11 and strengthened 35 clauses in 774798 steps
c [elim-12] incomplete 94 not tried 0% in round 3
c [gc-115] reconnected 380858 binary clauses (produced 0 empty 1 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 3215 = 2% variables out of 175795 scheduled
c [bca-11] limit of 10000000 steps and 2411768 added (scaled 2)
c [bca-11] 284853 out of 345162 literals actually usable 83%
c [bca-11] added 1040 blocked clauses in 894757 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 271643960 penalty 0 = 0 + 0
c [sweep-11-1] 50032 pos 36.2% + 88264 neg 63.8% = 138296 sched 80.1% ret 34284
c [sweep-11-1] 271656722 steps 8144 queries 2236.06 avg class size
c [sweep-11-1] 95165 decisions 7782 SAT calls 31.42 avg env size
c [sweep-11-1] 56351 variables remain 33% (116038 retained 67%)
c [decomp-41] removed 2147 variables
c [sweep-11-1] removed 2147 vars (0 failed, 1601 eqs, 1501 impls)
c [sweep-11] removed 2147 vars in TOTAL (1 rounds, 8143 queries)
c [phase-count-15] 1120774 negative 93.9% of 1192986 except 72212 6.1%
c [phase-count-15] 1105553 positive 92.7% of 1192986 except 87433 7.3%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 6 positive 22%, 21 negative 78%
c [sort-queue-15] sorted 88656 enqueued variables after 73983 conflicts
c [score-dist-15] active 81777 (48%), one 0 (0%), zero 88656 (52%)
c [score-dist-15] max exp 516, different 16 (3%)
c [score-dist-15] median active exp 506, avg 506.9
c [simplification-15] removed 5621 variables 3.2% (170433 remain 13%)
c [simplification-15] removed 30092 irredundant clauses 2.5% (1192986 remain 22%)
c [simplification-15] maximum reduction of 3% = max (3%, 2%)
c [simplification-15] geometric conflict interval increment 6666 = 26666 / 4
c [simplification-15] new conflict interval 33332
c [simplification-15] penalized conflict interval 33332 = 1 * 33332
c [simplification-15] hard conflict limit 123981 (soft 107315 + delta 16666)
c [simplification-15] new conflict limit 107315 (hard 123981)
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  973.3  170432  1192986     94792   59671 151051 372890   81   206  214  39%    259    7   69   93   73%
c i  973.3  170431  1192986     94831   59707 151051 372891   81   206  214  39%    246    8   62   93   66%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 21343 basic ate = 15392 trn 72% + 5951 lrg 28% in 3 updates
c bcas: 11 count, 20809 added (15921 skipped), 15273729 steps
c bkwd: tried 527783 clauses, 1054805 lits, 2.00 lits/clause
c bkwd: checked 39908079 occs, 75.61 occs/clause, 37.83 occs/lit
c bkwd: subsumed 13 binary, 140 ternary, 465 large
c bkwd: strengthened 8 binary, 0 ternary (0% self), 626 large (0% self)
c blkd: 5 bces, 86278 removed, 46213481 resolutions, 121455867 steps
c blkd: 43604 blocking literals 2%, 2580 pure
c bump: 110480 bumped seen, 113847545 lits 1030.5 on average
c card: 5 count, 0 units, 0 am1, 78777394 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 16447 subsumed
c card: 5989 at-most-one constraints found, average size 3.12
c card: 5989 at-most-one constraints used 100%, average size 3.12
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 4 cces, 93481 eliminated, 91152 ate 98%, 2329 abce 2%
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: 18938485 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 118 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 41 decompositions, 144355 equivalent 10%
c deco: 31360 decision-only clauses 28%, 70% reduction
c decs: 2313121 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 782033 eliminated 57%, 11296 pure 1%
c elms: 16 rounds, 1.3 rounds/bve
c elms: 676348 small 86%, 91809 large 12%
c elms: 828080 tried small, 676348 succeeded 82%, 151732 failed 18%
c elms: 348417 subsumed, 468734 strengthened, 14521 blocked
c elms: 44514619 copies, 55725894 resolutions, 15302158 ipos
c elms: 32612061 subchks, 59225901 strchks
c gaus: 4 extractions, 21430 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13537658 steps, 6768829 extr 50%, 6800246 elim 50%
c glue: 99.4 orig avg, 99.4 real avg, 5.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1626225 = 575999 simple 35% + 1039086 trn 64% + 11140 lrg 1%, 46637 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 110480 clauses, 151.0 length
c lrnd: 16686843 lits = 40621675 orig - 23934832 removed 59%
c lrnd: 37099 uips 34%, 44794 flips 41%
c mins: 70740 mins 64%, 2811 bin 3%, 5074 size 5%
c mins: 24594463 poisoned searches, 3596214 hits, 15% hit rate
c mins: 30680114 used twice searches, 1278834 hits, 4% hit rate
c move: moved 127389, 64139 bin 50%, 63250 trn 50%
c otfs: 1397 driving 45%, 1726 restarting 55%
c otfs: str 3123, 2481 red 79%, 642 irr 21%
c otfs: str 3123, 0 bin 0%, 1077 trn 34%, 2046 lrg 66%
c otfs: sub 101, 88 red 87%, 13 irr 13%
c otfs: sub 101, 0 bin 0%, 42 trn 42%, 59 lrg 58%
c phas: 15 computed, 994379 set, 461371 pos (46%), 533008 neg (54%)
c prbs: 5 basic, 1176823 probed, 20912 failed, 2475 lifted
c prbs: 6 simple, 1881872 probed, 2337 failed, 19857 eqs
c prbs: 6 treelook, 1664 probed, 93 failed, 0 lifted
c prom: 0 locked 0% out of 644707 tried
c prps: 1959793386 props, 812 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 11 count, 45179 quat, 12091 self1, 687 self2, 4002 dup
c queu: 15 sorted, 2313121 next (109272 steps 0.05)
c queu: 120006328 enq (333987905 steps 2.78), 113847545 deq 95%
c redc: 3943 clauses 18%, 21772 tried 22%, 156 sat 1%
c redc: 7432 lits 5%, 150185 tried 0%, 158 sat 0%
c redc: 606 times jump level reduced, 46.1 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 358741 removed, 248460 red 69%
c rsts: 4782 restarts 97%, 140 skipped 3%
c rsts: 140 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 15 count, 14 confs 93%, 0 vars 0%
c simp: 0 its 0%, 1 bin 7%, 0 trns 0%
c subl: 110480 count (233946 tried 2.1), 32547 sub out of 100164 (32.5%)
c swps: 11 count, 11 rounds, 13034 queries (1184.9/round)
c swps: 12440 sat calls, 1806 unsat (1.2% success rate)
c swps: 163188 decisions 13.1, 14539 conflicts 1.2
c swps; 14795.1 avg class size, 33.2 avg environment size
c swps: 1 failed, 2416 impls, 2345 equivs
c swp0: 4341 type 0 queries, 1043 unsat (24.0%), 4006 sat (92.3%)
c swp1: 8693 type 1 queries, 5173 unsat (59.5%), 6683 sat (76.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 4847537 calls to obtain time
c tops: 279882 fixed 20%, 55 its, 1769.78 confs/it
c trds: 11 transitive reductions, 20563 removed, 91 failed
c trds: 269341 nodes, 448031 edges, 22819588 steps
c trim: 666979 words, 2.5 MB
c trnr: 11 count, 16426 bin, 541558 trn, 419638367 steps
c unhd: 15 count, 15 rounds, 209890127 steps
c unhd: 27053 non-trivial sccs of average size 2.4
c unhd: 4071 units, 4052 bin, 19 trn, 0 lrg
c unhd: 5485 failed, 4684 stamp, 0 lits, 32 bin, 668 trn, 0 lrg
c unhd: 446925 tauts, 10070 bin 2%, 84572 trn 19%, 22420 lrg 5%
c unhd: 446925 tauts, 329863 stamp 74%, 314451 red 70%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 727640 str, 4052 bin 1%, 76713 trn 11%, 646875 lrg 89%, 303125 red 42%
c vars: 170431 remaining 12% and 1206270 removed 88% out of 1376701
c vars: 279882 fixed 20%, 782033 eliminated 57%, 144355 equivalent 10%
c vsts: 13266508546 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 6.7 search visits per propagation, 129137.8 per conflict
c wchs: 1232390645 pushed, 186909553 enlarged, 174 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         145343             0             0      14823191       4033188         35133
c 
c  0 0         60649  42         0   0<        0   0< 11549762  78   2422018  60     10190  29     0.8
c  1 5          2465   2         0   0         0   0    710230   5<   313002   8<     2077   6     0.1
c  2 6          5104   4         0   0         0   0   1088859   7    509166  13      3188   9     0.3
c  3 9          6303   4         0   0         0   0    477253   3    217523   5      2749   8     0.6
c  4 14         6142   4         0   0         0   0    334240   2    180033   4      2112   6<    1.1
c  5 21         7126   5<        0   0         0   0    179465   1     93807   2      2120   6     2.9
c  6 30         6121   4         0   0         0   0    135416   1     77826   2      3235   9     1.8
c  7 41         7010   5         0   0         0   0     86314   1     57135   1      2352   7     4.0
c  8 54         6239   4         0   0         0   0     64220   0     37970   1       981   3     2.5
c  9 69         3896   3         0   0         0   0     98673   1     61199   2      3554  10     1.5
c 10 86         2065   1         0   0         0   0     29756   0     18246   0      1696   5     1.5
c 11 126       21143  15         0   0         0   0     36731   0     22970   1       288   1     8.9
c 12 230        5142   4         0   0         0   0     23818   0     17678   0       574   2     3.4
c 13 534        5938   4         0   0         0   0      8454   0      4615   0        17   0    13.9
c 
c avg                  4.5           0.0           0.0           0.7           1.4           3.9
c std                  4.7           0.0           0.0           1.7           2.4           3.6
c 
c   82.503   8% sweep
c   82.208   8% probe
c   79.237   8% elim
c   35.123   4% bump
c   30.543   3% unhide
c   24.172   2% cce
c   16.807   2% block
c   13.448   1% bca
c    9.945   1% quatres
c 
c   16.139 < 1% rest (below)
c 
c    6.496   1% gauss
c    4.803   0% ternres
c    2.638   0% decide
c    1.464   0% transred
c    0.738   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   16.247   2% preprocessing     4%
c  381.681  38% inprocessing     96%
c ==================================
c  397.928  40% simplifying
c  598.428  60% search
c ==================================
c  996.381 100% all
c 
c         97338 conflicts,          97.7 confs/sec
c          2028 ternaries,          48.0 confs/ternary
c           996 binaries,           97.7 confs/binary
c            55 iterations,       1769.8 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          4782 restarts,            4.8 rests/sec,     20.4 confs/restart
c       2313121 decisions,        2321.5 decis/sec,     23.8 decis/conflict
c    1959793386 propagations,  1966910.8 props/sec,    847.3 props/decision
c 
c 996.4 seconds, 492.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
