c launch: /data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2
c host: atom07
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/UTI-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 260342 1391257' header
c read 260342 variables, 1391257 clauses, 3358569 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=3
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 247193 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] SUM (--score=3)
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  247193  1377238         0       0      0     0    0     0   58   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] found 6497 at-most-one constraints of average size 5.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6497 out of 6497 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62800 variables
c [simpleprobe-1] all 197542 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 1569 variables
c [simpleprobe-1] 20928 variables remain 11% (175045 retained 89%)
c [simpleprobe-1] removed 1569 variables, found 21725 hbrs, 357 units
c [unhide-1] limit 65541 based on 1048664 irredundant clauses
c [unhide-1-1] 0 units, 4657 failed, 11362 tauts, 0 hbrs, 11424 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 194552 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 60670 not tried 31% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74772 = 38% variables out of 194552 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 866695 negative 99.3% of 873213 except 6518 0.7%
c [phase-count-1] 702151 positive 80.4% of 873213 except 171062 19.6%
c [phase-count-1] less non-negative clauses 6518 than limit 87300 (10.0%)
c [phase-count-1] non-pos/non-neg = 171062/6518 = 26.24 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119780 negative 100%
c [sort-queue-1] sorted 119780 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119780 (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 83984 variables 41.2% (119780 remain 48%)
c [simplification-1] removed 504025 irredundant clauses 36.6% (873213 remain 63%)
c [simplification-1] maximum reduction of 41% = max (41%, 37%)
c [simplification-1] large reduction 41% >= 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    5.1  119779   873213        22      10      2 15335    0     2   57   0%      0    2    0    0 24705%
c i    5.1  119691   873213        36      12      6 15341    0     2   57   1%      0    2    0    0 23899%
c i    5.2  119655   873213        46      16     10 15342    0     2   57   1%      0    2    0    0 23560%
c i    5.2  119539   873213        50      19     10 15342    0     3   58   1%      0    3    0    0 23445%
c i    5.2  119186   873213        66      33     10 15343    0     4   58   3%      0    4    2    0 24423%
c i    5.2  118929   873213        67      33     10 15343    0     4   58   3%      0    4    2    0 24328%
c i    5.4  118919   873213       191     141     19 15345    1     7   59   9%      0    7    8    0 18462%
c i    5.4  118907   873213       194     142     20 15345    1     7   59   9%      0    7    8    0 18263%
c i    5.4  118896   873213       196     142     20 15346    1     7   59   9%      0    7    8    0 18124%
c i    5.6  118888   873213       302     221     34 15352    1    17   59   5%      0   17    8    0 13978%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 913 variables
c [simpleprobe-2] 19448 schedulable variables 16%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 259 variables
c [simpleprobe-2] 22189 variables remain 19% (96419 retained 81%)
c [simpleprobe-2] removed 259 variables, found 4312 hbrs, 102 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 65215 literals 27%
c [treelook-1] scheduling used 503577 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 303541 steps
c [treelook-1] 65178 literals remain 27%
c [treelook-1] 64499 variables remain to probed next time 54%
c [treelook-1] removed 33 variables, found 1398 hbrs
c [basicprobe-1] limit 6867440 based on 858430 irredundant clauses
c [basicprobe-1-0] 44123 probes remain 39% after last round
c [basicprobe-1-0] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5013 variables, found 19182 hbrs
c [unhide-2] limit 53651 based on 858430 irredundant clauses
c [unhide-2-2] 2 units, 2160 failed, 4852 tauts, 0 hbrs, 1372 literals
c [elim-2] 58145 variables 52% will be scheduled this time
c [elim-2] scheduled 58145 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 23429 not tried 21% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 38 = 0% variables out of 58145 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 790894 negative 99.2% of 797406 except 6512 0.8%
c [phase-count-2] 637724 positive 80.0% of 797406 except 159682 20.0%
c [phase-count-2] less non-negative clauses 6512 than limit 79700 (10.0%)
c [phase-count-2] non-pos/non-neg = 159682/6512 = 24.52 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 13670 negative 100%
c [sort-queue-2] sorted 102191 enqueued variables after 302 conflicts
c [score-dist-2] active 9673 (9%), one 0 (0%), zero 102191 (91%)
c [score-dist-2] max exp 514, different 14 (3%)
c [score-dist-2] median active exp 510, avg 509.9
c [simplification-2] removed 7016 variables 5.9% (111864 remain 45%)
c [simplification-2] removed 75807 irredundant clauses 8.7% (797406 remain 58%)
c [simplification-2] maximum reduction of 9% = max (6%, 9%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1021 (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    9.0  111863   797406       354     255     41 31994    1    19   54   5%      0   19    7    0 12449%
c i    9.2  111856   797406       484     348     61 32007    1    26   55   5%      0   26   10    0 11720%
c i    9.5  111792   797406       667     483     73 32035    2    37   55   4%      0   37    9    0 8433%
c i    9.5  111583   797406       673     488     73 32035    2    37   55   5%      0   37   10    0 8694%
c 
c [simplification-3] limit 1022 conflicts (hard 11000) hit after 1023 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3776 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3776 out of 3776 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 419 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 58320 literals 26%
c [treelook-2] scheduling used 398265 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 320163 steps
c [treelook-2] 58123 literals remain 26%
c [treelook-2] 44106 variables remain to probed next time 40%
c [decomp-7] removed 20 variables
c [treelook-2] removed 180 variables, found 1034 hbrs
c [unhide-3] limit 50000 with penalty 1 = 0 + 1
c [unhide-3-3] 0 units, 1710 failed, 18564 tauts, 0 hbrs, 1673 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 110125 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 31885 not tried 29% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3112 = 3% variables out of 110125 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 753556 negative 99.1% of 760020 except 6464 0.9%
c [phase-count-3] 606386 positive 79.8% of 760020 except 153634 20.2%
c [phase-count-3] less non-negative clauses 6464 than limit 76000 (10.0%)
c [phase-count-3] non-pos/non-neg = 153634/6464 = 23.77 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 4240 negative 100%
c [sort-queue-3] sorted 80889 enqueued variables after 1023 conflicts
c [score-dist-3] active 26124 (24%), one 0 (0%), zero 80889 (76%)
c [score-dist-3] max exp 517, different 17 (3%)
c [score-dist-3] median active exp 512, avg 511.8
c [simplification-3] removed 4565 variables 4.1% (107013 remain 43%)
c [simplification-3] removed 37386 irredundant clauses 4.7% (760020 remain 55%)
c [simplification-3] maximum reduction of 5% = max (4%, 5%)
c [simplification-3] large reduction 5% >= 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 13023 (soft 3023 + delta 10000)
c [simplification-3] new conflict limit 3023 (hard 13023)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.1  107012   760020      1103     755    138 27997    3    80   54   4%      2   80   17    0 7118%
c i   13.2  107008   760020      1124     761    148 28001    3    82   54   4%      2   82   16    0 6674%
c i   13.3  106855   760020      1152     780    153 28003    4    86   54   4%      1   85   16    0 6277%
c i   14.0  106162   760020      1432    1019    165 28011    6   134   54   4%      2  133   30    0 7531%
c i   14.1  106143   760020      1433    1019    165 28011    6   134   54   4%      2  133   30    0 7501%
c i   14.1  106134   760020      1444    1026    165 28011    6   136   54   4%      2  135   30    0 7416%
c i   14.4  106126   760020      1538    1112    170 28011    6   151   54   4%      2  149   32    0 6978%
c i   14.7  105860   760020      1665    1222    173 28015    8   171   54   5%      1  170   46    1 7745%
c i   14.9  105680   760020      1760    1304    174 28019   10   186   54   5%      1  184   57    1 8036%
c i   15.3  105674   760020      1937    1446    180 28024   14   195   54   7%      1  193   89    1 8964%
c i   16.0  105540   760020      2231    1606    187 28034   26   205   55  13%      2  202  161    2 8817%
c i   16.1  105533   760020      2259    1629    187 28035   27   206   55  13%      2  202  157    2 8357%
c i   16.1  105522   760020      2260    1629    187 28035   27   206   55  13%      2  202  156    2 8325%
c i   16.1  105515   760020      2265    1631    187 28035   27   206   55  13%      2  202  154    2 8207%
c i   16.1  105505   760020      2266    1631    187 28035   27   206   55  13%      2  202  154    2 8175%
c i   16.6  105495   760020      2496    1789    191 28050   33   214   55  15%      2  210  144    2 6114%
c i   17.1  105277   760020      2809    2054    203 28071   35   226   55  16%      2  221   89    3 3333%
c i   17.3  105156   760020      2864    2098    206 28072   36   231   55  16%      2  226   86    3 3142%
c i   17.4  105155   760020      2916    2141    212 28073   36   237   56  15%      2  232   81    3 2929%
c i   17.4  105154   760020      2917    2141    212 28073   36   237   56  15%      2  232   81    3 2917%
c i   17.4  105153   760020      2918    2141    212 28073   36   237   56  15%      2  232   80    3 2906%
c i   17.5  105152   760020      2919    2141    212 28073   36   237   56  15%      2  232   80    3 2895%
c i   17.5  105151   760020      2920    2141    212 28073   36   237   56  15%      2  232   80    3 2884%
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.5  105150   760020      2921    2141    212 28073   36   237   56  15%      2  231   79    3 2872%
c 
c [simplification-4] limit 3105 conflicts (hard 13023) hit after 3105 conflicts
c [decomp-8] removed 1931 variables
c [basicprobe-2] limit 9814064 penalty 0 = 0 + 0
c [basicprobe-2-0] 38014 probes remain 37% after last round
c [basicprobe-2-0] 50 units = 50 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2838 variables, found 31143 hbrs
c [unhide-4] limit 196281 with penalty 1 = 0 + 1
c [unhide-4-4] 0 units, 1689 failed, 5575 tauts, 0 hbrs, 11031 literals
c [elim-4] 22800 variables 23% will be scheduled this time
c [elim-4] scheduled 22800 variables 23%
c [elim-4] boosting limit by 20
c [elim-4] limit of 785125160 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 44191070 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 22800 scheduled
c [phase-count-4] 702321 negative 99.1% of 708787 except 6466 0.9%
c [phase-count-4] 567339 positive 80.0% of 708787 except 141448 20.0%
c [phase-count-4] less non-negative clauses 6466 than limit 70800 (10.0%)
c [phase-count-4] non-pos/non-neg = 141448/6466 = 21.88 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1718 negative 100%
c [sort-queue-4] sorted 61077 enqueued variables after 3105 conflicts
c [score-dist-4] active 39607 (39%), one 0 (0%), zero 61077 (61%)
c [score-dist-4] max exp 522, different 21 (4%)
c [score-dist-4] median active exp 515, avg 514.9
c [simplification-4] removed 4466 variables 4.2% (100684 remain 41%)
c [simplification-4] removed 51233 irredundant clauses 6.7% (708787 remain 51%)
c [simplification-4] maximum reduction of 7% = max (4%, 7%)
c [simplification-4] large reduction 7% >= 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 15105 (soft 5105 + delta 10000)
c [simplification-4] new conflict limit 5105 (hard 15105)
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   20.6  100683   708787      3152    2324    201 48166   41   264   53  16%      2  257  116    3 3635%
c i   20.7  100678   708787      3154    2324    201 48167   41   264   53  16%      2  257  115    3 3607%
c i   20.8  100674   708787      3198    2340    207 48175   43   267   53  16%      2  260  141    3 4167%
c i   20.8  100668   708787      3201    2340    207 48177   43   267   53  16%      2  260  139    3 4119%
c i   20.8  100666   708787      3202    2340    207 48177   43   267   53  16%      2  260  138    3 4102%
c i   20.8  100664   708787      3203    2340    207 48177   43   267   53  16%      2  260  138    3 4087%
c i   20.9  100658   708787      3217    2339    210 48180   44   267   53  17%      2  261  145    3 4234%
c i   20.9  100646   708787      3228    2344    210 48180   45   268   53  17%      2  261  155    3 4431%
c i   21.1  100639   708787      3289    2391    213 48185   46   272   53  17%      2  265  138    4 3863%
c i   21.2  100597   708787      3329    2425    215 48187   45   274   53  17%      1  267  121    4 3381%
c i   21.2  100589   708787      3332    2426    215 48188   45   274   53  17%      1  267  119    4 3342%
c i   21.2  100580   708787      3334    2426    215 48189   45   274   53  17%      1  267  118    4 3316%
c i   21.3  100571   708787      3335    2426    215 48189   45   274   53  17%      1  267  118    4 3303%
c i   21.4  100562   708787      3367    2445    215 48201   45   276   53  16%      1  269  105    4 2929%
c i   22.0  100552   708787      3626    2659    222 48228   43   296   53  15%      2  288   49    4 1348%
c i   22.6  100545   708787      3843    2839    225 48233   48   314   54  15%      2  305  106    4 2626%
c i   22.6  100540   708787      3849    2844    225 48233   48   315   54  15%      2  305  104    4 2581%
c i   23.6  100532   708787      4189    3112    230 48251   59   343   54  17%      2  332  163    5 3268%
c i   23.6  100523   708787      4190    3112    230 48251   59   343   54  17%      2  332  163    5 3256%
c i   23.8  100516   708787      4234    3136    230 48251   62   346   54  18%      2  334  190    5 3643%
c i   24.1  100515   708787      4330    3204    230 48251   66   350   54  19%      2  339  208    6 3732%
c i   24.8  100506   708787      4500    3272    230 48253   79   358   55  22%      2  346  301    7 4599%
c i   24.9  100494   708787      4506    3273    230 48253   79   358   55  22%      2  346  303    7 4599%
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   25.0  100493   708787      4525    3283    230 48254   81   359   55  23%      2  346  313    7 4663%
c i   25.1  100479   708787      4558    3305    230 48257   81   359   55  23%      2  347  287    7 4252%
c 
c [simplification-5] limit of 277 binary hit after 277 binaries
c [quatres-1] found 39465 quaternary clauses 37% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 100476 free variables schedulable
c [ternres-1] 15 ternary resolvents (1 bin, 14 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 75 xors of average arity 2.4
c [gauss-1] connected 177 occurrences of 163 variables (average 1.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 97 variables
c [simpleprobe-3] 19423 schedulable variables 19%
c [simpleprobe-3] limit 13135503 penalty 0 = 0 + 0
c [decomp-10] removed 562 variables
c [simpleprobe-3] 29486 variables remain 30% (70331 retained 70%)
c [simpleprobe-3] removed 562 variables, found 34635 hbrs, 221 units
c [unhide-5] limit 328387 with penalty 1 = 0 + 1
c [unhide-5-5] 1 units, 233 failed, 11123 tauts, 0 hbrs, 10560 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 234 transitive binary clauses
c [transred-1] found 2 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 99502 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 11847 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 15 clauses out of 431 (3%) of length 10
c [cce-1-1] eliminated 138 clauses out of 2520 (5%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 153 large clauses in 30000003 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 550468 clauses = 331313 binary + 219155 ternary
c [cce-1-1] tried to eliminate 308 small clauses 0%
c [cce-1-1] eliminated 62 binary clauses 0%
c [cce-1-1] eliminated 23 ternary clauses 0%
c [cce-1-1] eliminated 85 small clauses 0%
c [cce-1-1] eliminated 85 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 238 covered clauses in round 1
c [cce-1] eliminated 238 covered clauses in TOTAL during 1 rounds
c [cce-1] 238 < 1/100 * 676303 = 6763 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1352630 added (scaled 2)
c [bca-1] 178546 out of 199006 literals actually usable 90%
c [bca-1] added 228 blocked clauses in 543692 steps
c [sweep-1] limit 1352130 based on 676065 irredundant clauses
c [sweep-1-1] 8997 pos 9.0% + 90505 neg 91.0% = 99502 sched 100.0% ret 0
c [sweep-1-1] 1626186 steps 9 queries 30957.89 avg class size
c [sweep-1-1] 37 decisions 4 SAT calls 33.75 avg env size
c [sweep-1-1] 99496 variables remain 100% (6 retained 0%)
c [decomp-11] removed 11 variables
c [sweep-1-1] removed 11 vars (0 failed, 4 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 11 vars in TOTAL (1 rounds, 8 queries)
c [phase-count-5] 669625 negative 99.1% of 676046 except 6421 0.9%
c [phase-count-5] 549492 positive 81.3% of 676046 except 126554 18.7%
c [phase-count-5] less non-negative clauses 6421 than limit 67600 (10.0%)
c [phase-count-5] non-pos/non-neg = 126554/6421 = 19.71 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1282 negative 100%
c [sort-queue-5] sorted 51414 enqueued variables after 4732 conflicts
c [score-dist-5] active 48077 (48%), one 0 (0%), zero 51414 (52%)
c [score-dist-5] max exp 523, different 22 (4%)
c [score-dist-5] median active exp 516, avg 516.5
c [simplification-5] removed 985 variables 1.0% (99491 remain 40%)
c [simplification-5] removed 32741 irredundant clauses 4.6% (676046 remain 49%)
c [simplification-5] maximum reduction of 5% = max (1%, 5%)
c [simplification-5] forced so keeping old conflict interval 0
c [simplification-5] conflict limit remains at 5163 (hard 15105)
c [simplification-5] 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   30.5   99490   676046      4840    3450    277 92323   93   365   55  26%      2  350  282    8 3601%
c i   30.5   99488   676046      4841    3450    277 92323   93   365   55  26%      2  350  281    8 3587%
c i   30.5   99487   676046      4843    3450    277 92324   93   365   55  26%      2  350  279    8 3559%
c i   30.5   99486   676046      4844    3450    277 92324   93   364   55  26%      2  350  278    8 3545%
c i   30.6   99485   676046      4865    3463    277 92326   94   364   55  26%      2  350  270    8 3429%
c i   30.6   99477   676046      4866    3463    277 92326   93   364   55  26%      2  350  269    8 3415%
c i   30.6   99471   676046      4867    3463    277 92326   93   364   55  26%      2  350  268    8 3402%
c i   30.6   99463   676046      4868    3463    277 92326   93   364   55  26%      2  350  267    8 3389%
c i   30.6   99457   676046      4869    3463    277 92326   93   364   55  26%      2  350  266    8 3375%
c i   30.7   99450   676046      4870    3463    277 92326   93   364   55  26%      2  350  265    8 3362%
c i   30.7   99445   676046      4871    3463    277 92326   93   364   55  26%      2  349  264    8 3349%
c i   30.7   99438   676046      4873    3464    277 92326   93   364   55  26%      2  349  262    8 3324%
c i   30.7   99416   676046      4874    3464    277 92326   93   364   55  26%      2  349  261    8 3311%
c i   30.7   99394   676046      4878    3465    277 92326   93   364   55  26%      2  349  259    8 3282%
c i   31.3   99387   676046      5091    3617    278 92347   93   365   55  26%      2  349  158    8 1931%
c i   31.3   99382   676046      5094    3618    278 92348   93   365   55  26%      2  349  156    8 1911%
c i   31.3   99374   676046      5096    3618    278 92349   93   365   55  26%      2  349  155    8 1897%
c i   31.4   99365   676046      5097    3618    278 92349   93   364   55  26%      2  349  154    8 1889%
c i   31.4   99354   676046      5098    3618    278 92349   93   364   55  26%      2  349  154    8 1882%
c i   31.4   99341   676046      5099    3618    278 92349   93   364   55  26%      2  349  153    8 1875%
c i   31.8   99333   676046      5228    3700    288 92372   91   366   55  25%      2  350  110    8 1333%
c i   31.8   99322   676046      5229    3700    288 92372   91   366   55  25%      2  350  109    8 1328%
c i   31.8   99312   676046      5230    3700    288 92372   91   366   55  25%      2  349  109    8 1323%
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   31.8   99304   676046      5231    3700    288 92372   91   366   55  25%      2  349  108    8 1317%
c i   31.9   99293   676046      5239    3705    289 92372   91   366   55  25%      2  349  107    8 1302%
c 
c [simplification-6] limit 5334 conflicts (hard 15105) hit after 5338 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 99293 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 72197 variables remain 73% (27096 retained 27%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1883 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1883 out of 1883 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 289 variables
c [treelook-3] limit 381505 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 77158 literals 39%
c [treelook-3] scheduling used 483139 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 381505 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 405946 steps
c [treelook-3] 77152 literals remain 39%
c [treelook-3] 34863 variables remain to probed next time 35%
c [treelook-3] removed 0 variables, found 2955 hbrs
c [unhide-6] limit 381505 with penalty 1 = 0 + 1
c [unhide-6-6] 1 units, 720 failed, 7020 tauts, 0 hbrs, 9393 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 209 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 98798 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 972 blocked clauses
c [block-2] 972 < 1/100 * 674081 = 6740 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 98797 variables 100%
c [elim-5] limit of 38150543 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 10993 not tried 11% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1697 = 2% variables out of 98797 scheduled
c [bca-2] limit of 10000000 steps and 1334078 added (scaled 2)
c [bca-2] 175382 out of 194202 literals actually usable 90%
c [bca-2] added 147 blocked clauses in 539994 steps
c [sweep-2] limit 1333464 based on 666732 irredundant clauses
c [sweep-2-1] 9468 pos 9.8% + 87631 neg 90.2% = 97099 sched 100.0% ret 1
c [sweep-2-1] 1854107 steps 12 queries 21563.33 avg class size
c [sweep-2-1] 88 decisions 10 SAT calls 179.60 avg env size
c [sweep-2-1] 96771 variables remain 100% (27 retained 0%)
c [decomp-14] removed 305 variables
c [sweep-2-1] removed 305 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 305 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-6] 653967 negative 99.1% of 660200 except 6233 0.9%
c [phase-count-6] 530925 positive 80.4% of 660200 except 129275 19.6%
c [phase-count-6] less non-negative clauses 6233 than limit 66000 (10.0%)
c [phase-count-6] non-pos/non-neg = 129275/6233 = 20.74 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 1225 negative 100%
c [sort-queue-6] sorted 48619 enqueued variables after 5338 conflicts
c [score-dist-6] active 48176 (50%), one 0 (0%), zero 48619 (50%)
c [score-dist-6] max exp 523, different 22 (4%)
c [score-dist-6] median active exp 517, avg 516.7
c [simplification-6] removed 2498 variables 2.5% (96795 remain 39%)
c [simplification-6] removed 15846 irredundant clauses 2.3% (660200 remain 48%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 20338 (soft 10338 + delta 10000)
c [simplification-6] new conflict limit 10338 (hard 20338)
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   36.5   96794   660200      5341    2792    278 89178   90   367   51  25%      1  350   82    8  993%
c i   36.7   96418   660200      5418    2862    278 89179   89   367   52  24%      1  350   77    8  925%
c i   37.8   96415   660200      5970    3126    286 89193  112   375   54  30%      3  354  256   10 2448%
c i   39.5   96157   660200      6675    3545    292 89205  147   409   55  36%      4  385  424   14 3052%
c i   39.5   96151   660200      6688    3553    292 89205  148   410   55  36%      4  386  417   14 2993%
c i   39.5   96147   660200      6689    3553    292 89205  148   410   55  36%      4  386  415   14 2981%
c i   39.5   96143   660200      6691    3554    292 89205  148   410   55  36%      4  386  415   14 2974%
c i   39.6   96135   660200      6697    3558    292 89205  148   410   55  36%      4  386  414   14 2965%
c i   39.7   96134   660200      6764    3615    293 89206  149   414   55  36%      4  389  369   14 2602%
c i   47.9   96126   660200      9843    5626    337 89267  256   582   65  44%     32  535  490   28 1736%
c 
c [simplification-7] limit 10354 conflicts (hard 20338) hit after 10356 conflicts
c [quatres-2] found 38922 quaternary clauses 37% in total
c [quatres-2-2] added 1 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 21 xors of average arity 2.6
c [gauss-2] connected 54 occurrences of 47 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 32 variables
c [basicprobe-3] limit 34229533 penalty 0 = 0 + 0
c [basicprobe-3-0] 34551 probes remain 37% after last round
c [basicprobe-3-0] 165 units = 165 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1763 variables, found 100154 hbrs
c [bate-1] eliminated 91 asymmetric tautologies during probing
c [unhide-7] limit 684590 with penalty 1 = 0 + 1
c [unhide-7-7] 1 units, 144 failed, 8613 tauts, 0 hbrs, 68750 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 166 transitive binary clauses
c [transred-3] found 1 units
c [cce-2] limit of 17114766 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 8557383 steps for small clauses
c [cce-2-1] scheduling 328382 clauses = 309810 binary + 18572 ternary
c [cce-2-1] tried to eliminate 314 small clauses 0%
c [cce-2-1] eliminated 86 binary clauses 0%
c [cce-2-1] eliminated 7 ternary clauses 0%
c [cce-2-1] eliminated 93 small clauses 0%
c [cce-2-1] eliminated 2114 small clauses in 17114768 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2114 covered clauses in round 1
c [cce-2] eliminated 2114 covered clauses in TOTAL during 1 rounds
c [cce-2] 2114 < 1/100 * 637000 = 6370 considered unsuccessful
c [elim-6] 10855 variables 12% will be scheduled this time
c [elim-6] scheduled 10855 variables 12%
c [elim-6] limit of 136918133 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 24206641 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 10855 scheduled
c [bca-3] limit of 10000000 steps and 1266273 added (scaled 2)
c [bca-3] 166349 out of 188078 literals actually usable 88%
c [bca-3] added 49 blocked clauses in 495186 steps
c [sweep-3] limit 2053772 penalty 0 = 0 + 0
c [sweep-3-1] 9337 pos 9.9% + 84676 neg 90.1% = 94013 sched 100.0% ret 25
c [sweep-3-1] 2057379 steps 39 queries 12492.51 avg class size
c [sweep-3-1] 511 decisions 36 SAT calls 80.89 avg env size
c [sweep-3-1] 93391 variables remain 99% (647 retained 1%)
c [decomp-16] removed 62 variables
c [sweep-3-1] removed 62 vars (0 failed, 2 eqs, 7 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 62 vars in TOTAL (1 rounds, 38 queries)
c [phase-count-7] 626445 negative 99.0% of 632673 except 6228 1.0%
c [phase-count-7] 512545 positive 81.0% of 632673 except 120128 19.0%
c [phase-count-7] less non-negative clauses 6228 than limit 63200 (10.0%)
c [phase-count-7] non-pos/non-neg = 120128/6228 = 19.29 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 1141 negative 100%
c [sort-queue-7] sorted 45071 enqueued variables after 10356 conflicts
c [score-dist-7] active 48905 (52%), one 0 (0%), zero 45071 (48%)
c [score-dist-7] max exp 526, different 25 (5%)
c [score-dist-7] median active exp 518, avg 518.1
c [simplification-7] removed 2057 variables 2.1% (93976 remain 38%)
c [simplification-7] removed 27527 irredundant clauses 4.2% (632673 remain 46%)
c [simplification-7] maximum reduction of 4% = max (2%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 9000
c [simplification-7] penalized conflict interval 9000 = 1 * 9000
c [simplification-7] hard conflict limit 29356 (soft 19356 + delta 10000)
c [simplification-7] new conflict limit 19356 (hard 29356)
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   54.5   93975   632673     10407    6071    393 183771  245   616   60  40%     20  564  249   29  848%
c i   54.7   93968   632673     10552    6199    393 183772  243   623   61  39%     17  570  214   30  724%
c i   60.4   93965   632673     12907    8006    416 183824  239   738   65  32%     23  663  233   37  632%
c i   60.4   93952   632673     12910    8008    416 183824  238   738   65  32%     23  662  231   37  626%
c i   60.4   93945   632673     12911    8008    416 183824  238   737   65  32%     23  662  230   37  624%
c i   60.4   93940   632673     12912    8008    416 183824  238   737   65  32%     23  662  229   37  621%
c i   60.5   93934   632673     12913    8008    416 183824  238   737   65  32%     23  662  228   37  619%
c i   60.5   93930   632673     12914    8008    416 183824  238   737   65  32%     22  662  228   37  617%
c i   60.5   93924   632673     12915    8008    416 183824  238   737   65  32%     22  661  227   37  614%
c i   60.5   93921   632673     12929    8014    420 183827  237   737   65  32%     22  661  215   37  582%
c i   62.5   93914   632673     13628    8541    429 183841  229   714   65  32%     13  632  177   38  462%
c i   62.5   93913   632673     13630    8541    429 183841  229   714   65  32%     13  632  177   38  460%
c i   62.5   93908   632673     13633    8542    429 183842  229   714   65  32%     13  632  176   38  459%
c i   64.6   93905   632673     14669    9396    444 183851  201   733   66  27%      9  641  198   39  502%
c i   67.3   93895   632673     15645    9797    450 183875  264   744   71  36%      8  642  410   46  886%
c i   68.4   93862   632673     16071   10056    480 183879  265   735   71  36%      6  629  281   48  590%
c i   68.4   93853   632673     16072   10056    480 183879  265   734   71  36%      6  628  280   48  588%
c i   68.4   93845   632673     16073   10056    480 183879  265   734   71  36%      6  628  279   48  585%
c i   68.4   93835   632673     16074   10056    480 183879  265   734   71  36%      6  628  278   48  583%
c i   69.0   93826   632673     16274   10233    481 183883  254   728   71  35%      4  621  149   48  312%
c i   70.4   93817   632673     16772   10431    484 183889  263   704   74  37%      4  592  347   50  699%
c 
c [simplification-8] limit 19447 conflicts (hard 29356) hit after 19449 conflicts
c [quatres-3] found 39515 quaternary clauses 39% in total
c [ternres-3] limit 6179370 with penalty 1 = 1 + 0
c [ternres-3] 68216 schedulable variables 73%
c [ternres-3] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-3] 27960 variables remain 30% (65851 retained 70%)
c [decomp-17] removed 189 variables
c [simpleprobe-4] 28046 schedulable variables 30%
c [simpleprobe-4] limit 49434964 penalty 0 = 0 + 0
c [decomp-18] removed 1906 variables
c [simpleprobe-4] 12288 variables remain 13% (79593 retained 87%)
c [simpleprobe-4] removed 1906 variables, found 87298 hbrs, 937 units
c [unhide-8] limit 1235874 with penalty 1 = 0 + 1
c [unhide-8-8] 1 units, 543 failed, 23501 tauts, 0 hbrs, 75123 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 277 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 91571 variables 100%
c [block-3] limit of 61793705 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 28 blocked clauses
c [block-3] 28 < 1/100 * 611234 = 6112 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1215852 added (scaled 2)
c [bca-4] 157407 out of 183144 literals actually usable 86%
c [bca-4] added 107 blocked clauses in 470079 steps
c [sweep-4] limit 3707622 penalty 0 = 0 + 0
c [sweep-4-1] 9775 pos 10.7% + 81307 neg 89.3% = 91082 sched 99.5% ret 489
c [sweep-4-1] 3945208 steps 28 queries 20157.46 avg class size
c [sweep-4-1] 225 decisions 22 SAT calls 79.32 avg env size
c [sweep-4-1] 90961 variables remain 99% (610 retained 1%)
c [decomp-19] removed 42 variables
c [sweep-4-1] removed 42 vars (0 failed, 6 eqs, 11 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 42 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-8] 601256 negative 99.0% of 607495 except 6239 1.0%
c [phase-count-8] 488010 positive 80.3% of 607495 except 119485 19.7%
c [phase-count-8] less non-negative clauses 6239 than limit 60700 (10.0%)
c [phase-count-8] non-pos/non-neg = 119485/6239 = 19.15 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 962 negative 100%
c [sort-queue-8] sorted 40122 enqueued variables after 19449 conflicts
c [score-dist-8] active 51407 (56%), one 0 (0%), zero 40122 (44%)
c [score-dist-8] max exp 528, different 27 (5%)
c [score-dist-8] median active exp 520, avg 519.7
c [simplification-8] removed 2282 variables 2.4% (91529 remain 37%)
c [simplification-8] removed 25178 irredundant clauses 4.0% (607495 remain 44%)
c [simplification-8] maximum reduction of 4% = max (2%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 13000
c [simplification-8] penalized conflict interval 13000 = 1 * 13000
c [simplification-8] hard conflict limit 42449 (soft 32449 + delta 10000)
c [simplification-8] new conflict limit 32449 (hard 42449)
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   81.8   91528   607495     19590   11535    484 236250  291   583   69  50%     27  448  180   61  294%
c i   81.8   91527   607495     19600   11542    484 236250  290   582   69  50%     27  448  177   61  290%
c i   83.7   91526   607495     20458   12049    494 236252  273   546   73  50%     14  406  229   63  363%
c i   83.7   91519   607495     20465   12052    494 236252  273   545   73  50%     14  405  232   63  368%
c i   84.3   91513   607495     20702   12229    495 236253  271   546   73  50%     11  404  228   64  358%
c i   84.7   91480   607495     20905   12416    495 236255  260   552   73  47%      9  409  125   64  197%
c i   85.1   91475   607495     21141   12627    496 236261  246   556   73  44%      7  412   60   63   95%
c i   88.5   91466   607495     22948   13610    530 236274  257   551   73  47%     13  396  261   69  378%
c i   90.6   91464   607495     23705   13997    535 236276  278   569   73  49%      8  409  420   73  578%
c i   97.7   91462   607495     26391   14992    552 236310  332   577   77  58%     24  401  262   86  305%
c i   97.9   91358   607495     26494   15088    553 236310  326   582   77  56%     22  405  203   86  236%
c 
c [simplification-9] limit 32451 conflicts (hard 42449) hit after 32452 conflicts
c [ternres-4] limit 19795235 with penalty 0 = 0 + 0
c [ternres-4] 27265 schedulable variables 30%
c [ternres-4] 9 ternary resolvents (1 bin, 8 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-20] removed 178 variables
c [unhide-9] limit 989761 with penalty 2 = 0 + 2
c [unhide-9-9] 2 units, 50 failed, 7234 tauts, 0 hbrs, 119408 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 229 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 91179 variables 100%
c [elim-7] limit of 197952358 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1734 variables 2% in round 1 in 55428211 steps
c [elim-7-1] backward subsumption/strengthening limit 55428200
c [elim-7-1-1] backward checking 6977 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 8 and strengthened 166 clauses in 2602333 steps
c [elim-7-1] rescheduled 338 variables 0% by backward subsumption
c [elim-7-2] eliminated 52 variables 0% in round 2 in 377880 steps
c [elim-7-2] backward subsumption/strengthening limit 377800
c [elim-7-2-1] backward checking 352 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 6 clauses in 249873 steps
c [elim-7-2] rescheduled 7 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 8394 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1786 = 2% variables out of 91179 scheduled
c [bca-5] limit of 10000000 steps and 1188749 added (scaled 2)
c [bca-5] 155266 out of 178788 literals actually usable 87%
c [bca-5] added 78 blocked clauses in 471667 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 59385700 penalty 0 = 0 + 0
c [sweep-5-1] 9245 pos 10.4% + 79592 neg 89.6% = 88837 sched 99.4% ret 556
c [sweep-5-1] 59450088 steps 755 queries 1055.48 avg class size
c [sweep-5-1] 6093 decisions 655 SAT calls 86.18 avg env size
c [sweep-5-1] 65012 variables remain 73% (23911 retained 27%)
c [decomp-21] removed 724 variables
c [sweep-5-1] removed 724 vars (1 failed, 111 eqs, 194 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 724 vars in TOTAL (1 rounds, 754 queries)
c [phase-count-9] 584805 negative 99.0% of 590897 except 6092 1.0%
c [phase-count-9] 474893 positive 80.4% of 590897 except 116004 19.6%
c [phase-count-9] less non-negative clauses 6092 than limit 59000 (10.0%)
c [phase-count-9] non-pos/non-neg = 116004/6092 = 19.04 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 746 negative 100%
c [sort-queue-9] sorted 34381 enqueued variables after 32452 conflicts
c [score-dist-9] active 54288 (61%), one 0 (0%), zero 34381 (39%)
c [score-dist-9] max exp 530, different 29 (5%)
c [score-dist-9] median active exp 522, avg 521.1
c [simplification-9] removed 2689 variables 2.9% (88669 remain 36%)
c [simplification-9] removed 16598 irredundant clauses 2.7% (590897 remain 43%)
c [simplification-9] maximum reduction of 3% = max (3%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 18000
c [simplification-9] penalized conflict interval 18000 = 1 * 18000
c [simplification-9] hard conflict limit 60452 (soft 50452 + delta 10000)
c [simplification-9] new conflict limit 50452 (hard 60452)
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  124.3   88668   590897     32664    8969    555 285386  418   638   59  65%     74  422  333  119  279%
c i  124.5   88667   590897     32774    9070    556 285388  410   643   59  64%     65  426  253  119  212%
c i  130.7   88662   590897     35696   11100    563 285403  404   763   69  53%     26  524  457  131  350%
c i  130.8   88657   590897     35720   11111    563 285404  405   763   69  53%     26  525  465  131  356%
c i  130.8   88655   590897     35724   11112    563 285404  405   763   69  53%     25  525  465  131  356%
c i  130.9   88652   590897     35729   11114    563 285404  405   763   69  53%     25  525  461  131  352%
c i  130.9   88648   590897     35731   11115    563 285404  405   763   69  53%     25  524  458  131  350%
c i  134.7   88642   590897     37237   11713    567 285407  464   797   73  58%     10  546  562  141  398%
c i  141.7   88638   590897     39891   12620    573 285414  546   815   82  67%     19  542  583  161  363%
c i  151.2   88587   590897     43382   13258    577 285418  634   803   98  79%     30  502  603  189  319%
c i  151.9   88586   590897     43655   13449    582 285420  612   803   99  76%     21  500  394  189  208%
c i  153.0   88579   590897     44092   13728    587 285426  582   799   99  73%     12  493  274  190  144%
c i  154.7   88578   590897     44770   14062    591 285427  566   793   99  71%      4  481  500  193  259%
c i  157.1   88570   590897     45712   14363    593 285429  571   786  105  73%      1  468  576  199  290%
c i  168.0   88569   590897     49491   14955    598 285435  639   764  138  84%     33  420  703  226  311%
c i  168.1   88568   590897     49492   14955    598 285435  639   764  138  84%     33  420  700  226  310%
c i  168.1   88567   590897     49493   14955    598 285435  639   764  138  84%     33  420  697  226  309%
c i  168.1   88566   590897     49495   14956    598 285435  639   764  138  84%     33  420  692  226  307%
c 
c [simplification-10] limit 50486 conflicts (hard 60452) hit after 50488 conflicts
c [quatres-4] found 34660 quaternary clauses 36% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [ternres-5] limit 29598575 with penalty 0 = 0 + 0
c [ternres-5] all 88566 free variables schedulable
c [ternres-5] 87 ternary resolvents (0 bin, 87 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 1849910 penalty 3 = 3 + 0
c [card-4] found 4354 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1849910 for elimination
c [card-4] 4354 out of 4354 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1479928 penalty 2 = 2 + 0
c [gauss-3] extracted 21 xors of average arity 2.9
c [gauss-3] connected 61 occurrences of 61 variables (average 1.0)
c [gauss-3] limit 1479928 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 6 variables
c [treelook-4] limit 1479928 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 130085 literals 73%
c [treelook-4] scheduling used 1479930 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1479928 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 1512357 steps
c [treelook-4] 130046 literals remain 73%
c [treelook-4] 28142 variables remain to probed next time 32%
c [decomp-23] removed 1 variables
c [treelook-4] removed 4 variables, found 7594 hbrs
c [unhide-10] limit 2959857 with penalty 1 = 0 + 1
c [unhide-10-10] 5 units, 112 failed, 14678 tauts, 0 hbrs, 286065 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 208 transitive binary clauses
c [cce-3] limit of 36998219 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 25 clauses out of 1784 (1%) of length 9
c [cce-3-1] eliminated 25 clauses out of 589 (4%) of length 8
c [cce-3-1] eliminated 81 clauses out of 919 (9%) of length 7
c [cce-3-1] eliminated 3697 clauses out of 5828 (63%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 3828 large clauses in 36998219 steps
c [cce-3-1] allowing another 18499109 steps for small clauses
c [cce-3-1] scheduling 320975 clauses = 296765 binary + 24210 ternary
c [cce-3-1] tried to eliminate 771 small clauses 0%
c [cce-3-1] eliminated 193 binary clauses 0%
c [cce-3-1] eliminated 41 ternary clauses 0%
c [cce-3-1] eliminated 234 small clauses 0%
c [cce-3-1] eliminated 1404 small clauses in 36998221 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5232 covered clauses in round 1
c [cce-3] eliminated 5232 covered clauses in TOTAL during 1 rounds
c [cce-3] 5232 < 1/100 * 589753 = 5897 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 88429 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 11839430140 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2208 variables 2% in round 1 in 55073067 steps
c [elim-8-1] backward subsumption/strengthening limit 55073000
c [elim-8-1-1] backward checking 6744 touched variables 8%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 225 clauses in 3669735 steps
c [elim-8-1] rescheduled 485 variables 1% by backward subsumption
c [elim-8-2] eliminated 68 variables 0% in round 2 in 1963508 steps
c [elim-8-2] backward subsumption/strengthening limit 1963500
c [elim-8-2-1] backward checking 509 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 394329 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2276 = 3% variables out of 88429 scheduled
c [bca-6] limit of 10000000 steps and 1155956 added (scaled 2)
c [bca-6] 149679 out of 172308 literals actually usable 87%
c [bca-6] added 611 blocked clauses in 453759 steps
c [sweep-6] limit 8879572 penalty 0 = 0 + 0
c [sweep-6-1] 8163 pos 13.0% + 54754 neg 87.0% = 62917 sched 73.0% ret 23236
c [sweep-6-1] 8892066 steps 131 queries 4639.77 avg class size
c [sweep-6-1] 1631 decisions 109 SAT calls 98.07 avg env size
c [sweep-6-1] 61708 variables remain 72% (24410 retained 28%)
c [decomp-24] removed 65 variables
c [sweep-6-1] removed 65 vars (0 failed, 24 eqs, 41 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 65 vars in TOTAL (1 rounds, 130 queries)
c [phase-count-10] 575011 negative 99.6% of 577281 except 2270 0.4%
c [phase-count-10] 461935 positive 80.0% of 577281 except 115346 20.0%
c [phase-count-10] less non-negative clauses 2270 than limit 57700 (10.0%)
c [phase-count-10] non-pos/non-neg = 115346/2270 = 50.81 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 719 negative 100%
c [sort-queue-10] sorted 31727 enqueued variables after 50488 conflicts
c [score-dist-10] active 54361 (63%), one 0 (0%), zero 31727 (37%)
c [score-dist-10] max exp 531, different 30 (6%)
c [score-dist-10] median active exp 523, avg 522.0
c [simplification-10] removed 2478 variables 2.8% (86088 remain 35%)
c [simplification-10] removed 13616 irredundant clauses 2.3% (577281 remain 42%)
c [simplification-10] maximum reduction of 3% = max (3%, 2%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 23000
c [simplification-10] penalized conflict interval 23000 = 1 * 23000
c [simplification-10] hard conflict limit 84988 (soft 73488 + delta 11500)
c [simplification-10] new conflict limit 73488 (hard 84988)
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  179.8   86087   577281     51318    9601    699 279884  623   758   64  82%     11  403  609  236  258%
c i  196.8   86084   577281     59613   10817    714 279903  563   652   91  86%     97  254  375  278  135%
c i  196.8   86083   577281     59614   10817    714 279903  563   651   91  86%     97  254  373  278  134%
c i  196.8   86082   577281     59619   10820    714 279903  562   651   91  86%     97  254  367  278  132%
c i  196.8   86081   577281     59624   10824    714 279903  562   651   91  86%     96  253  361  278  130%
c i  196.8   86080   577281     59625   10824    714 279903  562   651   91  86%     96  253  360  278  129%
c i  196.9   86079   577281     59627   10825    714 279903  561   651   91  86%     96  253  358  278  129%
c i  196.9   86078   577281     59664   10847    714 279903  559   650   91  86%     92  252  349  278  126%
c i  196.9   86077   577281     59666   10848    714 279903  559   650   91  86%     92  252  348  278  125%
c i  196.9   86076   577281     59669   10850    714 279903  558   650   91  86%     91  252  345  278  124%
c i  199.4   86075   577281     60890   11037    717 279909  538   620   93  87%     23  217  471  282  167%
c i  199.4   86073   577281     60900   11042    717 279909  537   619   93  87%     23  217  464  282  165%
c i  199.5   86068   577281     60958   11060    717 279909  535   618   93  87%     21  216  441  282  157%
c i  199.6   86067   577281     60993   11091    717 279910  531   618   93  86%     19  216  399  282  142%
c i  199.6   86066   577281     61060   11130    717 279911  527   617   93  85%     17  214  366  282  130%
c i  208.3   85981   577281     64668   11687    757 279954  428   492   99  87%     24   81  314  286  110%
c i  220.3   85976   577281     73317   13364    786 279979  522   612  138  85%     96  195  625  304  205%
c i  220.4   85975   577281     73409   13447    788 279980  512   612  138  84%     86  195  450  304  148%
c i  220.5   85918   577281     73426   13458    788 279981  510   611  138  83%     84  194  426  304  140%
c i  220.5   85917   577281     73429   13460    788 279981  509   611  138  83%     84  194  421  304  139%
c 
c [simplification-11] limit 73529 conflicts (hard 84988) hit after 73530 conflicts
c [quatres-5] found 34992 quaternary clauses 38% in total
c [ternres-6] limit 38493375 with penalty 0 = 0 + 0
c [ternres-6] all 85917 free variables schedulable
c [ternres-6] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-25] removed 176 variables
c [basicprobe-4] limit 192466876 penalty 0 = 0 + 0
c [basicprobe-4-0] 26113 probes remain 32% after last round
c [basicprobe-4-0] 890 units = 880 failed (99%) + 10 lifted (1%)
c [basicprobe-4-0] removed 3182 variables, found 559273 hbrs
c [bate-2] eliminated 508 asymmetric tautologies during probing
c [unhide-11] limit 3849337 with penalty 1 = 0 + 1
c [unhide-11-12] 23 units, 113 failed, 48144 tauts, 0 hbrs, 95023 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 155 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 82543 variables 100%
c [block-4] limit of 96233438 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 219 blocked clauses
c [block-4] 219 < 1/100 * 552731 = 5527 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 82535 variables 100%
c [elim-9] limit of 769867506 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 2490 variables 3% in round 1 in 50647883 steps
c [elim-9-1] backward subsumption/strengthening limit 50647800
c [elim-9-1-1] backward checking 8215 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 18 and strengthened 419 clauses in 2496933 steps
c [elim-9-1] rescheduled 978 variables 1% by backward subsumption
c [elim-9-2] eliminated 132 variables 0% in round 2 in 1574588 steps
c [elim-9-2] backward subsumption/strengthening limit 1574500
c [elim-9-2-1] backward checking 1005 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 1 clauses in 529547 steps
c [elim-9-2] rescheduled 6 variables 0% by backward subsumption
c [elim-9-3] eliminated 2 variables 0% in round 3 in 3218 steps
c [elim-9-3] backward subsumption/strengthening limit 3200
c [elim-9-3-1] backward checking 9 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 3201 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 2636 = 3% variables out of 82535 scheduled
c [bca-7] limit of 10000000 steps and 1088162 added (scaled 2)
c [bca-7] 140183 out of 159800 literals actually usable 88%
c [bca-7] added 90 blocked clauses in 410144 steps
c [sweep-7] limit 11548012 penalty 0 = 0 + 0
c [sweep-7-1] 8116 pos 14.0% + 49910 neg 86.0% = 58026 sched 72.6% ret 21873
c [sweep-7-1] 11558201 steps 173 queries 3287.66 avg class size
c [sweep-7-1] 1997 decisions 143 SAT calls 101.22 avg env size
c [sweep-7-1] 55922 variables remain 70% (23966 retained 30%)
c [decomp-26] removed 113 variables
c [sweep-7-1] removed 113 vars (0 failed, 29 eqs, 54 impls)
c [sweep-7] removed 113 vars in TOTAL (1 rounds, 172 queries)
c [phase-count-11] 541142 negative 99.6% of 543312 except 2170 0.4%
c [phase-count-11] 434338 positive 79.9% of 543312 except 108974 20.1%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 108 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 28155 enqueued variables after 73530 conflicts
c [score-dist-11] active 51631 (65%), one 0 (0%), zero 28155 (35%)
c [score-dist-11] max exp 532, different 31 (6%)
c [score-dist-11] median active exp 523, avg 522.7
c [simplification-11] removed 6131 variables 7.1% (79786 remain 32%)
c [simplification-11] removed 33969 irredundant clauses 5.9% (543312 remain 39%)
c [simplification-11] maximum reduction of 7% = max (7%, 6%)
c [simplification-11] large reduction 7% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 85530 (soft 75530 + delta 10000)
c [simplification-11] new conflict limit 75530 (hard 85530)
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  237.6   79785   543312     73577    6522    966 734575  494   611   64  81%     69  193  266  303   88%
c i  237.7   79784   543312     73579    6522    966 734575  494   611   64  81%     69  193  266  303   88%
c i  238.1   79783   543312     73854    6644    966 734576  482   598   65  81%     48  179  303  303  100%
c i  239.5   79781   543312     74796    6813    966 734576  456   553   67  83%     10  132  337  304  111%
c i  239.5   79780   543312     74798    6814    966 734576  456   553   67  82%     10  132  334  304  110%
c i  239.6   79779   543312     74900    6865    966 734578  451   550   67  82%      6  129  309  304  102%
c i  241.5   79778   543312     76287    7160    972 734579  416   499   70  83%     -6   76  332  305  109%
c 
c [simplification-12] limit 75540 conflicts (hard 85530) hit after 78590 conflicts
c [ternres-7] limit 40201747 with penalty 0 = 0 + 0
c [ternres-7] all 79778 free variables schedulable
c [ternres-7] 192 ternary resolvents (0 bin, 192 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 8 variables
c [simpleprobe-5] 11588 schedulable variables 15%
c [simpleprobe-5] limit 160806988 penalty 0 = 0 + 0
c [decomp-28] removed 1465 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1465 variables, found 93489 hbrs, 1018 units
c [unhide-12] limit 4020174 with penalty 1 = 0 + 1
c [unhide-12-13] 6 units, 44 failed, 46841 tauts, 0 hbrs, 22156 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 132 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 78214 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 733 variables 1% in round 1 in 47902171 steps
c [elim-10-1] backward subsumption/strengthening limit 47902100
c [elim-10-1-1] backward checking 3312 touched variables 4%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 13 and strengthened 65 clauses in 1164299 steps
c [elim-10-1] rescheduled 162 variables 0% by backward subsumption
c [elim-10-2] eliminated 22 variables 0% in round 2 in 400536 steps
c [elim-10-2] backward subsumption/strengthening limit 400500
c [elim-10-2-1] backward checking 165 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 9 and strengthened 1 clauses in 162900 steps
c [elim-10-2] rescheduled 15 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 15202 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 758 = 1% variables out of 78214 scheduled
c [elim-10] 758 < 1/100 * 78214 = 782 considered unsuccessful
c [bca-8] limit of 10000000 steps and 1049475 added (scaled 2)
c [bca-8] 136247 out of 154914 literals actually usable 88%
c [bca-8] added 82 blocked clauses in 402161 steps
c [sweep-8] limit 12060524 penalty 0 = 0 + 0
c [sweep-8-1] 7504 pos 13.6% + 47627 neg 86.4% = 55131 sched 71.2% ret 22325
c [sweep-8-1] 12087333 steps 157 queries 3403.32 avg class size
c [sweep-8-1] 2301 decisions 140 SAT calls 83.39 avg env size
c [sweep-8-1] 52970 variables remain 69% (24224 retained 31%)
c [decomp-29] removed 326 variables
c [sweep-8-1] removed 326 vars (0 failed, 19 eqs, 30 impls)
c [sweep-8] removed 326 vars in TOTAL (1 rounds, 156 queries)
c [phase-count-12] 516617 negative 99.6% of 518740 except 2123 0.4%
c [phase-count-12] 408821 positive 78.8% of 518740 except 109919 21.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 4 negative 100%
c [sort-queue-12] sorted 25589 enqueued variables after 78590 conflicts
c [score-dist-12] active 51541 (67%), one 0 (0%), zero 25589 (33%)
c [score-dist-12] max exp 533, different 32 (6%)
c [score-dist-12] median active exp 523, avg 522.9
c [simplification-12] removed 2648 variables 3.3% (77130 remain 31%)
c [simplification-12] removed 24572 irredundant clauses 4.5% (518740 remain 38%)
c [simplification-12] maximum reduction of 5% = max (3%, 5%)
c [simplification-12] large reduction 5% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 90590 (soft 80590 + delta 10000)
c [simplification-12] new conflict limit 80590 (hard 90590)
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  251.7   77129   518740     78705    6259   1082 721413  368   449   62  82%      1   24  189  305   62%
c i  251.7   77128   518740     78707    6260   1082 721413  368   449   62  82%      1   24  187  305   61%
c i  251.7   77127   518740     78709    6261   1082 721413  368   449   62  82%      1   24  186  305   61%
c i  252.7   77126   518740     79514    6652   1083 721426  339   434   63  78%     -8    9  229  304   75%
c i  252.7   77125   518740     79515    6652   1083 721426  339   434   63  78%     -8    9  228  304   75%
c i  252.7   77124   518740     79540    6662   1083 721426  338   433   63  78%     -9    8  231  304   76%
c i  252.9   77123   518740     79777    6845   1084 721431  324   435   63  74%    -11    9  143  303   47%
c i  253.0   77122   518740     79778    6845   1084 721431  323   434   63  74%    -11    9  142  303   47%
c i  253.0   77121   518740     79780    6846   1084 721431  323   434   63  74%    -11    9  141  303   47%
c i  253.5   77120   518740     80432    7318   1090 721435  293   443   64  66%    -14   18   99  301   33%
c i  254.3   77116   518740     81082    7795   1097 721440  276   461   66  60%    -16   35  121  300   40%
c i  255.1   77111   518740     82128    8735   1109 721444  222   474   70  47%    -14   48   38  296   13%
c i  257.9   77110   518740     85112    9922   1121 721456  222   398   74  56%      9  -29  261  292   89%
c i  259.4   77109   518740     86296   10425   1135 721462  237   406   79  58%     -5  -20  338  292  116%
c i  261.6   77108   518740     87592   10777   1138 721463  263   408   79  65%     -9  -18  298  293  102%
c i  263.0   77107   518740     88489   11030   1143 721467  276   407   79  68%    -12  -19  286  293   98%
c i  263.9   77106   518740     89114   11339   1151 721473  271   404   80  67%    -14  -21  242  293   83%
c 
c [simplification-13] limit 80625 conflicts (hard 90590) hit after 90590 conflicts
c [quatres-6] found 35042 quaternary clauses 43% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [quatres-6-2] added 5 quaternary resolvents
c [ternres-8] limit 43497477 with penalty 0 = 0 + 0
c [ternres-8] all 77106 free variables schedulable
c [ternres-8] 232 ternary resolvents (0 bin, 232 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-30] removed 24 variables
c [treelook-5] limit 4349747 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 122659 literals 80%
c [treelook-5] scheduling used 2147752 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4349747 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 4400861 steps
c [treelook-5] 122576 literals remain 79%
c [treelook-5] 22207 variables remain to probed next time 29%
c [treelook-5] removed 6 variables, found 21562 hbrs
c [unhide-13] limit 4349747 with penalty 1 = 0 + 1
c [unhide-13-15] 4 units, 123 failed, 26063 tauts, 0 hbrs, 127650 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 156 transitive binary clauses
c [bca-9] limit of 10000000 steps and 1027112 added (scaled 2)
c [bca-9] 131587 out of 153864 literals actually usable 86%
c [bca-9] added 79 blocked clauses in 387864 steps
c [sweep-9] limit 13049243 penalty 0 = 0 + 0
c [sweep-9-1] 7384 pos 14.0% + 45416 neg 86.0% = 52800 sched 68.6% ret 24131
c [sweep-9-1] 13244925 steps 216 queries 2937.84 avg class size
c [sweep-9-1] 2688 decisions 198 SAT calls 102.00 avg env size
c [sweep-9-1] 49681 variables remain 65% (27173 retained 35%)
c [decomp-32] removed 206 variables
c [sweep-9-1] removed 206 vars (0 failed, 19 eqs, 40 impls)
c [sweep-9] removed 206 vars in TOTAL (1 rounds, 215 queries)
c [phase-count-13] 510169 negative 99.6% of 512290 except 2121 0.4%
c [phase-count-13] 405470 positive 79.1% of 512290 except 106820 20.9%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 4 positive 67%, 2 negative 33%
c [sort-queue-13] sorted 23944 enqueued variables after 90590 conflicts
c [score-dist-13] active 52781 (69%), one 0 (0%), zero 23944 (31%)
c [score-dist-13] max exp 533, different 32 (6%)
c [score-dist-13] median active exp 524, avg 523.2
c [simplification-13] removed 381 variables 0.5% (76725 remain 31%)
c [simplification-13] removed 6450 irredundant clauses 1.2% (512290 remain 37%)
c [simplification-13] maximum reduction of 1% = max (0%, 1%)
c [simplification-13] geometric conflict interval increment 11500 = 23000 / 2
c [simplification-13] new conflict interval 34500
c [simplification-13] penalized conflict interval 34500 = 1 * 34500
c [simplification-13] hard conflict limit 142340 (soft 125090 + delta 17250)
c [simplification-13] new conflict limit 125090 (hard 142340)
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  273.2   76724   512290     92193   12425   1369 732858  276   423   79  65%     12   -2   97  293   33%
c i  273.5   76723   512290     92469   12648   1373 732861  261   428   79  61%      4    3   69  292   24%
c i  273.6   76722   512290     92541   12682   1373 732861  261   426   79  61%      2    2  106  292   36%
c i  273.8   76721   512290     92807   12849   1374 732866  253   430   79  59%     -3    5  114  291   39%
c i  273.9   76720   512290     92896   12918   1374 732866  251   430   79  58%     -4    5  129  291   44%
c i  275.2   76717   512290     94117   13712   1382 732880  225   424   79  53%     -8   -0  135  288   47%
c i  277.1   76711   512290     95700   14456   1392 732887  223   392   83  57%     -6  -32  237  287   83%
c i  278.8   76710   512290     97022   15015   1411 732895  218   394   83  55%     -8  -30  103  285   36%
c i  279.0   76118   512290     97147   15118   1427 732895  213   400   83  53%     -9  -23   74  285   26%
c i  283.4   76114   512290    101001   16794   1449 732910  214   393   85  54%     24  -28  138  281   49%
c i  302.6   76108   512290    112921   18977   1458 732913  576   643  115  90%    138  199  526  328  161%
c i  304.6   76036   512290    114501   19101   1458 732913  583   639  143  91%     15  190  571  334  171%
c i  304.7   76035   512290    114509   19108   1458 732913  583   638  143  91%     15  190  557  334  167%
c i  306.9   76034   512290    116228   19260   1458 732913  591   641  143  92%    -10  187  570  341  167%
c i  307.0   76033   512290    116232   19263   1458 732913  591   640  143  92%    -10  187  571  341  167%
c i  307.0   76032   512290    116235   19264   1458 732913  591   640  143  92%    -10  187  566  341  166%
c i  307.0   76031   512290    116238   19266   1458 732913  591   640  143  92%    -10  186  566  341  166%
c i  307.0   76030   512290    116240   19267   1458 732913  590   640  143  92%    -11  186  562  341  165%
c i  307.0   76029   512290    116242   19268   1458 732913  590   640  143  92%    -11  186  558  341  163%
c i  307.0   76028   512290    116244   19269   1458 732913  590   640  143  92%    -11  186  553  341  162%
c i  307.1   76027   512290    116251   19275   1458 732913  589   640  143  92%    -11  186  539  341  158%
c i  307.8   76024   512290    117047   19612   1458 732917  591   670  151  88%    -19  214  657  344  191%
c 
c [simplification-14] limit 125115 conflicts (hard 142340) hit after 125116 conflicts
c [quatres-7] found 32819 quaternary clauses 43% in total
c [ternres-9] limit 53906343 with penalty 0 = 0 + 0
c [ternres-9] all 76024 free variables schedulable
c [ternres-9] 32 ternary resolvents (1 bin, 31 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 1347658 penalty 3 = 3 + 0
c [gauss-4] extracted 30 xors of average arity 2.8
c [gauss-4] connected 83 occurrences of 79 variables (average 1.1)
c [gauss-4] limit 1347658 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 29 variables
c [basicprobe-5] limit 269531719 penalty 0 = 0 + 0
c [basicprobe-5-0] 15497 probes remain 21% after last round
c [basicprobe-5-0] 1434 units = 1425 failed (99%) + 9 lifted (1%)
c [basicprobe-5-0] removed 3466 variables, found 637894 hbrs
c [bate-3] eliminated 754 asymmetric tautologies during probing
c [unhide-14] limit 2695317 with penalty 2 = 0 + 2
c [unhide-14-16] 2 units, 244 failed, 77743 tauts, 0 hbrs, 183794 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 90 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 336914648 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 702 (1%) of length 7
c [cce-4-1] eliminated 29 clauses out of 2486 (1%) of length 6
c [cce-4-1] eliminated 19675 clauses out of 29023 (68%) of length 5
c [cce-4-1] eliminated 13306 clauses out of 34573 (38%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 33014 large clauses in 336914651 steps
c [cce-4-1] allowing another 168457325 steps for small clauses
c [cce-4-1] scheduling 272261 clauses = 249639 binary + 22622 ternary
c [cce-4-1] tried to eliminate 12884 small clauses 5%
c [cce-4-1] eliminated 3510 binary clauses 1%
c [cce-4-1] eliminated 513 ternary clauses 2%
c [cce-4-1] eliminated 4023 small clauses 1%
c [cce-4-1] eliminated 6612 small clauses in 336914654 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 39626 covered clauses in round 1
c [cce-4] eliminated 39626 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 72276 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 16981 variables 23% in round 1 in 37633420 steps
c [elim-11-1] backward subsumption/strengthening limit 37633400
c [elim-11-1-1] backward checking 37614 touched variables 52%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 31 and strengthened 38 clauses in 5604389 steps
c [elim-11-1] rescheduled 164 variables 0% by backward subsumption
c [elim-11-2] eliminated 5 variables 0% in round 2 in 187174 steps
c [elim-11-2] backward subsumption/strengthening limit 187100
c [elim-11-2-1] backward checking 56 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 1 and strengthened 1 clauses in 187101 steps
c [elim-11-2] rescheduled 6 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 1737 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 16987 = 24% variables out of 72276 scheduled
c [bca-10] limit of 10000000 steps and 810351 added (scaled 2)
c [bca-10] 101762 out of 110580 literals actually usable 92%
c [bca-10] added 187 blocked clauses in 232414 steps
c [sweep-10] limit 16171903 penalty 0 = 0 + 0
c [sweep-10-1] 7434 pos 18.6% + 32506 neg 81.4% = 39940 sched 72.2% ret 15349
c [sweep-10-1] 16176242 steps 322 queries 1396.97 avg class size
c [sweep-10-1] 3837 decisions 288 SAT calls 122.78 avg env size
c [sweep-10-1] 36042 variables remain 65% (19001 retained 35%)
c [decomp-34] removed 600 variables
c [sweep-10-1] removed 600 vars (0 failed, 35 eqs, 53 impls)
c [sweep-10] removed 600 vars in TOTAL (1 rounds, 321 queries)
c [phase-count-14] 402171 negative 99.8% of 403084 except 913 0.2%
c [phase-count-14] 306290 positive 76.0% of 403084 except 96794 24.0%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 4 positive 8%, 48 negative 92%
c [sort-queue-14] sorted 15304 enqueued variables after 125116 conflicts
c [score-dist-14] active 39385 (72%), one 0 (0%), zero 15304 (28%)
c [score-dist-14] max exp 534, different 33 (6%)
c [score-dist-14] median active exp 525, avg 523.9
c [simplification-14] removed 21335 variables 28.1% (54689 remain 22%)
c [simplification-14] removed 109206 irredundant clauses 21.3% (403084 remain 29%)
c [simplification-14] maximum reduction of 28% = max (28%, 21%)
c [simplification-14] large reduction 28% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 137116 (soft 127116 + delta 10000)
c [simplification-14] new conflict limit 127116 (hard 137116)
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  350.1   54688   403084    125406    3430   1905 936342  588   749   59  79%     79  263  389  376  104%
c 
c [simplification-15] limit 127116 conflicts (hard 137116) hit after 128182 conflicts
c [ternres-10] limit 54653707 with penalty 0 = 0 + 0
c [ternres-10] all 54688 free variables schedulable
c [ternres-10] 641 ternary resolvents (0 bin, 641 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 1707928 penalty 4 = 4 + 0
c [card-5] found 1470 at-most-one constraints of average size 4.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1707928 for elimination
c [card-5] 1470 out of 1470 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 1 variables
c [simpleprobe-6] all 54688 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-36] removed 328 variables
c [simpleprobe-6] 24 variables remain 0% (54336 retained 100%)
c [simpleprobe-6] removed 328 variables, found 126822 hbrs, 269 units
c [unhide-15] limit 10930741 with penalty 0 = 0 + 0
c [unhide-15-20] 10 units, 30 failed, 95910 tauts, 0 hbrs, 67040 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 157 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 54175 variables 100%
c [block-5] limit of 68317134 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 183 blocked clauses
c [block-5] 183 < 1/100 * 391980 = 3919 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 54174 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 444 variables 1% in round 1 in 34149371 steps
c [elim-12-1] backward subsumption/strengthening limit 34149300
c [elim-12-1-1] backward checking 2979 touched variables 5%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 14 and strengthened 18 clauses in 971202 steps
c [elim-12-1] rescheduled 61 variables 0% by backward subsumption
c [elim-12-2] eliminated 8 variables 0% in round 2 in 171589 steps
c [elim-12-2] backward subsumption/strengthening limit 171500
c [elim-12-2-1] backward checking 47 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 7 and strengthened 0 clauses in 99908 steps
c [elim-12-2] rescheduled 6 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 81124 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 453 = 1% variables out of 54174 scheduled
c [elim-12] 453 < 1/100 * 54174 = 541 considered unsuccessful
c [bca-11] limit of 10000000 steps and 780743 added (scaled 2)
c [bca-11] 96673 out of 107444 literals actually usable 90%
c [bca-11] added 66 blocked clauses in 221143 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 163961120 penalty 0 = 0 + 0
c [sweep-11-1] 7058 pos 20.0% + 28166 neg 80.0% = 35224 sched 65.6% ret 18497
c [sweep-11-1] 164021014 steps 3684 queries 107.13 avg class size
c [sweep-11-1] 22893 decisions 3266 SAT calls 70.88 avg env size
c [sweep-11-1] 11887 variables remain 22% (41360 retained 78%)
c [decomp-37] removed 1553 variables
c [sweep-11-1] removed 1553 vars (0 failed, 425 eqs, 773 impls)
c [sweep-11] removed 1553 vars in TOTAL (1 rounds, 3683 queries)
c [phase-count-15] 384210 negative 99.8% of 385019 except 809 0.2%
c [phase-count-15] 292014 positive 75.8% of 385019 except 93005 24.2%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-15] sorted 12736 enqueued variables after 128182 conflicts
c [score-dist-15] active 39432 (76%), one 0 (0%), zero 12736 (24%)
c [score-dist-15] max exp 534, different 33 (6%)
c [score-dist-15] median active exp 524, avg 524.2
c [simplification-15] removed 2520 variables 4.6% (52168 remain 21%)
c [simplification-15] removed 18065 irredundant clauses 4.5% (385019 remain 28%)
c [simplification-15] maximum reduction of 5% = max (5%, 4%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 140182 (soft 130182 + delta 10000)
c [simplification-15] new conflict limit 130182 (hard 140182)
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  369.0   52167   385019    128583    5618   2172 1088187  477   729   64  65%      3  232  310  375   83%
c 
c [simplification-16] limit 130182 conflicts (hard 140182) hit after 131717 conflicts
c [quatres-8] found 29071 quaternary clauses 65% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-2] added 3 single-self-subsuming ternary resolvents
c [quatres-8-2] added 17 quaternary resolvents
c [ternres-11] limit 55828144 with penalty 0 = 0 + 0
c [ternres-11] all 52153 free variables schedulable
c [ternres-11] 502 ternary resolvents (2 bin, 500 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-38] removed 17 variables
c [treelook-6] limit 5582814 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 73224 literals 70%
c [treelook-6] scheduling used 1797138 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 5582814 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 5650224 steps
c [treelook-6] 73098 literals remain 70%
c [treelook-6] 11715 variables remain to probed next time 22%
c [decomp-39] removed 1 variables
c [treelook-6] removed 5 variables, found 34256 hbrs
c [unhide-16] limit 11165628 with penalty 0 = 0 + 0
c [unhide-16-24] 13 units, 126 failed, 84337 tauts, 0 hbrs, 49564 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 72 transitive binary clauses
c [cce-5] limit of 69785180 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-5-1] eliminated 2 clauses out of 22 (9%) of length 7
c [cce-5-1] eliminated 280 clauses out of 3264 (9%) of length 6
c [cce-5-1] eliminated 169 clauses out of 10742 (2%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 452 large clauses in 69785188 steps
c [cce-5-1] allowing another 34892594 steps for small clauses
c [cce-5-1] scheduling 204076 clauses = 185394 binary + 18682 ternary
c [cce-5-1] tried to eliminate 2761 small clauses 1%
c [cce-5-1] eliminated 827 binary clauses 0%
c [cce-5-1] eliminated 82 ternary clauses 0%
c [cce-5-1] eliminated 909 small clauses 0%
c [cce-5-1] eliminated 939 small clauses in 69785190 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1391 covered clauses in round 1
c [cce-5] eliminated 1391 covered clauses in TOTAL during 1 rounds
c [cce-5] 1391 < 1/100 * 378215 = 3782 considered unsuccessful
c [bca-12] limit of 10000000 steps and 755010 added (scaled 2)
c [bca-12] 89743 out of 104112 literals actually usable 86%
c [bca-12] added 53 blocked clauses in 206214 steps
c [sweep-12] limit 16748443 penalty 0 = 0 + 0
c [sweep-12-1] 2097 pos 18.8% + 9044 neg 81.2% = 11141 sched 21.4% ret 40914
c [sweep-12-1] 16777392 steps 529 queries 390.66 avg class size
c [sweep-12-1] 4084 decisions 462 SAT calls 66.48 avg env size
c [sweep-12-1] 9830 variables remain 19% (42147 retained 81%)
c [decomp-40] removed 206 variables
c [sweep-12-1] removed 206 vars (0 failed, 66 eqs, 127 impls)
c [sweep-12] removed 206 vars in TOTAL (1 rounds, 528 queries)
c [phase-count-16] 374999 negative 99.8% of 375806 except 807 0.2%
c [phase-count-16] 286148 positive 76.1% of 375806 except 89658 23.9%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-16] sorted 12529 enqueued variables after 131717 conflicts
c [score-dist-16] active 39320 (76%), one 0 (0%), zero 12529 (24%)
c [score-dist-16] max exp 534, different 33 (6%)
c [score-dist-16] median active exp 525, avg 524.3
c [simplification-16] removed 304 variables 0.6% (51849 remain 21%)
c [simplification-16] removed 9213 irredundant clauses 2.4% (375806 remain 27%)
c [simplification-16] maximum reduction of 2% = max (1%, 2%)
c [simplification-16] geometric conflict interval increment 11500 = 34500 / 3
c [simplification-16] new conflict interval 46000
c [simplification-16] penalized conflict interval 46000 = 1 * 46000
c [simplification-16] hard conflict limit 200717 (soft 177717 + delta 23000)
c [simplification-16] new conflict limit 177717 (hard 200717)
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  381.4   51848   375806    132374    7398   2581 1048901  365   563   66  65%      9   56  314  370   85%
c i  409.9   51817   375806    162710    9556   2593 1048914  167   186   95  90%    346 -233  127  313   40%
c i  429.1   51816   375806    185773   13080   2630 1048926  190   218  127  87%    209 -138  186  277   67%
c i  432.5   51814   375806    189259   13703   2633 1048929  204   228  127  90%    -84 -121  186  273   68%
c 
c [simplification-17] limit 177717 conflicts (hard 200717) hit after 200717 conflicts
c [quatres-9] found 28416 quaternary clauses 65% in total
c [quatres-9-2] added 1 single-self-subsuming ternary resolvents
c [ternres-12] limit 74680600 with penalty 0 = 0 + 0
c [ternres-12] all 51806 free variables schedulable
c [ternres-12] 146 ternary resolvents (4 bin, 142 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-41] removed 47 variables
c [basicprobe-6] limit 373403003 penalty 0 = 0 + 0
c [basicprobe-6-0] 14174 sched 29%, 1274 failed, 42 lifted, 896712 hbrs
c [decomp-42] removed 2497 variables
c [basicprobe-6-1] 14449 probes remain 29% after last round
c [basicprobe-6-1] 1339 units = 1297 failed (97%) + 42 lifted (3%)
c [basicprobe-6-1] removed 2520 variables, found 934427 hbrs
c [bate-4] eliminated 671 asymmetric tautologies during probing
c [unhide-17] limit 7468060 with penalty 1 = 0 + 1
c [unhide-17-26] 0 units, 32 failed, 136043 tauts, 0 hbrs, 54486 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 117 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 49263 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1608 variables 3% in round 1 in 33084653 steps
c [elim-13-1] backward subsumption/strengthening limit 33084600
c [elim-13-1-1] backward checking 8476 touched variables 17%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 39 and strengthened 54 clauses in 2140866 steps
c [elim-13-1] rescheduled 246 variables 0% by backward subsumption
c [elim-13-2] eliminated 19 variables 0% in round 2 in 315864 steps
c [elim-13-2] backward subsumption/strengthening limit 315800
c [elim-13-2-1] backward checking 246 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 13 and strengthened 6 clauses in 169086 steps
c [elim-13-2] rescheduled 45 variables 0% by backward subsumption
c [elim-13-3] eliminated 5 variables 0% in round 3 in 55752 steps
c [elim-13-3] backward subsumption/strengthening limit 55700
c [elim-13-3-1] backward checking 103 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 11 and strengthened 0 clauses in 55701 steps
c [elim-13] incomplete 12 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 1632 = 3% variables out of 49263 scheduled
c [bca-13] limit of 10000000 steps and 682518 added (scaled 2)
c [bca-13] 80352 out of 95264 literals actually usable 84%
c [bca-13] added 44 blocked clauses in 187846 steps
c [sweep-13] limit 22404180 penalty 0 = 0 + 0
c [sweep-13-1] 1706 pos 19.9% + 6853 neg 80.1% = 8559 sched 18.0% ret 39072
c [sweep-13-1] 22425219 steps 572 queries 177.02 avg class size
c [sweep-13-1] 4772 decisions 507 SAT calls 60.38 avg env size
c [sweep-13-1] 6958 variables remain 15% (40601 retained 85%)
c [decomp-43] removed 279 variables
c [sweep-13-1] removed 279 vars (0 failed, 64 eqs, 105 impls)
c [sweep-13] removed 279 vars in TOTAL (1 rounds, 571 queries)
c [phase-count-17] 339039 negative 99.8% of 339772 except 733 0.2%
c [phase-count-17] 257538 positive 75.8% of 339772 except 82234 24.2%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 10424 enqueued variables after 200717 conflicts
c [score-dist-17] active 36928 (78%), one 0 (0%), zero 10424 (22%)
c [score-dist-17] max exp 535, different 34 (6%)
c [score-dist-17] median active exp 526, avg 525.1
c [simplification-17] removed 4454 variables 8.6% (47352 remain 19%)
c [simplification-17] removed 36034 irredundant clauses 9.6% (339772 remain 25%)
c [simplification-17] maximum reduction of 10% = max (9%, 10%)
c [simplification-17] large reduction 10% >= 5% limit
c [simplification-17] next conflict interval 2007 = min (200717/100, 46000)
c [simplification-17] penalized conflict interval 2007 = 1 * 2007
c [simplification-17] hard conflict limit 212724 (soft 202724 + delta 10000)
c [simplification-17] new conflict limit 202724 (hard 212724)
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  468.1   47351   339772    201119   13004   2313 1324488  224   234   78  96%     43  -96  230  266   87%
c 
c [simplification-18] limit 202724 conflicts (hard 212724) hit after 212725 conflicts
c [quatres-10] found 26355 quaternary clauses 64% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 3 single-self-subsuming ternary resolvents
c [quatres-10-2] added 18 quaternary resolvents
c [ternres-13] limit 76955142 with penalty 0 = 0 + 0
c [ternres-13] all 47327 free variables schedulable
c [ternres-13] 828 ternary resolvents (0 bin, 828 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-44] removed 25 variables
c [simpleprobe-7] 22 schedulable variables 0%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-45] removed 85 variables
c [simpleprobe-7] 2212 variables remain 5% (45030 retained 95%)
c [simpleprobe-7] removed 85 variables, found 107092 hbrs, 29 units
c [unhide-18] limit 7695514 with penalty 1 = 0 + 1
c [unhide-18-29] 0 units, 16 failed, 130067 tauts, 0 hbrs, 55108 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 159 transitive binary clauses
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 47235 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 268 variables 1% in round 1 in 39382051 steps
c [elim-14-1] backward subsumption/strengthening limit 39382000
c [elim-14-1-1] backward checking 1900 touched variables 4%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 8 and strengthened 7 clauses in 626429 steps
c [elim-14-1] rescheduled 38 variables 0% by backward subsumption
c [elim-14-2] eliminated 3 variables 0% in round 2 in 89496 steps
c [elim-14-2] backward subsumption/strengthening limit 89400
c [elim-14-2-1] backward checking 30 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 3 and strengthened 0 clauses in 87919 steps
c [elim-14-2] rescheduled 5 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 40928 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 271 = 1% variables out of 47235 scheduled
c [elim-14] 271 < 1/100 * 47235 = 472 considered unsuccessful
c [bca-14] limit of 10000000 steps and 672578 added (scaled 2)
c [bca-14] 78473 out of 93930 literals actually usable 84%
c [bca-14] added 32 blocked clauses in 184891 steps
c [sweep-14] limit 23086542 penalty 0 = 0 + 0
c [sweep-14-1] 1307 pos 19.5% + 5398 neg 80.5% = 6705 sched 14.3% ret 40259
c [sweep-14-1] 23146168 steps 679 queries 124.72 avg class size
c [sweep-14-1] 5438 decisions 620 SAT calls 58.10 avg env size
c [sweep-14-1] 5054 variables remain 11% (41893 retained 89%)
c [decomp-46] removed 102 variables
c [sweep-14-1] removed 102 vars (0 failed, 60 eqs, 128 impls)
c [sweep-14] removed 102 vars in TOTAL (1 rounds, 678 queries)
c [phase-count-18] 334677 negative 99.8% of 335390 except 713 0.2%
c [phase-count-18] 254412 positive 75.9% of 335390 except 80978 24.1%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-18] sorted 10122 enqueued variables after 212725 conflicts
c [score-dist-18] active 36740 (78%), one 0 (0%), zero 10122 (22%)
c [score-dist-18] max exp 536, different 35 (7%)
c [score-dist-18] median active exp 526, avg 525.2
c [simplification-18] removed 465 variables 1.0% (46862 remain 19%)
c [simplification-18] removed 4382 irredundant clauses 1.3% (335390 remain 24%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 23000 = 46000 / 2
c [simplification-18] new conflict interval 69000
c [simplification-18] penalized conflict interval 69000 = 1 * 69000
c [simplification-18] hard conflict limit 316225 (soft 281725 + delta 34500)
c [simplification-18] new conflict limit 281725 (hard 316225)
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  494.9   46861   335390    227698   18960   2979 1276291  183   230   88  79%    245  -70   95  246   39%
c i  516.1   46842   335390    260075   26161   3018 1276322  146   270  112  54%    291   -1   53  225   24%
c 
c [simplification-19] limit 281725 conflicts (hard 316225) hit after 281725 conflicts
c [quatres-11] found 26210 quaternary clauses 62% in total
c [quatres-11-2] added 2 single-self-subsuming ternary resolvents
c [quatres-11-2] added 3 quaternary resolvents
c [ternres-14] limit 89746579 with penalty 0 = 0 + 0
c [ternres-14] all 46829 free variables schedulable
c [ternres-14] 168 ternary resolvents (1 bin, 167 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 1121832 penalty 4 = 4 + 0
c [gauss-5] extracted 18 xors of average arity 3.0
c [gauss-5] connected 54 occurrences of 51 variables (average 1.1)
c [gauss-5] limit 1121832 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-47] removed 1 variables
c [treelook-7] limit 8974657 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 66712 literals 71%
c [treelook-7] scheduling used 1851465 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 8974657 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 9089571 steps
c [treelook-7] 66631 literals remain 71%
c [treelook-7] 10473 variables remain to probed next time 22%
c [treelook-7] removed 0 variables, found 23287 hbrs
c [unhide-19] limit 2243664 with penalty 3 = 0 + 3
c [unhide-19-30] 0 units, 2 failed, 2627 tauts, 0 hbrs, 511593 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 113 transitive binary clauses
c [cce-6] limit of 56091612 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 134
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 133
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 132
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 131
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 130
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 129
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 128
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 127
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 126
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 125
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 124
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 123
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 122
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 121
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 120
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 119
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 117
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 116
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 115
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 114
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 113
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 111
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 110
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 109
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 108
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 107
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 106
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 105
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 104
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 103
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 102
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 101
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 100
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 99
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 98
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 97
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 96
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 95
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 94
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 93
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 92
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 91
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 90
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 89
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 88
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 87
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 86
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 85
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 84
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 83
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 82
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 81
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 80
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 79
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 78
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 77
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 76
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 75
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 74
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 73
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 72
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 71
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 70
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 69
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 68
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 67
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 66
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 65
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 64
c [cce-6-1] eliminated 7 clauses out of 8 (88%) of length 63
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 62
c [cce-6-1] eliminated 8 clauses out of 10 (80%) of length 61
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 60
c [cce-6-1] eliminated 8 clauses out of 9 (89%) of length 59
c [cce-6-1] eliminated 7 clauses out of 10 (70%) of length 58
c [cce-6-1] eliminated 8 clauses out of 10 (80%) of length 57
c [cce-6-1] eliminated 7 clauses out of 11 (64%) of length 56
c [cce-6-1] eliminated 10 clauses out of 12 (83%) of length 55
c [cce-6-1] eliminated 9 clauses out of 13 (69%) of length 54
c [cce-6-1] eliminated 9 clauses out of 12 (75%) of length 53
c [cce-6-1] eliminated 10 clauses out of 13 (77%) of length 52
c [cce-6-1] eliminated 11 clauses out of 14 (79%) of length 51
c [cce-6-1] eliminated 11 clauses out of 15 (73%) of length 50
c [cce-6-1] eliminated 10 clauses out of 13 (77%) of length 49
c [cce-6-1] eliminated 11 clauses out of 14 (79%) of length 48
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 47
c [cce-6-1] eliminated 12 clauses out of 15 (80%) of length 46
c [cce-6-1] eliminated 10 clauses out of 15 (67%) of length 45
c [cce-6-1] eliminated 11 clauses out of 13 (85%) of length 44
c [cce-6-1] eliminated 9 clauses out of 14 (64%) of length 43
c [cce-6-1] eliminated 12 clauses out of 14 (86%) of length 42
c [cce-6-1] eliminated 9 clauses out of 12 (75%) of length 41
c [cce-6-1] eliminated 11 clauses out of 14 (79%) of length 40
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 39
c [cce-6-1] eliminated 11 clauses out of 14 (79%) of length 38
c [cce-6-1] eliminated 11 clauses out of 15 (73%) of length 37
c [cce-6-1] eliminated 8 clauses out of 13 (62%) of length 36
c [cce-6-1] eliminated 12 clauses out of 13 (92%) of length 35
c [cce-6-1] eliminated 9 clauses out of 13 (69%) of length 34
c [cce-6-1] eliminated 11 clauses out of 14 (79%) of length 33
c [cce-6-1] eliminated 10 clauses out of 13 (77%) of length 32
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 31
c [cce-6-1] eliminated 11 clauses out of 14 (79%) of length 30
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 29
c [cce-6-1] eliminated 12 clauses out of 15 (80%) of length 28
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 27
c [cce-6-1] eliminated 11 clauses out of 15 (73%) of length 26
c [cce-6-1] eliminated 12 clauses out of 15 (80%) of length 25
c [cce-6-1] eliminated 11 clauses out of 16 (69%) of length 24
c [cce-6-1] eliminated 12 clauses out of 16 (75%) of length 23
c [cce-6-1] eliminated 13 clauses out of 18 (72%) of length 22
c [cce-6-1] eliminated 11 clauses out of 17 (65%) of length 21
c [cce-6-1] eliminated 15 clauses out of 19 (79%) of length 20
c [cce-6-1] eliminated 14 clauses out of 21 (67%) of length 19
c [cce-6-1] eliminated 18 clauses out of 23 (78%) of length 18
c [cce-6-1] eliminated 16 clauses out of 23 (70%) of length 17
c [cce-6-1] eliminated 15 clauses out of 23 (65%) of length 16
c [cce-6-1] eliminated 22 clauses out of 26 (85%) of length 15
c [cce-6-1] eliminated 19 clauses out of 28 (68%) of length 14
c [cce-6-1] eliminated 22 clauses out of 27 (81%) of length 13
c [cce-6-1] eliminated 19 clauses out of 28 (68%) of length 12
c [cce-6-1] eliminated 22 clauses out of 27 (81%) of length 11
c [cce-6-1] eliminated 24 clauses out of 37 (65%) of length 10
c [cce-6-1] eliminated 23 clauses out of 29 (79%) of length 9
c [cce-6-1] eliminated 23 clauses out of 33 (70%) of length 8
c [cce-6-1] eliminated 25 clauses out of 50 (50%) of length 7
c [cce-6-1] eliminated 26 clauses out of 2718 (1%) of length 6
c [cce-6-1] eliminated 25 clauses out of 9283 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 996 large clauses in 56091621 steps
c [cce-6-1] allowing another 28045810 steps for small clauses
c [cce-6-1] scheduling 278373 clauses = 171422 binary + 106951 ternary
c [cce-6-1] tried to eliminate 1534 small clauses 1%
c [cce-6-1] eliminated 259 binary clauses 0%
c [cce-6-1] eliminated 43 ternary clauses 0%
c [cce-6-1] eliminated 302 small clauses 0%
c [cce-6-1] eliminated 353 small clauses in 56091613 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1349 covered clauses in round 1
c [cce-6] eliminated 1349 covered clauses in TOTAL during 1 rounds
c [cce-6] 1349 < 1/100 * 333301 = 3333 considered unsuccessful
c [bca-15] limit of 10000000 steps and 665330 added (scaled 2)
c [bca-15] 73694 out of 93632 literals actually usable 79%
c [bca-15] added 1 blocked clauses in 203096 steps
c [sweep-15] limit 26923973 penalty 0 = 0 + 0
c [sweep-15-1] 1042 pos 20.9% + 3951 neg 79.1% = 4993 sched 10.7% ret 41822
c [sweep-15-1] 26944133 steps 725 queries 112.49 avg class size
c [sweep-15-1] 5821 decisions 653 SAT calls 74.83 avg env size
c [sweep-15-1] 3452 variables remain 7% (43290 retained 93%)
c [decomp-49] removed 191 variables
c [sweep-15-1] removed 191 vars (0 failed, 72 eqs, 133 impls)
c [sweep-15] removed 191 vars in TOTAL (1 rounds, 724 queries)
c [phase-count-19] 329970 negative 99.8% of 330687 except 717 0.2%
c [phase-count-19] 250560 positive 75.8% of 330687 except 80127 24.2%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 9532 enqueued variables after 281725 conflicts
c [score-dist-19] active 37092 (80%), one 0 (0%), zero 9532 (20%)
c [score-dist-19] max exp 536, different 35 (7%)
c [score-dist-19] median active exp 527, avg 526.1
c [simplification-19] removed 205 variables 0.4% (46624 remain 19%)
c [simplification-19] removed 4703 irredundant clauses 1.4% (330687 remain 24%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 34500 = 69000 / 2
c [simplification-19] new conflict interval 103500
c [simplification-19] penalized conflict interval 103500 = 1 * 103500
c [simplification-19] hard conflict limit 436975 (soft 385225 + delta 51750)
c [simplification-19] new conflict limit 385225 (hard 436975)
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 -  558.5   46624   330687    291552   24615   3247 1312364   31   331   94   9%    253   21   32  167   19%
c i  622.5   46623   330687    343444   40470   3296 1312386  292   321  277  91%    675   22  356  199  179%
c 
c [simplification-20] limit 385225 conflicts (hard 436975) hit after 385226 conflicts
c [quatres-12] found 26246 quaternary clauses 63% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [ternres-15] limit 119681525 with penalty 0 = 0 + 0
c [ternres-15] all 46622 free variables schedulable
c [ternres-15] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-50] removed 2 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 14235 sched 31%, 384 failed, 9 lifted, 451844 hbrs
c [decomp-51] removed 758 variables
c [basicprobe-7-1] 9026 probes remain 20% after last round
c [basicprobe-7-1] 438 units = 429 failed (98%) + 9 lifted (2%)
c [basicprobe-7-1] removed 815 variables, found 494675 hbrs
c [bate-5] eliminated 249 asymmetric tautologies during probing
c [unhide-20] limit 1250000 with penalty 4 = 0 + 4
c [unhide-20-31] 0 units, 23 failed, 127486 tauts, 0 hbrs, 3476200 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 136 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 45779 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 64 blocked clauses
c [block-6] 64 < 1/100 * 319580 = 3195 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 45777 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 429 variables 1% in round 1 in 28353228 steps
c [elim-15-1] backward subsumption/strengthening limit 28353200
c [elim-15-1-1] backward checking 3105 touched variables 7%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 19 and strengthened 9 clauses in 895462 steps
c [elim-15-1] rescheduled 76 variables 0% by backward subsumption
c [elim-15-2] eliminated 6 variables 0% in round 2 in 78039 steps
c [elim-15-2] backward subsumption/strengthening limit 78000
c [elim-15-2-1] backward checking 72 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 1 and strengthened 3 clauses in 78001 steps
c [elim-15-2] rescheduled 12 variables 0% by backward subsumption
c [elim-15-3] no variable eliminated in round 3 in 14310 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 435 = 1% variables out of 45777 scheduled
c [elim-15] 435 < 1/100 * 45777 = 457 considered unsuccessful
c [bca-16] limit of 10000000 steps and 638183 added (scaled 2)
c [bca-16] 69531 out of 90686 literals actually usable 77%
c [bca-16] added 19 blocked clauses in 201596 steps
c [sweep-16] limit 35904457 penalty 0 = 0 + 0
c [sweep-16-1] 590 pos 18.1% + 2669 neg 81.9% = 3259 sched 7.2% ret 42083
c [sweep-16-1] 35919869 steps 1476 queries 27.11 avg class size
c [sweep-16-1] 9172 decisions 1302 SAT calls 63.40 avg env size
c [sweep-16-1] 787 variables remain 2% (44517 retained 98%)
c [decomp-52] removed 293 variables
c [sweep-16-1] removed 293 vars (0 failed, 173 eqs, 271 impls)
c [sweep-16] removed 293 vars in TOTAL (1 rounds, 1475 queries)
c [phase-count-20] 317156 negative 99.8% of 317868 except 712 0.2%
c [phase-count-20] 238014 positive 74.9% of 317868 except 79854 25.1%
c [phase-count-20] skipping relative phase luck test
c [phase-20] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-20] sorted 8172 enqueued variables after 385226 conflicts
c [score-dist-20] active 36877 (82%), one 0 (0%), zero 8172 (18%)
c [score-dist-20] max exp 537, different 36 (7%)
c [score-dist-20] median active exp 528, avg 527.1
c [simplification-20] removed 1573 variables 3.4% (45049 remain 18%)
c [simplification-20] removed 12819 irredundant clauses 3.9% (317868 remain 23%)
c [simplification-20] maximum reduction of 4% = max (3%, 4%)
c [simplification-20] geometric conflict interval increment 20700 = 103500 / 5
c [simplification-20] new conflict interval 124200
c [simplification-20] penalized conflict interval 124200 = 1 * 124200
c [simplification-20] hard conflict limit 571526 (soft 509426 + delta 62100)
c [simplification-20] new conflict limit 509426 (hard 571526)
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 -  722.2   45049   317868    406018   26465   3194 1480315  384   396   88  97%    380   66  425  275  155%
c 
c [simplification-21] limit 509426 conflicts (hard 571526) hit after 509428 conflicts
c [quatres-13] found 26062 quaternary clauses 62% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 3 single-self-subsuming ternary resolvents
c [quatres-13-2] added 4 quaternary resolvents
c [ternres-16] limit 166751755 with penalty 0 = 0 + 0
c [ternres-16] all 45049 free variables schedulable
c [ternres-16] 296 ternary resolvents (1 bin, 295 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 5210992 penalty 4 = 4 + 0
c [card-6] found 2258 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 5210992 for elimination
c [card-6] 2258 out of 2258 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-53] removed 1 variables
c [simpleprobe-8] 1999 schedulable variables 4%
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-54] removed 35 variables
c [simpleprobe-8] 1472 variables remain 3% (43541 retained 97%)
c [simpleprobe-8] removed 35 variables, found 77116 hbrs, 8 units
c [unhide-21] limit 2500000 with penalty 3 = 0 + 3
c [unhide-21-33] 1 units, 6 failed, 95605 tauts, 0 hbrs, 291510 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 213 transitive binary clauses
c [bca-17] limit of 10000000 steps and 630650 added (scaled 2)
c [bca-17] 68899 out of 89994 literals actually usable 77%
c [bca-17] added 14 blocked clauses in 194141 steps
c [sweep-17] limit 50025526 penalty 0 = 0 + 0
c [sweep-17-1] 64 pos 9.1% + 639 neg 90.9% = 703 sched 1.6% ret 44293
c [sweep-17-1] 8294638 steps 545 queries 16.12 avg class size
c [sweep-17-1] 2816 decisions 480 SAT calls 55.28 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-55] removed 73 variables
c [sweep-17-1] removed 73 vars (0 failed, 65 eqs, 89 impls)
c [sweep-17-2] 8007 pos 17.8% + 36916 neg 82.2% = 44923 sched 100.0% ret 0
c [sweep-17-2] 41775582 steps 735 queries 414.39 avg class size
c [sweep-17-2] 17490 decisions 710 SAT calls 210.74 avg env size
c [sweep-17-2] 27584 variables remain 61% (17317 retained 39%)
c [decomp-56] removed 54 variables
c [sweep-17-2] removed 54 vars (0 failed, 24 eqs, 62 impls)
c [sweep-17] removed 127 vars in TOTAL (2 rounds, 1278 queries)
c [phase-count-21] 313615 negative 99.8% of 314329 except 714 0.2%
c [phase-count-21] 236142 positive 75.1% of 314329 except 78187 24.9%
c [phase-count-21] skipping relative phase luck test
c [phase-21] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-21] sorted 7827 enqueued variables after 509428 conflicts
c [score-dist-21] active 37042 (83%), one 0 (0%), zero 7827 (17%)
c [score-dist-21] max exp 538, different 37 (7%)
c [score-dist-21] median active exp 529, avg 527.7
c [simplification-21] removed 180 variables 0.4% (44869 remain 18%)
c [simplification-21] removed 3539 irredundant clauses 1.1% (314329 remain 23%)
c [simplification-21] maximum reduction of 1% = max (0%, 1%)
c [simplification-21] geometric conflict interval increment 62100 = 124200 / 2
c [simplification-21] new conflict interval 186300
c [simplification-21] penalized conflict interval 186300 = 1 * 186300
c [simplification-21] hard conflict limit 788878 (soft 695728 + delta 93150)
c [simplification-21] new conflict limit 695728 (hard 788878)
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 -  961.5   44869   314329    586822   24391   3433 1470707  590   610   82  97%    983   27  551  540  102%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2273 basic ate = 2129 trn 94% + 144 lrg 6% in 5 updates
c bcas: 17 count, 1887 added (289 skipped), 5805887 steps
c bkwd: tried 462471 clauses, 924679 lits, 2.00 lits/clause
c bkwd: checked 14722463 occs, 31.83 occs/clause, 15.92 occs/lit
c bkwd: subsumed 18 binary, 139 ternary, 40 large
c bkwd: strengthened 0 binary, 5 ternary (100% self), 1014 large (0% self)
c blkd: 6 bces, 13313 removed, 10637488 resolutions, 29672089 steps
c blkd: 15601 blocking literals 3%, 12 pure
c bump: 620001 bumped seen, 921127158 lits 1485.7 on average
c card: 6 count, 0 units, 0 am1, 472808229 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 78782 subsumed
c card: 20238 at-most-one constraints found, average size 4.70
c card: 20238 at-most-one constraints used 100%, average size 4.70
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: 6 cces, 44089 eliminated, 43900 ate 100%, 189 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: 4749826 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 159 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 56 decompositions, 10204 equivalent 4%
c deco: 474300 decision-only clauses 76%, 66% reduction
c decs: 6691269 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 106848 eliminated 41%, 121 pure 0%
c elms: 35 rounds, 2.3 rounds/bve
c elms: 85334 small 80%, 21381 large 20%
c elms: 207512 tried small, 85334 succeeded 41%, 122178 failed 59%
c elms: 59229 subsumed, 68443 strengthened, 1092 blocked
c elms: 22539004 copies, 22264131 resolutions, 5426619 ipos
c elms: 6964090 subchks, 4367837 strchks
c gaus: 5 extractions, 165 extracted, 2.6 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13900358 steps, 6950179 extr 50%, 675 elim 0%
c glue: 371.5 orig avg, 371.5 real avg, 11.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 3832994 = 552489 simple 14% + 3246941 trn 85% + 33564 lrg 1%, 6753 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 620001 clauses, 486.8 length
c lrnd: 301792242 lits = 727667036 orig - 425874794 removed 59%
c lrnd: 240701 uips 39%, 320460 flips 52%
c mins: 127760 mins 21%, 1025 bin 0%, 2283 size 0%
c mins: 120121324 poisoned searches, 32246506 hits, 27% hit rate
c mins: 133992962 used twice searches, 5520888 hits, 4% hit rate
c move: moved 24628, 17804 bin 72%, 6824 trn 28%
c otfs: 3443 driving 55%, 2772 restarting 45%
c otfs: str 6215, 6139 red 99%, 76 irr 1%
c otfs: str 6215, 0 bin 0%, 86 trn 1%, 6129 lrg 99%
c otfs: sub 34, 34 red 100%, 0 irr 0%
c otfs: sub 34, 0 bin 0%, 0 trn 0%, 34 lrg 100%
c phas: 21 computed, 145658 set, 119 pos (0%), 145539 neg (100%)
c prbs: 7 basic, 95819 probed, 4277 failed, 70 lifted
c prbs: 8 simple, 930925 probed, 2941 failed, 691 eqs
c prbs: 7 treelook, 360 probed, 24 failed, 0 lifted
c prom: 1774 locked 0% out of 865439 tried
c prps: 2277710784 props, 321 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 13 count, 48 quat, 15 self1, 0 self2, 899 dup
c queu: 21 sorted, 6691269 next (48706 steps 0.01)
c queu: 922167105 enq (2348747764 steps 2.55), 921127158 deq 100%
c redc: 2196 clauses 27%, 8223 tried 1%, 61 sat 1%
c redc: 6366 lits 8%, 81240 tried 0%, 61 sat 0%
c redc: 296 times jump level reduced, 120.0 levels on average
c reds: 3 count, 206805.7 conflicts per reduce
c reds: 0 memlim 0%, 3 arith 100%
c reds: 76530 collected 85%, 13711 retired 15%
c rmbd: 63396 removed, 19335 red 30%
c rsts: 6695 restarts 44%, 8502 skipped 56%
c rsts: 8502 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 21 count, 19 confs 90%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 620001 count (846561 tried 1.4), 451264 sub out of 616268 (73.2%)
c swps: 17 count, 18 rounds, 10769 queries (598.3/round)
c swps: 9605 sat calls, 80 unsat (0.3% success rate)
c swps: 91894 decisions 9.6, 3028 conflicts 0.3
c swps; 594.6 avg class size, 82.4 avg environment size
c swps: 1 failed, 2121 impls, 1199 equivs
c swp0: 3583 type 0 queries, 1689 unsat (47.1%), 3239 sat (90.4%)
c swp1: 7186 type 1 queries, 4214 unsat (58.6%), 6331 sat (88.1%)
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: 14623151 calls to obtain time
c tops: 98421 fixed 38%, 224 its, 2769.72 confs/it
c trds: 17 transitive reductions, 2823 removed, 3 failed
c trds: 13420 nodes, 46543 edges, 34013671 steps
c trim: 8661808 words, 33.0 MB
c trnr: 16 count, 11 bin, 3177 trn, 234034250 steps
c unhd: 21 count, 33 rounds, 129932465 steps
c unhd: 1244 non-trivial sccs of average size 2.2
c unhd: 72 units, 70 bin, 2 trn, 0 lrg
c unhd: 12777 failed, 12560 stamp, 0 lits, 194 bin, 8 trn, 0 lrg
c unhd: 983388 tauts, 15703 bin 2%, 8890 trn 1%, 183 lrg 0%
c unhd: 983388 tauts, 958612 stamp 97%, 904670 red 92%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5528923 str, 70 bin 0%, 2981 trn 0%, 5525872 lrg 100%, 5509865 red 100%
c vars: 44869 remaining 17% and 215473 removed 83% out of 260342
c vars: 98421 fixed 38%, 106848 eliminated 41%, 10204 equivalent 4%
c vsts: 21176014350 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 9.3 search visits per propagation, 32272.7 per conflict
c wchs: 851529235 pushed, 58472075 enlarged, 236 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         616316         76530         13711      47235296      15391983        268407
c 
c  0 0          7055   1        41   0         0   0  15172989  32   2314021  15     20941   8     0.3
c  1 5          1719   0        78   0       129   1   3706732   8    827919   5      5310   2     0.2
c  2 6          5004   1       348   0       170   1   4065957   9   1161231   8     10520   4     0.8
c  3 9          7730   1      1446   2       258   2   4577946  10<  1513327  10     13031   5     2.2
c  4 14        10119   2      3591   5       216   2   3698424   8   1337543   9     12291   5     6.4
c  5 21        14171   2      8014  10       436   3   3703131   8   1287394   8<    14415   5    20.1
c  6 30        14670   2      9088  12       339   2   2604932   6   1087125   7     13523   5    31.0
c  7 41        12953   2      7228   9       296   2   2073735   4   1154197   7     14438   5    21.5
c  8 54        11728   2      6344   8       260   2   1614973   3    855656   6     14553   5<   16.4
c  9 69        12356   2      7362  10<      253   2   1367975   3    797740   5     15294   6    22.0
c 10 86        17582   3      9668  13       417   3   2031954   4   1295853   8     45773  17    18.1
c 11 126       82593  13<     7260   9      1551  11<  1528581   3   1039619   7     42400  16    28.5
c 12 230      187726  30      9240  12      4670  34    739467   2    516567   3     41309  15    69.3
c 13 534      230910  37      6822   9      4716  34    348500   1    203791   1      4609   2   180.6
c 
c avg                 11.1           8.6          11.0           3.5           5.3           7.8
c std                  2.8           2.9           2.8           3.6           3.8           3.9
c 
c  199.515  20% bump
c   77.513   8% probe
c   43.054   4% unhide
c   30.510   3% sweep
c   21.206   2% elim
c   18.162   2% cce
c    4.929   0% bca
c    4.410   0% decide
c 
c   11.051 < 1% rest (below)
c 
c    3.945   0% block
c    2.206   0% gauss
c    2.074   0% transred
c    1.505   0% ternres
c    0.846   0% quatres
c    0.476   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.093   1% preprocessing     2%
c  218.911  22% inprocessing     98%
c ==================================
c  224.004  22% simplifying
c  775.189  78% search
c ==================================
c  999.197 100% all
c 
c        620417 conflicts,         620.9 confs/sec
c          1347 ternaries,         460.6 confs/ternary
c          1251 binaries,          495.9 confs/binary
c           224 iterations,       2769.7 confs/iteration
c 
c             3 reductions,          0.0 redus/sec, 206805.7 confs/reduction
c          6695 restarts,            6.7 rests/sec,     92.7 confs/restart
c       6691269 decisions,        6696.6 decis/sec,     10.8 decis/conflict
c    2277710784 propagations,  2279542.0 props/sec,    340.4 props/decision
c 
c 999.2 seconds, 483.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
