c launch: /data/cnf/sc2014/app/post-cbmc-aes-d-r2.cnf.bz2
c host: atom11
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/post-cbmc-aes-d-r2.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/post-cbmc-aes-d-r2.cnf.bz2
c no embedded options
c found 'p cnf 279119 1607567' header
c read 279119 variables, 1607567 clauses, 4321960 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 --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 172218 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 
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  172218  1356467         0       0      0     0    0     0   64   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 152399 variables
c [simpleprobe-1] all 124496 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 2155 variables
c [simpleprobe-1] 73174 variables remain 60% (49167 retained 40%)
c [simpleprobe-1] removed 2155 variables, found 18008 hbrs, 60 units
c [unhide-1] limit 59065 based on 945051 irredundant clauses
c [unhide-1-1] 42 units, 180 failed, 1986 tauts, 0 hbrs, 2392 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 117565 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 68230 not tried 58% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 44650 = 38% variables out of 117565 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 783129 negative 99.8% of 784795 except 1666 0.2%
c [phase-count-1] 490206 positive 62.5% of 784795 except 294589 37.5%
c [phase-count-1] less non-negative clauses 1666 than limit 78400 (10.0%)
c [phase-count-1] non-pos/non-neg = 294589/1666 = 176.82 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 72915 negative 100%
c [sort-queue-1] sorted 72915 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 72915 (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 86509 variables 54.3% (72915 remain 42%)
c [simplification-1] removed 571672 irredundant clauses 42.1% (784795 remain 58%)
c [simplification-1] maximum reduction of 54% = max (54%, 42%)
c [simplification-1] large reduction 54% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.3   72914   784795        27      20      2  2188    0     1   43   3%      0    1    0    0 24044%
c i    4.3   72913   784795        28      20      2  2188    0     1   43   3%      0    1    0    0 23950%
c i    4.3   72905   784795        60      32     17  2189    0     1   43   4%      0    1    1    0 22378%
c i    4.3   72729   784795       123      71     29  2194    0     2   43   6%      0    2    1    0 20426%
c i    4.3   72720   784795       153      91     36  2195    0     2   43   7%      0    2    1    0 19428%
c i    4.3   72710   784795       156      92     37  2195    0     2   43   7%      0    2    1    0 19228%
c i    4.3   72535   784795       197     119     45  2198    0     2   43   7%      0    2    2    0 18118%
c i    4.3   72421   784795       251     153     54  2199    0     3   43   8%      0    3    2    0 17390%
c i    4.4   72411   784795       348     196     90  2207    0     8   43   3%      0    8    3    0 14255%
c i    4.4   72402   784794       371     204     94  2212    0     9   43   3%      0    9    3    0 14093%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1049 variables
c [simpleprobe-2] 40148 schedulable variables 56%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 599 variables
c [simpleprobe-2] 41311 variables remain 58% (29956 retained 42%)
c [simpleprobe-2] removed 599 variables, found 3398 hbrs, 40 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 33129 literals 23%
c [treelook-1] scheduling used 301618 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300698 steps
c [treelook-1] 33098 literals remain 23%
c [treelook-1] 32709 variables remain to probed next time 46%
c [basicprobe-1] limit 6190440 based on 773805 irredundant clauses
c [basicprobe-1-0] 36939 probes remain 52% after last round
c [basicprobe-1-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 24 variables, found 3289 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 24 units, 319 failed, 52 tauts, 0 hbrs, 3085 literals
c [elim-2] 63908 variables 92% will be scheduled this time
c [elim-2] scheduled 63908 variables 92%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 43772 not tried 63% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 20142 = 32% variables out of 63908 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 662625 negative 99.8% of 664203 except 1578 0.2%
c [phase-count-2] 426796 positive 64.3% of 664203 except 237407 35.7%
c [phase-count-2] less non-negative clauses 1578 than limit 66400 (10.0%)
c [phase-count-2] non-pos/non-neg = 237407/1578 = 150.45 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 5839 negative 100%
c [sort-queue-2] sorted 49195 enqueued variables after 371 conflicts
c [score-dist-2] active 0 (0%), one 1315 (3%), zero 47880 (97%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 23206 variables 32.1% (49195 remain 29%)
c [simplification-2] removed 120591 irredundant clauses 15.4% (664203 remain 49%)
c [simplification-2] maximum reduction of 32% = max (32%, 15%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1013 (hard 11000)
c [simplification-2] 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    6.8   49194   664203       380     105     53  5234    0    10   40   3%      0   10    3    0 13904%
c i    6.8   49193   664203       381     105     53  5234    0    10   40   3%      0   10    3    0 13850%
c i    6.8   49119   664203       382     105     53  5234    0    10   40   3%      0   10    3    0 13796%
c i    6.8   49103   664203       383     105     53  5234    0    10   40   3%      0   10    3    0 13742%
c i    6.8   49095   664202       416     125     53  5234    0    10   40   3%      0   10    3    0 13587%
c i    6.8   49031   664202       417     125     53  5234    0    10   40   3%      0   10    3    0 13534%
c i    6.9   49012   664200       485     177     61  5235    0    12   40   4%      0   12    3    0 12529%
c i    6.9   49011   664200       486     177     61  5235    0    12   40   4%      0   12    3    0 12481%
c i    6.9   49010   664200       529     204     69  5236    0    12   40   4%      0   12    4    0 11662%
c i    6.9   49009   664200       533     204     71  5237    0    12   40   4%      0   12    3    0 11517%
c i    6.9   49008   664200       594     252     74  5239    1    13   40   4%      0   13    4    0 11409%
c i    6.9   48939   664200       617     265     80  5241    1    13   40   4%      0   13    4    0 10870%
c i    6.9   48918   664200       618     265     80  5241    1    13   40   4%      0   13    4    0 10828%
c i    6.9   48912   664200       619     265     80  5241    1    13   40   4%      0   13    4    0 10786%
c i    6.9   48911   664199       700     321     92  5244    1    15   40   4%      0   15    4    0 10291%
c i    6.9   48910   664197       746     348     98  5248    1    16   40   4%      0   15    4    0 9516%
c i    6.9   48909   664197       790     368    113  5254    1    16   40   4%      0   16    4    0 8606%
c i    6.9   48908   664197       808     378    119  5255    1    16   40   4%      0   16    4    0 8300%
c i    6.9   48902   664197       836     392    128  5255    1    17   40   4%      0   17    4    0 7900%
c i    6.9   48901   664197       864     406    136  5256    1    17   40   4%      0   17    4    0 7602%
c i    6.9   48900   664197       868     407    136  5258    1    17   40   4%      0   17    4    0 7516%
c i    6.9   48899   664197       869     407    136  5258    1    17   40   4%      0   17    4    0 7487%
c i    6.9   48886   664197       878     412    139  5258    1    17   40   4%      0   17    4    0 7321%
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    6.9   48877   664197       879     412    139  5258    1    17   40   4%      0   17    4    0 7292%
c i    6.9   48863   664197       880     412    139  5258    1    17   40   4%      0   17    4    0 7264%
c i    6.9   48849   664197       881     412    139  5258    1    17   40   4%      0   17    4    0 7236%
c i    6.9   48836   664197       882     412    139  5258    1    17   40   4%      0   17    4    0 7207%
c i    6.9   48813   664197       884     412    139  5258    1    17   40   4%      0   17    4    0 7179%
c i    6.9   48812   664197       924     436    146  5261    1    18   40   4%      0   17    4    0 7124%
c i    6.9   48796   664197       979     460    168  5263    1    18   40   4%      0   18    4    0 6463%
c i    6.9   48788   664197       981     460    169  5263    1    18   40   4%      0   18    4    0 6418%
c i    6.9   48773   664197       982     460    169  5263    1    18   40   4%      0   18    4    0 6393%
c i    6.9   48734   664197       983     460    169  5263    1    18   40   4%      0   18    4    0 6368%
c i    6.9   48733   664195      1117     544    205  5270    1    19   40   5%      0   19    4    0 5766%
c i    6.9   48732   664195      1124     548    206  5270    1    19   40   5%      0   19    4    0 5690%
c i    6.9   48731   664195      1161     570    209  5271    1    20   41   5%      0   19    4    0 5739%
c 
c [simplification-3] limit 1170 conflicts (hard 11000) hit after 1170 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 6 at-most-one constraints of average size 3.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 6 out of 6 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 887 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 20 units, 141 failed, 1790 tauts, 0 hbrs, 1508 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 47627 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 21631 not tried 45% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 19375 = 41% variables out of 47627 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 550192 negative 99.8% of 551224 except 1032 0.2%
c [phase-count-3] 363580 positive 66.0% of 551224 except 187644 34.0%
c [phase-count-3] less non-negative clauses 1032 than limit 55100 (10.0%)
c [phase-count-3] non-pos/non-neg = 187644/1032 = 181.83 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 4587 negative 100%
c [sort-queue-3] sorted 28252 enqueued variables after 1170 conflicts
c [score-dist-3] active 0 (0%), one 1151 (4%), zero 27101 (96%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 20479 variables 42.0% (28252 remain 16%)
c [simplification-3] removed 112971 irredundant clauses 17.0% (551224 remain 41%)
c [simplification-3] maximum reduction of 42% = max (42%, 17%)
c [simplification-3] large reduction 42% >= 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 13170 (soft 3170 + delta 10000)
c [simplification-3] new conflict limit 3170 (hard 13170)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.3   28251   551189      1985     893     91  1221    2    59   37   3%      4   59    7    0 4816%
c i    9.3   28250   551189      2031     936     91  1222    2    61   37   3%      4   61    7    0 4556%
c i    9.4   28249   551182      2211    1098     96  1225    2    65   37   3%      4   64    7    0 3877%
c i    9.4   28248   551182      2212    1098     96  1225    2    65   37   3%      4   64    7    0 3862%
c i    9.4   28247   551182      2213    1098     96  1225    2    65   37   3%      4   64    6    0 3847%
c i    9.4   28246   551182      2214    1098     96  1225    2    65   37   3%      4   64    6    0 3832%
c i    9.4   28245   551182      2215    1098     96  1225    2    65   37   3%      4   64    6    0 3817%
c i    9.4   28244   551182      2216    1098     96  1225    2    65   37   3%      4   64    6    0 3802%
c i    9.4   28243   551162      2840    1632    105  1248    3    64   38   5%      4   63    7    0 3115%
c 
c [simplification-4] limit 3220 conflicts (hard 13170) hit after 3220 conflicts
c [decomp-6] removed 27 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 7892 literals 14%
c [treelook-2] scheduling used 153034 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 162326 steps
c [treelook-2] 7882 literals remain 14%
c [treelook-2] 7471 variables remain to probed next time 26%
c [treelook-2] removed 0 variables, found 20 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 28 failed, 23 tauts, 0 hbrs, 606 literals
c [elim-4] 21223 variables 75% will be scheduled this time
c [elim-4] scheduled 21223 variables 75%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 18242 variables 65% in round 1 in 259687551 steps
c [elim-4-1] backward subsumption/strengthening limit 140312449
c [elim-4-1-1] backward checking 3051 touched variables 11%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 59 and strengthened 235 clauses in 76789177 steps
c [elim-4-1] rescheduled 681 variables 2% by backward subsumption
c [elim-4-2] eliminated 111 variables 0% in round 2 in 3521650 steps
c [elim-4-2] backward subsumption/strengthening limit 3521600
c [elim-4-2-1] backward checking 610 touched variables 2%
c [elim-4-2-1] incomplete backward checking 226 remain 37%
c [elim-4-2] subsumed 25 and strengthened 51 clauses in 3522028 steps
c [elim-4-2] rescheduled 140 variables 0% by backward subsumption
c [elim-4-3] eliminated 25 variables 0% in round 3 in 138686 steps
c [elim-4-3] backward subsumption/strengthening limit 138600
c [elim-4-3-1] backward checking 295 touched variables 1%
c [elim-4-3-1] incomplete backward checking 271 remain 92%
c [elim-4-3] subsumed 3 and strengthened 11 clauses in 140506 steps
c [elim-4] incomplete 12 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 18386 = 87% variables out of 21223 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 9817 enqueued variables after 3220 conflicts
c [score-dist-4] active 0 (0%), one 2362 (24%), zero 7455 (76%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 18423 variables 65.2% (9817 remain 6%)
c [simplification-4] removed 161117 irredundant clauses 29.2% (390032 remain 29%)
c [simplification-4] maximum reduction of 65% = max (65%, 29%)
c [simplification-4] large reduction 65% >= 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 15220 (soft 5220 + delta 10000)
c [simplification-4] new conflict limit 5220 (hard 15220)
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.8    9816   390025      3293     523     96    96    3    68   47   5%      4   66    7    0 2514%
c i   18.0    9814   389798      4560    1337    120   102    4    76   47   6%      9   73    8    0 1890%
c i   18.0    9813   389798      4569    1342    120   102    5    76   47   6%      9   73   10    0 2494%
c i   18.0    9812   389780      4697    1452    122   102    5    80   47   6%      8   77   10    0 2214%
c i   18.0    9811   389780      4698    1452    122   102    5    80   47   6%      8   77   10    0 2206%
c i   18.0    9810   389780      4699    1452    122   102    5    80   47   6%      8   77   10    0 2197%
c 
c [simplification-5] limit 5241 conflicts (hard 15220) hit after 5242 conflicts
c [quatres-1] found 5333 quaternary clauses 1% in total
c [quatres-1-2] added 34 single-self-subsuming ternary resolvents
c [quatres-1-2] added 44 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 9810 free variables schedulable
c [ternres-1] 44866 ternary resolvents (5031 bin, 39835 trn)
c [ternres-1] 217 variables remain 2% (9593 retained 98%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 49071 xors of average arity 2.9
c [gauss-1] connected 140803 occurrences of 7132 variables (average 19.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 1128 variables
c [basicprobe-2] limit 3116432 based on 389554 irredundant clauses
c [basicprobe-2-0] 1128 sched 13%, 69 failed, 1 lifted, 3695 hbrs
c [decomp-9] removed 249 variables
c [basicprobe-2-1] 173 probes remain 2% after last round
c [basicprobe-2-1] 70 units = 69 failed (99%) + 1 lifted (1%)
c [basicprobe-2-1] removed 249 variables, found 3823 hbrs
c [bate-1] eliminated 271 asymmetric tautologies during probing
c [unhide-5] limit 121095 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 673 tauts, 0 hbrs, 479 literals
c [transred-1] limit 605476 with penalty 0 = 0 + 0
c [transred-1] removed 221 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 8433 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] incomplete 24 not tried 0%
c [block-1] transition to [ all 1 rem 1 ] state
c [block-1] eliminated 33719 blocked clauses
c [block-1] considered successful since not run to completion yet
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 27
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 26
c [cce-1-1] eliminated 4 clauses out of 88 (5%) of length 11
c [cce-1-1] eliminated 26 clauses out of 459 (6%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 42 large clauses in 30000224 steps
c [cce-1-1] allowing another 15000112 steps for small clauses
c [cce-1-1] scheduling 4444 clauses = 3804 binary + 640 ternary
c [cce-1-1] tried to eliminate 1036 small clauses 23%
c [cce-1-1] eliminated 253 binary clauses 7%
c [cce-1-1] eliminated 20 ternary clauses 3%
c [cce-1-1] eliminated 273 small clauses 6%
c [cce-1-1] eliminated 273 small clauses in 30002091 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 315 covered clauses in round 1
c [cce-1] eliminated 315 covered clauses in TOTAL during 1 rounds
c [cce-1] 315 < 1/100 * 354219 = 3542 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3630 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1737 not tried 48% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 279 = 8% variables out of 3630 scheduled
c [bca-1] limit of 10000000 steps and 706540 added (scaled 2)
c [bca-1] 4614 out of 6704 literals actually usable 69%
c [bca-1] added 120 blocked clauses in 44241 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1405 pos 41.9% + 1946 neg 58.1% = 3351 sched 100.0% ret 0
c [sweep-1-1] 1056020 steps 53 queries 596.09 avg class size
c [sweep-1-1] 1010 decisions 51 SAT calls 24.71 avg env size
c [sweep-1-1] 3198 variables remain 95% (153 retained 5%)
c [decomp-10] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 52 queries)
c [sort-queue-5] sorted 3348 enqueued variables after 5242 conflicts
c [score-dist-5] active 0 (0%), one 2621 (78%), zero 727 (22%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 6462 variables 65.9% (3348 remain 2%)
c [simplification-5] removed 36736 irredundant clauses 9.4% (352963 remain 26%)
c [simplification-5] maximum reduction of 66% = max (66%, 9%)
c [simplification-5] large reduction 66% >= 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 17242 (soft 7242 + delta 10000)
c [simplification-5] new conflict limit 7242 (hard 17242)
c 
c [simplification-6] limit 7242 conflicts (hard 17242) hit after 7243 conflicts
c [quatres-2] found 3700 quaternary clauses 1% in total
c [quatres-2-2] added 202 single-self-subsuming ternary resolvents
c [quatres-2-2] added 242 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 101 schedulable variables 3%
c [ternres-2] 162 ternary resolvents (15 bin, 147 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 10 at-most-one constraints of average size 6.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 10 out of 10 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 7 variables
c [simpleprobe-3] 1894 schedulable variables 57%
c [simpleprobe-3] limit 3163782 penalty 0 = 0 + 0
c [simpleprobe-3] 1359 variables remain 41% (1982 retained 59%)
c [simpleprobe-3] removed 0 variables, found 210 hbrs, 0 units
c [transred-2] limit 790945 with penalty 0 = 0 + 0
c [transred-2] removed 130 transitive binary clauses
c [block-2] 24 variables 1% will be scheduled this time
c [block-2] scheduled 24 variables 1%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] incomplete 13 not tried 0%
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] no untried remaining variables left
c [elim-6] scheduled 3341 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1731 not tried 52% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 46 = 1% variables out of 3341 scheduled
c [bca-2] limit of 10000000 steps and 705556 added (scaled 2)
c [bca-2] 3654 out of 6592 literals actually usable 55%
c [bca-2] added 0 blocked clauses in 32035 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1445 pos 45.9% + 1700 neg 54.1% = 3145 sched 95.4% ret 150
c [sweep-2-1] 1042397 steps 53 queries 587.53 avg class size
c [sweep-2-1] 1139 decisions 50 SAT calls 23.68 avg env size
c [sweep-2-1] 2969 variables remain 90% (326 retained 10%)
c [decomp-13] removed 2 variables
c [sweep-2-1] removed 2 vars (0 failed, 2 eqs, 4 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 2 vars in TOTAL (1 rounds, 52 queries)
c [sort-queue-6] sorted 3293 enqueued variables after 7243 conflicts
c [score-dist-6] active 0 (0%), one 2877 (87%), zero 416 (13%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 55 variables 1.6% (3293 remain 2%)
c [simplification-6] removed 211 irredundant clauses 0.1% (352398 remain 26%)
c [simplification-6] maximum reduction of 2% = max (2%, 0%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 23909 (soft 13909 + delta 10000)
c [simplification-6] new conflict limit 13909 (hard 23909)
c 
c [simplification-7] limit 13909 conflicts (hard 23909) hit after 13909 conflicts
c [quatres-3] found 3794 quaternary clauses 1% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 71 single-self-subsuming ternary resolvents
c [quatres-3-2] added 97 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3293 free variables schedulable
c [ternres-3] 932 ternary resolvents (21 bin, 911 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 6688 xors of average arity 3.3
c [gauss-2] connected 21976 occurrences of 1730 variables (average 12.7)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] connected 3305 occurrences of 1730 variables (average 1.9)
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-6] limit 130583 with penalty 1 = 1 + 0
c [unhide-6-6] 0 units, 0 failed, 182 tauts, 0 hbrs, 373 literals
c [transred-3] limit 1305835 with penalty 0 = 0 + 0
c [transred-3] removed 66 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3293 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] incomplete 125 not tried 4%
c [block-3] transition to [ all 1 rem 1 ] state
c [block-3] eliminated 12 blocked clauses
c [block-3] considered successful since not run to completion yet
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500413 steps for small clauses
c [cce-2-1] scheduling 6749 clauses = 3337 binary + 3412 ternary
c [cce-2-1] tried to eliminate 466 small clauses 7%
c [cce-2-1] eliminated 7 binary clauses 0%
c [cce-2-1] eliminated 33 ternary clauses 1%
c [cce-2-1] eliminated 40 small clauses 1%
c [cce-2-1] eliminated 40 small clauses in 15000700 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 40 covered clauses in round 1
c [cce-2] eliminated 40 covered clauses in TOTAL during 1 rounds
c [cce-2] 40 < 1/100 * 351334 = 3513 considered unsuccessful
c [elim-7] 1731 variables 53% will be scheduled this time
c [elim-7] scheduled 1731 variables 53%
c [elim-7] limit of 26116707 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 1359 not tried 41% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 1 = 0% variables out of 1731 scheduled
c [elim-7] 1 < 1/100 * 1731 = 17 considered unsuccessful
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1348 pos 45.4% + 1620 neg 54.6% = 2968 sched 90.2% ret 324
c [sweep-3-1] 1050156 steps 45 queries 550.00 avg class size
c [sweep-3-1] 1140 decisions 43 SAT calls 32.58 avg env size
c [sweep-3-1] 2759 variables remain 84% (533 retained 16%)
c [decomp-15] removed 7 variables
c [sweep-3-1] removed 7 vars (0 failed, 1 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 7 vars in TOTAL (1 rounds, 44 queries)
c [sort-queue-7] sorted 3285 enqueued variables after 13909 conflicts
c [score-dist-7] active 0 (0%), one 3103 (94%), zero 182 (6%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 8 variables 0.2% (3285 remain 2%)
c [simplification-7] removed 305 irredundant clauses 0.1% (351055 remain 26%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 26666
c [simplification-7] penalized conflict interval 26666 = 1 * 26666
c [simplification-7] hard conflict limit 53908 (soft 40575 + delta 13333)
c [simplification-7] new conflict limit 40575 (hard 53908)
c 
c [simplification-8] limit 40575 conflicts (hard 53908) hit after 40576 conflicts
c [quatres-4] found 3719 quaternary clauses 1% in total
c [quatres-4-2] added 222 single-self-subsuming ternary resolvents
c [quatres-4-2] added 46 quaternary resolvents
c [ternres-4] limit 4065597 with penalty 0 = 0 + 0
c [ternres-4] all 3285 free variables schedulable
c [ternres-4] 1192 ternary resolvents (83 bin, 1109 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-16] removed 3 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 61 transitive binary clauses
c [block-4] 13 variables 0% will be scheduled this time
c [block-4] scheduled 13 variables 0%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] incomplete 1 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 [bca-3] limit of 10000000 steps and 694442 added (scaled 2)
c [bca-3] 1149 out of 6566 literals actually usable 17%
c [bca-3] added 0 blocked clauses in 37219 steps
c [sweep-4] limit 1219679 penalty 0 = 0 + 0
c [sweep-4-1] 1162 pos 42.2% + 1589 neg 57.8% = 2751 sched 83.8% ret 531
c [sweep-4-1] 1290867 steps 19 queries 639.16 avg class size
c [sweep-4-1] 834 decisions 18 SAT calls 54.61 avg env size
c [sweep-4-1] 2682 variables remain 82% (600 retained 18%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 18 queries)
c [sort-queue-8] sorted 3282 enqueued variables after 40576 conflicts
c [score-dist-8] active 0 (0%), one 3262 (99%), zero 20 (1%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 3 variables 0.1% (3282 remain 2%)
c [simplification-8] removed 127 irredundant clauses 0.0% (346832 remain 26%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 26666
c [simplification-8] new conflict interval 53332
c [simplification-8] penalized conflict interval 53332 = 1 * 53332
c [simplification-8] hard conflict limit 120574 (soft 93908 + delta 26666)
c [simplification-8] new conflict limit 93908 (hard 120574)
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 -   60.7    3282   342108     74208   20043   2583  2914    9    96   48   9%    664   42    9    5  170%
c 
c [simplification-9] limit of 338 binary hit after 338 binaries
c [quatres-5] found 3595 quaternary clauses 1% in total
c [quatres-5-1] added 2 double-self-subsuming ternary resolvents
c [quatres-5-2] added 120 single-self-subsuming ternary resolvents
c [quatres-5-2] added 14 quaternary resolvents
c [ternres-5] limit 7630845 with penalty 0 = 0 + 0
c [ternres-5] all 3282 free variables schedulable
c [ternres-5] 283 ternary resolvents (33 bin, 250 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-18] removed 3 variables
c [treelook-3] limit 190771 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 734 literals 11%
c [treelook-3] scheduling used 191627 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 190771 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 377795 steps
c [treelook-3] 729 literals remain 11%
c [treelook-3] 329 variables remain to probed next time 10%
c [treelook-3] removed 0 variables, found 75 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 28 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 3279 variables 100%
c [block-5] limit of 76308455 steps penalty 0 = 0 + 0
c [block-5] incomplete 112 not tried 3%
c [block-5] transition to [ all 1 rem 1 ] state
c [block-5] eliminated 1 blocked clauses
c [block-5] considered successful since not run to completion yet
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 3279 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1526169100 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 39 variables 1% in round 1 in 927422873 steps
c [elim-8-1] backward subsumption/strengthening limit 598746227
c [elim-8-1-1] backward checking 1071 touched variables 33%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 11 and strengthened 10 clauses in 3320291 steps
c [elim-8-1] rescheduled 28 variables 1% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 7080220 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 39 = 1% variables out of 3279 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 22892530 penalty 0 = 0 + 0
c [sweep-5-1] 1177 pos 44.4% + 1471 neg 55.6% = 2648 sched 81.7% ret 592
c [sweep-5-1] 11971042 steps 654 queries 52.97 avg class size
c [sweep-5-1] 14656 decisions 635 SAT calls 28.38 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-20] removed 21 variables
c [sweep-5-1] removed 21 vars (0 failed, 21 eqs, 27 impls)
c [sweep-5-2] 1438 pos 44.7% + 1781 neg 55.3% = 3219 sched 100.0% ret 0
c [sweep-5-2] 10924704 steps 366 queries 138.51 avg class size
c [sweep-5-2] 11189 decisions 369 SAT calls 34.05 avg env size
c [sweep-5-2] 860 variables remain 27% (2359 retained 73%)
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 9 impls)
c [sweep-5] removed 21 vars in TOTAL (2 rounds, 1018 queries)
c [sort-queue-9] sorted 3219 enqueued variables after 74225 conflicts
c [score-dist-9] active 0 (0%), one 3219 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 63 variables 1.9% (3219 remain 2%)
c [simplification-9] removed 46890 irredundant clauses 13.7% (295217 remain 22%)
c [simplification-9] maximum reduction of 14% = max (2%, 14%)
c [simplification-9] forced so keeping old conflict interval 53332
c [simplification-9] conflict limit remains at 93908 (hard 120574)
c [simplification-9] new binary interval 1000
c 
c [simplification-10] limit 93908 conflicts (hard 120574) hit after 93909 conflicts
c [quatres-6] found 3775 quaternary clauses 1% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 79 single-self-subsuming ternary resolvents
c [quatres-6-2] added 48 quaternary resolvents
c [ternres-6] limit 9529478 with penalty 0 = 0 + 0
c [ternres-6] all 3219 free variables schedulable
c [ternres-6] 317 ternary resolvents (27 bin, 290 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 595592 penalty 3 = 3 + 0
c [card-4] found 13 at-most-one constraints of average size 5.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 595592 for elimination
c [card-4] 13 out of 13 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 4037 xors of average arity 3.0
c [gauss-3] connected 12107 occurrences of 958 variables (average 12.6)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 1 variables
c [basicprobe-3] limit 47647394 penalty 0 = 0 + 0
c [basicprobe-3-0] 304 sched 9%, 1 failed, 0 lifted, 193 hbrs
c [decomp-23] removed 2 variables
c [basicprobe-3-1] 642 sched 20%, 1 failed, 0 lifted, 429 hbrs
c [decomp-24] removed 1 variables
c [basicprobe-3-2] 612 sched 19%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-3-3] 612 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-3] fully completed probing
c [basicprobe-3-3] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-3] removed 3 variables, found 634 hbrs
c [bate-2] eliminated 33 asymmetric tautologies during probing
c [unhide-7] limit 476473 with penalty 2 = 2 + 0
c [unhide-7-7] 0 units, 0 failed, 342 tauts, 0 hbrs, 685 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 217 transitive binary clauses
c [block-6] 1 variables 0% will be scheduled this time
c [block-6] scheduled 1 variables 0%
c [block-6] limit of 95294789 steps penalty 0 = 0 + 0
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 11911848 steps penalty 2 = 2 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 5957427 steps for small clauses
c [cce-3-1] scheduling 4449 clauses = 3473 binary + 976 ternary
c [cce-3-1] tried to eliminate 257 small clauses 6%
c [cce-3-1] eliminated 41 binary clauses 1%
c [cce-3-1] eliminated 10 ternary clauses 1%
c [cce-3-1] eliminated 51 small clauses 1%
c [cce-3-1] eliminated 51 small clauses in 11911853 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 51 covered clauses in round 1
c [cce-3] eliminated 51 covered clauses in TOTAL during 1 rounds
c [cce-3] 51 < 1/100 * 293023 = 2930 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 3215 variables 100%
c [elim-9] limit of 190589579 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 597 not tried 19% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 13 = 0% variables out of 3215 scheduled
c [elim-9] 13 < 1/100 * 3215 = 32 considered unsuccessful
c [sweep-6] limit 2858843 penalty 0 = 0 + 0
c [sweep-6-1] 349 pos 40.9% + 505 neg 59.1% = 854 sched 26.7% ret 2348
c [sweep-6-1] 2924063 steps 120 queries 67.98 avg class size
c [sweep-6-1] 3670 decisions 119 SAT calls 39.19 avg env size
c [sweep-6-1] 530 variables remain 17% (2672 retained 83%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 119 queries)
c [sort-queue-10] sorted 3202 enqueued variables after 93909 conflicts
c [score-dist-10] active 0 (0%), one 3202 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 17 variables 0.5% (3202 remain 2%)
c [simplification-10] removed 680 irredundant clauses 0.2% (292474 remain 22%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 26666 = 53332 / 2
c [simplification-10] new conflict interval 79998
c [simplification-10] penalized conflict interval 79998 = 1 * 79998
c [simplification-10] hard conflict limit 213906 (soft 173907 + delta 39999)
c [simplification-10] new conflict limit 173907 (hard 213906)
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 -   91.3    3202   290229    113801   27470   2181  3924    8    95   44   8%    827   25    9    6  136%
c -   98.2    3202   286112    162329   35580   2298  4074    8    84   45   9%    930    6    8    7  114%
c 
c [simplification-11] limit 173907 conflicts (hard 213906) hit after 173908 conflicts
c [quatres-7] found 3850 quaternary clauses 1% in total
c [quatres-7-2] added 89 single-self-subsuming ternary resolvents
c [quatres-7-2] added 38 quaternary resolvents
c [ternres-7] limit 15376805 with penalty 0 = 0 + 0
c [ternres-7] all 3202 free variables schedulable
c [ternres-7] 321 ternary resolvents (20 bin, 301 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 15 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 136 transitive binary clauses
c [bca-4] limit of 10000000 steps and 571122 added (scaled 2)
c [bca-4] 1095 out of 6376 literals actually usable 17%
c [bca-4] added 0 blocked clauses in 49214 steps
c [sort-queue-11] sorted 3187 enqueued variables after 173908 conflicts
c [score-dist-11] active 0 (0%), one 3187 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 15 variables 0.5% (3187 remain 2%)
c [simplification-11] removed 3 irredundant clauses 0.0% (285281 remain 21%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 79998
c [simplification-11] new conflict interval 159996
c [simplification-11] penalized conflict interval 159996 = 1 * 159996
c [simplification-11] hard conflict limit 413902 (soft 333904 + delta 79998)
c [simplification-11] new conflict limit 333904 (hard 413902)
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 -  104.9    3187   282787    212815   44470   2652  4041    7   127   61   6%    981   37    7    7   94%
c -  111.4    3187   279870    262126   53884   2762  4183    7    79   46   9%   1004   -9    8    7  114%
c -  119.2    3187   277576    312806   61118   2921  4322    7    80   46   9%   1015  -13    5    7   68%
c 
c [simplification-12] limit 333904 conflicts (hard 413902) hit after 345965 conflicts
c [quatres-8] found 4306 quaternary clauses 1% in total
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 136 single-self-subsuming ternary resolvents
c [quatres-8-2] added 36 quaternary resolvents
c [ternres-8] limit 25662861 with penalty 0 = 0 + 0
c [ternres-8] all 3187 free variables schedulable
c [ternres-8] 203 ternary resolvents (23 bin, 180 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 51 variables
c [simpleprobe-4] 1277 schedulable variables 41%
c [simpleprobe-4] limit 51325722 penalty 1 = 1 + 0
c [decomp-29] removed 1 variables
c [simpleprobe-4] 1198 variables remain 38% (1937 retained 62%)
c [simpleprobe-4] removed 1 variables, found 138 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 141 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 3135 variables 100%
c [block-7] limit of 128314305 steps penalty 1 = 1 + 0
c [block-7] incomplete 43 not tried 1%
c [block-7] transition to [ all 1 rem 1 ] state
c [block-7] eliminated 0 blocked clauses
c [elim-10] 556 variables 18% will be scheduled this time
c [elim-10] scheduled 556 variables 18%
c [elim-10] limit of 256628610 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 253 not tried 8% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 0 = 0% variables out of 556 scheduled
c [sweep-7] limit 3849429 penalty 1 = 1 + 0
c [sweep-7-1] 206 pos 39.0% + 322 neg 61.0% = 528 sched 16.8% ret 2607
c [sweep-7-1] 3909219 steps 98 queries 45.22 avg class size
c [sweep-7-1] 3743 decisions 97 SAT calls 50.70 avg env size
c [sweep-7-1] 260 variables remain 8% (2875 retained 92%)
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-7] removed 0 vars in TOTAL (1 rounds, 97 queries)
c [sort-queue-12] sorted 3135 enqueued variables after 345965 conflicts
c [score-dist-12] active 0 (0%), one 3135 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 52 variables 1.6% (3135 remain 2%)
c [simplification-12] removed 160 irredundant clauses 0.1% (275801 remain 20%)
c [simplification-12] maximum reduction of 2% = max (2%, 0%)
c [simplification-12] geometric conflict interval increment 53332 = 159996 / 3
c [simplification-12] new conflict interval 213328
c [simplification-12] penalized conflict interval 213328 = 1 * 213328
c [simplification-12] hard conflict limit 665957 (soft 559293 + delta 106664)
c [simplification-12] new conflict limit 559293 (hard 665957)
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 -  137.7    3135   274748    368391   67255   3059  4379    7    97   63   8%   1020    6    8    7  114%
c -  144.4    3135   273013    417550   74850   3200  4537    7   155   64   5%   1022   48    9    7  122%
c -  153.1    3135   270658    472802   84220   3444  4728    7    93   65   8%   1023   -5    8    7  112%
c -  161.5    3135   268873    528770   95129   3696  4886    7    63   65  10%   1024  -27    6    7   89%
c 
c [simplification-13] limit 559293 conflicts (hard 665957) hit after 559293 conflicts
c [quatres-9] found 5026 quaternary clauses 2% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-1] added 6 double-self-subsuming ternary resolvents
c [quatres-9-2] added 238 single-self-subsuming ternary resolvents
c [quatres-9-2] added 74 quaternary resolvents
c [ternres-9] limit 39169364 with penalty 0 = 0 + 0
c [ternres-9] all 3135 free variables schedulable
c [ternres-9] 429 ternary resolvents (31 bin, 398 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-31] removed 96 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 145 transitive binary clauses
c [sort-queue-13] sorted 3039 enqueued variables after 559293 conflicts
c [score-dist-13] active 0 (0%), one 3039 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 96 variables 3.1% (3039 remain 2%)
c [simplification-13] removed 17 irredundant clauses 0.0% (268156 remain 20%)
c [simplification-13] maximum reduction of 3% = max (3%, 0%)
c [simplification-13] geometric conflict interval increment 53332 = 213328 / 4
c [simplification-13] new conflict interval 266660
c [simplification-13] penalized conflict interval 266660 = 1 * 266660
c [simplification-13] hard conflict limit 959283 (soft 825953 + delta 133330)
c [simplification-13] new conflict limit 825953 (hard 959283)
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 -  170.6    3039   267434    587188   96342   3753  4549    7    66   66  11%   1024  -24    8    7  108%
c i  175.9    3038   266422    622331  122825   3953  4666    7    90   71   8%   1024   -2    4    7   60%
c -  179.1    3032   265974    643390  105182   4048  4757    7   137   66   5%  -6085   43    8    7  110%
c -  188.2    3032   264869    699351  113726   4324  4950    7    91   68   8%  -2003   -4    8    7  108%
c -  197.8    3032   264011    759950  123635   4576  5142    7    66   50  10%   -177  -31    5    7   68%
c i  197.8    3031   264011    760023  123675   4581  5146    7    65   55  10%   -175  -32    5    7   64%
c i  203.2    3024   263657    795542  150771   4715  5243    7   135   76   6%   -945   28    5    7   72%
c -  206.4    3018   263434    816759  132043   4763  5289    7    78   51   9%   -808  -32    9    7  128%
c i  208.2    3017   263190    827985  140045   4805  5327    7   102   76   6%   -520   -5    5    7   73%
c i  214.2    3010   262897    862759  167113   4953  5423    7    95   78   8%   -187   -9    6    7   80%
c -  215.9    3010   262798    872900  138336   4980  5437    8    94   52   9%   -486  -11    9    7  125%
c 
c [simplification-14] limit 825953 conflicts (hard 959283) hit after 898362 conflicts
c [quatres-10] found 6250 quaternary clauses 2% in total
c [quatres-10-1] removed 7 duplicate quaternary clauses
c [quatres-10-1] added 6 double-self-subsuming ternary resolvents
c [quatres-10-2] added 394 single-self-subsuming ternary resolvents
c [quatres-10-2] added 114 quaternary resolvents
c [ternres-10] limit 62654702 with penalty 0 = 0 + 0
c [ternres-10] all 3010 free variables schedulable
c [ternres-10] 486 ternary resolvents (51 bin, 435 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1566367 penalty 3 = 3 + 0
c [gauss-4] extracted 6997 xors of average arity 2.9
c [gauss-4] connected 20075 occurrences of 1433 variables (average 14.0)
c [gauss-4] limit 1566367 penalty 3 = 3 + 0
c [gauss-4] connected 2738 occurrences of 1433 variables (average 1.9)
c [gauss-4] fully completed
c [decomp-32] removed 234 variables
c [gauss-4] exported 0 unary, 1 binary and 36 ternary equations
c [unhide-8] limit 1566367 with penalty 3 = 3 + 0
c [unhide-8-8] 0 units, 0 failed, 4170 tauts, 0 hbrs, 12011 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 136 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 391591888 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 977 clauses out of 133208 (1%) of length 9
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 977 large clauses in 391592386 steps
c [cce-4-1] allowing another 195796193 steps for small clauses
c [cce-4-1] scheduling 4958 clauses = 3417 binary + 1541 ternary
c [cce-4-1] tried to eliminate 4958 small clauses 100%
c [cce-4-1] eliminated 192 binary clauses 6%
c [cce-4-1] eliminated 178 ternary clauses 12%
c [cce-4-1] eliminated 370 small clauses 7%
c [cce-4-1] eliminated 370 small clauses in 267270723 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 1347 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 62161149 steps for small clauses
c [cce-4-2] scheduling 4588 clauses = 3225 binary + 1363 ternary
c [cce-4-2] tried to eliminate 4304 small clauses 94%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 1347 covered clauses in TOTAL during 2 rounds
c [cce-4] 1347 < 1/100 * 259907 = 2599 considered unsuccessful
c [sort-queue-14] sorted 2776 enqueued variables after 898362 conflicts
c [score-dist-14] active 0 (0%), one 2776 (100%), zero 0 (0%)
c [score-dist-14] max exp 1, different 1 (50%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 234 variables 7.8% (2776 remain 2%)
c [simplification-14] removed 4107 irredundant clauses 1.6% (258560 remain 19%)
c [simplification-14] maximum reduction of 8% = max (8%, 2%)
c [simplification-14] large reduction 8% >= 5% limit
c [simplification-14] next conflict interval 8983 = min (898362/100, 266660)
c [simplification-14] penalized conflict interval 8983 = 1 * 8983
c [simplification-14] hard conflict limit 917345 (soft 907345 + delta 10000)
c [simplification-14] new conflict limit 907345 (hard 917345)
c 
c [simplification-15] limit 907345 conflicts (hard 917345) hit after 907345 conflicts
c [quatres-11] found 4644 quaternary clauses 1% in total
c [quatres-11-1] removed 9 duplicate quaternary clauses
c [quatres-11-1] added 5 double-self-subsuming ternary resolvents
c [quatres-11-2] added 69 single-self-subsuming ternary resolvents
c [quatres-11-2] added 73 quaternary resolvents
c [ternres-11] limit 63153430 with penalty 0 = 0 + 0
c [ternres-11] all 2776 free variables schedulable
c [ternres-11] 449 ternary resolvents (64 bin, 385 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1973544 penalty 4 = 4 + 0
c [card-5] found 65 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1973544 for elimination
c [card-5] 65 out of 65 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 7 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 84 transitive binary clauses
c [block-8] 43 variables 2% will be scheduled this time
c [block-8] scheduled 43 variables 2%
c [block-8] limit of 157883576 steps penalty 2 = 2 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 0 blocked clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 2769 variables 100%
c [elim-11] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 478 not tried 17% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 241 = 9% variables out of 2769 scheduled
c [bca-5] limit of 10000000 steps and 505140 added (scaled 2)
c [bca-5] 517 out of 5058 literals actually usable 10%
c [bca-5] added 0 blocked clauses in 137300 steps
c [sweep-8] limit 4736507 penalty 2 = 2 + 0
c [sweep-8-1] 82 pos 39.6% + 125 neg 60.4% = 207 sched 8.2% ret 2321
c [sweep-8-1] 4209691 steps 121 queries 15.49 avg class size
c [sweep-8-1] 3381 decisions 119 SAT calls 37.34 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-35] removed 3 variables
c [sweep-8-1] removed 3 vars (0 failed, 1 eqs, 3 impls)
c [sweep-8-2] 1060 pos 42.0% + 1465 neg 58.0% = 2525 sched 100.0% ret 0
c [sweep-8-2] 583207 steps 8 queries 882.88 avg class size
c [sweep-8-2] 344 decisions 7 SAT calls 87.43 avg env size
c [sweep-8-2] 2506 variables remain 99% (19 retained 1%)
c [decomp-36] removed 2 variables
c [sweep-8-2] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 5 vars in TOTAL (2 rounds, 127 queries)
c [sort-queue-15] sorted 2523 enqueued variables after 907345 conflicts
c [score-dist-15] active 0 (0%), one 2523 (100%), zero 0 (0%)
c [score-dist-15] max exp 1, different 1 (50%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 253 variables 9.1% (2523 remain 1%)
c [simplification-15] removed 6279 irredundant clauses 2.4% (252254 remain 19%)
c [simplification-15] maximum reduction of 9% = max (9%, 2%)
c [simplification-15] large reduction 9% >= 5% limit
c [simplification-15] next conflict interval 9073 = min (907345/100, 266660)
c [simplification-15] penalized conflict interval 9073 = 1 * 9073
c [simplification-15] hard conflict limit 926418 (soft 916418 + delta 10000)
c [simplification-15] new conflict limit 916418 (hard 926418)
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  232.5    2522   252225    911227  138599   3354  4257    7    95   56   8%    183  -19    4    7   59%
c i  232.9    2515   252203    914617  141245   3367  4260    8   118   73   6%   -478    3    8    7  110%
c i  233.7    2514   252178    919018  144527   3406  4288    8    95   73   8%   -455  -19    6    7   82%
c i  234.1    2507   252163    923010  147293   3434  4299    7   129   56   5%   -433   15    4    7   59%
c i  234.4    2500   252140    925506  148956   3456  4305    7   126   56   6%   -436   11    6    7   78%
c 
c [simplification-16] limit 916418 conflicts (hard 926418) hit after 926418 conflicts
c [quatres-12] found 5344 quaternary clauses 2% in total
c [quatres-12-1] removed 23 duplicate quaternary clauses
c [quatres-12-1] added 1 double-self-subsuming ternary resolvents
c [quatres-12-2] added 58 single-self-subsuming ternary resolvents
c [quatres-12-2] added 119 quaternary resolvents
c [ternres-12] limit 64268061 with penalty 0 = 0 + 0
c [ternres-12] all 2494 free variables schedulable
c [ternres-12] 33 ternary resolvents (20 bin, 13 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-5] limit 3213403 penalty 2 = 2 + 0
c [gauss-5] extracted 4261 xors of average arity 3.3
c [gauss-5] connected 14180 occurrences of 1087 variables (average 13.0)
c [gauss-5] limit 3213403 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-37] removed 19 variables
c [treelook-4] limit 803350 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 1660 literals 34%
c [treelook-4] scheduling used 708572 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 803350 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 854492 steps
c [treelook-4] 1651 literals remain 33%
c [treelook-4] 231 variables remain to probed next time 9%
c [treelook-4] removed 0 variables, found 114 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 139 transitive binary clauses
c [sort-queue-16] sorted 2475 enqueued variables after 926418 conflicts
c [score-dist-16] active 0 (0%), one 2475 (100%), zero 0 (0%)
c [score-dist-16] max exp 1, different 1 (50%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 19 variables 0.8% (2475 remain 1%)
c [simplification-16] removed 2584 irredundant clauses 1.0% (249556 remain 18%)
c [simplification-16] maximum reduction of 1% = max (1%, 1%)
c [simplification-16] geometric conflict interval increment 133330 = 266660 / 2
c [simplification-16] new conflict interval 399990
c [simplification-16] penalized conflict interval 399990 = 1 * 399990
c [simplification-16] hard conflict limit 1526403 (soft 1326408 + delta 199995)
c [simplification-16] new conflict limit 1326408 (hard 1526403)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  236.2    2474   249549    931748  141852   3371  4172    7    66   56  10%   -344  -49    5    7   62%
c i  237.9    2467   249495    946037  151539   3444  4206    6    81   56   8%   -156  -26    5    7   65%
c i  238.5    2460   249472    949922  154337   3490  4221    6    74   73   9%   -297  -32    4    7   59%
c -  240.0    2454   249414    960959  126528   3518  4239    7    64   66  10%   -148  -35    8    7  115%
c i  241.5    2453   249360    973999  136627   3565  4265    7    35   72  21%     63  -55    7    7   97%
c i  243.2    2445   249340    989597  147915   3607  4277    6    11   72  57%    -35  -66    5    7   70%
c i  243.3    2444   249340    990641  148458   3623  4286    6    10   72  60%   -172  -66    5    7   67%
c i  243.4    2443   249340    991430  149008   3639  4290    6    10   72  61%   -213  -65    5    7   69%
c i  243.4    2442   249340    991695  149123   3653  4298    6     9   72  61%   -222  -65    4    7   63%
c i  243.4    2439   249339    991806  149139   3665  4303    6     9   72  62%   -225  -65    4    7   59%
c i  243.4    2438   249339    991863  149137   3673  4306    6     9   72  62%   -227  -65    4    7   57%
c i  243.4    2433   249339    991883  149135   3674  4306    6     9   72  62%   -227  -65    4    7   56%
c i  243.4    2431   249339    991889  149133   3674  4306    6     9   72  62%   -228  -65    4    7   56%
c 0  243.4    2430   249339    991889  149133   3674  4306    6     9   72  62%   -228  -65    4    7   56%
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 
s UNSATISFIABLE
c
c bate: 304 basic ate = 204 trn 67% + 100 lrg 33% in 2 updates
c bcas: 5 count, 120 added (2 skipped), 300009 steps
c bkwd: tried 33687 clauses, 67049 lits, 1.99 lits/clause
c bkwd: checked 38497139 occs, 1142.79 occs/clause, 574.16 occs/lit
c bkwd: subsumed 0 binary, 24 ternary, 74 large
c bkwd: strengthened 4 binary, 9 ternary (100% self), 294 large (0% self)
c blkd: 8 bces, 33732 removed, 869910876 resolutions, 908930929 steps
c blkd: 8686 blocking literals 2%, 4803 pure
c bump: 920925 bumped seen, 22352001 lits 24.3 on average
c card: 5 count, 0 units, 0 am1, 10791417 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 178 subsumed
c card: 94 at-most-one constraints found, average size 3.86
c card: 94 at-most-one constraints used 100%, average size 3.86
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, 1753 eliminated, 1752 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: 5929527 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 77 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 38 decompositions, 39260 equivalent 14%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 4469742 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 11 elims, 105735 eliminated 38%, 736 pure 1%
c elms: 15 rounds, 1.4 rounds/bve
c elms: 64766 small 61%, 35430 large 34%
c elms: 69840 tried small, 64766 succeeded 93%, 5074 failed 7%
c elms: 2389 subsumed, 98046 strengthened, 28 blocked
c elms: 4576555 copies, 29209591 resolutions, 1042983 ipos
c elms: 1363769 subchks, 968479 strchks
c gaus: 5 extractions, 71054 extracted, 2.9 size, 4 max
c gaus: exported 0 units, 1 binary and 36 ternary equations
c gaus: 2 gc, 16560656 steps, 8280328 extr 50%, 3707223 elim 22%
c glue: 7.3 orig avg, 7.3 real avg, 1.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 30382 = 21754 simple 72% + 8500 trn 28% + 128 lrg 0%, 561 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 920925 clauses, 13.3 length
c lrnd: 12213840 lits = 13326496 orig - 1112656 removed 8%
c lrnd: 41346 uips 4%, 851233 flips 92%
c mins: 879919 mins 96%, 1724 bin 0%, 39282 size 4%
c mins: 7971376 poisoned searches, 786688 hits, 10% hit rate
c mins: 19251885 used twice searches, 3834671 hits, 20% hit rate
c move: moved 23490, 784 bin 3%, 22706 trn 97%
c otfs: 90311 driving 40%, 135220 restarting 60%
c otfs: str 225531, 167309 red 74%, 58222 irr 26%
c otfs: str 225531, 0 bin 0%, 989 trn 0%, 224542 lrg 100%
c otfs: sub 54420, 7453 red 14%, 46967 irr 86%
c otfs: sub 54420, 0 bin 0%, 426 trn 1%, 53994 lrg 99%
c phas: 3 computed, 83341 set, 0 pos (0%), 83341 neg (100%)
c prbs: 3 basic, 8571 probed, 77 failed, 1 lifted
c prbs: 4 simple, 195090 probed, 100 failed, 1038 eqs
c prbs: 4 treelook, 55 probed, 0 failed, 0 lifted
c prom: 158514 locked 27% out of 579257 tried
c prps: 65199042 props, 14 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 12 count, 945 quat, 1712 self1, 23 self2, 106 dup
c queu: 16 sorted, 4469742 next (89 steps 0.00)
c queu: 22825839 enq (0 steps 0.00), 22352001 deq 98%
c redc: 9279 clauses 2%, 465049 tried 47%, 6 sat 0%
c redc: 10725 lits 0%, 4545669 tried 34%, 6 sat 0%
c redc: 321 times jump level reduced, 5.1 levels on average
c reds: 17 count, 58346.4 conflicts per reduce
c reds: 0 memlim 0%, 17 arith 100%
c reds: 493016 collected 88%, 65991 retired 12%
c rmbd: 3144 removed, 928 red 30%
c rsts: 30387 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 16 count, 14 confs 88%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 920925 count (278136 tried 0.3), 137510 sub out of 915099 (15.0%)
c swps: 8 count, 10 rounds, 1527 queries (152.7/round)
c swps: 1508 sat calls, 7 unsat (12.8% success rate)
c swps: 41106 decisions 27.3, 19347 conflicts 12.8
c swps; 135.2 avg class size, 33.2 avg environment size
c swps: 0 failed, 53 impls, 26 equivs
c swp0: 505 type 0 queries, 23 unsat (4.6%), 500 sat (99.0%)
c swp1: 1022 type 1 queries, 101 unsat (9.9%), 1001 sat (97.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: 10781697 calls to obtain time
c tops: 129470 fixed 46%, 83 its, 11950.47 confs/it
c trds: 12 transitive reductions, 1504 removed, 0 failed
c trds: 81457 nodes, 75557 edges, 2617240 steps
c trim: 785556 words, 3.0 MB
c trnr: 12 count, 5419 bin, 44254 trn, 53791401 steps
c unhd: 8 count, 8 rounds, 23015020 steps
c unhd: 1631 non-trivial sccs of average size 2.0
c unhd: 86 units, 29 bin, 57 trn, 0 lrg
c unhd: 668 failed, 659 stamp, 0 lits, 0 bin, 8 trn, 0 lrg
c unhd: 9218 tauts, 63 bin 1%, 4156 trn 45%, 3782 lrg 41%
c unhd: 9218 tauts, 1217 stamp 13%, 6223 red 68%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 21139 str, 29 bin 0%, 4032 trn 19%, 17078 lrg 81%, 12827 red 61%
c vars: 4654 remaining 2% and 274465 removed 98% out of 279119
c vars: 129470 fixed 46%, 105735 eliminated 38%, 39260 equivalent 14%
c vsts: 6805075691 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 104.7 search visits per propagation, 6810.0 per conflict
c wchs: 3717625573 pushed, 9512220 enlarged, 199 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         916044        493016         65991       5787482       2772877        373422
c 
c  0 0        183041  20      7852   2         0   0   2809082  49    997541  36    106633  29     4.6
c  1 5        136977  15     81127  16     11457  17    890101  15<   453047  16<    54685  15     0.8
c  2 6        364954  40<   248122  50<    29558  45<  1706954  29    935633  34    135826  36<    1.9
c  3 9        165228  18    111851  23     14987  23    280446   5    288933  10     55182  15     1.0
c  4 14        52521   6     35607   7      7375  11     79613   1     80118   3     17304   5     0.4
c  5 21        11297   1      7281   1      2127   3     18377   0     15322   1      3358   1     0.1
c  6 30         1638   0       957   0       401   1      2339   0      1847   0       351   0     0.0
c  7 41          220   0       127   0        56   0       311   0       225   0        38   0     0.0
c  8 54          105   0        61   0        16   0       180   0       146   0        32   0     0.0
c  9 69           40   0        21   0        10   0        49   0        43   0         8   0     0.0
c 10 86           19   0        10   0         2   0        24   0        20   0         5   0     0.0
c 11 126           4   0         0   0         2   0         6   0         2   0         0   0     0.0
c 
c avg                  1.8           2.2           2.4           1.0           1.3           1.6
c std                  1.2           0.9           1.1           1.1           1.2           1.2
c 
c   37.678  15% block
c   32.561  13% elim
c    5.754   2% cce
c    4.444   2% probe
c    2.731   1% sweep
c    2.600   1% decide
c    1.849   1% unhide
c    1.534   1% gauss
c 
c    3.519 < 1% rest (below)
c 
c    1.200   0% bump
c    0.816   0% bca
c    0.556   0% transred
c    0.471   0% quatres
c    0.361   0% ternres
c    0.115   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.293   2% preprocessing     5%
c   90.382  37% inprocessing     95%
c ==================================
c   94.675  39% simplifying
c  148.746  61% search
c ==================================
c  243.426 100% all
c 
c        991889 conflicts,        4074.7 confs/sec
c          3442 ternaries,         288.2 confs/ternary
c          2165 binaries,          458.1 confs/binary
c            83 iterations,      11950.5 confs/iteration
c 
c            17 reductions,          0.1 redus/sec,  58346.4 confs/reduction
c         30387 restarts,          124.8 rests/sec,     32.6 confs/restart
c       4469742 decisions,       18361.8 decis/sec,      4.5 decis/conflict
c      65199042 propagations,   267839.4 props/sec,     14.6 props/decision
c 
c 243.4 seconds, 148.3 MB
c launch: done
