c launch: /data/cnf/sc2014/app/14pipe_q0_k.cnf.bz2
c host: atom04
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/14pipe_q0_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/14pipe_q0_k.cnf.bz2
c no embedded options
c found 'p cnf 222845 7702617' header
c read 222845 variables, 7702617 clauses, 22897135 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=5
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 222844 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  222844  7702616         0       0      0     0    0     0  177   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1925654 based on 7702616 irredundant clauses
c [card-1] found 2 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1925654 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 16 variables
c [simpleprobe-1] all 222829 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 15401656 based on 7700828 irredundant clauses
c [simpleprobe-1] 222829 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 0 variables, found 886 hbrs, 0 units
c [unhide-1] limit 481301 based on 7700828 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 222829 variables 100%
c [elim-1] limit of 7700828 steps based on 7700828 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 217883 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4901 = 2% variables out of 222829 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 7689281 negative 100.0% of 7691007 except 1726 0.0%
c [phase-count-1] 987411 positive 12.8% of 7691007 except 6703596 87.2%
c [phase-count-1] less non-negative clauses 1726 than limit 769100 (10.0%)
c [phase-count-1] non-pos/non-neg = 6703596/1726 = 3883.89 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 217928 negative 100%
c [sort-queue-1] sorted 217928 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 217928 (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 4901 variables 2.2% (217928 remain 98%)
c [simplification-1] removed 11609 irredundant clauses 0.2% (7691007 remain 100%)
c [simplification-1] maximum reduction of 2% = max (2%, 0%)
c [simplification-1] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-1] new conflict interval 6666
c [simplification-1] penalized conflict interval 6666 = 1 * 6666
c [simplification-1] hard conflict limit 16666 (soft 6666 + delta 10000)
c [simplification-1] new conflict limit 6666 (hard 16666)
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   10.9  217927  7691007       757     720      9   905   13   316  240   4%      3  313   57    1 6409%
c i   11.1  217926  7691007       899     838     19   918   15   326  241   5%      3  323   64    1 6214%
c i   11.1  217925  7691007       910     844     20   918   15   326  241   5%      3  323   65    1 6202%
c i   11.1  217924  7691007       912     845     20   918   15   326  241   5%      3  323   64    1 6157%
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 826 variables
c [treelook-1] limit 1921617 based on 7686471 irredundant clauses
c [treelook-1] scheduled 127871 literals 29%
c [treelook-1] scheduling used 1921619 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1921617 based on 7686471 irredundant clauses
c [treelook-1] used 3152168 steps
c [treelook-1] 127860 literals remain 29%
c [treelook-1] 119703 variables remain to probed next time 55%
c [treelook-1] removed 0 variables, found 482 hbrs
c [basicprobe-1] limit 61491768 based on 7686471 irredundant clauses
c [basicprobe-1-0] 108581 probes remain 50% after last round
c [basicprobe-1-0] 104 units = 104 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 104 variables, found 42507 hbrs
c [elim-2] 216953 variables 100% will be scheduled this time
c [elim-2] scheduled 216953 variables 100%
c [elim-2] limit of 7654841 steps based on 7654841 irredundant clauses
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 213292 not tried 98% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 3661 = 2% variables out of 216953 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 174125 enqueued variables after 2203 conflicts
c [score-dist-2] active 39212 (18%), one 0 (0%), zero 174125 (82%)
c [score-dist-2] max exp 579, different 456 (79%)
c [score-dist-2] median active exp 319, avg 303.0
c [simplification-2] removed 4587 variables 2.1% (213337 remain 96%)
c [simplification-2] removed 43540 irredundant clauses 0.6% (7647467 remain 99%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] forced so keeping old conflict interval 6666
c [simplification-2] conflict limit remains at 6671 (hard 16666)
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   29.7  213336  7647467      5359    4281    404 42993   42   559  243   8%     52  526   58    5 1259%
c i   29.7  213335  7647467      5360    4281    404 42993   42   559  243   8%     52  526   58    5 1254%
c i   29.7  213334  7647467      5361    4281    404 42993   42   559  243   8%     52  526   58    5 1249%
c 
c [simplification-3] limit 6691 conflicts (hard 16666) hit after 6691 conflicts
c [card-2] limit 1911866 based on 7647467 irredundant clauses
c [card-2] found 2 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1911866 for elimination
c [card-2] 2 out of 2 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 886 variables
c [simpleprobe-2] all 212451 free variables schedulable
c [simpleprobe-2] limit 15287388 based on 7643694 irredundant clauses
c [simpleprobe-2] 210569 variables remain 99% (1882 retained 1%)
c [simpleprobe-2] removed 0 variables, found 1837 hbrs, 0 units
c [unhide-2] limit 477730 based on 7643694 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 9 tauts, 0 hbrs, 7875 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 212451 variables 100%
c [elim-3] limit of 9854791 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 210061 not tried 99% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2390 = 1% variables out of 212451 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 185245 enqueued variables after 6691 conflicts
c [score-dist-3] active 24816 (12%), one 25456 (12%), zero 159789 (76%)
c [score-dist-3] max exp 738, different 568 (77%)
c [score-dist-3] median active exp 403, avg 431.8
c [simplification-3] removed 3273 variables 1.5% (210061 remain 94%)
c [simplification-3] removed 8613 irredundant clauses 0.1% (7638854 remain 99%)
c [simplification-3] maximum reduction of 2% = max (2%, 0%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 13332
c [simplification-3] penalized conflict interval 13332 = 1 * 13332
c [simplification-3] hard conflict limit 30023 (soft 20023 + delta 10000)
c [simplification-3] new conflict limit 20023 (hard 30023)
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   41.5  210060  7638854      6954    5587    506 43741   46   615  244   8%     21  568   51    6  879%
c i   44.2  210059  7638854      8331    6755    564 43811   49   706  244   7%     13  647   55    7  805%
c i   44.2  210058  7638854      8332    6755    564 43811   49   706  244   7%     13  646   55    7  802%
c 
c [simplification-4] limit of 1478 ternary hit after 1478 ternaries
c [decomp-7] removed 427 variables
c [elim-4] 209592 variables 100% will be scheduled this time
c [elim-4] scheduled 209592 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 464241132 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 106782 not tried 51% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 89939 = 43% variables out of 209592 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 108720 enqueued variables after 17926 conflicts
c [score-dist-4] active 10975 (9%), one 21737 (18%), zero 86983 (73%)
c [score-dist-4] max exp 591, different 469 (79%)
c [score-dist-4] median active exp 457, avg 405.3
c [simplification-4] removed 90363 variables 43.0% (119695 remain 54%)
c [simplification-4] removed 185566 irredundant clauses 2.4% (7453288 remain 97%)
c [simplification-4] maximum reduction of 43% = max (43%, 2%)
c [simplification-4] forced so keeping old conflict interval 13332
c [simplification-4] conflict limit remains at 20033 (hard 30023)
c [simplification-4] new ternary interval 10000
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   76.2  119694  7453288     18946   13520   1457 17116   43   476  240   9%    137  342   35   12  284%
c 
c [simplification-5] limit 20033 conflicts (hard 30023) hit after 20033 conflicts
c [quatres-1] found 26603 quaternary clauses 9% in total
c [quatres-1-2] added 1286 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 29813152 based on 7453288 irredundant clauses
c [ternres-1] all 119694 free variables schedulable
c [ternres-1] 1580 ternary resolvents (0 bin, 1580 trn)
c [ternres-1] 27209 variables remain 23% (92485 retained 77%)
c [gauss-1] limit 3726644 based on 7453288 irredundant clauses
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 1863156 based on 7452625 irredundant clauses
c [treelook-2] scheduled 112587 literals 47%
c [treelook-2] scheduling used 1863187 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1863156 based on 7452625 irredundant clauses
c [treelook-2] used 7322463 steps
c [treelook-2] 112581 literals remain 47%
c [treelook-2] 100488 variables remain to probed next time 84%
c [treelook-2] removed 0 variables, found 138 hbrs
c [transred-1] limit 7452625 based on 7452625 irredundant clauses
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 119694 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 122211997 steps penalty 3 = 0 + 3
c [block-1] incomplete 3449 not tried 3%
c [block-1] transition to [ all 1 rem 1 ] state
c [block-1] eliminated 370522 blocked clauses
c [block-1] considered successful since not run to completion yet
c [cce-1] limit of 7082103 steps based on 7082103 irredundant clauses
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] allowing another 3541556 steps for small clauses
c [cce-1-1] scheduling 6746245 clauses = 6745583 binary + 662 ternary
c [cce-1-1] tried to eliminate 40 small clauses 0%
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 0 covered clauses in round 1
c [cce-1] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 119694 variables 100%
c [elim-5] limit of 24442399 steps penalty 3 = 0 + 3
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 117243 not tried 98% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2451 = 2% variables out of 119694 scheduled
c [bca-1] limit of 10000000 steps and 14159804 added (scaled 2)
c [bca-1] 210483 out of 234488 literals actually usable 90%
c [bca-1] added 2954 blocked clauses in 645381 steps
c [sweep-1] limit 14159304 based on 7079652 irredundant clauses
c [sweep-1-1] 1523 pos 1.3% + 115720 neg 98.7% = 117243 sched 100.0% ret 0
c [sweep-1-1] 14364515 steps 324 queries 3344.62 avg class size
c [sweep-1-1] 12599 decisions 313 SAT calls 343.71 avg env size
c [sweep-1-1] 52659 variables remain 45% (64560 retained 55%)
c [decomp-10] removed 42 variables
c [sweep-1-1] removed 42 vars (0 failed, 13 eqs, 43 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 42 vars in TOTAL (1 rounds, 323 queries)
c [sort-queue-5] sorted 103919 enqueued variables after 20033 conflicts
c [score-dist-5] active 13282 (11%), one 20296 (17%), zero 83623 (71%)
c [score-dist-5] max exp 650, different 540 (83%)
c [score-dist-5] median active exp 437, avg 407.8
c [simplification-5] removed 2493 variables 2.1% (117201 remain 53%)
c [simplification-5] removed 386897 irredundant clauses 5.2% (7066391 remain 92%)
c [simplification-5] maximum reduction of 5% = max (2%, 5%)
c [simplification-5] large reduction 5% >= 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 32033 (soft 22033 + delta 10000)
c [simplification-5] new conflict limit 22033 (hard 32033)
c 
c [simplification-6] limit 22033 conflicts (hard 32033) hit after 22033 conflicts
c [quatres-2] found 27221 quaternary clauses 9% in total
c [quatres-2-2] added 213 quaternary resolvents
c [ternres-2] limit 28265564 based on 7066391 irredundant clauses
c [ternres-2] 26658 schedulable variables 23%
c [ternres-2] 1052 ternary resolvents (0 bin, 1052 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 1766597 based on 7066391 irredundant clauses
c [card-3] found 1 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1766597 for elimination
c [card-3] 1 out of 1 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 56531128 based on 7066391 irredundant clauses
c [basicprobe-2-0] 95816 probes remain 82% after last round
c [basicprobe-2-0] 177 units = 177 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 477 variables, found 12817 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-3] limit 441649 based on 7066389 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 4147 tauts, 0 hbrs, 36700 literals
c [block-2] 3391 variables 3% will be scheduled this time
c [block-2] scheduled 3391 variables 3%
c [block-2] limit of 12815969 steps penalty 3 = 0 + 3
c [block-2] incomplete 1431 not tried 1%
c [block-2] transition to [ all 0 rem 1 ] state
c [block-2] eliminated 0 blocked clauses
c [block-2] considered successful since not run to completion yet
c [elim-6] 104443 variables 89% will be scheduled this time
c [elim-6] scheduled 104443 variables 89%
c [elim-6] limit of 25631939 steps penalty 3 = 0 + 3
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 102389 not tried 88% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 2054 = 2% variables out of 104443 scheduled
c [bca-2] limit of 10000000 steps and 13922113 added (scaled 2)
c [bca-2] 203752 out of 229340 literals actually usable 89%
c [bca-2] added 119 blocked clauses in 637448 steps
c [sweep-2] limit 13920136 based on 6960068 irredundant clauses
c [sweep-2-1] 620 pos 1.2% + 50680 neg 98.8% = 51300 sched 44.7% ret 63369
c [sweep-2-1] 14034568 steps 458 queries 2480.83 avg class size
c [sweep-2-1] 17222 decisions 440 SAT calls 295.17 avg env size
c [sweep-2-1] 26900 variables remain 24% (87145 retained 76%)
c [decomp-12] removed 923 variables
c [sweep-2-1] removed 923 vars (0 failed, 21 eqs, 50 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 923 vars in TOTAL (1 rounds, 457 queries)
c [sort-queue-6] sorted 101733 enqueued variables after 22033 conflicts
c [score-dist-6] active 12013 (11%), one 22208 (20%), zero 79525 (70%)
c [score-dist-6] max exp 697, different 560 (80%)
c [score-dist-6] median active exp 456, avg 405.5
c [simplification-6] removed 3455 variables 2.9% (113746 remain 51%)
c [simplification-6] removed 238863 irredundant clauses 3.4% (6827528 remain 89%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 18332
c [simplification-6] penalized conflict interval 18332 = 1 * 18332
c [simplification-6] hard conflict limit 50365 (soft 40365 + delta 10000)
c [simplification-6] new conflict limit 40365 (hard 50365)
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  143.1  113745  6827484     28359   21154   5886 56552   47   515  228   9%    110  331   44   17  262%
c 
c [simplification-7] limit 40365 conflicts (hard 50365) hit after 40365 conflicts
c [quatres-3] found 27693 quaternary clauses 12% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 929 quaternary resolvents
c [ternres-3] limit 27309424 based on 6827356 irredundant clauses
c [ternres-3] all 113745 free variables schedulable
c [ternres-3] 525 ternary resolvents (0 bin, 525 trn)
c [ternres-3] 25867 variables remain 23% (87878 retained 77%)
c [gauss-2] limit 3413678 based on 6827356 irredundant clauses
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 1 variables
c [transred-2] limit 6826730 based on 6826730 irredundant clauses
c [transred-2] removed 4 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 113744 variables 100%
c [block-3] limit of 18281089 steps penalty 3 = 0 + 3
c [block-3] incomplete 37472 not tried 33%
c [block-3] transition to [ all 1 rem 1 ] state
c [block-3] eliminated 2864 blocked clauses
c [block-3] considered successful since not run to completion yet
c [cce-2] limit of 6823862 steps based on 6823862 irredundant clauses
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 3412053 steps for small clauses
c [cce-2-1] scheduling 6557060 clauses = 6552359 binary + 4701 ternary
c [cce-2-1] tried to eliminate 15 small clauses 0%
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 0 covered clauses in round 1
c [cce-2] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 113658 variables 100%
c [elim-7] limit of 36562178 steps penalty 3 = 0 + 3
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 101371 not tried 89% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2737 = 2% variables out of 113658 scheduled
c [bca-3] limit of 10000000 steps and 13639508 added (scaled 2)
c [bca-3] 184421 out of 221844 literals actually usable 83%
c [bca-3] added 154 blocked clauses in 584070 steps
c [sweep-3] limit 13637472 based on 6818736 irredundant clauses
c [sweep-3-1] 819 pos 3.4% + 23314 neg 96.6% = 24133 sched 21.8% ret 86788
c [sweep-3-1] 13672442 steps 399 queries 2458.10 avg class size
c [sweep-3-1] 17726 decisions 391 SAT calls 344.62 avg env size
c [sweep-3-1] 16711 variables remain 15% (94202 retained 85%)
c [decomp-14] removed 42 variables
c [sweep-3-1] removed 42 vars (0 failed, 14 eqs, 31 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 42 vars in TOTAL (1 rounds, 398 queries)
c [sort-queue-7] sorted 96756 enqueued variables after 40365 conflicts
c [score-dist-7] active 14123 (13%), one 28436 (26%), zero 68320 (62%)
c [score-dist-7] max exp 822, different 628 (76%)
c [score-dist-7] median active exp 547, avg 503.2
c [simplification-7] removed 2866 variables 2.5% (110879 remain 50%)
c [simplification-7] removed 14487 irredundant clauses 0.2% (6812869 remain 88%)
c [simplification-7] maximum reduction of 3% = max (3%, 0%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 23332
c [simplification-7] penalized conflict interval 23332 = 1 * 23332
c [simplification-7] hard conflict limit 75363 (soft 63697 + delta 11666)
c [simplification-7] new conflict limit 63697 (hard 75363)
c 
c [simplification-8] limit 63697 conflicts (hard 75363) hit after 63697 conflicts
c [quatres-4] found 23769 quaternary clauses 10% in total
c [quatres-4-2] added 168 quaternary resolvents
c [ternres-4] limit 27251432 based on 6812858 irredundant clauses
c [ternres-4] 25141 schedulable variables 23%
c [ternres-4] 68 ternary resolvents (0 bin, 68 trn)
c [ternres-4] fully completed ternary resolution
c [unhide-4] limit 425803 based on 6812858 irredundant clauses
c [unhide-4-4] 6 units, 1 failed, 452 tauts, 0 hbrs, 65418 literals
c [transred-3] limit 6805924 based on 6805924 irredundant clauses
c [transred-3] removed 0 transitive binary clauses
c [block-4] 1406 variables 1% will be scheduled this time
c [block-4] scheduled 1406 variables 1%
c [block-4] limit of 23386292 steps penalty 3 = 0 + 3
c [block-4] incomplete 220 not tried 0%
c [block-4] transition to [ all 0 rem 1 ] state
c [block-4] eliminated 0 blocked clauses
c [block-4] considered successful since not run to completion yet
c [elim-8] 98837 variables 89% will be scheduled this time
c [elim-8] scheduled 98837 variables 89%
c [elim-8] boosting limit by 20
c [elim-8] limit of 935451697 steps penalty 3 = 0 + 3
c [elim-8] rescheduling of touched variables disabled
c [elim-8] incomplete 23703 not tried 21% in round 1
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 5337 = 5% variables out of 98837 scheduled
c [bca-4] limit of 10000000 steps and 13583507 added (scaled 2)
c [bca-4] 169925 out of 211072 literals actually usable 81%
c [bca-4] added 195 blocked clauses in 555456 steps
c [sweep-4] limit 13581394 based on 6790697 irredundant clauses
c [sweep-4-1] 763 pos 5.9% + 12067 neg 94.1% = 12830 sched 12.2% ret 92705
c [sweep-4-1] 13592003 steps 449 queries 1650.70 avg class size
c [sweep-4-1] 22763 decisions 429 SAT calls 261.78 avg env size
c [sweep-4-1] 8798 variables remain 8% (94861 retained 92%)
c [decomp-16] removed 2611 variables
c [sweep-4-1] removed 2611 vars (0 failed, 23 eqs, 44 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2611 vars in TOTAL (1 rounds, 448 queries)
c [sort-queue-8] sorted 97994 enqueued variables after 63697 conflicts
c [score-dist-8] active 4930 (5%), one 40053 (39%), zero 57941 (56%)
c [score-dist-8] max exp 575, different 339 (59%)
c [score-dist-8] median active exp 350, avg 360.3
c [simplification-8] removed 7955 variables 7.2% (102924 remain 46%)
c [simplification-8] removed 428456 irredundant clauses 6.3% (6384402 remain 83%)
c [simplification-8] maximum reduction of 7% = max (7%, 6%)
c [simplification-8] large reduction 7% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 75697 (soft 65697 + delta 10000)
c [simplification-8] new conflict limit 65697 (hard 75697)
c 
c [simplification-9] limit 65697 conflicts (hard 75697) hit after 65697 conflicts
c [quatres-5] found 19625 quaternary clauses 9% in total
c [quatres-5-2] added 1058 single-self-subsuming ternary resolvents
c [quatres-5-2] added 1050 quaternary resolvents
c [ternres-5] limit 25537592 based on 6384398 irredundant clauses
c [ternres-5] all 102924 free variables schedulable
c [ternres-5] 2712 ternary resolvents (0 bin, 2712 trn)
c [ternres-5] 49977 variables remain 49% (52947 retained 51%)
c [simpleprobe-3] 101995 schedulable variables 99%
c [simpleprobe-3] limit 12768796 based on 6384398 irredundant clauses
c [simpleprobe-3] 95402 variables remain 93% (7522 retained 7%)
c [simpleprobe-3] removed 0 variables, found 3309 hbrs, 0 units
c [unhide-5] limit 399024 based on 6384398 irredundant clauses
c [unhide-5-5] 0 units, 0 failed, 13654 tauts, 0 hbrs, 11508 literals
c [block-5] scheduling all variables this time
c [block-5] scheduled 102924 variables 100%
c [block-5] limit of 23750859 steps penalty 3 = 0 + 3
c [block-5] incomplete 25172 not tried 24%
c [block-5] transition to [ all 1 rem 1 ] state
c [block-5] eliminated 5530 blocked clauses
c [block-5] considered successful since not run to completion yet
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 102884 variables 100%
c [elim-9] limit of 47501718 steps penalty 3 = 0 + 3
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 89507 not tried 87% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1014 = 1% variables out of 102884 scheduled
c [elim-9] 1014 < 1/100 * 102884 = 1028 considered unsuccessful
c [bca-5] limit of 10000000 steps and 12724955 added (scaled 2)
c [bca-5] 162300 out of 203742 literals actually usable 80%
c [bca-5] added 116 blocked clauses in 548784 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12722744 based on 6361372 irredundant clauses
c [sweep-5-1] 432 pos 5.8% + 7012 neg 94.2% = 7444 sched 7.3% ret 94426
c [sweep-5-1] 12750845 steps 470 queries 975.81 avg class size
c [sweep-5-1] 29423 decisions 463 SAT calls 332.02 avg env size
c [sweep-5-1] 5031 variables remain 5% (96755 retained 95%)
c [decomp-19] removed 125 variables
c [sweep-5-1] removed 125 vars (0 failed, 8 eqs, 15 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 125 vars in TOTAL (1 rounds, 469 queries)
c [sort-queue-9] sorted 96138 enqueued variables after 65697 conflicts
c [score-dist-9] active 5607 (6%), one 39132 (38%), zero 57006 (56%)
c [score-dist-9] max exp 594, different 330 (55%)
c [score-dist-9] median active exp 504, avg 456.5
c [simplification-9] removed 1179 variables 1.1% (101745 remain 46%)
c [simplification-9] removed 43921 irredundant clauses 0.7% (6340481 remain 82%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 11666 = 23332 / 2
c [simplification-9] new conflict interval 34998
c [simplification-9] penalized conflict interval 34998 = 1 * 34998
c [simplification-9] hard conflict limit 118194 (soft 100695 + delta 17499)
c [simplification-9] new conflict limit 100695 (hard 118194)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  261.1  101745  6340441     74904   18704   9128 51959   55   615  212   9%    501  298   64   32  200%
c 
c [simplification-10] limit 100695 conflicts (hard 118194) hit after 118194 conflicts
c [quatres-6] found 17614 quaternary clauses 8% in total
c [quatres-6-2] added 17 single-self-subsuming ternary resolvents
c [quatres-6-2] added 600 quaternary resolvents
c [ternres-6] limit 25361584 based on 6340396 irredundant clauses
c [ternres-6] 49397 schedulable variables 49%
c [ternres-6] 1786 ternary resolvents (0 bin, 1786 trn)
c [ternres-6] 52 variables remain 0% (101693 retained 100%)
c [card-4] limit 1585099 based on 6340396 irredundant clauses
c [card-4] found 2 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1585099 for elimination
c [card-4] 2 out of 2 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 3170198 based on 6340396 irredundant clauses
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-4] limit 6340396 based on 6340396 irredundant clauses
c [transred-4] removed 0 transitive binary clauses
c [block-6] 213 variables 0% will be scheduled this time
c [block-6] scheduled 213 variables 0%
c [block-6] limit of 35778407 steps penalty 3 = 0 + 3
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [cce-3] limit of 6340396 steps based on 6340396 irredundant clauses
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 3172312 steps for small clauses
c [cce-3-1] scheduling 6119825 clauses = 6093248 binary + 26577 ternary
c [cce-3-1] tried to eliminate 4 small clauses 0%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 1 small clauses 0%
c [cce-3-1] eliminated 1 small clauses in 6345921 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1 covered clauses in round 1
c [cce-3] eliminated 1 covered clauses in TOTAL during 1 rounds
c [cce-3] 1 < 1/100 * 6340396 = 63403 considered unsuccessful
c [bca-6] limit of 10000000 steps and 12683059 added (scaled 2)
c [bca-6] 166206 out of 203492 literals actually usable 82%
c [bca-6] added 107 blocked clauses in 584465 steps
c [sweep-6] limit 12680790 based on 6340395 irredundant clauses
c [sweep-6-1] 313 pos 6.2% + 4695 neg 93.8% = 5008 sched 4.9% ret 96737
c [sweep-6-1] 12762385 steps 358 queries 883.38 avg class size
c [sweep-6-1] 23711 decisions 344 SAT calls 352.05 avg env size
c [sweep-6-1] 3855 variables remain 4% (97890 retained 96%)
c [decomp-21] removed 12 variables
c [sweep-6-1] removed 12 vars (0 failed, 13 eqs, 27 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 12 vars in TOTAL (1 rounds, 357 queries)
c [sort-queue-10] sorted 96994 enqueued variables after 118194 conflicts
c [score-dist-10] active 4739 (5%), one 43945 (43%), zero 53049 (52%)
c [score-dist-10] max exp 565, different 356 (63%)
c [score-dist-10] median active exp 371, avg 355.1
c [simplification-10] removed 12 variables 0.0% (101733 remain 46%)
c [simplification-10] removed 8 irredundant clauses 0.0% (6340389 remain 82%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 34998
c [simplification-10] new conflict interval 69996
c [simplification-10] penalized conflict interval 69996 = 1 * 69996
c [simplification-10] hard conflict limit 223188 (soft 188190 + delta 34998)
c [simplification-10] new conflict limit 188190 (hard 223188)
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 -  300.8  101733  6340389    121563   26114  11668 52221   46   340  214  13%    767   -9   54   46  118%
c i  307.4  101732  6340388    140436   40658  12439 52289   31   216  223  14%    832 -129   17   44   39%
c -  322.4  101732  6340388    161821   28781  12923 52464   91   422  215  22%   -398   49   84   49  169%
c 
c [simplification-11] limit 188190 conflicts (hard 223188) hit after 188195 conflicts
c [quatres-7] found 16006 quaternary clauses 8% in total
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 267 quaternary resolvents
c [ternres-7] limit 25361168 based on 6340292 irredundant clauses
c [ternres-7] 52 schedulable variables 0%
c [ternres-7] 107 ternary resolvents (0 bin, 107 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-22] removed 3 variables
c [unhide-6] limit 396013 based on 6336223 irredundant clauses
c [unhide-6-6] 0 units, 0 failed, 2528 tauts, 0 hbrs, 35647 literals
c [elim-10] 22061 variables 22% will be scheduled this time
c [elim-10] scheduled 22061 variables 22%
c [elim-10] limit of 47466360 steps penalty 4 = 1 + 3
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 19253 not tried 19% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 35 = 0% variables out of 22061 scheduled
c [elim-10] 35 < 1/100 * 22061 = 220 considered unsuccessful
c [bca-7] limit of 10000000 steps and 12662796 added (scaled 2)
c [bca-7] 158386 out of 203392 literals actually usable 78%
c [bca-7] added 1849 blocked clauses in 540956 steps
c [sweep-7] limit 12660474 based on 6330237 irredundant clauses
c [sweep-7-1] 343 pos 8.9% + 3512 neg 91.1% = 3855 sched 3.8% ret 97840
c [sweep-7-1] 12674276 steps 278 queries 684.96 avg class size
c [sweep-7-1] 17964 decisions 270 SAT calls 259.27 avg env size
c [sweep-7-1] 3034 variables remain 3% (98658 retained 97%)
c [decomp-23] removed 15 variables
c [sweep-7-1] removed 15 vars (0 failed, 8 eqs, 14 impls)
c [sweep-7] 15 < 1/1000 * 101695 = 101 considered unsuccessful
c [sweep-7] removed 15 vars in TOTAL (1 rounds, 277 queries)
c [sort-queue-11] sorted 94502 enqueued variables after 188195 conflicts
c [score-dist-11] active 7178 (7%), one 48684 (48%), zero 45818 (45%)
c [score-dist-11] max exp 519, different 360 (69%)
c [score-dist-11] median active exp 381, avg 347.7
c [simplification-11] removed 52 variables 0.1% (101680 remain 46%)
c [simplification-11] removed 10811 irredundant clauses 0.2% (6329481 remain 82%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 69996
c [simplification-11] new conflict interval 139992
c [simplification-11] penalized conflict interval 139992 = 1 * 139992
c [simplification-11] hard conflict limit 398183 (soft 328187 + delta 69996)
c [simplification-11] new conflict limit 328187 (hard 398183)
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 -  352.3  101680  6329470    206999   28119  12492 51845   51   298  214  17%    310 -134   51   51  100%
c -  363.1  101680  6329470    247435   31591  12662 51852   35   439  218   8%    639   23   33   46   71%
c -  372.6  101680  6329470    285732   31645  12757 51857   21   241  217   9%    809 -147   24   37   64%
c i  374.7  101679  6329470    295168   38925  12828 51862   18   144  222  13%    838 -220   15   35   43%
c i  374.7  101678  6329470    295169   38925  12828 51862   18   144  222  13%    836 -220   15   35   43%
c -  388.0  101678  6329338    325989   29884  13777 52250   33   248  217  13%   -627 -123   37   37   99%
c 
c [simplification-12] limit 328197 conflicts (hard 398183) hit after 358269 conflicts
c [quatres-8] found 16353 quaternary clauses 8% in total
c [quatres-8-2] added 218 single-self-subsuming ternary resolvents
c [quatres-8-2] added 205 quaternary resolvents
c [ternres-8] limit 25317096 based on 6329274 irredundant clauses
c [ternres-8] all 101678 free variables schedulable
c [ternres-8] 215 ternary resolvents (0 bin, 215 trn)
c [ternres-8] 55056 variables remain 54% (46622 retained 46%)
c [decomp-24] removed 2 variables
c [treelook-3] limit 1580399 based on 6321599 irredundant clauses
c [treelook-3] scheduled 98318 literals 48%
c [treelook-3] scheduling used 1580413 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1580399 based on 6321599 irredundant clauses
c [treelook-3] used 2820337 steps
c [treelook-3] 98315 literals remain 48%
c [treelook-3] 88624 variables remain to probed next time 87%
c [treelook-3] removed 0 variables, found 32 hbrs
c [block-7] scheduling all variables this time
c [block-7] scheduled 101678 variables 100%
c [block-7] limit of 33233140 steps penalty 4 = 1 + 3
c [block-7] incomplete 23576 not tried 23%
c [block-7] transition to [ all 1 rem 1 ] state
c [block-7] eliminated 19212 blocked clauses
c [block-7] 19212 < 1/100 * 6321599 = 63215 considered unsuccessful
c [bca-8] limit of 10000000 steps and 12608021 added (scaled 2)
c [bca-8] 160732 out of 202452 literals actually usable 79%
c [bca-8] added 1147 blocked clauses in 572348 steps
c [sort-queue-12] sorted 90704 enqueued variables after 358269 conflicts
c [score-dist-12] active 10521 (10%), one 51083 (50%), zero 39621 (39%)
c [score-dist-12] max exp 724, different 388 (54%)
c [score-dist-12] median active exp 632, avg 607.9
c [simplification-12] removed 453 variables 0.4% (101225 remain 45%)
c [simplification-12] removed 26887 irredundant clauses 0.4% (6302387 remain 82%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 139992
c [simplification-12] new conflict interval 279984
c [simplification-12] penalized conflict interval 279984 = 1 * 279984
c [simplification-12] hard conflict limit 778245 (soft 638253 + delta 139992)
c [simplification-12] new conflict limit 638253 (hard 778245)
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 -  440.2  101225  6302385    376546   28471  14226 54410   71   343  213  21%    261  -66   74   49  151%
c i  444.2  101224  6302385    388989   37605  14778 54430   27   278  219  10%    393 -120   10   46   22%
c i  444.2  101223  6302385    388990   37605  14778 54430   27   278  219  10%    391 -120   10   46   22%
c -  457.9  101221  6302383    431058   34097  15283 54578   21   125  217  17%    -92 -224   16   40   39%
c i  462.5  101220  6302383    445927   45019  15328 54605   14   116  223  12%    135 -196    6   35   18%
c i  462.5  101219  6302383    445928   45019  15328 54605   14   116  223  12%    134 -196    6   35   18%
c -  472.9  101217  6302319    476745   34425  15995 54997   38   253  217  15%    -96  -55   44   36  123%
c 
c [simplification-13] limit of 5176 binary hit after 5176 binaries
c [quatres-9] found 15842 quaternary clauses 8% in total
c [quatres-9-2] added 15 single-self-subsuming ternary resolvents
c [quatres-9-2] added 279 quaternary resolvents
c [ternres-9] limit 25209268 based on 6302317 irredundant clauses
c [ternres-9] 54871 schedulable variables 54%
c [ternres-9] 87 ternary resolvents (3 bin, 84 trn)
c [ternres-9] 1165 variables remain 1% (100052 retained 99%)
c [decomp-26] removed 45 variables
c [basicprobe-3] limit 50339584 based on 6292448 irredundant clauses
c [basicprobe-3-0] 82092 probes remain 81% after last round
c [basicprobe-3-0] 99 units = 99 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 99 variables, found 12017 hbrs
c [transred-5] limit 6292448 based on 6292448 irredundant clauses
c [transred-5] removed 5 transitive binary clauses
c [bca-9] limit of 10000000 steps and 12514568 added (scaled 2)
c [bca-9] 158693 out of 202164 literals actually usable 78%
c [bca-9] added 1168 blocked clauses in 572632 steps
c [sweep-8] limit 12510748 based on 6255374 irredundant clauses
c [sweep-8-1] 576 pos 19.6% + 2357 neg 80.4% = 2933 sched 2.9% ret 98148
c [sweep-8-1] 12522807 steps 245 queries 504.77 avg class size
c [sweep-8-1] 16193 decisions 241 SAT calls 348.69 avg env size
c [sweep-8-1] 2230 variables remain 2% (98851 retained 98%)
c [decomp-27] removed 3 variables
c [sweep-8-1] removed 3 vars (0 failed, 3 eqs, 5 impls)
c [sweep-8] 3 < 1/1000 * 101081 = 101 considered unsuccessful
c [sweep-8] removed 3 vars in TOTAL (1 rounds, 244 queries)
c [sort-queue-13] sorted 88861 enqueued variables after 520568 conflicts
c [score-dist-13] active 12217 (12%), one 54751 (54%), zero 34110 (34%)
c [score-dist-13] max exp 917, different 659 (72%)
c [score-dist-13] median active exp 782, avg 637.9
c [simplification-13] removed 139 variables 0.1% (101078 remain 45%)
c [simplification-13] removed 46945 irredundant clauses 0.7% (6255372 remain 81%)
c [simplification-13] maximum reduction of 1% = max (0%, 1%)
c [simplification-13] forced so keeping old conflict interval 279984
c [simplification-13] conflict limit remains at 638273 (hard 778245)
c [simplification-13] new binary interval 10000
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 -  502.3  101078  6255372    532703   31944  13710 67466   44   419  212  10%    547  115   50   37  136%
c -  530.7  101078  6255366    580395   35445  14780 67601   31   340  214   9%    794    1   27   41   65%
c i  536.0  101077  6255366    598029   48895  14858 67618   16    96  221  17%    848 -211    9   37   24%
c -  549.4  101076  6255366    625243   36479  15313 67786   34   170  214  20%   -686 -144   28   38   74%
c 
c [simplification-14] limit 638273 conflicts (hard 778245) hit after 658852 conflicts
c [quatres-10] found 16126 quaternary clauses 8% in total
c [quatres-10-2] added 18 single-self-subsuming ternary resolvents
c [quatres-10-2] added 286 quaternary resolvents
c [ternres-10] limit 25021432 based on 6255358 irredundant clauses
c [ternres-10] 1164 schedulable variables 1%
c [ternres-10] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 3127679 based on 6255358 irredundant clauses
c [gauss-4] extracted 1 xors of average arity 2.0
c [gauss-4] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-4] limit 3125376 based on 6250753 irredundant clauses
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 32 variables
c [unhide-7] limit 390668 based on 6250689 irredundant clauses
c [unhide-7-7] 0 units, 0 failed, 19442 tauts, 0 hbrs, 10020 literals
c [cce-4] boosting limit by 10
c [cce-4] limit of 66756945 steps penalty 6 = 3 + 3
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 439
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 438
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 437
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 436
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 435
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 434
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 433
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 431
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 430
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 429
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 428
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 427
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 426
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 424
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 422
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 421
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 420
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 410
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 409
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 408
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 407
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 406
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 405
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 404
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 403
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 402
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 401
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 400
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 399
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 398
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 397
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 64 large clauses in 66757723 steps
c [cce-4-1] allowing another 33378861 steps for small clauses
c [cce-4-1] scheduling 6029176 clauses = 6005158 binary + 24018 ternary
c [cce-4-1] tried to eliminate 50 small clauses 0%
c [cce-4-1] eliminated 24 binary clauses 0%
c [cce-4-1] eliminated 24 small clauses 0%
c [cce-4-1] eliminated 24 small clauses in 66757812 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 88 covered clauses in round 1
c [cce-4] eliminated 88 covered clauses in TOTAL during 1 rounds
c [cce-4] 88 < 1/100 * 6230389 = 62303 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 101044 variables 100%
c [elim-11] limit of 25000000 steps penalty 5 = 2 + 3
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 89776 not tried 89% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 877 = 1% variables out of 101044 scheduled
c [elim-11] 877 < 1/100 * 101044 = 1010 considered unsuccessful
c [bca-10] limit of 10000000 steps and 12461888 added (scaled 2)
c [bca-10] 154826 out of 200336 literals actually usable 77%
c [bca-10] added 4315 blocked clauses in 580430 steps
c [sort-queue-14] sorted 90660 enqueued variables after 658852 conflicts
c [score-dist-14] active 9507 (9%), one 60555 (60%), zero 30105 (30%)
c [score-dist-14] max exp 954, different 551 (58%)
c [score-dist-14] median active exp 880, avg 759.2
c [simplification-14] removed 909 variables 0.9% (100167 remain 45%)
c [simplification-14] removed 26616 irredundant clauses 0.4% (6228742 remain 81%)
c [simplification-14] maximum reduction of 1% = max (1%, 0%)
c [simplification-14] geometric conflict interval increment 139992 = 279984 / 2
c [simplification-14] new conflict interval 419976
c [simplification-14] penalized conflict interval 419976 = 1 * 419976
c [simplification-14] hard conflict limit 1288816 (soft 1078828 + delta 209988)
c [simplification-14] new conflict limit 1078828 (hard 1288816)
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  579.8  100166  6228742    672441   64228  14727 71407   25   141  228  18%    192 -135   10   35   27%
c -  584.4  100166  6228728    683378   35656  14829 71508   29   247  212  12%   -680  -25   29   35   83%
c i  592.8  100165  6228710    709094   57025  14945 71634   20    74  223  27%   -127 -162   11   32   35%
c i  593.8  100163  6228710    712270   59740  14956 71641   15    60  223  26%   -601 -169    9   31   28%
c i  594.6  100162  6228710    714771   61823  14984 71648   12    41  225  31%   -607 -182    7   30   24%
c -  608.7  100152  6228660    732575   38280  15643 71730   47   266  212  18%   -254   17   33   35   94%
c i  616.5  100151  6228660    756428   55819  15854 71762   12    87  219  14%    136 -136    8   30   28%
c -  631.8  100149  6228602    783287   39864  16656 72265   37   272  213  14%     -4   -2   37   33  113%
c -  654.5  100149  6228529    832784   40852  17799 72983   37   302  213  12%    541   -2   50   35  142%
c i  657.9  100148  6228529    836549   43954  17921 72997   44   338  219  13%    568   32   44   36  124%
c i  657.9  100147  6228529    836550   43954  17921 72997   44   338  219  13%    567   32   44   36  123%
c i  667.2  100144  6228529    862726   62087  18314 73043   13    69  222  19%   -135 -195    7   32   22%
c i  669.5  100143  6228524    866767   65262  18482 73148   26   248  222  11%   -448  -13   38   32  117%
c -  680.9  100143  6228524    889050   43479  18990 73298   27   144  214  19%    -75 -128   18   33   56%
c i  684.5  100142  6228524    900862   51541  19036 73310   12    80  219  15%    106 -164    7   30   24%
c i  685.1  100140  6228524    901657   52178  19067 73349   16   184  219   9%   -169  -59   35   30  119%
c 
c [simplification-15] limit of 30 iterations hit after 31 iterations
c [quatres-11] found 12170 quaternary clauses 7% in total
c [quatres-11-2] added 265 single-self-subsuming ternary resolvents
c [quatres-11-2] added 564 quaternary resolvents
c [ternres-11] limit 24914096 based on 6228524 irredundant clauses
c [ternres-11] all 100140 free variables schedulable
c [ternres-11] 64 ternary resolvents (1 bin, 63 trn)
c [ternres-11] 40744 variables remain 41% (59396 retained 59%)
c [card-5] limit 1557131 based on 6228524 irredundant clauses
c [card-5] found 3 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1557131 for elimination
c [card-5] 3 out of 3 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-29] removed 108 variables
c [transred-6] limit 6153056 based on 6153056 irredundant clauses
c [transred-6] removed 3 transitive binary clauses
c [block-8] 23358 variables 23% will be scheduled this time
c [block-8] scheduled 23358 variables 23%
c [block-8] limit of 25000000 steps penalty 5 = 2 + 3
c [block-8] incomplete 16610 not tried 17%
c [block-8] transition to [ all 0 rem 1 ] state
c [block-8] eliminated 47721 blocked clauses
c [block-8] 47721 < 1/100 * 6153054 = 61530 considered unsuccessful
c [bca-11] limit of 10000000 steps and 12217228 added (scaled 2)
c [bca-11] 150032 out of 198630 literals actually usable 76%
c [bca-11] added 3523 blocked clauses in 550839 steps
c [sort-queue-15] sorted 94716 enqueued variables after 924643 conflicts
c [score-dist-15] active 4598 (5%), one 70201 (71%), zero 24515 (25%)
c [score-dist-15] max exp 539, different 343 (64%)
c [score-dist-15] median active exp 476, avg 433.0
c [simplification-15] removed 826 variables 0.8% (99314 remain 45%)
c [simplification-15] removed 123191 irredundant clauses 2.0% (6105333 remain 79%)
c [simplification-15] maximum reduction of 2% = max (1%, 2%)
c [simplification-15] forced so keeping old conflict interval 419976
c [simplification-15] conflict limit remains at 1078838 (hard 1288816)
c [simplification-15] new iteration interval 100
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  711.2   99313  6105300    938028   50400  11057 73979   38   349  217  11%    189   69   37   33  113%
c -  722.6   99313  6105300    972128   37028  11428 74225   26   159  207  16%    185 -103   26   31   86%
c i  726.6   99312  6105300    985410   47966  11476 74274   13    63  211  21%    339 -167    8   28   28%
c i  726.6   99308  6105300    985439   47987  11478 74274   13    63  211  21%    318 -166    8   28   28%
c i  734.0   99307  6105300    998854   58675  11861 74393   20   185  216  11%   -147  -44    9   28   34%
c i  737.4   99304  6105300   1004345   63020  12085 74590   32   381  217   8%   -248  148   41   28  144%
c -  750.5   99304  6105285   1026674   40372  12541 74873   37   292  207  13%     57   24   45   31  147%
c i  759.4   99303  6105285   1042097   52857  12996 75080   41   392  215  10%    260  116   41   32  127%
c i  765.7   99299  6105285   1060901   67868  13139 75105   13    61  221  22%      0 -199    7   30   22%
c 
c [simplification-16] limit 1078838 conflicts (hard 1288816) hit after 1080171 conflicts
c [quatres-12] found 11427 quaternary clauses 7% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 12 single-self-subsuming ternary resolvents
c [quatres-12-2] added 940 quaternary resolvents
c [ternres-12] limit 24421116 based on 6105279 irredundant clauses
c [ternres-12] 40405 schedulable variables 41%
c [ternres-12] 328 ternary resolvents (1 bin, 327 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-30] removed 30 variables
c [transred-7] limit 6087224 based on 6087224 irredundant clauses
c [transred-7] removed 0 transitive binary clauses
c [bca-12] limit of 10000000 steps and 12182771 added (scaled 2)
c [bca-12] 147985 out of 198570 literals actually usable 75%
c [bca-12] added 44813 blocked clauses in 594498 steps
c [sweep-9] limit 12174448 based on 6087224 irredundant clauses
c [sweep-9-1] 600 pos 32.2% + 1262 neg 67.8% = 1862 sched 1.9% ret 97422
c [sweep-9-1] 12175133 steps 285 queries 262.41 avg class size
c [sweep-9-1] 17929 decisions 272 SAT calls 337.14 avg env size
c [sweep-9-1] 1264 variables remain 1% (97925 retained 99%)
c [decomp-31] removed 107 variables
c [sweep-9-1] removed 107 vars (3 failed, 11 eqs, 20 impls)
c [sweep-9] removed 107 vars in TOTAL (1 rounds, 284 queries)
c [sort-queue-16] sorted 91177 enqueued variables after 1080171 conflicts
c [score-dist-16] active 8000 (8%), one 69446 (70%), zero 21731 (22%)
c [score-dist-16] max exp 826, different 445 (54%)
c [score-dist-16] median active exp 701, avg 665.9
c [simplification-16] removed 122 variables 0.1% (99177 remain 45%)
c [simplification-16] removed 23132 irredundant clauses 0.4% (6082147 remain 79%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 419976
c [simplification-16] new conflict interval 839952
c [simplification-16] penalized conflict interval 839952 = 1 * 839952
c [simplification-16] hard conflict limit 2340099 (soft 1920123 + delta 419976)
c [simplification-16] new conflict limit 1920123 (hard 2340099)
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  780.7   99176  6082147   1083016   48479   8334 119428   23   176  218  13%     81  -77    7   29   24%
c i  780.7   95900  6082147   1083061   48515   8334 119430   23   175  218  13%     66  -78    9   29   32%
c i  780.7   95899  6082147   1083063   48516   8334 119430   23   175  218  13%     66  -78   10   29   34%
c i  780.9   95898  6082130   1083600   48787   8335 119493   26   205  218  13%    -61  -48   44   29  150%
c i  780.9   95897  6082130   1083601   48787   8335 119493   26   205  218  13%    -61  -48   44   29  149%
c i  780.9   95896  6082130   1083602   48787   8335 119493   26   205  218  13%    -61  -48   43   29  148%
c i  780.9   95895  6082130   1083603   48787   8335 119493   26   205  218  13%    -61  -48   43   29  148%
c i  781.0   95894  6082130   1083719   48867   8335 119508   26   208  218  12%    -81  -45   37   29  127%
c i  781.0   95893  6082130   1083723   48866   8335 119508   26   208  218  12%    -82  -45   37   29  126%
c i  781.0   95892  6082130   1083724   48866   8335 119508   26   208  218  12%    -82  -45   37   29  126%
c i  781.1   95891  6082130   1083817   48921   8336 119514   26   208  218  12%    -96  -46   33   29  114%
c i  781.2   95890  6082130   1084314   49303   8337 119520   26   199  218  13%   -152  -54   27   29   93%
c i  781.2   95889  6082130   1084428   49399   8338 119520   27   200  218  14%   -162  -52   39   29  133%
c i  781.2   95888  6082130   1084439   49403   8338 119520   27   200  218  14%   -163  -53   38   29  129%
c i  781.2   95887  6082130   1084440   49403   8338 119520   27   200  218  14%   -163  -53   38   29  129%
c i  781.2   95886  6082130   1084448   49405   8338 119521   27   199  218  14%   -164  -53   37   29  126%
c i  781.3   95885  6082130   1084494   49428   8338 119522   27   199  218  14%   -167  -54   35   29  120%
c i  781.3   95884  6082130   1084495   49428   8338 119522   27   199  218  14%   -167  -54   35   29  120%
c i  781.3   95883  6082130   1084496   49428   8338 119522   27   199  218  14%   -167  -54   35   29  119%
c i  781.3   95882  6082130   1084511   49438   8338 119523   27   198  218  14%   -168  -54   34   29  114%
c i  781.4   95881  6082126   1084707   49511   8338 119567   28   209  218  14%   -181  -44   46   29  156%
c i  781.4   95880  6082126   1084708   49511   8338 119567   28   209  218  14%   -181  -44   46   29  155%
c i  781.4   95879  6082122   1084763   49532   8338 119570   28   207  218  14%   -185  -46   44   29  149%
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  781.4   95878  6082122   1084764   49532   8338 119570   28   207  218  14%   -185  -46   43   29  148%
c i  781.4   95877  6082122   1084790   49540   8338 119572   28   206  218  14%   -186  -47   41   29  140%
c i  781.4   95876  6082122   1084853   49583   8339 119575   28   205  218  14%   -190  -47   39   29  134%
c i  781.4   95875  6082122   1084855   49584   8339 119575   28   205  218  14%   -190  -47   39   29  134%
c i  781.4   95874  6082122   1084856   49584   8339 119575   28   205  218  14%   -190  -48   39   29  133%
c i  781.4   95873  6082122   1084857   49584   8339 119575   28   205  218  14%   -190  -48   39   29  133%
c i  781.5   95872  6082122   1084875   49594   8339 119575   28   205  218  14%   -191  -48   38   29  128%
c i  781.5   95871  6082122   1084991   49667   8339 119576   28   205  218  14%   -196  -48   34   29  117%
c i  781.5   95870  6082122   1084998   49671   8339 119576   28   205  218  14%   -197  -48   34   29  116%
c i  781.5   95869  6082122   1085002   49673   8339 119576   28   204  218  14%   -197  -48   34   29  115%
c i  781.5   95868  6082122   1085003   49673   8339 119576   28   204  218  14%   -197  -48   34   29  115%
c i  781.5   95867  6082122   1085004   49673   8339 119576   28   204  218  14%   -197  -48   34   29  114%
c i  782.1   95866  6082122   1085965   50350   8342 119617   30   234  219  13%   -218  -18   40   29  137%
c i  782.1   95865  6082122   1086084   50429   8343 119638   30   234  219  13%   -221  -18   36   29  122%
c i  782.1   95864  6082122   1086085   50429   8343 119638   30   234  219  13%   -221  -18   36   29  122%
c i  782.1   95863  6082122   1086091   50428   8343 119641   30   234  219  13%   -221  -18   35   29  119%
c i  782.2   95862  6082122   1086248   50551   8343 119645   30   228  219  13%   -223  -24   30   29  100%
c i  782.3   95860  6082122   1086406   50687   8344 119650   30   228  219  13%   -225  -24   30   29  101%
c i  782.4   95859  6082122   1086635   50846   8345 119657   31   238  219  13%   -227  -14   39   30  131%
c i  782.9   95858  6082122   1087660   51566   8354 119713   32   242  219  13%   -226  -10   36   30  122%
c i  783.0   95857  6082122   1087865   51687   8354 119742   32   238  219  14%   -227  -14   41   30  137%
c i  783.2   95856  6082122   1088171   51911   8359 119745   32   241  219  13%   -228  -10   31   30  104%
c i  783.2   95855  6082122   1088173   51912   8359 119745   32   241  219  13%   -228  -11   31   30  104%
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  783.2   95854  6082122   1088224   51931   8361 119746   32   239  219  13%   -228  -13   28   30   94%
c i  783.2   95853  6082122   1088225   51931   8361 119746   32   239  219  13%   -228  -13   28   30   93%
c i  783.2   95852  6082122   1088226   51931   8361 119746   32   239  219  13%   -228  -13   28   30   93%
c i  783.3   95851  6082122   1088409   52054   8364 119749   32   250  219  13%   -228   -1   34   30  113%
c i  783.3   95850  6082122   1088514   52127   8364 119755   32   252  219  13%   -228    0   32   30  108%
c i  783.4   95849  6082122   1088734   52285   8364 119757   32   265  219  12%   -228   13   35   30  118%
c i  783.7   95848  6082122   1089258   52636   8367 119770   33   267  219  12%   -227   16   37   30  124%
c i  783.8   95847  6082122   1089577   52867   8368 119779   33   266  219  12%   -226   15   34   30  115%
c i  784.4   95846  6082122   1090965   53929   8378 119836   33   270  219  12%   -215   18   34   30  115%
c i  784.8   95845  6082118   1091704   54477   8378 119870   33   271  219  12%   -215   19   38   30  127%
c i  785.0   95844  6082118   1092096   54776   8379 119881   34   274  219  12%   -215   22   40   30  135%
c i  785.1   95843  6082117   1092137   54805   8380 119881   33   273  219  12%   -215   20   36   30  121%
c i  785.2   95842  6082117   1092432   55003   8381 119898   34   269  219  13%   -215   17   41   30  137%
c i  785.2   95841  6082117   1092500   55040   8383 119899   34   268  219  13%   -215   16   37   30  124%
c i  785.7   95840  6082117   1093333   55706   8387 119920   34   266  219  13%   -211   13   32   30  105%
c i  785.7   95839  6082117   1093357   55727   8387 119920   34   265  219  13%   -211   12   30   30  101%
c i  785.8   95838  6082117   1093590   55903   8388 119929   33   259  219  13%   -212    6   30   30  100%
c i  785.8   95837  6082117   1093764   56037   8388 119940   33   256  219  13%   -212    4   36   30  119%
c i  785.9   95836  6082117   1093805   56070   8389 119940   33   256  219  13%   -212    3   33   30  111%
c i  786.2   95835  6082117   1094687   56783   8392 119953   32   226  219  14%   -207  -26   24   30   80%
c i  786.6   95834  6082115   1095776   57628   8395 119993   32   229  219  14%   -201  -23   30   30  101%
c i  786.6   95833  6082115   1095784   57635   8395 119993   32   229  219  14%   -201  -23   30   30   99%
c i  786.7   95832  6082115   1095992   57800   8396 120004   32   229  219  14%   -202  -23   36   30  120%
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  786.7   95831  6082115   1095996   57802   8396 120004   32   229  219  14%   -202  -23   36   30  119%
c i  786.7   95830  6082115   1096146   57922   8397 120005   32   230  219  14%   -202  -22   34   30  115%
c i  786.7   95829  6082115   1096147   57922   8397 120005   32   230  219  14%   -202  -22   34   30  115%
c i  786.8   95828  6082115   1096356   58083   8397 120009   31   222  219  14%   -203  -30   25   30   82%
c i  787.1   95827  6082115   1097143   58680   8401 120026   31   237  219  13%   -200  -14   27   30   90%
c i  787.6   95826  6082115   1098735   60009   8408 120045   28   246  219  12%   -187   -6   22   30   74%
c i  787.6   95825  6082115   1098736   60009   8408 120045   28   246  219  12%   -188   -6   22   30   73%
c i  787.7   95824  6082115   1098746   60018   8408 120045   28   245  219  11%   -188   -6   21   30   71%
c i  788.1   95823  6082115   1100023   60976   8414 120103   29   290  219  10%   -185   39   31   30  106%
c i  788.1   95822  6082115   1100047   60989   8417 120103   29   289  219  10%   -185   37   29   30   99%
c i  788.3   95821  6082115   1100876   61560   8418 120119   28   322  219   9%   -185   70   29   30   96%
c i  788.5   95820  6082115   1101494   61999   8419 120136   27   292  219   9%   -186   40   20   30   67%
c i  791.1   95819  6082109   1108632   67891   8452 120299   23   250  219   9%    -82   -5   20   29   70%
c i  792.4   95818  6082103   1113794   71914   8462 120402   16   151  219  11%   -102 -101    8   28   30%
c i  792.6   95817  6082103   1114216   72279   8464 120405   16   150  219  11%   -123 -102   12   28   42%
c i  792.8   95815  6082103   1114803   72759   8467 120411   15   140  219  11%   -139 -111    9   28   34%
c i  793.0   95814  6082101   1115416   73224   8475 120417   14   126  219  11%   -147 -124    7   27   24%
c i  793.0   94610  6082101   1115432   73236   8477 120417   14   126  219  11%   -147 -124    7   27   24%
c i  793.5   94609  6082101   1117238   74616   8498 120441   13   110  219  12%   -143 -137    9   27   34%
c i  794.0   94608  6082101   1118913   76070   8502 120446   12   114  219  11%   -140 -129    9   27   34%
c i  794.0   94606  6082101   1119052   76150   8508 120452   12   111  219  11%   -142 -132    8   27   28%
c i  794.0   92883  6082101   1119057   76151   8509 120453   12   111  219  11%   -142 -132    7   27   28%
c i  794.1   92882  6082101   1119149   76228   8510 120455   12   109  219  11%   -143 -134    7   27   25%
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  794.1   92880  6082101   1119292   76318   8513 120457   12   106  219  11%   -144 -137    6   27   22%
c i  794.1   92166  6082101   1119299   76312   8516 120458   12   105  219  11%   -144 -137    6   27   22%
c 0  794.1   91172  6082101   1119299   76312   8516 120458   12   105  219  11%   -144 -137    6   27   22%
c 
s UNSATISFIABLE
c
c bate: 2 basic ate = 0 trn 0% + 2 lrg 100% in 1 updates
c bcas: 12 count, 60460 added (13149 skipped), 6967307 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 8 bces, 445849 removed, 86624816 resolutions, 267759965 steps
c blkd: 11449 blocking literals 3%, 1324 pure
c bump: 1056030 bumped seen, 149511821 lits 141.6 on average
c card: 5 count, 0 units, 0 am1, 65784658 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 96 subsumed
c card: 10 at-most-one constraints found, average size 3.10
c card: 10 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: 4 cces, 89 eliminated, 88 ate 99%, 1 abce 1%
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: 30599752 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 84 gcs, 0 rescored clauses, 555 rescored vars
c dcps: 31 decompositions, 3463 equivalent 2%
c deco: 7345 decision-only clauses 1%, 56% reduction
c decs: 32258289 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 11 elims, 116720 eliminated 52%, 10 pure 0%
c elms: 11 rounds, 1.0 rounds/bve
c elms: 82083 small 70%, 33303 large 29%
c elms: 82223 tried small, 82083 succeeded 100%, 140 failed 0%
c elms: 985 subsumed, 311045 strengthened, 0 blocked
c elms: 6858042 copies, 19348084 resolutions, 1678994 ipos
c elms: 35733458 subchks, 7557524 strchks
c gaus: 4 extractions, 1 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 27607398 steps, 13803699 extr 50%, 3 elim 0%
c glue: 37.7 orig avg, 37.7 real avg, 5.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 81684 = 6032 simple 7% + 75487 trn 92% + 165 lrg 0%, 1481 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1056030 clauses, 67.6 length
c lrnd: 71377287 lits = 103335114 orig - 31957827 removed 31%
c lrnd: 378100 uips 36%, 512332 flips 49%
c mins: 1026493 mins 97%, 9788 bin 1%, 11234 size 1%
c mins: 176963241 poisoned searches, 12142566 hits, 7% hit rate
c mins: 262754668 used twice searches, 26328262 hits, 10% hit rate
c move: moved 436982, 435560 bin 100%, 1422 trn 0%
c otfs: 64141 driving 15%, 363988 restarting 85%
c otfs: str 428129, 390464 red 91%, 37665 irr 9%
c otfs: str 428129, 0 bin 0%, 2293 trn 1%, 425836 lrg 99%
c otfs: sub 2975, 2000 red 67%, 975 irr 33%
c otfs: sub 2975, 0 bin 0%, 13 trn 0%, 2962 lrg 100%
c phas: 1 computed, 217928 set, 0 pos (0%), 217928 neg (100%)
c prbs: 3 basic, 25725 probed, 380 failed, 0 lifted
c prbs: 3 simple, 297748 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 20 probed, 0 failed, 0 lifted
c prom: 113104 locked 2% out of 6376822 tried
c prps: 3488090224 props, 106 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 12 count, 6787 quat, 1605 self1, 0 self2, 8 dup
c queu: 16 sorted, 32258289 next (9384608 steps 0.29)
c queu: 156004513 enq (156615204 steps 1.00), 149511821 deq 96%
c redc: 8777 clauses 12%, 72378 tried 6%, 163 sat 0%
c redc: 40965 lits 6%, 675110 tried 1%, 163 sat 0%
c redc: 2466 times jump level reduced, 39.5 levels on average
c reds: 20 count, 55964.9 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595075 collected 84%, 110636 retired 16%
c rmbd: 13047 removed, 220 red 2%
c rsts: 19841 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 16 count, 12 confs 75%, 0 vars 0%
c simp: 1 its 6%, 2 bin 12%, 1 trns 6%
c subl: 1056030 count (1763612 tried 1.7), 133298 sub out of 1020344 (13.1%)
c swps: 9 count, 9 rounds, 3257 queries (361.9/round)
c swps: 3163 sat calls, 28 unsat (0.3% success rate)
c swps: 175530 decisions 55.5, 872 conflicts 0.3
c swps; 1567.6 avg class size, 317.8 avg environment size
c swps: 3 failed, 249 impls, 114 equivs
c swp0: 1082 type 0 queries, 65 unsat (6.0%), 1057 sat (97.7%)
c swp1: 2175 type 1 queries, 340 unsat (15.6%), 2086 sat (95.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 66630160 calls to obtain time
c tops: 11490 fixed 5%, 132 its, 8479.54 confs/it
c trds: 7 transitive reductions, 12 removed, 0 failed
c trds: 710 nodes, 27665 edges, 45966591 steps
c trim: 2161978 words, 8.2 MB
c trnr: 12 count, 5 bin, 8525 trn, 250089234 steps
c unhd: 7 count, 7 rounds, 66687511 steps
c unhd: 204 non-trivial sccs of average size 2.1
c unhd: 6 units, 6 bin, 0 trn, 0 lrg
c unhd: 2 failed, 1 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 40232 tauts, 88 bin 0%, 336 trn 1%, 4143 lrg 10%
c unhd: 40232 tauts, 35665 stamp 89%, 3174 red 8%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 167168 str, 6 bin 0%, 1537 trn 1%, 165625 lrg 99%, 94228 red 56%
c vars: 91172 remaining 41% and 131673 removed 59% out of 222845
c vars: 11490 fixed 5%, 116720 eliminated 52%, 3463 equivalent 2%
c vsts: 13752597017 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 3.9 search visits per propagation, 12103.2 per conflict
c wchs: 1552006516 pushed, 116027346 enlarged, 131 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1027131        595075        110636      37098077      15133144        886262
c 
c  0 0         40433   4      3746   1         0   0  16309848  44   4297485  28     55138   6     1.0
c  1 5         18505   2      6278   1      2097   2   1568270   4   1010613   7     27334   3     0.3
c  2 6         62705   6     25423   4      7503   7   3860616  10<  1940321  13     85556  10     1.2
c  3 9        107964  11     49104   8     12486  11   4667344  13   1885630  12<   125823  14     2.1
c  4 14       143613  14     82765  14     13514  12   4534481  12   1725938  11    129249  15     2.3
c  5 21       146697  14     96055  16     13590  12   2420301   7   1397503   9    122750  14<    4.7
c  6 30       143862  14<    96727  16<    12177  11<  1460740   4   1146439   8    131012  15     5.1
c  7 41       108342  11     71535  12     10799  10   1004514   3    814023   5     93917  11     4.9
c  8 54        83354   8     55127   9      9994   9    629218   2    499456   3     65554   7     2.7
c  9 69        69265   7     46838   8      9434   9    350893   1    241358   2     27822   3     3.2
c 10 86        81862   8     51889   9     14255  13    234001   1    148094   1     17625   2     6.1
c 11 126       19157   2      9013   2      4417   4     54729   0     24715   0      4199   0     3.5
c 12 230        1372   0       575   0       370   0      3122   0      1569   0       283   0     0.4
c 
c avg                  5.6           6.0           6.2           2.2           3.0           4.7
c std                  2.7           2.4           2.7           2.4           2.6           2.4
c 
c   62.340   8% block
c   59.059   7% elim
c   29.414   4% probe
c   21.073   3% decide
c   19.817   2% sweep
c   15.632   2% unhide
c   13.608   2% bump
c   12.796   2% bca
c    6.016   1% quatres
c    5.031   1% cce
c 
c    8.319 < 1% rest (below)
c 
c    4.842   1% gauss
c    1.480   0% rescore
c    0.937   0% ternres
c    0.782   0% transred
c    0.277   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    9.335   1% preprocessing     4%
c  243.010  31% inprocessing     96%
c ==================================
c  252.345  32% simplifying
c  541.758  68% search
c ==================================
c  794.103 100% all
c 
c       1119299 conflicts,        1409.5 confs/sec
c         24594 ternaries,          45.5 confs/ternary
c         10528 binaries,          106.3 confs/binary
c           132 iterations,       8479.5 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  55964.9 confs/reduction
c         19841 restarts,           25.0 rests/sec,     56.4 confs/restart
c      32258289 decisions,       40622.3 decis/sec,     28.8 decis/conflict
c    3488090224 propagations,  4392492.7 props/sec,    108.1 props/decision
c 
c 794.1 seconds, 465.6 MB
c launch: done
