c launch: /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c host: atom05
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/manol-pipe-g10bid_i.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c no embedded options
c found 'p cnf 266405 792175' header
c read 266405 variables, 792175 clauses, 1848407 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=2
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 266404 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] VMTF (--score=2)
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  266404   792174         0       0      0     0    0     0   44   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 1 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 1 out of 1 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 1 at-most-one constraints, 1 used 100%
c [card-1] exported 1 binary clauses, 1.0 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 266404 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 7402 variables
c [simpleprobe-1] 91801 variables remain 35% (167201 retained 65%)
c [simpleprobe-1] removed 7402 variables, found 953 hbrs, 86 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 83 failed, 201 tauts, 0 hbrs, 171 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 257663 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 64530 not tried 25% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 193123 = 75% variables out of 257663 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 313684 negative 95.8% of 327495 except 13811 4.2%
c [phase-count-1] 311324 positive 95.1% of 327495 except 16171 4.9%
c [phase-1] phase bias: 23065 positive 36%, 41475 negative 64%
c [sort-queue-1] sorted 64540 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 64540 (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 201864 variables 75.8% (64540 remain 24%)
c [simplification-1] removed 464679 irredundant clauses 58.7% (327495 remain 41%)
c [simplification-1] maximum reduction of 76% = max (76%, 59%)
c [simplification-1] large reduction 76% >= 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.2   64539   327495        20      13      1    55    0     0   37   4%      0    0    0    0 24521%
c i    5.3   64527   327495       170     124     15    59    0     4   37   4%      0    4    2    0 18888%
c i    5.6   64514   327495       442     326     45    67    1    30   38   2%      1   30    6    0 14093%
c i    5.6   64502   327495       473     339     50    77    1    30   38   2%      1   30    5    0 13016%
c i    5.6   64430   327495       474     339     50    77    1    30   38   2%      1   30    5    0 12966%
c i    5.6   64372   327495       514     365     54    79    1    32   38   2%      1   32    6    0 12245%
c i    5.6   64331   327495       530     369     58    82    1    32   38   2%      1   32    5    0 11640%
c i    5.6   64264   327495       532     369     59    82    1    32   38   2%      1   32    5    0 11555%
c i    5.6   64262   327495       534     369     59    83    1    32   38   2%      1   32    5    0 11470%
c i    5.9   64261   327495       748     517     82    95    1    44   38   2%      1   44    6    0 9370%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 577 variables
c [simpleprobe-2] 22415 schedulable variables 35%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 22463 variables remain 35% (41500 retained 65%)
c [simpleprobe-2] removed 0 variables, found 67 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 37064 literals 29%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302800 steps
c [treelook-1] 36946 literals remain 29%
c [treelook-1] 31965 variables remain to probed next time 50%
c [decomp-5] removed 1 variables
c [treelook-1] removed 30 variables, found 454 hbrs
c [basicprobe-1] limit 2587848 based on 323481 irredundant clauses
c [basicprobe-1-0] 30965 probes remain 51% after last round
c [basicprobe-1-0] 1625 units = 879 failed (54%) + 746 lifted (46%)
c [basicprobe-1-0] removed 2751 variables, found 2745 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 33 units, 84 failed, 108 tauts, 0 hbrs, 2370 literals
c [elim-2] 60986 variables 100% will be scheduled this time
c [elim-2] scheduled 60986 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 13743 not tried 23% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 26846 = 44% variables out of 60986 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 240122 negative 97.0% of 247610 except 7488 3.0%
c [phase-count-2] 240325 positive 97.1% of 247610 except 7285 2.9%
c [phase-2] phase bias: 0 positive 0%, 19 negative 100%
c [sort-queue-2] sorted 34152 enqueued variables after 748 conflicts
c [score-dist-2] active 0 (0%), one 3691 (11%), zero 30461 (89%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 30093 variables 46.8% (34152 remain 13%)
c [simplification-2] removed 79885 irredundant clauses 24.4% (247610 remain 31%)
c [simplification-2] maximum reduction of 47% = max (47%, 24%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1020 (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    8.8   34151   247610       852     239     39   437    1    49   35   2%      1   49    7    0 8768%
c i    8.8   34148   247610       874     258     39   437    1    50   35   3%      1   50    8    0 9270%
c i    8.8   34131   247610       904     280     39   438    1    52   35   3%      1   52    8    0 9003%
c 
c [simplification-3] limit 1020 conflicts (hard 11000) hit after 1020 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 60 at-most-one constraints of average size 3.0
c [card-2] found 15 at-most-two constraints of average size 4.4
c [card-2] using previous limit 1000000 for elimination
c [card-2] 75 out of 75 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 104 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 19692 literals 29%
c [treelook-2] scheduling used 300030 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 305702 steps
c [treelook-2] 19567 literals remain 29%
c [treelook-2] 11590 variables remain to probed next time 34%
c [treelook-2] removed 67 variables, found 84 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 12 units, 34 failed, 2326 tauts, 0 hbrs, 5683 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 33940 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 3732 not tried 11% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1638 = 5% variables out of 33940 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 230954 negative 97.0% of 238165 except 7211 3.0%
c [phase-count-3] 231955 positive 97.4% of 238165 except 6210 2.6%
c [phase-3] phase bias: 1 positive 50%, 1 negative 50%
c [sort-queue-3] sorted 32302 enqueued variables after 1020 conflicts
c [score-dist-3] active 0 (0%), one 4234 (13%), zero 28068 (87%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 1827 variables 5.4% (32302 remain 12%)
c [simplification-3] removed 9445 irredundant clauses 3.8% (238165 remain 30%)
c [simplification-3] maximum reduction of 5% = max (5%, 4%)
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 13020 (soft 3020 + delta 10000)
c [simplification-3] new conflict limit 3020 (hard 13020)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   10.8   32301   238164      1194     424     68   381    2    57   35   3%      1   56    7    0 6406%
c i   10.8   32299   238164      1195     424     68   381    2    56   35   3%      1   56    7    0 6381%
c i   10.9   32296   238164      1594     682    101   392    2    60   35   3%      2   59    7    0 4781%
c i   11.0   32295   238164      1980     906    131   402    2    69   35   4%      2   68    7    0 3686%
c i   11.1   32294   238164      2657    1302    174   418    3    76   35   4%      4   74    7    0 2955%
c i   11.1   32287   238164      2910    1479    184   420    3    81   35   4%      4   79    8    0 2827%
c 
c [simplification-4] limit 3030 conflicts (hard 13020) hit after 3030 conflicts
c [decomp-8] removed 36 variables
c [basicprobe-2] limit 1901520 based on 237690 irredundant clauses
c [basicprobe-2-0] 14053 sched 44%, 147 failed, 49 lifted, 1294 hbrs
c [decomp-9] removed 525 variables
c [basicprobe-2-1] 15871 probes remain 50% after last round
c [basicprobe-2-1] 199 units = 150 failed (75%) + 49 lifted (25%)
c [basicprobe-2-1] removed 531 variables, found 1360 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 4 units, 16 failed, 79 tauts, 0 hbrs, 2444 literals
c [elim-4] 3574 variables 11% will be scheduled this time
c [elim-4] scheduled 3574 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 97125543 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 7 = 0% variables out of 3574 scheduled
c [elim-4] 7 < 1/100 * 3574 = 35 considered unsuccessful
c [phase-count-4] 222952 negative 96.9% of 230073 except 7121 3.1%
c [phase-count-4] 224539 positive 97.6% of 230073 except 5534 2.4%
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-4] sorted 31709 enqueued variables after 3030 conflicts
c [score-dist-4] active 0 (0%), one 6765 (21%), zero 24944 (79%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 578 variables 1.8% (31709 remain 12%)
c [simplification-4] removed 8091 irredundant clauses 3.4% (230073 remain 29%)
c [simplification-4] maximum reduction of 3% = max (2%, 3%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 5000
c [simplification-4] penalized conflict interval 5000 = 1 * 5000
c [simplification-4] hard conflict limit 18030 (soft 8030 + delta 10000)
c [simplification-4] new conflict limit 8030 (hard 18030)
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.5   31708   230073      5339    3054    278  1122    5   100   34   5%     23   95    9    1 1719%
c 
c [simplification-5] limit 8030 conflicts (hard 18030) hit after 8030 conflicts
c [quatres-1] found 26496 quaternary clauses 23% in total
c [quatres-1-2] added 252 single-self-subsuming ternary resolvents
c [quatres-1-2] added 6543 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 31706 free variables schedulable
c [ternres-1] 11953 ternary resolvents (294 bin, 11659 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 18386 xors of average arity 3.0
c [gauss-1] connected 55050 occurrences of 7021 variables (average 7.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 80 variables
c [unhide-5] limit 111494 with penalty 0 = 0 + 0
c [unhide-5-5] 6 units, 12 failed, 340 tauts, 0 hbrs, 2065 literals
c [transred-1] limit 557474 with penalty 0 = 0 + 0
c [transred-1] removed 132 transitive binary clauses
c [transred-1] found 2 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 31588 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 6530 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 21 (14%) of length 24
c [cce-1-1] eliminated 2 clauses out of 70 (3%) of length 22
c [cce-1-1] eliminated 12 clauses out of 93 (13%) of length 21
c [cce-1-1] eliminated 14 clauses out of 136 (10%) of length 20
c [cce-1-1] eliminated 18 clauses out of 192 (9%) of length 19
c [cce-1-1] eliminated 17 clauses out of 281 (6%) of length 18
c [cce-1-1] eliminated 12 clauses out of 358 (3%) of length 17
c [cce-1-1] eliminated 36 clauses out of 383 (9%) of length 16
c [cce-1-1] eliminated 46 clauses out of 465 (10%) of length 15
c [cce-1-1] eliminated 79 clauses out of 667 (12%) of length 14
c [cce-1-1] eliminated 83 clauses out of 698 (12%) of length 13
c [cce-1-1] eliminated 139 clauses out of 1102 (13%) of length 12
c [cce-1-1] eliminated 288 clauses out of 1982 (15%) of length 11
c [cce-1-1] eliminated 320 clauses out of 2389 (13%) of length 10
c [cce-1-1] eliminated 666 clauses out of 4376 (15%) of length 9
c [cce-1-1] eliminated 563 clauses out of 7452 (8%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2298 large clauses in 30000883 steps
c [cce-1-1] allowing another 15000441 steps for small clauses
c [cce-1-1] scheduling 100846 clauses = 26143 binary + 74703 ternary
c [cce-1-1] tried to eliminate 17503 small clauses 17%
c [cce-1-1] eliminated 99 binary clauses 0%
c [cce-1-1] eliminated 190 ternary clauses 0%
c [cce-1-1] eliminated 289 small clauses 0%
c [cce-1-1] eliminated 289 small clauses in 30000042 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2587 covered clauses in round 1
c [cce-1] eliminated 2587 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 439998 added (scaled 2)
c [bca-1] 48688 out of 62622 literals actually usable 78%
c [bca-1] added 82 blocked clauses in 154768 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 11575 pos 37.0% + 19735 neg 63.0% = 31310 sched 100.0% ret 0
c [sweep-1-1] 1010330 steps 105 queries 6110.63 avg class size
c [sweep-1-1] 3295 decisions 104 SAT calls 53.08 avg env size
c [sweep-1-1] 29361 variables remain 94% (1949 retained 6%)
c [decomp-11] removed 30 variables
c [sweep-1-1] removed 30 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 30 vars in TOTAL (1 rounds, 104 queries)
c [sort-queue-5] sorted 31280 enqueued variables after 8030 conflicts
c [score-dist-5] active 0 (0%), one 10501 (34%), zero 20779 (66%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 426 variables 1.3% (31280 remain 12%)
c [simplification-5] removed 10424 irredundant clauses 4.5% (219649 remain 28%)
c [simplification-5] maximum reduction of 5% = max (1%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 20030 (soft 10030 + delta 10000)
c [simplification-5] new conflict limit 10030 (hard 20030)
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   16.4   31279   219649      8171   11044  14820  2652    6   119   36   5%     29  110    8    1 1043%
c i   16.5   31276   219649      8575   11316  14840  2654    6   118   36   5%     20  108    8    1  997%
c 
c [simplification-6] limit 10030 conflicts (hard 20030) hit after 10030 conflicts
c [quatres-2] found 31694 quaternary clauses 27% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 148 single-self-subsuming ternary resolvents
c [quatres-2-2] added 3430 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 31270 free variables schedulable
c [ternres-2] 301 ternary resolvents (15 bin, 286 trn)
c [ternres-2] 19194 variables remain 61% (12076 retained 39%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 98 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 98 out of 98 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 11 variables
c [simpleprobe-3] 10997 schedulable variables 35%
c [simpleprobe-3] limit 1418755 penalty 1 = 1 + 0
c [simpleprobe-3] 11015 variables remain 35% (20254 retained 65%)
c [simpleprobe-3] removed 0 variables, found 23 hbrs, 0 units
c [unhide-6] limit 141875 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 21 failed, 1197 tauts, 0 hbrs, 1823 literals
c [transred-2] limit 709377 with penalty 0 = 0 + 0
c [transred-2] removed 120 transitive binary clauses
c [transred-2] found 11 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 31219 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 1949 blocked clauses
c [block-2] 1949 < 1/100 * 219468 = 2194 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 413 (0%) of length 15
c [cce-2-1] eliminated 4 clauses out of 2028 (0%) of length 10
c [cce-2-1] eliminated 2 clauses out of 3613 (0%) of length 9
c [cce-2-1] eliminated 226 clauses out of 6755 (3%) of length 8
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 233 large clauses in 30000098 steps
c [cce-2-1] allowing another 15000049 steps for small clauses
c [cce-2-1] scheduling 35249 clauses = 25694 binary + 9555 ternary
c [cce-2-1] tried to eliminate 17406 small clauses 49%
c [cce-2-1] eliminated 167 binary clauses 1%
c [cce-2-1] eliminated 136 ternary clauses 1%
c [cce-2-1] eliminated 303 small clauses 1%
c [cce-2-1] eliminated 303 small clauses in 30000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 536 covered clauses in round 1
c [cce-2] eliminated 536 covered clauses in TOTAL during 1 rounds
c [cce-2] 536 < 1/100 * 217041 = 2170 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 30780 variables 100%
c [elim-5] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 5144 not tried 17% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1607 = 5% variables out of 30780 scheduled
c [bca-2] limit of 10000000 steps and 428469 added (scaled 2)
c [bca-2] 43954 out of 58348 literals actually usable 75%
c [bca-2] added 61 blocked clauses in 147554 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 10180 pos 37.3% + 17126 neg 62.7% = 27306 sched 93.6% ret 1867
c [sweep-2-1] 1004044 steps 153 queries 4340.83 avg class size
c [sweep-2-1] 4444 decisions 152 SAT calls 41.92 avg env size
c [sweep-2-1] 25443 variables remain 87% (3728 retained 13%)
c [decomp-14] removed 6 variables
c [sweep-2-1] removed 6 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 6 vars in TOTAL (1 rounds, 152 queries)
c [sort-queue-6] sorted 29167 enqueued variables after 10030 conflicts
c [score-dist-6] active 0 (0%), one 11222 (38%), zero 17945 (62%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 2103 variables 6.7% (29167 remain 11%)
c [simplification-6] removed 5753 irredundant clauses 2.6% (213896 remain 27%)
c [simplification-6] maximum reduction of 7% = max (7%, 3%)
c [simplification-6] large reduction 7% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 22030 (soft 12030 + delta 10000)
c [simplification-6] new conflict limit 12030 (hard 22030)
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.3   29166   213896     11818   14862   9637  1863    7   132   35   5%     34  118   10    1  891%
c 
c [simplification-7] limit 12030 conflicts (hard 22030) hit after 12032 conflicts
c [quatres-3] found 32608 quaternary clauses 27% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 2 double-self-subsuming ternary resolvents
c [quatres-3-2] added 129 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2721 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 17929 schedulable variables 61%
c [ternres-3] 505 ternary resolvents (18 bin, 487 trn)
c [ternres-3] 5155 variables remain 18% (24009 retained 82%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 9145 xors of average arity 3.0
c [gauss-2] connected 27435 occurrences of 5089 variables (average 5.4)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 14762 literals 25%
c [treelook-3] scheduling used 300030 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 301949 steps
c [treelook-3] 14633 literals remain 25%
c [treelook-3] 7879 variables remain to probed next time 27%
c [decomp-16] removed 1 variables
c [treelook-3] removed 3 variables, found 33 hbrs
c [unhide-7] limit 166155 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 1 failed, 262 tauts, 0 hbrs, 1097 literals
c [transred-3] limit 830778 with penalty 0 = 0 + 0
c [transred-3] removed 83 transitive binary clauses
c [transred-3] found 3 units
c [elim-6] 5136 variables 18% will be scheduled this time
c [elim-6] scheduled 5136 variables 18%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 2196 not tried 8% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 5136 scheduled
c [bca-3] limit of 10000000 steps and 427461 added (scaled 2)
c [bca-3] 42514 out of 58310 literals actually usable 73%
c [bca-3] added 7 blocked clauses in 146371 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 9534 pos 37.5% + 15900 neg 62.5% = 25434 sched 87.2% ret 3720
c [sweep-3-1] 1009909 steps 167 queries 4280.38 avg class size
c [sweep-3-1] 4378 decisions 163 SAT calls 39.24 avg env size
c [sweep-3-1] 23656 variables remain 81% (5498 retained 19%)
c [decomp-17] removed 2 variables
c [sweep-3-1] removed 2 vars (0 failed, 3 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 2 vars in TOTAL (1 rounds, 166 queries)
c [sort-queue-7] sorted 29152 enqueued variables after 12032 conflicts
c [score-dist-7] active 0 (0%), one 11702 (40%), zero 17450 (60%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 12 variables 0.0% (29152 remain 11%)
c [simplification-7] removed 451 irredundant clauses 0.2% (213445 remain 27%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 25000
c [simplification-7] penalized conflict interval 25000 = 1 * 25000
c [simplification-7] hard conflict limit 49532 (soft 37032 + delta 12500)
c [simplification-7] new conflict limit 37032 (hard 49532)
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   23.3   29151   213445     17690   21514  10438  1889    7   120   36   6%     70   98    8    2  490%
c i   24.6   29150   213445     24455   26324  10734  1914    8   110   36   7%     80   79    7    2  348%
c i   24.7   29145   213445     25005   26734  10761  1917    7   109   36   7%     44   77    7    2  319%
c i   26.3   29141   213445     32648   32322  11101  1945    7   105   36   7%     88   66    8    3  299%
c 
c [simplification-8] limit 37032 conflicts (hard 49532) hit after 37033 conflicts
c [quatres-4] found 36477 quaternary clauses 29% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 5 double-self-subsuming ternary resolvents
c [quatres-4-2] added 122 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1478 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 5150 schedulable variables 18%
c [ternres-4] 1223 ternary resolvents (49 bin, 1174 trn)
c [ternres-4] 22 variables remain 0% (29114 retained 100%)
c [decomp-18] removed 32 variables
c [basicprobe-3] limit 12296947 penalty 0 = 0 + 0
c [basicprobe-3-0] 14670 sched 51%, 47 failed, 0 lifted, 1023 hbrs
c [decomp-19] removed 124 variables
c [basicprobe-3-1] 15302 sched 53%, 9 failed, 0 lifted, 228 hbrs
c [decomp-20] removed 23 variables
c [basicprobe-3-2] 15304 sched 53%, 1 failed, 0 lifted, 44 hbrs
c [decomp-21] removed 2 variables
c [basicprobe-3-3] 15299 sched 53%, 3 failed, 0 lifted, 23 hbrs
c [decomp-22] removed 4 variables
c [basicprobe-3-4] 15292 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-5] 14946 probes remain 52% after last round
c [basicprobe-3-5] 60 units = 60 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 153 variables, found 1319 hbrs
c [bate-1] eliminated 257 asymmetric tautologies during probing
c [unhide-8] limit 491877 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 0 failed, 1285 tauts, 0 hbrs, 8510 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 132 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 28967 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1192 blocked clauses
c [block-3] 1192 < 1/100 * 211020 = 2110 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 29
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 27
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 26
c [cce-3-1] eliminated 1 clauses out of 13 (8%) of length 25
c [cce-3-1] eliminated 1 clauses out of 20 (5%) of length 24
c [cce-3-1] eliminated 9 clauses out of 38 (24%) of length 23
c [cce-3-1] eliminated 1 clauses out of 64 (2%) of length 22
c [cce-3-1] eliminated 2 clauses out of 67 (3%) of length 21
c [cce-3-1] eliminated 2 clauses out of 136 (1%) of length 20
c [cce-3-1] eliminated 5 clauses out of 196 (3%) of length 19
c [cce-3-1] eliminated 8 clauses out of 310 (3%) of length 18
c [cce-3-1] eliminated 13 clauses out of 365 (4%) of length 17
c [cce-3-1] eliminated 12 clauses out of 387 (3%) of length 16
c [cce-3-1] eliminated 13 clauses out of 485 (3%) of length 15
c [cce-3-1] eliminated 26 clauses out of 693 (4%) of length 14
c [cce-3-1] eliminated 56 clauses out of 786 (7%) of length 13
c [cce-3-1] eliminated 62 clauses out of 1265 (5%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 217 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 32765 clauses = 23904 binary + 8861 ternary
c [cce-3-1] tried to eliminate 5123 small clauses 16%
c [cce-3-1] eliminated 53 binary clauses 0%
c [cce-3-1] eliminated 81 ternary clauses 1%
c [cce-3-1] eliminated 134 small clauses 0%
c [cce-3-1] eliminated 134 small clauses in 15000043 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 351 covered clauses in round 1
c [cce-3] eliminated 351 covered clauses in TOTAL during 1 rounds
c [cce-3] 351 < 1/100 * 209828 = 2098 considered unsuccessful
c [bca-4] limit of 10000000 steps and 419529 added (scaled 2)
c [bca-4] 37474 out of 57616 literals actually usable 65%
c [bca-4] added 11 blocked clauses in 148401 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 8561 pos 36.6% + 14849 neg 63.4% = 23410 sched 81.3% ret 5397
c [sweep-4-1] 1001926 steps 146 queries 4387.36 avg class size
c [sweep-4-1] 3334 decisions 140 SAT calls 34.76 avg env size
c [sweep-4-1] 22204 variables remain 77% (6603 retained 23%)
c [decomp-24] removed 11 variables
c [sweep-4-1] removed 11 vars (0 failed, 9 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 11 vars in TOTAL (1 rounds, 145 queries)
c [sort-queue-8] sorted 28796 enqueued variables after 37033 conflicts
c [score-dist-8] active 0 (0%), one 14540 (50%), zero 14256 (50%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 340 variables 1.2% (28796 remain 11%)
c [simplification-8] removed 4009 irredundant clauses 1.9% (209436 remain 26%)
c [simplification-8] maximum reduction of 2% = max (1%, 2%)
c [simplification-8] geometric conflict interval increment 8333 = 25000 / 3
c [simplification-8] new conflict interval 33333
c [simplification-8] penalized conflict interval 33333 = 1 * 33333
c [simplification-8] hard conflict limit 87032 (soft 70366 + delta 16666)
c [simplification-8] new conflict limit 70366 (hard 87032)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   34.5   28795   209436     51187   46779  12207  2547    8   124   39   6%    227   67    7    4  191%
c 
c [simplification-9] limit 70366 conflicts (hard 87032) hit after 70366 conflicts
c [quatres-5] found 39353 quaternary clauses 29% in total
c [quatres-5-1] removed 13 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 111 single-self-subsuming ternary resolvents
c [quatres-5-2] added 344 quaternary resolvents
c [ternres-5] limit 5167221 with penalty 0 = 0 + 0
c [ternres-5] 20 schedulable variables 0%
c [ternres-5] 1436 ternary resolvents (57 bin, 1379 trn)
c [ternres-5] 1 variables remain 0% (28792 retained 100%)
c [decomp-25] removed 11 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 125 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 28785 variables 100%
c [elim-7] limit of 51672211 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 1077 not tried 4% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 537 = 2% variables out of 28785 scheduled
c [bca-5] limit of 10000000 steps and 415998 added (scaled 2)
c [bca-5] 33279 out of 56498 literals actually usable 59%
c [bca-5] added 19 blocked clauses in 159659 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 15501660 penalty 0 = 0 + 0
c [sweep-5-1] 9658 pos 44.4% + 12110 neg 55.6% = 21768 sched 77.1% ret 6480
c [sweep-5-1] 15509508 steps 2609 queries 478.00 avg class size
c [sweep-5-1] 54970 decisions 2602 SAT calls 30.49 avg env size
c [sweep-5-1] 4310 variables remain 15% (23935 retained 85%)
c [decomp-26] removed 39 variables
c [sweep-5-1] removed 39 vars (0 failed, 38 eqs, 21 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 39 vars in TOTAL (1 rounds, 2608 queries)
c [sort-queue-9] sorted 28209 enqueued variables after 70366 conflicts
c [score-dist-9] active 0 (0%), one 16888 (60%), zero 11321 (40%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 584 variables 2.0% (28209 remain 11%)
c [simplification-9] removed 1942 irredundant clauses 0.9% (207494 remain 26%)
c [simplification-9] maximum reduction of 2% = max (2%, 1%)
c [simplification-9] geometric conflict interval increment 11111 = 33333 / 3
c [simplification-9] new conflict interval 44444
c [simplification-9] penalized conflict interval 44444 = 1 * 44444
c [simplification-9] hard conflict limit 137032 (soft 114810 + delta 22222)
c [simplification-9] new conflict limit 114810 (hard 137032)
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   51.1   28208   207494     95599   79690  13643  2186    8    90   43   9%    470    8    8    6  140%
c -   53.2   28200   207494    101892   40852  13834  2195    8   106   38   7%   -118   23    8    6  134%
c 
c [simplification-10] limit 114810 conflicts (hard 137032) hit after 114810 conflicts
c [quatres-6] found 40529 quaternary clauses 28% in total
c [quatres-6-1] removed 32 duplicate quaternary clauses
c [quatres-6-2] added 161 single-self-subsuming ternary resolvents
c [quatres-6-2] added 268 quaternary resolvents
c [ternres-6] limit 8774978 with penalty 0 = 0 + 0
c [ternres-6] all 28200 free variables schedulable
c [ternres-6] 671 ternary resolvents (35 bin, 636 trn)
c [ternres-6] 500 variables remain 2% (27700 retained 98%)
c [card-4] limit 548436 penalty 3 = 3 + 0
c [card-4] found 110 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 548436 for elimination
c [card-4] 110 out of 110 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 4062 xors of average arity 3.0
c [gauss-3] connected 12185 occurrences of 3127 variables (average 3.9)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-9] limit 877497 with penalty 1 = 1 + 0
c [unhide-9-9] 0 units, 2 failed, 352 tauts, 0 hbrs, 9779 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 130 transitive binary clauses
c [transred-6] found 2 units
c [elim-8] 1073 variables 4% will be scheduled this time
c [elim-8] scheduled 1073 variables 4%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3509991400 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 140866386 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 1073 scheduled
c [bca-6] limit of 10000000 steps and 410674 added (scaled 2)
c [bca-6] 36754 out of 56396 literals actually usable 65%
c [bca-6] added 13 blocked clauses in 164662 steps
c [sweep-6] limit 2632493 penalty 0 = 0 + 0
c [sweep-6-1] 1904 pos 44.2% + 2406 neg 55.8% = 4310 sched 15.3% ret 23887
c [sweep-6-1] 2632992 steps 891 queries 847.37 avg class size
c [sweep-6-1] 11473 decisions 885 SAT calls 18.61 avg env size
c [sweep-6-1] 2629 variables remain 9% (25568 retained 91%)
c [decomp-28] removed 9 variables
c [sweep-6-1] removed 9 vars (0 failed, 8 eqs, 9 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 9 vars in TOTAL (1 rounds, 890 queries)
c [sort-queue-10] sorted 28188 enqueued variables after 114810 conflicts
c [score-dist-10] active 0 (0%), one 18104 (64%), zero 10084 (36%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 12 variables 0.0% (28188 remain 11%)
c [simplification-10] removed 2500 irredundant clauses 1.2% (204994 remain 26%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 22222 = 44444 / 2
c [simplification-10] new conflict interval 66666
c [simplification-10] penalized conflict interval 66666 = 1 * 66666
c [simplification-10] hard conflict limit 214809 (soft 181476 + delta 33333)
c [simplification-10] new conflict limit 181476 (hard 214809)
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   62.4   28187   204994    127613   62040  15173  2111    8    93   40   8%    252    6    7    6  117%
c i   65.1   28185   204994    137563   70102  15459  2122    8   105   41   7%    -76   18    8    7  128%
c i   75.0   28182   204994    178748  104018  16396  2159    8   147   44   5%    353   46    6    7   89%
c -   75.0   28163   204994    178894   63685  16398  2159    8   147   38   5%    268   46    9    7  118%
c i   75.5   28162   204994    183110   67292  16459  2163    8   191   54   4%   -206   84    9    7  119%
c i   77.1   28092   204994    194960   76816  16811  2189    7   138   55   5%    -68   21    9    7  123%
c i   77.5   28085   204994    196576   78101  16849  2192    8   165   55   5%   -186   47    9    7  129%
c i   78.1   28084   204994    200649   81434  16973  2205    8   172   55   4%   -173   53    9    7  120%
c i   78.4   28078   204994    202527   83040  17006  2210    8   151   55   5%   -192   30    8    7  116%
c i   78.9   28077   204994    206143   86003  17120  2218    7   126   55   6%   -164    5    8    7  105%
c i   79.2   28075   204994    207412   87011  17164  2227    8   131   55   6%   -182   10    7    7   99%
c i   80.0   28070   204994    210334   89369  17232  2234    8   133   56   6%   -163   11    9    7  118%
c i   80.1   28068   204994    210922   89822  17262  2236    8   128   56   6%   -173    6    9    7  117%
c i   80.1   28065   204994    211215   90037  17273  2239    8   130   56   6%   -176    8    8    7  113%
c 
c [simplification-11] limit 181476 conflicts (hard 214809) hit after 214810 conflicts
c [quatres-7] found 39771 quaternary clauses 26% in total
c [quatres-7-1] removed 10 duplicate quaternary clauses
c [quatres-7-1] added 5 double-self-subsuming ternary resolvents
c [quatres-7-2] added 2896 single-self-subsuming ternary resolvents
c [quatres-7-2] added 423 quaternary resolvents
c [ternres-7] limit 15003257 with penalty 0 = 0 + 0
c [ternres-7] 483 schedulable variables 2%
c [ternres-7] 4258 ternary resolvents (67 bin, 4191 trn)
c [ternres-7] 1 variables remain 0% (28062 retained 100%)
c [decomp-29] removed 530 variables
c [simpleprobe-4] 9712 schedulable variables 35%
c [simpleprobe-4] limit 15003257 penalty 2 = 2 + 0
c [decomp-30] removed 22 variables
c [simpleprobe-4] 4334 variables remain 16% (23302 retained 84%)
c [simpleprobe-4] removed 22 variables, found 197 hbrs, 2 units
c [unhide-10] limit 3000651 with penalty 0 = 0 + 0
c [unhide-10-11] 3 units, 3 failed, 4317 tauts, 0 hbrs, 42847 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 186 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 27620 variables 100%
c [block-4] limit of 37508144 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 5945 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 187540722 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-4-1] eliminated 2 clauses out of 142 (1%) of length 20
c [cce-4-1] eliminated 6 clauses out of 185 (3%) of length 19
c [cce-4-1] eliminated 10 clauses out of 294 (3%) of length 18
c [cce-4-1] eliminated 17 clauses out of 353 (5%) of length 17
c [cce-4-1] eliminated 13 clauses out of 354 (4%) of length 16
c [cce-4-1] eliminated 13 clauses out of 433 (3%) of length 15
c [cce-4-1] eliminated 18 clauses out of 577 (3%) of length 14
c [cce-4-1] eliminated 15 clauses out of 671 (2%) of length 13
c [cce-4-1] eliminated 48 clauses out of 1061 (5%) of length 12
c [cce-4-1] eliminated 101 clauses out of 1668 (6%) of length 11
c [cce-4-1] eliminated 153 clauses out of 2205 (7%) of length 10
c [cce-4-1] eliminated 163 clauses out of 3359 (5%) of length 9
c [cce-4-1] eliminated 387 clauses out of 5839 (7%) of length 8
c [cce-4-1] eliminated 1239 clauses out of 12874 (10%) of length 7
c [cce-4-1] eliminated 1297 clauses out of 27671 (5%) of length 6
c [cce-4-1] eliminated 1462 clauses out of 17285 (8%) of length 5
c [cce-4-1] eliminated 860 clauses out of 19128 (4%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 5805 large clauses in 109157046 steps
c [cce-4-1] allowing another 54578523 steps for small clauses
c [cce-4-1] scheduling 90429 clauses = 22404 binary + 68025 ternary
c [cce-4-1] tried to eliminate 90429 small clauses 100%
c [cce-4-1] eliminated 165 binary clauses 1%
c [cce-4-1] eliminated 755 ternary clauses 1%
c [cce-4-1] eliminated 920 small clauses 1%
c [cce-4-1] eliminated 920 small clauses in 120505033 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 6725 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 33517844 steps for small clauses
c [cce-4-2] scheduling 89511 clauses = 22239 binary + 67272 ternary
c [cce-4-2] tried to eliminate 38608 small clauses 43%
c [cce-4-2] eliminated 2 ternary clauses 0%
c [cce-4-2] eliminated 2 small clauses 0%
c [cce-4-2] eliminated 2 small clauses in 67035691 steps
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 2 covered clauses in round 2
c [cce-4] eliminated 6727 covered clauses in TOTAL during 2 rounds
c [bca-7] limit of 10000000 steps and 373638 added (scaled 2)
c [bca-7] 31154 out of 54014 literals actually usable 58%
c [bca-7] added 63 blocked clauses in 169409 steps
c [sweep-7] limit 4500977 penalty 0 = 0 + 0
c [sweep-7-1] 1440 pos 56.0% + 1130 neg 44.0% = 2570 sched 9.5% ret 24436
c [sweep-7-1] 4581177 steps 1420 queries 363.77 avg class size
c [sweep-7-1] 19245 decisions 1422 SAT calls 18.22 avg env size
c [sweep-7-1] 92 variables remain 0% (26914 retained 100%)
c [decomp-31] removed 37 variables
c [sweep-7-1] removed 37 vars (0 failed, 2 eqs, 0 impls)
c [sweep-7] removed 37 vars in TOTAL (1 rounds, 1419 queries)
c [sort-queue-11] sorted 26969 enqueued variables after 214810 conflicts
c [score-dist-11] active 0 (0%), one 18456 (68%), zero 8513 (32%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 1094 variables 3.9% (26969 remain 10%)
c [simplification-11] removed 18541 irredundant clauses 9.0% (186453 remain 24%)
c [simplification-11] maximum reduction of 9% = max (4%, 9%)
c [simplification-11] large reduction 9% >= 5% limit
c [simplification-11] next conflict interval 2148 = min (214810/100, 66666)
c [simplification-11] penalized conflict interval 2148 = 1 * 2148
c [simplification-11] hard conflict limit 226958 (soft 216958 + delta 10000)
c [simplification-11] new conflict limit 216958 (hard 226958)
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   86.4   26968   186453    218525   78977  22029  2749    7   149   43   5%    -78   25    6    7   77%
c i   87.0   26957   186452    221983   81626  22170  2769    8   142   43   5%   -128   16    6    7   76%
c i   87.2   26954   186452    222986   82382  22199  2771    8   136   43   6%   -146   11    7    7   95%
c i   87.2   26952   186452    222987   82382  22199  2771    8   136   43   6%   -146   10    7    7   94%
c i   87.4   26949   186452    224352   83414  22254  2781    8   142   43   5%   -149   16    9    7  122%
c 
c [simplification-12] limit 216968 conflicts (hard 226958) hit after 226960 conflicts
c [quatres-8] found 36562 quaternary clauses 26% in total
c [quatres-8-1] removed 139 duplicate quaternary clauses
c [quatres-8-1] added 7 double-self-subsuming ternary resolvents
c [quatres-8-2] added 411 single-self-subsuming ternary resolvents
c [quatres-8-2] added 305 quaternary resolvents
c [ternres-8] limit 15664109 with penalty 0 = 0 + 0
c [ternres-8] 1 schedulable variables 0%
c [ternres-8] 7222 ternary resolvents (718 bin, 6504 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-32] removed 142 variables
c [treelook-4] limit 1566410 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 22364 literals 42%
c [treelook-4] scheduling used 752902 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1566410 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1575061 steps
c [treelook-4] 22236 literals remain 41%
c [treelook-4] 7101 variables remain to probed next time 26%
c [decomp-33] removed 1 variables
c [treelook-4] removed 7 variables, found 2706 hbrs
c [unhide-11] limit 3132821 with penalty 0 = 0 + 0
c [unhide-11-13] 2 units, 34 failed, 3888 tauts, 0 hbrs, 17097 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 387 transitive binary clauses
c [transred-8] found 4 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 26784 variables 100%
c [elim-9] limit of 156641095 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 3420 variables 13% in round 1 in 112774161 steps
c [elim-9-1] backward subsumption/strengthening limit 43866934
c [elim-9-1-1] backward checking 6809 touched variables 25%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 6 and strengthened 4 clauses in 6149167 steps
c [elim-9-1] rescheduled 35 variables 0% by backward subsumption
c [elim-9-2] eliminated 5 variables 0% in round 2 in 673307 steps
c [elim-9-2] backward subsumption/strengthening limit 673300
c [elim-9-2-1] backward checking 36 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 406343 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 3425 = 13% variables out of 26784 scheduled
c [bca-8] limit of 10000000 steps and 343040 added (scaled 2)
c [bca-8] 27585 out of 46720 literals actually usable 59%
c [bca-8] added 49 blocked clauses in 149323 steps
c [sweep-8] limit 4699232 penalty 0 = 0 + 0
c [sweep-8-1] 55 pos 68.8% + 25 neg 31.2% = 80 sched 0.3% ret 23279
c [sweep-8-1] 45080 steps 45 queries 32.09 avg class size
c [sweep-8-1] 608 decisions 44 SAT calls 17.73 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-34] removed 14 variables
c [sweep-8-1] removed 14 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8-2] 11402 pos 48.8% + 11943 neg 51.2% = 23345 sched 100.0% ret 0
c [sweep-8-2] 4680257 steps 479 queries 1453.34 avg class size
c [sweep-8-2] 13824 decisions 484 SAT calls 48.08 avg env size
c [sweep-8-2] 13530 variables remain 58% (9815 retained 42%)
c [decomp-35] removed 25 variables
c [sweep-8-2] removed 25 vars (0 failed, 18 eqs, 10 impls)
c [sweep-8] removed 39 vars in TOTAL (2 rounds, 522 queries)
c [sort-queue-12] sorted 23320 enqueued variables after 226960 conflicts
c [score-dist-12] active 0 (0%), one 16286 (70%), zero 7034 (30%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 3622 variables 13.4% (23320 remain 9%)
c [simplification-12] removed 15278 irredundant clauses 8.2% (171173 remain 22%)
c [simplification-12] maximum reduction of 13% = max (13%, 8%)
c [simplification-12] large reduction 13% >= 5% limit
c [simplification-12] next conflict interval 2269 = min (226960/100, 66666)
c [simplification-12] penalized conflict interval 2269 = 1 * 2269
c [simplification-12] hard conflict limit 239229 (soft 229229 + delta 10000)
c [simplification-12] new conflict limit 229229 (hard 239229)
c 
c [simplification-13] limit 229229 conflicts (hard 239229) hit after 235024 conflicts
c [quatres-9] found 27853 quaternary clauses 22% in total
c [quatres-9-1] removed 24 duplicate quaternary clauses
c [quatres-9-1] added 4 double-self-subsuming ternary resolvents
c [quatres-9-2] added 86 single-self-subsuming ternary resolvents
c [quatres-9-2] added 417 quaternary resolvents
c [ternres-9] limit 16089137 with penalty 0 = 0 + 0
c [ternres-9] all 23320 free variables schedulable
c [ternres-9] 5671 ternary resolvents (655 bin, 5016 trn)
c [ternres-9] 17 variables remain 0% (23303 retained 100%)
c [decomp-36] removed 68 variables
c [basicprobe-4] limit 80445688 penalty 0 = 0 + 0
c [basicprobe-4-0] 11854 sched 51%, 19 failed, 0 lifted, 588 hbrs
c [decomp-37] removed 58 variables
c [basicprobe-4-1] 12102 sched 52%, 4 failed, 0 lifted, 96 hbrs
c [decomp-38] removed 9 variables
c [basicprobe-4-2] 12084 sched 52%, 2 failed, 0 lifted, 11 hbrs
c [decomp-39] removed 8 variables
c [basicprobe-4-3] 12082 sched 52%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-4] 12082 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-4] fully completed probing
c [basicprobe-4-4] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-4-4] removed 75 variables, found 698 hbrs
c [bate-2] eliminated 104 asymmetric tautologies during probing
c [unhide-12] limit 3217827 with penalty 0 = 0 + 0
c [unhide-12-15] 0 units, 0 failed, 2957 tauts, 0 hbrs, 11431 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 158 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 23177 variables 100%
c [block-5] limit of 80445688 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 3565 blocked clauses
c [cce-5] limit of 40222844 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 44
c [cce-5-1] eliminated 1 clauses out of 8 (12%) of length 26
c [cce-5-1] eliminated 6 clauses out of 29 (21%) of length 24
c [cce-5-1] eliminated 3 clauses out of 35 (9%) of length 23
c [cce-5-1] eliminated 2 clauses out of 52 (4%) of length 22
c [cce-5-1] eliminated 6 clauses out of 65 (9%) of length 21
c [cce-5-1] eliminated 7 clauses out of 160 (4%) of length 20
c [cce-5-1] eliminated 11 clauses out of 177 (6%) of length 19
c [cce-5-1] eliminated 14 clauses out of 289 (5%) of length 18
c [cce-5-1] eliminated 14 clauses out of 344 (4%) of length 17
c [cce-5-1] eliminated 17 clauses out of 349 (5%) of length 16
c [cce-5-1] eliminated 26 clauses out of 447 (6%) of length 15
c [cce-5-1] eliminated 25 clauses out of 582 (4%) of length 14
c [cce-5-1] eliminated 16 clauses out of 700 (2%) of length 13
c [cce-5-1] eliminated 32 clauses out of 1026 (3%) of length 12
c [cce-5-1] eliminated 37 clauses out of 1594 (2%) of length 11
c [cce-5-1] eliminated 75 clauses out of 2093 (4%) of length 10
c [cce-5-1] eliminated 226 clauses out of 3421 (7%) of length 9
c [cce-5-1] eliminated 280 clauses out of 5564 (5%) of length 8
c [cce-5-1] eliminated 6 clauses out of 11403 (0%) of length 7
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 805 large clauses in 40222845 steps
c [cce-5-1] allowing another 20111422 steps for small clauses
c [cce-5-1] scheduling 75739 clauses = 18950 binary + 56789 ternary
c [cce-5-1] tried to eliminate 28698 small clauses 38%
c [cce-5-1] eliminated 165 binary clauses 1%
c [cce-5-1] eliminated 578 ternary clauses 1%
c [cce-5-1] eliminated 743 small clauses 1%
c [cce-5-1] eliminated 743 small clauses in 40222844 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1548 covered clauses in round 1
c [cce-5] eliminated 1548 covered clauses in TOTAL during 1 rounds
c [cce-5] 1548 < 1/100 * 166769 = 1667 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 22729 variables 100%
c [elim-10] limit of 321782753 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 700 variables 3% in round 1 in 98642654 steps
c [elim-10-1] backward subsumption/strengthening limit 98642600
c [elim-10-1-1] backward checking 1984 touched variables 9%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 10 and strengthened 0 clauses in 3406351 steps
c [elim-10-1] rescheduled 15 variables 0% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 921404 steps
c [elim-10-2] backward subsumption/strengthening limit 921400
c [elim-10-2-1] backward checking 5 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 2 clauses in 273096 steps
c [elim-10-2] rescheduled 5 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 375891 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 701 = 3% variables out of 22729 scheduled
c [bca-9] limit of 10000000 steps and 325830 added (scaled 2)
c [bca-9] 25359 out of 44058 literals actually usable 58%
c [bca-9] added 132 blocked clauses in 145763 steps
c [sweep-9] limit 4826741 penalty 0 = 0 + 0
c [sweep-9-1] 5326 pos 41.9% + 7378 neg 58.1% = 12704 sched 57.7% ret 9324
c [sweep-9-1] 4828479 steps 906 queries 1055.10 avg class size
c [sweep-9-1] 23169 decisions 904 SAT calls 36.21 avg env size
c [sweep-9-1] 6702 variables remain 30% (15326 retained 70%)
c [decomp-41] removed 27 variables
c [sweep-9-1] removed 27 vars (0 failed, 24 eqs, 16 impls)
c [sweep-9] removed 27 vars in TOTAL (1 rounds, 905 queries)
c [sort-queue-13] sorted 22001 enqueued variables after 235024 conflicts
c [score-dist-13] active 0 (0%), one 15463 (70%), zero 6538 (30%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 1319 variables 5.7% (22001 remain 8%)
c [simplification-13] removed 8603 irredundant clauses 5.0% (162570 remain 21%)
c [simplification-13] maximum reduction of 6% = max (6%, 5%)
c [simplification-13] large reduction 6% >= 5% limit
c [simplification-13] next conflict interval 2350 = min (235024/100, 66666)
c [simplification-13] penalized conflict interval 2350 = 1 * 2350
c [simplification-13] hard conflict limit 247374 (soft 237374 + delta 10000)
c [simplification-13] new conflict limit 237374 (hard 247374)
c 
c [simplification-14] limit 237374 conflicts (hard 247374) hit after 237375 conflicts
c [quatres-10] found 26719 quaternary clauses 22% in total
c [quatres-10-1] removed 34 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 89 single-self-subsuming ternary resolvents
c [quatres-10-2] added 141 quaternary resolvents
c [ternres-10] limit 16189336 with penalty 0 = 0 + 0
c [ternres-10] 17 schedulable variables 0%
c [ternres-10] 2463 ternary resolvents (80 bin, 2383 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 404733 penalty 3 = 3 + 0
c [gauss-4] extracted 2995 xors of average arity 3.0
c [gauss-4] connected 8978 occurrences of 2367 variables (average 3.8)
c [gauss-4] limit 404733 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-42] removed 3 variables
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 130 transitive binary clauses
c [transred-10] found 2 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 21996 variables 100%
c [block-6] limit of 161893361 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 423 blocked clauses
c [block-6] 423 < 1/100 * 162544 = 1625 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 21952 variables 100%
c [elim-11] limit of 323786722 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 55 variables 0% in round 1 in 97391829 steps
c [elim-11-1] backward subsumption/strengthening limit 97391800
c [elim-11-1-1] backward checking 500 touched variables 2%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 1852315 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 55 = 0% variables out of 21952 scheduled
c [elim-11] 55 < 1/100 * 21952 = 219 considered unsuccessful
c [bca-10] limit of 10000000 steps and 324524 added (scaled 2)
c [bca-10] 24762 out of 43796 literals actually usable 57%
c [bca-10] added 5 blocked clauses in 145231 steps
c [sweep-10] limit 4856800 penalty 0 = 0 + 0
c [sweep-10-1] 2787 pos 42.0% + 3855 neg 58.0% = 6642 sched 30.3% ret 15255
c [sweep-10-1] 4858768 steps 1526 queries 625.58 avg class size
c [sweep-10-1] 28299 decisions 1501 SAT calls 26.09 avg env size
c [sweep-10-1] 2612 variables remain 12% (19285 retained 88%)
c [decomp-43] removed 69 variables
c [sweep-10-1] removed 69 vars (0 failed, 63 eqs, 43 impls)
c [sweep-10] removed 69 vars in TOTAL (1 rounds, 1525 queries)
c [sort-queue-14] sorted 21828 enqueued variables after 237375 conflicts
c [score-dist-14] active 0 (0%), one 15447 (71%), zero 6381 (29%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 173 variables 0.8% (21828 remain 8%)
c [simplification-14] removed 676 irredundant clauses 0.4% (161894 remain 20%)
c [simplification-14] maximum reduction of 1% = max (1%, 0%)
c [simplification-14] geometric conflict interval increment 33333 = 66666 / 2
c [simplification-14] new conflict interval 99999
c [simplification-14] penalized conflict interval 99999 = 1 * 99999
c [simplification-14] hard conflict limit 387373 (soft 337374 + delta 49999)
c [simplification-14] new conflict limit 337374 (hard 387373)
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  104.6   21827   161894    247030   75667  19242  3275    8   113   41   7%    171  -17    8    8  103%
c i  105.5   21826   161894    255238   82425  19458  3298    8   208   41   4%    -46   74    8    8  111%
c i  107.1   21824   161894    267454   92523  19805  3334    7   113   41   7%     28  -25    5    8   72%
c -  108.7   21820   161894    279006   65303  20062  3370    8   109   37   7%     26  -22    9    8  116%
c i  109.3   21819   161894    283295   68780  20167  3385    8   178   39   5%     90   47    9    8  124%
c 
c [simplification-15] limit of 528 binary hit after 540 binaries
c [quatres-11] found 28168 quaternary clauses 21% in total
c [quatres-11-1] removed 23 duplicate quaternary clauses
c [quatres-11-1] added 4 double-self-subsuming ternary resolvents
c [quatres-11-2] added 58 single-self-subsuming ternary resolvents
c [quatres-11-2] added 138 quaternary resolvents
c [ternres-11] limit 18487344 with penalty 0 = 0 + 0
c [ternres-11] all 21811 free variables schedulable
c [ternres-11] 1571 ternary resolvents (139 bin, 1432 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 577729 penalty 4 = 4 + 0
c [card-5] found 161 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 577729 for elimination
c [card-5] 161 out of 161 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-44] removed 73 variables
c [simpleprobe-5] 3382 schedulable variables 16%
c [simpleprobe-5] limit 36974688 penalty 1 = 1 + 0
c [decomp-45] removed 28 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 28 variables, found 1208 hbrs, 3 units
c [unhide-13] limit 1848734 with penalty 1 = 1 + 0
c [unhide-13-16] 0 units, 0 failed, 431 tauts, 0 hbrs, 14694 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 437 transitive binary clauses
c [bca-11] limit of 10000000 steps and 322439 added (scaled 2)
c [bca-11] 24329 out of 43456 literals actually usable 56%
c [bca-11] added 11 blocked clauses in 152557 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 55462030 penalty 0 = 0 + 0
c [sweep-11-1] 1382 pos 53.0% + 1227 neg 47.0% = 2609 sched 12.0% ret 19118
c [sweep-11-1] 2596342 steps 1534 queries 365.34 avg class size
c [sweep-11-1] 23892 decisions 1531 SAT calls 20.43 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-46] removed 22 variables
c [sweep-11-1] removed 22 vars (0 failed, 10 eqs, 5 impls)
c [sweep-11-2] 9838 pos 45.3% + 11867 neg 54.7% = 21705 sched 100.0% ret 0
c [sweep-11-2] 15409585 steps 2992 queries 227.98 avg class size
c [sweep-11-2] 63917 decisions 2986 SAT calls 30.88 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-47] removed 66 variables
c [sweep-11-2] removed 66 vars (0 failed, 78 eqs, 32 impls)
c [sweep-11-3] 9814 pos 45.4% + 11825 neg 54.6% = 21639 sched 100.0% ret 0
c [sweep-11-3] 14432117 steps 2828 queries 181.38 avg class size
c [sweep-11-3] 61225 decisions 2825 SAT calls 31.53 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-48] removed 46 variables
c [sweep-11-3] removed 46 vars (0 failed, 61 eqs, 19 impls)
c [sweep-11] removed 134 vars in TOTAL (3 rounds, 7351 queries)
c [sort-queue-15] sorted 21593 enqueued variables after 292915 conflicts
c [score-dist-15] active 0 (0%), one 15715 (73%), zero 5878 (27%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 218 variables 1.0% (21593 remain 8%)
c [simplification-15] removed 1107 irredundant clauses 0.7% (160787 remain 20%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] forced so keeping old conflict interval 99999
c [simplification-15] conflict limit remains at 337374 (hard 387373)
c [simplification-15] 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  115.4   21592   160786    298636   80661  20529  4240    8   126   41   6%     86   -7    9    8  113%
c i  115.4   21591   160786    298637   80661  20529  4240    8   126   41   6%     85   -7    9    8  112%
c i  116.6   21587   160786    305583   86340  20748  4253    8   187   41   4%    -39   52    8    8  109%
c i  117.0   21581   160786    308323   88722  20810  4264    8   123   42   6%    -94  -13    7    8   94%
c i  118.3   21574   160786    316133   95068  21041  4282    8   128   42   6%    -13   -7    5    8   67%
c i  121.2   21571   160786    334194  109913  21534  4315    8   178   45   4%    142   39    7    8   87%
c -  122.8   21571   160786    342801   80949  21771  4330    8   131   38   6%     -0  -10    8    8   96%
c 
c [simplification-16] limit 337384 conflicts (hard 387373) hit after 347524 conflicts
c [quatres-12] found 30288 quaternary clauses 21% in total
c [quatres-12-1] removed 59 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 126 single-self-subsuming ternary resolvents
c [quatres-12-2] added 158 quaternary resolvents
c [ternres-12] limit 21256307 with penalty 0 = 0 + 0
c [ternres-12] all 21571 free variables schedulable
c [ternres-12] 2623 ternary resolvents (204 bin, 2419 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-49] removed 103 variables
c [treelook-5] limit 2125630 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 18121 literals 42%
c [treelook-5] scheduling used 645508 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2125630 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2131808 steps
c [treelook-5] 17145 literals remain 40%
c [treelook-5] 5481 variables remain to probed next time 26%
c [decomp-50] removed 4 variables
c [treelook-5] removed 7 variables, found 402 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 535 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 21483 variables 100%
c [block-7] limit of 106281539 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 1316 blocked clauses
c [block-7] 1316 < 1/100 * 160123 = 1601 considered unsuccessful
c [cce-6] limit of 26570384 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 5 clauses out of 62 (8%) of length 22
c [cce-6-1] eliminated 9 clauses out of 164 (5%) of length 20
c [cce-6-1] eliminated 6 clauses out of 175 (3%) of length 19
c [cce-6-1] eliminated 18 clauses out of 286 (6%) of length 18
c [cce-6-1] eliminated 17 clauses out of 328 (5%) of length 17
c [cce-6-1] eliminated 21 clauses out of 328 (6%) of length 16
c [cce-6-1] eliminated 16 clauses out of 409 (4%) of length 15
c [cce-6-1] eliminated 22 clauses out of 551 (4%) of length 14
c [cce-6-1] eliminated 17 clauses out of 674 (3%) of length 13
c [cce-6-1] eliminated 37 clauses out of 919 (4%) of length 12
c [cce-6-1] eliminated 44 clauses out of 1531 (3%) of length 11
c [cce-6-1] eliminated 56 clauses out of 1994 (3%) of length 10
c [cce-6-1] eliminated 78 clauses out of 3270 (2%) of length 9
c [cce-6-1] eliminated 105 clauses out of 5352 (2%) of length 8
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 451 large clauses in 26570421 steps
c [cce-6-1] allowing another 13285210 steps for small clauses
c [cce-6-1] scheduling 71230 clauses = 17808 binary + 53422 ternary
c [cce-6-1] tried to eliminate 23265 small clauses 33%
c [cce-6-1] eliminated 31 binary clauses 0%
c [cce-6-1] eliminated 186 ternary clauses 0%
c [cce-6-1] eliminated 217 small clauses 0%
c [cce-6-1] eliminated 217 small clauses in 26570391 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 668 covered clauses in round 1
c [cce-6] eliminated 668 covered clauses in TOTAL during 1 rounds
c [cce-6] 668 < 1/100 * 158807 = 1588 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 21347 variables 100%
c [elim-12] limit of 212563078 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 286 variables 1% in round 1 in 93498020 steps
c [elim-12-1] backward subsumption/strengthening limit 93498000
c [elim-12-1-1] backward checking 1222 touched variables 6%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 7 and strengthened 18 clauses in 3070235 steps
c [elim-12-1] rescheduled 47 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 822402 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 286 = 1% variables out of 21347 scheduled
c [bca-12] limit of 10000000 steps and 311756 added (scaled 2)
c [bca-12] 22674 out of 42124 literals actually usable 54%
c [bca-12] added 104 blocked clauses in 152120 steps
c [sweep-12] limit 6376892 penalty 0 = 0 + 0
c [sweep-12-1] 9530 pos 45.2% + 11531 neg 54.8% = 21061 sched 100.0% ret 0
c [sweep-12-1] 6379862 steps 595 queries 1053.84 avg class size
c [sweep-12-1] 18005 decisions 591 SAT calls 46.05 avg env size
c [sweep-12-1] 8703 variables remain 41% (12358 retained 59%)
c [decomp-51] removed 22 variables
c [sweep-12-1] removed 22 vars (0 failed, 14 eqs, 7 impls)
c [sweep-12] removed 22 vars in TOTAL (1 rounds, 594 queries)
c [sort-queue-16] sorted 21039 enqueued variables after 347524 conflicts
c [score-dist-16] active 0 (0%), one 15466 (74%), zero 5573 (26%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 532 variables 2.5% (21039 remain 8%)
c [simplification-16] removed 5285 irredundant clauses 3.3% (155501 remain 20%)
c [simplification-16] maximum reduction of 3% = max (2%, 3%)
c [simplification-16] geometric conflict interval increment 24999 = 99999 / 4
c [simplification-16] new conflict interval 124998
c [simplification-16] penalized conflict interval 124998 = 1 * 124998
c [simplification-16] hard conflict limit 535021 (soft 472522 + delta 62499)
c [simplification-16] new conflict limit 472522 (hard 535021)
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  128.4   21038   155501    351644   82210  22896  4506    9   140   41   6%    129    0    9    8  117%
c -  137.1   21038   155501    404878   90607  24272  4615    8   114   38   7%    504  -28    8    8   99%
c 
c [simplification-17] limit of 5602 ternary hit after 5602 ternaries
c [quatres-13] found 32854 quaternary clauses 20% in total
c [quatres-13-1] removed 20 duplicate quaternary clauses
c [quatres-13-1] added 4 double-self-subsuming ternary resolvents
c [quatres-13-2] added 136 single-self-subsuming ternary resolvents
c [quatres-13-2] added 171 quaternary resolvents
c [ternres-13] limit 27182597 with penalty 0 = 0 + 0
c [ternres-13] all 21038 free variables schedulable
c [ternres-13] 2820 ternary resolvents (280 bin, 2540 trn)
c [ternres-13] 1 variables remain 0% (21037 retained 100%)
c [decomp-52] removed 71 variables
c [basicprobe-5] limit 135912988 penalty 0 = 0 + 0
c [basicprobe-5-0] 10963 sched 52%, 4 failed, 0 lifted, 557 hbrs
c [decomp-53] removed 24 variables
c [basicprobe-5-1] 10912 sched 52%, 0 failed, 0 lifted, 39 hbrs
c [basicprobe-5-2] 10910 sched 52%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-5-3] 10908 sched 52%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-5-4] 10907 sched 52%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-5-5] 10906 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-5] fully completed probing
c [basicprobe-5-5] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-5-5] removed 24 variables, found 627 hbrs
c [bate-3] eliminated 39 asymmetric tautologies during probing
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 479 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 20944 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 190 variables 1% in round 1 in 93101471 steps
c [elim-13-1] backward subsumption/strengthening limit 93101400
c [elim-13-1-1] backward checking 654 touched variables 3%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 2 and strengthened 2 clauses in 1502102 steps
c [elim-13-1] rescheduled 21 variables 0% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 663252 steps
c [elim-13-2] backward subsumption/strengthening limit 663200
c [elim-13-2-1] backward checking 3 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 87083 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 191 = 1% variables out of 20944 scheduled
c [elim-13] 191 < 1/100 * 20944 = 209 considered unsuccessful
c [bca-13] limit of 10000000 steps and 308334 added (scaled 2)
c [bca-13] 20401 out of 41508 literals actually usable 49%
c [bca-13] added 31 blocked clauses in 200729 steps
c [sweep-13] limit 8154779 penalty 0 = 0 + 0
c [sweep-13-1] 3899 pos 45.4% + 4680 neg 54.6% = 8579 sched 41.3% ret 12174
c [sweep-13-1] 8163048 steps 701 queries 598.67 avg class size
c [sweep-13-1] 19976 decisions 700 SAT calls 45.24 avg env size
c [sweep-13-1] 4537 variables remain 22% (16216 retained 78%)
c [decomp-58] removed 27 variables
c [sweep-13-1] removed 27 vars (0 failed, 28 eqs, 7 impls)
c [sweep-13] removed 27 vars in TOTAL (1 rounds, 700 queries)
c [sort-queue-17] sorted 20726 enqueued variables after 460766 conflicts
c [score-dist-17] active 0 (0%), one 15357 (74%), zero 5369 (26%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 312 variables 1.5% (20726 remain 8%)
c [simplification-17] removed 1735 irredundant clauses 1.1% (153766 remain 19%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] forced so keeping old conflict interval 124998
c [simplification-17] conflict limit remains at 472522 (hard 535021)
c [simplification-17] new ternary interval 10000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  153.0   20726   153766    465281  101567  26785  4903    9   127   41   7%    817  -13   10    8  116%
c 
c [simplification-18] limit 472522 conflicts (hard 535021) hit after 472522 conflicts
c [quatres-14] found 32811 quaternary clauses 20% in total
c [quatres-14-1] removed 17 duplicate quaternary clauses
c [quatres-14-1] added 1 double-self-subsuming ternary resolvents
c [quatres-14-2] added 117 single-self-subsuming ternary resolvents
c [quatres-14-2] added 183 quaternary resolvents
c [ternres-14] limit 27879398 with penalty 0 = 0 + 0
c [ternres-14] 1 schedulable variables 0%
c [ternres-14] 480 ternary resolvents (10 bin, 470 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-59] removed 4 variables
c [simpleprobe-6] all 20722 free variables schedulable
c [simpleprobe-6] limit 111517594 penalty 0 = 0 + 0
c [decomp-60] removed 26 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 26 variables, found 1385 hbrs, 1 units
c [unhide-14] limit 1393969 with penalty 2 = 2 + 0
c [unhide-14-17] 0 units, 0 failed, 5395 tauts, 0 hbrs, 27838 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 483 transitive binary clauses
c [bca-14] limit of 10000000 steps and 307872 added (scaled 2)
c [bca-14] 20924 out of 41394 literals actually usable 51%
c [bca-14] added 14 blocked clauses in 173746 steps
c [sweep-14] limit 8363819 penalty 0 = 0 + 0
c [sweep-14-1] 2449 pos 54.1% + 2075 neg 45.9% = 4524 sched 21.9% ret 16172
c [sweep-14-1] 7944830 steps 1974 queries 265.95 avg class size
c [sweep-14-1] 38190 decisions 1976 SAT calls 25.59 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-61] removed 36 variables
c [sweep-14-1] removed 36 vars (0 failed, 29 eqs, 7 impls)
c [sweep-14-2] 10056 pos 48.7% + 10604 neg 51.3% = 20660 sched 100.0% ret 0
c [sweep-14-2] 425782 steps 26 queries 5027.50 avg class size
c [sweep-14-2] 1065 decisions 25 SAT calls 81.36 avg env size
c [sweep-14-2] 20390 variables remain 99% (270 retained 1%)
c [sweep-14-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14] removed 36 vars in TOTAL (2 rounds, 1998 queries)
c [sort-queue-18] sorted 20660 enqueued variables after 472522 conflicts
c [score-dist-18] active 0 (0%), one 15337 (74%), zero 5323 (26%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 66 variables 0.3% (20660 remain 8%)
c [simplification-18] removed 292 irredundant clauses 0.2% (153474 remain 19%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 124998
c [simplification-18] new conflict interval 249996
c [simplification-18] penalized conflict interval 249996 = 1 * 249996
c [simplification-18] hard conflict limit 847516 (soft 722518 + delta 124998)
c [simplification-18] new conflict limit 722518 (hard 847516)
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 -  164.5   20660   153474    523732  112353  26467  4680    9   112   40   8%    939  -19   11    9  125%
c -  174.6   20660   153474    578882  123425  27340  4735    9    73   55  12%    987  -39   10    9  116%
c i  181.7   20659   153474    611166  152117  27956  4759    9    38   64  23%   1002  -51   11    9  123%
c -  186.6   20659   153474    631418  132231  28223  4785    9    38   55  23%  -2017  -40    7    9   76%
c i  187.9   20658   153474    637624  137809  28295  4786    8    27   60  30%  -1742  -47    6    9   69%
c i  187.9   20656   153474    637625  137809  28295  4786    8    27   60  30%  -1742  -47    6    9   69%
c i  188.3   20511   153474    639177  139172  28314  4790    8    33   60  25%  -1995  -40   10    9  113%
c i  191.1   20496   153474    651941  150553  28514  4829    8    27   62  31%  -1557  -39    5    9   59%
c i  191.1   20489   153474    651998  150570  28520  4833    8    26   62  31%  -1566  -40    5    9   55%
c i  191.7   20482   153474    654458  152723  28540  4841    8    21   62  37%  -1638  -44    6    9   71%
c i  191.7   20370   153474    654461  152723  28540  4843    8    20   62  37%  -1638  -44    6    9   71%
c i  191.7   20354   153474    654465  152724  28541  4844    8    20   62  37%  -1638  -44    6    9   70%
c i  191.7   19902   153474    654474  152731  28542  4844    8    20   62  37%  -1638  -44    6    9   69%
c i  191.7   19898   153474    654480  152732  28543  4845    8    20   62  37%  -1638  -44    6    9   68%
c i  191.7   19888   153474    654481  152732  28543  4845    8    20   62  37%  -1639  -44    6    9   68%
c 0  191.7   19690   153474    654481  152732  28543  4845    8    20   62  37%  -1639  -44    6    9   68%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 400 basic ate = 51 trn 13% + 349 lrg 87% in 3 updates
c bcas: 14 count, 602 added (1579 skipped), 2210293 steps
c bkwd: tried 113597 clauses, 227160 lits, 2.00 lits/clause
c bkwd: checked 9411109 occs, 82.85 occs/clause, 41.43 occs/lit
c bkwd: subsumed 0 binary, 3 ternary, 22 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 26 large (0% self)
c blkd: 7 bces, 20920 removed, 9370329 resolutions, 24438941 steps
c blkd: 6845 blocking literals 1%, 2119 pure
c bump: 618568 bumped seen, 22784144 lits 36.8 on average
c card: 5 count, 0 units, 1 am1, 11138754 steps
c card: 1 rescheduled, 2 eliminated, 8 resolved, 2111 subsumed
c card: 430 at-most-one constraints found, average size 3.07
c card: 430 at-most-one constraints used 100%, average size 3.07
c card: 15 at-most-two constraints found, average size 4.40
c card: 15 at-most-two constraints used 100%, average size 4.40
c cces: 6 cces, 12417 eliminated, 11752 ate 95%, 665 abce 5%
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: 2640582 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 116 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 62 decompositions, 6382 equivalent 2%
c deco: 1 decision-only clauses 0%, 42% reduction
c decs: 8438811 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 13 elims, 230475 eliminated 87%, 641 pure 0%
c elms: 21 rounds, 1.6 rounds/bve
c elms: 217381 small 94%, 10334 large 4%
c elms: 306583 tried small, 217381 succeeded 71%, 89202 failed 29%
c elms: 9802 subsumed, 7200 strengthened, 1780 blocked
c elms: 9590819 copies, 16611504 resolutions, 6240419 ipos
c elms: 7139997 subchks, 6395490 strchks
c gaus: 4 extractions, 34588 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7810374 steps, 3905187 extr 50%, 3952886 elim 51%
c glue: 8.1 orig avg, 8.1 real avg, 1.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 15566 = 3833 simple 25% + 10511 trn 68% + 1222 lrg 8%, 1242 sub 8%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 618568 clauses, 18.8 length
c lrnd: 11638864 lits = 15103486 orig - 3464622 removed 23%
c lrnd: 194075 uips 31%, 273840 flips 44%
c mins: 587916 mins 95%, 597 bin 0%, 30054 size 5%
c mins: 15264167 poisoned searches, 2324476 hits, 15% hit rate
c mins: 27274636 used twice searches, 2343905 hits, 9% hit rate
c move: moved 14981, 3155 bin 21%, 11826 trn 79%
c otfs: 41850 driving 52%, 39349 restarting 48%
c otfs: str 81199, 80944 red 100%, 255 irr 0%
c otfs: str 81199, 0 bin 0%, 588 trn 1%, 80611 lrg 99%
c otfs: sub 746, 736 red 99%, 10 irr 1%
c otfs: sub 746, 0 bin 0%, 73 trn 10%, 673 lrg 90%
c phas: 4 computed, 64561 set, 23066 pos (36%), 41495 neg (64%)
c prbs: 5 basic, 449993 probed, 1118 failed, 795 lifted
c prbs: 6 simple, 508855 probed, 92 failed, 251 eqs
c prbs: 5 treelook, 1356 probed, 28 failed, 0 lifted
c prom: 82361 locked 17% out of 480600 tried
c prps: 261128836 props, 30 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 14 count, 16720 quat, 4842 self1, 39 self2, 642 dup
c queu: 18 sorted, 8438811 next (167 steps 0.00)
c queu: 23566180 enq (23566143 steps 1.00), 22784144 deq 97%
c redc: 24387 clauses 9%, 281285 tried 43%, 9 sat 0%
c redc: 31370 lits 1%, 2587066 tried 17%, 9 sat 0%
c redc: 715 times jump level reduced, 9.5 levels on average
c reds: 9 count, 72720.1 conflicts per reduce
c reds: 0 memlim 0%, 9 arith 100%
c reds: 239881 collected 70%, 101732 retired 30%
c rmbd: 1278 removed, 669 red 52%
c rsts: 21423 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 18 count, 15 confs 83%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 1 trns 6%
c subl: 618568 count (251376 tried 0.4), 52880 sub out of 609291 (8.7%)
c swps: 14 count, 18 rounds, 19079 queries (1059.9/round)
c swps: 19035 sat calls, 344 unsat (0.3% success rate)
c swps: 393309 decisions 20.7, 5937 conflicts 0.3
c swps; 589.4 avg class size, 29.7 avg environment size
c swps: 0 failed, 189 impls, 386 equivs
c swp0: 6353 type 0 queries, 552 unsat (8.7%), 6297 sat (99.1%)
c swp1: 12726 type 1 queries, 3192 unsat (25.1%), 12396 sat (97.4%)
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: 18115180 calls to obtain time
c tops: 9858 fixed 4%, 70 its, 9349.73 confs/it
c trds: 14 transitive reductions, 3517 removed, 24 failed
c trds: 712906 nodes, 338168 edges, 4224572 steps
c trim: 600979 words, 2.3 MB
c trnr: 14 count, 2621 bin, 40576 trn, 179417867 steps
c unhd: 14 count, 17 rounds, 36760900 steps
c unhd: 1071 non-trivial sccs of average size 2.5
c unhd: 60 units, 60 bin, 0 trn, 0 lrg
c unhd: 290 failed, 285 stamp, 0 lits, 2 bin, 2 trn, 0 lrg
c unhd: 23138 tauts, 95 bin 0%, 11006 trn 48%, 8664 lrg 37%
c unhd: 23138 tauts, 3373 stamp 15%, 18721 red 81%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 147849 str, 60 bin 0%, 1845 trn 1%, 145944 lrg 99%, 126754 red 86%
c vars: 19690 remaining 7% and 246715 removed 93% out of 266405
c vars: 9858 fixed 4%, 230475 eliminated 87%, 6382 equivalent 2%
c vsts: 3985745853 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 15.3 search visits per propagation, 5923.2 per conflict
c wchs: 1121667304 pushed, 32052392 enlarged, 196 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         626011        239881        101732      24831303       2716965        284002
c 
c  0 0        192061  31      5559   2         0   0  19063518  77<  1573334  58    150663  53     3.9
c  1 5         70495  11     34762  14     13654  13   2389861  10    333173  12<    40467  14<    0.6
c  2 6        149185  24<    83516  35     31396  31   2264766   9    463120  17     53597  19     1.5
c  3 9        130026  21     71431  30<    30515  30<   851404   3    251217   9     28928  10     2.0
c  4 14        58243   9     31606  13     16631  16    205378   1     73008   3      8012   3     1.3
c  5 21        18603   3      9563   4      6451   6     43888   0     17695   1      1827   1     0.4
c  6 30         5392   1      2548   1      2205   2      9636   0      4026   0       357   0     0.2
c  7 41         1427   0       657   0       599   1      2092   0      1047   0       107   0     0.1
c  8 54          427   0       179   0       201   0       564   0       264   0        38   0     0.0
c  9 69           94   0        44   0        46   0       123   0        55   0         3   0     0.0
c 10 86           51   0        14   0        30   0        64   0        22   0         3   0     0.0
c 11 126           7   0         2   0         4   0         9   0         4   0         0   0     0.0
c 
c avg                  1.8           2.6           2.8           0.4           0.9           1.0
c std                  1.5           1.2           1.3           0.9           1.2           1.2
c 
c   20.134  11% elim
c    9.255   5% sweep
c    8.845   5% probe
c    5.958   3% decide
c    5.899   3% cce
c    3.773   2% unhide
c    2.469   1% quatres
c    2.273   1% block
c    1.922   1% bump
c    1.643   1% bca
c 
c    3.256 < 1% rest (below)
c 
c    1.622   1% ternres
c    0.886   0% gauss
c    0.385   0% transred
c    0.363   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.215   3% preprocessing     8%
c   57.085  30% inprocessing     92%
c ==================================
c   62.299  32% simplifying
c  129.405  68% search
c ==================================
c  191.709 100% all
c 
c        654481 conflicts,        3413.9 confs/sec
c          7045 ternaries,          92.9 confs/ternary
c           914 binaries,          716.1 confs/binary
c            70 iterations,       9349.7 confs/iteration
c 
c             9 reductions,          0.0 redus/sec,  72720.1 confs/reduction
c         21423 restarts,          111.7 rests/sec,     30.6 confs/restart
c       8438811 decisions,       44018.8 decis/sec,     12.9 decis/conflict
c     261128836 propagations,  1362109.7 props/sec,     30.9 props/decision
c 
c 191.7 seconds, 75.5 MB
c launch: done
