c launch: /data/cnf/sc2014/app/UR-15-10p1.cnf.bz2
c host: atom20
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/UR-15-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-15-10p1.cnf.bz2
c no embedded options
c found 'p cnf 199996 1019200' header
c read 199996 variables, 1019200 clauses, 2430990 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 189747 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  189747  1008281         0       0      0     0    0     0   53   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 6083 at-most-one constraints of average size 5.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6083 out of 6083 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54081 variables
c [simpleprobe-1] all 145915 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 53 variables
c [simpleprobe-1] 237 variables remain 0% (145625 retained 100%)
c [simpleprobe-1] removed 53 variables, found 13804 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 4 units, 592 failed, 7212 tauts, 0 hbrs, 8802 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 145473 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 32892 not tried 23% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 55795 = 38% variables out of 145473 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 615269 negative 99.2% of 620148 except 4879 0.8%
c [phase-count-1] 489917 positive 79.0% of 620148 except 130231 21.0%
c [phase-count-1] less non-negative clauses 4879 than limit 62000 (10.0%)
c [phase-count-1] non-pos/non-neg = 130231/4879 = 26.69 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 89678 negative 100%
c [sort-queue-1] sorted 89678 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 89678 (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 62173 variables 40.9% (89678 remain 47%)
c [simplification-1] removed 388133 irredundant clauses 38.5% (620148 remain 62%)
c [simplification-1] maximum reduction of 41% = max (41%, 38%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.9   89677   620148         8       7      0  9660    0     5   42   0%      0    5    0    0 25223%
c i    4.0   89622   620148       120      95     12  9667    0     7   43   3%      0    7    2    0 20134%
c i    4.0   89510   620148       124      98     12  9667    0     7   43   3%      0    7    2    0 19911%
c i    4.1   89499   620148       140     111     14  9667    0     8   43   3%      0    8    3    0 19279%
c i    4.2   89243   620148       169     138     15  9667    0     9   43   3%      0    9    3    0 18948%
c i    4.2   89231   620148       185     148     17  9670    0     9   43   3%      0    9    3    0 18030%
c i    4.3   88937   620148       280     228     20  9675    1    13   43   6%      0   13    8    0 17494%
c i    4.3   88805   620148       289     231     20  9680    1    13   43   6%      0   13    8    0 16931%
c i    4.3   88796   620148       306     239     23  9684    1    13   43   6%      0   13    8    0 16130%
c i    4.3   88235   620148       316     244     26  9685    1    13   43   6%      0   13    8    0 15595%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1847 variables
c [simpleprobe-2] 234 schedulable variables 0%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] fully completed simple probing
c [simpleprobe-2] removed 0 variables, found 412 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 58363 literals 33%
c [treelook-1] scheduling used 300336 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 624621 steps
c [treelook-1] 58355 literals remain 33%
c [treelook-1] 56102 variables remain to probed next time 64%
c [treelook-1] removed 2 variables, found 5114 hbrs
c [basicprobe-1] limit 4874048 based on 609256 irredundant clauses
c [basicprobe-1-0] 33062 probes remain 39% after last round
c [basicprobe-1-0] 18 units = 18 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2470 variables, found 24588 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 5 units, 1341 failed, 7125 tauts, 0 hbrs, 1610 literals
c [elim-2] 31792 variables 38% will be scheduled this time
c [elim-2] scheduled 31792 variables 38%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 10137 not tried 12% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 3 = 0% variables out of 31792 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 568713 negative 99.1% of 573592 except 4879 0.9%
c [phase-count-2] 451608 positive 78.7% of 573592 except 121984 21.3%
c [phase-count-2] less non-negative clauses 4879 than limit 57300 (10.0%)
c [phase-count-2] non-pos/non-neg = 121984/4879 = 25.00 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 5757 negative 100%
c [sort-queue-2] sorted 84457 enqueued variables after 316 conflicts
c [score-dist-2] active 0 (0%), one 12289 (15%), zero 72168 (85%)
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 3418 variables 3.9% (84457 remain 45%)
c [simplification-2] removed 46556 irredundant clauses 7.5% (573592 remain 57%)
c [simplification-2] maximum reduction of 8% = max (4%, 8%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1005 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    6.8   84456   573592       367     278     31 30370    1    15   40   6%      0   15    8    0 13997%
c i    6.9   84452   573592       408     316     33 30370    1    16   40   6%      0   16    8    0 13128%
c i    6.9   84414   573592       460     348     43 30379    1    18   40   6%      0   18    8    0 11526%
c i    7.0   83833   573592       498     379     47 30381    1    19   40   6%      0   19    9    0 11332%
c i    7.0   83507   573592       503     380     47 30384    1    19   40   6%      0   19    8    0 11130%
c i    7.0   83457   573592       523     396     49 30385    1    20   40   6%      0   20    8    0 10502%
c i    7.1   83452   573592       587     433     60 30399    1    22   40   5%      0   22    7    0 8773%
c i    7.2   83440   573592       606     441     64 30405    1    22   40   5%      0   22    7    0 8308%
c i    7.2   83170   573592       618     446     67 30407    1    22   40   5%      0   22    7    0 8205%
c i    7.3   83142   573592       634     458     68 30409    1    23   40   5%      0   23    7    0 7994%
c i    7.3   83107   573592       675     488     73 30413    1    24   40   5%      0   24    6    0 7278%
c i    7.5   83091   573592       764     563     76 30423    1    26   41   5%      0   26    6    0 6330%
c i    7.5   83081   573592       787     584     77 30423    1    27   41   5%      0   27    6    0 6280%
c i    7.7   83070   573592       879     649     92 30434    2    31   41   5%      0   31    7    0 6399%
c i    7.7   82861   573592       880     649     92 30434    2    31   41   5%      0   31    7    0 6375%
c i    7.8   82846   573592       953     697    103 30445    2    34   41   5%      0   34    6    0 5758%
c 
c [simplification-3] limit 1017 conflicts (hard 11000) hit after 1017 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3695 at-most-one constraints of average size 4.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3695 out of 3695 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1850 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 55037 literals 33%
c [treelook-2] scheduling used 301180 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 418113 steps
c [treelook-2] 55032 literals remain 33%
c [treelook-2] 44556 variables remain to probed next time 54%
c [treelook-2] removed 1 variables, found 3100 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 576 failed, 12153 tauts, 0 hbrs, 489 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 82031 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 17139 not tried 21% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2294 = 3% variables out of 82031 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 540803 negative 99.1% of 545638 except 4835 0.9%
c [phase-count-3] 430767 positive 78.9% of 545638 except 114871 21.1%
c [phase-count-3] less non-negative clauses 4835 than limit 54500 (10.0%)
c [phase-count-3] non-pos/non-neg = 114871/4835 = 23.76 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 826 negative 100%
c [sort-queue-3] sorted 79737 enqueued variables after 1017 conflicts
c [score-dist-3] active 0 (0%), one 27522 (35%), zero 52215 (65%)
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 2994 variables 3.6% (79737 remain 42%)
c [simplification-3] removed 27954 irredundant clauses 4.9% (545638 remain 54%)
c [simplification-3] maximum reduction of 5% = max (4%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13017 (soft 3017 + delta 10000)
c [simplification-3] new conflict limit 3017 (hard 13017)
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.0   79736   545638      1045     751     98 29721    2    38   39   5%      0   38    8    0 6442%
c i   10.1   79696   545638      1055     760     98 29721    2    38   39   5%      0   38    9    0 6602%
c i   10.1   79113   545638      1106     787    111 29729    2    39   39   5%      0   39    8    0 5836%
c i   10.2   79082   545638      1199     844    124 29741    2    42   39   5%      0   42    7    0 5097%
c i   10.3   79070   545638      1230     866    127 29746    2    43   39   5%      0   42    7    0 4840%
c i   10.3   78820   545638      1233     868    127 29746    2    43   39   5%      0   42    7    0 4806%
c i   10.4   78812   545638      1335     947    136 29756    2    45   39   5%      0   45    6    0 4215%
c i   10.6   78546   545638      1450    1025    154 29773    2    50   39   4%      0   49    6    0 3869%
c i   10.7   78532   545638      1489    1054    157 29779    2    51   39   4%      0   51    6    0 3658%
c i   10.7   78523   545638      1531    1090    160 29781    3    52   39   5%      0   51   10    0 5357%
c i   10.8   78490   545638      1553    1108    160 29784    3    53   39   5%      0   52   12    0 6133%
c i   10.8   78474   545638      1579    1130    160 29787    3    53   39   5%      0   53   12    0 5848%
c i   10.8   78183   545638      1581    1131    160 29787    3    53   39   5%      0   53   12    0 5805%
c i   10.9   78169   545638      1643    1184    164 29790    3    55   39   5%      0   55   12    0 5669%
c i   10.9   78070   545638      1679    1208    167 29796    3    55   39   5%      0   55   12    0 5396%
c i   11.0   78060   545638      1699    1224    170 29796    3    56   39   5%      0   55   11    0 5151%
c i   11.0   78047   545638      1738    1255    176 29797    3    57   39   5%      0   56   12    0 5187%
c i   11.0   78041   545638      1742    1257    177 29797    3    57   39   5%      0   56   12    0 5117%
c i   11.1   78033   545638      1834    1337    180 29803    3    58   39   6%      0   57   14    0 5339%
c i   11.1   78027   545638      1845    1346    180 29804    3    58   39   6%      0   57   13    0 5184%
c 
c [simplification-4] limit of 208 binary hit after 208 binaries
c [decomp-8] removed 1773 variables
c [basicprobe-2] limit 4265368 based on 533171 irredundant clauses
c [basicprobe-2-0] 28920 probes remain 38% after last round
c [basicprobe-2-0] 21 units = 21 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 893 variables, found 13103 hbrs
c [unhide-4] limit 160488 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 1006 failed, 5972 tauts, 0 hbrs, 1251 literals
c [elim-4] 9885 variables 13% will be scheduled this time
c [elim-4] scheduled 9885 variables 13%
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 19562173 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 9885 scheduled
c [phase-count-4] 513258 negative 99.1% of 518093 except 4835 0.9%
c [phase-count-4] 407429 positive 78.6% of 518093 except 110664 21.4%
c [phase-count-4] less non-negative clauses 4835 than limit 51800 (10.0%)
c [phase-count-4] non-pos/non-neg = 110664/4835 = 22.89 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 412 negative 100%
c [sort-queue-4] sorted 76325 enqueued variables after 2020 conflicts
c [score-dist-4] active 0 (0%), one 33539 (44%), zero 42786 (56%)
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 1702 variables 2.2% (76325 remain 40%)
c [simplification-4] removed 27545 irredundant clauses 5.0% (518093 remain 51%)
c [simplification-4] maximum reduction of 5% = max (2%, 5%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3028 (hard 13017)
c [simplification-4] 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   12.8   76324   518093      2080    1521    180 34063    4    63   37   6%      1   61   14    0 4573%
c i   13.0   76316   518093      2269    1669    202 34079    4    68   37   6%      1   66   11    0 3389%
c i   13.1   76287   518093      2308    1701    208 34079    4    68   37   6%      1   67   11    0 3205%
c i   13.2   76276   518093      2368    1740    217 34089    4    69   37   6%      1   68   10    0 2828%
c i   13.5   76264   518093      2594    1930    228 34104    5    72   38   7%      1   70   13    0 3275%
c i   13.6   76170   518093      2689    2014    233 34109    5    75   38   7%      1   73   13    0 3063%
c i   13.6   76164   518093      2693    2016    234 34109    5    75   38   7%      1   73   13    0 3033%
c i   13.7   76149   518093      2728    2045    237 34111    5    76   38   7%      1   74   13    0 2985%
c i   13.7   76138   518093      2766    2072    242 34116    5    76   38   7%      1   74   12    0 2743%
c i   13.8   76127   518093      2814    2111    247 34119    5    77   38   7%      1   75   11    0 2617%
c i   14.1   76118   518093      2974    2215    269 34149    5    82   38   7%      1   80   10    0 2130%
c i   14.1   76109   518093      2991    2228    270 34149    5    82   38   7%      1   80   10    0 2182%
c 
c [simplification-5] limit 3030 conflicts (hard 13017) hit after 3030 conflicts
c [quatres-1] found 29252 quaternary clauses 36% in total
c [quatres-1-2] added 4 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 76102 free variables schedulable
c [ternres-1] 13 ternary resolvents (0 bin, 13 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 58 xors of average arity 2.5
c [gauss-1] connected 147 occurrences of 128 variables (average 1.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 42 variables
c [unhide-5] limit 243681 with penalty 0 = 0 + 0
c [unhide-5-5] 2 units, 325 failed, 9405 tauts, 0 hbrs, 1960 literals
c [transred-1] limit 1218409 with penalty 0 = 0 + 0
c [transred-1] removed 124 transitive binary clauses
c [transred-1] found 8 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 75661 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 9338 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 14 clauses out of 354 (4%) of length 10
c [cce-1-1] eliminated 134 clauses out of 1994 (7%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 148 large clauses in 30000006 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 265721 clauses = 250541 binary + 15180 ternary
c [cce-1-1] tried to eliminate 417 small clauses 0%
c [cce-1-1] eliminated 123 binary clauses 0%
c [cce-1-1] eliminated 7 ternary clauses 0%
c [cce-1-1] eliminated 130 small clauses 0%
c [cce-1-1] eliminated 130 small clauses in 30000032 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 278 covered clauses in round 1
c [cce-1] eliminated 278 covered clauses in TOTAL during 1 rounds
c [cce-1] 278 < 1/100 * 495782 = 4957 considered unsuccessful
c [bca-1] limit of 10000000 steps and 991508 added (scaled 2)
c [bca-1] 134385 out of 151324 literals actually usable 89%
c [bca-1] added 160 blocked clauses in 407794 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4261 pos 5.6% + 71400 neg 94.4% = 75661 sched 100.0% ret 0
c [sweep-1-1] 1329835 steps 10 queries 24439.10 avg class size
c [sweep-1-1] 75 decisions 9 SAT calls 64.00 avg env size
c [sweep-1-1] 75642 variables remain 100% (17 retained 0%)
c [decomp-10] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 9 queries)
c [phase-count-5] 490651 negative 99.0% of 495466 except 4815 1.0%
c [phase-count-5] 397794 positive 80.3% of 495466 except 97672 19.7%
c [phase-count-5] less non-negative clauses 4815 than limit 49500 (10.0%)
c [phase-count-5] non-pos/non-neg = 97672/4815 = 20.28 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 257 negative 100%
c [sort-queue-5] sorted 75658 enqueued variables after 3030 conflicts
c [score-dist-5] active 0 (0%), one 37411 (49%), zero 38247 (51%)
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 444 variables 0.6% (75658 remain 40%)
c [simplification-5] removed 22627 irredundant clauses 4.4% (495466 remain 49%)
c [simplification-5] maximum reduction of 4% = max (1%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 4000
c [simplification-5] penalized conflict interval 4000 = 1 * 4000
c [simplification-5] hard conflict limit 17030 (soft 7030 + delta 10000)
c [simplification-5] new conflict limit 7030 (hard 17030)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   17.3   75657   495466      3114    2320    309 45071    6    83   37   7%      1   81   11    0 2264%
c i   17.4   75646   495466      3217    2407    318 45077    6    84   38   7%      1   82   11    0 2183%
c i   17.7   75640   495466      3447    2583    341 45104    6    90   38   7%      1   87   13    1 2488%
c i   17.7   75634   495466      3448    2583    341 45104    6    90   38   7%      1   87   13    1 2478%
c i   17.8   75627   495466      3469    2599    345 45104    6    91   38   7%      1   88   13    1 2384%
c i   17.8   75620   495466      3477    2601    347 45107    6    91   38   7%      1   88   13    1 2324%
c i   17.8   75615   495466      3484    2606    347 45108    6    91   38   7%      1   88   12    1 2271%
c i   17.9   75604   495466      3599    2692    360 45122    6    93   38   7%      1   90   11    1 1933%
c i   17.9   75595   495466      3603    2692    362 45123    6    93   38   7%      1   90   10    1 1906%
c i   17.9   75438   495466      3614    2701    362 45124    6    93   38   7%      1   90   10    1 1849%
c i   18.0   75427   495466      3675    2753    365 45127    7    96   38   7%      1   93   18    1 3054%
c i   18.2   75413   495466      3833    2879    377 45143    7    98   38   7%      1   95   15    1 2405%
c i   18.2   75298   495466      3848    2888    377 45148    7    98   38   7%      1   95   14    1 2293%
c i   18.2   75276   495466      3850    2889    377 45148    7    98   38   7%      1   95   14    1 2276%
c i   18.3   75269   495466      3913    2939    382 45155    7    99   38   7%      1   96   13    1 2059%
c i   18.3   75261   495466      3921    2943    383 45157    7    99   38   7%      1   96   13    1 2008%
c i   18.4   75186   495466      3948    2956    386 45166    7    99   38   7%      1   96   12    1 1873%
c i   18.5   75176   495466      4014    3011    389 45173    7    99   38   7%      1   96   11    1 1699%
c i   18.6   75141   495466      4068    3057    393 45176    7   100   38   7%      1   96   12    1 1810%
c i   18.6   75128   495466      4085    3071    393 45178    7   100   38   7%      1   97   12    1 1846%
c i   18.6   75058   495466      4116    3094    397 45180    7   100   38   7%      1   97   12    1 1790%
c i   18.7   74920   495466      4183    3142    404 45190    7   100   38   7%      1   96   11    1 1596%
c i   18.7   74913   495466      4202    3154    407 45192    7   100   38   7%      1   96   10    1 1522%
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   18.8   74768   495466      4235    3177    411 45196    7   101   38   7%      1   97    9    1 1399%
c i   19.0   74657   495466      4382    3268    432 45229    7   103   38   7%      1   99    9    1 1273%
c i   19.1   74608   495466      4413    3292    434 45233    7   103   38   7%      1   99    8    1 1221%
c i   19.1   74607   495466      4414    3292    434 45233    7   103   38   7%      1   99    8    1 1216%
c i   19.1   74605   495466      4443    3311    437 45239    7   103   38   7%      1   99    8    1 1199%
c i   19.1   74604   495466      4444    3311    437 45239    7   103   38   7%      1   99    8    1 1194%
c i   19.1   74592   495466      4455    3321    437 45239    7   103   38   7%      1   99    8    1 1173%
c i   19.1   74581   495466      4480    3336    441 45244    7   103   38   7%      1   99    8    1 1114%
c i   19.4   74571   495466      4720    3539    459 45257    8   104   38   7%      1   99   13    1 1697%
c i   19.5   74562   495466      4786    3595    463 45262    8   105   38   7%      1  100   12    1 1618%
c i   19.5   74551   495466      4801    3604    466 45264    8   106   38   7%      1  101   12    1 1611%
c i   19.5   74341   495466      4817    3619    466 45264    8   106   38   7%      1  101   12    1 1637%
c i   19.6   74331   495466      4843    3644    466 45264    8   106   38   7%      1  102   15    1 1881%
c i   19.6   74328   495466      4869    3664    470 45265    8   106   38   7%      1  102   15    1 1947%
c i   19.6   74316   495466      4896    3687    472 45266    8   107   38   7%      1  102   14    1 1841%
c i   19.6   74303   495466      4920    3705    473 45270    8   107   38   7%      1  102   14    1 1729%
c i   19.8   74293   495466      4975    3749    478 45274    8   108   38   7%      1  103   12    1 1567%
c i   19.8   74292   495466      4976    3749    478 45274    8   108   38   7%      1  103   12    1 1561%
c i   19.9   74283   495466      5082    3832    482 45291    8   114   38   7%      1  109   16    1 1966%
c i   20.0   74274   495466      5145    3879    488 45298    8   114   38   7%      1  109   14    1 1683%
c i   20.0   74265   495466      5146    3879    488 45298    8   114   38   7%      1  109   14    1 1677%
c i   20.2   74254   495466      5301    4008    498 45312    8   116   38   7%      1  110   14    1 1597%
c i   20.3   74245   495466      5343    4037    504 45317    8   116   38   7%      1  110   13    1 1447%
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   74113   495466      5344    4037    504 45317    8   116   38   7%      1  110   13    1 1441%
c i   20.4   74110   495466      5401    4087    505 45322    8   117   38   7%      1  112   12    1 1365%
c i   20.6   74079   495466      5554    4214    515 45329   10   123   38   8%      1  117   27    1 2770%
c i   20.6   74069   495466      5572    4226    517 45330   10   124   38   8%      1  118   26    1 2653%
c i   20.8   74058   495466      5656    4296    521 45335   10   128   38   8%      1  122   23    1 2293%
c i   20.8   74046   495466      5670    4304    523 45338   10   128   38   8%      1  122   22    1 2197%
c i   20.8   74040   495466      5686    4318    524 45338   10   129   38   8%      1  123   22    1 2164%
c i   20.9   74032   495466      5723    4348    526 45340   10   130   38   8%      1  124   23    1 2274%
c i   21.0   74024   495466      5792    4403    532 45345   10   130   38   8%      1  124   21    1 2008%
c i   21.0   73880   495466      5794    4403    532 45346   10   130   38   8%      1  124   21    1 1993%
c i   21.2   73847   495466      5950    4533    541 45361   11   136   38   8%      1  130   23    1 2104%
c i   21.3   73838   495466      5980    4557    542 45361   11   136   38   8%      1  129   22    1 1958%
c i   21.3   73830   495466      5986    4559    545 45361   11   135   38   8%      1  129   21    1 1921%
c i   21.3   73822   495466      6010    4576    548 45364   11   135   38   8%      1  128   20    1 1795%
c i   21.4   73812   495466      6061    4606    555 45376   11   136   38   8%      1  129   17    1 1542%
c i   21.5   73805   495466      6132    4651    573 45381   11   135   39   8%      1  128   15    1 1318%
c i   21.8   73804   495466      6289    4780    583 45393   12   142   39   8%      1  134   23    1 1902%
c i   22.0   73792   495466      6464    4938    586 45399   12   142   39   9%      1  135   26    1 2058%
c i   22.0   73789   495466      6472    4943    587 45400   12   142   39   9%      1  135   26    1 2022%
c i   22.0   73778   495466      6514    4973    592 45406   12   143   39   9%      1  135   23    1 1791%
c i   22.1   73765   495466      6532    4987    594 45407   12   143   39   9%      1  135   22    1 1716%
c i   22.1   73764   495466      6539    4992    594 45408   12   143   39   9%      1  135   22    1 1689%
c i   22.1   73753   495466      6541    4992    594 45409   12   143   39   9%      1  135   22    1 1676%
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   22.2   73741   495466      6583    5027    596 45412   13   144   39   9%      1  136   23    1 1754%
c i   22.2   73738   495466      6584    5027    596 45412   13   144   39   9%      1  136   23    1 1747%
c i   22.2   73710   495466      6611    5049    597 45414   13   144   39   9%      1  136   22    1 1682%
c i   22.2   73166   495466      6646    5077    601 45415   13   145   39   9%      1  137   21    1 1571%
c i   22.3   73153   495466      6651    5080    602 45415   13   145   39   9%      1  137   20    1 1550%
c i   22.4   73146   495466      6743    5155    608 45423   13   145   39   9%      1  136   20    1 1458%
c i   22.7   73142   495466      6961    5339    619 45438   13   148   39   9%      1  139   25    1 1790%
c 
c [simplification-6] limit 7125 conflicts (hard 17030) hit after 7125 conflicts
c [quatres-2] found 27924 quaternary clauses 38% in total
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 73142 free variables schedulable
c [ternres-2] 8 ternary resolvents (1 bin, 7 trn)
c [ternres-2] 38750 variables remain 53% (34392 retained 47%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2268 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2268 out of 2268 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 2588 variables
c [simpleprobe-3] all 73070 free variables schedulable
c [simpleprobe-3] limit 5528119 penalty 1 = 1 + 0
c [decomp-12] removed 610 variables
c [simpleprobe-3] 42900 variables remain 59% (29560 retained 41%)
c [simpleprobe-3] removed 610 variables, found 14065 hbrs, 269 units
c [unhide-6] limit 552811 with penalty 0 = 0 + 0
c [unhide-6-6] 11 units, 459 failed, 5466 tauts, 0 hbrs, 8130 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 205 transitive binary clauses
c [transred-2] found 6 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 71683 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 642 blocked clauses
c [block-2] 642 < 1/100 * 473189 = 4731 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 71683 variables 100%
c [elim-5] limit of 27640599 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 6831 not tried 10% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3378 = 5% variables out of 71683 scheduled
c [bca-2] limit of 10000000 steps and 917164 added (scaled 2)
c [bca-2] 113521 out of 136612 literals actually usable 83%
c [bca-2] added 67 blocked clauses in 310783 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4167 pos 6.1% + 64122 neg 93.9% = 68289 sched 100.0% ret 16
c [sweep-2-1] 1197642 steps 11 queries 16596.09 avg class size
c [sweep-2-1] 120 decisions 9 SAT calls 48.11 avg env size
c [sweep-2-1] 68259 variables remain 100% (46 retained 0%)
c [decomp-13] removed 14 variables
c [sweep-2-1] removed 14 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-6] 453779 negative 99.0% of 458266 except 4487 1.0%
c [phase-count-6] 366598 positive 80.0% of 458266 except 91668 20.0%
c [phase-count-6] less non-negative clauses 4487 than limit 45800 (10.0%)
c [phase-count-6] non-pos/non-neg = 91668/4487 = 20.43 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 41 negative 100%
c [sort-queue-6] sorted 68291 enqueued variables after 7125 conflicts
c [score-dist-6] active 0 (0%), one 44139 (65%), zero 24152 (35%)
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 4851 variables 6.6% (68291 remain 36%)
c [simplification-6] removed 37200 irredundant clauses 7.5% (458266 remain 45%)
c [simplification-6] maximum reduction of 8% = max (7%, 8%)
c [simplification-6] large reduction 8% >= 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 19125 (soft 9125 + delta 10000)
c [simplification-6] new conflict limit 9125 (hard 19125)
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   26.3   68290   458266      7291    4641    574 50233   14   154   37   9%      1  145   22    2 1420%
c i   26.3   68286   458266      7316    4660    576 50236   14   154   37   9%      1  145   20    2 1325%
c i   26.4   68277   458266      7414    4743    583 50241   14   156   37   9%      1  146   18    2 1146%
c i   26.6   68269   458266      7530    4842    588 50249   14   157   37   9%      1  147   20    2 1275%
c i   26.7   68265   458266      7622    4922    593 50253   14   159   37   9%      1  149   23    2 1399%
c i   26.8   68257   458266      7667    4960    594 50258   14   160   37   9%      1  150   21    2 1319%
c i   27.0   68252   458266      7839    5113    600 50268   14   162   37   9%      1  151   17    2 1044%
c i   27.0   68246   458266      7850    5121    602 50268   14   162   37   9%      1  151   17    2 1020%
c i   27.2   68237   458266      8032    5278    607 50283   15   163   37   9%      1  152   30    2 1726%
c i   27.3   68234   458266      8120    5351    610 50292   15   164   37   9%      1  152   27    2 1542%
c i   27.3   68221   458266      8192    5413    613 50296   16   164   37  10%      1  153   30    2 1660%
c i   27.4   68216   458266      8245    5458    615 50300   16   164   37  10%      1  153   32    2 1719%
c i   27.6   68209   458266      8390    5564    632 50320   16   165   37  10%      1  153   21    2 1147%
c i   27.6   68208   458266      8391    5564    632 50320   16   165   37  10%      1  153   21    2 1142%
c i   27.7   68206   458266      8496    5652    637 50325   16   163   37  10%      1  151   21    2 1126%
c i   28.1   68197   458266      8850    5939    658 50352   17   163   37  10%      2  150   21    2 1040%
c i   28.4   68190   458266      9018    6081    669 50365   17   163   37  10%      1  149   20    2  970%
c i   28.4   68183   458266      9046    6106    670 50366   17   165   37  10%      1  151   20    2  960%
c i   28.5   68176   458266      9120    6159    677 50376   17   165   37  10%      1  151   17    2  831%
c 
c [simplification-7] limit 9135 conflicts (hard 19125) hit after 9136 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 36160 schedulable variables 53%
c [ternres-3] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-3] 2739 variables remain 4% (65433 retained 96%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 31 xors of average arity 2.9
c [gauss-2] connected 91 occurrences of 88 variables (average 1.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 13 variables
c [treelook-3] limit 344977 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 54973 literals 40%
c [treelook-3] scheduling used 346200 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 344977 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 406957 steps
c [treelook-3] 54964 literals remain 40%
c [treelook-3] 32310 variables remain to probed next time 47%
c [treelook-3] removed 2 variables, found 2566 hbrs
c [unhide-7] limit 689954 with penalty 0 = 0 + 0
c [unhide-7-7] 2 units, 122 failed, 5244 tauts, 0 hbrs, 8004 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 201 transitive binary clauses
c [transred-3] found 6 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 259 (1%) of length 10
c [cce-2-1] eliminated 16 clauses out of 1214 (1%) of length 9
c [cce-2-1] eliminated 22 clauses out of 434 (5%) of length 8
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 40 large clauses in 15000002 steps
c [cce-2-1] allowing another 7500001 steps for small clauses
c [cce-2-1] scheduling 242389 clauses = 223638 binary + 18751 ternary
c [cce-2-1] tried to eliminate 271 small clauses 0%
c [cce-2-1] eliminated 62 binary clauses 0%
c [cce-2-1] eliminated 11 ternary clauses 0%
c [cce-2-1] eliminated 73 small clauses 0%
c [cce-2-1] eliminated 1482 small clauses in 15000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1522 covered clauses in round 1
c [cce-2] eliminated 1522 covered clauses in TOTAL during 1 rounds
c [cce-2] 1522 < 1/100 * 452424 = 4524 considered unsuccessful
c [elim-6] 6815 variables 10% will be scheduled this time
c [elim-6] scheduled 6815 variables 10%
c [elim-6] limit of 68995467 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 16106802 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 6815 scheduled
c [bca-3] limit of 10000000 steps and 902195 added (scaled 2)
c [bca-3] 110069 out of 135998 literals actually usable 81%
c [bca-3] added 130 blocked clauses in 296495 steps
c [sweep-3] limit 1034932 penalty 0 = 0 + 0
c [sweep-3-1] 4381 pos 6.4% + 63574 neg 93.6% = 67955 sched 99.9% ret 43
c [sweep-3-1] 1292397 steps 11 queries 23370.64 avg class size
c [sweep-3-1] 71 decisions 8 SAT calls 53.62 avg env size
c [sweep-3-1] 67910 variables remain 100% (74 retained 0%)
c [decomp-16] removed 28 variables
c [sweep-3-1] removed 28 vars (0 failed, 2 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 28 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-7] 446151 negative 99.0% of 450638 except 4487 1.0%
c [phase-count-7] 361026 positive 80.1% of 450638 except 89612 19.9%
c [phase-count-7] less non-negative clauses 4487 than limit 45000 (10.0%)
c [phase-count-7] non-pos/non-neg = 89612/4487 = 19.97 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 41 negative 100%
c [sort-queue-7] sorted 67970 enqueued variables after 9136 conflicts
c [score-dist-7] active 0 (0%), one 45691 (67%), zero 22279 (33%)
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 202 variables 0.3% (67970 remain 36%)
c [simplification-7] removed 7628 irredundant clauses 1.7% (450638 remain 45%)
c [simplification-7] maximum reduction of 2% = max (0%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 10666
c [simplification-7] penalized conflict interval 10666 = 1 * 10666
c [simplification-7] hard conflict limit 29802 (soft 19802 + delta 10000)
c [simplification-7] new conflict limit 19802 (hard 29802)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   31.4   67969   450638      9170    6181    678 52676   17   169   38  10%      1  155   22    2 1033%
c i   31.8   67963   450638      9487    6468    689 52690   18   169   38  10%      2  155   23    2 1028%
c i   32.1   67962   450638      9748    6696    695 52702   18   171   38  11%      2  156   31    2 1329%
c i   32.2   67961   450638      9750    6697    695 52702   18   171   38  11%      2  156   31    2 1320%
c i   32.2   67957   450638      9793    6728    697 52710   18   170   38  11%      2  155   28    2 1181%
c i   32.2   67956   450638      9804    6738    697 52710   18   170   38  11%      2  155   27    2 1146%
c i   32.3   67955   450638      9837    6766    698 52713   18   171   38  11%      2  156   26    2 1122%
c i   32.3   67954   450638      9876    6800    698 52716   18   172   38  11%      2  157   26    2 1107%
c i   32.5   67953   450638     10025    6934    700 52726   19   173   38  11%      1  157   29    2 1210%
c i   32.5   67947   450638     10063    6959    708 52729   19   173   38  11%      1  157   28    2 1159%
c i   32.6   67912   450638     10084    6973    710 52733   19   173   38  11%      1  157   27    2 1106%
c i   32.6   67906   450638     10111    6996    711 52733   19   173   38  11%      1  157   25    2 1032%
c i   32.7   67902   450638     10163    7039    715 52736   19   173   38  11%      1  157   25    2 1005%
c i   32.7   67893   450638     10194    7062    716 52742   19   173   38  11%      1  157   24    2  976%
c i   32.8   67884   450638     10239    7097    719 52748   19   174   38  11%      1  158   22    2  887%
c i   32.8   67874   450638     10268    7118    722 52751   19   173   38  11%      1  157   20    2  810%
c i   32.8   67868   450638     10269    7118    722 52751   19   173   38  11%      1  157   20    2  807%
c i   33.0   67722   450638     10404    7241    724 52756   19   172   38  11%      1  155   24    3  948%
c i   33.0   67714   450638     10432    7260    728 52758   19   174   38  11%      1  157   23    3  894%
c i   33.1   67608   450638     10457    7275    730 52764   19   173   38  11%      1  156   21    3  826%
c i   33.2   67579   450638     10507    7315    733 52770   19   173   38  11%      1  156   19    3  761%
c i   33.2   67574   450638     10560    7362    735 52772   19   172   38  11%      1  155   19    3  724%
c i   33.4   67501   450638     10662    7452    739 52778   19   173   38  11%      1  156   16    3  631%
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   33.4   67500   450638     10729    7508    740 52783   19   172   38  11%      1  155   19    3  738%
c i   33.6   67499   450638     10812    7578    745 52788   19   173   38  11%      1  156   17    3  647%
c i   33.6   67494   450638     10813    7578    745 52788   19   173   38  11%      1  156   17    3  644%
c i   34.1   67471   450638     11247    7944    760 52829   19   175   38  11%      2  157   19    3  696%
c i   34.1   67470   450638     11248    7944    760 52829   19   175   38  11%      2  156   19    3  693%
c i   34.5   67469   450638     11539    8203    774 52843   19   174   38  11%      2  155   17    3  620%
c i   34.6   67459   450638     11558    8218    774 52846   19   174   38  11%      2  155   17    3  609%
c i   34.7   67451   450638     11654    8299    780 52853   19   175   38  11%      2  156   16    3  572%
c i   34.9   67450   450638     11840    8452    788 52864   19   174   38  11%      2  154   21    3  743%
c i   35.0   67441   450638     12010    8614    788 52868   19   173   38  11%      2  152   24    3  808%
c i   35.1   67438   450638     12037    8638    788 52870   19   173   38  11%      2  153   24    3  811%
c i   35.2   67429   450638     12102    8696    789 52875   20   175   38  11%      1  154   26    3  867%
c i   35.3   67420   450638     12145    8732    790 52880   20   176   38  11%      1  155   26    3  878%
c i   35.4   67408   450638     12212    8791    792 52885   20   178   38  11%      1  157   25    3  845%
c i   35.4   67395   450638     12224    8799    793 52887   20   178   38  11%      1  157   25    3  822%
c i   35.5   67384   450638     12378    8926    801 52898   20   176   38  11%      1  155   25    3  800%
c i   35.6   67383   450638     12453    8982    808 52908   20   175   38  11%      1  154   20    3  653%
c i   36.2   67377   450638     12846    9318    829 52932   20   180   38  11%      2  158   28    3  882%
c i   36.4   67234   450638     12996    9447    838 52941   21   186   39  11%      2  163   34    3 1037%
c i   36.6   67233   450638     13123    9555    846 52948   22   186   39  12%      2  163   35    3 1053%
c i   36.7   67232   450638     13206    9632    848 52951   22   189   39  12%      1  166   38    3 1108%
c i   36.8   67231   450638     13218    9640    849 52953   22   189   39  12%      1  166   37    3 1091%
c i   36.8   67159   450638     13242    9662    849 52954   22   188   39  12%      1  165   35    3 1018%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   36.9   67158   450638     13343    9750    856 52958   22   188   39  12%      1  164   31    3  906%
c i   37.1   67157   450638     13426    9826    857 52961   22   190   39  12%      1  166   34    3  959%
c i   37.2   67147   450638     13495    9885    860 52965   22   193   39  12%      1  169   30    4  856%
c i   37.3   67138   450638     13539    9925    861 52965   22   194   39  12%      1  170   31    4  879%
c i   37.3   67137   450638     13543    9925    862 52966   22   194   39  12%      1  169   31    4  866%
c i   37.4   67136   450638     13643   10019    865 52967   22   194   40  12%      1  169   28    4  792%
c i   37.4   67135   450638     13669   10043    865 52968   22   193   40  12%      1  169   26    4  732%
c i   37.5   67134   450638     13731   10095    869 52973   22   196   41  11%      1  171   27    4  752%
c i   38.0   67123   450638     14056   10376    879 52990   23   195   41  12%      1  170   28    4  751%
c i   38.0   67120   450638     14086   10402    880 52992   23   195   41  12%      1  170   27    4  717%
c i   38.2   67119   450638     14274   10577    885 52995   23   201   41  12%      1  175   33    4  857%
c i   38.3   67118   450638     14319   10607    887 53006   23   201   41  12%      1  175   30    4  787%
c i   38.6   67106   450638     14534   10797    895 53017   24   203   41  12%      1  176   29    4  741%
c i   38.6   67105   450638     14598   10856    897 53018   23   201   41  12%      1  174   25    4  650%
c i   38.7   67098   450638     14656   10904    898 53021   23   201   41  12%      1  174   24    4  603%
c i   38.8   66946   450638     14679   10920    900 53024   23   201   41  12%      1  174   23    4  587%
c i   39.4   66940   450638     15089   11285    908 53046   25   203   41  12%      2  175   43    4 1038%
c i   39.4   66939   450638     15106   11301    908 53046   25   203   41  12%      2  174   43    4 1044%
c i   39.5   66935   450638     15243   11428    912 53048   25   205   41  12%      2  176   42    4  995%
c i   39.6   66934   450638     15302   11481    915 53050   26   206   41  13%      2  177   43    4 1006%
c i   40.0   66865   450638     15519   11664    926 53068   26   208   42  13%      2  179   40    4  913%
c i   40.2   66860   450638     15680   11809    928 53070   27   210   42  13%      1  180   41    4  916%
c i   40.4   66859   450638     15773   11893    932 53073   28   212   42  13%      1  182   46    5 1013%
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   40.5   66063   450638     15885   11991    933 53083   28   212   42  13%      1  182   42    5  919%
c i   40.8   65978   450638     16106   12191    939 53096   28   214   42  13%      1  183   37    5  787%
c i   41.1   65969   450638     16266   12328    949 53107   29   216   42  13%      1  185   37    5  775%
c i   41.1   65965   450638     16294   12353    949 53109   29   218   42  13%      1  186   36    5  755%
c i   41.4   65715   450638     16469   12520    950 53114   29   217   42  13%      1  185   35    5  711%
c i   42.4   65707   450638     17230   13202    979 53150   30   221   43  13%      4  187   36    5  686%
c i   42.4   65706   450638     17231   13202    979 53150   30   221   43  13%      4  187   36    5  683%
c i   42.4   65698   450638     17245   13213    980 53151   30   220   43  13%      4  186   34    5  654%
c i   42.6   65697   450638     17340   13299    982 53155   29   219   43  13%      4  185   29    5  562%
c i   43.2   65696   450638     17821   13731    992 53174   30   218   43  14%      4  182   33    5  602%
c i   43.3   65695   450638     17906   13799    998 53179   30   217   43  14%      3  181   37    5  670%
c i   43.8   65694   450638     18220   14077   1007 53198   30   221   43  14%      3  184   28    6  509%
c i   43.8   65646   450638     18258   14110   1009 53200   30   221   43  13%      3  184   27    6  477%
c i   44.7   65644   450638     18949   14713   1037 53244   31   221   44  14%      4  182   43    6  721%
c i   44.7   65643   450638     18950   14713   1037 53244   31   221   44  14%      4  182   42    6  718%
c i   44.8   65637   450638     19030   14787   1038 53246   31   220   44  14%      4  181   41    6  684%
c i   44.8   65617   450638     19048   14801   1039 53246   31   221   44  14%      4  181   39    6  661%
c i   44.9   65616   450638     19050   14802   1039 53246   31   220   44  14%      4  181   39    6  657%
c i   44.9   65610   450638     19072   14822   1039 53247   31   221   44  14%      4  182   38    6  632%
c i   44.9   65609   450638     19073   14822   1039 53247   31   221   44  14%      4  182   38    6  630%
c i   45.0   65602   450638     19144   14888   1039 53247   31   221   44  14%      4  181   42    6  699%
c i   45.2   65574   450638     19264   14998   1042 53252   31   219   44  14%      3  179   38    6  630%
c i   45.2   65571   450638     19265   14998   1042 53252   31   219   44  14%      3  179   38    6  628%
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   45.2   65566   450638     19266   14998   1042 53252   31   219   44  14%      3  179   38    6  626%
c i   45.4   65564   450638     19461   15178   1047 53257   31   219   44  14%      3  178   33    6  547%
c i   45.6   65563   450638     19588   15298   1047 53260   31   219   44  14%      3  178   35    6  573%
c i   45.9   65558   450638     19770   15463   1050 53267   31   219   44  14%      2  178   31    6  493%
c 
c [simplification-8] limit 19894 conflicts (hard 29802) hit after 19894 conflicts
c [quatres-3] found 29020 quaternary clauses 41% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [ternres-4] limit 7427894 with penalty 0 = 0 + 0
c [ternres-4] 2623 schedulable variables 4%
c [ternres-4] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 3327 variables
c [basicprobe-3] limit 37139471 penalty 0 = 0 + 0
c [basicprobe-3-0] 21909 probes remain 34% after last round
c [basicprobe-3-0] 166 units = 166 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1053 variables, found 92190 hbrs
c [bate-1] eliminated 89 asymmetric tautologies during probing
c [unhide-8] limit 1485578 with penalty 0 = 0 + 0
c [unhide-8-8] 7 units, 885 failed, 14528 tauts, 0 hbrs, 53527 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 124 transitive binary clauses
c [transred-4] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 62970 variables 100%
c [block-3] limit of 37139471 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 341 blocked clauses
c [block-3] 341 < 1/100 * 423509 = 4235 considered unsuccessful
c [bca-4] limit of 10000000 steps and 834884 added (scaled 2)
c [bca-4] 94844 out of 125940 literals actually usable 75%
c [bca-4] added 238 blocked clauses in 250113 steps
c [sweep-4] limit 2228368 penalty 0 = 0 + 0
c [sweep-4-1] 4135 pos 6.6% + 58777 neg 93.4% = 62912 sched 99.9% ret 57
c [sweep-4-1] 2364577 steps 24 queries 8536.58 avg class size
c [sweep-4-1] 636 decisions 23 SAT calls 316.43 avg env size
c [sweep-4-1] 62711 variables remain 100% (253 retained 0%)
c [decomp-18] removed 38 variables
c [sweep-4-1] removed 38 vars (0 failed, 1 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 38 vars in TOTAL (1 rounds, 23 queries)
c [phase-count-8] 412504 negative 98.9% of 416972 except 4468 1.1%
c [phase-count-8] 330694 positive 79.3% of 416972 except 86278 20.7%
c [phase-count-8] less non-negative clauses 4468 than limit 41600 (10.0%)
c [phase-count-8] non-pos/non-neg = 86278/4468 = 19.31 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 10 negative 100%
c [sort-queue-8] sorted 62931 enqueued variables after 19894 conflicts
c [score-dist-8] active 0 (0%), one 45651 (73%), zero 17280 (27%)
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 2372 variables 3.6% (62931 remain 33%)
c [simplification-8] removed 33666 irredundant clauses 7.5% (416972 remain 41%)
c [simplification-8] maximum reduction of 7% = max (4%, 7%)
c [simplification-8] large reduction 7% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 31894 (soft 21894 + delta 10000)
c [simplification-8] new conflict limit 21894 (hard 31894)
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   50.9   62930   416972     20414   15743   1030 127922   36   230   47  15%      4  187   50    7  733%
c i   51.2   62929   416972     20666   15959   1041 127938   35   232   47  15%      3  188   37    7  532%
c i   51.9   62928   416972     21155   16411   1053 127949   38   235   47  16%      3  190   50    7  693%
c i   52.1   62927   416972     21279   16523   1054 127953   38   234   47  16%      3  189   50    7  679%
c i   52.1   62926   416972     21280   16523   1054 127953   38   234   47  16%      3  189   50    7  677%
c i   52.2   62915   416972     21348   16584   1057 127956   38   236   47  16%      3  190   45    7  611%
c i   52.3   62900   416972     21418   16643   1061 127960   38   235   47  16%      3  190   41    7  559%
c i   52.8   62899   416972     21881   17040   1079 127986   37   229   47  16%      3  182   29    8  381%
c 
c [simplification-9] limit 21904 conflicts (hard 31894) hit after 21904 conflicts
c [quatres-4] found 31544 quaternary clauses 45% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-5] limit 8132521 with penalty 0 = 0 + 0
c [ternres-5] all 62899 free variables schedulable
c [ternres-5] 25 ternary resolvents (0 bin, 25 trn)
c [ternres-5] 62 variables remain 0% (62837 retained 100%)
c [decomp-19] removed 96 variables
c [simpleprobe-4] 37824 schedulable variables 60%
c [simpleprobe-4] limit 32530084 penalty 0 = 0 + 0
c [decomp-20] removed 992 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 992 variables, found 54681 hbrs, 440 units
c [unhide-9] limit 1626504 with penalty 0 = 0 + 0
c [unhide-9-9] 7 units, 104 failed, 9747 tauts, 0 hbrs, 30626 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 261 transitive binary clauses
c [transred-5] found 6 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 61718 variables 100%
c [elim-7] limit of 81325210 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2451 variables 4% in round 1 in 37187937 steps
c [elim-7-1] backward subsumption/strengthening limit 37187900
c [elim-7-1-1] backward checking 8697 touched variables 14%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 16 and strengthened 96 clauses in 3138176 steps
c [elim-7-1] rescheduled 288 variables 0% by backward subsumption
c [elim-7-2] eliminated 28 variables 0% in round 2 in 602693 steps
c [elim-7-2] backward subsumption/strengthening limit 602600
c [elim-7-2-1] backward checking 266 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 2 and strengthened 9 clauses in 210529 steps
c [elim-7-2] rescheduled 21 variables 0% by backward subsumption
c [elim-7-3] eliminated 3 variables 0% in round 3 in 19858 steps
c [elim-7-3] backward subsumption/strengthening limit 19800
c [elim-7-3-1] backward checking 30 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 1 and strengthened 2 clauses in 19801 steps
c [elim-7] incomplete 12 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2482 = 4% variables out of 61718 scheduled
c [bca-5] limit of 10000000 steps and 791373 added (scaled 2)
c [bca-5] 90918 out of 118474 literals actually usable 77%
c [bca-5] added 63 blocked clauses in 242449 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 24397560 penalty 0 = 0 + 0
c [sweep-5-1] 3700 pos 6.3% + 55326 neg 93.7% = 59026 sched 99.6% ret 210
c [sweep-5-1] 24489353 steps 290 queries 1242.69 avg class size
c [sweep-5-1] 2987 decisions 252 SAT calls 106.51 avg env size
c [sweep-5-1] 50739 variables remain 86% (8422 retained 14%)
c [decomp-21] removed 126 variables
c [sweep-5-1] removed 126 vars (0 failed, 45 eqs, 76 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 126 vars in TOTAL (1 rounds, 289 queries)
c [phase-count-9] 390427 negative 99.0% of 394485 except 4058 1.0%
c [phase-count-9] 312078 positive 79.1% of 394485 except 82407 20.9%
c [phase-count-9] less non-negative clauses 4058 than limit 39400 (10.0%)
c [phase-count-9] non-pos/non-neg = 82407/4058 = 20.31 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 10 negative 100%
c [sort-queue-9] sorted 59110 enqueued variables after 21904 conflicts
c [score-dist-9] active 0 (0%), one 43766 (74%), zero 15344 (26%)
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 3789 variables 6.0% (59110 remain 31%)
c [simplification-9] removed 22487 irredundant clauses 5.4% (394485 remain 39%)
c [simplification-9] maximum reduction of 6% = max (6%, 5%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 33904 (soft 23904 + delta 10000)
c [simplification-9] new conflict limit 23904 (hard 33904)
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   58.8   59109   394485     22260   13107    988 191356   37   228   43  16%      3  180   35    8  449%
c i   59.0   59108   394485     22421   13248    992 191366   37   229   43  16%      2  181   33    8  429%
c i   59.0   59100   394485     22422   13248    992 191366   37   229   43  16%      2  180   33    8  427%
c i   60.4   58937   394485     23548   14273   1031 191396   37   234   43  16%      7  182   33    8  404%
c i   60.7   58934   394485     23748   14458   1037 191400   36   234   43  16%      6  181   29    8  344%
c 
c [simplification-10] limit 23914 conflicts (hard 33904) hit after 23914 conflicts
c [quatres-5] found 30904 quaternary clauses 45% in total
c [quatres-5-2] added 4 quaternary resolvents
c [ternres-6] limit 8813342 with penalty 0 = 0 + 0
c [ternres-6] 58 schedulable variables 0%
c [ternres-6] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 550833 penalty 3 = 3 + 0
c [card-4] found 1400 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 550833 for elimination
c [card-4] 1400 out of 1400 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 10 xors of average arity 2.8
c [gauss-3] connected 28 occurrences of 28 variables (average 1.0)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 10 variables
c [treelook-4] limit 881334 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 84360 literals 72%
c [treelook-4] scheduling used 881408 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 881334 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1080575 steps
c [treelook-4] 84352 literals remain 72%
c [treelook-4] 25916 variables remain to probed next time 44%
c [treelook-4] removed 0 variables, found 6560 hbrs
c [unhide-10] limit 1762668 with penalty 0 = 0 + 0
c [unhide-10-10] 6 units, 341 failed, 17986 tauts, 0 hbrs, 25737 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 226 transitive binary clauses
c [cce-3] limit of 11016678 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 193 (1%) of length 10
c [cce-3-1] eliminated 2 clauses out of 388 (1%) of length 8
c [cce-3-1] eliminated 21 clauses out of 598 (4%) of length 7
c [cce-3-1] eliminated 587 clauses out of 4071 (14%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 611 large clauses in 11016679 steps
c [cce-3-1] allowing another 5508339 steps for small clauses
c [cce-3-1] scheduling 216440 clauses = 197713 binary + 18727 ternary
c [cce-3-1] tried to eliminate 235 small clauses 0%
c [cce-3-1] eliminated 56 binary clauses 0%
c [cce-3-1] eliminated 11 ternary clauses 0%
c [cce-3-1] eliminated 67 small clauses 0%
c [cce-3-1] eliminated 3131 small clauses in 11016678 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3742 covered clauses in round 1
c [cce-3] eliminated 3742 covered clauses in TOTAL during 1 rounds
c [cce-3] 3742 < 1/100 * 393038 = 3930 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 58634 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3525337100 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 296 variables 1% in round 1 in 35599613 steps
c [elim-8-1] backward subsumption/strengthening limit 35599600
c [elim-8-1-1] backward checking 1378 touched variables 2%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 6 and strengthened 31 clauses in 659210 steps
c [elim-8-1] rescheduled 96 variables 0% by backward subsumption
c [elim-8-2] eliminated 8 variables 0% in round 2 in 288400 steps
c [elim-8-2] backward subsumption/strengthening limit 288400
c [elim-8-2-1] backward checking 75 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 2 clauses in 111563 steps
c [elim-8-2] rescheduled 8 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 10569 steps
c [elim-8-3] backward subsumption/strengthening limit 10500
c [elim-8-3-1] backward checking 10 touched variables 0%
c [elim-8-3-1] incomplete backward checking 2 remain 20%
c [elim-8-3] subsumed 0 and strengthened 2 clauses in 10551 steps
c [elim-8] incomplete 8 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 307 = 1% variables out of 58634 scheduled
c [elim-8] 307 < 1/100 * 58634 = 586 considered unsuccessful
c [bca-6] limit of 10000000 steps and 777621 added (scaled 2)
c [bca-6] 89317 out of 116656 literals actually usable 77%
c [bca-6] added 57 blocked clauses in 236770 steps
c [sweep-6] limit 2644002 penalty 0 = 0 + 0
c [sweep-6-1] 3276 pos 6.5% + 46959 neg 93.5% = 50235 sched 86.1% ret 8092
c [sweep-6-1] 3062021 steps 35 queries 5829.63 avg class size
c [sweep-6-1] 606 decisions 28 SAT calls 136.36 avg env size
c [sweep-6-1] 49908 variables remain 86% (8328 retained 14%)
c [decomp-24] removed 101 variables
c [sweep-6-1] removed 101 vars (0 failed, 6 eqs, 11 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 101 vars in TOTAL (1 rounds, 34 queries)
c [phase-count-10] 384532 negative 99.1% of 387980 except 3448 0.9%
c [phase-count-10] 305773 positive 78.8% of 387980 except 82207 21.2%
c [phase-count-10] less non-negative clauses 3448 than limit 38700 (10.0%)
c [phase-count-10] non-pos/non-neg = 82207/3448 = 23.84 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 10 negative 100%
c [sort-queue-10] sorted 58226 enqueued variables after 23914 conflicts
c [score-dist-10] active 0 (0%), one 43696 (75%), zero 14530 (25%)
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 708 variables 1.2% (58226 remain 31%)
c [simplification-10] removed 6505 irredundant clauses 1.6% (387980 remain 38%)
c [simplification-10] maximum reduction of 2% = max (1%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 17332
c [simplification-10] penalized conflict interval 17332 = 1 * 17332
c [simplification-10] hard conflict limit 51246 (soft 41246 + delta 10000)
c [simplification-10] new conflict limit 41246 (hard 51246)
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   64.8   58225   387980     23992   11993   1035 180783   36   232   40  15%      5  179   28    8  332%
c i   65.3   58222   387980     24408   12375   1048 180793   34   221   40  16%      4  167   22    8  254%
c i   65.3   58215   387980     24409   12375   1048 180793   34   221   40  16%      4  167   21    8  253%
c i   66.0   58171   387980     25058   12952   1070 180820   35   226   40  15%      5  170   32    9  366%
c i   66.2   58170   387980     25145   13032   1073 180823   35   228   40  15%      4  172   33    9  379%
c i   66.2   58169   387980     25186   13064   1077 180826   35   228   40  15%      4  172   37    9  415%
c i   66.4   58168   387980     25366   13224   1081 180836   36   228   40  16%      3  171   52    9  581%
c i   66.9   58167   387980     25709   13543   1091 180844   36   228   40  16%      3  170   37    9  407%
c i   67.3   57958   387980     26063   13847   1111 180862   35   226   40  16%      3  167   37    9  401%
c i   67.3   57953   387980     26064   13847   1111 180862   35   226   40  16%      3  167   37    9  400%
c i   67.4   57941   387980     26137   13910   1113 180866   36   227   40  16%      3  168   41    9  446%
c i   67.4   57870   387980     26138   13910   1113 180866   36   227   40  16%      3  168   41    9  444%
c i   67.9   57868   387980     26487   14234   1121 180875   36   228   41  16%      2  169   40    9  421%
c i   68.1   57867   387980     26639   14376   1125 180879   36   230   41  15%      2  170   36    9  383%
c i   68.1   57866   387980     26663   14391   1128 180883   35   229   41  15%      2  169   34    9  360%
c i   68.3   57856   387980     26822   14534   1132 180891   35   228   41  15%      2  168   32    9  336%
c i   68.4   57855   387980     26856   14565   1133 180892   35   228   41  15%      2  168   31    9  330%
c i   68.5   57853   387980     26936   14639   1134 180894   35   228   41  15%      2  168   34   10  355%
c i   68.7   57851   387980     27137   14822   1137 180903   35   227   41  16%      1  166   37   10  388%
c i   69.1   57850   387980     27401   15059   1145 180912   35   226   41  16%      1  164   32   10  334%
c i   69.2   57816   387980     27470   15113   1150 180918   35   225   41  15%      1  163   30   10  304%
c i   69.2   57807   387980     27483   15119   1154 180920   35   224   41  15%      1  162   28   10  292%
c i   70.0   57667   387980     28155   15709   1174 180957   36   230   41  16%      3  166   38   10  375%
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   70.1   57664   387980     28177   15728   1174 180958   36   230   41  16%      3  166   37   10  369%
c i   70.2   57654   387980     28225   15773   1175 180958   36   230   41  16%      3  166   40   10  395%
c i   70.9   57653   387980     28806   16285   1197 180979   37   233   41  16%      3  168   43   10  416%
c i   71.1   57652   387980     28952   16408   1204 180982   37   232   41  16%      3  166   39   10  379%
c i   71.4   57651   387980     29185   16618   1217 180990   36   233   42  15%      3  167   31   10  295%
c i   71.5   57650   387980     29223   16655   1217 180990   36   233   42  15%      2  166   31   10  294%
c i   71.6   57649   387980     29272   16695   1223 180992   36   232   42  15%      2  166   29   10  278%
c i   71.6   57635   387980     29273   16695   1223 180992   36   232   42  15%      2  166   29   10  277%
c i   71.7   57624   387980     29402   16810   1226 180999   36   232   43  15%      2  166   33   11  314%
c i   72.4   57623   387980     29867   17234   1242 181014   38   238   44  16%      2  170   50   11  461%
c i   72.6   57407   387980     30001   17356   1245 181017   38   238   44  16%      2  169   48   11  443%
c i   72.8   57403   387980     30156   17500   1246 181022   38   238   45  16%      2  169   45   11  407%
c i   72.8   57402   387980     30159   17501   1246 181023   38   238   45  16%      2  169   44   11  402%
c i   73.1   57401   387980     30444   17748   1251 181039   38   238   46  16%      2  169   46   11  416%
c i   73.6   57400   387980     30784   18062   1260 181047   38   237   46  16%      2  167   33   11  292%
c i   73.7   57397   387980     30908   18172   1269 181050   38   235   46  16%      2  165   33   11  297%
c i   74.1   57396   387980     31192   18440   1274 181054   37   234   47  16%      2  163   35   11  305%
c i   74.7   57395   387980     31765   18954   1288 181073   41   232   47  18%      3  159   61   12  517%
c i   75.1   57394   387980     32013   19181   1295 181079   40   230   47  17%      2  156   39   12  326%
c i   75.2   56841   387980     32067   19231   1298 181079   39   230   47  17%      2  157   35   12  297%
c i   75.7   56840   387980     32461   19575   1312 181091   40   230   47  17%      2  156   49   12  409%
c i   75.8   56826   387980     32541   19647   1313 181094   40   230   47  18%      2  155   49   12  405%
c i   76.1   56825   387980     32738   19828   1318 181101   41   232   47  18%      2  157   52   12  428%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   76.6   56823   387980     33055   20117   1326 181107   42   234   47  18%      2  158   52   12  418%
c i   76.7   56822   387980     33191   20238   1331 181112   42   233   47  18%      2  157   44   12  357%
c i   77.3   56818   387980     33665   20667   1341 181126   43   231   47  19%      2  153   45   13  356%
c i   77.4   56817   387980     33718   20713   1341 181128   43   231   47  19%      2  153   49   13  384%
c i   77.9   56816   387980     34111   21074   1350 181140   43   224   47  19%      2  145   42   13  326%
c i   78.0   56811   387980     34178   21135   1350 181144   43   224   48  19%      2  146   48   13  366%
c i   79.0   56810   387980     34905   21791   1375 181168   42   222   48  19%      4  142   38   13  284%
c i   79.1   56799   387980     35058   21936   1377 181169   43   222   48  20%      3  142   52   13  384%
c i   79.2   56798   387980     35146   22006   1378 181172   43   219   48  20%      3  138   47   13  351%
c i   80.0   56797   387980     35747   22531   1395 181209   44   222   48  20%      3  140   56   14  408%
c i   80.2   56796   387980     35851   22623   1400 181210   44   223   48  20%      3  141   59   14  426%
c i   80.9   56795   387980     36329   23052   1409 181229   46   225   48  20%      3  141   66   14  465%
c i   84.7   56794   387980     39075   25527   1491 181312   45   225   55  20%     27  136   39   15  252%
c i   84.8   56793   387980     39161   25602   1493 181316   45   226   55  20%     24  137   38   15  245%
c i   85.0   56792   387980     39304   25736   1496 181316   45   227   55  20%     21  138   46   15  298%
c i   85.3   56772   387980     39560   25963   1503 181323   45   225   55  20%     17  135   43   16  277%
c i   85.5   56771   387980     39696   26087   1506 181325   46   228   55  20%     14  138   55   16  351%
c i   86.2   56770   387980     40139   26490   1516 181340   48   237   57  20%     10  146   67   16  416%
c i   86.6   56769   387980     40372   26703   1523 181346   47   237   57  20%      8  146   46   16  288%
c i   87.3   56768   387980     40919   27208   1539 181360   46   235   57  20%      6  142   48   16  296%
c i   87.4   56767   387980     40952   27235   1540 181363   47   234   57  20%      5  141   49   16  302%
c i   87.5   56766   387980     41048   27327   1541 181364   46   232   57  20%      5  139   46   16  283%
c i   87.5   56765   387980     41053   27327   1542 181367   46   232   57  20%      5  139   45   16  278%
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   87.5   56666   387980     41054   27327   1542 181367   46   232   57  20%      5  139   45   16  276%
c i   87.5   56664   387980     41055   27327   1542 181367   46   232   57  20%      5  139   45   16  275%
c i   87.8   56663   387980     41290   27547   1545 181370   46   230   57  20%      4  136   49   16  299%
c 
c [simplification-11] limit 41311 conflicts (hard 51246) hit after 41311 conflicts
c [quatres-6] found 27418 quaternary clauses 44% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 3 quaternary resolvents
c [ternres-7] limit 14789922 with penalty 0 = 0 + 0
c [ternres-7] all 56663 free variables schedulable
c [ternres-7] 286 ternary resolvents (0 bin, 286 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 1789 variables
c [basicprobe-4] limit 73949611 penalty 0 = 0 + 0
c [basicprobe-4-0] 17534 probes remain 31% after last round
c [basicprobe-4-0] 327 units = 326 failed (100%) + 1 lifted (0%)
c [basicprobe-4-0] removed 694 variables, found 160572 hbrs
c [bate-2] eliminated 167 asymmetric tautologies during probing
c [unhide-11] limit 1478992 with penalty 1 = 0 + 1
c [unhide-11-11] 6 units, 89 failed, 10731 tauts, 0 hbrs, 103081 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 275 transitive binary clauses
c [transred-7] found 3 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 55588 variables 100%
c [block-4] limit of 36974805 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 39 blocked clauses
c [block-4] 39 < 1/100 * 365925 = 3659 considered unsuccessful
c [bca-7] limit of 10000000 steps and 729805 added (scaled 2)
c [bca-7] 77353 out of 111178 literals actually usable 70%
c [bca-7] added 20 blocked clauses in 209861 steps
c [sweep-7] limit 4436976 penalty 0 = 0 + 0
c [sweep-7-1] 3512 pos 7.3% + 44272 neg 92.7% = 47784 sched 86.0% ret 7804
c [sweep-7-1] 4612030 steps 39 queries 4964.69 avg class size
c [sweep-7-1] 678 decisions 36 SAT calls 197.08 avg env size
c [sweep-7-1] 47452 variables remain 85% (8120 retained 15%)
c [decomp-26] removed 46 variables
c [sweep-7-1] removed 46 vars (0 failed, 3 eqs, 9 impls)
c [sweep-7] 46 < 1/1000 * 55588 = 55 considered unsuccessful
c [sweep-7] removed 46 vars in TOTAL (1 rounds, 38 queries)
c [phase-count-11] 360814 negative 99.1% of 364251 except 3437 0.9%
c [phase-count-11] 285848 positive 78.5% of 364251 except 78403 21.5%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 55542 enqueued variables after 41311 conflicts
c [score-dist-11] active 0 (0%), one 43033 (77%), zero 12509 (23%)
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 1121 variables 2.0% (55542 remain 29%)
c [simplification-11] removed 23729 irredundant clauses 6.1% (364251 remain 36%)
c [simplification-11] maximum reduction of 6% = max (2%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 53311 (soft 43311 + delta 10000)
c [simplification-11] new conflict limit 43311 (hard 53311)
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   95.0   55541   364251     41312   27201   1854 333672   46   230   50  20%      4  136   49   16  297%
c i   95.3   55536   364251     41464   27331   1864 333677   46   231   65  20%      3  137   49   17  295%
c i   95.6   55530   364251     41680   27515   1872 333681   47   234   65  20%      2  139   55   17  328%
c i   95.7   55529   364251     41749   27578   1875 333682   48   233   65  20%      2  139   63   17  373%
c i   96.1   55511   364251     42026   27834   1879 333685   48   236   65  21%      2  140   58   17  344%
c i   96.1   55510   364251     42038   27841   1882 333686   48   235   65  21%      2  140   56   17  330%
c i   96.6   55486   364251     42367   28149   1889 333690   48   236   65  20%      1  140   45   17  263%
c i   96.9   55485   364251     42580   28351   1891 333692   48   233   65  21%      1  137   45   17  265%
c i   97.4   55484   364251     43019   28721   1914 333723   48   227   65  21%      1  130   44   17  255%
c 
c [simplification-12] limit 43311 conflicts (hard 53311) hit after 43312 conflicts
c [quatres-7] found 27842 quaternary clauses 45% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [ternres-8] limit 15462074 with penalty 0 = 0 + 0
c [ternres-8] all 55484 free variables schedulable
c [ternres-8] 17 ternary resolvents (0 bin, 17 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 71 variables
c [simpleprobe-5] all 55471 free variables schedulable
c [simpleprobe-5] limit 61848296 penalty 0 = 0 + 0
c [decomp-28] removed 753 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 753 variables, found 66347 hbrs, 363 units
c [unhide-12] limit 1546207 with penalty 1 = 0 + 1
c [unhide-12-12] 6 units, 434 failed, 49655 tauts, 0 hbrs, 123029 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 170 transitive binary clauses
c [transred-8] found 1 units
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 54564 variables 100%
c [elim-9] limit of 154620740 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1882 variables 3% in round 1 in 31566823 steps
c [elim-9-1] backward subsumption/strengthening limit 31566800
c [elim-9-1-1] backward checking 6746 touched variables 12%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 34 and strengthened 164 clauses in 2270168 steps
c [elim-9-1] rescheduled 427 variables 1% by backward subsumption
c [elim-9-2] eliminated 53 variables 0% in round 2 in 468377 steps
c [elim-9-2] backward subsumption/strengthening limit 468300
c [elim-9-2-1] backward checking 379 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 6 and strengthened 7 clauses in 224788 steps
c [elim-9-2] rescheduled 27 variables 0% by backward subsumption
c [elim-9-3] eliminated 1 variables 0% in round 3 in 28320 steps
c [elim-9-3] backward subsumption/strengthening limit 28300
c [elim-9-3-1] backward checking 12 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 2 clauses in 28301 steps
c [elim-9] incomplete 8 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1938 = 4% variables out of 54564 scheduled
c [bca-8] limit of 10000000 steps and 702769 added (scaled 2)
c [bca-8] 75549 out of 105254 literals actually usable 72%
c [bca-8] added 44 blocked clauses in 200327 steps
c [sort-queue-12] sorted 52626 enqueued variables after 43312 conflicts
c [score-dist-12] active 0 (0%), one 41036 (78%), zero 11590 (22%)
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 2858 variables 5.2% (52626 remain 28%)
c [simplification-12] removed 13300 irredundant clauses 3.7% (350951 remain 35%)
c [simplification-12] maximum reduction of 5% = max (5%, 4%)
c [simplification-12] large reduction 5% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 55312 (soft 45312 + delta 10000)
c [simplification-12] new conflict limit 45312 (hard 55312)
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  102.9   52625   350951     43549   19278   1756 302130   49   230   48  21%      2  132   53   18  297%
c i  103.0   52416   350951     43593   19320   1756 302131   49   230   48  21%      2  132   51   18  287%
c i  103.0   52415   350951     43611   19336   1756 302132   49   230   48  21%      2  131   49   18  277%
c i  103.3   52409   350951     43860   19576   1759 302135   47   226   48  21%      1  128   36   18  204%
c i  103.8   52408   350951     44209   19895   1764 302146   47   226   48  21%      1  127   42   18  234%
c i  103.9   52407   350951     44347   20020   1769 302149   46   225   48  21%      1  125   39   18  216%
c i  104.3   52406   350951     44671   20314   1781 302156   46   223   48  20%      1  123   37   18  205%
c 
c [simplification-13] limit 45312 conflicts (hard 55312) hit after 45313 conflicts
c [ternres-9] limit 16133326 with penalty 0 = 0 + 0
c [ternres-9] all 52406 free variables schedulable
c [ternres-9] 544 ternary resolvents (0 bin, 544 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-29] removed 224 variables
c [unhide-13] limit 3226665 with penalty 0 = 0 + 0
c [unhide-13-14] 5 units, 149 failed, 18204 tauts, 0 hbrs, 60204 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 184 transitive binary clauses
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 52158 variables 100%
c [elim-10] limit of 322666535 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 297 variables 1% in round 1 in 29948889 steps
c [elim-10-1] backward subsumption/strengthening limit 29948800
c [elim-10-1-1] backward checking 1869 touched variables 4%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 6 and strengthened 4 clauses in 730604 steps
c [elim-10-1] rescheduled 27 variables 0% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 19473 steps
c [elim-10-2] backward subsumption/strengthening limit 19400
c [elim-10-2-1] backward checking 10 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 2 clauses in 19401 steps
c [elim-10-2] rescheduled 8 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 11827 steps
c [elim-10-3] backward subsumption/strengthening limit 11800
c [elim-10-3-1] backward checking 10 touched variables 0%
c [elim-10-3-1] incomplete backward checking 6 remain 60%
c [elim-10-3] subsumed 0 and strengthened 2 clauses in 11826 steps
c [elim-10] incomplete 8 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 303 = 1% variables out of 52158 scheduled
c [elim-10] 303 < 1/100 * 52158 = 521 considered unsuccessful
c [bca-9] limit of 10000000 steps and 683473 added (scaled 2)
c [bca-9] 73359 out of 103712 literals actually usable 71%
c [bca-9] added 17 blocked clauses in 194067 steps
c [sweep-8] limit 2419999 penalty 1 = 1 + 0
c [sweep-8-1] 3670 pos 8.2% + 40927 neg 91.8% = 44597 sched 86.0% ret 7258
c [sweep-8-1] 2643484 steps 35 queries 4879.80 avg class size
c [sweep-8-1] 982 decisions 30 SAT calls 298.50 avg env size
c [sweep-8-1] 44330 variables remain 85% (7521 retained 15%)
c [decomp-30] removed 8 variables
c [sweep-8-1] removed 8 vars (0 failed, 5 eqs, 8 impls)
c [sweep-8] 8 < 1/1000 * 51855 = 51 considered unsuccessful
c [sweep-8] removed 8 vars in TOTAL (1 rounds, 34 queries)
c [sort-queue-13] sorted 51847 enqueued variables after 45313 conflicts
c [score-dist-13] active 0 (0%), one 40562 (78%), zero 11285 (22%)
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 559 variables 1.1% (51847 remain 27%)
c [simplification-13] removed 9703 irredundant clauses 2.8% (341248 remain 34%)
c [simplification-13] maximum reduction of 3% = max (1%, 3%)
c [simplification-13] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-13] new conflict interval 22332
c [simplification-13] penalized conflict interval 22332 = 1 * 22332
c [simplification-13] hard conflict limit 78811 (soft 67645 + delta 11166)
c [simplification-13] new conflict limit 67645 (hard 78811)
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  108.8   51846   341248     45436   20767   2256 271234   44   219   49  20%      3  117   38   18  208%
c i  108.8   51845   341248     45454   20784   2256 271234   44   219   49  20%      3  117   36   18  197%
c i  108.9   51844   341248     45549   20863   2259 271239   44   218   49  20%      2  116   44   18  241%
c i  109.0   51843   341248     45624   20937   2259 271239   44   217   49  20%      2  114   38   18  208%
c i  109.7   51837   341248     46027   21316   2270 271247   45   218   49  21%      2  115   45   18  243%
c i  110.1   51836   341248     46455   21710   2281 271259   44   212   49  21%      2  108   37   19  200%
c i  110.9   51835   341248     47082   22291   2293 271275   43   214   49  20%      2  109   44   19  236%
c i  113.3   51832   341248     48947   24019   2345 271317   41   204   49  20%     14   97   47   19  243%
c i  113.9   51831   341248     49427   24472   2352 271326   42   207   49  20%     10   99   42   19  218%
c i  114.0   51830   341248     49480   24521   2352 271326   41   209   49  20%      9  100   42   20  214%
c i  114.7   51829   341248     50001   25000   2363 271333   44   212   49  21%      6  103   67   20  336%
c i  115.1   51828   341248     50458   25430   2371 271340   43   212   49  20%      4  102   37   20  185%
c i  115.4   51827   341248     50773   25705   2374 271346   44   214   50  21%      3  104   63   20  311%
c i  117.1   51826   341248     52366   27121   2410 271386   47   221   50  21%     11  108   46   21  220%
c i  117.4   51825   341248     52645   27385   2416 271387   46   223   50  21%      8  110   38   21  181%
c i  117.8   51824   341248     53010   27721   2421 271397   45   226   50  20%      6  112   43   21  203%
c i  118.4   51823   341248     53521   28196   2425 271403   45   220   50  21%      4  105   52   21  243%
c i  118.9   51822   341248     54009   28620   2439 271418   47   227   51  21%      3  112   51   22  235%
c i  119.0   51821   341248     54102   28694   2444 271423   47   225   52  21%      3  109   48   22  224%
c i  119.6   51820   341248     54665   29191   2461 271434   47   217   54  22%      2  100   41   22  189%
c i  120.3   51819   341248     55220   29697   2468 271447   45   209   56  22%      2   92   38   22  175%
c i  120.7   51818   341248     55599   30048   2472 271453   47   216   57  22%      2   98   57   22  260%
c i  121.0   51817   341248     55864   30292   2479 271457   47   219   57  22%      1  101   57   22  256%
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  121.0   51811   341248     55865   30292   2479 271457   47   219   57  22%      1  100   57   22  255%
c i  121.0   51810   341248     55866   30292   2479 271457   47   219   57  22%      1  100   56   22  254%
c i  121.0   51809   341248     55867   30292   2479 271457   47   219   57  22%      1  100   56   22  253%
c i  121.0   51808   341248     55878   30302   2479 271457   47   219   58  22%      1  100   57   22  254%
c i  121.6   51807   341248     56440   30806   2482 271462   48   217   58  22%      1   98   49   23  216%
c i  121.8   51623   341248     56519   30864   2487 271476   48   215   58  22%      1   96   41   23  184%
c i  122.1   51365   341248     56719   31046   2488 271479   49   219   61  22%      1   99   58   23  256%
c i  122.3   51364   341248     56935   31251   2491 271483   48   219   61  22%      0   99   51   23  226%
c i  123.0   51363   341248     57514   31793   2499 271486   50   228   61  22%      1  107   64   23  279%
c i  123.4   51362   341248     57763   32021   2504 271488   52   229   61  23%      1  108   80   23  341%
c i  123.7   51361   341248     58130   32358   2514 271497   52   229   61  22%      1  107   58   23  248%
c i  124.3   51360   341248     58596   32784   2517 271504   52   223   63  23%      1  101   48   24  203%
c i  124.4   51359   341248     58667   32843   2519 271506   52   222   63  23%      1   99   46   24  195%
c i  125.0   51358   341248     59186   33299   2527 271510   54   223   64  24%      1   99   77   24  319%
c i  125.2   51357   341248     59316   33414   2530 271513   54   223   64  24%      1  100   69   24  288%
c i  126.2   51356   341248     60085   34093   2539 271515   56   226   64  25%      2  101   51   25  207%
c i  127.0   51355   341248     60781   34705   2550 271521   60   228   64  26%      3  102   67   25  268%
c i  127.1   51354   341248     60799   34715   2550 271521   60   228   64  26%      3  102   72   25  284%
c i  127.9   51333   341248     61448   35313   2555 271531   60   224   64  27%      3   97   57   26  223%
c i  130.1   51332   341248     63291   36978   2584 271560   60   227   64  26%     13   98   55   26  206%
c i  130.7   51329   341248     63875   37507   2591 271566   59   228   65  26%      8   97   47   27  176%
c i  131.0   51328   341248     64081   37692   2592 271568   59   228   65  26%      7   97   51   27  189%
c i  131.0   51327   341248     64151   37758   2592 271569   61   230   65  26%      6   99   76   27  281%
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  131.2   51326   341248     64226   37827   2594 271571   61   229   65  27%      5   98   73   27  269%
c i  131.8   51325   341248     64722   38266   2604 271577   63   231   65  27%      4   99   88   27  321%
c i  132.4   51324   341248     65207   38717   2609 271583   61   227   65  27%      3   94   55   28  201%
c i  132.5   51323   341248     65284   38782   2612 271589   60   224   65  27%      2   92   50   28  181%
c i  133.9   51322   341248     66298   39715   2624 271599   64   238   68  27%      5  104   81   28  286%
c i  134.1   51321   341248     66416   39815   2626 271601   64   236   68  27%      4  102   78   28  274%
c i  134.5   51320   341248     66673   40035   2631 271606   64   234   68  27%      3  100   66   28  232%
c i  135.5   51319   341248     67410   40707   2642 271618   67   237   70  28%      3  101   85   29  293%
c i  135.6   51318   341248     67448   40743   2642 271619   67   239   70  28%      3  103   87   29  301%
c 
c [simplification-14] limit 67675 conflicts (hard 78811) hit after 67675 conflicts
c [quatres-8] found 26326 quaternary clauses 44% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 3 quaternary resolvents
c [ternres-10] limit 22653615 with penalty 0 = 0 + 0
c [ternres-10] all 51318 free variables schedulable
c [ternres-10] 106 ternary resolvents (0 bin, 106 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 566340 penalty 3 = 3 + 0
c [gauss-4] extracted 21 xors of average arity 3.0
c [gauss-4] connected 62 occurrences of 62 variables (average 1.0)
c [gauss-4] limit 566340 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 4 variables
c [treelook-5] limit 1132680 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 83369 literals 81%
c [treelook-5] scheduling used 1132684 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1132680 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 1170402 steps
c [treelook-5] 83334 literals remain 81%
c [treelook-5] 20611 variables remain to probed next time 40%
c [decomp-32] removed 1 variables
c [treelook-5] removed 9 variables, found 5152 hbrs
c [unhide-14] limit 2265361 with penalty 1 = 0 + 1
c [unhide-14-15] 4 units, 111 failed, 7426 tauts, 0 hbrs, 185626 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 237 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 141585096 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 349 (0%) of length 8
c [cce-4-1] eliminated 6 clauses out of 518 (1%) of length 7
c [cce-4-1] eliminated 1370 clauses out of 3338 (41%) of length 6
c [cce-4-1] eliminated 10027 clauses out of 23223 (43%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 11404 large clauses in 141585097 steps
c [cce-4-1] allowing another 70792548 steps for small clauses
c [cce-4-1] scheduling 261584 clauses = 178537 binary + 83047 ternary
c [cce-4-1] tried to eliminate 3078 small clauses 1%
c [cce-4-1] eliminated 545 binary clauses 0%
c [cce-4-1] eliminated 159 ternary clauses 0%
c [cce-4-1] eliminated 704 small clauses 0%
c [cce-4-1] eliminated 1129 small clauses in 141585096 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 12533 covered clauses in round 1
c [cce-4] eliminated 12533 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 644164 added (scaled 2)
c [bca-10] 65999 out of 102494 literals actually usable 64%
c [bca-10] added 19 blocked clauses in 188447 steps
c [sort-queue-14] sorted 51246 enqueued variables after 67675 conflicts
c [score-dist-14] active 0 (0%), one 41254 (81%), zero 9992 (19%)
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 72 variables 0.1% (51246 remain 27%)
c [simplification-14] removed 19615 irredundant clauses 5.7% (321633 remain 32%)
c [simplification-14] maximum reduction of 6% = max (0%, 6%)
c [simplification-14] large reduction 6% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 79675 (soft 69675 + delta 10000)
c [simplification-14] new conflict limit 69675 (hard 79675)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  143.9   51245   321633     68201   41272   2852 264502   64   235   83  27%      3   98   56   29  192%
c i  144.5   51244   321633     68652   41682   2859 264506   64   236   83  27%      2   98   64   30  218%
c i  144.7   51243   321633     68744   41765   2860 264509   63   234   83  27%      2   96   56   30  191%
c i  144.7   51242   321633     68768   41788   2860 264509   63   233   83  27%      2   95   54   30  182%
c i  145.5   51241   321633     69389   42363   2869 264517   62   231   83  27%      2   93   60   30  201%
c i  145.9   51240   321633     69668   42608   2871 264517   63   230   83  27%      1   91   65   30  216%
c 
c [simplification-15] limit 69675 conflicts (hard 79675) hit after 69676 conflicts
c [quatres-9] found 26296 quaternary clauses 53% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [ternres-11] limit 23219298 with penalty 0 = 0 + 0
c [ternres-11] all 51240 free variables schedulable
c [ternres-11] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 725603 penalty 4 = 4 + 0
c [card-5] found 1619 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 725603 for elimination
c [card-5] 1619 out of 1619 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-33] removed 6 variables
c [basicprobe-5] limit 116096493 penalty 0 = 0 + 0
c [basicprobe-5-0] 13741 probes remain 27% after last round
c [basicprobe-5-0] 558 units = 552 failed (99%) + 6 lifted (1%)
c [basicprobe-5-0] removed 1005 variables, found 240161 hbrs
c [bate-3] eliminated 291 asymmetric tautologies during probing
c [unhide-15] limit 2321929 with penalty 1 = 0 + 1
c [unhide-15-16] 1 units, 10 failed, 5773 tauts, 0 hbrs, 129188 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 207 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 50156 variables 100%
c [block-5] limit of 29024123 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 335 blocked clauses
c [block-5] 335 < 1/100 * 309119 = 3091 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 50154 variables 100%
c [elim-11] limit of 232192987 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 6528 variables 13% in round 1 in 25672290 steps
c [elim-11-1] backward subsumption/strengthening limit 25672200
c [elim-11-1-1] backward checking 17844 touched variables 36%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 9 and strengthened 22 clauses in 3347304 steps
c [elim-11-1] rescheduled 65 variables 0% by backward subsumption
c [elim-11-2] eliminated 5 variables 0% in round 2 in 636300 steps
c [elim-11-2] backward subsumption/strengthening limit 636300
c [elim-11-2-1] backward checking 43 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 282998 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 6533 = 13% variables out of 50154 scheduled
c [bca-11] limit of 10000000 steps and 585403 added (scaled 2)
c [bca-11] 69258 out of 87244 literals actually usable 79%
c [bca-11] added 117 blocked clauses in 179680 steps
c [sort-queue-15] sorted 43621 enqueued variables after 69676 conflicts
c [score-dist-15] active 0 (0%), one 34974 (80%), zero 8647 (20%)
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 7619 variables 14.9% (43621 remain 23%)
c [simplification-15] removed 29385 irredundant clauses 9.1% (292248 remain 29%)
c [simplification-15] maximum reduction of 15% = max (15%, 9%)
c [simplification-15] large reduction 15% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 81676 (soft 71676 + delta 10000)
c [simplification-15] new conflict limit 71676 (hard 81676)
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  156.8   43620   292248     70772    9308   2748 463033   52   205   37  25%      5   64   20   30   66%
c i  156.8   43619   292248     70778    9311   2749 463034   52   204   37  25%      5   64   19   30   64%
c i  157.1   43618   292248     71295    9796   2764 463043   47   195   38  24%      3   54   13   30   44%
c 
c [simplification-16] limit 71677 conflicts (hard 81676) hit after 71678 conflicts
c [ternres-12] limit 23555094 with penalty 0 = 0 + 0
c [ternres-12] all 43618 free variables schedulable
c [ternres-12] 396 ternary resolvents (0 bin, 396 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-34] removed 59 variables
c [simpleprobe-6] all 43562 free variables schedulable
c [simpleprobe-6] limit 94220378 penalty 0 = 0 + 0
c [decomp-35] removed 269 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 269 variables, found 76644 hbrs, 171 units
c [unhide-16] limit 4711018 with penalty 0 = 0 + 0
c [unhide-16-18] 8 units, 63 failed, 57511 tauts, 0 hbrs, 27541 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 170 transitive binary clauses
c [transred-12] found 3 units
c [cce-5] limit of 29443868 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 8 clauses out of 227 (4%) of length 7
c [cce-5-1] eliminated 122 clauses out of 2576 (5%) of length 6
c [cce-5-1] eliminated 1 clauses out of 12742 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 131 large clauses in 29443870 steps
c [cce-5-1] allowing another 14721935 steps for small clauses
c [cce-5-1] scheduling 168411 clauses = 150144 binary + 18267 ternary
c [cce-5-1] tried to eliminate 837 small clauses 0%
c [cce-5-1] eliminated 179 binary clauses 0%
c [cce-5-1] eliminated 46 ternary clauses 0%
c [cce-5-1] eliminated 225 small clauses 0%
c [cce-5-1] eliminated 467 small clauses in 29443873 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 598 covered clauses in round 1
c [cce-5] eliminated 598 covered clauses in TOTAL during 1 rounds
c [cce-5] 598 < 1/100 * 286977 = 2869 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 43153 variables 100%
c [elim-12] limit of 471101892 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 343 variables 1% in round 1 in 23527758 steps
c [elim-12-1] backward subsumption/strengthening limit 23527700
c [elim-12-1-1] backward checking 1995 touched variables 5%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 29 and strengthened 12 clauses in 685816 steps
c [elim-12-1] rescheduled 76 variables 0% by backward subsumption
c [elim-12-2] eliminated 10 variables 0% in round 2 in 106535 steps
c [elim-12-2] backward subsumption/strengthening limit 106500
c [elim-12-2-1] backward checking 68 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 2 clauses in 90267 steps
c [elim-12-2] rescheduled 8 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 12720 steps
c [elim-12-3] backward subsumption/strengthening limit 12700
c [elim-12-3-1] backward checking 10 touched variables 0%
c [elim-12-3-1] incomplete backward checking 6 remain 60%
c [elim-12-3] subsumed 0 and strengthened 2 clauses in 12781 steps
c [elim-12] incomplete 8 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 356 = 1% variables out of 43153 scheduled
c [elim-12] 356 < 1/100 * 43153 = 431 considered unsuccessful
c [bca-12] limit of 10000000 steps and 571004 added (scaled 2)
c [bca-12] 66017 out of 85596 literals actually usable 77%
c [bca-12] added 124 blocked clauses in 166971 steps
c [sweep-9] limit 1766632 penalty 2 = 2 + 0
c [sweep-9-1] 3717 pos 10.0% + 33620 neg 90.0% = 37337 sched 87.2% ret 5460
c [sweep-9-1] 1848197 steps 29 queries 4723.24 avg class size
c [sweep-9-1] 592 decisions 27 SAT calls 168.52 avg env size
c [sweep-9-1] 37083 variables remain 87% (5714 retained 13%)
c [decomp-36] removed 4 variables
c [sweep-9-1] removed 4 vars (0 failed, 1 eqs, 3 impls)
c [sweep-9] 4 < 1/1000 * 42797 = 42 considered unsuccessful
c [sweep-9] removed 4 vars in TOTAL (1 rounds, 28 queries)
c [sort-queue-16] sorted 42793 enqueued variables after 71678 conflicts
c [score-dist-16] active 0 (0%), one 34569 (81%), zero 8224 (19%)
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 825 variables 1.9% (42793 remain 23%)
c [simplification-16] removed 7235 irredundant clauses 2.5% (285013 remain 28%)
c [simplification-16] maximum reduction of 2% = max (2%, 2%)
c [simplification-16] geometric conflict interval increment 7444 = 22332 / 3
c [simplification-16] new conflict interval 29776
c [simplification-16] penalized conflict interval 29776 = 1 * 29776
c [simplification-16] hard conflict limit 116342 (soft 101454 + delta 14888)
c [simplification-16] new conflict limit 101454 (hard 116342)
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  162.4   42792   285013     71933    9923   3011 472627   43   195   39  22%      3   54   17   30   56%
c i  162.5   42791   285013     72184   10144   3023 472638   41   188   39  22%      2   47   13   29   43%
c i  163.2   42790   285013     73803   11636   3045 472663   37   186   39  20%     10   43   27   29   92%
c i  163.3   42789   285013     74169   11965   3051 472669   36   186   40  19%      7   43   36   29  124%
c i  163.3   42726   285013     74177   11971   3052 472669   36   186   40  19%      7   43   40   29  135%
c i  164.3   42725   285013     75769   13438   3072 472693   31   158   41  20%     11   14   17   29   58%
c i  165.7   42722   285013     77869   15359   3107 472726   31   160   44  19%     17   15   33   29  113%
c i  167.0   42721   285013     80397   17708   3151 472759   28   144   48  20%     22   -1   31   29  108%
c i  167.3   42720   285013     80866   18151   3159 472765   28   141   48  20%     14   -4   26   29   90%
c i  167.4   42719   285013     80989   18258   3166 472768   27   139   48  20%     12   -6   21   29   73%
c i  167.4   42701   285013     80990   18258   3166 472768   27   139   48  20%     12   -6   21   29   73%
c i  167.5   42683   285013     81079   18339   3168 472772   27   138   48  20%     10   -7   21   29   73%
c i  167.5   42682   285013     81207   18462   3171 472772   28   140   49  20%      9   -5   30   29  103%
c i  167.6   42681   285013     81219   18471   3171 472773   28   139   49  20%      9   -5   29   29  100%
c i  167.6   42680   285013     81312   18557   3171 472774   28   139   49  20%      7   -5   27   29   93%
c i  168.0   42679   285013     81870   19092   3174 472776   28   141   50  20%      4   -4   28   29   98%
c i  168.1   42678   285013     81947   19164   3176 472777   29   143   50  20%      4   -1   41   29  140%
c i  168.1   42674   285013     82030   19244   3177 472777   29   144   50  20%      3   -0   42   29  146%
c i  168.4   42673   285013     82424   19616   3183 472781   29   151   50  19%      2    7   30   29  105%
c i  168.9   42672   285013     83382   20484   3218 472799   27   144   51  19%      3   -0   21   29   72%
c i  171.7   42667   285013     87384   24226   3264 472840   28   134   60  21%     41  -11   36   29  123%
c i  172.8   42666   285013     88698   25460   3281 472856   31   147   60  21%     16    2   38   29  129%
c i  173.1   42664   285013     89174   25905   3288 472860   32   155   60  20%      9   10   48   29  163%
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  173.8   42652   285013     90028   26695   3302 472870   32   157   62  20%      5   11   37   29  128%
c i  176.8   42573   285013     94240   30595   3338 472900   28   117   69  24%     43  -28   23   29   78%
c i  178.1   42572   285013     95862   32113   3352 472922   28   105   72  27%     15  -39   51   29  175%
c i  178.7   42571   285013     96706   32899   3365 472933   28   108   72  26%      6  -36   23   29   79%
c i  178.8   42570   285013     96936   33111   3369 472935   28   111   72  25%      4  -33   27   29   95%
c i  179.0   42569   285013     97174   33342   3371 472935   29   115   72  25%      2  -29   38   29  131%
c i  180.0   42568   285013     98229   34334   3385 472945   30   126   72  24%      2  -17   29   29  100%
c i  180.0   42567   285013     98284   34386   3386 472945   30   125   72  24%      1  -18   26   29   90%
c i  180.9   42566   285013     99276   35318   3397 472951   31   134   74  24%      1   -9   29   29   99%
c 
c [simplification-17] limit 101465 conflicts (hard 116342) hit after 101466 conflicts
c [quatres-10] found 28171 quaternary clauses 57% in total
c [quatres-10-2] added 6 single-self-subsuming ternary resolvents
c [quatres-10-2] added 3 quaternary resolvents
c [ternres-13] limit 28918890 with penalty 0 = 0 + 0
c [ternres-13] all 42566 free variables schedulable
c [ternres-13] 301 ternary resolvents (0 bin, 301 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-37] removed 238 variables
c [treelook-6] limit 2891889 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 71742 literals 84%
c [treelook-6] scheduling used 1486575 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2891889 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2962521 steps
c [treelook-6] 71699 literals remain 84%
c [treelook-6] 14459 variables remain to probed next time 34%
c [treelook-6] removed 6 variables, found 14751 hbrs
c [unhide-17] limit 2891889 with penalty 1 = 0 + 1
c [unhide-17-20] 7 units, 30 failed, 23168 tauts, 0 hbrs, 992763 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 149 transitive binary clauses
c [transred-13] found 2 units
c [bca-13] limit of 10000000 steps and 565020 added (scaled 2)
c [bca-13] 56230 out of 85008 literals actually usable 66%
c [bca-13] added 27 blocked clauses in 164240 steps
c [sort-queue-17] sorted 42503 enqueued variables after 101466 conflicts
c [score-dist-17] active 0 (0%), one 34726 (82%), zero 7777 (18%)
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 63 variables 0.1% (42503 remain 22%)
c [simplification-17] removed 3017 irredundant clauses 1.1% (281996 remain 28%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 14888 = 29776 / 2
c [simplification-17] new conflict interval 44664
c [simplification-17] penalized conflict interval 44664 = 1 * 44664
c [simplification-17] hard conflict limit 168462 (soft 146130 + delta 22332)
c [simplification-17] new conflict limit 146130 (hard 168462)
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  189.1   42502   281996    102788   38525   3634 463790   34   148   85  23%     31    5   28   30   93%
c i  189.2   42501   281996    102934   38661   3634 463792   34   150   85  23%     26    7   29   30   98%
c i  189.6   42500   281996    103446   39133   3635 463795   33   141   85  24%     14   -2   27   30   92%
c i  190.0   42499   281996    103873   39533   3639 463802   33   139   86  24%      7   -4   30   30  101%
c i  192.5   42498   281996    106332   41793   3672 463836   36   151   86  24%     16    8   31   30  103%
c i  194.1   42497   281996    108112   43456   3696 463854   36   151   86  24%     10    8   31   30  103%
c i  197.2   42484   281996    111296   46395   3730 463889   39   162   86  24%     25   19   54   31  177%
c i  197.2   42482   281996    111344   46439   3731 463889   40   163   86  24%     24   20   54   31  176%
c i  197.7   42481   281996    111781   46833   3737 463896   39   159   86  24%     13   16   37   31  122%
c i  198.2   42480   281996    112322   47336   3743 463901   39   158   86  24%      5   15   48   31  155%
c i  198.4   42479   281996    112650   47644   3744 463904   39   158   86  24%      2   14   39   31  128%
c i  200.2   42478   281996    114309   49191   3762 463923   41   163   86  25%      5   19   50   31  161%
c i  200.8   42477   281996    114801   49635   3767 463931   42   165   87  26%      1   20   52   31  165%
c i  202.9   42476   281996    117135   51826   3784 463957   39   148   87  26%     13    3   37   31  117%
c i  203.0   42475   281996    117236   51917   3785 463960   38   145   87  26%     11    0   29   31   92%
c i  205.1   42474   281996    119142   53696   3806 463977   40   148   89  27%      9    3   45   32  141%
c i  205.1   42473   281996    119148   53701   3806 463977   40   148   89  27%      9    3   44   32  139%
c i  209.3   42472   281996    123174   57449   3840 464018   44   161   96  27%     36   15   43   33  133%
c i  214.0   42464   281996    127109   61007   3873 464064   55   188   97  29%     34   40   55   34  161%
c -  214.6   42464   281996    127543   24994   3887 464068   55   190   43  29%     19   43   56   34  162%
c i  214.8   42463   281996    127640   25086   3887 464069   55   191   50  29%     17   44   59   34  170%
c i  217.3   42225   281996    130385   27635   3907 464088   53   193   53  28%     17   44   82   35  233%
c i  217.7   41791   281996    130735   27969   3909 464089   53   193   53  27%      9   43   59   35  169%
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  218.3   41790   281996    131336   28526   3914 464094   54   199   53  27%      1   49   77   35  218%
c i  218.5   41789   281996    131486   28645   3916 464097   55   197   53  28%     -0   47   72   35  203%
c i  219.0   41788   281996    132045   29165   3919 464101   56   203   55  27%     -4   52   71   36  198%
c i  219.3   41787   281996    132236   29344   3921 464101   56   203   55  28%     -5   52   67   36  188%
c i  220.0   41778   281996    132950   30001   3931 464110   57   199   55  29%     -6   48   45   36  125%
c i  220.2   41697   281996    133176   30215   3935 464112   57   198   55  29%     -7   47   48   36  132%
c i  220.5   41696   281996    133479   30497   3939 464114   56   196   55  29%     -8   44   47   36  130%
c i  221.3   41695   281996    134275   31225   3945 464120   53   182   58  29%     -7   29   36   36  100%
c i  221.4   41694   281996    134348   31291   3946 464121   53   185   58  29%     -7   32   46   36  127%
c i  221.5   41693   281996    134745   31640   3949 464124   51   174   58  29%     -8   21   26   36   71%
c i  224.7   41692   281996    138059   34783   3957 464131   40   121   69  33%     24  -31   35   36   96%
c i  225.0   41688   281996    138290   34987   3962 464134   43   129   69  33%     17  -23   71   36  196%
c i  227.5   41658   281996    140617   37147   3980 464154   44   141   72  32%     12  -11   38   37  104%
c i  227.5   41657   281996    140649   37175   3980 464155   45   143   72  31%     11   -9   46   37  127%
c i  227.8   41656   281996    140969   37471   3980 464157   47   146   72  32%      5   -5   62   37  170%
c i  228.2   41655   281996    141274   37751   3984 464158   48   150   72  32%      1   -1   58   37  157%
c i  228.8   41654   281996    141923   38334   3992 464160   49   152   76  32%     -3    1   56   37  151%
c i  230.4   41653   281996    143387   39678   3998 464178   52   167   76  31%     -0   15   71   38  190%
c i  231.0   41652   281996    144007   40265   4003 464182   50   163   76  31%     -4   11   35   38   94%
c i  231.1   41651   281996    144098   40339   4005 464185   50   164   76  31%     -4   12   40   38  106%
c i  231.4   41650   281996    144370   40581   4010 464186   50   163   76  31%     -6   11   49   38  130%
c 
c [simplification-18] limit 146131 conflicts (hard 168462) hit after 146131 conflicts
c [quatres-11] found 27381 quaternary clauses 54% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 1 single-self-subsuming ternary resolvents
c [quatres-11-2] added 2 quaternary resolvents
c [ternres-14] limit 39484981 with penalty 0 = 0 + 0
c [ternres-14] all 41558 free variables schedulable
c [ternres-14] 58 ternary resolvents (0 bin, 58 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-39] removed 1166 variables
c [basicprobe-6] limit 197424905 penalty 0 = 0 + 0
c [basicprobe-6-0] 5388 probes remain 13% after last round
c [basicprobe-6-0] 806 units = 799 failed (99%) + 7 lifted (1%)
c [basicprobe-6-0] removed 1283 variables, found 391714 hbrs
c [bate-4] eliminated 1113 asymmetric tautologies during probing
c [unhide-18] limit 1974249 with penalty 2 = 0 + 2
c [unhide-18-21] 3 units, 59 failed, 61480 tauts, 0 hbrs, 794409 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 133 transitive binary clauses
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 40016 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 883 variables 2% in round 1 in 20679453 steps
c [elim-13-1] backward subsumption/strengthening limit 20679400
c [elim-13-1-1] backward checking 4425 touched variables 11%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 11 and strengthened 36 clauses in 1259399 steps
c [elim-13-1] rescheduled 124 variables 0% by backward subsumption
c [elim-13-2] eliminated 14 variables 0% in round 2 in 387337 steps
c [elim-13-2] backward subsumption/strengthening limit 387300
c [elim-13-2-1] backward checking 124 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 6 and strengthened 6 clauses in 120986 steps
c [elim-13-2] rescheduled 25 variables 0% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 25165 steps
c [elim-13-3] backward subsumption/strengthening limit 25100
c [elim-13-3-1] backward checking 12 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 2 clauses in 25101 steps
c [elim-13] incomplete 8 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 898 = 2% variables out of 40016 scheduled
c [bca-14] limit of 10000000 steps and 518789 added (scaled 2)
c [bca-14] 52091 out of 78238 literals actually usable 67%
c [bca-14] added 16 blocked clauses in 146214 steps
c [sort-queue-18] sorted 39118 enqueued variables after 146131 conflicts
c [score-dist-18] active 0 (0%), one 32999 (84%), zero 6119 (16%)
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 2440 variables 5.9% (39118 remain 21%)
c [simplification-18] removed 23122 irredundant clauses 8.2% (258874 remain 26%)
c [simplification-18] maximum reduction of 8% = max (6%, 8%)
c [simplification-18] large reduction 8% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 158131 (soft 148131 + delta 10000)
c [simplification-18] new conflict limit 148131 (hard 158131)
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  248.2   39117   258874    146704   31072   4016 696586   51   165   59  31%     10   12   32   38   84%
c 
c [simplification-19] limit 148131 conflicts (hard 158131) hit after 148596 conflicts
c [quatres-12] found 26359 quaternary clauses 54% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 3 quaternary resolvents
c [ternres-15] limit 39914352 with penalty 0 = 0 + 0
c [ternres-15] all 39117 free variables schedulable
c [ternres-15] 591 ternary resolvents (0 bin, 591 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 498929 penalty 4 = 4 + 0
c [gauss-5] extracted 6 xors of average arity 2.8
c [gauss-5] connected 17 occurrences of 17 variables (average 1.0)
c [gauss-5] limit 498929 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-40] removed 34 variables
c [simpleprobe-7] all 39083 free variables schedulable
c [simpleprobe-7] limit 159657409 penalty 0 = 0 + 0
c [decomp-41] removed 161 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 161 variables, found 84845 hbrs, 103 units
c [unhide-19] limit 7982870 with penalty 0 = 0 + 0
c [unhide-19-25] 6 units, 22 failed, 60856 tauts, 0 hbrs, 249338 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 156 transitive binary clauses
c [transred-15] found 1 units
c [cce-6] limit of 24946470 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 33
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 13
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 11
c [cce-6-1] eliminated 1 clauses out of 8 (12%) of length 10
c [cce-6-1] eliminated 2 clauses out of 41 (5%) of length 9
c [cce-6-1] eliminated 1 clauses out of 75 (1%) of length 8
c [cce-6-1] eliminated 3 clauses out of 146 (2%) of length 7
c [cce-6-1] eliminated 6 clauses out of 2536 (0%) of length 6
c [cce-6-1] eliminated 207 clauses out of 10152 (2%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 254 large clauses in 24946471 steps
c [cce-6-1] allowing another 12473235 steps for small clauses
c [cce-6-1] scheduling 155956 clauses = 139240 binary + 16716 ternary
c [cce-6-1] tried to eliminate 861 small clauses 1%
c [cce-6-1] eliminated 169 binary clauses 0%
c [cce-6-1] eliminated 32 ternary clauses 0%
c [cce-6-1] eliminated 201 small clauses 0%
c [cce-6-1] eliminated 271 small clauses in 24946472 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 525 covered clauses in round 1
c [cce-6] eliminated 525 covered clauses in TOTAL during 1 rounds
c [cce-6] 525 < 1/100 * 253207 = 2532 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 38892 variables 100%
c [elim-14] limit of 798287048 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 433 variables 1% in round 1 in 19852920 steps
c [elim-14-1] backward subsumption/strengthening limit 19852900
c [elim-14-1-1] backward checking 2371 touched variables 6%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 11 and strengthened 4 clauses in 616362 steps
c [elim-14-1] rescheduled 42 variables 0% by backward subsumption
c [elim-14-2] eliminated 4 variables 0% in round 2 in 341056 steps
c [elim-14-2] backward subsumption/strengthening limit 341000
c [elim-14-2-1] backward checking 51 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 1 and strengthened 2 clauses in 108236 steps
c [elim-14-2] rescheduled 11 variables 0% by backward subsumption
c [elim-14-3] eliminated 1 variables 0% in round 3 in 18193 steps
c [elim-14-3] backward subsumption/strengthening limit 18100
c [elim-14-3-1] backward checking 12 touched variables 0%
c [elim-14-3-1] incomplete backward checking 11 remain 92%
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 18110 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 438 = 1% variables out of 38892 scheduled
c [bca-15] limit of 10000000 steps and 504299 added (scaled 2)
c [bca-15] 51744 out of 76910 literals actually usable 67%
c [bca-15] added 19 blocked clauses in 141181 steps
c [sort-queue-19] sorted 38454 enqueued variables after 148596 conflicts
c [score-dist-19] active 0 (0%), one 32593 (85%), zero 5861 (15%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 663 variables 1.7% (38454 remain 20%)
c [simplification-19] removed 7249 irredundant clauses 2.8% (251625 remain 25%)
c [simplification-19] maximum reduction of 3% = max (2%, 3%)
c [simplification-19] geometric conflict interval increment 11166 = 44664 / 4
c [simplification-19] new conflict interval 55830
c [simplification-19] penalized conflict interval 55830 = 1 * 55830
c [simplification-19] hard conflict limit 232341 (soft 204426 + delta 27915)
c [simplification-19] new conflict limit 204426 (hard 232341)
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  260.9   38453   251625    152114   29692   4268 704459   42   147   55  29%     54   -6   26   38   68%
c i  265.2   38452   251625    157313   34531   4305 704482   41   139   69  30%     49  -12   48   38  126%
c i  268.1   38451   251625    161041   38047   4325 704504   35   111   76  32%     27  -39   59   38  156%
c i  268.1   38450   251625    161081   38085   4326 704504   35   111   76  31%     25  -38   56   38  148%
c i  271.9   38449   251625    165942   42583   4372 704556   35   109   80  32%     41  -37   49   38  130%
c i  274.1   38448   251625    168197   44702   4389 704568   41   139   80  30%      8   -7   45   38  118%
c i  274.2   38447   251625    168277   44759   4393 704568   43   140   81  30%      6   -6   61   38  159%
c i  274.6   38446   251625    168779   45211   4396 704570   44   142   81  31%     -2   -3   60   38  157%
c i  276.1   38445   251625    170404   46695   4408 704581   44   140   89  32%     -3   -6   34   38   90%
c i  276.5   38444   251625    170838   47091   4416 704588   43   136   89  31%     -7   -9   33   38   87%
c i  279.1   38443   251625    173692   49656   4432 704599   48   151  101  31%     11    5   40   39  102%
c i  280.0   38442   251625    175049   50877   4441 704606   43   135  101  32%     -2  -11   25   39   63%
c i  294.0   38441   251625    188469   63402   4516 704660   43   132  121  32%    161  -10   39   39   99%
c -  295.5   38403   251625    189757   30470   4523 704666   50   146   48  34%     29    5   70   40  177%
c i  302.9   38402   251625    198177   38342   4559 704704   38   106   72  36%     96  -34   33   40   84%
c i  303.5   38401   251625    198898   39024   4560 704707   37   100   72  37%     30  -39   29   40   73%
c i  306.4   38400   251625    201817   41729   4581 704721   39    96   83  40%     -6  -41   70   39  178%
c i  309.1   38399   251625    204355   43988   4603 704729   50   135   84  37%    -12   -2   61   40  150%
c i  310.7   38398   251625    206139   45600   4610 704744   48   132   92  36%    -20   -5   24   41   59%
c i  312.0   38397   251625    207385   46747   4619 704753   49   133   94  37%    -25   -4   53   41  129%
c i  312.6   38343   251625    207942   47241   4623 704754   51   137   94  37%    -28    0   64   41  156%
c i  312.9   38342   251625    208224   47490   4625 704754   53   143   94  37%    -30    6   75   41  183%
c i  316.6   38341   251625    212251   51284   4648 704768   39   108   99  37%     10  -28   22   41   54%
c 
c [simplification-20] limit 204426 conflicts (hard 232341) hit after 215459 conflicts
c [quatres-13] found 26494 quaternary clauses 52% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 3 quaternary resolvents
c [ternres-16] limit 54520228 with penalty 0 = 0 + 0
c [ternres-16] all 38341 free variables schedulable
c [ternres-16] 319 ternary resolvents (0 bin, 319 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-42] removed 116 variables
c [treelook-7] limit 5452022 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 60800 literals 79%
c [treelook-7] scheduling used 1605700 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 5452022 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5524537 steps
c [treelook-7] 60725 literals remain 79%
c [treelook-7] 11864 variables remain to probed next time 31%
c [treelook-7] removed 13 variables, found 31191 hbrs
c [unhide-20] limit 2726011 with penalty 2 = 0 + 2
c [unhide-20-26] 0 units, 144 failed, 25410 tauts, 0 hbrs, 1437200 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 137 transitive binary clauses
c [transred-16] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 38245 variables 100%
c [block-6] limit of 34075142 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 21 blocked clauses
c [block-6] 21 < 1/100 * 250234 = 2502 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 38244 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 122 variables 0% in round 1 in 19701108 steps
c [elim-15-1] backward subsumption/strengthening limit 19701100
c [elim-15-1-1] backward checking 796 touched variables 2%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 4 and strengthened 4 clauses in 247120 steps
c [elim-15-1] rescheduled 21 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 17820 steps
c [elim-15-2] backward subsumption/strengthening limit 17800
c [elim-15-2-1] backward checking 12 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 17801 steps
c [elim-15-2] fully rescheduled 38121 variables 100%
c [elim-15-3] eliminated 13 variables 0% in round 3 in 19668377 steps
c [elim-15-3] backward subsumption/strengthening limit 19668300
c [elim-15-3-1] backward checking 112 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 1 and strengthened 2 clauses in 103591 steps
c [elim-15] incomplete 11 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 136 = 0% variables out of 38244 scheduled
c [elim-15] 136 < 1/100 * 38244 = 382 considered unsuccessful
c [bca-16] limit of 10000000 steps and 498913 added (scaled 2)
c [bca-16] 47178 out of 76218 literals actually usable 62%
c [bca-16] added 9 blocked clauses in 155721 steps
c [sweep-10] limit 2044508 penalty 3 = 3 + 0
c [sweep-10-1] 3263 pos 9.7% + 30339 neg 90.3% = 33602 sched 88.2% ret 4506
c [sweep-10-1] 2198875 steps 30 queries 5395.73 avg class size
c [sweep-10-1] 704 decisions 25 SAT calls 450.64 avg env size
c [sweep-10-1] 33377 variables remain 88% (4729 retained 12%)
c [decomp-44] removed 17 variables
c [sweep-10-1] removed 17 vars (0 failed, 4 eqs, 7 impls)
c [sweep-10] 17 < 1/1000 * 38108 = 38 considered unsuccessful
c [sweep-10] removed 17 vars in TOTAL (1 rounds, 29 queries)
c [sort-queue-20] sorted 38091 enqueued variables after 215459 conflicts
c [score-dist-20] active 0 (0%), one 32632 (86%), zero 5459 (14%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 250 variables 0.7% (38091 remain 20%)
c [simplification-20] removed 2740 irredundant clauses 1.1% (248885 remain 25%)
c [simplification-20] maximum reduction of 1% = max (1%, 1%)
c [simplification-20] geometric conflict interval increment 27915 = 55830 / 2
c [simplification-20] new conflict interval 83745
c [simplification-20] penalized conflict interval 83745 = 1 * 83745
c [simplification-20] hard conflict limit 341076 (soft 299204 + delta 41872)
c [simplification-20] new conflict limit 299204 (hard 341076)
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  329.2   38090   248885    216995   53279   4822 681626   56   159  106  35%     22   22   65   42  155%
c i  329.7   38089   248885    217374   53622   4823 681628   56   158  106  35%      4   22   54   42  127%
c i  334.8   38088   248885    221842   57715   4847 681642   49   137  106  36%     18   -0   35   43   82%
c i  336.2   38087   248885    223008   58803   4856 681646   44   119  106  37%    -12  -19   16   42   37%
c i  339.7   38085   248885    226042   61519   4874 681660   52   136  108  38%     -3   -1   58   43  135%
c -  347.1   38085   248885    232603   34115   4915 681691   47   113   49  41%     50  -25   24   44   54%
c i  349.0   38084   248885    234490   35840   4933 681702   56   140   59  40%     77    3   77   45  171%
c i  353.0   38083   248885    238626   39577   4972 681727   51   141   62  36%     12    3   38   45   83%
c i  354.0   38057   248885    239686   40537   4978 681732   52   152   66  34%    -15   14   52   45  115%
c i  358.7   38053   248885    244002   44437   4997 681752   60   156   71  38%     14   17   60   46  130%
c i  365.8   38052   248885    250814   50641   5032 681785   51   123   86  41%     51  -15   29   47   62%
c i  367.8   38051   248885    252652   52357   5038 681788   42   102   90  41%     -9  -36   30   46   65%
c i  368.3   38047   248885    253095   52749   5040 681788   46   112   92  41%    -18  -25   58   46  125%
c i  369.5   38046   248885    254272   53861   5044 681790   44   108   95  40%    -25  -29   49   46  106%
c i  374.6   38045   248885    259169   58441   5059 681800   42    99  112  43%     22  -35   44   46   95%
c i  376.1   38016   248885    260487   59608   5066 681806   50   116  112  43%    -13  -18   70   46  152%
c i  377.1   38015   248885    261202   60242   5069 681810   52   122  112  43%    -22  -12   62   46  134%
c i  377.1   38014   248885    261204   60242   5069 681811   52   121  112  43%    -22  -12   62   46  133%
c i  378.6   38013   248885    262455   61355   5090 681822   52   122  112  43%    -25  -11   29   47   63%
c i  379.4   38011   248885    263308   62161   5096 681826   47   109  112  43%    -27  -24   24   46   52%
c i  381.7   38010   248885    265391   64077   5103 681831   51   117  124  44%    -17  -15   57   47  122%
c i  383.4   38009   248885    266697   65219   5108 681838   58   137  124  42%    -22    5   73   47  156%
c -  389.7   38009   248885    271567   35647   5130 681855   59   137   50  43%     25    3   35   48   73%
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  392.2   38008   248885    273965   37775   5135 681865   54   122   62  44%     61  -11   41   48   85%
c i  392.2   38007   248885    274001   37810   5135 681865   53   121   62  44%     57  -12   36   48   75%
c i  393.5   38006   248885    275428   39090   5139 681868   51   128   63  40%     -4   -5   55   48  114%
c i  400.3   38005   248885    282063   45161   5181 681915   42    97   83  43%     50  -35   36   48   76%
c i  403.4   38004   248885    285228   47978   5193 681924   40    90   84  45%     -0  -40   41   48   86%
c i  403.4   38001   248885    285255   47995   5195 681926   40    90   84  44%     -1  -40   38   47   80%
c i  403.5   37630   248885    285301   48038   5195 681926   40    89   84  44%     -3  -41   33   47   69%
c i  404.2   37629   248885    285893   48540   5200 681931   46   103   84  45%    -16  -27   76   48  158%
c i  406.5   37627   248885    287830   50262   5214 681944   54   132   89  41%    -17    2   63   48  130%
c i  417.3   37622   248885    297792   59135   5259 681982   41    86  110  47%     98  -41   44   48   92%
c i  418.8   37621   248885    299054   60343   5265 681991   35    73  121  48%      7  -53   20   47   43%
c i  422.2   37620   248885    302087   63183   5281 682005   34    82  121  41%     -7  -43   39   47   82%
c i  428.2   37619   248885    307473   67977   5315 682042   51   116  121  44%     27   -7   84   48  176%
c i  430.3   37618   248885    309035   69346   5320 682046   60   135  123  44%    -15   12   77   48  160%
c i  430.9   37617   248885    309565   69828   5323 682047   60   134  123  44%    -23   11   72   48  149%
c i  431.4   37616   248885    309981   70199   5325 682050   61   138  123  44%    -28   15   77   49  159%
c -  434.3   37613   248885    312210   38482   5344 682062   51   111   51  46%    -18  -12   28   48   58%
c i  435.9   37612   248885    314150   40144   5372 682087   42    90   60  47%     10  -33   17   48   37%
c i  438.0   37604   248885    316098   41898   5386 682100   51   111   62  45%    -15  -10   69   48  144%
c i  438.9   37602   248885    317029   42717   5395 682108   48   108   65  44%    -25  -14   28   48   58%
c i  444.8   37595   248885    323075   48215   5435 682162   41    98   72  42%     39  -22   22   47   46%
c i  445.4   37593   248885    323633   48722   5435 682162   43   106   73  41%      8  -14   59   47  125%
c i  445.5   37590   248885    323722   48809   5435 682162   44   107   73  41%      4  -12   61   47  129%
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  449.5   37589   248885    327637   52557   5447 682180   32    73   83  44%      8  -45   22   46   49%
c i  453.4   37588   248885    331144   55799   5462 682189   39    95  117  41%      3  -21   56   46  123%
c i  456.4   37587   248885    333394   57730   5475 682193   55   126  121  43%    -12   10   96   47  206%
c 
c [simplification-21] limit 299209 conflicts (hard 341076) hit after 336681 conflicts
c [quatres-14] found 25567 quaternary clauses 50% in total
c [quatres-14-2] added 8 single-self-subsuming ternary resolvents
c [quatres-14-2] added 7 quaternary resolvents
c [ternres-17] limit 83141537 with penalty 0 = 0 + 0
c [ternres-17] all 37587 free variables schedulable
c [ternres-17] 198 ternary resolvents (0 bin, 198 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2598173 penalty 4 = 4 + 0
c [card-6] found 2248 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2598173 for elimination
c [card-6] 2248 out of 2248 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-45] removed 542 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 6066 sched 17%, 752 failed, 20 lifted, 323174 hbrs
c [decomp-46] removed 1449 variables
c [basicprobe-7-1] 4804 probes remain 14% after last round
c [basicprobe-7-1] 1068 units = 1047 failed (98%) + 21 lifted (2%)
c [basicprobe-7-1] removed 1971 variables, found 453205 hbrs
c [bate-5] eliminated 1372 asymmetric tautologies during probing
c [unhide-21] limit 4157076 with penalty 2 = 0 + 2
c [unhide-21-28] 0 units, 31 failed, 73303 tauts, 0 hbrs, 1689615 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 177 transitive binary clauses
c [bca-17] limit of 10000000 steps and 447645 added (scaled 2)
c [bca-17] 41999 out of 71102 literals actually usable 59%
c [bca-17] added 6 blocked clauses in 148398 steps
c [sort-queue-21] sorted 35550 enqueued variables after 336681 conflicts
c [score-dist-21] active 0 (0%), one 31787 (89%), zero 3763 (11%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 2037 variables 5.4% (35550 remain 19%)
c [simplification-21] removed 25594 irredundant clauses 10.3% (223291 remain 22%)
c [simplification-21] maximum reduction of 10% = max (5%, 10%)
c [simplification-21] large reduction 10% >= 5% limit
c [simplification-21] next conflict interval 3366 = min (336681/100, 83745)
c [simplification-21] penalized conflict interval 3366 = 1 * 3366
c [simplification-21] hard conflict limit 350047 (soft 340047 + delta 10000)
c [simplification-21] new conflict limit 340047 (hard 350047)
c 
c [simplification-22] limit 340047 conflicts (hard 350047) hit after 350049 conflicts
c [quatres-15] found 25027 quaternary clauses 48% in total
c [quatres-15-1] removed 12 duplicate quaternary clauses
c [quatres-15-2] added 3 single-self-subsuming ternary resolvents
c [quatres-15-2] added 2 quaternary resolvents
c [ternres-18] limit 86299286 with penalty 0 = 0 + 0
c [ternres-18] all 35550 free variables schedulable
c [ternres-18] 177 ternary resolvents (0 bin, 177 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-47] removed 7 variables
c [simpleprobe-8] all 35543 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-48] removed 73 variables
c [simpleprobe-8] 86 variables remain 0% (35384 retained 100%)
c [simpleprobe-8] removed 73 variables, found 93175 hbrs, 30 units
c [unhide-22] limit 4314964 with penalty 2 = 0 + 2
c [unhide-22-29] 1 units, 7 failed, 63560 tauts, 0 hbrs, 879469 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 124 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 35458 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 985 variables 3% in round 1 in 17070476 steps
c [elim-16-1] backward subsumption/strengthening limit 17070400
c [elim-16-1-1] backward checking 4877 touched variables 14%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 14 and strengthened 17 clauses in 1081348 steps
c [elim-16-1] rescheduled 85 variables 0% by backward subsumption
c [elim-16-2] eliminated 8 variables 0% in round 2 in 63720 steps
c [elim-16-2] backward subsumption/strengthening limit 63700
c [elim-16-2-1] backward checking 75 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 12 and strengthened 2 clauses in 63701 steps
c [elim-16-2] rescheduled 21 variables 0% by backward subsumption
c [elim-16-3] eliminated 4 variables 0% in round 3 in 38224 steps
c [elim-16-3] backward subsumption/strengthening limit 38200
c [elim-16-3-1] backward checking 39 touched variables 0%
c [elim-16-3-1] incomplete backward checking 7 remain 18%
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 38250 steps
c [elim-16] incomplete 8 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 997 = 3% variables out of 35458 scheduled
c [bca-18] limit of 10000000 steps and 441592 added (scaled 2)
c [bca-18] 41816 out of 68924 literals actually usable 61%
c [bca-18] added 10 blocked clauses in 137733 steps
c [sort-queue-22] sorted 34461 enqueued variables after 350049 conflicts
c [score-dist-22] active 0 (0%), one 30991 (90%), zero 3470 (10%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 1089 variables 3.1% (34461 remain 18%)
c [simplification-22] removed 3028 irredundant clauses 1.4% (220263 remain 22%)
c [simplification-22] maximum reduction of 3% = max (3%, 1%)
c [simplification-22] geometric conflict interval increment 20936 = 83745 / 4
c [simplification-22] new conflict interval 104681
c [simplification-22] penalized conflict interval 104681 = 1 * 104681
c [simplification-22] hard conflict limit 507070 (soft 454730 + delta 52340)
c [simplification-22] new conflict limit 454730 (hard 507070)
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  509.9   34460   220263    351276   47539   5209 862708   48   104   69  46%    203   -6   38   46   83%
c i  528.9   34459   220263    370668   64915   5286 862761   41    91   90  45%    202  -14   32   44   71%
c i  533.5   34452   220263    375208   68846   5316 862774   35    68   90  52%    -26  -35   42   44   96%
c -  538.3   34410   220263    379889   39588   5333 862783   31    61   52  51%    -24  -39   27   43   62%
c i  541.7   34409   220263    383703   43028   5361 862801   28    56   60  49%     35  -42   13   42   30%
c 1  546.2   34385   220263    388832   47686   5381 862812   33    73   67  45%    -14  -23   27   41   66%
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 SATISFIABLE
c
c bate: 3032 basic ate = 1823 trn 60% + 1209 lrg 40% in 5 updates
c bcas: 18 count, 1143 added (375 skipped), 3777244 steps
c bkwd: tried 332976 clauses, 665712 lits, 2.00 lits/clause
c bkwd: checked 10180505 occs, 30.57 occs/clause, 15.29 occs/lit
c bkwd: subsumed 17 binary, 128 ternary, 24 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 438 large (0% self)
c blkd: 6 bces, 10716 removed, 7695542 resolutions, 21299313 steps
c blkd: 11962 blocking literals 3%, 4 pure
c bump: 388202 bumped seen, 226800853 lits 584.2 on average
c card: 6 count, 0 units, 0 am1, 332288238 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 69245 subsumed
c card: 17313 at-most-one constraints found, average size 4.71
c card: 17313 at-most-one constraints used 100%, average size 4.71
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 6 cces, 13988 eliminated, 13924 ate 100%, 64 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3450190 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 151 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 48 decompositions, 8399 equivalent 4%
c deco: 20872 decision-only clauses 5%, 68% reduction
c decs: 4964319 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 75852 eliminated 38%, 8 pure 0%
c elms: 45 rounds, 2.8 rounds/bve
c elms: 61500 small 81%, 14340 large 19%
c elms: 169968 tried small, 61500 succeeded 36%, 108468 failed 64%
c elms: 36457 subsumed, 49761 strengthened, 563 blocked
c elms: 17881918 copies, 17641125 resolutions, 4665574 ipos
c elms: 4182699 subchks, 2632735 strchks
c gaus: 5 extractions, 126 extracted, 2.7 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9131416 steps, 4565708 extr 50%, 571 elim 0%
c glue: 43.1 orig avg, 43.1 real avg, 4.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1899654 = 403973 simple 21% + 1474940 trn 78% + 20741 lrg 1%, 4748 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 388202 clauses, 290.7 length
c lrnd: 112868437 lits = 152465887 orig - 39597450 removed 26%
c lrnd: 171666 uips 44%, 181415 flips 47%
c mins: 352838 mins 92%, 3369 bin 1%, 6280 size 2%
c mins: 263968036 poisoned searches, 61006508 hits, 23% hit rate
c mins: 306586307 used twice searches, 7672848 hits, 3% hit rate
c move: moved 20074, 11350 bin 57%, 8724 trn 43%
c otfs: 877 driving 23%, 2915 restarting 77%
c otfs: str 3792, 3743 red 99%, 49 irr 1%
c otfs: str 3792, 0 bin 0%, 81 trn 2%, 3711 lrg 98%
c otfs: sub 11, 11 red 100%, 0 irr 0%
c otfs: sub 11, 0 bin 0%, 2 trn 18%, 9 lrg 82%
c phas: 11 computed, 97042 set, 0 pos (0%), 97042 neg (100%)
c prbs: 7 basic, 44357 probed, 2929 failed, 35 lifted
c prbs: 8 simple, 1028729 probed, 1377 failed, 870 eqs
c prbs: 7 treelook, 164 probed, 27 failed, 0 lifted
c prom: 69971 locked 7% out of 1042719 tried
c prps: 1321072383 props, 252 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 15 count, 35 quat, 19 self1, 1 self2, 1458 dup
c queu: 22 sorted, 4964319 next (6 steps 0.00)
c queu: 228249084 enq (228249039 steps 1.00), 226800853 deq 99%
c redc: 7067 clauses 25%, 28239 tried 7%, 211 sat 1%
c redc: 16514 lits 5%, 306983 tried 0%, 211 sat 0%
c redc: 911 times jump level reduced, 25.4 levels on average
c reds: 6 count, 64805.3 conflicts per reduce
c reds: 0 memlim 0%, 6 arith 100%
c reds: 157520 collected 77%, 47525 retired 23%
c rmbd: 46536 removed, 10152 red 22%
c rsts: 11865 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: 22 count, 20 confs 91%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 388202 count (455192 tried 1.2), 24963 sub out of 378364 (6.6%)
c swps: 10 count, 10 rounds, 504 queries (50.4/round)
c swps: 447 sat calls, 27 unsat (0.6% success rate)
c swps: 7451 decisions 16.7, 247 conflicts 0.6
c swps; 4199.6 avg class size, 159.4 avg environment size
c swps: 0 failed, 123 impls, 68 equivs
c swp0: 164 type 0 queries, 35 unsat (21.3%), 157 sat (95.7%)
c swp1: 340 type 1 queries, 219 unsat (64.4%), 279 sat (82.1%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 10706001 calls to obtain time
c tops: 81360 fixed 41%, 562 its, 691.87 confs/it
c trds: 18 transitive reductions, 3260 removed, 40 failed
c trds: 15259 nodes, 44089 edges, 35244990 steps
c trim: 1226809 words, 4.7 MB
c trnr: 18 count, 1 bin, 3073 trn, 140813364 steps
c unhd: 22 count, 29 rounds, 87348794 steps
c unhd: 554 non-trivial sccs of average size 2.1
c unhd: 95 units, 90 bin, 2 trn, 3 lrg
c unhd: 6900 failed, 6856 stamp, 0 lits, 17 bin, 18 trn, 3 lrg
c unhd: 551915 tauts, 16755 bin 3%, 14331 trn 3%, 977 lrg 0%
c unhd: 551915 tauts, 519852 stamp 94%, 493842 red 89%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6811599 str, 90 bin 0%, 2379 trn 0%, 6809130 lrg 100%, 6796425 red 100%
c vars: 34385 remaining 17% and 165611 removed 83% out of 199996
c vars: 81360 fixed 41%, 75852 eliminated 38%, 8399 equivalent 4%
c vsts: 10054936033 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 7.6 search visits per propagation, 24324.5 per conflict
c wchs: 1406120836 pushed, 58071996 enlarged, 221 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         378399        157520         47525      25739391       3506922        191245
c 
c  0 0         38693  10      8062   5         0   0  15406572  60   1612915  46     54037  28     2.8
c  1 5         16827   4      5665   4      1775   4   2098940   8<   317673   9     17184   9     1.7
c  2 6         44710  12     18517  12      5099  11   2778976  11    453123  13<    28216  15     5.4
c  3 9         49515  13     23322  15      6090  13   1817030   7    296091   8     19541  10<    8.4
c  4 14        41511  11     20169  13      5329  11   1149520   4    204049   6     15358   8     8.2
c  5 21        36985  10<    18560  12<     4955  10    829946   3    175187   5     13801   7     8.0
c  6 30        33797   9     16953  11      4759  10<   592011   2    135709   4     11431   6     8.2
c  7 41        29576   8     15158  10      4361   9    441501   2    112995   3      9899   5     8.6
c  8 54        23573   6     11743   7      3619   8    251316   1     67724   2      6858   4     7.6
c  9 69        17462   5      8398   5      2897   6    166946   1     53562   2      5402   3     6.2
c 10 86        16297   4      6405   4      2886   6    122187   0     42180   1      4902   3     3.8
c 11 126       17166   5      3089   2      3205   7     64265   0     25467   1      3248   2     2.0
c 12 230       11536   3      1387   1      2423   5     19217   0      9697   0      1302   1     2.3
c 13 534         751   0        92   0       127   0       964   0       550   0        66   0     0.3
c 
c avg                  4.9           4.9           6.0           1.3           2.1           3.2
c std                  3.3           2.8           3.2           2.1           2.7           3.1
c 
c   55.184  10% probe
c   31.223   6% bump
c   29.958   5% unhide
c   15.965   3% elim
c    8.199   2% cce
c    5.335   1% sweep
c    3.296   1% bca
c    3.130   1% decide
c 
c    8.019 < 1% rest (below)
c 
c    2.577   0% block
c    1.985   0% transred
c    1.317   0% gauss
c    0.953   0% ternres
c    0.815   0% quatres
c    0.371   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.884   1% preprocessing     3%
c  133.464  24% inprocessing     97%
c ==================================
c  137.348  25% simplifying
c  408.814  75% search
c ==================================
c  546.176 100% all
c 
c        388832 conflicts,         711.9 confs/sec
c          4571 ternaries,          85.1 confs/ternary
c          4587 binaries,           84.8 confs/binary
c           562 iterations,        691.9 confs/iteration
c 
c             6 reductions,          0.0 redus/sec,  64805.3 confs/reduction
c         11865 restarts,           21.7 rests/sec,     32.8 confs/restart
c       4964319 decisions,        9089.2 decis/sec,     12.8 decis/conflict
c    1321072383 propagations,  2418766.7 props/sec,    266.1 props/decision
c 
c 546.2 seconds, 149.2 MB
c launch: done
