c launch: /data/cnf/sc2014/app/11pipe_q0_k.cnf.bz2
c host: atom03
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/11pipe_q0_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/11pipe_q0_k.cnf.bz2
c no embedded options
c found 'p cnf 104244 3007883' header
c read 104244 variables, 3007883 clauses, 8917203 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=0
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 104243 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] STATIC (--score=0)
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  104243  3007882         0       0      0     0    0     0   85   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 751970 based on 3007882 irredundant clauses
c [card-1] found 1 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 751970 for elimination
c [card-1] 1 out of 1 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 13 variables
c [simpleprobe-1] all 104231 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 6014020 based on 3007010 irredundant clauses
c [simpleprobe-1] 104231 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 0 variables, found 809 hbrs, 0 units
c [unhide-1] limit 187938 based on 3007010 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 104231 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 100236 not tried 96% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 3993 = 4% variables out of 104231 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 2998023 negative 100.0% of 2998988 except 965 0.0%
c [phase-count-1] 457171 positive 15.2% of 2998988 except 2541817 84.8%
c [phase-count-1] less non-negative clauses 965 than limit 299800 (10.0%)
c [phase-count-1] non-pos/non-neg = 2541817/965 = 2634.01 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 100238 negative 100%
c [sort-queue-1] sorted 100238 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 100238 (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 3993 variables 3.8% (100238 remain 96%)
c [simplification-1] removed 8894 irredundant clauses 0.3% (2998988 remain 100%)
c [simplification-1] maximum reduction of 4% = max (4%, 0%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] hard conflict limit 14000 (soft 4000 + delta 10000)
c [simplification-1] new conflict limit 4000 (hard 14000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.0  100237  2998988        53      45      7   809    0    25   98   1%      0   25    4    0 23842%
c i    4.4  100236  2998988       194     172     16   811    1   149   98   1%      0  149   15    0 18589%
c i    6.2  100235  2998988       851     689     76   838    6   686   98   1%      3  682   30    0 7794%
c i    6.2  100234  2998988       852     689     76   838    6   686   98   1%      3  681   30    0 7763%
c i    6.2  100233  2998988       853     689     76   838    6   685   98   1%      3  681   29    0 7733%
c i    7.0  100232  2998988      1173     942    109   852    8   844   98   1%      3  837   35    1 6290%
c i    7.3  100231  2998988      1264     989    134   866    8   954   98   1%      3  945   30    1 5134%
c i    7.5  100230  2998988      1374    1086    142   868    9  1078   98   1%      2 1067   33    1 5129%
c i   11.2  100229  2998988      2985    2463    282   907   17  1960   99   1%     13 1912   29    1 1985%
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 1528 variables
c [treelook-1] limit 747890 based on 2991561 irredundant clauses
c [treelook-1] scheduled 61673 literals 31%
c [treelook-1] scheduling used 749677 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 747890 based on 2991561 irredundant clauses
c [treelook-1] used 2093672 steps
c [treelook-1] 61640 literals remain 31%
c [treelook-1] 57951 variables remain to probed next time 59%
c [treelook-1] removed 0 variables, found 66 hbrs
c [basicprobe-1] limit 23932488 based on 2991561 irredundant clauses
c [basicprobe-1-0] 54761 probes remain 56% after last round
c [basicprobe-1-0] 87 units = 87 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 87 variables, found 19151 hbrs
c [elim-2] 98621 variables 100% will be scheduled this time
c [elim-2] scheduled 98621 variables 100%
c [elim-2] limit of 18746785 steps penalty 1 = 0 + 1
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 87130 not tried 88% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 11491 = 12% variables out of 98621 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 87132 enqueued variables after 3163 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 87132 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 13097 variables 13.1% (87132 remain 84%)
c [simplification-2] removed 46585 irredundant clauses 1.6% (2952403 remain 98%)
c [simplification-2] maximum reduction of 13% = max (13%, 2%)
c [simplification-2] forced so keeping old conflict interval 4000
c [simplification-2] conflict limit remains at 4020 (hard 14000)
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   17.1   87131  2952403      3361    2642    259 16834   18  2272   97   1%     10 2212   30    2 1858%
c i   18.3   87130  2952403      3936    3155    306 16837   20  2511   97   1%      7 2432   32    2 1657%
c i   18.3   87129  2952403      3937    3154    306 16838   20  2511   97   1%      7 2431   31    2 1651%
c i   18.3   87128  2952403      3938    3154    306 16838   20  2510   97   1%      7 2430   31    2 1644%
c i   18.3   87127  2952403      3939    3153    306 16839   20  2510   97   1%      7 2430   31    2 1638%
c 
c [simplification-3] limit 4050 conflicts (hard 14000) hit after 4050 conflicts
c [card-2] limit 738100 based on 2952403 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 738100 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 510 variables
c [simpleprobe-2] all 86622 free variables schedulable
c [simpleprobe-2] limit 5898078 based on 2949039 irredundant clauses
c [simpleprobe-2] 73564 variables remain 85% (13058 retained 15%)
c [simpleprobe-2] removed 0 variables, found 2867 hbrs, 0 units
c [unhide-2] limit 184314 based on 2949039 irredundant clauses
c [unhide-2-2] 1 units, 0 failed, 25 tauts, 0 hbrs, 13725 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 86621 variables 100%
c [elim-3] limit of 23562326 steps penalty 1 = 0 + 1
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 71684 not tried 83% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 14937 = 17% variables out of 86621 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 71684 enqueued variables after 4050 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 71684 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 15443 variables 17.7% (71684 remain 69%)
c [simplification-3] removed 33510 irredundant clauses 1.1% (2918893 remain 97%)
c [simplification-3] maximum reduction of 18% = max (18%, 1%)
c [simplification-3] large reduction 18% >= 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 16050 (soft 6050 + delta 10000)
c [simplification-3] new conflict limit 6050 (hard 16050)
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   24.4   71683  2918893      4197    3153    212 15723   20  2598   95   1%      6 2508   21    2 1066%
c i   25.4   71682  2918893      4683    3533    257 15750   20  2767   96   1%      5 2660   22    2 1064%
c i   27.4   71681  2918893      5577    4373    286 15756   23  3182   96   1%      7 3036   33    3 1281%
c 
c [simplification-4] limit 6050 conflicts (hard 16050) hit after 6051 conflicts
c [decomp-7] removed 125 variables
c [unhide-3] limit 182328 based on 2917250 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 3568 tauts, 0 hbrs, 11376 literals
c [elim-4] 71559 variables 100% will be scheduled this time
c [elim-4] scheduled 71559 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 647485210 steps penalty 1 = 0 + 1
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 3186 not tried 4% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 14934 = 21% variables out of 71559 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 56625 enqueued variables after 6051 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 56625 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 15056 variables 21.0% (56625 remain 54%)
c [simplification-4] removed 37954 irredundant clauses 1.3% (2880939 remain 96%)
c [simplification-4] maximum reduction of 21% = max (21%, 1%)
c [simplification-4] large reduction 21% >= 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 18051 (soft 8051 + delta 10000)
c [simplification-4] new conflict limit 8051 (hard 18051)
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   48.0   56624  2880939      7501    4831    266 10433   24  3449  101   1%     17 3211   21    3  637%
c i   48.0   56623  2880939      7502    4831    266 10433   24  3448  101   1%     17 3210   21    3  634%
c 
c [simplification-5] limit 8061 conflicts (hard 18051) hit after 8062 conflicts
c [quatres-1] found 19061 quaternary clauses 11% in total
c [quatres-1-2] added 327 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 11523752 based on 2880938 irredundant clauses
c [ternres-1] all 56623 free variables schedulable
c [ternres-1] 3841 ternary resolvents (0 bin, 3841 trn)
c [ternres-1] 744 variables remain 1% (55879 retained 99%)
c [gauss-1] limit 1440469 based on 2880938 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 720086 based on 2880346 irredundant clauses
c [treelook-2] scheduled 53684 literals 47%
c [treelook-2] scheduling used 720101 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 720086 based on 2880346 irredundant clauses
c [treelook-2] used 1404594 steps
c [treelook-2] 53682 literals remain 47%
c [treelook-2] 48634 variables remain to probed next time 86%
c [treelook-2] removed 0 variables, found 8 hbrs
c [transred-1] limit 2880346 based on 2880346 irredundant clauses
c [transred-1] removed 1 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 56623 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 250000000 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 125390 blocked clauses
c [cce-1] limit of 15000000 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 304
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 302
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 301
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 6 large clauses in 15001225 steps
c [cce-1-1] allowing another 7500612 steps for small clauses
c [cce-1-1] scheduling 2553398 clauses = 2551554 binary + 1844 ternary
c [cce-1-1] tried to eliminate 75 small clauses 0%
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 6 covered clauses in round 1
c [cce-1] eliminated 6 covered clauses in TOTAL during 1 rounds
c [cce-1] 6 < 1/100 * 2754955 = 27549 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 56623 variables 100%
c [elim-5] limit of 40333481 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 36073 not tried 64% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2325 = 4% variables out of 56623 scheduled
c [bca-1] limit of 10000000 steps and 5505628 added (scaled 2)
c [bca-1] 89451 out of 108598 literals actually usable 82%
c [bca-1] added 1704 blocked clauses in 280659 steps
c [sweep-1] limit 5505128 based on 2752564 irredundant clauses
c [sweep-1-1] 682 pos 1.3% + 53616 neg 98.7% = 54298 sched 100.0% ret 0
c [sweep-1-1] 5762543 steps 233 queries 1783.75 avg class size
c [sweep-1-1] 7747 decisions 226 SAT calls 284.35 avg env size
c [sweep-1-1] 17018 variables remain 31% (37280 retained 69%)
c [decomp-10] removed 7 variables
c [sweep-1-1] removed 7 vars (0 failed, 7 eqs, 21 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 7 vars in TOTAL (1 rounds, 232 queries)
c [sort-queue-5] sorted 54291 enqueued variables after 8062 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 54291 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 2332 variables 4.1% (54291 remain 52%)
c [simplification-5] removed 128376 irredundant clauses 4.5% (2752562 remain 92%)
c [simplification-5] maximum reduction of 4% = max (4%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 8000
c [simplification-5] penalized conflict interval 8000 = 1 * 8000
c [simplification-5] hard conflict limit 26062 (soft 16062 + delta 10000)
c [simplification-5] new conflict limit 16062 (hard 26062)
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   80.3   54290  2752560     14885   11908   6078 17756   31  4195  104   1%     94 3587   30    6  488%
c 
c [simplification-6] limit 16062 conflicts (hard 26062) hit after 16066 conflicts
c [quatres-2] found 18796 quaternary clauses 11% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 331 quaternary resolvents
c [ternres-2] limit 11010240 based on 2752560 irredundant clauses
c [ternres-2] 725 schedulable variables 1%
c [ternres-2] 5851 ternary resolvents (1 bin, 5850 trn)
c [ternres-2] 128 variables remain 0% (54162 retained 100%)
c [card-3] limit 688140 based on 2752560 irredundant clauses
c [card-3] found 3 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 688140 for elimination
c [card-3] 3 out of 3 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 1 variables
c [basicprobe-2] limit 22017696 based on 2752212 irredundant clauses
c [basicprobe-2-0] 44522 probes remain 82% after last round
c [basicprobe-2-0] 101 units = 101 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 214 variables, found 5605 hbrs
c [bate-1] eliminated 42 asymmetric tautologies during probing
c [unhide-4] limit 172010 based on 2752170 irredundant clauses
c [unhide-4-4] 0 units, 2 failed, 720 tauts, 0 hbrs, 66379 literals
c [transred-2] limit 2721304 based on 2721304 irredundant clauses
c [transred-2] removed 1 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 54075 variables 100%
c [block-2] limit of 36851460 steps penalty 1 = 0 + 1
c [block-2] incomplete 261 not tried 0%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 28994 blocked clauses
c [elim-6] 3133 variables 6% will be scheduled this time
c [elim-6] scheduled 3133 variables 6%
c [elim-6] limit of 73702920 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 2 variables 0% in round 1 in 28455269 steps
c [elim-6-1] backward subsumption/strengthening limit 28455200
c [elim-6-1-1] backward checking 2013 touched variables 4%
c [elim-6-1-1] incomplete backward checking 3791 remain 188%
c [elim-6-1] subsumed 0 and strengthened 2605 clauses in 28463553 steps
c [elim-6-1] rescheduled 1810 variables 3% by backward subsumption
c [elim-6] incomplete 99 not tried 0% in round 2
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 2 = 0% variables out of 3133 scheduled
c [elim-6] 2 < 1/100 * 3133 = 31 considered unsuccessful
c [bca-2] limit of 10000000 steps and 5383630 added (scaled 2)
c [bca-2] 73517 out of 107412 literals actually usable 68%
c [bca-2] added 348 blocked clauses in 223902 steps
c [sweep-2] limit 5382278 based on 2691139 irredundant clauses
c [sweep-2-1] 510 pos 3.0% + 16324 neg 97.0% = 16834 sched 31.3% ret 36871
c [sweep-2-1] 5393581 steps 174 queries 1192.22 avg class size
c [sweep-2-1] 6966 decisions 163 SAT calls 243.88 avg env size
c [sweep-2-1] 10306 variables remain 19% (43396 retained 81%)
c [decomp-12] removed 15 variables
c [sweep-2-1] removed 15 vars (0 failed, 12 eqs, 24 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 15 vars in TOTAL (1 rounds, 173 queries)
c [sort-queue-6] sorted 53690 enqueued variables after 16066 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 53690 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 600 variables 1.1% (53690 remain 52%)
c [simplification-6] removed 62374 irredundant clauses 2.3% (2690186 remain 89%)
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 14666
c [simplification-6] penalized conflict interval 14666 = 1 * 14666
c [simplification-6] hard conflict limit 40732 (soft 30732 + delta 10000)
c [simplification-6] new conflict limit 30732 (hard 40732)
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  111.5   53689  2690172     23622   20357  12056 30353   34  4475  105   1%    107 3431   44    9  467%
c i  111.7   53688  2690172     23690   20417  12058 30356   33  4434  105   1%     99 3386   40    9  421%
c i  112.1   53505  2690172     23900   20602  12068 30362   33  4431  105   1%     79 3372   33    9  351%
c i  117.5   53201  2690154     27282   23739  12114 30392   32  3905  107   1%     26 2700   29   11  276%
c 
c [simplification-7] limit 30732 conflicts (hard 40732) hit after 30741 conflicts
c [quatres-3] found 15723 quaternary clauses 12% in total
c [quatres-3-2] added 470 quaternary resolvents
c [ternres-3] limit 10760612 based on 2690153 irredundant clauses
c [ternres-3] 127 schedulable variables 0%
c [ternres-3] 6951 ternary resolvents (0 bin, 6951 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1345076 based on 2690153 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 29 variables
c [unhide-5] limit 337635 with penalty 3 = 0 + 3
c [unhide-5-5] 0 units, 0 failed, 19665 tauts, 0 hbrs, 11858 literals
c [transred-3] limit 2599520 based on 2599520 irredundant clauses
c [transred-3] removed 2 transitive binary clauses
c [block-3] 253 variables 0% will be scheduled this time
c [block-3] scheduled 253 variables 0%
c [block-3] limit of 67527119 steps penalty 1 = 0 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-2] limit of 16881779 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 4 clauses out of 6 (67%) of length 301
c [cce-2-1] eliminated 6 clauses out of 8 (75%) of length 300
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 297
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 296
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 295
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 294
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 20 large clauses in 16882005 steps
c [cce-2-1] allowing another 8441002 steps for small clauses
c [cce-2-1] scheduling 2423244 clauses = 2421336 binary + 1908 ternary
c [cce-2-1] tried to eliminate 41 small clauses 0%
c [cce-2-1] eliminated 5 binary clauses 0%
c [cce-2-1] eliminated 5 small clauses 0%
c [cce-2-1] eliminated 5 small clauses in 16881811 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 25 covered clauses in round 1
c [cce-2] eliminated 25 covered clauses in TOTAL during 1 rounds
c [cce-2] 25 < 1/100 * 2599518 = 25995 considered unsuccessful
c [bca-3] limit of 10000000 steps and 5200512 added (scaled 2)
c [bca-3] 58872 out of 106346 literals actually usable 55%
c [bca-3] added 324 blocked clauses in 175175 steps
c [sweep-3] limit 5198986 based on 2599493 irredundant clauses
c [sweep-3-1] 587 pos 5.8% + 9592 neg 94.2% = 10179 sched 19.1% ret 42993
c [sweep-3-1] 5259026 steps 170 queries 907.10 avg class size
c [sweep-3-1] 7793 decisions 165 SAT calls 255.47 avg env size
c [sweep-3-1] 7202 variables remain 14% (45498 retained 86%)
c [decomp-14] removed 633 variables
c [sweep-3-1] removed 633 vars (0 failed, 7 eqs, 15 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 633 vars in TOTAL (1 rounds, 169 queries)
c [sort-queue-7] sorted 52539 enqueued variables after 30741 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 52539 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 662 variables 1.2% (52539 remain 50%)
c [simplification-7] removed 158972 irredundant clauses 5.9% (2531181 remain 84%)
c [simplification-7] maximum reduction of 6% = max (1%, 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 42741 (soft 32741 + delta 10000)
c [simplification-7] new conflict limit 32741 (hard 42741)
c 
c [simplification-8] limit 32741 conflicts (hard 42741) hit after 32741 conflicts
c [quatres-4] found 16213 quaternary clauses 11% in total
c [quatres-4-2] added 445 single-self-subsuming ternary resolvents
c [quatres-4-2] added 302 quaternary resolvents
c [ternres-4] limit 10124720 based on 2531180 irredundant clauses
c [ternres-4] all 52539 free variables schedulable
c [ternres-4] 406 ternary resolvents (0 bin, 406 trn)
c [ternres-4] 21465 variables remain 41% (31074 retained 59%)
c [transred-4] limit 2531180 based on 2531180 irredundant clauses
c [transred-4] removed 0 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 52539 variables 100%
c [elim-7] limit of 71825647 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 26490 not tried 50% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 838 = 2% variables out of 52539 scheduled
c [bca-4] limit of 10000000 steps and 5057988 added (scaled 2)
c [bca-4] 56099 out of 103404 literals actually usable 54%
c [bca-4] added 10 blocked clauses in 179088 steps
c [sweep-4] limit 5056300 based on 2528150 irredundant clauses
c [sweep-4-1] 369 pos 5.8% + 6035 neg 94.2% = 6404 sched 12.4% ret 45297
c [sweep-4-1] 5090812 steps 168 queries 623.10 avg class size
c [sweep-4-1] 8814 decisions 163 SAT calls 337.82 avg env size
c [sweep-4-1] 4838 variables remain 9% (46859 retained 91%)
c [decomp-16] removed 12 variables
c [sweep-4-1] removed 12 vars (0 failed, 8 eqs, 20 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 12 vars in TOTAL (1 rounds, 167 queries)
c [sort-queue-8] sorted 51689 enqueued variables after 32741 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 51689 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 850 variables 1.6% (51689 remain 50%)
c [simplification-8] removed 4219 irredundant clauses 0.2% (2526962 remain 84%)
c [simplification-8] maximum reduction of 2% = max (2%, 0%)
c [simplification-8] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-8] new conflict interval 21332
c [simplification-8] penalized conflict interval 21332 = 1 * 21332
c [simplification-8] hard conflict limit 64739 (soft 54073 + delta 10666)
c [simplification-8] new conflict limit 54073 (hard 64739)
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  142.8   51688  2526956     34358   29421  15045 24139   36  4104  109   1%     76 2618   41   13  312%
c i  145.0   51687  2526956     35593   30526  15087 24165   36  4126  109   1%     17 2594   35   14  261%
c i  153.5   51609  2526941     40652   35315  15136 24207   36  4037  109   1%     43 2325   33   15  217%
c i  153.5   51505  2526941     40653   35315  15136 24207   36  4036  109   1%     43 2324   33   15  216%
c i  172.2   51468  2526887     52112   45872  15416 24346   37  3935  114   1%    133 1839   41   19  219%
c 
c [simplification-9] limit 54083 conflicts (hard 64739) hit after 54083 conflicts
c [quatres-5] found 13967 quaternary clauses 11% in total
c [quatres-5-2] added 14 single-self-subsuming ternary resolvents
c [quatres-5-2] added 335 quaternary resolvents
c [ternres-5] limit 11318664 with penalty 1 = 0 + 1
c [ternres-5] 21002 schedulable variables 41%
c [ternres-5] 287 ternary resolvents (0 bin, 287 trn)
c [ternres-5] 2937 variables remain 6% (48513 retained 94%)
c [decomp-17] removed 297 variables
c [simpleprobe-3] 43765 schedulable variables 85%
c [simpleprobe-3] limit 11318664 penalty 3 = 2 + 1
c [decomp-18] removed 3 variables
c [simpleprobe-3] 37023 variables remain 72% (14366 retained 28%)
c [simpleprobe-3] removed 3 variables, found 3688 hbrs, 1 units
c [unhide-6] limit 282966 with penalty 4 = 1 + 3
c [unhide-6-6] 0 units, 0 failed, 1539 tauts, 0 hbrs, 36893 literals
c [block-4] scheduling all variables this time
c [block-4] scheduled 51389 variables 100%
c [block-4] limit of 56593322 steps penalty 2 = 1 + 1
c [block-4] incomplete 7549 not tried 15%
c [block-4] transition to [ all 1 rem 1 ] state
c [block-4] eliminated 165490 blocked clauses
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 48229 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4527465820 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 680 variables 1% in round 1 in 349457490 steps
c [elim-8-1] backward subsumption/strengthening limit 349457400
c [elim-8-1-1] backward checking 3636 touched variables 8%
c [elim-8-1-1] incomplete backward checking 5410 remain 149%
c [elim-8-1] subsumed 10 and strengthened 8194 clauses in 349459428 steps
c [elim-8-1] rescheduled 3186 variables 7% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 26347594 steps
c [elim-8-2] backward subsumption/strengthening limit 26347500
c [elim-8-2-1] backward checking 5449 touched variables 11%
c [elim-8-2-1] incomplete backward checking 5578 remain 102%
c [elim-8-2] subsumed 0 and strengthened 2273 clauses in 26349782 steps
c [elim-8-2] rescheduled 1780 variables 4% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 15960857 steps
c [elim-8-3] backward subsumption/strengthening limit 15960800
c [elim-8-3-1] backward checking 5591 touched variables 12%
c [elim-8-3-1] incomplete backward checking 5588 remain 100%
c [elim-8-3] subsumed 2 and strengthened 138 clauses in 15960816 steps
c [elim-8] incomplete 114 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 683 = 1% variables out of 48229 scheduled
c [bca-5] limit of 10000000 steps and 4506479 added (scaled 2)
c [bca-5] 45433 out of 95094 literals actually usable 48%
c [bca-5] added 157 blocked clauses in 132840 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 33955990 penalty 1 = 0 + 1
c [sweep-5-1] 364 pos 8.1% + 4157 neg 91.9% = 4521 sched 9.5% ret 43025
c [sweep-5-1] 33957411 steps 1012 queries 222.92 avg class size
c [sweep-5-1] 72620 decisions 940 SAT calls 365.27 avg env size
c [sweep-5-1] 393 variables remain 1% (47017 retained 99%)
c [decomp-19] removed 217 variables
c [sweep-5-1] removed 217 vars (0 failed, 72 eqs, 72 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 217 vars in TOTAL (1 rounds, 1011 queries)
c [sort-queue-9] sorted 47329 enqueued variables after 54083 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 47329 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 4121 variables 8.0% (47329 remain 45%)
c [simplification-9] removed 297769 irredundant clauses 11.8% (2229118 remain 74%)
c [simplification-9] maximum reduction of 12% = max (8%, 12%)
c [simplification-9] large reduction 12% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 66083 (soft 56083 + delta 10000)
c [simplification-9] new conflict limit 56083 (hard 66083)
c 
c [simplification-10] limit 56083 conflicts (hard 66083) hit after 56085 conflicts
c [quatres-6] found 14812 quaternary clauses 11% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-2] added 45 single-self-subsuming ternary resolvents
c [quatres-6-2] added 239 quaternary resolvents
c [ternres-6] limit 11623885 with penalty 1 = 0 + 1
c [ternres-6] 2728 schedulable variables 6%
c [ternres-6] 60 ternary resolvents (0 bin, 60 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 726492 penalty 4 = 3 + 1
c [card-4] no at-most-one constraint found
c [card-4] no at-most-two constraint found
c [gauss-3] limit 1114556 based on 2229112 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-5] limit 2229112 based on 2229112 irredundant clauses
c [transred-5] removed 0 transitive binary clauses
c [block-5] 6926 variables 15% will be scheduled this time
c [block-5] scheduled 6926 variables 15%
c [block-5] limit of 116238859 steps penalty 1 = 0 + 1
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 15788 blocked clauses
c [block-5] 15788 < 1/100 * 2229112 = 22291 considered unsuccessful
c [cce-3] limit of 14529857 steps penalty 3 = 2 + 1
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7266961 steps for small clauses
c [cce-3-1] scheduling 2084441 clauses = 2067897 binary + 16544 ternary
c [cce-3-1] tried to eliminate 29 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 14530444 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 * 2213324 = 22133 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 47200 variables 100%
c [elim-9] limit of 232477718 steps penalty 1 = 0 + 1
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 4705 not tried 10% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 4859 = 10% variables out of 47200 scheduled
c [bca-6] limit of 10000000 steps and 4002965 added (scaled 2)
c [bca-6] 37488 out of 84684 literals actually usable 44%
c [bca-6] added 9839 blocked clauses in 146779 steps
c [sweep-6] limit 4001194 based on 2000597 irredundant clauses
c [sweep-6-1] 15 pos 5.0% + 283 neg 95.0% = 298 sched 0.7% ret 42043
c [sweep-6-1] 4025233 steps 164 queries 47.62 avg class size
c [sweep-6-1] 10302 decisions 137 SAT calls 244.36 avg env size
c [sweep-6-1] 7 variables remain 0% (42334 retained 100%)
c [decomp-21] removed 26 variables
c [sweep-6-1] removed 26 vars (0 failed, 26 eqs, 36 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 26 vars in TOTAL (1 rounds, 163 queries)
c [sort-queue-10] sorted 42315 enqueued variables after 56085 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 42315 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 5014 variables 10.6% (42315 remain 41%)
c [simplification-10] removed 228548 irredundant clauses 10.3% (2000564 remain 67%)
c [simplification-10] maximum reduction of 11% = max (11%, 10%)
c [simplification-10] large reduction 11% >= 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 68085 (soft 58085 + delta 10000)
c [simplification-10] new conflict limit 58085 (hard 68085)
c 
c [simplification-11] limit 58085 conflicts (hard 68085) hit after 58088 conflicts
c [quatres-7] found 13664 quaternary clauses 11% in total
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 203 quaternary resolvents
c [ternres-7] limit 11911194 with penalty 1 = 0 + 1
c [ternres-7] all 42315 free variables schedulable
c [ternres-7] 1662 ternary resolvents (0 bin, 1662 trn)
c [ternres-7] 11959 variables remain 28% (30356 retained 72%)
c [elim-10] 4697 variables 11% will be scheduled this time
c [elim-10] scheduled 4697 variables 11%
c [elim-10] limit of 238223882 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 44 variables 0% in round 1 in 225519993 steps
c [elim-10-1] backward subsumption/strengthening limit 12703889
c [elim-10-1-1] backward checking 2829 touched variables 7%
c [elim-10-1-1] incomplete backward checking 3028 remain 107%
c [elim-10-1] subsumed 0 and strengthened 313 clauses in 12710604 steps
c [elim-10] incomplete 1180 not tried 3% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 44 = 1% variables out of 4697 scheduled
c [elim-10] 44 < 1/100 * 4697 = 46 considered unsuccessful
c [bca-7] limit of 10000000 steps and 3984487 added (scaled 2)
c [bca-7] 37010 out of 84544 literals actually usable 44%
c [bca-7] added 0 blocked clauses in 130690 steps
c [sweep-7] limit 7146716 penalty 0 = 0 + 0
c [sweep-7-1] 0 pos 0.0% + 7 neg 100.0% = 7 sched 0.0% ret 42264
c [sweep-7-1] 105061 steps 5 queries 3.40 avg class size
c [sweep-7-1] 230 decisions 4 SAT calls 140.75 avg env size
c [sweep-7-1] fully completed sweeping round
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-2] 594 pos 1.4% + 41677 neg 98.6% = 42271 sched 100.0% ret 0
c [sweep-7-2] 7054718 steps 266 queries 586.70 avg class size
c [sweep-7-2] 11074 decisions 259 SAT calls 259.93 avg env size
c [sweep-7-2] 6551 variables remain 15% (35720 retained 85%)
c [decomp-24] removed 9 variables
c [sweep-7-2] removed 9 vars (0 failed, 9 eqs, 41 impls)
c [sweep-7] 9 < 1/1000 * 42271 = 42 considered unsuccessful
c [sweep-7] removed 9 vars in TOTAL (2 rounds, 269 queries)
c [sort-queue-11] sorted 42262 enqueued variables after 58088 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 42262 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 53 variables 0.1% (42262 remain 41%)
c [simplification-11] removed 11666 irredundant clauses 0.6% (1988898 remain 66%)
c [simplification-11] maximum reduction of 1% = max (0%, 1%)
c [simplification-11] geometric conflict interval increment 10666 = 21332 / 2
c [simplification-11] new conflict interval 31998
c [simplification-11] penalized conflict interval 31998 = 1 * 31998
c [simplification-11] hard conflict limit 106085 (soft 90086 + delta 15999)
c [simplification-11] new conflict limit 90086 (hard 106085)
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 -  244.4   42262  1988886     67490   13548  16114 33426   41  3338   84   1%    175  973   44   22  197%
c 
c [simplification-12] limit 90086 conflicts (hard 106085) hit after 90086 conflicts
c [quatres-8] found 14020 quaternary clauses 11% in total
c [quatres-8-2] added 5 single-self-subsuming ternary resolvents
c [quatres-8-2] added 315 quaternary resolvents
c [ternres-8] limit 32452752 with penalty 0 = 0 + 0
c [ternres-8] 11944 schedulable variables 28%
c [ternres-8] 123 ternary resolvents (0 bin, 123 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-25] removed 2 variables
c [treelook-3] limit 811318 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 44005 literals 52%
c [treelook-3] scheduling used 812799 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 811318 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 1090905 steps
c [treelook-3] 43999 literals remain 52%
c [treelook-3] 37584 variables remain to probed next time 89%
c [treelook-3] removed 0 variables, found 3 hbrs
c [unhide-7] limit 202829 with penalty 5 = 2 + 3
c [unhide-7-7] 0 units, 0 failed, 12240 tauts, 0 hbrs, 9920 literals
c [block-6] scheduling all variables this time
c [block-6] scheduled 42260 variables 100%
c [block-6] limit of 162263764 steps penalty 1 = 1 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 25326 blocked clauses
c [sort-queue-12] sorted 41805 enqueued variables after 90086 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 41805 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 457 variables 1.1% (41805 remain 40%)
c [simplification-12] removed 39585 irredundant clauses 2.0% (1949273 remain 65%)
c [simplification-12] maximum reduction of 2% = max (1%, 2%)
c [simplification-12] geometric conflict interval increment 10666 = 31998 / 3
c [simplification-12] new conflict interval 42664
c [simplification-12] penalized conflict interval 42664 = 1 * 42664
c [simplification-12] hard conflict limit 154082 (soft 132750 + delta 21332)
c [simplification-12] new conflict limit 132750 (hard 154082)
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 -  297.5   41805  1949210    116800   20912  16616 36913   44  2943   84   1%    624  227   53   31  173%
c 
c [simplification-13] limit 132750 conflicts (hard 154082) hit after 132753 conflicts
c [quatres-9] found 14558 quaternary clauses 11% in total
c [quatres-9-2] added 6 single-self-subsuming ternary resolvents
c [quatres-9-2] added 278 quaternary resolvents
c [ternres-9] limit 42293959 with penalty 0 = 0 + 0
c [ternres-9] all 41805 free variables schedulable
c [ternres-9] 37 ternary resolvents (0 bin, 37 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-27] removed 2 variables
c [basicprobe-3] limit 211469796 penalty 0 = 0 + 0
c [basicprobe-3-0] 5233 probes remain 13% after last round
c [basicprobe-3-0] 155 units = 155 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 155 variables, found 55608 hbrs
c [bate-2] eliminated 117 asymmetric tautologies during probing
c [transred-6] limit 1949076 based on 1949076 irredundant clauses
c [transred-6] removed 8 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 41648 variables 100%
c [block-7] limit of 422939592 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 582 blocked clauses
c [block-7] 582 < 1/100 * 1949072 = 19490 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 41645 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 1311 not tried 3% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 248 = 1% variables out of 41645 scheduled
c [elim-11] 248 < 1/100 * 41645 = 416 considered unsuccessful
c [bca-8] limit of 10000000 steps and 3857575 added (scaled 2)
c [bca-8] 38471 out of 82796 literals actually usable 46%
c [bca-8] added 26 blocked clauses in 127338 steps
c [sweep-8] limit 6344093 penalty 1 = 1 + 0
c [sweep-8-1] 269 pos 4.2% + 6168 neg 95.8% = 6437 sched 15.5% ret 34960
c [sweep-8-1] 6360025 steps 185 queries 516.09 avg class size
c [sweep-8-1] 12039 decisions 182 SAT calls 363.43 avg env size
c [sweep-8-1] 4171 variables remain 10% (37226 retained 90%)
c [decomp-28] removed 8 variables
c [sweep-8-1] removed 8 vars (0 failed, 7 eqs, 19 impls)
c [sweep-8] 8 < 1/1000 * 41397 = 41 considered unsuccessful
c [sweep-8] removed 8 vars in TOTAL (1 rounds, 184 queries)
c [sort-queue-13] sorted 41389 enqueued variables after 132753 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 41389 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 416 variables 1.0% (41389 remain 40%)
c [simplification-13] removed 23757 irredundant clauses 1.2% (1925438 remain 64%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 21332 = 42664 / 2
c [simplification-13] new conflict interval 63996
c [simplification-13] penalized conflict interval 63996 = 1 * 63996
c [simplification-13] hard conflict limit 228747 (soft 196749 + delta 31998)
c [simplification-13] new conflict limit 196749 (hard 228747)
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 -  353.7   41389  1925405    161832   25310  15096 79073   39  2923   85   1%    823  -18   38   35  108%
c 
c [simplification-14] limit 196749 conflicts (hard 228747) hit after 202407 conflicts
c [quatres-10] found 15252 quaternary clauses 11% in total
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 289 quaternary resolvents
c [ternres-10] limit 56614862 with penalty 0 = 0 + 0
c [ternres-10] all 41389 free variables schedulable
c [ternres-10] 17 ternary resolvents (0 bin, 17 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1415371 penalty 3 = 3 + 0
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [cce-4] boosting limit by 10
c [cce-4] limit of 353842890 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 298
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 297
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 294
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 290
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 288
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 287
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 286
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 282
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 280
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 278
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 276
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 273
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 272
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 271
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 270
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 268
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 266
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 264
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 263
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 262
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 261
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 260
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 259
c [cce-4-1] eliminated 5 clauses out of 8 (62%) of length 258
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 257
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 256
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 255
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 254
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 253
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 252
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 251
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 250
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 248
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 246
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 244
c [cce-4-1] eliminated 4 clauses out of 8 (50%) of length 243
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 242
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 241
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 240
c [cce-4-1] eliminated 5 clauses out of 7 (71%) of length 239
c [cce-4-1] eliminated 7 clauses out of 10 (70%) of length 238
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 237
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 236
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 235
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 231
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 226
c [cce-4-1] eliminated 4 clauses out of 7 (57%) of length 225
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 224
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 223
c [cce-4-1] eliminated 4 clauses out of 7 (57%) of length 222
c [cce-4-1] eliminated 33 clauses out of 35 (94%) of length 221
c [cce-4-1] eliminated 12 clauses out of 15 (80%) of length 220
c [cce-4-1] eliminated 10 clauses out of 12 (83%) of length 219
c [cce-4-1] eliminated 6 clauses out of 9 (67%) of length 218
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 217
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 216
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 215
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 214
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 212
c [cce-4-1] eliminated 5 clauses out of 7 (71%) of length 211
c [cce-4-1] eliminated 6 clauses out of 10 (60%) of length 210
c [cce-4-1] eliminated 8 clauses out of 10 (80%) of length 209
c [cce-4-1] eliminated 14 clauses out of 16 (88%) of length 208
c [cce-4-1] eliminated 12 clauses out of 14 (86%) of length 207
c [cce-4-1] eliminated 18 clauses out of 20 (90%) of length 206
c [cce-4-1] eliminated 12 clauses out of 14 (86%) of length 205
c [cce-4-1] eliminated 26 clauses out of 34 (76%) of length 204
c [cce-4-1] eliminated 24 clauses out of 24 (100%) of length 203
c [cce-4-1] eliminated 16 clauses out of 19 (84%) of length 202
c [cce-4-1] eliminated 31 clauses out of 34 (91%) of length 201
c [cce-4-1] eliminated 30 clauses out of 37 (81%) of length 200
c [cce-4-1] eliminated 17 clauses out of 23 (74%) of length 199
c [cce-4-1] eliminated 19 clauses out of 24 (79%) of length 198
c [cce-4-1] eliminated 3 clauses out of 8 (38%) of length 197
c [cce-4-1] eliminated 4 clauses out of 11 (36%) of length 196
c [cce-4-1] eliminated 1 clauses out of 9 (11%) of length 195
c [cce-4-1] eliminated 3 clauses out of 8 (38%) of length 194
c [cce-4-1] eliminated 2 clauses out of 12 (17%) of length 193
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 192
c [cce-4-1] eliminated 1 clauses out of 7 (14%) of length 191
c [cce-4-1] eliminated 2 clauses out of 19 (11%) of length 190
c [cce-4-1] eliminated 4 clauses out of 20 (20%) of length 189
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 188
c [cce-4-1] eliminated 15 clauses out of 24 (62%) of length 187
c [cce-4-1] eliminated 8 clauses out of 21 (38%) of length 186
c [cce-4-1] eliminated 15 clauses out of 22 (68%) of length 185
c [cce-4-1] eliminated 21 clauses out of 29 (72%) of length 184
c [cce-4-1] eliminated 25 clauses out of 34 (74%) of length 183
c [cce-4-1] eliminated 12 clauses out of 17 (71%) of length 182
c [cce-4-1] eliminated 11 clauses out of 55 (20%) of length 181
c [cce-4-1] eliminated 6 clauses out of 9 (67%) of length 180
c [cce-4-1] eliminated 1 clauses out of 29 (3%) of length 179
c [cce-4-1] eliminated 7 clauses out of 15 (47%) of length 177
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 561 large clauses in 353843360 steps
c [cce-4-1] allowing another 176921680 steps for small clauses
c [cce-4-1] scheduling 1787377 clauses = 1785710 binary + 1667 ternary
c [cce-4-1] tried to eliminate 2116 small clauses 0%
c [cce-4-1] eliminated 93 binary clauses 0%
c [cce-4-1] eliminated 93 small clauses 0%
c [cce-4-1] eliminated 93 small clauses in 353844174 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 654 covered clauses in round 1
c [cce-4] eliminated 654 covered clauses in TOTAL during 1 rounds
c [cce-4] 654 < 1/100 * 1925380 = 19253 considered unsuccessful
c [bca-9] limit of 10000000 steps and 3856156 added (scaled 2)
c [bca-9] 34514 out of 82780 literals actually usable 42%
c [bca-9] added 88 blocked clauses in 140196 steps
c [sort-queue-14] sorted 41389 enqueued variables after 202407 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 41389 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 0 variables 0.0% (41389 remain 40%)
c [simplification-14] removed 654 irredundant clauses 0.0% (1924726 remain 64%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 63996
c [simplification-14] new conflict interval 127992
c [simplification-14] penalized conflict interval 127992 = 1 * 127992
c [simplification-14] hard conflict limit 394395 (soft 330399 + delta 63996)
c [simplification-14] new conflict limit 330399 (hard 394395)
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 -  381.6   41389  1924723    205806   28629  15410 79441   38  2705   85   1%    921 -340   39   37  107%
c -  403.9   41389  1924713    249210   30509  15717 79586   41  2883   86   1%    971   27   38   38   98%
c -  423.4   41389  1924680    292429   32668  15881 79701   41  2929   86   1%    997  316   37   39   95%
c -  443.3   41389  1924651    335690   34353  15955 79782   41  2441   87   2%   1010 -302   46   39  117%
c 
c [simplification-15] limit 330399 conflicts (hard 394395) hit after 339148 conflicts
c [quatres-11] found 16018 quaternary clauses 12% in total
c [quatres-11-2] added 3 single-self-subsuming ternary resolvents
c [quatres-11-2] added 206 quaternary resolvents
c [ternres-11] limit 81399804 with penalty 0 = 0 + 0
c [ternres-11] all 41389 free variables schedulable
c [ternres-11] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2543743 penalty 4 = 4 + 0
c [card-5] found 6 at-most-one constraints of average size 3.5
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2543743 for elimination
c [card-5] 6 out of 6 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-30] removed 1 variables
c [simpleprobe-4] 29873 schedulable variables 72%
c [simpleprobe-4] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-4] 21774 variables remain 53% (19614 retained 47%)
c [simpleprobe-4] removed 0 variables, found 8393 hbrs, 0 units
c [transred-7] limit 1924623 based on 1924623 irredundant clauses
c [transred-7] removed 2 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 41388 variables 100%
c [block-8] limit of 400000000 steps penalty 1 = 1 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 934 blocked clauses
c [block-8] 934 < 1/100 * 1924621 = 19246 considered unsuccessful
c [bca-10] limit of 10000000 steps and 3854122 added (scaled 2)
c [bca-10] 39101 out of 82770 literals actually usable 47%
c [bca-10] added 215 blocked clauses in 152211 steps
c [sort-queue-15] sorted 41384 enqueued variables after 339148 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 41384 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 5 variables 0.0% (41384 remain 40%)
c [simplification-15] removed 960 irredundant clauses 0.0% (1923687 remain 64%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 127992
c [simplification-15] new conflict interval 255984
c [simplification-15] penalized conflict interval 255984 = 1 * 255984
c [simplification-15] hard conflict limit 723124 (soft 595132 + delta 127992)
c [simplification-15] new conflict limit 595132 (hard 723124)
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 -  472.9   41384  1923685    379370   35370  16263 88486   40  2392   85   2%   1017 -249   36   40   91%
c -  492.2   41384  1923685    424574   36235  16400 88573   39  1893   85   2%   1020 -584   37   40   93%
c -  512.2   41384  1923679    470246   37531  16506 88649   42  3020   86   1%   1022  434   46   40  115%
c -  533.3   41384  1923644    516678   39086  16692 88733   42  2389   86   2%   1023 -279   45   41  110%
c -  554.7   41384  1923622    564004   40718  16787 88813   38  3679   87   1%   1024  841   41   41  101%
c -  574.8   41384  1923620    611461   41683  16912 88874   40  1570   86   3%   1024 -1233   34   41   82%
c 
c [simplification-16] limit 595132 conflicts (hard 723124) hit after 621203 conflicts
c [quatres-12] found 16970 quaternary clauses 12% in total
c [quatres-12-2] added 8 single-self-subsuming ternary resolvents
c [quatres-12-2] added 202 quaternary resolvents
c [ternres-12] limit 129835047 with penalty 0 = 0 + 0
c [ternres-12] all 41384 free variables schedulable
c [ternres-12] 34 ternary resolvents (0 bin, 34 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-32] removed 3 variables
c [unhide-8] limit 312500 with penalty 6 = 3 + 3
c [unhide-8-8] 0 units, 0 failed, 1997 tauts, 0 hbrs, 45845 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 6 transitive binary clauses
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 41381 variables 100%
c [elim-12] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 3156 not tried 8% in round 1
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 9 = 0% variables out of 41381 scheduled
c [elim-12] 9 < 1/100 * 41381 = 413 considered unsuccessful
c [bca-11] limit of 10000000 steps and 3852029 added (scaled 2)
c [bca-11] 38090 out of 82746 literals actually usable 46%
c [bca-11] added 482 blocked clauses in 158460 steps
c [sweep-9] limit 9737628 penalty 2 = 2 + 0
c [sweep-9-1] 254 pos 6.1% + 3909 neg 93.9% = 4163 sched 10.1% ret 37209
c [sweep-9-1] 9741400 steps 326 queries 311.19 avg class size
c [sweep-9-1] 20389 decisions 318 SAT calls 256.85 avg env size
c [sweep-9-1] 1940 variables remain 5% (39432 retained 95%)
c [decomp-33] removed 10 variables
c [sweep-9-1] removed 10 vars (0 failed, 9 eqs, 34 impls)
c [sweep-9] 10 < 1/1000 * 41372 = 41 considered unsuccessful
c [sweep-9] removed 10 vars in TOTAL (1 rounds, 325 queries)
c [sort-queue-16] sorted 41362 enqueued variables after 621203 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 41362 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 22 variables 0.1% (41362 remain 40%)
c [simplification-16] removed 1323 irredundant clauses 0.1% (1922297 remain 64%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 255984
c [simplification-16] new conflict interval 511968
c [simplification-16] penalized conflict interval 511968 = 1 * 511968
c [simplification-16] hard conflict limit 1389155 (soft 1133171 + delta 255984)
c [simplification-16] new conflict limit 1133171 (hard 1389155)
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 -  604.6   41362  1922288    659025   43185  16878 87432   44  3271   87   1%   1024  555   44   41  107%
c -  625.6   41362  1922275    707339   43932  16966 87516   39  2101   87   2%   1024 -573   32   41   79%
c -  649.6   41362  1922275    756865   44211  17098 87613   42  2164   87   2%   1024 -477   48   41  117%
c -  671.3   41362  1922264    807155   45527  17199 87683   43  2426   87   2%   1024 -189   40   41   96%
c -  693.9   41362  1922263    857887   46120  17297 87755   40  1976   87   2%   1024 -377   45   41  110%
c -  716.8   41362  1922255    909616   46944  17345 87844   41  2120   88   2%   1024 -346   41   41  101%
c -  741.0   41362  1922251    962442   48137  17379 87904   41  2901   87   1%   1024  343   42   41  101%
c -  762.8   41362  1922246   1014724   48444  17482 87979   42  2537   87   2%   1024 -232   38   42   89%
c -  786.3   41362  1922235   1068664   50012  17550 88062   42  2729   87   2%   1024  208   43   42  102%
c -  809.9   41362  1922231   1123644   50706  17641 88124   41  2136   88   2%   1024 -201   48   41  116%
c 
c [simplification-17] limit 1133171 conflicts (hard 1389155) hit after 1136045 conflicts
c [quatres-13] found 18093 quaternary clauses 12% in total
c [quatres-13-2] added 51 single-self-subsuming ternary resolvents
c [quatres-13-2] added 181 quaternary resolvents
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] all 41362 free variables schedulable
c [ternres-13] 100 ternary resolvents (0 bin, 100 trn)
c [ternres-13] fully completed ternary resolution
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2 transitive binary clauses
c [bca-12] limit of 10000000 steps and 3851552 added (scaled 2)
c [bca-12] 33689 out of 82726 literals actually usable 41%
c [bca-12] added 65 blocked clauses in 151124 steps
c [sort-queue-17] sorted 41362 enqueued variables after 1136045 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 41362 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 0 variables 0.0% (41362 remain 40%)
c [simplification-17] removed 2 irredundant clauses 0.0% (1922228 remain 64%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 511968
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] hard conflict limit 2636045 (soft 2136045 + delta 500000)
c [simplification-17] new conflict limit 2136045 (hard 2636045)
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 -  835.4   41362  1922226   1178646   51502  17825 88249   42  2272   88   2%   1024  -21   41   42   98%
c -  861.0   41362  1922226   1235225   52734  17893 88322   43  2823   89   2%   1024  204   48   41  117%
c -  885.7   41362  1922226   1292246   53680  17965 88393   43  2406   88   2%   1024   15   44   42  105%
c -  912.7   41362  1922224   1350872   54704  18023 88461   41  2241   89   2%   1024 -229   44   41  105%
c -  940.7   41362  1922222   1408551   54828  18072 88522   43  3514   89   1%   1024  801   42   43   98%
c -  965.8   41362  1922221   1467920   56307  18128 88577   42  2913   88   1%   1024  389   42   42  100%
c -  991.8   41362  1922221   1527748   56945  18180 88650   41  3317   89   1%   1024  790   38   42   90%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 159 basic ate = 86 trn 54% + 73 lrg 46% in 2 updates
c bcas: 12 count, 13258 added (8252 skipped), 1998462 steps
c bkwd: tried 54763 clauses, 102103 lits, 1.86 lits/clause
c bkwd: checked 239138879 occs, 4366.80 occs/clause, 2342.13 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 12 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 13523 large (0% self)
c blkd: 8 bces, 362504 removed, 90067118 resolutions, 270356830 steps
c blkd: 11943 blocking literals 6%, 4119 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 5 count, 0 units, 0 am1, 18612673 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 128 subsumed
c card: 12 at-most-one constraints found, average size 3.33
c card: 12 at-most-one constraints used 100%, average size 3.33
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, 686 eliminated, 685 ate 100%, 1 abce 0%
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: 11925086 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 81 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 34 decompositions, 2565 equivalent 2%
c deco: 20 decision-only clauses 0%, 47% reduction
c decs: 274670494 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 58482 eliminated 56%, 676 pure 1%
c elms: 17 rounds, 1.4 rounds/bve
c elms: 36166 small 62%, 17521 large 30%
c elms: 36207 tried small, 36166 succeeded 100%, 41 failed 0%
c elms: 7758 subsumed, 224000 strengthened, 0 blocked
c elms: 16617550 copies, 41835942 resolutions, 690136 ipos
c elms: 106992652 subchks, 43392933 strchks
c gaus: 4 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 11084482 steps, 5542241 extr 50%, 0 elim 0%
c glue: 40.7 orig avg, 40.7 real avg, 6.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 99636 = 15757 simple 16% + 83821 trn 84% + 58 lrg 0%, 3288 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1482922 clauses, 123.7 length
c lrnd: 183430346 lits = 214244002 orig - 30813656 removed 14%
c lrnd: 957553 uips 65%, 112787 flips 8%
c mins: 1465514 mins 99%, 2871 bin 0%, 12651 size 1%
c mins: 103764915 poisoned searches, 35509033 hits, 34% hit rate
c mins: 277496420 used twice searches, 33784543 hits, 12% hit rate
c move: moved 339019, 335105 bin 99%, 3914 trn 1%
c otfs: 60305 driving 20%, 235794 restarting 80%
c otfs: str 296099, 292255 red 99%, 3844 irr 1%
c otfs: str 296099, 0 bin 0%, 364 trn 0%, 295735 lrg 100%
c otfs: sub 630, 117 red 19%, 513 irr 81%
c otfs: sub 630, 0 bin 0%, 5 trn 1%, 625 lrg 99%
c phas: 1 computed, 100238 set, 0 pos (0%), 100238 neg (100%)
c prbs: 3 basic, 68070 probed, 343 failed, 0 lifted
c prbs: 4 simple, 159941 probed, 1 failed, 0 eqs
c prbs: 3 treelook, 41 probed, 0 failed, 0 lifted
c prom: 128165 locked 12% out of 1099545 tried
c prps: 2173792645 props, 8 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 13 count, 3678 quat, 581 self1, 0 self2, 22 dup
c queu: 17 sorted, 274670495 next (0 steps 0.00)
c queu: 1012729 enq (1012711 steps 1.00), 0 deq 0%
c redc: 9011 clauses 22%, 40141 tried 3%, 107 sat 0%
c redc: 40931 lits 9%, 459905 tried 0%, 107 sat 0%
c redc: 1247 times jump level reduced, 998.3 levels on average
c reds: 30 count, 51420.0 conflicts per reduce
c reds: 0 memlim 0%, 30 arith 100%
c reds: 967831 collected 75%, 326294 retired 25%
c rmbd: 7109 removed, 1363 red 19%
c rsts: 15366 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 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: 17 count, 16 confs 94%, 0 vars 0%
c simp: 0 its 0%, 1 bin 6%, 0 trns 0%
c subl: 1482922 count (1772535 tried 1.2), 103901 sub out of 1473311 (7.1%)
c swps: 9 count, 10 rounds, 2693 queries (269.3/round)
c swps: 2557 sat calls, 22 unsat (0.2% success rate)
c swps: 157974 decisions 61.8, 627 conflicts 0.2
c swps; 545.2 avg class size, 310.4 avg environment size
c swps: 0 failed, 282 impls, 157 equivs
c swp0: 894 type 0 queries, 72 unsat (8.1%), 871 sat (97.4%)
c swp1: 1799 type 1 queries, 400 unsat (22.2%), 1665 sat (92.6%)
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: 549341323 calls to obtain time
c tops: 1835 fixed 2%, 29 its, 53193.10 confs/it
c trds: 9 transitive reductions, 22 removed, 0 failed
c trds: 918 nodes, 24396 edges, 20842261 steps
c trim: 2801052 words, 10.7 MB
c trnr: 13 count, 1 bin, 19387 trn, 213483503 steps
c unhd: 8 count, 8 rounds, 38722472 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 2 failed, 2 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 39754 tauts, 23 bin 0%, 355 trn 1%, 4418 lrg 11%
c unhd: 39754 tauts, 34958 stamp 88%, 4315 red 11%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 195996 str, 1 bin 0%, 1012 trn 1%, 194983 lrg 99%, 111780 red 57%
c vars: 41362 remaining 40% and 62882 removed 60% out of 104244
c vars: 1835 fixed 2%, 58482 eliminated 56%, 2565 equivalent 2%
c vsts: 29216174706 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 13.8 search visits per propagation, 18778.4 per conflict
c wchs: 2390650873 pushed, 192437117 enlarged, 132 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1476989        967831        326294      81899670       9061664       1030473
c 
c  0 0         37233   3      6152   1         0   0  49858223  61   1948246  21     65158   6     1.3
c  1 5         11666   1      4734   0      4932   2   4043365   5<   284291   3     14865   1     0.2
c  2 6         45401   3     25804   3     13836   4   6878433   8    743472   8     54390   5     0.9
c  3 9        101633   7     68639   7     21827   7   6014418   7   1298183  14    124374  12     2.2
c  4 14       178175  12    134440  14     29643   9   4623287   6   1565414  17<   182004  18     3.1
c  5 21       232333  16    172538  18     39469  12   3491516   4   1287593  14    197553  19<    4.2
c  6 30       250723  17<   174199  18<    48878  15<  2697817   3    864638  10    173298  17     5.4
c  7 41       237959  16    156919  16     52636  16   1893881   2    567464   6    119789  12     5.9
c  8 54       175387  12    109356  11     45305  14   1090716   1    270553   3     55495   5     4.6
c  9 69       102720   7     59949   6     31090  10    833396   1    132374   1     26767   3     3.5
c 10 86        80957   5     44124   5     28467   9    440124   1     82726   1     14443   1     3.7
c 11 126       21954   1     10647   1      9737   3     33388   0     16188   0      2235   0     1.6
c 12 230         843   0       330   0       470   0      1096   0       521   0       102   0     0.1
c 13 534           5   0         0   0         4   0        10   0         1   0         0   0     0.0
c 
c avg                  6.0           6.0           6.5           1.5           3.5           4.8
c std                  2.3           2.1           2.4           2.3           2.5           2.2
c 
c  176.257  18% decide
c   71.132   7% elim
c   54.747   5% block
c   19.750   2% probe
c    8.608   1% sweep
c    7.849   1% unhide
c    4.846   0% cce
c 
c   11.834 < 1% rest (below)
c 
c    4.487   0% bca
c    3.585   0% quatres
c    1.870   0% gauss
c    1.388   0% ternres
c    0.370   0% transred
c    0.134   0% card
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.747   0% preprocessing     2%
c  189.481  19% inprocessing     98%
c ==================================
c  193.229  19% simplifying
c  805.152  81% search
c ==================================
c  998.382 100% all
c 
c       1542600 conflicts,        1545.1 confs/sec
c          5554 ternaries,         277.7 confs/ternary
c          3818 binaries,          404.0 confs/binary
c            29 iterations,      53193.1 confs/iteration
c 
c            30 reductions,          0.0 redus/sec,  51420.0 confs/reduction
c         15366 restarts,           15.4 rests/sec,    100.4 confs/restart
c     274670494 decisions,      275115.6 decis/sec,    178.1 decis/conflict
c    2173792645 propagations,  2177315.1 props/sec,      7.9 props/decision
c 
c 998.4 seconds, 199.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
