c launch: /data/cnf/sc2014/app/SAT_dat.k70-24_1_rule_1.cnf.bz2
c host: atom02
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.k70-24_1_rule_1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k70-24_1_rule_1.cnf.bz2
c no embedded options
c found 'p cnf 1131652 4433524' header
c read 1131652 variables, 4433524 clauses, 11129247 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 1096149 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 1096149  4397887         0       0      0     0    0     0  254   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1099471 based on 4397887 irredundant clauses
c [card-1] found 972 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1099471 for elimination
c [card-1] 972 out of 972 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 275789 variables
c [simpleprobe-1] all 855863 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 6951694 based on 3475847 irredundant clauses
c [decomp-2] removed 2404 variables
c [simpleprobe-1] 722398 variables remain 85% (131061 retained 15%)
c [simpleprobe-1] removed 2404 variables, found 8129 hbrs, 778 units
c [unhide-1] limit 216302 based on 3460846 irredundant clauses
c [unhide-1-1] 1003 units, 1105 failed, 7637 tauts, 0 hbrs, 42551 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 849097 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 768445 not tried 91% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 81297 = 10% variables out of 849097 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3049395 negative 95.2% of 3203267 except 153872 4.8%
c [phase-count-1] 2998266 positive 93.6% of 3203267 except 205001 6.4%
c [phase-1] phase bias: 356508 positive 46%, 411292 negative 54%
c [sort-queue-1] sorted 767800 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 767800 (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 160584 variables 17.3% (767800 remain 70%)
c [simplification-1] removed 1194620 irredundant clauses 27.2% (3203267 remain 73%)
c [simplification-1] maximum reduction of 27% = max (17%, 27%)
c [simplification-1] large reduction 27% >= 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   13.4  767799  3203267         8       5     17  6599    0     1  204   1%      0    1    0    0 25168%
c i   13.4  767798  3203267        10       5     17  6600    0     1  204   1%      0    1    0    0 24999%
c i   13.4  767770  3203267        11       5     17  6600    0     1  204   1%      0    1    0    0 24902%
c i   13.4  767580  3203267        14       6     17  6601    0     1  204   1%      0    1    0    0 24688%
c i   13.4  767579  3203267        18       8     18  6601    0     1  204   1%      0    1    0    0 24592%
c i   13.4  767521  3203267        19       8     18  6601    0     1  204   1%      0    1    0    0 24496%
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 2798 variables
c [simpleprobe-2] 647635 schedulable variables 85%
c [simpleprobe-2] limit 6390718 based on 3195359 irredundant clauses
c [decomp-4] removed 1614 variables
c [simpleprobe-2] 576749 variables remain 76% (186639 retained 24%)
c [simpleprobe-2] removed 1614 variables, found 26091 hbrs, 331 units
c [treelook-1] limit 797158 based on 3188632 irredundant clauses
c [treelook-1] scheduled 161088 literals 11%
c [treelook-1] scheduling used 797162 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 797158 based on 3188632 irredundant clauses
c [treelook-1] used 801563 steps
c [treelook-1] 160880 literals remain 11%
c [treelook-1] 159041 variables remain to probed next time 21%
c [decomp-5] removed 275 variables
c [treelook-1] removed 461 variables, found 10870 hbrs
c [basicprobe-1] limit 25493336 based on 3186667 irredundant clauses
c [basicprobe-1-0] 681583 probes remain 91% after last round
c [basicprobe-1-0] 2661 units = 1609 failed (60%) + 1052 lifted (40%)
c [basicprobe-1-0] removed 11620 variables, found 158337 hbrs
c [unhide-2] limit 199166 based on 3186667 irredundant clauses
c [unhide-2-2] 642 units, 759 failed, 10172 tauts, 0 hbrs, 28548 literals
c [elim-2] 749627 variables 100% will be scheduled this time
c [elim-2] scheduled 749627 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 665381 not tried 89% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 84248 = 11% variables out of 749627 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 2790460 negative 95.1% of 2934589 except 144129 4.9%
c [phase-count-2] 2739087 positive 93.3% of 2934589 except 195502 6.7%
c [phase-2] phase bias: 904 positive 27%, 2384 negative 73%
c [sort-queue-2] sorted 657325 enqueued variables after 630 conflicts
c [score-dist-2] active 8054 (1%), one 0 (0%), zero 657325 (99%)
c [score-dist-2] max exp 506, different 6 (1%)
c [score-dist-2] median active exp 503, avg 502.8
c [simplification-2] removed 101996 variables 13.3% (665379 remain 61%)
c [simplification-2] removed 268678 irredundant clauses 8.4% (2934589 remain 67%)
c [simplification-2] maximum reduction of 13% = max (13%, 8%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1031 (hard 11000)
c [simplification-2] 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   34.8  665378  2934589       941     565    147 138640    1    14  196   5%      5   14    4    0 8407%
c i   34.9  665377  2934589       942     565    147 138640    1    14  196   5%      5   14    4    0 8374%
c 
c [simplification-3] limit 1041 conflicts (hard 11000) hit after 1041 conflicts
c [card-2] limit 733647 based on 2934589 irredundant clauses
c [card-2] found 680 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 733647 for elimination
c [card-2] 680 out of 680 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 3894 variables
c [treelook-2] limit 731908 based on 2927634 irredundant clauses
c [treelook-2] scheduled 137728 literals 10%
c [treelook-2] scheduling used 732235 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 731908 based on 2927634 irredundant clauses
c [treelook-2] used 736325 steps
c [treelook-2] 137602 literals remain 10%
c [treelook-2] 86741 variables remain to probed next time 13%
c [decomp-7] removed 83 variables
c [treelook-2] removed 89 variables, found 3245 hbrs
c [unhide-3] limit 182952 based on 2927236 irredundant clauses
c [unhide-3-3] 363 units, 609 failed, 14051 tauts, 0 hbrs, 17677 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 660316 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 511718 not tried 77% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 148631 = 23% variables out of 660316 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 2456557 negative 95.0% of 2587104 except 130547 5.0%
c [phase-count-3] 2402611 positive 92.9% of 2587104 except 184493 7.1%
c [phase-3] phase bias: 786 positive 31%, 1729 negative 69%
c [sort-queue-3] sorted 499058 enqueued variables after 1041 conflicts
c [score-dist-3] active 12627 (2%), one 0 (0%), zero 499058 (98%)
c [score-dist-3] max exp 507, different 7 (1%)
c [score-dist-3] median active exp 503, avg 502.9
c [simplification-3] removed 153692 variables 23.1% (511685 remain 47%)
c [simplification-3] removed 347485 irredundant clauses 11.8% (2587104 remain 59%)
c [simplification-3] maximum reduction of 23% = max (23%, 12%)
c [simplification-3] large reduction 23% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13041 (soft 3041 + delta 10000)
c [simplification-3] new conflict limit 3041 (hard 13041)
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   52.3  511684  2587104      1662     924    205 95184    1    39  187   4%      6   39    6    0 5872%
c i   52.3  511677  2587104      1663     924    205 95184    1    39  187   4%      6   39    6    0 5849%
c i   53.5  511539  2587104      2106    1313    229 95192    2    39  187   5%      5   38    7    0 4486%
c i   55.7  511538  2587104      2308    1466    250 95211    2    50  187   4%      4   50    6    0 3372%
c i   59.4  511500  2587104      2792    1845    301 95250    3    65  187   5%      4   64   11    0 4479%
c 
c [simplification-4] limit 3051 conflicts (hard 13041) hit after 3051 conflicts
c [decomp-8] removed 987 variables
c [basicprobe-2] limit 20671256 based on 2583907 irredundant clauses
c [basicprobe-2-0] 393404 probes remain 77% after last round
c [basicprobe-2-0] 1105 units = 1041 failed (94%) + 64 lifted (6%)
c [basicprobe-2-0] removed 2194 variables, found 108775 hbrs
c [unhide-4] limit 161494 based on 2583907 irredundant clauses
c [unhide-4-4] 332 units, 417 failed, 10505 tauts, 0 hbrs, 46354 literals
c [elim-4] 507700 variables 100% will be scheduled this time
c [elim-4] scheduled 507700 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 560496300 steps penalty 1 = 0 + 1
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 729 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 240520 = 47% variables out of 507700 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 1768968 negative 95.6% of 1850024 except 81056 4.4%
c [phase-count-4] 1737313 positive 93.9% of 1850024 except 112711 6.1%
c [phase-4] phase bias: 1079 positive 43%, 1453 negative 57%
c [sort-queue-4] sorted 247610 enqueued variables after 3051 conflicts
c [score-dist-4] active 19570 (7%), one 0 (0%), zero 247610 (93%)
c [score-dist-4] max exp 509, different 9 (2%)
c [score-dist-4] median active exp 503, avg 503.6
c [simplification-4] removed 244320 variables 47.8% (267180 remain 24%)
c [simplification-4] removed 737080 irredundant clauses 28.5% (1850024 remain 42%)
c [simplification-4] maximum reduction of 48% = max (48%, 28%)
c [simplification-4] large reduction 48% >= 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 15051 (soft 5051 + delta 10000)
c [simplification-4] new conflict limit 5051 (hard 15051)
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   85.7  267179  1850024      3323     889    242 62643    4    70  167   6%      4   68   12    0 3570%
c i   85.8  267178  1850024      3324     889    242 62643    4    70  167   6%      4   68   12    0 3556%
c i   86.7  267177  1850024      3454    1004    249 62647    4    76  167   6%      4   74    9    0 2623%
c i   86.8  267176  1850024      3466    1015    249 62647    4    76  167   6%      4   74    9    0 2592%
c i   86.9  267175  1850024      3475    1023    249 62647    4    76  167   6%      4   75    9    0 2554%
c i   87.1  267174  1850024      3498    1044    250 62647    4    77  167   6%      4   76    9    0 2431%
c 
c [simplification-5] limit 5062 conflicts (hard 15051) hit after 5062 conflicts
c [quatres-1] found 233790 quaternary clauses 41% in total
c [quatres-1-1] removed 8 duplicate quaternary clauses
c [quatres-1-1] added 3 double-self-subsuming ternary resolvents
c [quatres-1-2] added 1469 single-self-subsuming ternary resolvents
c [quatres-1-2] added 7514 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 23667880 with penalty 0 = 0 + 0
c [ternres-1] all 267174 free variables schedulable
c [ternres-1] 99029 ternary resolvents (2639 bin, 96390 trn)
c [ternres-1] 7396 variables remain 3% (259778 retained 97%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 9493 xors of average arity 2.9
c [gauss-1] connected 27969 occurrences of 10193 variables (average 2.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 2412 variables
c [simpleprobe-3] 202388 schedulable variables 76%
c [simpleprobe-3] limit 18934307 penalty 0 = 0 + 0
c [decomp-10] removed 1094 variables
c [simpleprobe-3] 190985 variables remain 72% (72683 retained 28%)
c [simpleprobe-3] removed 1094 variables, found 46541 hbrs, 221 units
c [unhide-5] limit 118339 with penalty 3 = 0 + 3
c [unhide-5-5] 358 units, 302 failed, 29029 tauts, 0 hbrs, 37154 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 808 transitive binary clauses
c [transred-1] found 32 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 262867 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 20915 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-1-1] eliminated 5 clauses out of 9 (56%) of length 29
c [cce-1-1] eliminated 3 clauses out of 9 (33%) of length 28
c [cce-1-1] eliminated 7 clauses out of 8 (88%) of length 27
c [cce-1-1] eliminated 5 clauses out of 10 (50%) of length 26
c [cce-1-1] eliminated 2 clauses out of 9 (22%) of length 25
c [cce-1-1] eliminated 9 clauses out of 12 (75%) of length 24
c [cce-1-1] eliminated 7 clauses out of 12 (58%) of length 23
c [cce-1-1] eliminated 4 clauses out of 12 (33%) of length 22
c [cce-1-1] eliminated 2 clauses out of 12 (17%) of length 21
c [cce-1-1] eliminated 4 clauses out of 12 (33%) of length 20
c [cce-1-1] eliminated 13 clauses out of 18 (72%) of length 19
c [cce-1-1] eliminated 24 clauses out of 605 (4%) of length 18
c [cce-1-1] eliminated 283 clauses out of 784 (36%) of length 17
c [cce-1-1] eliminated 219 clauses out of 567 (39%) of length 16
c [cce-1-1] eliminated 221 clauses out of 1183 (19%) of length 15
c [cce-1-1] eliminated 487 clauses out of 1694 (29%) of length 14
c [cce-1-1] eliminated 910 clauses out of 3758 (24%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2207 large clauses in 30000003 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 1015895 clauses = 803288 binary + 212607 ternary
c [cce-1-1] tried to eliminate 7367 small clauses 1%
c [cce-1-1] eliminated 1158 binary clauses 0%
c [cce-1-1] eliminated 326 ternary clauses 0%
c [cce-1-1] eliminated 1484 small clauses 0%
c [cce-1-1] eliminated 1484 small clauses in 30000016 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3691 covered clauses in round 1
c [cce-1] eliminated 3691 covered clauses in TOTAL during 1 rounds
c [cce-1] 3691 < 1/100 * 1781501 = 17815 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 262315 variables 100%
c [elim-5] limit of 94671539 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 25255 not tried 10% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 15580 = 6% variables out of 262315 scheduled
c [bca-1] limit of 10000000 steps and 3459332 added (scaled 2)
c [bca-1] 470053 out of 493472 literals actually usable 95%
c [bca-1] added 5667 blocked clauses in 1487710 steps
c [sweep-1] limit 3458832 based on 1729416 irredundant clauses
c [sweep-1-1] 94546 pos 38.3% + 152189 neg 61.7% = 246735 sched 100.0% ret 0
c [sweep-1-1] 3478532 steps 96 queries 76205.04 avg class size
c [sweep-1-1] 1172 decisions 80 SAT calls 34.76 avg env size
c [sweep-1-1] 246331 variables remain 100% (399 retained 0%)
c [decomp-11] removed 582 variables
c [sweep-1-1] removed 582 vars (0 failed, 27 eqs, 36 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 582 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-5] 1649617 negative 95.4% of 1728264 except 78647 4.6%
c [phase-count-5] 1632947 positive 94.5% of 1728264 except 95317 5.5%
c [phase-5] phase bias: 330 positive 52%, 302 negative 48%
c [sort-queue-5] sorted 217541 enqueued variables after 5062 conflicts
c [score-dist-5] active 28612 (12%), one 0 (0%), zero 217541 (88%)
c [score-dist-5] max exp 510, different 10 (2%)
c [score-dist-5] median active exp 504, avg 504.2
c [simplification-5] removed 21021 variables 7.9% (246153 remain 22%)
c [simplification-5] removed 121760 irredundant clauses 6.6% (1728264 remain 39%)
c [simplification-5] maximum reduction of 8% = max (8%, 7%)
c [simplification-5] large reduction 8% >= 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 17062 (soft 7062 + delta 10000)
c [simplification-5] new conflict limit 7062 (hard 17062)
c 
c [simplification-6] limit 7062 conflicts (hard 17062) hit after 7062 conflicts
c [quatres-2] found 238901 quaternary clauses 42% in total
c [quatres-2-1] removed 47 duplicate quaternary clauses
c [quatres-2-1] added 22 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1642 single-self-subsuming ternary resolvents
c [quatres-2-2] added 5182 quaternary resolvents
c [ternres-2] limit 6912624 based on 1728156 irredundant clauses
c [ternres-2] 6665 schedulable variables 3%
c [ternres-2] 44270 ternary resolvents (1267 bin, 43003 trn)
c [ternres-2] 3610 variables remain 1% (242543 retained 99%)
c [card-3] limit 809131 penalty 2 = 2 + 0
c [card-3] found 403 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 809131 for elimination
c [card-3] 403 out of 403 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 296 variables
c [treelook-3] limit 647304 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 69055 literals 14%
c [treelook-3] scheduling used 647319 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 647304 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 650570 steps
c [treelook-3] 68937 literals remain 14%
c [treelook-3] 35089 variables remain to probed next time 14%
c [decomp-13] removed 6 variables
c [treelook-3] removed 12 variables, found 918 hbrs
c [unhide-6] limit 161826 with penalty 3 = 0 + 3
c [unhide-6-6] 216 units, 491 failed, 11065 tauts, 0 hbrs, 31148 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 917 transitive binary clauses
c [transred-2] found 18 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 245206 variables 100%
c [block-2] limit of 64730493 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 22331 blocked clauses
c [elim-6] 695 variables 0% will be scheduled this time
c [elim-6] scheduled 695 variables 0%
c [elim-6] limit of 129460986 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 161 not tried 0% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 49 = 7% variables out of 695 scheduled
c [elim-6] 49 < 1/100 * 695 = 6 considered unsuccessful
c [bca-2] limit of 10000000 steps and 3385045 added (scaled 2)
c [bca-2] 456770 out of 489680 literals actually usable 93%
c [bca-2] added 1482 blocked clauses in 1439940 steps
c [sweep-2] limit 3381712 based on 1690856 irredundant clauses
c [sweep-2-1] 93063 pos 38.1% + 151402 neg 61.9% = 244465 sched 99.8% ret 374
c [sweep-2-1] 3400195 steps 96 queries 72629.84 avg class size
c [sweep-2-1] 1321 decisions 91 SAT calls 31.44 avg env size
c [sweep-2-1] 243879 variables remain 100% (953 retained 0%)
c [decomp-14] removed 633 variables
c [sweep-2-1] removed 633 vars (0 failed, 13 eqs, 16 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 633 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-6] 1612704 negative 95.5% of 1689295 except 76591 4.5%
c [phase-count-6] 1592837 positive 94.3% of 1689295 except 96458 5.7%
c [phase-6] phase bias: 66 positive 42%, 90 negative 58%
c [sort-queue-6] sorted 212934 enqueued variables after 7062 conflicts
c [score-dist-6] active 31272 (13%), one 0 (0%), zero 212934 (87%)
c [score-dist-6] max exp 511, different 11 (2%)
c [score-dist-6] median active exp 504, avg 504.5
c [simplification-6] removed 1947 variables 0.8% (244206 remain 22%)
c [simplification-6] removed 38969 irredundant clauses 2.3% (1689295 remain 38%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 23728 (soft 13728 + delta 10000)
c [simplification-6] new conflict limit 13728 (hard 23728)
c 
c [simplification-7] limit 13728 conflicts (hard 23728) hit after 13728 conflicts
c [quatres-3] found 238335 quaternary clauses 43% in total
c [quatres-3-1] removed 16 duplicate quaternary clauses
c [quatres-3-1] added 8 double-self-subsuming ternary resolvents
c [quatres-3-2] added 637 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2284 quaternary resolvents
c [ternres-3] limit 11608480 with penalty 0 = 0 + 0
c [ternres-3] 3516 schedulable variables 1%
c [ternres-3] 64006 ternary resolvents (1834 bin, 62172 trn)
c [ternres-3] 1682 variables remain 1% (242524 retained 99%)
c [gauss-2] limit 1160848 penalty 1 = 1 + 0
c [gauss-2] extracted 3937 xors of average arity 3.0
c [gauss-2] connected 11732 occurrences of 4662 variables (average 2.5)
c [gauss-2] limit 1160848 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 399 variables
c [basicprobe-3] limit 58042404 penalty 0 = 0 + 0
c [basicprobe-3-0] 109531 probes remain 46% after last round
c [basicprobe-3-0] 4326 units = 3988 failed (92%) + 338 lifted (8%)
c [basicprobe-3-0] removed 5719 variables, found 200910 hbrs
c [bate-1] eliminated 3983 asymmetric tautologies during probing
c [unhide-7] limit 290212 with penalty 3 = 0 + 3
c [unhide-7-7] 52 units, 154 failed, 22712 tauts, 0 hbrs, 20428 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 1582 transitive binary clauses
c [transred-3] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 237862 variables 100%
c [block-3] limit of 116084808 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 3111 blocked clauses
c [block-3] 3111 < 1/100 * 1598191 = 15981 considered unsuccessful
c [cce-2] limit of 29021202 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 5 (40%) of length 26
c [cce-2-1] eliminated 3 clauses out of 5 (60%) of length 25
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 24
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 23
c [cce-2-1] eliminated 1 clauses out of 15 (7%) of length 19
c [cce-2-1] eliminated 8 clauses out of 551 (1%) of length 18
c [cce-2-1] eliminated 7 clauses out of 496 (1%) of length 17
c [cce-2-1] eliminated 11 clauses out of 359 (3%) of length 16
c [cce-2-1] eliminated 25 clauses out of 800 (3%) of length 15
c [cce-2-1] eliminated 315 clauses out of 1463 (22%) of length 14
c [cce-2-1] eliminated 476 clauses out of 2978 (16%) of length 13
c [cce-2-1] eliminated 347 clauses out of 5115 (7%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1197 large clauses in 29021227 steps
c [cce-2-1] allowing another 14510613 steps for small clauses
c [cce-2-1] scheduling 886914 clauses = 686139 binary + 200775 ternary
c [cce-2-1] tried to eliminate 6121 small clauses 1%
c [cce-2-1] eliminated 755 binary clauses 0%
c [cce-2-1] eliminated 294 ternary clauses 0%
c [cce-2-1] eliminated 1049 small clauses 0%
c [cce-2-1] eliminated 1049 small clauses in 29021443 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2246 covered clauses in round 1
c [cce-2] eliminated 2246 covered clauses in TOTAL during 1 rounds
c [cce-2] 2246 < 1/100 * 1593224 = 15932 considered unsuccessful
c [bca-3] limit of 10000000 steps and 3186030 added (scaled 2)
c [bca-3] 437775 out of 475430 literals actually usable 92%
c [bca-3] added 669 blocked clauses in 1328940 steps
c [sweep-3] limit 3482544 penalty 0 = 0 + 0
c [sweep-3-1] 89224 pos 37.7% + 147585 neg 62.3% = 236809 sched 99.6% ret 905
c [sweep-3-1] 3484304 steps 80 queries 71351.52 avg class size
c [sweep-3-1] 1678 decisions 76 SAT calls 49.25 avg env size
c [sweep-3-1] 236069 variables remain 99% (1643 retained 1%)
c [decomp-16] removed 5407 variables
c [sweep-3-1] removed 5407 vars (0 failed, 5 eqs, 8 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 5407 vars in TOTAL (1 rounds, 79 queries)
c [phase-count-7] 1505431 negative 95.1% of 1583057 except 77626 4.9%
c [phase-count-7] 1489298 positive 94.1% of 1583057 except 93759 5.9%
c [phase-7] phase bias: 212 positive 50%, 213 negative 50%
c [sort-queue-7] sorted 196273 enqueued variables after 13728 conflicts
c [score-dist-7] active 36034 (16%), one 0 (0%), zero 196273 (84%)
c [score-dist-7] max exp 513, different 13 (3%)
c [score-dist-7] median active exp 505, avg 505.3
c [simplification-7] removed 11899 variables 4.9% (232307 remain 21%)
c [simplification-7] removed 106238 irredundant clauses 6.3% (1583057 remain 36%)
c [simplification-7] maximum reduction of 6% = max (5%, 6%)
c [simplification-7] large reduction 6% >= 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 25728 (soft 15728 + delta 10000)
c [simplification-7] new conflict limit 15728 (hard 25728)
c 
c [simplification-8] limit 15728 conflicts (hard 25728) hit after 15728 conflicts
c [quatres-4] found 229851 quaternary clauses 44% in total
c [quatres-4-1] removed 26 duplicate quaternary clauses
c [quatres-4-1] added 43 double-self-subsuming ternary resolvents
c [quatres-4-2] added 681 single-self-subsuming ternary resolvents
c [quatres-4-2] added 2460 quaternary resolvents
c [ternres-4] limit 12984583 with penalty 0 = 0 + 0
c [ternres-4] 1594 schedulable variables 1%
c [ternres-4] 63361 ternary resolvents (1741 bin, 61620 trn)
c [ternres-4] 195 variables remain 0% (232112 retained 100%)
c [decomp-17] removed 480 variables
c [simpleprobe-4] 167024 schedulable variables 72%
c [simpleprobe-4] limit 51938334 penalty 0 = 0 + 0
c [decomp-18] removed 3284 variables
c [simpleprobe-4] 110814 variables remain 48% (117729 retained 52%)
c [simpleprobe-4] removed 3284 variables, found 87869 hbrs, 619 units
c [unhide-8] limit 649229 with penalty 2 = 0 + 2
c [unhide-8-8] 107 units, 217 failed, 32873 tauts, 0 hbrs, 32543 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1579 transitive binary clauses
c [transred-4] found 9 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 228249 variables 100%
c [elim-7] limit of 129845835 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 6602 not tried 3% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 15973 = 7% variables out of 228249 scheduled
c [bca-4] limit of 10000000 steps and 2992297 added (scaled 2)
c [bca-4] 388773 out of 424554 literals actually usable 92%
c [bca-4] added 1310 blocked clauses in 1234219 steps
c [sweep-4] limit 3895375 penalty 0 = 0 + 0
c [sweep-4-1] 78421 pos 37.2% + 132360 neg 62.8% = 210781 sched 99.3% ret 1495
c [sweep-4-1] 3904897 steps 124 queries 66632.27 avg class size
c [sweep-4-1] 1300 decisions 109 SAT calls 34.73 avg env size
c [sweep-4-1] 210269 variables remain 99% (2006 retained 1%)
c [decomp-19] removed 701 variables
c [sweep-4-1] removed 701 vars (0 failed, 22 eqs, 34 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 701 vars in TOTAL (1 rounds, 123 queries)
c [phase-count-8] 1418844 negative 95.1% of 1492309 except 73465 4.9%
c [phase-count-8] 1402141 positive 94.0% of 1492309 except 90168 6.0%
c [phase-8] phase bias: 205 positive 51%, 195 negative 49%
c [sort-queue-8] sorted 177460 enqueued variables after 15728 conflicts
c [score-dist-8] active 34115 (16%), one 0 (0%), zero 177460 (84%)
c [score-dist-8] max exp 514, different 14 (3%)
c [score-dist-8] median active exp 505, avg 505.4
c [simplification-8] removed 20732 variables 8.9% (211575 remain 19%)
c [simplification-8] removed 90748 irredundant clauses 5.7% (1492309 remain 34%)
c [simplification-8] maximum reduction of 9% = max (9%, 6%)
c [simplification-8] large reduction 9% >= 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 27728 (soft 17728 + delta 10000)
c [simplification-8] new conflict limit 17728 (hard 27728)
c 
c [simplification-9] limit 17728 conflicts (hard 27728) hit after 17728 conflicts
c [quatres-5] found 230706 quaternary clauses 45% in total
c [quatres-5-1] removed 216 duplicate quaternary clauses
c [quatres-5-1] added 21 double-self-subsuming ternary resolvents
c [quatres-5-2] added 716 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3912 quaternary resolvents
c [ternres-5] limit 14221875 with penalty 0 = 0 + 0
c [ternres-5] 180 schedulable variables 0%
c [ternres-5] 37798 ternary resolvents (855 bin, 36943 trn)
c [ternres-5] 6 variables remain 0% (211569 retained 100%)
c [decomp-20] removed 200 variables
c [treelook-4] limit 1422187 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 106115 literals 25%
c [treelook-4] scheduling used 1422190 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1422187 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1458036 steps
c [treelook-4] 106016 literals remain 25%
c [treelook-4] 28528 variables remain to probed next time 13%
c [decomp-21] removed 9 variables
c [treelook-4] removed 23 variables, found 1711 hbrs
c [unhide-9] limit 711093 with penalty 2 = 0 + 2
c [unhide-9-9] 90 units, 148 failed, 12022 tauts, 0 hbrs, 10848 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1400 transitive binary clauses
c [transred-5] found 10 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 211100 variables 100%
c [block-4] limit of 71109378 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 4800 blocked clauses
c [block-4] 4800 < 1/100 * 1481058 = 14810 considered unsuccessful
c [elim-8] 161 variables 0% will be scheduled this time
c [elim-8] scheduled 161 variables 0%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5688750300 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 44863126 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1 = 1% variables out of 161 scheduled
c [elim-8] 1 < 1/100 * 161 = 1 considered unsuccessful
c [bca-5] limit of 10000000 steps and 2950548 added (scaled 2)
c [bca-5] 381213 out of 421876 literals actually usable 90%
c [bca-5] added 250 blocked clauses in 1208655 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 42665620 penalty 0 = 0 + 0
c [sweep-5-1] 77581 pos 37.1% + 131378 neg 62.9% = 208959 sched 99.1% ret 1978
c [sweep-5-1] 42697146 steps 1195 queries 25871.38 avg class size
c [sweep-5-1] 15604 decisions 1148 SAT calls 34.83 avg env size
c [sweep-5-1] 196257 variables remain 93% (14597 retained 7%)
c [decomp-22] removed 896 variables
c [sweep-5-1] removed 896 vars (0 failed, 185 eqs, 226 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 896 vars in TOTAL (1 rounds, 1194 queries)
c [phase-count-9] 1396549 negative 95.0% of 1469837 except 73288 5.0%
c [phase-count-9] 1380849 positive 93.9% of 1469837 except 88988 6.1%
c [phase-9] phase bias: 40 positive 40%, 60 negative 60%
c [sort-queue-9] sorted 171957 enqueued variables after 17728 conflicts
c [score-dist-9] active 38084 (18%), one 0 (0%), zero 171957 (82%)
c [score-dist-9] max exp 514, different 14 (3%)
c [score-dist-9] median active exp 505, avg 505.3
c [simplification-9] removed 1534 variables 0.7% (210041 remain 19%)
c [simplification-9] removed 22472 irredundant clauses 1.5% (1469837 remain 33%)
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 13332
c [simplification-9] penalized conflict interval 13332 = 1 * 13332
c [simplification-9] hard conflict limit 41060 (soft 31060 + delta 10000)
c [simplification-9] new conflict limit 31060 (hard 41060)
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  236.1  210040  1469837     23046   29992 131532 214511   34   106  171  32%    252   75   32   10  324%
c i  236.8  210039  1469837     23580   30497 131533 214513   34   106  171  32%    134   75   36   10  350%
c i  237.0  210038  1469837     23769   30663 131534 214514   34   106  171  32%    105   75   37   10  362%
c i  238.2  210031  1469837     24632   31439 131539 214516   36   106  171  34%     26   73   48   11  453%
c i  239.9  209994  1469837     25540   32280 131551 214522   36   105  172  34%     -8   71   35   11  320%
c i  242.6  209993  1469837     27183   33820 131570 214544   35   103  172  34%    -20   67   27   12  235%
c i  248.7  209992  1469837     30880   37288 131615 214575   34    95  173  36%      4   57   37   13  286%
c i  249.9  209991  1469837     31496   37868 131622 214577   36    93  173  39%    -13   54   49   13  377%
c i  255.6  209990  1469837     34414   40619 131656 214591   37    85  175  43%     -6   43   39   14  276%
c i  261.7  209989  1469837     37191   43151 131692 214606   40    77  176  52%     -7   34   37   15  241%
c 
c [simplification-10] limit 31060 conflicts (hard 41060) hit after 40442 conflicts
c [quatres-6] found 231140 quaternary clauses 45% in total
c [quatres-6-1] removed 15 duplicate quaternary clauses
c [quatres-6-1] added 14 double-self-subsuming ternary resolvents
c [quatres-6-2] added 350 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1274 quaternary resolvents
c [ternres-6] limit 23412931 with penalty 0 = 0 + 0
c [ternres-6] 6 schedulable variables 0%
c [ternres-6] 17613 ternary resolvents (213 bin, 17400 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1463308 penalty 3 = 3 + 0
c [card-4] found 776 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1463308 for elimination
c [card-4] 776 out of 776 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1170646 penalty 2 = 2 + 0
c [gauss-3] extracted 3051 xors of average arity 3.0
c [gauss-3] connected 9122 occurrences of 3545 variables (average 2.6)
c [gauss-3] limit 1170646 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 59 variables
c [basicprobe-4] limit 117064656 penalty 0 = 0 + 0
c [basicprobe-4-0] 90944 sched 46%, 5047 failed, 293 lifted, 171961 hbrs
c [decomp-24] removed 15978 variables
c [basicprobe-4-1] 100408 probes remain 53% after last round
c [basicprobe-4-1] 5953 units = 5631 failed (95%) + 322 lifted (5%)
c [basicprobe-4-1] removed 20178 variables, found 190442 hbrs
c [bate-2] eliminated 5509 asymmetric tautologies during probing
c [unhide-10] limit 1170646 with penalty 2 = 0 + 2
c [unhide-10-10] 62 units, 82 failed, 29894 tauts, 0 hbrs, 70714 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2166 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 29266164 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 22
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 19
c [cce-3-1] eliminated 6 clauses out of 519 (1%) of length 18
c [cce-3-1] eliminated 16 clauses out of 662 (2%) of length 17
c [cce-3-1] eliminated 11 clauses out of 346 (3%) of length 16
c [cce-3-1] eliminated 13 clauses out of 928 (1%) of length 15
c [cce-3-1] eliminated 32 clauses out of 893 (4%) of length 14
c [cce-3-1] eliminated 545 clauses out of 2564 (21%) of length 13
c [cce-3-1] eliminated 124 clauses out of 4784 (3%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 755 large clauses in 29266330 steps
c [cce-3-1] allowing another 14633165 steps for small clauses
c [cce-3-1] scheduling 699271 clauses = 542702 binary + 156569 ternary
c [cce-3-1] tried to eliminate 7425 small clauses 1%
c [cce-3-1] eliminated 1663 binary clauses 0%
c [cce-3-1] eliminated 410 ternary clauses 0%
c [cce-3-1] eliminated 2073 small clauses 0%
c [cce-3-1] eliminated 2986 small clauses in 29266167 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3741 covered clauses in round 1
c [cce-3] eliminated 3741 covered clauses in TOTAL during 1 rounds
c [cce-3] 3741 < 1/100 * 1307929 = 13079 considered unsuccessful
c [bca-6] limit of 10000000 steps and 2613565 added (scaled 2)
c [bca-6] 339893 out of 379262 literals actually usable 90%
c [bca-6] added 584 blocked clauses in 1068502 steps
c [sweep-6] limit 7023879 penalty 0 = 0 + 0
c [sweep-6-1] 64619 pos 36.5% + 112388 neg 63.5% = 177007 sched 93.3% ret 12623
c [sweep-6-1] 7034610 steps 233 queries 40995.63 avg class size
c [sweep-6-1] 3099 decisions 215 SAT calls 34.05 avg env size
c [sweep-6-1] 175195 variables remain 92% (14434 retained 8%)
c [decomp-25] removed 1781 variables
c [sweep-6-1] removed 1781 vars (0 failed, 22 eqs, 37 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 1781 vars in TOTAL (1 rounds, 232 queries)
c [phase-count-10] 1232304 negative 94.8% of 1299769 except 67465 5.2%
c [phase-count-10] 1214022 positive 93.4% of 1299769 except 85747 6.6%
c [phase-10] phase bias: 188 positive 55%, 151 negative 45%
c [sort-queue-10] sorted 151294 enqueued variables after 40442 conflicts
c [score-dist-10] active 36555 (19%), one 0 (0%), zero 151294 (81%)
c [score-dist-10] max exp 516, different 16 (3%)
c [score-dist-10] median active exp 505, avg 505.6
c [simplification-10] removed 22140 variables 10.5% (187849 remain 17%)
c [simplification-10] removed 170068 irredundant clauses 11.6% (1299769 remain 30%)
c [simplification-10] maximum reduction of 12% = max (11%, 12%)
c [simplification-10] large reduction 12% >= 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 52442 (soft 42442 + delta 10000)
c [simplification-10] new conflict limit 42442 (hard 52442)
c 
c [simplification-11] limit 42442 conflicts (hard 52442) hit after 42442 conflicts
c [quatres-7] found 208853 quaternary clauses 46% in total
c [quatres-7-1] removed 74 duplicate quaternary clauses
c [quatres-7-1] added 114 double-self-subsuming ternary resolvents
c [quatres-7-2] added 838 single-self-subsuming ternary resolvents
c [quatres-7-2] added 2221 quaternary resolvents
c [ternres-7] limit 24107338 with penalty 0 = 0 + 0
c [ternres-7] all 187849 free variables schedulable
c [ternres-7] 22461 ternary resolvents (887 bin, 21574 trn)
c [ternres-7] 8068 variables remain 4% (179781 retained 96%)
c [decomp-26] removed 112 variables
c [simpleprobe-5] 88814 schedulable variables 47%
c [simpleprobe-5] limit 96429353 penalty 0 = 0 + 0
c [decomp-27] removed 3556 variables
c [simpleprobe-5] 52222 variables remain 28% (131959 retained 72%)
c [simpleprobe-5] removed 3556 variables, found 134891 hbrs, 315 units
c [unhide-11] limit 1205366 with penalty 2 = 0 + 2
c [unhide-11-11] 26 units, 23 failed, 15162 tauts, 0 hbrs, 16904 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2347 transitive binary clauses
c [transred-7] found 3 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 184126 variables 100%
c [elim-9] limit of 241073384 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 1225 not tried 1% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 13301 = 7% variables out of 184126 scheduled
c [bca-7] limit of 10000000 steps and 2428549 added (scaled 2)
c [bca-7] 303500 out of 341652 literals actually usable 89%
c [bca-7] added 1558 blocked clauses in 984408 steps
c [sweep-7] limit 7232201 penalty 0 = 0 + 0
c [sweep-7-1] 56477 pos 35.9% + 101011 neg 64.1% = 157488 sched 92.2% ret 13337
c [sweep-7-1] 7252632 steps 255 queries 29768.98 avg class size
c [sweep-7-1] 3867 decisions 246 SAT calls 37.67 avg env size
c [sweep-7-1] 155365 variables remain 91% (15396 retained 9%)
c [decomp-28] removed 449 variables
c [sweep-7-1] removed 449 vars (0 failed, 39 eqs, 48 impls)
c [sweep-7] removed 449 vars in TOTAL (1 rounds, 254 queries)
c [phase-count-11] 1147371 negative 94.9% of 1209596 except 62225 5.1%
c [phase-count-11] 1129584 positive 93.4% of 1209596 except 80012 6.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 171 positive 46%, 199 negative 54%
c [sort-queue-11] sorted 135922 enqueued variables after 42442 conflicts
c [score-dist-11] active 34454 (20%), one 0 (0%), zero 135922 (80%)
c [score-dist-11] max exp 516, different 16 (3%)
c [score-dist-11] median active exp 505, avg 505.6
c [simplification-11] removed 17473 variables 9.3% (170376 remain 16%)
c [simplification-11] removed 90173 irredundant clauses 6.9% (1209596 remain 28%)
c [simplification-11] maximum reduction of 9% = max (9%, 7%)
c [simplification-11] large reduction 9% >= 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 54442 (soft 44442 + delta 10000)
c [simplification-11] new conflict limit 44442 (hard 54442)
c 
c [simplification-12] limit 44442 conflicts (hard 54442) hit after 44443 conflicts
c [quatres-8] found 202279 quaternary clauses 46% in total
c [quatres-8-1] removed 859 duplicate quaternary clauses
c [quatres-8-1] added 40 double-self-subsuming ternary resolvents
c [quatres-8-2] added 493 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2755 quaternary resolvents
c [ternres-8] limit 24675422 with penalty 0 = 0 + 0
c [ternres-8] 7218 schedulable variables 4%
c [ternres-8] 28420 ternary resolvents (1069 bin, 27351 trn)
c [ternres-8] 323 variables remain 0% (170053 retained 100%)
c [decomp-29] removed 243 variables
c [treelook-5] limit 2467542 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 130819 literals 38%
c [treelook-5] scheduling used 2467570 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 2467542 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2526816 steps
c [treelook-5] 130514 literals remain 38%
c [treelook-5] 22353 variables remain to probed next time 13%
c [decomp-30] removed 15 variables
c [treelook-5] removed 20 variables, found 2109 hbrs
c [unhide-12] limit 1233771 with penalty 2 = 0 + 2
c [unhide-12-12] 28 units, 214 failed, 42155 tauts, 0 hbrs, 30179 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2293 transitive binary clauses
c [transred-8] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 169948 variables 100%
c [block-5] limit of 61688555 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2672 blocked clauses
c [block-5] 2672 < 1/100 * 1207527 = 12075 considered unsuccessful
c [elim-10] 1222 variables 1% will be scheduled this time
c [elim-10] scheduled 1222 variables 1%
c [elim-10] limit of 493508443 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 191720662 steps
c [elim-10] fully completed in 1 rounds
c [gc-86] reconnected 287581 binary clauses (produced 0 empty 1 units)
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 118 = 10% variables out of 1222 scheduled
c [elim-10] 118 < 1/100 * 1222 = 12 considered unsuccessful
c [bca-8] limit of 10000000 steps and 2407902 added (scaled 2)
c [bca-8] 298538 out of 339508 literals actually usable 88%
c [bca-8] added 418 blocked clauses in 954450 steps
c [sweep-8] limit 7402626 penalty 0 = 0 + 0
c [sweep-8-1] 55626 pos 36.0% + 98833 neg 64.0% = 154459 sched 91.0% ret 15294
c [sweep-8-1] 7418330 steps 298 queries 39665.98 avg class size
c [sweep-8-1] 3495 decisions 281 SAT calls 33.27 avg env size
c [sweep-8-1] 152575 variables remain 90% (17120 retained 10%)
c [decomp-31] removed 543 variables
c [sweep-8-1] removed 543 vars (0 failed, 43 eqs, 49 impls)
c [sweep-8] removed 543 vars in TOTAL (1 rounds, 297 queries)
c [phase-count-12] 1135900 negative 94.8% of 1198766 except 62866 5.2%
c [phase-count-12] 1117903 positive 93.3% of 1198766 except 80863 6.7%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 70 positive 49%, 74 negative 51%
c [sort-queue-12] sorted 134408 enqueued variables after 44443 conflicts
c [score-dist-12] active 34802 (21%), one 0 (0%), zero 134408 (79%)
c [score-dist-12] max exp 516, different 16 (3%)
c [score-dist-12] median active exp 505, avg 505.6
c [simplification-12] removed 1166 variables 0.7% (169210 remain 15%)
c [simplification-12] removed 10830 irredundant clauses 0.9% (1198766 remain 27%)
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 23332
c [simplification-12] penalized conflict interval 23332 = 1 * 23332
c [simplification-12] hard conflict limit 79441 (soft 67775 + delta 11666)
c [simplification-12] new conflict limit 67775 (hard 79441)
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  320.4  169209  1198766     45633   42838 111796 287277   40    60  162  66%     76   14   35   18  190%
c i  320.7  169208  1198766     46156   43272 111797 287278   40    59  162  68%     31   12   39   19  211%
c i  320.8  169207  1198766     46305   43394 111796 287282   40    58  162  69%     22   12   38   19  203%
c 
c [simplification-13] limit 67775 conflicts (hard 79441) hit after 67775 conflicts
c [quatres-9] found 200370 quaternary clauses 46% in total
c [quatres-9-1] removed 19 duplicate quaternary clauses
c [quatres-9-1] added 19 double-self-subsuming ternary resolvents
c [quatres-9-2] added 471 single-self-subsuming ternary resolvents
c [quatres-9-2] added 777 quaternary resolvents
c [ternres-9] limit 33645836 with penalty 0 = 0 + 0
c [ternres-9] 310 schedulable variables 0%
c [ternres-9] 20899 ternary resolvents (650 bin, 20249 trn)
c [ternres-9] 6 variables remain 0% (169196 retained 100%)
c [decomp-32] removed 169 variables
c [basicprobe-5] limit 168229180 penalty 0 = 0 + 0
c [basicprobe-5-0] 87332 sched 53%, 1976 failed, 395 lifted, 50669 hbrs
c [decomp-33] removed 6012 variables
c [basicprobe-5-1] 57639 probes remain 36% after last round
c [basicprobe-5-1] 2835 units = 2394 failed (84%) + 441 lifted (16%)
c [basicprobe-5-1] removed 7209 variables, found 61970 hbrs
c [bate-3] eliminated 4363 asymmetric tautologies during probing
c [unhide-13] limit 1682291 with penalty 2 = 0 + 2
c [unhide-13-13] 23 units, 79 failed, 11396 tauts, 0 hbrs, 90052 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2404 transitive binary clauses
c [transred-9] found 2 units
c [bca-9] limit of 10000000 steps and 2260057 added (scaled 2)
c [bca-9] 281461 out of 323534 literals actually usable 87%
c [bca-9] added 148 blocked clauses in 913221 steps
c [sweep-9] limit 10093750 penalty 0 = 0 + 0
c [sweep-9-1] 51179 pos 35.1% + 94435 neg 64.9% = 145614 sched 90.0% ret 16152
c [sweep-9-1] 10136211 steps 357 queries 30002.43 avg class size
c [sweep-9-1] 4844 decisions 340 SAT calls 37.99 avg env size
c [sweep-9-1] 142852 variables remain 88% (18913 retained 12%)
c [decomp-34] removed 818 variables
c [sweep-9-1] removed 818 vars (0 failed, 45 eqs, 51 impls)
c [sweep-9] removed 818 vars in TOTAL (1 rounds, 356 queries)
c [phase-count-13] 1064785 negative 94.7% of 1124639 except 59854 5.3%
c [phase-count-13] 1045291 positive 92.9% of 1124639 except 79348 7.1%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 84 positive 40%, 127 negative 60%
c [sort-queue-13] sorted 124094 enqueued variables after 67775 conflicts
c [score-dist-13] active 36854 (23%), one 0 (0%), zero 124094 (77%)
c [score-dist-13] max exp 516, different 16 (3%)
c [score-dist-13] median active exp 505, avg 505.9
c [simplification-13] removed 8254 variables 4.9% (160948 remain 15%)
c [simplification-13] removed 74127 irredundant clauses 6.2% (1124639 remain 26%)
c [simplification-13] maximum reduction of 6% = max (5%, 6%)
c [simplification-13] large reduction 6% >= 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 79775 (soft 69775 + delta 10000)
c [simplification-13] new conflict limit 69775 (hard 79775)
c 
c [simplification-14] limit 69775 conflicts (hard 79775) hit after 69777 conflicts
c [quatres-10] found 187276 quaternary clauses 46% in total
c [quatres-10-1] removed 133 duplicate quaternary clauses
c [quatres-10-1] added 18 double-self-subsuming ternary resolvents
c [quatres-10-2] added 508 single-self-subsuming ternary resolvents
c [quatres-10-2] added 859 quaternary resolvents
c [ternres-10] limit 34961164 with penalty 0 = 0 + 0
c [ternres-10] 6 schedulable variables 0%
c [ternres-10] 5551 ternary resolvents (40 bin, 5511 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 874029 penalty 3 = 3 + 0
c [gauss-4] extracted 1960 xors of average arity 3.0
c [gauss-4] connected 5864 occurrences of 2524 variables (average 2.3)
c [gauss-4] limit 874029 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-35] removed 11 variables
c [simpleprobe-6] 44708 schedulable variables 28%
c [simpleprobe-6] limit 139844656 penalty 0 = 0 + 0
c [decomp-36] removed 3057 variables
c [simpleprobe-6] 24937 variables remain 16% (132943 retained 84%)
c [simpleprobe-6] removed 3057 variables, found 115154 hbrs, 159 units
c [unhide-14] limit 1748058 with penalty 2 = 0 + 2
c [unhide-14-14] 5 units, 25 failed, 63156 tauts, 0 hbrs, 65755 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2207 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 218507275 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 260 (0%) of length 16
c [cce-4-1] eliminated 2 clauses out of 972 (0%) of length 15
c [cce-4-1] eliminated 18 clauses out of 929 (2%) of length 14
c [cce-4-1] eliminated 14 clauses out of 1747 (1%) of length 13
c [cce-4-1] eliminated 488 clauses out of 3817 (13%) of length 12
c [cce-4-1] eliminated 542 clauses out of 4868 (11%) of length 11
c [cce-4-1] eliminated 4550 clauses out of 11258 (40%) of length 10
c [cce-4-1] eliminated 3604 clauses out of 11604 (31%) of length 9
c [cce-4-1] eliminated 4507 clauses out of 18584 (24%) of length 8
c [cce-4-1] eliminated 4146 clauses out of 23622 (18%) of length 7
c [cce-4-1] eliminated 5253 clauses out of 42362 (12%) of length 6
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 23125 large clauses in 218507371 steps
c [cce-4-1] allowing another 109253685 steps for small clauses
c [cce-4-1] scheduling 587262 clauses = 447297 binary + 139965 ternary
c [cce-4-1] tried to eliminate 64598 small clauses 11%
c [cce-4-1] eliminated 7523 binary clauses 2%
c [cce-4-1] eliminated 2584 ternary clauses 2%
c [cce-4-1] eliminated 10107 small clauses 2%
c [cce-4-1] eliminated 10569 small clauses in 218507575 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 33694 covered clauses in round 1
c [cce-4] eliminated 33694 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 157792 variables 100%
c [elim-11] limit of 349611641 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 12540 variables 8% in round 1 in 316777020 steps
c [elim-11-1] backward subsumption/strengthening limit 32834621
c [elim-11-1-1] backward checking 54817 touched variables 35%
c [elim-11-1-1] incomplete backward checking 34728 remain 63%
c [elim-11-1] subsumed 521 and strengthened 422 clauses in 32834674 steps
c [elim-11] incomplete 2508 not tried 2% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 12551 = 8% variables out of 157792 scheduled
c [bca-10] limit of 10000000 steps and 2048227 added (scaled 2)
c [bca-10] 252037 out of 290484 literals actually usable 87%
c [bca-10] added 2821 blocked clauses in 812741 steps
c [sweep-10] limit 10488349 penalty 0 = 0 + 0
c [sweep-10-1] 44039 pos 34.4% + 84138 neg 65.6% = 128177 sched 88.3% ret 17064
c [sweep-10-1] 10502524 steps 377 queries 21423.71 avg class size
c [sweep-10-1] 5708 decisions 373 SAT calls 41.49 avg env size
c [sweep-10-1] 124595 variables remain 86% (20619 retained 14%)
c [decomp-37] removed 338 variables
c [sweep-10-1] removed 338 vars (0 failed, 41 eqs, 42 impls)
c [sweep-10] removed 338 vars in TOTAL (1 rounds, 376 queries)
c [phase-count-14] 963598 negative 94.5% of 1019773 except 56175 5.5%
c [phase-count-14] 947620 positive 92.9% of 1019773 except 72153 7.1%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 138 positive 46%, 160 negative 54%
c [sort-queue-14] sorted 109639 enqueued variables after 69777 conflicts
c [score-dist-14] active 35264 (24%), one 0 (0%), zero 109639 (76%)
c [score-dist-14] max exp 516, different 16 (3%)
c [score-dist-14] median active exp 505, avg 506.0
c [simplification-14] removed 16045 variables 10.0% (144903 remain 13%)
c [simplification-14] removed 104866 irredundant clauses 9.3% (1019773 remain 23%)
c [simplification-14] maximum reduction of 10% = max (10%, 9%)
c [simplification-14] large reduction 10% >= 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 81777 (soft 71777 + delta 10000)
c [simplification-14] new conflict limit 71777 (hard 81777)
c 
c [simplification-15] limit 71777 conflicts (hard 81777) hit after 71777 conflicts
c [quatres-11] found 180417 quaternary clauses 49% in total
c [quatres-11-1] removed 470 duplicate quaternary clauses
c [quatres-11-1] added 14 double-self-subsuming ternary resolvents
c [quatres-11-2] added 505 single-self-subsuming ternary resolvents
c [quatres-11-2] added 2471 quaternary resolvents
c [ternres-11] limit 36220979 with penalty 0 = 0 + 0
c [ternres-11] all 144903 free variables schedulable
c [ternres-11] 21069 ternary resolvents (808 bin, 20261 trn)
c [ternres-11] 1526 variables remain 1% (143377 retained 99%)
c [card-5] limit 1131905 penalty 4 = 4 + 0
c [card-5] found 724 at-most-one constraints of average size 3.3
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1131905 for elimination
c [card-5] 724 out of 724 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-38] removed 69 variables
c [treelook-6] limit 3622097 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 129082 literals 45%
c [treelook-6] scheduling used 2777930 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3622097 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3729525 steps
c [treelook-6] 128853 literals remain 44%
c [treelook-6] 19390 variables remain to probed next time 13%
c [decomp-39] removed 6 variables
c [treelook-6] removed 11 variables, found 4126 hbrs
c [unhide-15] limit 1811048 with penalty 2 = 0 + 2
c [unhide-15-15] 5 units, 19 failed, 5571 tauts, 0 hbrs, 12550 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 2348 transitive binary clauses
c [transred-11] found 4 units
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 144781 variables 100%
c [elim-12] limit of 724419590 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 2257 variables 2% in round 1 in 303575859 steps
c [elim-12-1] backward subsumption/strengthening limit 303575800
c [elim-12-1-1] backward checking 15517 touched variables 11%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 139 and strengthened 108 clauses in 23442908 steps
c [elim-12-1] rescheduled 744 variables 1% by backward subsumption
c [elim-12-2] eliminated 32 variables 0% in round 2 in 4844473 steps
c [elim-12-2] backward subsumption/strengthening limit 4844400
c [elim-12-2-1] backward checking 236 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 25 and strengthened 12 clauses in 845306 steps
c [elim-12-2] rescheduled 92 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 922916 steps
c [elim-12-3] backward subsumption/strengthening limit 922900
c [elim-12-3-1] backward checking 23 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 6 and strengthened 1 clauses in 497696 steps
c [elim-12] incomplete 17 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 2291 = 2% variables out of 144781 scheduled
c [bca-11] limit of 10000000 steps and 2018715 added (scaled 2)
c [bca-11] 244016 out of 284982 literals actually usable 86%
c [bca-11] added 422 blocked clauses in 792350 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 108662930 penalty 0 = 0 + 0
c [sweep-11-1] 41992 pos 34.3% + 80284 neg 65.7% = 122276 sched 85.8% ret 20214
c [sweep-11-1] 108667658 steps 3550 queries 4183.99 avg class size
c [sweep-11-1] 46504 decisions 3370 SAT calls 35.31 avg env size
c [sweep-11-1] 77797 variables remain 55% (64592 retained 45%)
c [decomp-40] removed 953 variables
c [sweep-11-1] removed 953 vars (0 failed, 603 eqs, 638 impls)
c [sweep-11] removed 953 vars in TOTAL (1 rounds, 3549 queries)
c [phase-count-15] 945630 negative 94.4% of 1001921 except 56291 5.6%
c [phase-count-15] 929942 positive 92.8% of 1001921 except 71979 7.2%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 41 positive 53%, 36 negative 47%
c [sort-queue-15] sorted 97978 enqueued variables after 71777 conflicts
c [score-dist-15] active 43559 (31%), one 0 (0%), zero 97978 (69%)
c [score-dist-15] max exp 516, different 16 (3%)
c [score-dist-15] median active exp 504, avg 505.5
c [simplification-15] removed 3366 variables 2.3% (141537 remain 13%)
c [simplification-15] removed 17852 irredundant clauses 1.8% (1001921 remain 23%)
c [simplification-15] maximum reduction of 2% = max (2%, 2%)
c [simplification-15] geometric conflict interval increment 7777 = 23332 / 3
c [simplification-15] new conflict interval 31109
c [simplification-15] penalized conflict interval 31109 = 1 * 31109
c [simplification-15] hard conflict limit 118440 (soft 102886 + delta 15554)
c [simplification-15] new conflict limit 102886 (hard 118440)
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  433.2  141536  1001921     71873   55604 114312 286745   33    74  159  45%    292   19   46   20  227%
c i  459.4  141535  1001921     78787   61668 114329 286760   40    78  163  51%      0   21   31   22  138%
c i  469.4  141534  1001921     85315   68002 114356 286777   39    82  167  47%     -2   23   41   24  173%
c i  476.0  141533  1001921     89255   71672 114370 286791   35    75  169  47%    -38   15   32   24  131%
c i  476.7  141532  1001921     89903   72262 114376 286795   35    74  169  47%    -57   13   32   25  129%
c -  476.8  141532  1001921     89933   44754 114377 286795   34    74  147  47%    -58   13   30   24  124%
c i  483.0  141531  1001921     93645   48175 114398 286802   33    71  151  46%    -38   10   26   25  106%
c i  498.6  141519  1001921    102177   56194 114468 286848   26    68  154  38%     38    6   22   25   89%
c i  499.0  141518  1001921    102365   56367 114471 286849   26    68  155  38%     19    6   22   25   87%
c 
c [simplification-16] limit 102886 conflicts (hard 118440) hit after 108259 conflicts
c [quatres-12] found 179776 quaternary clauses 49% in total
c [quatres-12-1] removed 53 duplicate quaternary clauses
c [quatres-12-1] added 35 double-self-subsuming ternary resolvents
c [quatres-12-2] added 600 single-self-subsuming ternary resolvents
c [quatres-12-2] added 1331 quaternary resolvents
c [ternres-12] limit 58392349 with penalty 0 = 0 + 0
c [ternres-12] 1470 schedulable variables 1%
c [ternres-12] 14291 ternary resolvents (714 bin, 13577 trn)
c [ternres-12] 1 variables remain 0% (141517 retained 100%)
c [decomp-41] removed 105 variables
c [basicprobe-6] limit 291961745 penalty 0 = 0 + 0
c [basicprobe-6-0] 51229 sched 37%, 625 failed, 13 lifted, 20730 hbrs
c [decomp-42] removed 1618 variables
c [basicprobe-6-1] 89816 sched 65%, 616 failed, 15 lifted, 15475 hbrs
c [decomp-43] removed 1813 variables
c [basicprobe-6-2] 64370 probes remain 47% after last round
c [basicprobe-6-2] 1299 units = 1271 failed (98%) + 28 lifted (2%)
c [basicprobe-6-2] removed 3471 variables, found 37288 hbrs
c [bate-4] eliminated 2564 asymmetric tautologies during probing
c [unhide-16] limit 2919617 with penalty 2 = 0 + 2
c [unhide-16-16] 5 units, 30 failed, 35580 tauts, 0 hbrs, 57498 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 2047 transitive binary clauses
c [transred-12] found 2 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 137948 variables 100%
c [block-6] limit of 72990436 steps penalty 3 = 3 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 3621 blocked clauses
c [block-6] 3621 < 1/100 * 966091 = 9660 considered unsuccessful
c [cce-5] limit of 72990436 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-5-1] eliminated 3 clauses out of 3 (100%) of length 21
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-5-1] eliminated 7 clauses out of 394 (2%) of length 18
c [cce-5-1] eliminated 1 clauses out of 316 (0%) of length 17
c [cce-5-1] eliminated 1 clauses out of 414 (0%) of length 16
c [cce-5-1] eliminated 49 clauses out of 813 (6%) of length 15
c [cce-5-1] eliminated 58 clauses out of 838 (7%) of length 14
c [cce-5-1] eliminated 98 clauses out of 1598 (6%) of length 13
c [cce-5-1] eliminated 316 clauses out of 2571 (12%) of length 12
c [cce-5-1] eliminated 677 clauses out of 3255 (21%) of length 11
c [cce-5-1] eliminated 1020 clauses out of 5859 (17%) of length 10
c [cce-5-1] eliminated 1021 clauses out of 8929 (11%) of length 9
c [cce-5-1] eliminated 21 clauses out of 14246 (0%) of length 8
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 3274 large clauses in 72990452 steps
c [cce-5-1] allowing another 36495226 steps for small clauses
c [cce-5-1] scheduling 506519 clauses = 375729 binary + 130790 ternary
c [cce-5-1] tried to eliminate 21839 small clauses 4%
c [cce-5-1] eliminated 3774 binary clauses 1%
c [cce-5-1] eliminated 1264 ternary clauses 1%
c [cce-5-1] eliminated 5038 small clauses 1%
c [cce-5-1] eliminated 5038 small clauses in 72990436 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 8312 covered clauses in round 1
c [cce-5] eliminated 8312 covered clauses in TOTAL during 1 rounds
c [cce-5] 8312 < 1/100 * 962267 = 9622 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 137747 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 3778 variables 3% in round 1 in 277944996 steps
c [elim-13-1] backward subsumption/strengthening limit 277944900
c [elim-13-1-1] backward checking 26644 touched variables 19%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 290 and strengthened 412 clauses in 30647276 steps
c [elim-13-1] rescheduled 3786 variables 3% by backward subsumption
c [elim-13-2] eliminated 69 variables 0% in round 2 in 23082890 steps
c [elim-13-2] backward subsumption/strengthening limit 23082800
c [elim-13-2-1] backward checking 568 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 24 and strengthened 45 clauses in 1534457 steps
c [elim-13-2] rescheduled 186 variables 0% by backward subsumption
c [elim-13-3] eliminated 6 variables 0% in round 3 in 2186570 steps
c [elim-13-3] backward subsumption/strengthening limit 2186500
c [elim-13-3-1] backward checking 49 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 2 and strengthened 5 clauses in 564849 steps
c [elim-13] incomplete 12 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 3935 = 3% variables out of 137747 scheduled
c [bca-12] limit of 10000000 steps and 1876660 added (scaled 2)
c [bca-12] 225613 out of 267626 literals actually usable 84%
c [bca-12] added 949 blocked clauses in 733323 steps
c [sweep-12] limit 17517704 penalty 0 = 0 + 0
c [sweep-12-1] 26134 pos 35.7% + 46979 neg 64.3% = 73113 sched 54.6% ret 60699
c [sweep-12-1] 17524750 steps 971 queries 10114.75 avg class size
c [sweep-12-1] 10311 decisions 897 SAT calls 30.62 avg env size
c [sweep-12-1] 68422 variables remain 51% (65379 retained 49%)
c [decomp-44] removed 446 variables
c [sweep-12-1] removed 446 vars (0 failed, 203 eqs, 211 impls)
c [sweep-12] removed 446 vars in TOTAL (1 rounds, 970 queries)
c [phase-count-16] 879898 negative 94.3% of 933196 except 53298 5.7%
c [phase-count-16] 865570 positive 92.8% of 933196 except 67626 7.2%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 48 positive 31%, 109 negative 69%
c [sort-queue-16] sorted 88057 enqueued variables after 108259 conflicts
c [score-dist-16] active 45309 (34%), one 0 (0%), zero 88057 (66%)
c [score-dist-16] max exp 517, different 17 (3%)
c [score-dist-16] median active exp 505, avg 506.1
c [simplification-16] removed 8152 variables 5.8% (133366 remain 12%)
c [simplification-16] removed 68725 irredundant clauses 6.9% (933196 remain 21%)
c [simplification-16] maximum reduction of 7% = max (6%, 7%)
c [simplification-16] large reduction 7% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 120259 (soft 110259 + delta 10000)
c [simplification-16] new conflict limit 110259 (hard 120259)
c 
c [simplification-17] limit 110259 conflicts (hard 120259) hit after 110260 conflicts
c [quatres-13] found 168455 quaternary clauses 49% in total
c [quatres-13-1] removed 57 duplicate quaternary clauses
c [quatres-13-1] added 13 double-self-subsuming ternary resolvents
c [quatres-13-2] added 308 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1622 quaternary resolvents
c [ternres-13] limit 60595109 with penalty 0 = 0 + 0
c [ternres-13] 1 schedulable variables 0%
c [ternres-13] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-7] 20109 schedulable variables 15%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 2405 variables
c [simpleprobe-7] 11128 variables remain 8% (119833 retained 92%)
c [simpleprobe-7] removed 2405 variables, found 115474 hbrs, 157 units
c [unhide-17] limit 3029755 with penalty 2 = 0 + 2
c [unhide-17-17] 0 units, 1 failed, 6641 tauts, 0 hbrs, 14517 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 2703 transitive binary clauses
c [transred-13] found 4 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 130868 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 2009 variables 2% in round 1 in 265556982 steps
c [elim-14-1] backward subsumption/strengthening limit 265556900
c [elim-14-1-1] backward checking 16889 touched variables 13%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 180 and strengthened 178 clauses in 21888645 steps
c [elim-14-1] rescheduled 1158 variables 1% by backward subsumption
c [elim-14-2] eliminated 43 variables 0% in round 2 in 15760159 steps
c [elim-14-2] backward subsumption/strengthening limit 15760100
c [elim-14-2-1] backward checking 408 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 18 and strengthened 19 clauses in 778351 steps
c [elim-14-2] rescheduled 97 variables 0% by backward subsumption
c [elim-14-3] eliminated 8 variables 0% in round 3 in 746410 steps
c [elim-14-3] backward subsumption/strengthening limit 746400
c [elim-14-3-1] backward checking 54 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 4 and strengthened 7 clauses in 459326 steps
c [elim-14] incomplete 21 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 2074 = 2% variables out of 130868 scheduled
c [bca-13] limit of 10000000 steps and 1813983 added (scaled 2)
c [bca-13] 215045 out of 257590 literals actually usable 83%
c [bca-13] added 481 blocked clauses in 701544 steps
c [sweep-13] limit 18178532 penalty 0 = 0 + 0
c [sweep-13-1] 23741 pos 36.2% + 41874 neg 63.8% = 65615 sched 50.9% ret 63179
c [sweep-13-1] 18196338 steps 892 queries 7290.71 avg class size
c [sweep-13-1] 9978 decisions 861 SAT calls 31.30 avg env size
c [sweep-13-1] 60911 variables remain 47% (67848 retained 53%)
c [decomp-47] removed 247 variables
c [sweep-13-1] removed 247 vars (0 failed, 135 eqs, 120 impls)
c [sweep-13] removed 247 vars in TOTAL (1 rounds, 891 queries)
c [phase-count-17] 846509 negative 94.0% of 900763 except 54254 6.0%
c [phase-count-17] 834618 positive 92.7% of 900763 except 66145 7.3%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 26 positive 36%, 46 negative 64%
c [sort-queue-17] sorted 83756 enqueued variables after 110260 conflicts
c [score-dist-17] active 44791 (35%), one 0 (0%), zero 83756 (65%)
c [score-dist-17] max exp 517, different 17 (3%)
c [score-dist-17] median active exp 505, avg 506.0
c [simplification-17] removed 4819 variables 3.6% (128547 remain 12%)
c [simplification-17] removed 32433 irredundant clauses 3.5% (900763 remain 20%)
c [simplification-17] maximum reduction of 4% = max (4%, 3%)
c [simplification-17] geometric conflict interval increment 6221 = 31109 / 5
c [simplification-17] new conflict interval 37330
c [simplification-17] penalized conflict interval 37330 = 1 * 37330
c [simplification-17] hard conflict limit 166255 (soft 147590 + delta 18665)
c [simplification-17] new conflict limit 147590 (hard 166255)
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 -  691.8  128547   900763    129241   47925 109213 323786   51    65  144  79%    280    1   50   34  149%
c 
c [simplification-18] limit 147590 conflicts (hard 166255) hit after 155287 conflicts
c [quatres-14] found 163652 quaternary clauses 49% in total
c [quatres-14-1] removed 79 duplicate quaternary clauses
c [quatres-14-1] added 32 double-self-subsuming ternary resolvents
c [quatres-14-2] added 142 single-self-subsuming ternary resolvents
c [quatres-14-2] added 916 quaternary resolvents
c [decomp-48] removed 3 variables
c [treelook-7] limit 12856952 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 118711 literals 46%
c [treelook-7] scheduling used 2607053 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 12856952 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 13204761 steps
c [treelook-7] 118300 literals remain 46%
c [treelook-7] 17050 variables remain to probed next time 13%
c [decomp-49] removed 46 variables
c [treelook-7] removed 98 variables, found 43281 hbrs
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-18] 2 units, 18 failed, 65090 tauts, 0 hbrs, 62504 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 2104 transitive binary clauses
c [transred-14] found 1 units
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 128408 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 1086 variables 1% in round 1 in 254617852 steps
c [elim-15-1] backward subsumption/strengthening limit 254617800
c [elim-15-1-1] backward checking 13663 touched variables 11%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 360 and strengthened 628 clauses in 18446544 steps
c [elim-15-1] rescheduled 1487 variables 1% by backward subsumption
c [elim-15-2] eliminated 31 variables 0% in round 2 in 8574180 steps
c [elim-15-2] backward subsumption/strengthening limit 8574100
c [elim-15-2-1] backward checking 457 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 33 and strengthened 24 clauses in 1357957 steps
c [elim-15-2] rescheduled 114 variables 0% by backward subsumption
c [elim-15-3] eliminated 2 variables 0% in round 3 in 2089926 steps
c [elim-15-3] backward subsumption/strengthening limit 2089900
c [elim-15-3-1] backward checking 63 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 2 and strengthened 6 clauses in 597533 steps
c [elim-15] incomplete 15 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 1124 = 1% variables out of 128408 scheduled
c [elim-15] 1124 < 1/100 * 128408 = 1284 considered unsuccessful
c [bca-14] limit of 10000000 steps and 1791029 added (scaled 2)
c [bca-14] 210643 out of 254570 literals actually usable 83%
c [bca-14] added 723 blocked clauses in 689464 steps
c [sweep-14] limit 38570857 penalty 0 = 0 + 0
c [sweep-14-1] 21987 pos 36.4% + 38393 neg 63.6% = 60380 sched 47.4% ret 66904
c [sweep-14-1] 38577366 steps 2067 queries 4490.63 avg class size
c [sweep-14-1] 23466 decisions 1973 SAT calls 30.85 avg env size
c [sweep-14-1] 48857 variables remain 38% (78390 retained 62%)
c [decomp-50] removed 496 variables
c [sweep-14-1] removed 496 vars (0 failed, 350 eqs, 307 impls)
c [sweep-14] removed 496 vars in TOTAL (1 rounds, 2066 queries)
c [phase-count-18] 836495 negative 94.0% of 889734 except 53239 6.0%
c [phase-count-18] 824159 positive 92.6% of 889734 except 65575 7.4%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 11 positive 39%, 17 negative 61%
c [sort-queue-18] sorted 78603 enqueued variables after 155287 conflicts
c [score-dist-18] active 48185 (38%), one 0 (0%), zero 78603 (62%)
c [score-dist-18] max exp 518, different 18 (3%)
c [score-dist-18] median active exp 505, avg 506.4
c [simplification-18] removed 1759 variables 1.4% (126788 remain 12%)
c [simplification-18] removed 11029 irredundant clauses 1.2% (889734 remain 20%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 18665 = 37330 / 2
c [simplification-18] new conflict interval 55995
c [simplification-18] penalized conflict interval 55995 = 1 * 55995
c [simplification-18] hard conflict limit 239279 (soft 211282 + delta 27997)
c [simplification-18] new conflict limit 211282 (hard 239279)
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 -  965.8  126788   889734    169088   49575 105140 293078   51    56  143  90%    619   -6   53   41  130%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 16419 basic ate = 12299 trn 75% + 4120 lrg 25% in 4 updates
c bcas: 14 count, 17482 added (14346 skipped), 14349467 steps
c bkwd: tried 1263514 clauses, 2524627 lits, 2.00 lits/clause
c bkwd: checked 93691891 occs, 74.15 occs/clause, 37.11 occs/lit
c bkwd: subsumed 20 binary, 410 ternary, 1174 large
c bkwd: strengthened 9 binary, 1 ternary (100% self), 1857 large (0% self)
c blkd: 6 bces, 57450 removed, 41553369 resolutions, 109071102 steps
c blkd: 34454 blocking literals 2%, 1458 pure
c bump: 183296 bumped seen, 100023350 lits 545.7 on average
c card: 5 count, 0 units, 0 am1, 74688017 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 8826 subsumed
c card: 3555 at-most-one constraints found, average size 3.10
c card: 3555 at-most-one constraints used 100%, average size 3.10
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: 5 cces, 50309 eliminated, 46299 ate 92%, 4010 abce 8%
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: 15562771 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 132 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 50 decompositions, 119705 equivalent 11%
c deco: 1126 decision-only clauses 1%, 73% reduction
c decs: 1283735 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 621572 eliminated 55%, 10371 pure 2%
c elms: 28 rounds, 1.9 rounds/bve
c elms: 536817 small 86%, 72926 large 12%
c elms: 699325 tried small, 536817 succeeded 77%, 162508 failed 23%
c elms: 308358 subsumed, 405515 strengthened, 14675 blocked
c elms: 49221199 copies, 60765285 resolutions, 13719283 ipos
c elms: 39636888 subchks, 70703286 strchks
c gaus: 4 extractions, 18441 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10414794 steps, 5207397 extr 50%, 5232430 elim 50%
c glue: 37.4 orig avg, 37.4 real avg, 5.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1380881 = 534149 simple 39% + 833177 trn 60% + 13555 lrg 1%, 37863 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 183296 clauses, 89.6 length
c lrnd: 16418481 lits = 32878564 orig - 16460083 removed 50%
c lrnd: 47099 uips 26%, 89128 flips 49%
c mins: 176472 mins 96%, 1963 bin 1%, 3735 size 2%
c mins: 58072920 poisoned searches, 6145955 hits, 11% hit rate
c mins: 84063642 used twice searches, 4482466 hits, 5% hit rate
c move: moved 85905, 41260 bin 48%, 44645 trn 52%
c otfs: 1066 driving 34%, 2027 restarting 66%
c otfs: str 3093, 2586 red 84%, 507 irr 16%
c otfs: str 3093, 0 bin 0%, 798 trn 26%, 2295 lrg 74%
c otfs: sub 107, 96 red 90%, 11 irr 10%
c otfs: sub 107, 0 bin 0%, 29 trn 27%, 78 lrg 73%
c phas: 18 computed, 779544 set, 360907 pos (46%), 418637 neg (54%)
c prbs: 6 basic, 1081977 probed, 15934 failed, 2245 lifted
c prbs: 7 simple, 1297679 probed, 2580 failed, 16908 eqs
c prbs: 7 treelook, 1261 probed, 105 failed, 0 lifted
c prom: 3757 locked 0% out of 988437 tried
c prps: 2103812792 props, 1582 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 14 count, 35578 quat, 9360 self1, 396 self2, 3375 dup
c queu: 18 sorted, 1283735 next (66402 steps 0.05)
c queu: 105306711 enq (221470678 steps 2.10), 100023350 deq 95%
c redc: 2735 clauses 16%, 17641 tried 10%, 161 sat 1%
c redc: 5029 lits 4%, 123347 tried 0%, 162 sat 0%
c redc: 465 times jump level reduced, 34.9 levels on average
c reds: 3 count, 57832.7 conflicts per reduce
c reds: 0 memlim 0%, 3 arith 100%
c reds: 76506 collected 95%, 4087 retired 5%
c rmbd: 287794 removed, 200150 red 70%
c rsts: 8115 restarts 88%, 1103 skipped 12%
c rsts: 1103 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: 18 count, 17 confs 94%, 0 vars 0%
c simp: 0 its 0%, 1 bin 6%, 0 trns 0%
c subl: 183296 count (418106 tried 2.3), 23007 sub out of 175836 (13.1%)
c swps: 14 count, 14 rounds, 10577 queries (755.5/round)
c swps: 10060 sat calls, 1267 unsat (1.1% success rate)
c swps: 132347 decisions 13.2, 10864 conflicts 1.1
c swps; 13934.6 avg class size, 34.0 avg environment size
c swps: 0 failed, 1823 impls, 1733 equivs
c swp0: 3521 type 0 queries, 538 unsat (15.3%), 3363 sat (95.5%)
c swp1: 7056 type 1 queries, 4158 unsat (58.9%), 5481 sat (77.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 2934444 calls to obtain time
c tops: 263587 fixed 23%, 40 its, 4337.45 confs/it
c trds: 14 transitive reductions, 26905 removed, 96 failed
c trds: 326335 nodes, 562315 edges, 28015741 steps
c trim: 685646 words, 2.6 MB
c trnr: 13 count, 12717 bin, 426051 trn, 304854362 steps
c unhd: 18 count, 18 rounds, 184619026 steps
c unhd: 22586 non-trivial sccs of average size 2.5
c unhd: 3319 units, 3298 bin, 19 trn, 2 lrg
c unhd: 4693 failed, 4059 stamp, 0 lits, 35 bin, 525 trn, 2 lrg
c unhd: 424711 tauts, 8476 bin 2%, 67422 trn 16%, 13163 lrg 3%
c unhd: 424711 tauts, 335650 stamp 79%, 328291 red 77%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 687924 str, 3298 bin 0%, 57593 trn 8%, 627033 lrg 91%, 355830 red 52%
c vars: 126788 remaining 11% and 1004864 removed 89% out of 1131652
c vars: 263587 fixed 23%, 621572 eliminated 55%, 119705 equivalent 11%
c vsts: 16261852119 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 7.7 search visits per propagation, 90100.0 per conflict
c wchs: 1378432993 pushed, 166510674 enlarged, 200 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         211414         76506          4087      24428978       6600855         76726
c 
c  0 0         47228  22        41   0         0   0  18167285  74   3340814  51     17325  23     0.6
c  1 5          2326   1        65   0       202   5   1325309   5<   510529   8      4902   6     0.1
c  2 6          6566   3       727   1       349   9   2162868   9    968034  15<    12812  17     0.3
c  3 9         12342   6      3689   5       476  12   1275780   5    747743  11     11985  16<    1.5
c  4 14        14836   7      5936   8       498  12    682067   3    429260   7     11262  15     2.2
c  5 21        15135   7<     6441   8       474  12<   373125   2    276682   4      7144   9     1.6
c  6 30        22040  10     11973  16       473  12    200451   1    155238   2      5217   7     2.7
c  7 41        33510  16     18281  24<      599  15    116736   0     86735   1      3597   5     4.6
c  8 54        48700  23     25704  34       768  19    102558   0     73286   1      1827   2     7.1
c  9 69         6154   3      3291   4       177   4     16277   0      9488   0       458   1     1.1
c 10 86         2104   1       302   0        58   1      5480   0      2631   0       190   0     0.6
c 11 126         473   0        56   0        13   0      1042   0       415   0         7   0     0.1
c 
c avg                  4.9           6.6           5.4           0.7           1.5           2.9
c std                  3.2           1.6           2.3           1.4           2.0           2.3
c 
c   82.671   8% elim
c   73.382   7% probe
c   53.539   5% sweep
c   27.762   3% unhide
c   24.638   2% bump
c   15.046   2% cce
c   14.908   1% block
c   12.049   1% bca
c    9.462   1% quatres
c 
c   11.108 < 1% rest (below)
c 
c    4.441   0% gauss
c    3.391   0% ternres
c    1.808   0% transred
c    0.940   0% decide
c    0.528   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   13.252   1% preprocessing     4%
c  322.781  32% inprocessing     96%
c ==================================
c  336.033  34% simplifying
c  661.023  66% search
c ==================================
c  997.076 100% all
c 
c        173498 conflicts,         174.0 confs/sec
c          1454 ternaries,         119.3 confs/ternary
c           805 binaries,          215.5 confs/binary
c            40 iterations,       4337.4 confs/iteration
c 
c             3 reductions,          0.0 redus/sec,  57832.7 confs/reduction
c          8115 restarts,            8.1 rests/sec,     21.4 confs/restart
c       1283735 decisions,        1287.5 decis/sec,      7.4 decis/conflict
c    2103812792 propagations,  2109983.1 props/sec,   1638.8 props/decision
c 
c 997.1 seconds, 389.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
