c launch: /data/cnf/sc2014/app/UCG-20-10p1.cnf.bz2
c host: atom22
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/UCG-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 259258 1388006' header
c read 259258 variables, 1388006 clauses, 3352067 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=3
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 246109 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] SUM (--score=3)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  246109  1373987         0       0      0     0    0     0   58   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6014 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6014 out of 6014 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62780 variables
c [simpleprobe-1] all 196478 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 221 variables
c [simpleprobe-1] 15148 variables remain 8% (181109 retained 92%)
c [simpleprobe-1] removed 221 variables, found 15749 hbrs, 20 units
c [unhide-1] limit 66079 based on 1057273 irredundant clauses
c [unhide-1-1] 25 units, 1431 failed, 8310 tauts, 0 hbrs, 12876 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 194130 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 60833 not tried 31% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74191 = 38% variables out of 194130 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 874938 negative 99.2% of 881558 except 6620 0.8%
c [phase-count-1] 709837 positive 80.5% of 881558 except 171721 19.5%
c [phase-count-1] less non-negative clauses 6620 than limit 88100 (10.0%)
c [phase-count-1] non-pos/non-neg = 171721/6620 = 25.94 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119939 negative 100%
c [sort-queue-1] sorted 119939 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119939 (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 82741 variables 40.8% (119939 remain 49%)
c [simplification-1] removed 492429 irredundant clauses 35.8% (881558 remain 64%)
c [simplification-1] maximum reduction of 41% = max (41%, 36%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.2  119938   881558        33      29      2 11266    0     7   58   1%      0    7    1    0 23589%
c i    5.2  119924   881558        51      41      3 11268    0    10   58   2%      0   10    2    0 23000%
c i    5.3  119467   881558       117      77     13 11284    0    12   60   2%      0   12    2    0 18912%
c i    5.4  119307   881558       195     122     21 11305    0    13   60   2%      0   13    3    0 15934%
c i    5.4  118930   881558       206     126     24 11307    0    13   60   2%      0   13    3    0 15730%
c i    5.8  118920   881558       407     266     44 11337    1    19   60   3%      0   19    6    0 13859%
c i    5.8  118906   881558       408     266     44 11337    1    19   60   3%      0   19    6    0 13805%
c i    5.8  118894   881558       411     268     44 11337    1    19   60   3%      0   19    6    0 13671%
c i    5.8  118880   881558       412     268     44 11337    1    19   60   3%      0   19    6    0 13618%
c i    5.8  118866   881558       413     268     44 11337    1    19   60   3%      0   19    6    0 13565%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1092 variables
c [simpleprobe-2] 14563 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 15724 variables remain 13% (103123 retained 87%)
c [simpleprobe-2] removed 0 variables, found 1770 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 69807 literals 29%
c [treelook-1] scheduling used 474293 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 438946 steps
c [treelook-1] 69802 literals remain 29%
c [treelook-1] 68059 variables remain to probed next time 57%
c [treelook-1] removed 1 variables, found 3610 hbrs
c [basicprobe-1] limit 7009536 based on 876192 irredundant clauses
c [basicprobe-1-0] 43475 probes remain 38% after last round
c [basicprobe-1-0] 32 units = 32 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5359 variables, found 18501 hbrs
c [unhide-2] limit 54762 based on 876192 irredundant clauses
c [unhide-2-2] 14 units, 2558 failed, 8963 tauts, 0 hbrs, 1470 literals
c [elim-2] 57563 variables 52% will be scheduled this time
c [elim-2] scheduled 57563 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 23446 not tried 21% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 42 = 0% variables out of 57563 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 790013 negative 99.2% of 796633 except 6620 0.8%
c [phase-count-2] 637694 positive 80.0% of 796633 except 158939 20.0%
c [phase-count-2] less non-negative clauses 6620 than limit 79600 (10.0%)
c [phase-count-2] non-pos/non-neg = 158939/6620 = 24.01 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 12946 negative 100%
c [sort-queue-2] sorted 98990 enqueued variables after 413 conflicts
c [score-dist-2] active 11424 (10%), one 0 (0%), zero 98990 (90%)
c [score-dist-2] max exp 515, different 15 (3%)
c [score-dist-2] median active exp 510, avg 509.6
c [simplification-2] removed 8442 variables 7.1% (110414 remain 45%)
c [simplification-2] removed 84925 irredundant clauses 9.6% (796633 remain 58%)
c [simplification-2] maximum reduction of 10% = max (7%, 10%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1033 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.1  110413   796633       432     275     39 22051    1    20   54   4%      0   19    6    0 13810%
c i    9.1  110402   796633       433     275     39 22051    1    20   54   4%      0   19    6    0 13756%
c i    9.1  110388   796633       434     275     39 22051    1    19   54   4%      0   19    6    0 13703%
c i    9.1  110374   796633       436     276     39 22051    1    20   54   4%      0   19    6    0 13950%
c i    9.1  110364   796633       437     276     39 22051    1    20   54   4%      0   19    6    0 13896%
c i    9.1  110360   796633       438     276     39 22051    1    20   54   4%      0   19    6    0 13842%
c i    9.1  110347   796633       439     276     39 22051    1    20   54   4%      0   19    6    0 13788%
c i    9.1  110338   796633       440     276     39 22051    1    19   54   4%      0   19    6    0 13735%
c i    9.1  110328   796633       448     279     43 22051    1    20   54   4%      0   20    6    0 13384%
c i    9.3  110318   796633       577     380     57 22057    1    27   54   4%      0   27    8    0 12073%
c i    9.4  110308   796633       606     402     62 22058    1    29   54   4%      0   28   10    0 12915%
c i    9.6  110297   796633       756     528     70 22065    3    40   54   8%      1   40   32    0 15511%
c i    9.6  110284   796633       777     539     71 22065    3    41   54   8%      1   41   34    0 15146%
c i    9.6  110088   796633       796     557     71 22065    3    42   54   8%      1   42   33    0 14231%
c i    9.7  110080   796633       809     569     71 22065    4    44   54   8%      1   43   34    0 14018%
c i    9.7  110067   796633       824     582     71 22066    4    45   54   9%      0   44   36    0 14082%
c i    9.7  110066   796633       828     584     71 22067    4    45   54   9%      0   44   36    0 13874%
c i    9.7  110053   796633       829     584     71 22067    4    45   54   9%      0   44   36    0 13820%
c i    9.7  110039   796633       831     585     71 22067    4    45   54   9%      0   44   37    0 13968%
c i    9.7  110038   796633       833     585     71 22067    4    45   54   9%      0   44   38    0 14104%
c i    9.7  110037   796633       835     585     71 22067    4    45   54   9%      0   45   39    0 14229%
c i    9.7  110036   796633       837     585     71 22067    4    45   54  10%      0   45   40    0 14346%
c 
c [simplification-3] limit 1131 conflicts (hard 11000) hit after 1132 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3976 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3976 out of 3976 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 714 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 58282 literals 27%
c [treelook-2] scheduling used 306347 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 386702 steps
c [treelook-2] 58278 literals remain 27%
c [treelook-2] 39031 variables remain to probed next time 36%
c [treelook-2] removed 0 variables, found 3513 hbrs
c [unhide-3] limit 61635 with penalty 1 = 0 + 1
c [unhide-3-3] 2 units, 1299 failed, 18302 tauts, 0 hbrs, 2331 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 107931 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 30721 not tried 28% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1395 = 1% variables out of 107931 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 751523 negative 99.1% of 758053 except 6530 0.9%
c [phase-count-3] 604684 positive 79.8% of 758053 except 153369 20.2%
c [phase-count-3] less non-negative clauses 6530 than limit 75800 (10.0%)
c [phase-count-3] non-pos/non-neg = 153369/6530 = 23.49 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 8993 negative 100%
c [sort-queue-3] sorted 87821 enqueued variables after 1132 conflicts
c [score-dist-3] active 18715 (18%), one 0 (0%), zero 87821 (82%)
c [score-dist-3] max exp 518, different 18 (3%)
c [score-dist-3] median active exp 512, avg 512.1
c [simplification-3] removed 3500 variables 3.2% (106536 remain 43%)
c [simplification-3] removed 38580 irredundant clauses 4.8% (758053 remain 55%)
c [simplification-3] maximum reduction of 5% = max (3%, 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 13132 (soft 3132 + delta 10000)
c [simplification-3] new conflict limit 3132 (hard 13132)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.0  106535   758053      1164     759     89 22951    7    73   53   9%      1   73   40    0 8636%
c i   13.1  106524   758053      1201     784     92 22954    7    77   53  10%      1   77   45    1 8811%
c i   13.2  106516   758053      1258     826     97 22961    8    83   53  10%      1   82   53    1 9146%
c i   13.2  106515   758053      1259     826     97 22961    8    83   53  10%      1   82   53    1 9111%
c i   13.2  106505   758053      1260     826     97 22961    8    83   53  10%      1   82   52    1 9075%
c i   13.2  106495   758053      1261     826     97 22961    8    83   53  10%      1   82   52    1 9040%
c i   13.2  106486   758053      1263     827     97 22961    8    83   53  10%      1   82   52    1 8989%
c i   13.4  106476   758053      1413     947    102 22969   12    98   53  12%      1   97   76    1 9370%
c i   13.5  106255   758053      1466     989    104 22972   12   101   53  12%      1  100   69    1 8239%
c i   13.7  106247   758053      1602    1078    119 22982   15   108   53  14%      1  107   84    1 8049%
c i   13.9  106246   758053      1696    1147    127 22985   17   115   53  14%      1  114   82    1 7114%
c i   14.0  106234   758053      1739    1182    131 22988   17   119   53  14%      1  118   79    1 6598%
c i   14.3  106222   758053      1943    1335    147 22998   25   143   53  18%      1  141  133    2 7494%
c i   14.8  106129   758053      2283    1576    157 23022   29   150   54  20%      2  148   97    2 4478%
c i   14.9  106128   758053      2297    1585    158 23023   30   151   54  20%      2  148   95    2 4366%
c i   15.2  105788   758053      2464    1702    161 23025   32   155   54  21%      1  152   94    2 3888%
c i   15.5  105753   758053      2592    1751    161 23025   37   157   54  23%      1  154  129    3 4638%
c i   15.5  105752   758053      2598    1751    161 23025   37   157   54  24%      1  154  130    3 4659%
c i   15.5  105751   758053      2599    1751    161 23025   37   157   54  24%      1  154  129    3 4641%
c i   15.5  105750   758053      2600    1751    161 23025   37   157   54  24%      1  154  129    3 4623%
c i   15.5  105749   758053      2601    1751    161 23025   37   157   54  24%      1  154  128    3 4605%
c i   15.5  105748   758053      2632    1759    161 23025   38   158   54  24%      1  154  135    3 4684%
c i   15.7  105747   758053      2699    1810    161 23025   39   159   54  24%      1  155  123    3 4164%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.1  105702   758053      3007    2009    165 23046   44   166   54  26%      2  162  108    3 3119%
c 
c [simplification-4] limit of 211 binary hit after 211 binaries
c [decomp-8] removed 891 variables
c [basicprobe-2] limit 8289539 penalty 0 = 0 + 0
c [basicprobe-2-0] 38682 probes remain 38% after last round
c [basicprobe-2-0] 32 units = 32 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3465 variables, found 18672 hbrs
c [unhide-4] limit 165790 with penalty 1 = 0 + 1
c [unhide-4-4] 6 units, 1624 failed, 7220 tauts, 0 hbrs, 5488 literals
c [elim-4] 22412 variables 22% will be scheduled this time
c [elim-4] scheduled 22412 variables 22%
c [elim-4] boosting limit by 20
c [elim-4] limit of 663163180 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 17 variables 0% in round 1 in 43237648 steps
c [elim-4-1] backward subsumption/strengthening limit 43237600
c [elim-4-1-1] backward checking 118 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 4 and strengthened 0 clauses in 156553 steps
c [elim-4-1] rescheduled 11 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 10808 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 17 = 0% variables out of 22412 scheduled
c [elim-4] 17 < 1/100 * 22412 = 224 considered unsuccessful
c [phase-count-4] 694112 negative 99.1% of 700642 except 6530 0.9%
c [phase-count-4] 556241 positive 79.4% of 700642 except 144401 20.6%
c [phase-count-4] less non-negative clauses 6530 than limit 70000 (10.0%)
c [phase-count-4] non-pos/non-neg = 144401/6530 = 22.11 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 8293 negative 100%
c [sort-queue-4] sorted 76631 enqueued variables after 3096 conflicts
c [score-dist-4] active 23191 (23%), one 0 (0%), zero 76631 (77%)
c [score-dist-4] max exp 522, different 22 (4%)
c [score-dist-4] median active exp 515, avg 514.8
c [simplification-4] removed 5871 variables 5.6% (99822 remain 41%)
c [simplification-4] removed 57411 irredundant clauses 7.6% (700642 remain 51%)
c [simplification-4] maximum reduction of 8% = max (6%, 8%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3198 (hard 13132)
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   18.6   99821   700642      3115    2085    153 31748   44   174   50  25%      2  170   81    4 2324%
c 
c [simplification-5] limit 3198 conflicts (hard 13132) hit after 3200 conflicts
c [quatres-1] found 39922 quaternary clauses 37% in total
c [quatres-1-2] added 3 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 99686 free variables schedulable
c [ternres-1] 76 ternary resolvents (0 bin, 76 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 81 xors of average arity 2.3
c [gauss-1] connected 185 occurrences of 151 variables (average 1.2)
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 110 variables
c [unhide-5] limit 342648 with penalty 0 = 0 + 0
c [unhide-5-5] 7 units, 523 failed, 17936 tauts, 0 hbrs, 6649 literals
c [transred-1] limit 1713241 with penalty 0 = 0 + 0
c [transred-1] removed 220 transitive binary clauses
c [transred-1] found 12 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 98680 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 12258 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 25 clauses out of 433 (6%) of length 10
c [cce-1-1] eliminated 70 clauses out of 2593 (3%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 95 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 346947 clauses = 329067 binary + 17880 ternary
c [cce-1-1] tried to eliminate 357 small clauses 0%
c [cce-1-1] eliminated 136 binary clauses 0%
c [cce-1-1] eliminated 4 ternary clauses 0%
c [cce-1-1] eliminated 140 small clauses 0%
c [cce-1-1] eliminated 140 small clauses in 30000008 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 235 covered clauses in round 1
c [cce-1] eliminated 235 covered clauses in TOTAL during 1 rounds
c [cce-1] 235 < 1/100 * 661896 = 6618 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1323822 added (scaled 2)
c [bca-1] 187686 out of 197362 literals actually usable 95%
c [bca-1] added 374 blocked clauses in 621972 steps
c [sweep-1] limit 1323322 based on 661661 irredundant clauses
c [sweep-1-1] 4304 pos 4.4% + 94376 neg 95.6% = 98680 sched 100.0% ret 0
c [sweep-1-1] 1681015 steps 14 queries 18842.79 avg class size
c [sweep-1-1] 118 decisions 11 SAT calls 66.55 avg env size
c [sweep-1-1] 98649 variables remain 100% (31 retained 0%)
c [decomp-10] removed 5 variables
c [sweep-1-1] removed 5 vars (0 failed, 2 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 5 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-5] 655146 negative 99.0% of 661655 except 6509 1.0%
c [phase-count-5] 532749 positive 80.5% of 661655 except 128906 19.5%
c [phase-count-5] less non-negative clauses 6509 than limit 66100 (10.0%)
c [phase-count-5] non-pos/non-neg = 128906/6509 = 19.80 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 8036 negative 100%
c [sort-queue-5] sorted 74901 enqueued variables after 3200 conflicts
c [score-dist-5] active 23774 (24%), one 0 (0%), zero 74901 (76%)
c [score-dist-5] max exp 522, different 22 (4%)
c [score-dist-5] median active exp 515, avg 514.9
c [simplification-5] removed 1011 variables 1.0% (98675 remain 40%)
c [simplification-5] removed 38987 irredundant clauses 5.6% (661655 remain 48%)
c [simplification-5] maximum reduction of 6% = max (1%, 6%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 15200 (soft 5200 + delta 10000)
c [simplification-5] new conflict limit 5200 (hard 15200)
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.7   98674   661655      3313    2242    239 44676   45   187   50  24%      2  182   87    4 2330%
c i   23.4   98666   661655      3782    2608    248 44689   56   213   50  26%      2  207  145    5 3107%
c i   23.4   98656   661655      3786    2611    248 44689   55   214   50  26%      2  207  143    5 3065%
c i   23.5   98643   661655      3880    2689    255 44696   59   227   50  26%      2  220  165    5 3318%
c i   23.5   98206   661655      3881    2689    255 44696   59   227   50  26%      2  220  164    5 3305%
c i   23.9   98203   661655      4099    2877    257 44710   66   254   50  26%      2  246  184    6 3274%
c i   24.2   98196   661655      4301    3054    259 44716   76   277   51  28%      2  269  242    6 3753%
c i   24.4   98187   661655      4388    3101    259 44716   84   286   52  29%      2  277  303    7 4317%
c 
c [simplification-6] limit 5212 conflicts (hard 15200) hit after 5212 conflicts
c [quatres-2] found 36790 quaternary clauses 35% in total
c [quatres-2-2] added 1 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 98016 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 68838 variables remain 70% (29178 retained 30%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2345 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2345 out of 2345 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 672 variables
c [simpleprobe-3] 11999 schedulable variables 12%
c [simpleprobe-3] limit 5606858 penalty 1 = 1 + 0
c [decomp-12] removed 59 variables
c [simpleprobe-3] 11237 variables remain 11% (86707 retained 89%)
c [simpleprobe-3] removed 59 variables, found 7742 hbrs, 24 units
c [unhide-6] limit 280342 with penalty 1 = 0 + 1
c [unhide-6-6] 20 units, 1072 failed, 6171 tauts, 0 hbrs, 60452 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 277 transitive binary clauses
c [transred-2] found 9 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 96656 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 637 blocked clauses
c [block-2] 637 < 1/100 * 656034 = 6560 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 96656 variables 100%
c [elim-5] limit of 28034294 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 15097 not tried 16% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1903 = 2% variables out of 96656 scheduled
c [bca-2] limit of 10000000 steps and 1278453 added (scaled 2)
c [bca-2] 179262 out of 189508 literals actually usable 95%
c [bca-2] added 210 blocked clauses in 595699 steps
c [sweep-2] limit 1277766 based on 638883 irredundant clauses
c [sweep-2-1] 3863 pos 4.1% + 90863 neg 95.9% = 94726 sched 100.0% ret 27
c [sweep-2-1] 1333937 steps 17 queries 25461.35 avg class size
c [sweep-2-1] 95 decisions 13 SAT calls 76.85 avg env size
c [sweep-2-1] 94597 variables remain 100% (77 retained 0%)
c [decomp-13] removed 85 variables
c [sweep-2-1] removed 85 vars (0 failed, 3 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 85 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-6] 631809 negative 99.0% of 638217 except 6408 1.0%
c [phase-count-6] 510906 positive 80.1% of 638217 except 127311 19.9%
c [phase-count-6] less non-negative clauses 6408 than limit 63800 (10.0%)
c [phase-count-6] non-pos/non-neg = 127311/6408 = 19.87 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 7964 negative 100%
c [sort-queue-6] sorted 70704 enqueued variables after 5212 conflicts
c [score-dist-6] active 23964 (25%), one 0 (0%), zero 70704 (75%)
c [score-dist-6] max exp 524, different 24 (5%)
c [score-dist-6] median active exp 517, avg 516.3
c [simplification-6] removed 3348 variables 3.4% (94668 remain 38%)
c [simplification-6] removed 23438 irredundant clauses 3.5% (638217 remain 46%)
c [simplification-6] maximum reduction of 4% = max (3%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 19212 (soft 9212 + delta 10000)
c [simplification-6] new conflict limit 9212 (hard 19212)
c 
c [simplification-7] limit 9212 conflicts (hard 19212) hit after 9212 conflicts
c [quatres-3] found 38099 quaternary clauses 36% in total
c [quatres-3-2] added 1 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 12 xors of average arity 3.0
c [gauss-2] connected 36 occurrences of 33 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-7] limit 467721 with penalty 1 = 0 + 1
c [unhide-7-7] 4 units, 315 failed, 8072 tauts, 0 hbrs, 44806 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 284 transitive binary clauses
c [transred-3] found 8 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500008 steps for small clauses
c [cce-2-1] scheduling 499732 clauses = 312666 binary + 187066 ternary
c [cce-2-1] tried to eliminate 134 small clauses 0%
c [cce-2-1] eliminated 23 binary clauses 0%
c [cce-2-1] eliminated 6 ternary clauses 0%
c [cce-2-1] eliminated 29 small clauses 0%
c [cce-2-1] eliminated 5142 small clauses in 15000021 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5142 covered clauses in round 1
c [cce-2] eliminated 5142 covered clauses in TOTAL during 1 rounds
c [cce-2] 5142 < 1/100 * 631665 = 6316 considered unsuccessful
c [elim-6] 15084 variables 16% will be scheduled this time
c [elim-6] scheduled 15084 variables 16%
c [elim-6] limit of 93544225 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 32436809 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 15084 scheduled
c [bca-3] limit of 10000000 steps and 1253140 added (scaled 2)
c [bca-3] 175484 out of 188270 literals actually usable 93%
c [bca-3] added 171 blocked clauses in 578114 steps
c [sweep-3] limit 1403163 penalty 0 = 0 + 0
c [sweep-3-1] 3967 pos 4.2% + 90094 neg 95.8% = 94061 sched 99.9% ret 73
c [sweep-3-1] 1425923 steps 16 queries 30136.62 avg class size
c [sweep-3-1] 103 decisions 12 SAT calls 45.00 avg env size
c [sweep-3-1] 93651 variables remain 100% (103 retained 0%)
c [decomp-15] removed 383 variables
c [sweep-3-1] removed 383 vars (1 failed, 2 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 383 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-7] 618439 negative 99.0% of 624847 except 6408 1.0%
c [phase-count-7] 499751 positive 80.0% of 624847 except 125096 20.0%
c [phase-count-7] less non-negative clauses 6408 than limit 62400 (10.0%)
c [phase-count-7] non-pos/non-neg = 125096/6408 = 19.52 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 7600 negative 100%
c [sort-queue-7] sorted 66310 enqueued variables after 9212 conflicts
c [score-dist-7] active 27441 (29%), one 0 (0%), zero 66310 (71%)
c [score-dist-7] max exp 526, different 26 (5%)
c [score-dist-7] median active exp 518, avg 517.7
c [simplification-7] removed 917 variables 1.0% (93751 remain 38%)
c [simplification-7] removed 13370 irredundant clauses 2.1% (624847 remain 45%)
c [simplification-7] maximum reduction of 2% = max (1%, 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 29878 (soft 19878 + delta 10000)
c [simplification-7] new conflict limit 19878 (hard 29878)
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   60.0   93750   624847     18465    9230    405 45934  418   584   81  72%    185  485  608   80  758%
c i   60.0   93745   624847     18467    9231    405 45934  418   584   81  72%    184  485  604   80  753%
c 
c [simplification-8] limit 19883 conflicts (hard 29878) hit after 19883 conflicts
c [quatres-4] found 38932 quaternary clauses 37% in total
c [ternres-3] limit 5107023 with penalty 1 = 1 + 0
c [ternres-3] 65860 schedulable variables 70%
c [ternres-3] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-3] 29427 variables remain 31% (64314 retained 69%)
c [decomp-16] removed 10 variables
c [treelook-3] limit 510702 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 76402 literals 41%
c [treelook-3] scheduling used 523261 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 510702 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 628392 steps
c [treelook-3] 76309 literals remain 41%
c [treelook-3] 29794 variables remain to probed next time 32%
c [decomp-17] removed 107 variables
c [treelook-3] removed 186 variables, found 5829 hbrs
c [unhide-8] limit 1021404 with penalty 1 = 0 + 1
c [unhide-8-8] 6 units, 490 failed, 4427 tauts, 0 hbrs, 109838 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 256 transitive binary clauses
c [transred-4] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 92622 variables 100%
c [block-3] limit of 51070238 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 14 blocked clauses
c [block-3] 14 < 1/100 * 623714 = 6237 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1229329 added (scaled 2)
c [bca-4] 168512 out of 185246 literals actually usable 91%
c [bca-4] added 221 blocked clauses in 548838 steps
c [sweep-4] limit 3064214 penalty 0 = 0 + 0
c [sweep-4-1] 4294 pos 4.6% + 88235 neg 95.4% = 92529 sched 99.9% ret 93
c [sweep-4-1] 3086821 steps 49 queries 14108.59 avg class size
c [sweep-4-1] 258 decisions 42 SAT calls 45.26 avg env size
c [sweep-4-1] 92110 variables remain 99% (496 retained 1%)
c [decomp-18] removed 27 variables
c [sweep-4-1] removed 27 vars (0 failed, 6 eqs, 14 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 27 vars in TOTAL (1 rounds, 48 queries)
c [phase-count-8] 607638 negative 99.0% of 614046 except 6408 1.0%
c [phase-count-8] 489608 positive 79.7% of 614046 except 124438 20.3%
c [phase-count-8] less non-negative clauses 6408 than limit 61400 (10.0%)
c [phase-count-8] non-pos/non-neg = 124438/6408 = 19.42 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 7105 negative 100%
c [sort-queue-8] sorted 60745 enqueued variables after 19883 conflicts
c [score-dist-8] active 31850 (34%), one 0 (0%), zero 60745 (66%)
c [score-dist-8] max exp 529, different 29 (5%)
c [score-dist-8] median active exp 521, avg 520.3
c [simplification-8] removed 1146 variables 1.2% (92595 remain 38%)
c [simplification-8] removed 10801 irredundant clauses 1.7% (614046 remain 45%)
c [simplification-8] maximum reduction of 2% = max (1%, 2%)
c [simplification-8] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-8] new conflict interval 17332
c [simplification-8] penalized conflict interval 17332 = 1 * 17332
c [simplification-8] hard conflict limit 47215 (soft 37215 + delta 10000)
c [simplification-8] new conflict limit 37215 (hard 47215)
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.5   92594   614046     33662   15341    498 49145  578   659  114  88%    181  435  541  180  300%
c i  104.4   92593   614046     34714   15641    512 49155  558   644  114  87%     44  414  435  185  235%
c i  104.5   92591   614046     34715   15641    512 49155  558   644  114  87%     43  414  433  185  234%
c i  104.5   92589   614046     34716   15641    512 49155  558   644  114  87%     43  414  431  185  233%
c i  104.5   92586   614046     34732   15656    512 49155  556   644  114  86%     42  414  414  185  224%
c i  111.5   92434   614046     38037   16914    526 49190  692   851  114  81%     -2  595  731  214  342%
c i  116.7   91929   614046     40288   18269    534 49241  648   901  169  72%    -16  624  565  226  250%
c i  118.8   91925   614046     41230   18774    550 49274  615   895  169  69%    -26  610  323  230  141%
c i  118.8   91917   614046     41241   18783    550 49275  614   896  169  69%    -26  610  310  230  135%
c i  118.9   91916   614046     41242   18783    550 49275  614   895  169  69%    -26  610  309  230  135%
c i  118.9   91915   614046     41243   18783    550 49275  613   895  169  69%    -26  609  308  230  134%
c i  118.9   91914   614046     41244   18783    550 49275  613   895  169  69%    -26  609  307  230  134%
c i  119.1   91913   614046     41362   18874    553 49282  597   899  169  66%    -27  613  205  229   89%
c i  119.1   91843   614046     41405   18911    555 49283  591   902  169  66%    -28  615  176  229   77%
c i  119.1   91842   614046     41406   18911    555 49283  591   902  169  66%    -28  614  176  229   77%
c i  119.2   91841   614046     41407   18911    555 49283  591   901  169  66%    -28  614  175  229   76%
c i  119.2   91840   614046     41408   18911    555 49283  591   901  169  66%    -28  614  174  229   76%
c i  119.2   91839   614046     41465   18961    556 49284  583   905  169  64%    -28  617  144  229   63%
c i  119.3   91828   614046     41478   18972    556 49284  581   906  169  64%    -29  618  138  229   60%
c i  119.3   91821   614046     41574   19057    556 49284  568   910  169  62%    -30  621   98  229   43%
c i  119.4   91812   614046     41646   19116    559 49286  558   912  169  61%    -30  623   80  228   35%
c i  119.4   91802   614046     41653   19119    559 49286  558   912  169  61%    -30  623   80  228   35%
c i  119.4   91791   614046     41655   19119    559 49286  557   912  169  61%    -30  622   79  228   35%
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  119.5   91782   614046     41738   19187    559 49288  547   914  169  60%    -31  624   70  228   31%
c i  119.5   91775   614046     41745   19193    559 49288  546   914  169  60%    -31  624   70  228   31%
c i  119.6   91765   614046     41758   19205    559 49288  545   915  169  60%    -31  624   70  228   31%
c i  119.6   91756   614046     41778   19222    559 49288  542   915  169  59%    -31  625   70  228   31%
c i  119.6   91747   614046     41821   19261    559 49288  537   917  169  59%    -32  626   70  228   31%
c i  119.7   91737   614046     41822   19261    559 49288  537   916  169  59%    -32  625   70  228   31%
c i  119.7   91724   614046     41823   19261    559 49288  537   916  169  59%    -32  625   69  228   30%
c i  119.7   91714   614046     41824   19261    559 49288  537   916  169  59%    -32  625   69  228   30%
c i  119.7   91705   614046     41825   19261    559 49288  537   916  169  59%    -32  625   69  228   30%
c i  119.7   91689   614046     41826   19261    559 49288  537   915  169  59%    -32  624   69  228   30%
c i  119.8   91676   614046     41885   19310    559 49288  530   917  169  58%    -32  625   67  228   30%
c i  120.1   91664   614046     42198   19577    561 49292  495   924  170  54%    -34  629   57  227   25%
c i  120.2   91480   614046     42201   19579    561 49292  495   924  170  54%    -34  629   57  227   25%
c i  120.8   91473   614046     42835   20125    578 49309  436   930  171  47%    -34  629   65  226   29%
c i  120.8   91419   614046     42858   20144    579 49309  434   930  171  47%    -34  629   66  225   29%
c i  120.9   91418   614046     42859   20144    579 49309  434   929  171  47%    -34  628   66  225   29%
c i  120.9   91417   614046     42860   20144    579 49309  434   929  171  47%    -34  628   66  225   29%
c i  123.2   91416   614046     44438   21481    585 49325  338   931  174  36%    -26  615  303  223  136%
c i  123.2   91403   614046     44439   21481    585 49325  338   930  174  36%    -26  614  302  223  135%
c i  124.6   91402   614046     45424   22396    587 49333  278   925  179  30%    -28  600   49  221   22%
c i  125.3   91392   614046     46271   23135    658 49336  231   933  179  25%    -30  600   28  218   13%
c i  125.3   91384   614046     46290   23147    664 49336  230   933  179  25%    -30  600   28  218   13%
c i  125.5   91375   614046     46394   23240    666 49340  226   934  179  24%    -30  600   34  218   15%
c 
c [simplification-9] limit 37385 conflicts (hard 47215) hit after 47215 conflicts
c [ternres-4] limit 24367856 with penalty 0 = 0 + 0
c [ternres-4] 28786 schedulable variables 31%
c [ternres-4] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 1302 variables
c [basicprobe-3] limit 121839284 penalty 0 = 0 + 0
c [basicprobe-3-0] 31516 probes remain 36% after last round
c [basicprobe-3-0] 489 units = 489 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 3176 variables, found 150881 hbrs
c [bate-1] eliminated 279 asymmetric tautologies during probing
c [unhide-9] limit 1218392 with penalty 2 = 0 + 2
c [unhide-9-9] 2 units, 126 failed, 12648 tauts, 0 hbrs, 511105 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 172 transitive binary clauses
c [transred-5] found 3 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 87894 variables 100%
c [elim-7] limit of 243678568 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1981 variables 2% in round 1 in 53230105 steps
c [elim-7-1] backward subsumption/strengthening limit 53230100
c [elim-7-1-1] backward checking 7137 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 5 and strengthened 141 clauses in 2394850 steps
c [elim-7-1] rescheduled 324 variables 0% by backward subsumption
c [elim-7-2] eliminated 46 variables 0% in round 2 in 356294 steps
c [elim-7-2] backward subsumption/strengthening limit 356200
c [elim-7-2-1] backward checking 337 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 258741 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 2027 = 2% variables out of 87894 scheduled
c [bca-5] limit of 10000000 steps and 1141182 added (scaled 2)
c [bca-5] 153246 out of 171736 literals actually usable 89%
c [bca-5] added 92 blocked clauses in 479529 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 73103570 penalty 0 = 0 + 0
c [sweep-5-1] 5676 pos 6.6% + 79754 neg 93.4% = 85430 sched 99.5% ret 437
c [sweep-5-1] 73187898 steps 879 queries 900.63 avg class size
c [sweep-5-1] 8176 decisions 715 SAT calls 85.10 avg env size
c [sweep-5-1] 63036 variables remain 74% (22015 retained 26%)
c [decomp-20] removed 1516 variables
c [sweep-5-1] removed 1516 vars (0 failed, 200 eqs, 297 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1516 vars in TOTAL (1 rounds, 878 queries)
c [phase-count-9] 554597 negative 98.9% of 560847 except 6250 1.1%
c [phase-count-9] 445183 positive 79.4% of 560847 except 115664 20.6%
c [phase-count-9] less non-negative clauses 6250 than limit 56000 (10.0%)
c [phase-count-9] non-pos/non-neg = 115664/6250 = 18.51 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 1425 negative 100%
c [sort-queue-9] sorted 39887 enqueued variables after 47215 conflicts
c [score-dist-9] active 44464 (53%), one 0 (0%), zero 39887 (47%)
c [score-dist-9] max exp 531, different 30 (6%)
c [score-dist-9] median active exp 523, avg 522.4
c [simplification-9] removed 7014 variables 7.7% (84351 remain 34%)
c [simplification-9] removed 53199 irredundant clauses 8.7% (560847 remain 41%)
c [simplification-9] maximum reduction of 9% = max (8%, 9%)
c [simplification-9] large reduction 9% >= 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 59215 (soft 49215 + delta 10000)
c [simplification-9] new conflict limit 49215 (hard 59215)
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.5   84350   560847     49314   11669    701 216168  189   954   63  20%     -6  594   69  215   32%
c i  143.8   84342   560847     49620   11932    701 216172  187   956   66  20%    -14  593  139  215   65%
c i  144.2   84341   560847     49980   12258    719 216176  175   958   67  18%    -20  592   65  214   30%
c i  144.3   84331   560847     50006   12280    720 216176  174   959   67  18%    -20  592   60  214   28%
c i  145.6   84319   560847     50924   13019    721 216178  196   963   73  20%    -25  588  304  215  142%
c i  145.7   84227   560847     50993   13087    721 216178  194   963   73  20%    -26  588  251  214  117%
c i  148.0   84226   560847     52331   14106    724 216187  231   968   77  24%    -24  581  416  217  192%
c 
c [simplification-10] limit 49215 conflicts (hard 59215) hit after 55540 conflicts
c [quatres-5] found 39217 quaternary clauses 42% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 7 quaternary resolvents
c [ternres-5] limit 27649581 with penalty 0 = 0 + 0
c [ternres-5] all 84224 free variables schedulable
c [ternres-5] 869 ternary resolvents (0 bin, 869 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 1728098 penalty 3 = 3 + 0
c [card-4] found 5230 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1728098 for elimination
c [card-4] 5230 out of 5230 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1382479 penalty 2 = 2 + 0
c [gauss-3] extracted 32 xors of average arity 2.7
c [gauss-3] connected 87 occurrences of 54 variables (average 1.6)
c [gauss-3] limit 1382479 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-21] removed 2 variables
c [simpleprobe-4] 9574 schedulable variables 11%
c [simpleprobe-4] limit 110598325 penalty 0 = 0 + 0
c [decomp-22] removed 2674 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 2674 variables, found 116727 hbrs, 975 units
c [unhide-10] limit 1382479 with penalty 2 = 0 + 2
c [unhide-10-10] 4 units, 389 failed, 55755 tauts, 0 hbrs, 142762 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 356 transitive binary clauses
c [transred-6] found 3 units
c [cce-3] limit of 34561976 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 23 clauses out of 1413 (2%) of length 9
c [cce-3-1] eliminated 20 clauses out of 620 (3%) of length 8
c [cce-3-1] eliminated 70 clauses out of 845 (8%) of length 7
c [cce-3-1] eliminated 3100 clauses out of 5518 (56%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 3213 large clauses in 34561987 steps
c [cce-3-1] allowing another 17280993 steps for small clauses
c [cce-3-1] scheduling 417284 clauses = 276028 binary + 141256 ternary
c [cce-3-1] tried to eliminate 406 small clauses 0%
c [cce-3-1] eliminated 84 binary clauses 0%
c [cce-3-1] eliminated 24 ternary clauses 0%
c [cce-3-1] eliminated 108 small clauses 0%
c [cce-3-1] eliminated 3920 small clauses in 34561981 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 7133 covered clauses in round 1
c [cce-3] eliminated 7133 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 81211 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 11059832520 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3266 variables 4% in round 1 in 51288527 steps
c [elim-8-1] backward subsumption/strengthening limit 51288500
c [elim-8-1-1] backward checking 9527 touched variables 12%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 8 and strengthened 684 clauses in 4434395 steps
c [elim-8-1] rescheduled 1426 variables 2% by backward subsumption
c [elim-8-2] eliminated 234 variables 0% in round 2 in 2742884 steps
c [elim-8-2] backward subsumption/strengthening limit 2742800
c [elim-8-2-1] backward checking 1585 touched variables 2%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 1 clauses in 869392 steps
c [elim-8-2] rescheduled 5 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 3810 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 3500 = 4% variables out of 81211 scheduled
c [bca-6] limit of 10000000 steps and 1030930 added (scaled 2)
c [bca-6] 136387 out of 155424 literals actually usable 88%
c [bca-6] added 464 blocked clauses in 412285 steps
c [sweep-6] limit 8294874 penalty 0 = 0 + 0
c [sweep-6-1] 4870 pos 8.3% + 53909 neg 91.7% = 58779 sched 75.6% ret 18932
c [sweep-6-1] 8296091 steps 83 queries 5507.10 avg class size
c [sweep-6-1] 850 decisions 64 SAT calls 95.39 avg env size
c [sweep-6-1] 58312 variables remain 75% (19385 retained 25%)
c [decomp-23] removed 32 variables
c [sweep-6-1] removed 32 vars (0 failed, 20 eqs, 33 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 32 vars in TOTAL (1 rounds, 82 queries)
c [phase-count-10] 511913 negative 99.4% of 514749 except 2836 0.6%
c [phase-count-10] 400312 positive 77.8% of 514749 except 114437 22.2%
c [phase-count-10] less non-negative clauses 2836 than limit 51400 (10.0%)
c [phase-count-10] non-pos/non-neg = 114437/2836 = 40.35 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 637 negative 100%
c [sort-queue-10] sorted 30884 enqueued variables after 55540 conflicts
c [score-dist-10] active 46795 (60%), one 0 (0%), zero 30884 (40%)
c [score-dist-10] max exp 531, different 30 (6%)
c [score-dist-10] median active exp 523, avg 522.9
c [simplification-10] removed 6545 variables 7.8% (77679 remain 32%)
c [simplification-10] removed 46098 irredundant clauses 8.2% (514749 remain 37%)
c [simplification-10] maximum reduction of 8% = max (8%, 8%)
c [simplification-10] large reduction 8% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 67540 (soft 57540 + delta 10000)
c [simplification-10] new conflict limit 57540 (hard 67540)
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  163.8   77678   514749     55631    8939    780 244444  490   978   58  50%      1  562  700  239  293%
c i  163.9   77671   514749     55632    8939    780 244444  490   978   58  50%      1  562  697  239  291%
c i  166.6   77664   514749     57009    9706    782 244446  562  1055   64  53%    -16  627  826  249  331%
c i  166.6   77660   514749     57020    9711    782 244449  561  1056   64  53%    -16  628  811  249  325%
c i  168.0   77657   514749     57758   10264    786 244455  562  1092   71  52%    -22  656  604  253  239%
c i  168.2   77656   514749     57826   10309    786 244457  564  1094   71  52%    -23  658  616  253  243%
c i  170.5   77651   514749     58987   11114    786 244462  585  1137   76  51%    -23  689  779  260  300%
c i  172.8   77643   514749     60167   11999    790 244465  596  1170   86  51%    -23  710  669  267  251%
c i  177.5   77624   514749     62627   13821    790 244466  641  1208  102  53%     -8  721  761  282  270%
c i  178.7   77623   514749     63334   14307    792 244472  642  1206  113  53%    -18  712  596  286  208%
c i  178.7   77622   514749     63335   14307    792 244472  642  1206  113  53%    -18  711  593  286  208%
c i  178.8   77621   514749     63347   14316    792 244473  641  1206  113  53%    -18  711  578  286  202%
c i  178.9   77620   514749     63415   14381    793 244473  631  1206  113  52%    -19  710  457  286  160%
c i  178.9   77619   514749     63416   14381    793 244473  631  1206  113  52%    -19  710  455  286  159%
c i  178.9   77618   514749     63417   14381    793 244473  631  1205  113  52%    -19  710  453  286  159%
c i  179.0   77617   514749     63424   14386    794 244473  630  1205  113  52%    -19  709  448  286  157%
c i  179.0   77616   514749     63425   14386    794 244473  630  1205  113  52%    -19  709  446  286  156%
c i  179.0   77615   514749     63426   14386    794 244473  630  1205  113  52%    -19  709  444  286  156%
c i  179.0   77614   514749     63430   14389    794 244473  630  1204  113  52%    -19  709  443  286  155%
c i  179.3   77613   514749     63548   14492    794 244473  621  1205  113  52%    -20  708  388  286  136%
c i  179.3   77612   514749     63550   14492    794 244474  620  1205  113  52%    -20  708  385  286  135%
c i  179.3   77611   514749     63551   14492    794 244474  620  1204  113  52%    -20  707  383  286  134%
c i  179.3   77610   514749     63552   14492    794 244474  620  1204  113  52%    -20  707  382  286  134%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  179.4   77607   514749     63562   14501    794 244474  620  1204  113  51%    -20  707  382  286  134%
c i  179.5   77606   514749     63625   14548    798 244474  617  1205  113  51%    -21  707  397  286  139%
c i  179.5   77605   514749     63629   14551    798 244474  616  1204  113  51%    -21  706  394  286  138%
c i  179.5   77604   514749     63631   14551    798 244475  616  1204  113  51%    -21  706  391  286  137%
c i  179.6   77603   514749     63637   14555    798 244476  615  1204  113  51%    -21  706  386  286  135%
c i  179.7   77602   514749     63672   14583    798 244476  615  1203  113  51%    -22  705  402  286  141%
c i  180.3   77597   514749     64021   14828    798 244479  616  1207  113  51%    -24  705  600  288  209%
c i  184.2   77596   514749     65665   15251    798 244484  781  1227  113  64%    -18  707 1046  308  339%
c i  186.7   77558   514749     66776   15616    799 244488  846  1231  113  69%    -20  699 1032  321  322%
c i  187.1   77555   514749     66980   15727    800 244495  845  1231  145  69%    -22  698  905  322  281%
c 
c [simplification-11] limit 57637 conflicts (hard 67540) hit after 67540 conflicts
c [quatres-6] found 36896 quaternary clauses 43% in total
c [quatres-6-2] added 2 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-6] limit 33136713 with penalty 0 = 0 + 0
c [ternres-6] all 77551 free variables schedulable
c [ternres-6] 315 ternary resolvents (0 bin, 315 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-24] removed 131 variables
c [treelook-4] limit 3313671 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 126515 literals 82%
c [treelook-4] scheduling used 1750112 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3313671 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 3351485 steps
c [treelook-4] 126445 literals remain 82%
c [treelook-4] 22269 variables remain to probed next time 29%
c [treelook-4] removed 10 variables, found 22784 hbrs
c [unhide-11] limit 1656835 with penalty 2 = 0 + 2
c [unhide-11-11] 2 units, 45 failed, 12128 tauts, 0 hbrs, 658078 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 227 transitive binary clauses
c [transred-7] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 77478 variables 100%
c [block-4] limit of 82841783 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 48 blocked clauses
c [block-4] 48 < 1/100 * 503686 = 5036 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 77475 variables 100%
c [elim-9] limit of 662734269 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 397 variables 1% in round 1 in 48349885 steps
c [elim-9-1] backward subsumption/strengthening limit 48349800
c [elim-9-1-1] backward checking 2125 touched variables 3%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 2 clauses in 791266 steps
c [elim-9-1] rescheduled 8 variables 0% by backward subsumption
c [elim-9-2] eliminated 2 variables 0% in round 2 in 2350 steps
c [elim-9-2] backward subsumption/strengthening limit 2300
c [elim-9-2-1] backward checking 20 touched variables 0%
c [elim-9-2-1] incomplete backward checking 16 remain 80%
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 2328 steps
c [elim-9-2] fully rescheduled 77072 variables 99%
c [elim-9-3] eliminated 5 variables 0% in round 3 in 48293445 steps
c [elim-9-3] backward subsumption/strengthening limit 48293400
c [elim-9-3-1] backward checking 46 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 102043 steps
c [elim-9] fully completed in 3 rounds
c [gc-73] reconnected 264739 binary clauses (produced 0 empty 3 units)
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 411 = 1% variables out of 77475 scheduled
c [elim-9] 411 < 1/100 * 77475 = 774 considered unsuccessful
c [bca-7] limit of 10000000 steps and 1006222 added (scaled 2)
c [bca-7] 132356 out of 154130 literals actually usable 86%
c [bca-7] added 67 blocked clauses in 398503 steps
c [sweep-7] limit 9941014 penalty 0 = 0 + 0
c [sweep-7-1] 4334 pos 7.5% + 53545 neg 92.5% = 57879 sched 75.1% ret 19185
c [sweep-7-1] 10006172 steps 161 queries 2390.57 avg class size
c [sweep-7-1] 1358 decisions 136 SAT calls 97.22 avg env size
c [sweep-7-1] 56309 variables remain 73% (20509 retained 27%)
c [decomp-26] removed 328 variables
c [sweep-7-1] removed 328 vars (0 failed, 32 eqs, 55 impls)
c [sweep-7] removed 328 vars in TOTAL (1 rounds, 160 queries)
c [phase-count-11] 497690 negative 99.4% of 500512 except 2822 0.6%
c [phase-count-11] 389217 positive 77.8% of 500512 except 111295 22.2%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 147 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 26627 enqueued variables after 67540 conflicts
c [score-dist-11] active 50109 (65%), one 0 (0%), zero 26627 (35%)
c [score-dist-11] max exp 532, different 31 (6%)
c [score-dist-11] median active exp 524, avg 523.2
c [simplification-11] removed 815 variables 1.1% (76736 remain 31%)
c [simplification-11] removed 14237 irredundant clauses 2.8% (500512 remain 36%)
c [simplification-11] maximum reduction of 3% = max (1%, 3%)
c [simplification-11] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-11] new conflict interval 22332
c [simplification-11] penalized conflict interval 22332 = 1 * 22332
c [simplification-11] hard conflict limit 101038 (soft 89872 + delta 11166)
c [simplification-11] new conflict limit 89872 (hard 101038)
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  201.3   76735   500512     69353   13678   1056 269108  882  1245   89  71%     -8  687  996  343  290%
c i  204.6   76734   500512     70586   14208   1056 269109  941  1252  107  75%    -16  682 1147  357  321%
c i  210.1   76733   500512     72465   14803   1059 269114 1026  1274  107  81%    -12  684 1114  380  293%
c i  212.9   76732   500512     73486   15072   1074 269127 1062  1287  107  83%    -18  686 1083  392  276%
c i  227.3   76731   500512     80135   16545   1092 269140 1277  1395  143  92%     57  723 1341  480  279%
c i  228.0   76730   500512     80495   16694   1092 269140 1267  1399  143  91%     31  724 1183  484  245%
c i  229.8   76619   500512     81407   16960   1093 269141 1264  1407  215  90%     -1  722 1171  494  237%
c i  230.3   76612   500512     81722   17223   1094 269146 1233  1428  215  86%     -8  739  946  496  191%
c i  230.3   76609   500512     81723   17223   1094 269146 1233  1428  215  86%     -8  739  942  496  190%
c i  230.3   76605   500512     81724   17223   1094 269146 1232  1427  215  86%     -8  739  939  496  189%
c i  230.4   76603   500512     81726   17224   1094 269146 1232  1427  215  86%     -9  738  934  496  188%
c i  230.4   76600   500512     81727   17224   1094 269146 1231  1427  215  86%     -9  738  930  496  188%
c i  230.4   76597   500512     81728   17224   1094 269146 1231  1427  215  86%     -9  738  927  496  187%
c i  230.4   76592   500512     81729   17224   1094 269146 1231  1426  215  86%     -9  737  923  496  186%
c i  230.4   76570   500512     81730   17224   1094 269146 1231  1426  215  86%     -9  737  919  496  185%
c i  230.4   76566   500512     81731   17224   1094 269146 1230  1425  215  86%     -9  736  916  496  185%
c i  230.4   76563   500512     81732   17224   1094 269146 1230  1425  215  86%     -9  736  912  496  184%
c i  230.4   76559   500512     81733   17224   1094 269146 1230  1425  215  86%     -9  736  909  496  183%
c i  230.6   76552   500512     81858   17333   1094 269147 1213  1432  216  85%    -11  742  810  496  163%
c i  230.7   76548   500512     81898   17370   1094 269147 1207  1435  216  84%    -12  744  780  496  157%
c i  230.9   76547   500512     82010   17477   1095 269148 1189  1444  216  82%    -14  752  704  496  142%
c i  234.4   76546   500512     83482   18450   1108 269156 1199  1517  223  79%    -16  808 1241  512  243%
c 
c [simplification-12] limit 89967 conflicts (hard 101038) hit after 89972 conflicts
c [quatres-7] found 35812 quaternary clauses 43% in total
c [ternres-7] limit 43657651 with penalty 0 = 0 + 0
c [ternres-7] all 76536 free variables schedulable
c [ternres-7] 82 ternary resolvents (0 bin, 82 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 228 variables
c [basicprobe-4] limit 218288258 penalty 0 = 0 + 0
c [basicprobe-4-0] 22123 probes remain 30% after last round
c [basicprobe-4-0] 971 units = 922 failed (95%) + 49 lifted (5%)
c [basicprobe-4-0] removed 2736 variables, found 204885 hbrs
c [bate-2] eliminated 506 asymmetric tautologies during probing
c [unhide-12] limit 1091441 with penalty 3 = 0 + 3
c [unhide-12-12] 9 units, 679 failed, 59981 tauts, 0 hbrs, 609167 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 170 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 1091441290 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 757 (0%) of length 7
c [cce-4-1] eliminated 116 clauses out of 2545 (5%) of length 6
c [cce-4-1] eliminated 25178 clauses out of 36553 (69%) of length 5
c [cce-4-1] eliminated 19304 clauses out of 30984 (62%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 44599 large clauses in 688504580 steps
c [cce-4-1] allowing another 344252290 steps for small clauses
c [cce-4-1] scheduling 270007 clauses = 245867 binary + 24140 ternary
c [cce-4-1] tried to eliminate 42102 small clauses 16%
c [cce-4-1] eliminated 10034 binary clauses 4%
c [cce-4-1] eliminated 2149 ternary clauses 9%
c [cce-4-1] eliminated 12183 small clauses 5%
c [cce-4-1] eliminated 17883 small clauses in 1091441294 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 62482 covered clauses in round 1
c [cce-4] eliminated 62482 covered clauses in TOTAL during 1 rounds
c [bca-8] limit of 10000000 steps and 837443 added (scaled 2)
c [bca-8] 122918 out of 146290 literals actually usable 84%
c [bca-8] added 117 blocked clauses in 302675 steps
c [sweep-8] limit 13097295 penalty 0 = 0 + 0
c [sweep-8-1] 4020 pos 7.4% + 50010 neg 92.6% = 54030 sched 73.9% ret 19114
c [sweep-8-1] 13100838 steps 221 queries 2477.19 avg class size
c [sweep-8-1] 2500 decisions 198 SAT calls 134.26 avg env size
c [sweep-8-1] 51297 variables remain 70% (21829 retained 30%)
c [decomp-28] removed 306 variables
c [sweep-8-1] removed 306 vars (0 failed, 22 eqs, 40 impls)
c [sweep-8] removed 306 vars in TOTAL (1 rounds, 220 queries)
c [phase-count-12] 416350 negative 99.8% of 417202 except 852 0.2%
c [phase-count-12] 317122 positive 76.0% of 417202 except 100080 24.0%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 5 positive 12%, 37 negative 88%
c [sort-queue-12] sorted 21549 enqueued variables after 89972 conflicts
c [score-dist-12] active 51289 (70%), one 0 (0%), zero 21549 (30%)
c [score-dist-12] max exp 533, different 32 (6%)
c [score-dist-12] median active exp 524, avg 523.9
c [simplification-12] removed 3698 variables 4.8% (72838 remain 30%)
c [simplification-12] removed 83310 irredundant clauses 16.6% (417202 remain 30%)
c [simplification-12] maximum reduction of 17% = max (5%, 17%)
c [simplification-12] large reduction 17% >= 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 101972 (soft 91972 + delta 10000)
c [simplification-12] new conflict limit 91972 (hard 101972)
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  299.3   72837   417202     89989   21066   3286 412208 1386  1600  148  87%     54  809 1497  594  252%
c i  306.0   72834   417202     92259   21445   3287 412210 1391  1560  160  89%     -2  742 1126  622  181%
c i  308.8   72807   417202     93285   21633   3288 412212 1402  1558  160  90%    -15  729 1374  635  217%
c 
c [simplification-13] limit 91972 conflicts (hard 101972) hit after 96205 conflicts
c [ternres-8] limit 46302084 with penalty 0 = 0 + 0
c [ternres-8] all 72807 free variables schedulable
c [ternres-8] 34 ternary resolvents (0 bin, 34 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-29] removed 39 variables
c [simpleprobe-5] all 72799 free variables schedulable
c [simpleprobe-5] limit 185208337 penalty 0 = 0 + 0
c [decomp-30] removed 1769 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1769 variables, found 103663 hbrs, 880 units
c [unhide-13] limit 1157552 with penalty 3 = 0 + 3
c [unhide-13-13] 1 units, 14 failed, 9116 tauts, 0 hbrs, 413426 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 290 transitive binary clauses
c [cce-5] limit of 231510421 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 3 clauses out of 763 (0%) of length 7
c [cce-5-1] eliminated 50 clauses out of 2408 (2%) of length 6
c [cce-5-1] eliminated 6 clauses out of 11340 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 59 large clauses in 231510425 steps
c [cce-5-1] allowing another 115755212 steps for small clauses
c [cce-5-1] scheduling 344749 clauses = 228663 binary + 116086 ternary
c [cce-5-1] tried to eliminate 4893 small clauses 1%
c [cce-5-1] eliminated 743 binary clauses 0%
c [cce-5-1] eliminated 305 ternary clauses 0%
c [cce-5-1] eliminated 1048 small clauses 0%
c [cce-5-1] eliminated 1142 small clauses in 231510432 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1201 covered clauses in round 1
c [cce-5] eliminated 1201 covered clauses in TOTAL during 1 rounds
c [cce-5] 1201 < 1/100 * 393541 = 3935 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 71012 variables 100%
c [elim-10] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 20478 variables 29% in round 1 in 33785674 steps
c [elim-10-1] backward subsumption/strengthening limit 33785600
c [elim-10-1-1] backward checking 42527 touched variables 60%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 7 and strengthened 52 clauses in 5743751 steps
c [elim-10-1] rescheduled 145 variables 0% by backward subsumption
c [elim-10-2] eliminated 5 variables 0% in round 2 in 68744 steps
c [elim-10-2] backward subsumption/strengthening limit 68700
c [elim-10-2-1] backward checking 77 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 3 clauses in 68701 steps
c [elim-10-2] rescheduled 9 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 2834 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 20483 = 29% variables out of 71012 scheduled
c [bca-9] limit of 10000000 steps and 696596 added (scaled 2)
c [bca-9] 93750 out of 101060 literals actually usable 93%
c [bca-9] added 292 blocked clauses in 223361 steps
c [sweep-9] limit 13890625 penalty 0 = 0 + 0
c [sweep-9-1] 3524 pos 9.1% + 35189 neg 90.9% = 38713 sched 76.6% ret 11816
c [sweep-9-1] 13982802 steps 306 queries 1435.75 avg class size
c [sweep-9-1] 3166 decisions 278 SAT calls 89.56 avg env size
c [sweep-9-1] 35998 variables remain 72% (14229 retained 28%)
c [decomp-31] removed 421 variables
c [sweep-9-1] removed 421 vars (0 failed, 31 eqs, 63 impls)
c [sweep-9] removed 421 vars in TOTAL (1 rounds, 305 queries)
c [phase-count-13] 345233 negative 99.8% of 346033 except 800 0.2%
c [phase-count-13] 249589 positive 72.1% of 346033 except 96444 27.9%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 7 positive 12%, 51 negative 88%
c [sort-queue-13] sorted 12866 enqueued variables after 96205 conflicts
c [score-dist-13] active 37242 (74%), one 0 (0%), zero 12866 (26%)
c [score-dist-13] max exp 533, different 32 (6%)
c [score-dist-13] median active exp 524, avg 523.8
c [simplification-13] removed 22699 variables 31.2% (50108 remain 20%)
c [simplification-13] removed 71169 irredundant clauses 17.1% (346033 remain 25%)
c [simplification-13] maximum reduction of 31% = max (31%, 17%)
c [simplification-13] large reduction 31% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 108205 (soft 98205 + delta 10000)
c [simplification-13] new conflict limit 98205 (hard 108205)
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  334.8   50107   346033     97461    3234   2504 404402 1095  1509   47  73%     18  636  227  660   34%
c i  334.8   50089   346033     97467    3237   2506 404402 1094  1508   47  73%     18  636  224  660   34%
c i  334.8   50086   346033     97476    3243   2506 404403 1092  1508   47  72%     17  635  219  660   33%
c 
c [simplification-14] limit 98207 conflicts (hard 108205) hit after 100240 conflicts
c [quatres-8] found 21646 quaternary clauses 52% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 14 quaternary resolvents
c [ternres-9] limit 46901923 with penalty 0 = 0 + 0
c [ternres-9] all 50080 free variables schedulable
c [ternres-9] 558 ternary resolvents (2 bin, 556 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 1172548 penalty 3 = 3 + 0
c [gauss-4] extracted 28 xors of average arity 2.9
c [gauss-4] connected 82 occurrences of 82 variables (average 1.0)
c [gauss-4] limit 1172548 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 2 variables
c [treelook-5] limit 4690192 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 67145 literals 67%
c [treelook-5] scheduling used 1262937 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4690192 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 4733253 steps
c [treelook-5] 67056 literals remain 67%
c [treelook-5] 9124 variables remain to probed next time 18%
c [treelook-5] removed 11 variables, found 35839 hbrs
c [unhide-14] limit 9380384 with penalty 0 = 0 + 0
c [unhide-14-18] 11 units, 263 failed, 113431 tauts, 0 hbrs, 289122 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 285 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 49739 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 540 variables 1% in round 1 in 29236127 steps
c [elim-11-1] backward subsumption/strengthening limit 29236100
c [elim-11-1-1] backward checking 3536 touched variables 7%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 16 clauses in 917690 steps
c [elim-11-1] rescheduled 65 variables 0% by backward subsumption
c [elim-11-2] eliminated 2 variables 0% in round 2 in 66414 steps
c [elim-11-2] backward subsumption/strengthening limit 66400
c [elim-11-2-1] backward checking 37 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 3 clauses in 62028 steps
c [elim-11-2] rescheduled 15 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 13122 steps
c [elim-11-3] backward subsumption/strengthening limit 13100
c [elim-11-3-1] backward checking 11 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 13101 steps
c [elim-11] incomplete 8 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 543 = 1% variables out of 49739 scheduled
c [bca-10] limit of 10000000 steps and 675426 added (scaled 2)
c [bca-10] 87419 out of 98394 literals actually usable 89%
c [bca-10] added 96 blocked clauses in 209740 steps
c [sweep-10] limit 14070577 penalty 0 = 0 + 0
c [sweep-10-1] 3338 pos 9.5% + 31941 neg 90.5% = 35279 sched 71.7% ret 13917
c [sweep-10-1] 14075140 steps 324 queries 1381.31 avg class size
c [sweep-10-1] 3602 decisions 303 SAT calls 100.55 avg env size
c [sweep-10-1] 32765 variables remain 67% (16320 retained 33%)
c [decomp-34] removed 224 variables
c [sweep-10-1] removed 224 vars (0 failed, 31 eqs, 48 impls)
c [sweep-10] removed 224 vars in TOTAL (1 rounds, 323 queries)
c [phase-count-14] 335247 negative 99.8% of 335980 except 733 0.2%
c [phase-count-14] 241559 positive 71.9% of 335980 except 94421 28.1%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 12 positive 100%, 0 negative 0%
c [sort-queue-14] sorted 11737 enqueued variables after 100240 conflicts
c [score-dist-14] active 37235 (76%), one 0 (0%), zero 11737 (24%)
c [score-dist-14] max exp 533, different 32 (6%)
c [score-dist-14] median active exp 524, avg 524.0
c [simplification-14] removed 1108 variables 2.2% (48972 remain 20%)
c [simplification-14] removed 10053 irredundant clauses 2.9% (335980 remain 24%)
c [simplification-14] maximum reduction of 3% = max (2%, 3%)
c [simplification-14] geometric conflict interval increment 5583 = 22332 / 4
c [simplification-14] new conflict interval 27915
c [simplification-14] penalized conflict interval 27915 = 1 * 27915
c [simplification-14] hard conflict limit 142112 (soft 128155 + delta 13957)
c [simplification-14] new conflict limit 128155 (hard 142112)
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  345.6   48971   335980    101830    6249   2739 321046  730  1390   56  53%     21  482  494  651   76%
c i  352.4   48970   335980    106674    9386   2759 321067  709  1330   89  53%     28  390  590  656   90%
c i  352.4   48969   335980    106687    9396   2759 321067  707  1330   89  53%     27  390  567  656   86%
c i  352.4   48967   335980    106700    9406   2759 321067  705  1330   89  53%     27  390  548  656   83%
c i  353.6   48966   335980    107493    9914   2760 321072  717  1325   90  54%     -1  381  753  657  115%
c i  353.6   48964   335980    107494    9914   2760 321072  717  1325   90  54%     -1  380  750  657  114%
c i  353.6   48958   335980    107495    9914   2760 321072  717  1324   90  54%     -1  380  747  657  114%
c i  368.1   48952   335980    116248   14782   2789 321094  859  1303  135  66%     85  312  870  679  128%
c 
c [simplification-15] limit 128175 conflicts (hard 142112) hit after 128175 conflicts
c [quatres-9] found 21499 quaternary clauses 52% in total
c [quatres-9-2] added 14 quaternary resolvents
c [ternres-10] limit 55158460 with penalty 0 = 0 + 0
c [ternres-10] all 48944 free variables schedulable
c [ternres-10] 517 ternary resolvents (1 bin, 516 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 1723701 penalty 4 = 4 + 0
c [card-5] found 3543 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1723701 for elimination
c [card-5] 3543 out of 3543 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 32 variables
c [basicprobe-5] limit 275792304 penalty 0 = 0 + 0
c [basicprobe-5-0] 3637 probes remain 8% after last round
c [basicprobe-5-0] 1266 units = 1222 failed (97%) + 44 lifted (3%)
c [basicprobe-5-0] removed 2341 variables, found 405763 hbrs
c [bate-3] eliminated 1555 asymmetric tautologies during probing
c [unhide-15] limit 1378961 with penalty 3 = 0 + 3
c [unhide-15-19] 1 units, 35 failed, 4811 tauts, 0 hbrs, 1140863 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 385 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 46573 variables 100%
c [block-5] limit of 68948076 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 300 blocked clauses
c [block-5] 300 < 1/100 * 311011 = 3110 considered unsuccessful
c [cce-6] limit of 137896152 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 43
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 35
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 34
c [cce-6-1] eliminated 1 clauses out of 2 (50%) 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 2 clauses out of 2 (100%) of length 24
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 23
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 22
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 18
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 17
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 16
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 14
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 12
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 10
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 9
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 8
c [cce-6-1] eliminated 1 clauses out of 66 (2%) of length 7
c [cce-6-1] eliminated 117 clauses out of 3330 (4%) of length 6
c [cce-6-1] eliminated 1059 clauses out of 13798 (8%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1242 large clauses in 137896163 steps
c [cce-6-1] allowing another 68948081 steps for small clauses
c [cce-6-1] scheduling 179157 clauses = 162136 binary + 17021 ternary
c [cce-6-1] tried to eliminate 5048 small clauses 3%
c [cce-6-1] eliminated 1056 binary clauses 1%
c [cce-6-1] eliminated 197 ternary clauses 1%
c [cce-6-1] eliminated 1253 small clauses 1%
c [cce-6-1] eliminated 1253 small clauses in 137896152 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 2495 covered clauses in round 1
c [cce-6] eliminated 2495 covered clauses in TOTAL during 1 rounds
c [cce-6] 2495 < 1/100 * 310483 = 3104 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 46569 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 1417 variables 3% in round 1 in 26353980 steps
c [elim-12-1] backward subsumption/strengthening limit 26353900
c [elim-12-1-1] backward checking 7293 touched variables 16%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 15 and strengthened 63 clauses in 1676477 steps
c [elim-12-1] rescheduled 166 variables 0% by backward subsumption
c [elim-12-2] eliminated 8 variables 0% in round 2 in 71220 steps
c [elim-12-2] backward subsumption/strengthening limit 71200
c [elim-12-2-1] backward checking 93 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 0 and strengthened 9 clauses in 71201 steps
c [elim-12-2] rescheduled 26 variables 0% by backward subsumption
c [elim-12-3] eliminated 2 variables 0% in round 3 in 15191 steps
c [elim-12-3] backward subsumption/strengthening limit 15100
c [elim-12-3-1] backward checking 23 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 2 clauses in 15101 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 1427 = 3% variables out of 46569 scheduled
c [bca-11] limit of 10000000 steps and 613880 added (scaled 2)
c [bca-11] 77069 out of 90286 literals actually usable 85%
c [bca-11] added 44 blocked clauses in 189234 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 165475380 penalty 0 = 0 + 0
c [sweep-11-1] 3525 pos 11.7% + 26535 neg 88.3% = 30060 sched 66.6% ret 15082
c [sweep-11-1] 165480686 steps 4051 queries 91.51 avg class size
c [sweep-11-1] 25734 decisions 3611 SAT calls 92.37 avg env size
c [sweep-11-1] 7212 variables remain 16% (37087 retained 84%)
c [decomp-36] removed 1807 variables
c [sweep-11-1] removed 1807 vars (0 failed, 504 eqs, 893 impls)
c [sweep-11] removed 1807 vars in TOTAL (1 rounds, 4050 queries)
c [phase-count-15] 299831 negative 99.8% of 300562 except 731 0.2%
c [phase-count-15] 213878 positive 71.2% of 300562 except 86684 28.8%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 1 positive 20%, 4 negative 80%
c [sort-queue-15] sorted 7524 enqueued variables after 128175 conflicts
c [score-dist-15] active 35811 (83%), one 0 (0%), zero 7524 (17%)
c [score-dist-15] max exp 534, different 30 (6%)
c [score-dist-15] median active exp 525, avg 525.0
c [simplification-15] removed 5609 variables 11.5% (43335 remain 18%)
c [simplification-15] removed 35418 irredundant clauses 10.5% (300562 remain 22%)
c [simplification-15] maximum reduction of 11% = max (11%, 11%)
c [simplification-15] large reduction 11% >= 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 140175 (soft 130175 + delta 10000)
c [simplification-15] new conflict limit 130175 (hard 140175)
c 
c [simplification-16] limit 130175 conflicts (hard 140175) hit after 130176 conflicts
c [quatres-10] found 18370 quaternary clauses 50% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 6 quaternary resolvents
c [ternres-11] limit 55763635 with penalty 0 = 0 + 0
c [ternres-11] all 43335 free variables schedulable
c [ternres-11] 1344 ternary resolvents (0 bin, 1344 trn)
c [ternres-11] fully completed ternary resolution
c [simpleprobe-6] all 43335 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 688 variables
c [simpleprobe-6] 40 variables remain 0% (42607 retained 100%)
c [simpleprobe-6] removed 688 variables, found 244278 hbrs, 280 units
c [unhide-16] limit 2788181 with penalty 2 = 0 + 2
c [unhide-16-20] 4 units, 72 failed, 207106 tauts, 0 hbrs, 111222 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 605 transitive binary clauses
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 42586 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 487 variables 1% in round 1 in 27626003 steps
c [elim-13-1] backward subsumption/strengthening limit 27626000
c [elim-13-1-1] backward checking 3037 touched variables 7%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 22 and strengthened 60 clauses in 748869 steps
c [elim-13-1] rescheduled 166 variables 0% by backward subsumption
c [elim-13-2] eliminated 12 variables 0% in round 2 in 179841 steps
c [elim-13-2] backward subsumption/strengthening limit 179800
c [elim-13-2-1] backward checking 120 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 18 and strengthened 10 clauses in 108403 steps
c [elim-13-2] rescheduled 50 variables 0% by backward subsumption
c [elim-13-3] eliminated 3 variables 0% in round 3 in 125177 steps
c [elim-13-3] backward subsumption/strengthening limit 125100
c [elim-13-3-1] backward checking 42 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 0 and strengthened 3 clauses in 68550 steps
c [elim-13] incomplete 12 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 502 = 1% variables out of 42586 scheduled
c [bca-12] limit of 10000000 steps and 581146 added (scaled 2)
c [bca-12] 67824 out of 84170 literals actually usable 81%
c [bca-12] added 42 blocked clauses in 162280 steps
c [sweep-12] limit 16729090 penalty 0 = 0 + 0
c [sweep-12-1] 547 pos 8.4% + 5933 neg 91.6% = 6480 sched 15.4% ret 35604
c [sweep-12-1] 16733711 steps 501 queries 211.57 avg class size
c [sweep-12-1] 3356 decisions 445 SAT calls 93.96 avg env size
c [sweep-12-1] 5291 variables remain 13% (36775 retained 87%)
c [decomp-39] removed 228 variables
c [sweep-12-1] removed 228 vars (0 failed, 63 eqs, 114 impls)
c [sweep-12] removed 228 vars in TOTAL (1 rounds, 500 queries)
c [phase-count-16] 288610 negative 99.8% of 289323 except 713 0.2%
c [phase-count-16] 202896 positive 70.1% of 289323 except 86427 29.9%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-16] sorted 6764 enqueued variables after 130176 conflicts
c [score-dist-16] active 35092 (84%), one 0 (0%), zero 6764 (16%)
c [score-dist-16] max exp 534, different 30 (6%)
c [score-dist-16] median active exp 525, avg 525.1
c [simplification-16] removed 1479 variables 3.4% (41856 remain 17%)
c [simplification-16] removed 11239 irredundant clauses 3.7% (289323 remain 21%)
c [simplification-16] maximum reduction of 4% = max (3%, 4%)
c [simplification-16] geometric conflict interval increment 5583 = 27915 / 5
c [simplification-16] new conflict interval 33498
c [simplification-16] penalized conflict interval 33498 = 1 * 33498
c [simplification-16] hard conflict limit 180423 (soft 163674 + delta 16749)
c [simplification-16] new conflict limit 163674 (hard 180423)
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  430.5   41855   289323    134656   12636   4735 638692  792  1065   99  74%    210   19  612  718   85%
c i  430.9   41854   289323    135069   12935   4736 638692  774  1063  106  73%    120   16  577  718   80%
c i  467.3   41830   289323    162012   17814   4753 638698  792   916  233  86%    291  -98  657  762   86%
c 
c [simplification-17] limit 163674 conflicts (hard 180423) hit after 180424 conflicts
c [quatres-11] found 17122 quaternary clauses 48% in total
c [quatres-11-2] added 1 single-self-subsuming ternary resolvents
c [quatres-11-2] added 2 quaternary resolvents
c [ternres-12] limit 68570559 with penalty 0 = 0 + 0
c [ternres-12] all 41828 free variables schedulable
c [ternres-12] 343 ternary resolvents (0 bin, 343 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-40] removed 30 variables
c [treelook-6] limit 6857055 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 57237 literals 68%
c [treelook-6] scheduling used 1320701 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 6857055 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 6916068 steps
c [treelook-6] 57042 literals remain 68%
c [treelook-6] 7339 variables remain to probed next time 18%
c [treelook-6] removed 22 variables, found 47574 hbrs
c [unhide-17] limit 3428527 with penalty 2 = 0 + 2
c [unhide-17-22] 7 units, 48 failed, 90221 tauts, 0 hbrs, 494600 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 408 transitive binary clauses
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 41758 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 186 variables 0% in round 1 in 27457978 steps
c [elim-14-1] backward subsumption/strengthening limit 27457900
c [elim-14-1-1] backward checking 1269 touched variables 3%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 4 and strengthened 3 clauses in 328648 steps
c [elim-14-1] rescheduled 16 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 11820 steps
c [elim-14-2] backward subsumption/strengthening limit 11800
c [elim-14-2-1] backward checking 10 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 2 clauses in 11801 steps
c [elim-14-2] rescheduled 8 variables 0% by backward subsumption
c [elim-14-3] eliminated 1 variables 0% in round 3 in 7132 steps
c [elim-14-3] backward subsumption/strengthening limit 7100
c [elim-14-3-1] backward checking 10 touched variables 0%
c [elim-14-3-1] incomplete backward checking 3 remain 30%
c [elim-14-3] subsumed 0 and strengthened 2 clauses in 7108 steps
c [elim-14] incomplete 8 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 188 = 0% variables out of 41758 scheduled
c [elim-14] 188 < 1/100 * 41758 = 417 considered unsuccessful
c [bca-13] limit of 10000000 steps and 569621 added (scaled 2)
c [bca-13] 65411 out of 83142 literals actually usable 79%
c [bca-13] added 39 blocked clauses in 164959 steps
c [sweep-13] limit 20571167 penalty 0 = 0 + 0
c [sweep-13-1] 444 pos 8.7% + 4662 neg 91.3% = 5106 sched 12.3% ret 36464
c [sweep-13-1] 20574161 steps 742 queries 102.95 avg class size
c [sweep-13-1] 4277 decisions 662 SAT calls 73.62 avg env size
c [sweep-13-1] 3469 variables remain 8% (38072 retained 92%)
c [decomp-42] removed 186 variables
c [sweep-13-1] removed 186 vars (0 failed, 90 eqs, 171 impls)
c [sweep-13] removed 186 vars in TOTAL (1 rounds, 741 queries)
c [phase-count-17] 282784 negative 99.7% of 283493 except 709 0.3%
c [phase-count-17] 199184 positive 70.3% of 283493 except 84309 29.7%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 6310 enqueued variables after 180424 conflicts
c [score-dist-17] active 35074 (85%), one 0 (0%), zero 6310 (15%)
c [score-dist-17] max exp 535, different 27 (5%)
c [score-dist-17] median active exp 526, avg 526.1
c [simplification-17] removed 444 variables 1.1% (41384 remain 17%)
c [simplification-17] removed 5830 irredundant clauses 2.0% (283493 remain 21%)
c [simplification-17] maximum reduction of 2% = max (1%, 2%)
c [simplification-17] geometric conflict interval increment 11166 = 33498 / 3
c [simplification-17] new conflict interval 44664
c [simplification-17] penalized conflict interval 44664 = 1 * 44664
c [simplification-17] hard conflict limit 247420 (soft 225088 + delta 22332)
c [simplification-17] new conflict limit 225088 (hard 247420)
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  543.4   41383   283493    209803   25716   4872 605481  778   798  267  97%    464 -120  741  759   98%
c i  552.0   41382   283493    216472   27198   4872 605498  757   804  267  94%   -166 -103  728  758   96%
c 
c [simplification-18] limit 225088 conflicts (hard 247420) hit after 247420 conflicts
c [quatres-12] found 17213 quaternary clauses 48% in total
c [quatres-12-2] added 8 quaternary resolvents
c [ternres-13] limit 88294947 with penalty 0 = 0 + 0
c [ternres-13] all 41346 free variables schedulable
c [ternres-13] 206 ternary resolvents (0 bin, 206 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-43] removed 38 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 3825 sched 9%, 522 failed, 28 lifted, 84881 hbrs
c [decomp-44] removed 855 variables
c [basicprobe-6-1] 1143 probes remain 3% after last round
c [basicprobe-6-1] 990 units = 942 failed (95%) + 48 lifted (5%)
c [basicprobe-6-1] removed 1587 variables, found 212311 hbrs
c [bate-4] eliminated 298 asymmetric tautologies during probing
c [unhide-18] limit 2207373 with penalty 3 = 0 + 3
c [unhide-18-23] 0 units, 20 failed, 86126 tauts, 0 hbrs, 248708 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 490 transitive binary clauses
c [cce-7] limit of 110368684 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 83
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 79
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 78
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 76
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 74
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 72
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 70
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 69
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 68
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 67
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 66
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 65
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 64
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 63
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 62
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 61
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 60
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 59
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 58
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 57
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 56
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 55
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 54
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 53
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 52
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 51
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 50
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 49
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 48
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 47
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 46
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 45
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 44
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 43
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 42
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 41
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 40
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 39
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 38
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 37
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 36
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 35
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 34
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 33
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 32
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 31
c [cce-7-1] eliminated 6 clauses out of 9 (67%) of length 30
c [cce-7-1] eliminated 6 clauses out of 9 (67%) of length 29
c [cce-7-1] eliminated 6 clauses out of 9 (67%) of length 28
c [cce-7-1] eliminated 8 clauses out of 12 (67%) of length 27
c [cce-7-1] eliminated 9 clauses out of 12 (75%) of length 26
c [cce-7-1] eliminated 9 clauses out of 14 (64%) of length 25
c [cce-7-1] eliminated 11 clauses out of 14 (79%) of length 24
c [cce-7-1] eliminated 10 clauses out of 18 (56%) of length 23
c [cce-7-1] eliminated 13 clauses out of 17 (76%) of length 22
c [cce-7-1] eliminated 15 clauses out of 21 (71%) of length 21
c [cce-7-1] eliminated 15 clauses out of 21 (71%) of length 20
c [cce-7-1] eliminated 18 clauses out of 23 (78%) of length 19
c [cce-7-1] eliminated 14 clauses out of 21 (67%) of length 18
c [cce-7-1] eliminated 18 clauses out of 22 (82%) of length 17
c [cce-7-1] eliminated 15 clauses out of 25 (60%) of length 16
c [cce-7-1] eliminated 21 clauses out of 29 (72%) of length 15
c [cce-7-1] eliminated 21 clauses out of 29 (72%) of length 14
c [cce-7-1] eliminated 21 clauses out of 28 (75%) of length 13
c [cce-7-1] eliminated 21 clauses out of 28 (75%) of length 12
c [cce-7-1] eliminated 19 clauses out of 29 (66%) of length 11
c [cce-7-1] eliminated 22 clauses out of 36 (61%) of length 10
c [cce-7-1] eliminated 27 clauses out of 41 (66%) of length 9
c [cce-7-1] eliminated 35 clauses out of 52 (67%) of length 8
c [cce-7-1] eliminated 43 clauses out of 121 (36%) of length 7
c [cce-7-1] eliminated 161 clauses out of 3157 (5%) of length 6
c [cce-7-1] eliminated 86 clauses out of 11647 (1%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 812 large clauses in 110368701 steps
c [cce-7-1] allowing another 55184350 steps for small clauses
c [cce-7-1] scheduling 222248 clauses = 154626 binary + 67622 ternary
c [cce-7-1] tried to eliminate 3651 small clauses 2%
c [cce-7-1] eliminated 603 binary clauses 0%
c [cce-7-1] eliminated 121 ternary clauses 0%
c [cce-7-1] eliminated 724 small clauses 0%
c [cce-7-1] eliminated 884 small clauses in 110368690 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1696 covered clauses in round 1
c [cce-7] eliminated 1696 covered clauses in TOTAL during 1 rounds
c [cce-7] 1696 < 1/100 * 267763 = 2677 considered unsuccessful
c [bca-14] limit of 10000000 steps and 533748 added (scaled 2)
c [bca-14] 61254 out of 79496 literals actually usable 77%
c [bca-14] added 24 blocked clauses in 165288 steps
c [sweep-14] limit 26488484 penalty 0 = 0 + 0
c [sweep-14-1] 267 pos 8.6% + 2845 neg 91.4% = 3112 sched 7.8% ret 36635
c [sweep-14-1] 26522266 steps 995 queries 48.57 avg class size
c [sweep-14-1] 6872 decisions 886 SAT calls 94.05 avg env size
c [sweep-14-1] 1377 variables remain 3% (38316 retained 97%)
c [decomp-45] removed 250 variables
c [sweep-14-1] removed 250 vars (0 failed, 113 eqs, 228 impls)
c [sweep-14] removed 250 vars in TOTAL (1 rounds, 994 queries)
c [phase-count-18] 264677 negative 99.7% of 265387 except 710 0.3%
c [phase-count-18] 183783 positive 69.3% of 265387 except 81604 30.7%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 5284 enqueued variables after 247420 conflicts
c [score-dist-18] active 34213 (87%), one 0 (0%), zero 5284 (13%)
c [score-dist-18] max exp 536, different 27 (5%)
c [score-dist-18] median active exp 527, avg 526.8
c [simplification-18] removed 1849 variables 4.5% (39497 remain 16%)
c [simplification-18] removed 18106 irredundant clauses 6.4% (265387 remain 19%)
c [simplification-18] maximum reduction of 6% = max (4%, 6%)
c [simplification-18] large reduction 6% >= 5% limit
c [simplification-18] next conflict interval 2474 = min (247420/100, 44664)
c [simplification-18] penalized conflict interval 2474 = 1 * 2474
c [simplification-18] hard conflict limit 259894 (soft 249894 + delta 10000)
c [simplification-18] new conflict limit 249894 (hard 259894)
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  620.1   39496   265387    248945   31261   4853 697309  713   732  188  97%    234 -123  662  748   88%
c i  621.6   39495   265387    250083   31343   4853 697310  699   716  188  98%    -89 -137  653  747   87%
c 
c [simplification-19] limit 249894 conflicts (hard 259894) hit after 259895 conflicts
c [quatres-13] found 15949 quaternary clauses 48% in total
c [quatres-13-2] added 2 single-self-subsuming ternary resolvents
c [quatres-13-2] added 2 quaternary resolvents
c [ternres-14] limit 91652749 with penalty 0 = 0 + 0
c [ternres-14] all 39488 free variables schedulable
c [ternres-14] 347 ternary resolvents (2 bin, 345 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 1145659 penalty 4 = 4 + 0
c [gauss-5] extracted 39 xors of average arity 3.0
c [gauss-5] connected 117 occurrences of 117 variables (average 1.0)
c [gauss-5] limit 1145659 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-46] removed 1 variables
c [simpleprobe-7] 38 schedulable variables 0%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-47] removed 82 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 82 variables, found 115336 hbrs, 36 units
c [unhide-19] limit 2291318 with penalty 3 = 0 + 3
c [unhide-19-25] 2 units, 24 failed, 126032 tauts, 0 hbrs, 284092 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 513 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 39383 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 756 variables 2% in round 1 in 23234999 steps
c [elim-15-1] backward subsumption/strengthening limit 23234900
c [elim-15-1-1] backward checking 4550 touched variables 12%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 7 and strengthened 20 clauses in 1116709 steps
c [elim-15-1] rescheduled 52 variables 0% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 83389 steps
c [elim-15-2] backward subsumption/strengthening limit 83300
c [elim-15-2-1] backward checking 33 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 2 clauses in 66011 steps
c [elim-15-2] rescheduled 8 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 8442 steps
c [elim-15-3] backward subsumption/strengthening limit 8400
c [elim-15-3-1] backward checking 10 touched variables 0%
c [elim-15-3-1] incomplete backward checking 6 remain 60%
c [elim-15-3] subsumed 0 and strengthened 2 clauses in 8464 steps
c [elim-15] incomplete 8 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 759 = 2% variables out of 39383 scheduled
c [bca-15] limit of 10000000 steps and 520280 added (scaled 2)
c [bca-15] 59572 out of 77250 literals actually usable 77%
c [bca-15] added 67 blocked clauses in 141596 steps
c [sweep-15] limit 27495824 penalty 0 = 0 + 0
c [sweep-15-1] 98 pos 7.7% + 1168 neg 92.3% = 1266 sched 3.3% ret 37358
c [sweep-15-1] 15811057 steps 952 queries 18.73 avg class size
c [sweep-15-1] 6160 decisions 812 SAT calls 66.85 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-48] removed 165 variables
c [sweep-15-1] removed 165 vars (0 failed, 140 eqs, 210 impls)
c [sweep-15-2] 4304 pos 11.2% + 34155 neg 88.8% = 38459 sched 100.0% ret 0
c [sweep-15-2] 11714162 steps 265 queries 1220.72 avg class size
c [sweep-15-2] 4990 decisions 250 SAT calls 129.79 avg env size
c [sweep-15-2] 33056 variables remain 86% (5362 retained 14%)
c [decomp-49] removed 66 variables
c [sweep-15-2] removed 66 vars (0 failed, 22 eqs, 32 impls)
c [sweep-15] removed 231 vars in TOTAL (2 rounds, 1215 queries)
c [phase-count-19] 257770 negative 99.7% of 258466 except 696 0.3%
c [phase-count-19] 178341 positive 69.0% of 258466 except 80125 31.0%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 4777 enqueued variables after 259895 conflicts
c [score-dist-19] active 33616 (88%), one 0 (0%), zero 4777 (12%)
c [score-dist-19] max exp 536, different 25 (5%)
c [score-dist-19] median active exp 527, avg 526.9
c [simplification-19] removed 1095 variables 2.8% (38393 remain 16%)
c [simplification-19] removed 6921 irredundant clauses 2.6% (258466 remain 19%)
c [simplification-19] maximum reduction of 3% = max (3%, 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 343640 (soft 315725 + delta 27915)
c [simplification-19] new conflict limit 315725 (hard 343640)
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  741.0   38392   258466    339729   23915   4777 629001  492   559  398  88%    693 -114  440  611   72%
c 
c [simplification-20] limit 315725 conflicts (hard 343640) hit after 343642 conflicts
c [quatres-14] found 15889 quaternary clauses 46% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 3 quaternary resolvents
c [ternres-15] limit 110022167 with penalty 0 = 0 + 0
c [ternres-15] all 38392 free variables schedulable
c [ternres-15] 215 ternary resolvents (3 bin, 212 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-50] removed 2 variables
c [treelook-7] limit 11002216 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 52444 literals 68%
c [treelook-7] scheduling used 1224388 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 11002216 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 11074293 steps
c [treelook-7] 52219 literals remain 68%
c [treelook-7] 6791 variables remain to probed next time 18%
c [treelook-7] removed 0 variables, found 61545 hbrs
c [unhide-20] limit 5000000 with penalty 2 = 0 + 2
c [unhide-20-28] 6 units, 25 failed, 128818 tauts, 0 hbrs, 604552 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 428 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 38352 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 28 blocked clauses
c [block-6] 28 < 1/100 * 255824 = 2558 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 38351 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 132 variables 0% in round 1 in 23527411 steps
c [elim-16-1] backward subsumption/strengthening limit 23527400
c [elim-16-1-1] backward checking 935 touched variables 2%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 2 and strengthened 9 clauses in 252743 steps
c [elim-16-1] rescheduled 33 variables 0% by backward subsumption
c [elim-16-2] eliminated 1 variables 0% in round 2 in 198337 steps
c [elim-16-2] backward subsumption/strengthening limit 198300
c [elim-16-2-1] backward checking 15 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 2 clauses in 44704 steps
c [elim-16-2] rescheduled 8 variables 0% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 9216 steps
c [elim-16-3] backward subsumption/strengthening limit 9200
c [elim-16-3-1] backward checking 10 touched variables 0%
c [elim-16-3-1] incomplete backward checking 6 remain 60%
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 9212 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 134 = 0% variables out of 38351 scheduled
c [elim-16] 134 < 1/100 * 38351 = 383 considered unsuccessful
c [bca-16] limit of 10000000 steps and 512596 added (scaled 2)
c [bca-16] 57804 out of 76436 literals actually usable 76%
c [bca-16] added 26 blocked clauses in 149942 steps
c [sweep-16] limit 33006650 penalty 0 = 0 + 0
c [sweep-16-1] 3883 pos 11.8% + 29038 neg 88.2% = 32921 sched 86.1% ret 5296
c [sweep-16-1] 33032871 steps 819 queries 400.85 avg class size
c [sweep-16-1] 13171 decisions 795 SAT calls 159.41 avg env size
c [sweep-16-1] 22205 variables remain 58% (15962 retained 42%)
c [decomp-52] removed 83 variables
c [sweep-16-1] removed 83 vars (0 failed, 28 eqs, 75 impls)
c [sweep-16] removed 83 vars in TOTAL (1 rounds, 818 queries)
c [phase-count-20] 254134 negative 99.7% of 254828 except 694 0.3%
c [phase-count-20] 175992 positive 69.1% of 254828 except 78836 30.9%
c [phase-count-20] skipping relative phase luck test
c [phase-20] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-20] sorted 4533 enqueued variables after 343642 conflicts
c [score-dist-20] active 33601 (88%), one 0 (0%), zero 4533 (12%)
c [score-dist-20] max exp 537, different 26 (5%)
c [score-dist-20] median active exp 528, avg 527.5
c [simplification-20] removed 258 variables 0.7% (38134 remain 15%)
c [simplification-20] removed 3638 irredundant clauses 1.4% (254828 remain 19%)
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 469259 (soft 427387 + delta 41872)
c [simplification-20] new conflict limit 427387 (hard 469259)
c 
c [simplification-21] limit 427387 conflicts (hard 469259) hit after 427387 conflicts
c [quatres-15] found 15958 quaternary clauses 46% in total
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 2 quaternary resolvents
c [ternres-16] limit 126873381 with penalty 0 = 0 + 0
c [ternres-16] all 38134 free variables schedulable
c [ternres-16] 99 ternary resolvents (1 bin, 98 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 3964793 penalty 4 = 4 + 0
c [card-6] found 3938 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 3964793 for elimination
c [card-6] 3938 out of 3938 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-53] removed 1 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 1574 sched 4%, 244 failed, 4 lifted, 11894 hbrs
c [decomp-54] removed 330 variables
c [basicprobe-7-1] 13398 sched 36%, 275 failed, 13 lifted, 48114 hbrs
c [decomp-55] removed 461 variables
c [basicprobe-7-2] 8195 probes remain 22% after last round
c [basicprobe-7-2] 609 units = 592 failed (97%) + 17 lifted (3%)
c [basicprobe-7-2] removed 879 variables, found 64541 hbrs
c [bate-5] eliminated 204 asymmetric tautologies during probing
c [unhide-21] limit 2500000 with penalty 3 = 0 + 3
c [unhide-21-30] 0 units, 4 failed, 51054 tauts, 0 hbrs, 367746 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 394 transitive binary clauses
c [bca-17] limit of 10000000 steps and 487629 added (scaled 2)
c [bca-17] 55115 out of 74492 literals actually usable 74%
c [bca-17] added 26 blocked clauses in 161260 steps
c [sweep-17] limit 38062014 penalty 0 = 0 + 0
c [sweep-17-1] 3104 pos 14.1% + 18892 neg 85.9% = 21996 sched 59.1% ret 15249
c [sweep-17-1] 38065818 steps 1138 queries 218.33 avg class size
c [sweep-17-1] 11483 decisions 1091 SAT calls 115.41 avg env size
c [sweep-17-1] 14059 variables remain 38% (23178 retained 62%)
c [decomp-56] removed 57 variables
c [sweep-17-1] removed 57 vars (0 failed, 52 eqs, 135 impls)
c [sweep-17] removed 57 vars in TOTAL (1 rounds, 1137 queries)
c [sort-queue-21] sorted 3876 enqueued variables after 427387 conflicts
c [score-dist-21] active 33312 (90%), one 0 (0%), zero 3876 (10%)
c [score-dist-21] max exp 538, different 27 (5%)
c [score-dist-21] median active exp 528, avg 527.9
c [simplification-21] removed 946 variables 2.5% (37188 remain 15%)
c [simplification-21] removed 12019 irredundant clauses 4.7% (242809 remain 18%)
c [simplification-21] maximum reduction of 5% = max (2%, 5%)
c [simplification-21] large reduction 5% >= 5% limit
c [simplification-21] next conflict interval 4273 = min (427387/100, 83745)
c [simplification-21] penalized conflict interval 4273 = 1 * 4273
c [simplification-21] hard conflict limit 441660 (soft 431660 + delta 10000)
c [simplification-21] new conflict limit 431660 (hard 441660)
c 
c [simplification-22] limit 431660 conflicts (hard 441660) hit after 431662 conflicts
c [quatres-16] found 15819 quaternary clauses 46% in total
c [quatres-16-2] added 1 single-self-subsuming ternary resolvents
c [quatres-16-2] added 1 quaternary resolvents
c [ternres-17] limit 127744789 with penalty 0 = 0 + 0
c [ternres-17] all 37188 free variables schedulable
c [ternres-17] 138 ternary resolvents (2 bin, 136 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-57] removed 2 variables
c [simpleprobe-8] all 37186 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-58] removed 148 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 148 variables, found 105657 hbrs, 38 units
c [unhide-22] limit 2500000 with penalty 3 = 0 + 3
c [unhide-22-31] 0 units, 9 failed, 94410 tauts, 0 hbrs, 78201 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 480 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 798404931 steps penalty 3 = 3 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 86
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 85
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 56
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 54
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 53
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 52
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 51
c [cce-8-1] eliminated 2 clauses out of 8 (25%) of length 50
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 49
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 48
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 47
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 46
c [cce-8-1] eliminated 6 clauses out of 7 (86%) of length 45
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 44
c [cce-8-1] eliminated 4 clauses out of 9 (44%) of length 43
c [cce-8-1] eliminated 6 clauses out of 9 (67%) of length 42
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 41
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 40
c [cce-8-1] eliminated 7 clauses out of 11 (64%) of length 39
c [cce-8-1] eliminated 5 clauses out of 10 (50%) of length 38
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 37
c [cce-8-1] eliminated 5 clauses out of 10 (50%) of length 36
c [cce-8-1] eliminated 7 clauses out of 11 (64%) of length 35
c [cce-8-1] eliminated 6 clauses out of 12 (50%) of length 34
c [cce-8-1] eliminated 9 clauses out of 15 (60%) of length 33
c [cce-8-1] eliminated 7 clauses out of 13 (54%) of length 32
c [cce-8-1] eliminated 8 clauses out of 12 (67%) of length 31
c [cce-8-1] eliminated 8 clauses out of 14 (57%) of length 30
c [cce-8-1] eliminated 11 clauses out of 16 (69%) of length 29
c [cce-8-1] eliminated 11 clauses out of 20 (55%) of length 28
c [cce-8-1] eliminated 14 clauses out of 20 (70%) of length 27
c [cce-8-1] eliminated 12 clauses out of 20 (60%) of length 26
c [cce-8-1] eliminated 12 clauses out of 19 (63%) of length 25
c [cce-8-1] eliminated 11 clauses out of 20 (55%) of length 24
c [cce-8-1] eliminated 11 clauses out of 20 (55%) of length 23
c [cce-8-1] eliminated 12 clauses out of 17 (71%) of length 22
c [cce-8-1] eliminated 10 clauses out of 24 (42%) of length 21
c [cce-8-1] eliminated 12 clauses out of 21 (57%) of length 20
c [cce-8-1] eliminated 12 clauses out of 21 (57%) of length 19
c [cce-8-1] eliminated 14 clauses out of 24 (58%) of length 18
c [cce-8-1] eliminated 15 clauses out of 28 (54%) of length 17
c [cce-8-1] eliminated 16 clauses out of 28 (57%) of length 16
c [cce-8-1] eliminated 19 clauses out of 36 (53%) of length 15
c [cce-8-1] eliminated 18 clauses out of 30 (60%) of length 14
c [cce-8-1] eliminated 18 clauses out of 34 (53%) of length 13
c [cce-8-1] eliminated 17 clauses out of 29 (59%) of length 12
c [cce-8-1] eliminated 23 clauses out of 38 (61%) of length 11
c [cce-8-1] eliminated 21 clauses out of 43 (49%) of length 10
c [cce-8-1] eliminated 23 clauses out of 49 (47%) of length 9
c [cce-8-1] eliminated 26 clauses out of 52 (50%) of length 8
c [cce-8-1] eliminated 31 clauses out of 123 (25%) of length 7
c [cce-8-1] eliminated 31 clauses out of 2933 (1%) of length 6
c [cce-8-1] eliminated 813 clauses out of 11108 (7%) of length 5
c [cce-8-1] eliminated 1632 clauses out of 15070 (11%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 2979 large clauses in 323733848 steps
c [cce-8-1] allowing another 161866924 steps for small clauses
c [cce-8-1] scheduling 198580 clauses = 143776 binary + 54804 ternary
c [cce-8-1] tried to eliminate 49650 small clauses 25%
c [cce-8-1] eliminated 6842 binary clauses 5%
c [cce-8-1] eliminated 1503 ternary clauses 3%
c [cce-8-1] eliminated 8345 small clauses 4%
c [cce-8-1] eliminated 8474 small clauses in 798404932 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 11453 covered clauses in round 1
c [cce-8] eliminated 11453 covered clauses in TOTAL during 1 rounds
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 36999 variables 100%
c [elim-17] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 820 variables 2% in round 1 in 19761295 steps
c [elim-17-1] backward subsumption/strengthening limit 19761200
c [elim-17-1-1] backward checking 5167 touched variables 14%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 2 and strengthened 29 clauses in 989033 steps
c [elim-17-1] rescheduled 84 variables 0% by backward subsumption
c [elim-17-2] eliminated 3 variables 0% in round 2 in 182456 steps
c [elim-17-2] backward subsumption/strengthening limit 182400
c [elim-17-2-1] backward checking 43 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 50610 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 823 = 2% variables out of 36999 scheduled
c [bca-18] limit of 10000000 steps and 461120 added (scaled 2)
c [bca-18] 53288 out of 72354 literals actually usable 74%
c [bca-18] added 22 blocked clauses in 148752 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 2008 pos 14.9% + 11486 neg 85.1% = 13494 sched 37.3% ret 22682
c [sweep-18-1] 108762484 steps 4153 queries 36.07 avg class size
c [sweep-18-1] 32492 decisions 3980 SAT calls 83.79 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-59] removed 179 variables
c [sweep-18-1] removed 179 vars (0 failed, 179 eqs, 564 impls)
c [sweep-18-2] 4159 pos 11.6% + 31838 neg 88.4% = 35997 sched 100.0% ret 0
c [sweep-18-2] 160730073 steps 5312 queries 62.84 avg class size
c [sweep-18-2] 51230 decisions 5172 SAT calls 96.95 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-60] removed 246 variables
c [sweep-18-2] removed 246 vars (0 failed, 158 eqs, 536 impls)
c [sweep-18-3] 4155 pos 11.6% + 31596 neg 88.4% = 35751 sched 100.0% ret 0
c [sweep-18-3] 157931628 steps 5215 queries 57.99 avg class size
c [sweep-18-3] 50051 decisions 5160 SAT calls 92.42 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-61] removed 114 variables
c [sweep-18-3] removed 114 vars (0 failed, 72 eqs, 354 impls)
c [sweep-18] removed 539 vars in TOTAL (3 rounds, 14677 queries)
c [sort-queue-22] sorted 3229 enqueued variables after 431662 conflicts
c [score-dist-22] active 32408 (91%), one 0 (0%), zero 3229 (9%)
c [score-dist-22] max exp 538, different 26 (5%)
c [score-dist-22] median active exp 528, avg 528.1
c [simplification-22] removed 1551 variables 4.2% (35637 remain 14%)
c [simplification-22] removed 15669 irredundant clauses 6.5% (227140 remain 17%)
c [simplification-22] maximum reduction of 6% = max (4%, 6%)
c [simplification-22] large reduction 6% >= 5% limit
c [simplification-22] next conflict interval 4316 = min (431662/100, 83745)
c [simplification-22] penalized conflict interval 4316 = 1 * 4316
c [simplification-22] hard conflict limit 445978 (soft 435978 + delta 10000)
c [simplification-22] new conflict limit 435978 (hard 445978)
c 
c [simplification-23] limit 435978 conflicts (hard 445978) hit after 440178 conflicts
c [quatres-17] found 14148 quaternary clauses 43% in total
c [quatres-17-2] added 7 single-self-subsuming ternary resolvents
c [quatres-17-2] added 2 quaternary resolvents
c [ternres-18] limit 129619605 with penalty 0 = 0 + 0
c [ternres-18] all 35637 free variables schedulable
c [ternres-18] 310 ternary resolvents (2 bin, 308 trn)
c [ternres-18] fully completed ternary resolution
c [unhide-23] limit 5000000 with penalty 2 = 0 + 2
c [unhide-23-34] 1 units, 29 failed, 86265 tauts, 0 hbrs, 307223 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 465 transitive binary clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 35611 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 139 variables 0% in round 1 in 18842487 steps
c [elim-18-1] backward subsumption/strengthening limit 18842400
c [elim-18-1-1] backward checking 1195 touched variables 3%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 0 and strengthened 1 clauses in 260011 steps
c [elim-18-1] rescheduled 4 variables 0% by backward subsumption
c [elim-18-2] no variable eliminated in round 2 in 1114 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 139 = 0% variables out of 35611 scheduled
c [elim-18] 139 < 1/100 * 35611 = 356 considered unsuccessful
c [bca-19] limit of 10000000 steps and 450227 added (scaled 2)
c [bca-19] 49373 out of 70946 literals actually usable 70%
c [bca-19] added 7 blocked clauses in 141875 steps
c [sweep-19] limit 38885881 penalty 0 = 0 + 0
c [sweep-19-1] 4170 pos 11.8% + 31302 neg 88.2% = 35472 sched 100.0% ret 0
c [sweep-19-1] 38904915 steps 1047 queries 287.43 avg class size
c [sweep-19-1] 18246 decisions 1035 SAT calls 159.61 avg env size
c [sweep-19-1] 18717 variables remain 53% (16736 retained 47%)
c [decomp-63] removed 30 variables
c [sweep-19-1] removed 30 vars (0 failed, 14 eqs, 90 impls)
c [sweep-19] 30 < 1/1000 * 35472 = 35 considered unsuccessful
c [sweep-19] removed 30 vars in TOTAL (1 rounds, 1046 queries)
c [sort-queue-23] sorted 3106 enqueued variables after 440178 conflicts
c [score-dist-23] active 32336 (91%), one 0 (0%), zero 3106 (9%)
c [score-dist-23] max exp 538, different 26 (5%)
c [score-dist-23] median active exp 528, avg 528.1
c [simplification-23] removed 195 variables 0.5% (35442 remain 14%)
c [simplification-23] removed 3121 irredundant clauses 1.4% (224019 remain 16%)
c [simplification-23] maximum reduction of 1% = max (1%, 1%)
c [simplification-23] geometric conflict interval increment 41872 = 83745 / 2
c [simplification-23] new conflict interval 125617
c [simplification-23] penalized conflict interval 125617 = 1 * 125617
c [simplification-23] hard conflict limit 628603 (soft 565795 + delta 62808)
c [simplification-23] new conflict limit 565795 (hard 628603)
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  949.5   35441   224019    451643   39064   6066 448709  558   614  144  91%    706  -10  540  570   95%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2842 basic ate = 2800 trn 99% + 42 lrg 1% in 5 updates
c bcas: 19 count, 2401 added (3667 skipped), 5795902 steps
c bkwd: tried 475206 clauses, 950155 lits, 2.00 lits/clause
c bkwd: checked 14579448 occs, 30.68 occs/clause, 15.34 occs/lit
c bkwd: subsumed 16 binary, 65 ternary, 15 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1125 large (0% self)
c blkd: 6 bces, 13285 removed, 10020108 resolutions, 27843576 steps
c blkd: 16555 blocking literals 3%, 8 pure
c bump: 502078 bumped seen, 927771029 lits 1847.9 on average
c card: 6 count, 0 units, 0 am1, 341125824 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 85821 subsumed
c card: 25046 at-most-one constraints found, average size 4.58
c card: 25046 at-most-one constraints used 100%, average size 4.58
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: 8 cces, 76829 eliminated, 76439 ate 99%, 390 abce 1%
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: 4740073 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 178 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 63 decompositions, 10931 equivalent 4%
c deco: 380782 decision-only clauses 76%, 56% reduction
c decs: 7888671 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 18 elims, 108485 eliminated 42%, 219 pure 0%
c elms: 49 rounds, 2.7 rounds/bve
c elms: 85937 small 79%, 22321 large 21%
c elms: 248320 tried small, 85937 succeeded 35%, 162383 failed 65%
c elms: 47816 subsumed, 71395 strengthened, 1459 blocked
c elms: 24632925 copies, 24457960 resolutions, 6749183 ipos
c elms: 6978108 subchks, 4627591 strchks
c gaus: 5 extractions, 192 extracted, 2.6 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13404020 steps, 6702010 extr 50%, 986 elim 0%
c glue: 640.4 orig avg, 640.4 real avg, 12.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2209163 = 710922 simple 32% + 1427971 trn 65% + 70270 lrg 3%, 4733 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 502078 clauses, 727.0 length
c lrnd: 365005261 lits = 726260845 orig - 361255584 removed 50%
c lrnd: 207726 uips 41%, 263078 flips 52%
c mins: 50528 mins 12%, 1993 bin 0%, 2768 size 1%
c mins: 23521791 poisoned searches, 6218886 hits, 26% hit rate
c mins: 28188986 used twice searches, 2558891 hits, 9% hit rate
c move: moved 45808, 32461 bin 71%, 13347 trn 29%
c otfs: 3707 driving 37%, 6385 restarting 63%
c otfs: str 10092, 9936 red 98%, 156 irr 2%
c otfs: str 10092, 0 bin 0%, 106 trn 1%, 9986 lrg 99%
c otfs: sub 21, 21 red 100%, 0 irr 0%
c otfs: sub 21, 0 bin 0%, 0 trn 0%, 21 lrg 100%
c phas: 20 computed, 183204 set, 174 pos (0%), 183030 neg (100%)
c prbs: 7 basic, 111091 probed, 4231 failed, 158 lifted
c prbs: 8 simple, 1007014 probed, 2253 failed, 1200 eqs
c prbs: 7 treelook, 575 probed, 25 failed, 0 lifted
c prom: 0 locked 0% out of 790718 tried
c prps: 2263693878 props, 266 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 17 count, 67 quat, 20 self1, 1 self2, 1640 dup
c queu: 23 sorted, 7888671 next (38296 steps 0.00)
c queu: 928875281 enq (1910069520 steps 2.06), 927771029 deq 100%
c redc: 1987 clauses 21%, 9475 tried 2%, 75 sat 1%
c redc: 4610 lits 6%, 81308 tried 0%, 75 sat 0%
c redc: 237 times jump level reduced, 154.8 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 57710 removed, 15396 red 27%
c rsts: 6238 restarts 79%, 1640 skipped 21%
c rsts: 1640 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 23 count, 21 confs 91%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 502078 count (797948 tried 1.6), 359231 sub out of 496961 (72.3%)
c swps: 19 count, 22 rounds, 27238 queries (1238.1/round)
c swps: 25671 sat calls, 285 unsat (0.3% success rate)
c swps: 248288 decisions 9.7, 7599 conflicts 0.3
c swps; 277.0 avg class size, 97.0 avg environment size
c swps: 1 failed, 3970 impls, 1784 equivs
c swp0: 9073 type 0 queries, 4129 unsat (45.5%), 8588 sat (94.7%)
c swp1: 18165 type 1 queries, 9555 unsat (52.6%), 16866 sat (92.8%)
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: 16782127 calls to obtain time
c tops: 104401 fixed 40%, 198 its, 2516.10 confs/it
c trds: 19 transitive reductions, 6705 removed, 41 failed
c trds: 30249 nodes, 92470 edges, 37738810 steps
c trim: 3458647 words, 13.2 MB
c trnr: 18 count, 13 bin, 5463 trn, 167890997 steps
c unhd: 23 count, 34 rounds, 100522041 steps
c unhd: 1203 non-trivial sccs of average size 2.2
c unhd: 134 units, 132 bin, 2 trn, 0 lrg
c unhd: 11094 failed, 11025 stamp, 0 lits, 41 bin, 7 trn, 0 lrg
c unhd: 1217303 tauts, 18492 bin 2%, 13729 trn 1%, 242 lrg 0%
c unhd: 1217303 tauts, 1184840 stamp 97%, 1126491 red 93%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6504777 str, 132 bin 0%, 3249 trn 0%, 6501396 lrg 100%, 6483957 red 100%
c vars: 35441 remaining 14% and 223817 removed 86% out of 259258
c vars: 104401 fixed 40%, 108485 eliminated 42%, 10931 equivalent 4%
c vsts: 15833770458 visits, 89% srch, 11% simp, 0% lkhd
c vsts: 6.7 search visits per propagation, 28343.4 per conflict
c wchs: 971628944 pushed, 69585534 enlarged, 264 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         497028             0             0      46817682      12248409        267518
c 
c  0 0          8209   2         0   0<        0   0< 12431875  27   1625894  13     19519   7     0.3
c  1 5          1193   0         0   0         0   0   1850932   4    238081   2      2818   1     0.1
c  2 6          2306   0         0   0         0   0   3091520   7    498636   4      8600   3     0.2
c  3 9          3080   1         0   0         0   0   4337559   9    937075   8     13618   5     0.5
c  4 14         3634   1         0   0         0   0   3664925   8   1132893   9     12768   5     1.6
c  5 21         3176   1         0   0         0   0   2790894   6<   825806   7      8481   3     1.9
c  6 30         3308   1         0   0         0   0   2600600   6    765221   6     12377   5     1.2
c  7 41         3596   1         0   0         0   0   1850721   4    487782   4<    13612   5     1.8
c  8 54         3882   1         0   0         0   0   1264546   3    404020   3     10130   4     2.5
c  9 69         3092   1         0   0         0   0   1094946   2    347418   3      7962   3<    2.3
c 10 86         5907   1         0   0         0   0   2019045   4    665288   5     19323   7     4.9
c 11 126       13200   3         0   0         0   0   4614191  10   1862510  15     38691  14    10.6
c 12 230       65964  13<        0   0         0   0   4141842   9   1825465  15     70040  26    66.1
c 13 534      369719  74         0   0         0   0   1051072   2    625621   5     29151  11   212.5
c 14 1526       6762   1         0   0         0   0     13014   0      6699   0       428   0    30.7
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                 12.2           0.0           0.0           5.0           6.9           8.7
c std                  2.4           0.0           0.0           4.4           4.4           4.1
c 
c  191.996  19% bump
c   78.675   8% unhide
c   64.482   6% cce
c   57.946   6% probe
c   46.262   5% sweep
c   23.361   2% elim
c    4.892   0% bca
c 
c   14.575 < 1% rest (below)
c 
c    4.813   0% decide
c    3.452   0% block
c    2.137   0% transred
c    1.726   0% gauss
c    1.291   0% ternres
c    0.676   0% quatres
c    0.481   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.133   1% preprocessing     2%
c  298.110  30% inprocessing     98%
c ==================================
c  303.243  30% simplifying
c  696.029  70% search
c ==================================
c  999.276 100% all
c 
c        498187 conflicts,         498.5 confs/sec
c          1119 ternaries,         445.2 confs/ternary
c          1518 binaries,          328.2 confs/binary
c           198 iterations,       2516.1 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          6238 restarts,            6.2 rests/sec,     79.9 confs/restart
c       7888671 decisions,        7894.4 decis/sec,     15.8 decis/conflict
c    2263693878 propagations,  2265333.5 props/sec,    287.0 props/decision
c 
c 999.3 seconds, 473.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
