c launch: /data/cnf/sc2014/app/manol-pipe-c10nidw.cnf.bz2
c host: atom09
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/manol-pipe-c10nidw.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-c10nidw.cnf.bz2
c no embedded options
c found 'p cnf 433601 1291714' header
c read 433601 variables, 1291714 clauses, 3013998 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 433600 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  433600  1291713         0       0      0     0    0     0   73   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 2 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 433600 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 506 variables
c [simpleprobe-1] 181013 variables remain 42% (252081 retained 58%)
c [simpleprobe-1] removed 506 variables, found 1058 hbrs, 10 units
c [unhide-1] limit 80637 based on 1290202 irredundant clauses
c [unhide-1-1] 0 units, 64 failed, 105 tauts, 0 hbrs, 114 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 431402 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 189604 not tried 44% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 241798 = 56% variables out of 431402 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 744044 negative 95.9% of 775692 except 31648 4.1%
c [phase-count-1] 716116 positive 92.3% of 775692 except 59576 7.7%
c [phase-1] phase bias: 59937 positive 32%, 129667 negative 68%
c [sort-queue-1] sorted 189604 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 189604 (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 243996 variables 56.3% (189604 remain 44%)
c [simplification-1] removed 516021 irredundant clauses 39.9% (775692 remain 60%)
c [simplification-1] maximum reduction of 56% = max (56%, 40%)
c [simplification-1] large reduction 56% >= 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    7.6  189603   775692         1       0      0   154    0     0   66   0%      0    0    0    0    0%
c i    7.6  189477   775692        22      13      3   157    0     0   67   3%      0    0    0    0 24672%
c i    8.2  189444   775692       368     311     21   167    1    15   69   4%      1   15    6    0 14881%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1010 conflicts
c [decomp-3] removed 625 variables
c [simpleprobe-2] 78809 schedulable variables 42%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 2 variables
c [simpleprobe-2] 78841 variables remain 42% (110136 retained 58%)
c [simpleprobe-2] removed 2 variables, found 30 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 46512 literals 12%
c [treelook-1] scheduling used 300115 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 315665 steps
c [treelook-1] 46411 literals remain 12%
c [treelook-1] 45379 variables remain to probed next time 24%
c [treelook-1] removed 0 variables, found 489 hbrs
c [basicprobe-1] limit 6185008 based on 773126 irredundant clauses
c [basicprobe-1-0] 141402 probes remain 76% after last round
c [basicprobe-1-0] 471 units = 97 failed (21%) + 374 lifted (79%)
c [basicprobe-1-0] removed 2531 variables, found 5909 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 10 units, 33 failed, 341 tauts, 0 hbrs, 2897 literals
c [elim-2] 186352 variables 100% will be scheduled this time
c [elim-2] scheduled 186352 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 76681 not tried 41% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 109660 = 59% variables out of 186352 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 476110 negative 97.4% of 488749 except 12639 2.6%
c [phase-count-2] 469451 positive 96.1% of 488749 except 19298 3.9%
c [phase-2] phase bias: 23 positive 21%, 86 negative 79%
c [sort-queue-2] sorted 68952 enqueued variables after 1010 conflicts
c [score-dist-2] active 7740 (10%), one 0 (0%), zero 68952 (90%)
c [score-dist-2] max exp 518, different 17 (3%)
c [score-dist-2] median active exp 512, avg 511.5
c [simplification-2] removed 112698 variables 59.5% (76692 remain 18%)
c [simplification-2] removed 286943 irredundant clauses 37.0% (488749 remain 38%)
c [simplification-2] maximum reduction of 60% = max (60%, 37%)
c [simplification-2] large reduction 60% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13010 (soft 3010 + delta 10000)
c [simplification-2] new conflict limit 3010 (hard 13010)
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   15.9   76691   488749      2911    1588     61  1104    6    82   61   7%     25   80   13    0 2792%
c 
c [simplification-3] limit 3010 conflicts (hard 13010) hit after 3011 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 40 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 40 out of 40 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 141 variables
c [unhide-3] limit 141561 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 9 failed, 943 tauts, 0 hbrs, 4200 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 76495 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 21560 not tried 28% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 14227 = 19% variables out of 76495 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 447690 negative 97.3% of 460097 except 12407 2.7%
c [phase-count-3] 445560 positive 96.8% of 460097 except 14537 3.2%
c [phase-3] phase bias: 6 positive 12%, 44 negative 88%
c [sort-queue-3] sorted 53646 enqueued variables after 3011 conflicts
c [score-dist-3] active 8622 (14%), one 0 (0%), zero 53646 (86%)
c [score-dist-3] max exp 521, different 19 (4%)
c [score-dist-3] median active exp 513, avg 513.2
c [simplification-3] removed 14421 variables 18.8% (62268 remain 14%)
c [simplification-3] removed 28652 irredundant clauses 5.9% (460097 remain 36%)
c [simplification-3] maximum reduction of 19% = max (19%, 6%)
c [simplification-3] large reduction 19% >= 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 15011 (soft 5011 + delta 10000)
c [simplification-3] new conflict limit 5011 (hard 15011)
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   19.3   62267   460097      3500    1362     75   616    8    91   61   9%     16   88   28    1 4109%
c i   19.7   62264   460097      4568    2190    105   622   10   118   61   9%     11  113   13    1 1360%
c 
c [simplification-4] limit 5011 conflicts (hard 15011) hit after 5013 conflicts
c [decomp-7] removed 78 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 11039 literals 9%
c [treelook-2] scheduling used 150633 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 164638 steps
c [treelook-2] 10988 literals remain 9%
c [treelook-2] 6798 variables remain to probed next time 11%
c [treelook-2] removed 0 variables, found 59 hbrs
c [unhide-4] limit 176624 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 9 failed, 16 tauts, 0 hbrs, 6903 literals
c [elim-4] 21486 variables 35% will be scheduled this time
c [elim-4] scheduled 21486 variables 35%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1716 variables 3% in round 1 in 290263424 steps
c [elim-4-1] backward subsumption/strengthening limit 109736576
c [elim-4-1-1] backward checking 13264 touched variables 21%
c [elim-4-1-1] incomplete backward checking 13065 remain 98%
c [elim-4-1] subsumed 973 and strengthened 1804 clauses in 109738095 steps
c [elim-4] incomplete 1456 not tried 2% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 1719 = 8% variables out of 21486 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 439586 negative 97.3% of 451879 except 12293 2.7%
c [phase-count-4] 439024 positive 97.2% of 451879 except 12855 2.8%
c [phase-4] phase bias: 8 positive 100%, 0 negative 0%
c [sort-queue-4] sorted 49450 enqueued variables after 5013 conflicts
c [score-dist-4] active 10959 (18%), one 0 (0%), zero 49450 (82%)
c [score-dist-4] max exp 522, different 20 (4%)
c [score-dist-4] median active exp 514, avg 514.3
c [simplification-4] removed 1833 variables 2.9% (60409 remain 14%)
c [simplification-4] removed 8218 irredundant clauses 1.8% (451879 remain 35%)
c [simplification-4] maximum reduction of 3% = max (3%, 2%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 5000
c [simplification-4] penalized conflict interval 5000 = 1 * 5000
c [simplification-4] hard conflict limit 20013 (soft 10013 + delta 10000)
c [simplification-4] new conflict limit 10013 (hard 20013)
c 
c [simplification-5] limit 10013 conflicts (hard 20013) hit after 10015 conflicts
c [quatres-1] found 40273 quaternary clauses 18% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 588 single-self-subsuming ternary resolvents
c [quatres-1-2] added 6534 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 60409 free variables schedulable
c [ternres-1] 6591 ternary resolvents (37 bin, 6554 trn)
c [ternres-1] 1557 variables remain 3% (58852 retained 97%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 16149 xors of average arity 3.0
c [gauss-1] connected 48440 occurrences of 8933 variables (average 5.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 7 variables
c [basicprobe-2] limit 8805695 penalty 0 = 0 + 0
c [basicprobe-2-0] 31563 sched 54%, 245 failed, 23 lifted, 3966 hbrs
c [decomp-10] removed 1886 variables
c [basicprobe-2-1] 17193 probes remain 29% after last round
c [basicprobe-2-1] 284 units = 261 failed (92%) + 23 lifted (8%)
c [basicprobe-2-1] removed 1949 variables, found 4480 hbrs
c [bate-1] eliminated 256 asymmetric tautologies during probing
c [unhide-5] limit 352227 with penalty 0 = 0 + 0
c [unhide-5-5] 2 units, 1 failed, 1574 tauts, 0 hbrs, 8630 literals
c [transred-1] limit 1761139 with penalty 0 = 0 + 0
c [transred-1] removed 291 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 58449 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 12287 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 63 (2%) of length 29
c [cce-1-1] eliminated 1 clauses out of 58 (2%) of length 28
c [cce-1-1] eliminated 4 clauses out of 152 (3%) of length 27
c [cce-1-1] eliminated 16 clauses out of 86 (19%) of length 26
c [cce-1-1] eliminated 4 clauses out of 122 (3%) of length 25
c [cce-1-1] eliminated 2 clauses out of 257 (1%) of length 24
c [cce-1-1] eliminated 10 clauses out of 181 (6%) of length 23
c [cce-1-1] eliminated 8 clauses out of 262 (3%) of length 22
c [cce-1-1] eliminated 17 clauses out of 235 (7%) of length 21
c [cce-1-1] eliminated 26 clauses out of 272 (10%) of length 20
c [cce-1-1] eliminated 15 clauses out of 412 (4%) of length 19
c [cce-1-1] eliminated 30 clauses out of 608 (5%) of length 18
c [cce-1-1] eliminated 35 clauses out of 620 (6%) of length 17
c [cce-1-1] eliminated 37 clauses out of 774 (5%) of length 16
c [cce-1-1] eliminated 101 clauses out of 882 (11%) of length 15
c [cce-1-1] eliminated 101 clauses out of 942 (11%) of length 14
c [cce-1-1] eliminated 125 clauses out of 1240 (10%) of length 13
c [cce-1-1] eliminated 173 clauses out of 2141 (8%) of length 12
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 706 large clauses in 30000056 steps
c [cce-1-1] allowing another 15000028 steps for small clauses
c [cce-1-1] scheduling 142177 clauses = 54658 binary + 87519 ternary
c [cce-1-1] tried to eliminate 12945 small clauses 9%
c [cce-1-1] eliminated 91 binary clauses 0%
c [cce-1-1] eliminated 65 ternary clauses 0%
c [cce-1-1] eliminated 156 small clauses 0%
c [cce-1-1] eliminated 156 small clauses in 30000071 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 862 covered clauses in round 1
c [cce-1] eliminated 862 covered clauses in TOTAL during 1 rounds
c [cce-1] 862 < 1/100 * 412957 = 4129 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 57444 variables 100%
c [elim-5] limit of 35222782 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 5129 not tried 9% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3684 = 6% variables out of 57444 scheduled
c [bca-1] limit of 10000000 steps and 804550 added (scaled 2)
c [bca-1] 93748 out of 107522 literals actually usable 87%
c [bca-1] added 443 blocked clauses in 290817 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 18769 pos 34.9% + 34991 neg 65.1% = 53760 sched 100.0% ret 0
c [sweep-1-1] 1021118 steps 71 queries 10193.11 avg class size
c [sweep-1-1] 2670 decisions 70 SAT calls 67.50 avg env size
c [sweep-1-1] 52940 variables remain 98% (820 retained 2%)
c [decomp-11] removed 9 variables
c [sweep-1-1] removed 9 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 9 vars in TOTAL (1 rounds, 70 queries)
c [sort-queue-5] sorted 39037 enqueued variables after 10015 conflicts
c [score-dist-5] active 14714 (27%), one 0 (0%), zero 39037 (73%)
c [score-dist-5] max exp 524, different 21 (4%)
c [score-dist-5] median active exp 516, avg 516.1
c [simplification-5] removed 6658 variables 11.0% (53751 remain 12%)
c [simplification-5] removed 49978 irredundant clauses 11.1% (401901 remain 31%)
c [simplification-5] maximum reduction of 11% = max (11%, 11%)
c [simplification-5] large reduction 11% >= 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 22015 (soft 12015 + delta 10000)
c [simplification-5] new conflict limit 12015 (hard 22015)
c 
c [simplification-6] limit 12015 conflicts (hard 22015) hit after 12015 conflicts
c [quatres-2] found 41767 quaternary clauses 20% in total
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1035 single-self-subsuming ternary resolvents
c [quatres-2-2] added 3930 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1423 schedulable variables 3%
c [ternres-2] 3007 ternary resolvents (88 bin, 2919 trn)
c [ternres-2] 876 variables remain 2% (52875 retained 98%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 157 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 157 out of 157 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 7 variables
c [simpleprobe-3] 22384 schedulable variables 42%
c [simpleprobe-3] limit 7780940 penalty 0 = 0 + 0
c [decomp-13] removed 4 variables
c [simpleprobe-3] 22434 variables remain 42% (31306 retained 58%)
c [simpleprobe-3] removed 4 variables, found 62 hbrs, 0 units
c [unhide-6] limit 389047 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 4 failed, 440 tauts, 0 hbrs, 5862 literals
c [transred-2] limit 1945235 with penalty 0 = 0 + 0
c [transred-2] removed 88 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 53732 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 981 blocked clauses
c [block-2] 981 < 1/100 * 401807 = 4018 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 53588 variables 100%
c [elim-6] limit of 38904704 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 4584 not tried 9% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 210 = 0% variables out of 53588 scheduled
c [elim-6] 210 < 1/100 * 53588 = 535 considered unsuccessful
c [bca-2] limit of 10000000 steps and 801241 added (scaled 2)
c [bca-2] 91029 out of 106758 literals actually usable 85%
c [bca-2] added 4 blocked clauses in 287175 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 18864 pos 35.9% + 33701 neg 64.1% = 52565 sched 98.5% ret 813
c [sweep-2-1] 1001650 steps 75 queries 11591.17 avg class size
c [sweep-2-1] 2981 decisions 74 SAT calls 85.47 avg env size
c [sweep-2-1] 51807 variables remain 97% (1566 retained 3%)
c [decomp-14] removed 9 variables
c [sweep-2-1] removed 9 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 9 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-6] sorted 38617 enqueued variables after 12015 conflicts
c [score-dist-6] active 14752 (28%), one 0 (0%), zero 38617 (72%)
c [score-dist-6] max exp 525, different 22 (4%)
c [score-dist-6] median active exp 516, avg 516.3
c [simplification-6] removed 382 variables 0.7% (53369 remain 12%)
c [simplification-6] removed 1833 irredundant clauses 0.5% (400068 remain 31%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 15000
c [simplification-6] penalized conflict interval 15000 = 1 * 15000
c [simplification-6] hard conflict limit 37015 (soft 27015 + delta 10000)
c [simplification-6] new conflict limit 27015 (hard 37015)
c 
c [simplification-7] limit 27015 conflicts (hard 37015) hit after 27017 conflicts
c [quatres-3] found 44744 quaternary clauses 22% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 215 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1062 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 855 schedulable variables 2%
c [ternres-3] 4000 ternary resolvents (126 bin, 3874 trn)
c [ternres-3] 126 variables remain 0% (53243 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 8335 xors of average arity 3.0
c [gauss-2] connected 25004 occurrences of 5880 variables (average 4.3)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 6 variables
c [unhide-7] limit 652004 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 1 failed, 347 tauts, 0 hbrs, 20049 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 68 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 68 (1%) of length 29
c [cce-2-1] eliminated 1 clauses out of 83 (1%) of length 26
c [cce-2-1] eliminated 2 clauses out of 183 (1%) of length 23
c [cce-2-1] eliminated 3 clauses out of 280 (1%) of length 22
c [cce-2-1] eliminated 7 clauses out of 257 (3%) of length 21
c [cce-2-1] eliminated 5 clauses out of 289 (2%) of length 20
c [cce-2-1] eliminated 4 clauses out of 455 (1%) of length 19
c [cce-2-1] eliminated 19 clauses out of 717 (3%) of length 18
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 42 large clauses in 15000110 steps
c [cce-2-1] allowing another 7500055 steps for small clauses
c [cce-2-1] scheduling 121114 clauses = 50670 binary + 70444 ternary
c [cce-2-1] tried to eliminate 4681 small clauses 4%
c [cce-2-1] eliminated 11 binary clauses 0%
c [cce-2-1] eliminated 30 ternary clauses 0%
c [cce-2-1] eliminated 41 small clauses 0%
c [cce-2-1] eliminated 78 small clauses in 15000806 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 120 covered clauses in round 1
c [cce-2] eliminated 120 covered clauses in TOTAL during 1 rounds
c [cce-2] 120 < 1/100 * 399810 = 3998 considered unsuccessful
c [bca-3] limit of 10000000 steps and 800103 added (scaled 2)
c [bca-3] 89703 out of 106726 literals actually usable 84%
c [bca-3] added 7 blocked clauses in 295669 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 18721 pos 36.1% + 33077 neg 63.9% = 51798 sched 97.1% ret 1564
c [sweep-3-1] 1005304 steps 85 queries 12229.46 avg class size
c [sweep-3-1] 2771 decisions 84 SAT calls 67.85 avg env size
c [sweep-3-1] 49387 variables remain 93% (3975 retained 7%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 84 queries)
c [sort-queue-7] sorted 38267 enqueued variables after 27017 conflicts
c [score-dist-7] active 15095 (28%), one 0 (0%), zero 38267 (72%)
c [score-dist-7] max exp 528, different 25 (5%)
c [score-dist-7] median active exp 516, avg 517.2
c [simplification-7] removed 7 variables 0.0% (53362 remain 12%)
c [simplification-7] removed 378 irredundant clauses 0.1% (399690 remain 31%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 35000
c [simplification-7] penalized conflict interval 35000 = 1 * 35000
c [simplification-7] hard conflict limit 79517 (soft 62017 + delta 17500)
c [simplification-7] new conflict limit 62017 (hard 79517)
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 -   56.1   53362   399690     70622   33447  14582  3038   40    50   64  81%    644  -10   42   24  177%
c 
c [simplification-8] limit 62017 conflicts (hard 79517) hit after 79517 conflicts
c [quatres-4] found 45596 quaternary clauses 22% in total
c [quatres-4-2] added 57 single-self-subsuming ternary resolvents
c [quatres-4-2] added 458 quaternary resolvents
c [ternres-4] limit 6360402 with penalty 0 = 0 + 0
c [ternres-4] 126 schedulable variables 0%
c [ternres-4] 5700 ternary resolvents (55 bin, 5645 trn)
c [ternres-4] 9 variables remain 0% (53353 retained 100%)
c [decomp-17] removed 1 variables
c [unhide-8] limit 1272080 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 1 failed, 846 tauts, 0 hbrs, 31213 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 46 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 53359 variables 100%
c [block-3] limit of 31802010 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 11 blocked clauses
c [block-3] 11 < 1/100 * 399686 = 3996 considered unsuccessful
c [elim-7] 4579 variables 9% will be scheduled this time
c [elim-7] scheduled 4579 variables 9%
c [elim-7] limit of 63604021 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 2078 not tried 4% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 0 = 0% variables out of 4579 scheduled
c [bca-4] limit of 10000000 steps and 799799 added (scaled 2)
c [bca-4] 90436 out of 106720 literals actually usable 85%
c [bca-4] added 13 blocked clauses in 311640 steps
c [sweep-4] limit 1908120 penalty 0 = 0 + 0
c [sweep-4-1] 18610 pos 37.7% + 30774 neg 62.3% = 49384 sched 92.6% ret 3975
c [sweep-4-1] 1957636 steps 161 queries 10500.51 avg class size
c [sweep-4-1] 4714 decisions 161 SAT calls 48.45 avg env size
c [sweep-4-1] 47349 variables remain 89% (6007 retained 11%)
c [decomp-18] removed 7 variables
c [sweep-4-1] removed 7 vars (0 failed, 1 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 7 vars in TOTAL (1 rounds, 160 queries)
c [sort-queue-8] sorted 38144 enqueued variables after 79517 conflicts
c [score-dist-8] active 15208 (29%), one 0 (0%), zero 38144 (71%)
c [score-dist-8] max exp 533, different 30 (6%)
c [score-dist-8] median active exp 516, avg 517.8
c [simplification-8] removed 10 variables 0.0% (53352 remain 12%)
c [simplification-8] removed 209 irredundant clauses 0.1% (399481 remain 31%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 35000
c [simplification-8] new conflict interval 70000
c [simplification-8] penalized conflict interval 70000 = 1 * 70000
c [simplification-8] hard conflict limit 184517 (soft 149517 + delta 35000)
c [simplification-8] new conflict limit 149517 (hard 184517)
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 -   65.4   53352   399481    108578   35950  19647  3143   37    61   65  62%    811    2   42   31  137%
c -   71.5   53352   399481    144358   37483  19698  3145   34    49   66  71%    901   -8   34   33  105%
c 
c [simplification-9] limit 149517 conflicts (hard 184517) hit after 153565 conflicts
c [quatres-5] found 46054 quaternary clauses 22% in total
c [quatres-5-1] added 3 double-self-subsuming ternary resolvents
c [quatres-5-2] added 113 single-self-subsuming ternary resolvents
c [quatres-5-2] added 471 quaternary resolvents
c [ternres-5] limit 11450017 with penalty 0 = 0 + 0
c [ternres-5] 9 schedulable variables 0%
c [ternres-5] 5022 ternary resolvents (112 bin, 4910 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-19] removed 3 variables
c [treelook-3] limit 286250 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 8280 literals 8%
c [treelook-3] scheduling used 286279 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 286250 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 287044 steps
c [treelook-3] 8255 literals remain 8%
c [treelook-3] 3302 variables remain to probed next time 6%
c [treelook-3] removed 0 variables, found 375 hbrs
c [unhide-9] limit 2290003 with penalty 0 = 0 + 0
c [unhide-9-9] 0 units, 0 failed, 889 tauts, 0 hbrs, 24340 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 90 transitive binary clauses
c [bca-5] limit of 10000000 steps and 798613 added (scaled 2)
c [bca-5] 90298 out of 106700 literals actually usable 85%
c [bca-5] added 2 blocked clauses in 314949 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 34350050 penalty 0 = 0 + 0
c [sweep-5-1] 17364 pos 36.7% + 29979 neg 63.3% = 47343 sched 88.7% ret 6006
c [sweep-5-1] 34356794 steps 3584 queries 1333.48 avg class size
c [sweep-5-1] 58565 decisions 3567 SAT calls 24.58 avg env size
c [sweep-5-1] 17021 variables remain 32% (36327 retained 68%)
c [decomp-21] removed 105 variables
c [sweep-5-1] removed 105 vars (0 failed, 72 eqs, 59 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 105 vars in TOTAL (1 rounds, 3583 queries)
c [sort-queue-9] sorted 37348 enqueued variables after 153565 conflicts
c [score-dist-9] active 15896 (30%), one 0 (0%), zero 37348 (70%)
c [score-dist-9] max exp 535, different 32 (6%)
c [score-dist-9] median active exp 517, avg 518.6
c [simplification-9] removed 108 variables 0.2% (53244 remain 12%)
c [simplification-9] removed 1421 irredundant clauses 0.4% (398060 remain 31%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 70000
c [simplification-9] new conflict interval 140000
c [simplification-9] penalized conflict interval 140000 = 1 * 140000
c [simplification-9] hard conflict limit 363565 (soft 293565 + delta 70000)
c [simplification-9] new conflict limit 293565 (hard 363565)
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 -   80.8   53244   398060    185929   36271  22106  4025   13   316   65   4%    959  170   14   25   54%
c i   82.3   53243   398060    219161   56835  22113  4032    7   346   74   2%    985  132    5   19   27%
c i   82.9   53198   398060    221310   58736  22119  4032   19   332   74   6%  -1893  114   36   20  180%
c -   85.8   53196   398060    233311   39340  22140  4033   34   178   66  19%  -1781  -43   40   22  179%
c -   95.8   53196   398060    269485   38587  22262  4037   30   212   65  14%   -591   13   32   28  115%
c i  103.4   53195   398060    298873   64100  22328  4038   23   260   81   9%     -7   29   10   30   32%
c i  104.5   53190   398060    301760   66143  22336  4038   25   215   81  11%  -1068  -16   37   30  122%
c -  107.1   53188   398060    310406   40107  22340  4039   65   117   66  55%   -914 -105   86   34  252%
c i  107.4   53187   398060    311485   41137  22342  4039   61   114   71  54%   -882 -107   41   35  120%
c -  119.0   53185   398060    347852   44080  22345  4039   87    91   69  96%   -159  -77   89   56  159%
c 
c [simplification-10] limit 293565 conflicts (hard 363565) hit after 363566 conflicts
c [quatres-6] found 46122 quaternary clauses 22% in total
c [quatres-6-1] removed 10 duplicate quaternary clauses
c [quatres-6-1] added 5 double-self-subsuming ternary resolvents
c [quatres-6-2] added 794 single-self-subsuming ternary resolvents
c [quatres-6-2] added 779 quaternary resolvents
c [ternres-6] limit 26522054 with penalty 0 = 0 + 0
c [ternres-6] all 53185 free variables schedulable
c [ternres-6] 4639 ternary resolvents (108 bin, 4531 trn)
c [ternres-6] 273 variables remain 1% (52912 retained 99%)
c [card-4] limit 1657628 penalty 3 = 3 + 0
c [card-4] found 280 at-most-one constraints of average size 3.2
c [card-4] found 130 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1657628 for elimination
c [card-4] 409 out of 410 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1326102 penalty 2 = 2 + 0
c [gauss-3] extracted 10035 xors of average arity 3.0
c [gauss-3] connected 30064 occurrences of 6597 variables (average 4.6)
c [gauss-3] limit 1326102 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 72 variables
c [basicprobe-3] limit 132610273 penalty 0 = 0 + 0
c [basicprobe-3-0] 15860 sched 30%, 54 failed, 0 lifted, 1260 hbrs
c [decomp-23] removed 104 variables
c [basicprobe-3-1] 28302 sched 53%, 36 failed, 0 lifted, 386 hbrs
c [decomp-24] removed 52 variables
c [basicprobe-3-2] 28269 sched 53%, 1 failed, 0 lifted, 65 hbrs
c [decomp-25] removed 2 variables
c [basicprobe-3-3] 28273 sched 53%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-4] 28273 sched 53%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-5] 28273 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-5] fully completed probing
c [basicprobe-3-5] 91 units = 91 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 158 variables, found 1715 hbrs
c [bate-2] eliminated 146 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 346 transitive binary clauses
c [cce-3] limit of 33152568 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 61 (7%) of length 29
c [cce-3-1] eliminated 15 clauses out of 117 (13%) of length 26
c [cce-3-1] eliminated 5 clauses out of 100 (5%) of length 25
c [cce-3-1] eliminated 16 clauses out of 238 (7%) of length 24
c [cce-3-1] eliminated 9 clauses out of 187 (5%) of length 23
c [cce-3-1] eliminated 12 clauses out of 278 (4%) of length 22
c [cce-3-1] eliminated 15 clauses out of 245 (6%) of length 21
c [cce-3-1] eliminated 12 clauses out of 287 (4%) of length 20
c [cce-3-1] eliminated 19 clauses out of 448 (4%) of length 19
c [cce-3-1] eliminated 31 clauses out of 679 (5%) of length 18
c [cce-3-1] eliminated 35 clauses out of 652 (5%) of length 17
c [cce-3-1] eliminated 73 clauses out of 975 (7%) of length 16
c [cce-3-1] eliminated 77 clauses out of 971 (8%) of length 15
c [cce-3-1] eliminated 78 clauses out of 1096 (7%) of length 14
c [cce-3-1] eliminated 14 clauses out of 1460 (1%) of length 13
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 415 large clauses in 33152643 steps
c [cce-3-1] allowing another 16576321 steps for small clauses
c [cce-3-1] scheduling 121382 clauses = 50379 binary + 71003 ternary
c [cce-3-1] tried to eliminate 8290 small clauses 7%
c [cce-3-1] eliminated 84 binary clauses 0%
c [cce-3-1] eliminated 138 ternary clauses 0%
c [cce-3-1] eliminated 222 small clauses 0%
c [cce-3-1] eliminated 222 small clauses in 33152569 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 637 covered clauses in round 1
c [cce-3] eliminated 637 covered clauses in TOTAL during 1 rounds
c [cce-3] 637 < 1/100 * 395105 = 3951 considered unsuccessful
c [bca-6] limit of 10000000 steps and 789670 added (scaled 2)
c [bca-6] 89571 out of 105912 literals actually usable 85%
c [bca-6] added 51 blocked clauses in 316629 steps
c [sweep-6] limit 7956616 penalty 0 = 0 + 0
c [sweep-6-1] 7244 pos 42.9% + 9658 neg 57.1% = 16902 sched 31.9% ret 36053
c [sweep-6-1] 7958572 steps 1579 queries 2635.28 avg class size
c [sweep-6-1] 23528 decisions 1570 SAT calls 21.65 avg env size
c [sweep-6-1] 12544 variables remain 24% (40411 retained 76%)
c [decomp-28] removed 39 variables
c [sweep-6-1] removed 39 vars (0 failed, 39 eqs, 17 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 39 vars in TOTAL (1 rounds, 1578 queries)
c [sort-queue-10] sorted 35939 enqueued variables after 363566 conflicts
c [score-dist-10] active 16977 (32%), one 0 (0%), zero 35939 (68%)
c [score-dist-10] max exp 537, different 34 (6%)
c [score-dist-10] median active exp 520, avg 520.9
c [simplification-10] removed 269 variables 0.5% (52916 remain 12%)
c [simplification-10] removed 3750 irredundant clauses 0.9% (394310 remain 31%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 70000 = 140000 / 2
c [simplification-10] new conflict interval 210000
c [simplification-10] penalized conflict interval 210000 = 1 * 210000
c [simplification-10] hard conflict limit 678566 (soft 573566 + delta 105000)
c [simplification-10] new conflict limit 573566 (hard 678566)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  137.3   52916   394310    404566   43518  25755  4859   50    97   68  52%    526  -38   75   46  161%
c -  147.0   52916   394310    449088   43381  25772  4859   16   108   68  15%    772  -13   15   43   34%
c -  156.7   52916   394310    499946   44834  25802  4859   70    95   68  74%    908  -17   71   46  153%
c -  166.2   52916   394310    547873   44700  25813  4859   62    99   69  62%    968   -7   56   47  119%
c -  176.5   52916   394310    598265   45513  25817  4859   68    95   68  72%    998   -8   68   48  140%
c 
c [simplification-11] limit 573566 conflicts (hard 678566) hit after 609216 conflicts
c [quatres-7] found 45925 quaternary clauses 22% in total
c [quatres-7-1] removed 8 duplicate quaternary clauses
c [quatres-7-2] added 77 single-self-subsuming ternary resolvents
c [quatres-7-2] added 257 quaternary resolvents
c [ternres-7] limit 46023310 with penalty 0 = 0 + 0
c [ternres-7] 266 schedulable variables 1%
c [ternres-7] 6415 ternary resolvents (275 bin, 6140 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-29] removed 42 variables
c [simpleprobe-4] 22080 schedulable variables 42%
c [simpleprobe-4] limit 184093241 penalty 0 = 0 + 0
c [decomp-30] removed 71 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 71 variables, found 1860 hbrs, 9 units
c [unhide-10] limit 4602331 with penalty 1 = 1 + 0
c [unhide-10-11] 0 units, 0 failed, 4410 tauts, 0 hbrs, 59502 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 383 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 52803 variables 100%
c [block-4] limit of 115058276 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 4268 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 52147 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1041 variables 2% in round 1 in 356376371 steps
c [elim-8-1] backward subsumption/strengthening limit 356376300
c [elim-8-1-1] backward checking 4651 touched variables 9%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 21 and strengthened 2 clauses in 10488640 steps
c [elim-8-1] rescheduled 53 variables 0% by backward subsumption
c [elim-8-2] eliminated 5 variables 0% in round 2 in 63049278 steps
c [elim-8-2] backward subsumption/strengthening limit 63049200
c [elim-8-2-1] backward checking 31 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 16 clauses in 356873 steps
c [elim-8-2] rescheduled 10 variables 0% by backward subsumption
c [elim-8-3] eliminated 7 variables 0% in round 3 in 99168 steps
c [elim-8-3] backward subsumption/strengthening limit 99100
c [elim-8-3-1] backward checking 15 touched variables 0%
c [elim-8-3-1] incomplete backward checking 9 remain 60%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 99214 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1056 = 2% variables out of 52147 scheduled
c [bca-7] limit of 10000000 steps and 770472 added (scaled 2)
c [bca-7] 86704 out of 102184 literals actually usable 85%
c [bca-7] added 30 blocked clauses in 309084 steps
c [sweep-7] limit 13806993 penalty 0 = 0 + 0
c [sweep-7-1] 4705 pos 39.3% + 7270 neg 60.7% = 11975 sched 23.4% ret 39116
c [sweep-7-1] 13808132 steps 4749 queries 1165.88 avg class size
c [sweep-7-1] 54267 decisions 4751 SAT calls 16.56 avg env size
c [sweep-7-1] 2489 variables remain 5% (48591 retained 95%)
c [decomp-31] removed 24 variables
c [sweep-7-1] removed 24 vars (0 failed, 9 eqs, 11 impls)
c [sweep-7] 24 < 1/1000 * 51091 = 51 considered unsuccessful
c [sweep-7] removed 24 vars in TOTAL (1 rounds, 4748 queries)
c [sort-queue-11] sorted 33951 enqueued variables after 609216 conflicts
c [score-dist-11] active 17116 (34%), one 0 (0%), zero 33951 (66%)
c [score-dist-11] max exp 538, different 34 (6%)
c [score-dist-11] median active exp 521, avg 521.6
c [simplification-11] removed 1849 variables 3.5% (51067 remain 12%)
c [simplification-11] removed 9652 irredundant clauses 2.4% (384658 remain 30%)
c [simplification-11] maximum reduction of 3% = max (3%, 2%)
c [simplification-11] geometric conflict interval increment 52500 = 210000 / 4
c [simplification-11] new conflict interval 262500
c [simplification-11] penalized conflict interval 262500 = 1 * 262500
c [simplification-11] hard conflict limit 1002966 (soft 871716 + delta 131250)
c [simplification-11] new conflict limit 871716 (hard 1002966)
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 -  201.6   51067   384658    670198   45851  21004  3682   12    98   66  12%   1015   -5   12   40   30%
c -  212.4   51067   384658    735665   47126  21027  3682   64   109   67  59%   1021    5   76   38  201%
c -  221.8   51067   384658    775644   48416  21096  3682   49   118   66  41%   1022    9   46   43  106%
c -  233.9   51067   384658    828883   48857  21112  3682   27    90   67  30%   1023  -12   37   43   86%
c -  245.8   51067   384658    879324   49226  21124  3683   64    92   68  69%   1024   -4   72   47  153%
c 
c [simplification-12] limit 871716 conflicts (hard 1002966) hit after 888025 conflicts
c [quatres-8] found 44752 quaternary clauses 22% in total
c [quatres-8-1] removed 28 duplicate quaternary clauses
c [quatres-8-2] added 232 single-self-subsuming ternary resolvents
c [quatres-8-2] added 665 quaternary resolvents
c [ternres-8] limit 69180246 with penalty 0 = 0 + 0
c [ternres-8] all 51067 free variables schedulable
c [ternres-8] 6007 ternary resolvents (420 bin, 5587 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-32] removed 17 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 228 transitive binary clauses
c [transred-8] found 8 units
c [bca-8] limit of 10000000 steps and 769403 added (scaled 2)
c [bca-8] 86282 out of 102066 literals actually usable 85%
c [bca-8] added 6 blocked clauses in 314562 steps
c [sort-queue-12] sorted 33874 enqueued variables after 888025 conflicts
c [score-dist-12] active 17158 (34%), one 0 (0%), zero 33874 (66%)
c [score-dist-12] max exp 539, different 35 (6%)
c [score-dist-12] median active exp 521, avg 521.9
c [simplification-12] removed 35 variables 0.1% (51032 remain 12%)
c [simplification-12] removed 344 irredundant clauses 0.1% (384314 remain 30%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 262500
c [simplification-12] new conflict interval 525000
c [simplification-12] penalized conflict interval 525000 = 1 * 525000
c [simplification-12] hard conflict limit 1675525 (soft 1413025 + delta 262500)
c [simplification-12] new conflict limit 1413025 (hard 1675525)
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 -  257.9   51032   384314    932120   51403  25577  3726   24    96   68  25%   1024    3   59   38  155%
c -  268.8   51032   384314    978783   52482  25583  3726   33    82   69  40%   1024   -9   64   40  160%
c -  282.3   51032   384314   1028554   52540  25596  3727   66    90   69  74%   1024   -2   66   45  148%
c -  294.6   51032   384314   1072477   53184  25642  3727   39   148   70  26%   1024   47   53   48  109%
c -  307.0   51032   384314   1115626   54382  25657  3727   58    83   70  70%   1024  -17   65   53  122%
c -  320.5   51032   384314   1158879   54647  25678  3729   58    75   71  78%   1024  -16   58   56  103%
c -  334.4   51032   384314   1203822   54965  25686  3729   69    79   71  88%   1024  -11   67   59  114%
c -  348.9   51032   384314   1250019   56431  25691  3729   66    72   72  92%   1024  -12   68   60  112%
c -  361.5   51032   384314   1294757   56214  25695  3729   38   106   71  36%   1024   11   40   51   79%
c -  376.8   51032   384314   1340235   57920  25702  3729   47    81   72  58%   1024  -12   46   45  102%
c -  389.7   51032   384314   1403127   58860  25721  3729   53    91   70  58%   1024   -4   64   40  160%
c 
c [simplification-13] limit 1413025 conflicts (hard 1675525) hit after 1424989 conflicts
c [quatres-9] found 45356 quaternary clauses 21% in total
c [quatres-9-1] removed 6 duplicate quaternary clauses
c [quatres-9-1] added 6 double-self-subsuming ternary resolvents
c [quatres-9-2] added 50 single-self-subsuming ternary resolvents
c [quatres-9-2] added 90 quaternary resolvents
c [ternres-9] limit 124358769 with penalty 0 = 0 + 0
c [ternres-9] all 51032 free variables schedulable
c [ternres-9] 403 ternary resolvents (91 bin, 312 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-33] removed 24 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 157 transitive binary clauses
c [transred-9] found 4 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 51002 variables 100%
c [block-5] limit of 400000000 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2238 blocked clauses
c [block-5] 2238 < 1/100 * 384225 = 3842 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 50727 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 157 variables 0% in round 1 in 347062218 steps
c [elim-9-1] backward subsumption/strengthening limit 52937782
c [elim-9-1-1] backward checking 783 touched variables 2%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 6 clauses in 3699931 steps
c [elim-9-1] rescheduled 12 variables 0% by backward subsumption
c [elim-9-2] eliminated 2 variables 0% in round 2 in 304597 steps
c [elim-9-2] backward subsumption/strengthening limit 304500
c [elim-9-2-1] backward checking 12 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 219606 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 159 = 0% variables out of 50727 scheduled
c [elim-9] 159 < 1/100 * 50727 = 507 considered unsuccessful
c [bca-9] limit of 10000000 steps and 763486 added (scaled 2)
c [bca-9] 85313 out of 101138 literals actually usable 84%
c [bca-9] added 12 blocked clauses in 337011 steps
c [sweep-8] limit 18653815 penalty 1 = 1 + 0
c [sweep-8-1] 1022 pos 41.7% + 1429 neg 58.3% = 2451 sched 4.8% ret 48117
c [sweep-8-1] 1998746 steps 1482 queries 547.65 avg class size
c [sweep-8-1] 17232 decisions 1481 SAT calls 15.94 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-34] removed 52 variables
c [sweep-8-1] removed 52 vars (0 failed, 2 eqs, 1 impls)
c [sweep-8-2] 17355 pos 34.4% + 33161 neg 65.6% = 50516 sched 100.0% ret 0
c [sweep-8-2] 16659886 steps 1489 queries 1901.65 avg class size
c [sweep-8-2] 33829 decisions 1491 SAT calls 35.32 avg env size
c [sweep-8-2] 26572 variables remain 53% (23929 retained 47%)
c [decomp-35] removed 28 variables
c [sweep-8-2] removed 28 vars (0 failed, 5 eqs, 5 impls)
c [sweep-8] removed 80 vars in TOTAL (2 rounds, 2969 queries)
c [sort-queue-13] sorted 33191 enqueued variables after 1424989 conflicts
c [score-dist-13] active 17297 (34%), one 0 (0%), zero 33191 (66%)
c [score-dist-13] max exp 541, different 37 (7%)
c [score-dist-13] median active exp 522, avg 522.6
c [simplification-13] removed 544 variables 1.1% (50488 remain 12%)
c [simplification-13] removed 3838 irredundant clauses 1.0% (380476 remain 29%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 262500 = 525000 / 2
c [simplification-13] new conflict interval 787500
c [simplification-13] penalized conflict interval 787500 = 1 * 787500
c [simplification-13] hard conflict limit 2606239 (soft 2212489 + delta 393750)
c [simplification-13] new conflict limit 2212489 (hard 2606239)
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 -  413.3   50488   380476   1451014   59994  25316  3514   55   100   70  55%   1024    2   71   42  169%
c -  426.7   50488   380476   1498704   61589  25357  3514   60    83   71  73%   1024  -11   68   49  141%
c -  439.2   50488   380476   1545930   61452  25368  3514   73    85   71  86%   1024   -5   76   56  136%
c -  452.8   50488   380476   1594332   61349  25370  3514   45    91   71  50%   1024    4   42   57   73%
c -  464.3   50488   380476   1645310   61115  25371  3514   69    82   71  84%   1024   -9   73   58  125%
c -  477.5   50488   380476   1703775   61834  25381  3514   57    90   72  64%   1024   -5   64   55  118%
c -  492.5   50488   380476   1756040   62716  25386  3514   65    77   73  84%   1024  -12   69   58  118%
c -  507.6   50488   380476   1808629   63590  25393  3515   62    75   73  82%   1024  -10   67   55  121%
c -  523.3   50488   380476   1861977   64018  25399  3515   66    75   74  88%   1024   -7   71   60  119%
c -  540.5   50488   380476   1914199   65037  25406  3516   41    83   73  49%   1024   -1   37   50   75%
c -  555.4   50488   380476   1969078   64676  25419  3516   42    97   72  43%   1024    6   36   47   77%
c -  569.7   50488   380476   2024109   66164  25420  3516   64    74   73  86%   1024  -11   64   54  118%
c -  585.1   50488   380476   2078718   66818  25426  3516   42    85   73  49%   1024    3   45   53   84%
c -  601.0   50488   380476   2134328   66564  25428  3516   62    77   73  80%   1024   -2   63   54  116%
c -  619.2   50488   380476   2191041   67996  25428  3516   45    76   74  58%   1024   -1   44   54   80%
c 
c [simplification-14] limit 2212489 conflicts (hard 2606239) hit after 2224354 conflicts
c [quatres-10] found 45270 quaternary clauses 21% in total
c [quatres-10-1] removed 7 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 45 single-self-subsuming ternary resolvents
c [quatres-10-2] added 395 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 50488 free variables schedulable
c [ternres-10] 758 ternary resolvents (96 bin, 662 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 5139613 penalty 3 = 3 + 0
c [gauss-4] extracted 36447 xors of average arity 3.0
c [gauss-4] connected 109339 occurrences of 10227 variables (average 10.7)
c [gauss-4] limit 5139613 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-11] limit 2500000 with penalty 3 = 2 + 1
c [unhide-11-12] 1 units, 2 failed, 603 tauts, 0 hbrs, 153466 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 133 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 1284903375 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 34
c [cce-4-1] eliminated 1 clauses out of 73 (1%) of length 28
c [cce-4-1] eliminated 1 clauses out of 79 (1%) of length 27
c [cce-4-1] eliminated 1 clauses out of 104 (1%) of length 26
c [cce-4-1] eliminated 2 clauses out of 220 (1%) of length 24
c [cce-4-1] eliminated 4 clauses out of 183 (2%) of length 23
c [cce-4-1] eliminated 4 clauses out of 250 (2%) of length 22
c [cce-4-1] eliminated 4 clauses out of 274 (1%) of length 21
c [cce-4-1] eliminated 1 clauses out of 295 (0%) of length 20
c [cce-4-1] eliminated 2 clauses out of 439 (0%) of length 19
c [cce-4-1] eliminated 8 clauses out of 675 (1%) of length 18
c [cce-4-1] eliminated 9 clauses out of 619 (1%) of length 17
c [cce-4-1] eliminated 10 clauses out of 900 (1%) of length 16
c [cce-4-1] eliminated 9 clauses out of 912 (1%) of length 15
c [cce-4-1] eliminated 10 clauses out of 1010 (1%) of length 14
c [cce-4-1] eliminated 81 clauses out of 1398 (6%) of length 13
c [cce-4-1] eliminated 166 clauses out of 2291 (7%) of length 12
c [cce-4-1] eliminated 480 clauses out of 3607 (13%) of length 11
c [cce-4-1] eliminated 605 clauses out of 4776 (13%) of length 10
c [cce-4-1] eliminated 1044 clauses out of 7668 (14%) of length 9
c [cce-4-1] eliminated 1815 clauses out of 12617 (14%) of length 8
c [cce-4-1] eliminated 2545 clauses out of 25745 (10%) of length 7
c [cce-4-1] eliminated 2173 clauses out of 57532 (4%) of length 6
c [cce-4-1] eliminated 1258 clauses out of 30818 (4%) of length 5
c [cce-4-1] eliminated 1218 clauses out of 33770 (4%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 11452 large clauses in 305281097 steps
c [cce-4-1] allowing another 152640548 steps for small clauses
c [cce-4-1] scheduling 125307 clauses = 47549 binary + 77758 ternary
c [cce-4-1] tried to eliminate 125307 small clauses 100%
c [cce-4-1] eliminated 542 binary clauses 1%
c [cce-4-1] eliminated 723 ternary clauses 1%
c [cce-4-1] eliminated 1265 small clauses 1%
c [cce-4-1] eliminated 1383 small clauses in 258889104 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 12835 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 135292942 steps for small clauses
c [cce-4-2] scheduling 124044 clauses = 47007 binary + 77037 ternary
c [cce-4-2] tried to eliminate 124044 small clauses 100%
c [cce-4-2] eliminated 2 ternary clauses 0%
c [cce-4-2] eliminated 2 small clauses 0%
c [cce-4-2] eliminated 2 small clauses in 236781327 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 2 covered clauses in round 2
c [cce-4-3] completed large round (ATE)
c [cce-4-3] allowing another 135235181 steps for small clauses
c [cce-4-3] scheduling 124042 clauses = 47007 binary + 77035 ternary
c [cce-4-3] tried to eliminate 124042 small clauses 100%
c [cce-4-3] completed small round (ATE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 12837 covered clauses in TOTAL during 3 rounds
c [bca-10] limit of 10000000 steps and 735814 added (scaled 2)
c [bca-10] 84619 out of 100966 literals actually usable 84%
c [bca-10] added 18 blocked clauses in 352708 steps
c [sweep-9] limit 61675362 penalty 0 = 0 + 0
c [sweep-9-1] 9732 pos 36.6% + 16836 neg 63.4% = 26568 sched 52.6% ret 23914
c [sweep-9-1] 36159695 steps 9134 queries 820.42 avg class size
c [sweep-9-1] 113235 decisions 9128 SAT calls 18.19 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-37] removed 71 variables
c [sweep-9-1] removed 71 vars (0 failed, 53 eqs, 32 impls)
c [sweep-9-2] 17003 pos 33.7% + 33408 neg 66.3% = 50411 sched 100.0% ret 0
c [sweep-9-2] 25516598 steps 2583 queries 1174.73 avg class size
c [sweep-9-2] 48519 decisions 2578 SAT calls 31.06 avg env size
c [sweep-9-2] 19270 variables remain 38% (31105 retained 62%)
c [decomp-38] removed 66 variables
c [sweep-9-2] removed 66 vars (0 failed, 14 eqs, 7 impls)
c [sweep-9] removed 137 vars in TOTAL (2 rounds, 11715 queries)
c [sort-queue-14] sorted 32147 enqueued variables after 2224354 conflicts
c [score-dist-14] active 18198 (36%), one 0 (0%), zero 32147 (64%)
c [score-dist-14] max exp 542, different 38 (7%)
c [score-dist-14] median active exp 523, avg 523.4
c [simplification-14] removed 143 variables 0.3% (50345 remain 12%)
c [simplification-14] removed 13816 irredundant clauses 3.6% (366660 remain 28%)
c [simplification-14] maximum reduction of 4% = max (0%, 4%)
c [simplification-14] geometric conflict interval increment 157500 = 787500 / 5
c [simplification-14] new conflict interval 945000
c [simplification-14] penalized conflict interval 945000 = 1 * 945000
c [simplification-14] hard conflict limit 3641854 (soft 3169354 + delta 472500)
c [simplification-14] new conflict limit 3169354 (hard 3641854)
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 -  658.3   50345   366660   2246806   69302  24626  4129   62    70   73  88%   1024   -7   66   53  124%
c -  675.3   50345   366660   2302621   68984  24630  4129   60    71   74  84%   1024   -5   63   51  125%
c -  693.3   50345   366660   2360867   69580  24632  4129   37    86   73  43%   1024    9   45   49   92%
c -  710.6   50345   366660   2418881   70010  24634  4129   50    72   73  70%   1024   -5   49   49  101%
c -  727.0   50345   366660   2479772   70733  24637  4129   49    74   74  66%   1024   -1   31   50   63%
c -  743.5   50345   366660   2541470   71463  24639  4129   60    70   74  86%   1024   -5   60   51  117%
c -  764.4   50345   366660   2603565   72039  24639  4129   59    67   74  87%   1024   -5   57   53  107%
c -  784.6   50345   366660   2668029   72892  24639  4129   57    69   75  83%   1024   -1   59   55  107%
c -  805.8   50345   366660   2730529   73413  24639  4129   59    65   74  92%   1024   -5   57   55  103%
c -  826.4   50345   366660   2793675   73478  24640  4129   58    64   75  91%   1024   -4   58   55  105%
c -  845.8   50345   366660   2858595   73179  24647  4129   59    64   76  93%   1024   -6   62   54  114%
c -  869.1   50345   366660   2926338   75214  24653  4129   53    71   77  74%   1024    2   54   57   95%
c -  891.8   50345   366660   2993445   74637  24653  4129   59    65   77  92%   1024   -2   61   57  106%
c -  913.9   50345   366660   3062326   75512  24653  4129   51    68   77  75%   1024    1   24   56   43%
c -  936.9   50345   366660   3131791   74349  24654  4129   57    60   77  96%   1024   -5   57   57  100%
c 
c [simplification-15] limit 3169354 conflicts (hard 3641854) hit after 3169354 conflicts
c [quatres-11] found 44390 quaternary clauses 22% in total
c [quatres-11-1] removed 19 duplicate quaternary clauses
c [quatres-11-1] added 3 double-self-subsuming ternary resolvents
c [quatres-11-2] added 88 single-self-subsuming ternary resolvents
c [quatres-11-2] added 194 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 50345 free variables schedulable
c [ternres-11] 1473 ternary resolvents (89 bin, 1384 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 10426583 penalty 4 = 4 + 0
c [card-5] found 223 at-most-one constraints of average size 3.0
c [card-5] found 142 at-most-two constraints of average size 4.0
c [card-5] using previous limit 10426583 for elimination
c [card-5] 365 out of 365 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] generated 31 at-most-one constraints, 8 used 26%
c [card-5] exported 8 binary clauses, 1.0 per/constraint
c [treelook-4] limit 4170633 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 13507 literals 13%
c [treelook-4] scheduling used 1020890 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 4170633 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 4181665 steps
c [treelook-4] 10927 literals remain 11%
c [treelook-4] 2648 variables remain to probed next time 5%
c [decomp-40] removed 34 variables
c [treelook-4] removed 98 variables, found 1281 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 480 transitive binary clauses
c [transred-11] found 2 units
c [bca-11] limit of 10000000 steps and 732103 added (scaled 2)
c [bca-11] 83871 out of 100492 literals actually usable 83%
c [bca-11] added 6 blocked clauses in 359950 steps
c [sweep-10] limit 100095198 penalty 0 = 0 + 0
c [sweep-10-1] 7170 pos 37.2% + 12081 neg 62.8% = 19251 sched 38.3% ret 30994
c [sweep-10-1] 24326996 steps 7588 queries 693.10 avg class size
c [sweep-10-1] 92373 decisions 7583 SAT calls 17.68 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-41] removed 27 variables
c [sweep-10-1] removed 27 vars (0 failed, 15 eqs, 11 impls)
c [sweep-10-2] 16766 pos 33.4% + 33452 neg 66.6% = 50218 sched 100.0% ret 0
c [sweep-10-2] 48246647 steps 8005 queries 469.91 avg class size
c [sweep-10-2] 115876 decisions 8001 SAT calls 22.04 avg env size
c [sweep-10-2] fully completed sweeping round
c [decomp-42] removed 29 variables
c [sweep-10-2] removed 29 vars (0 failed, 28 eqs, 15 impls)
c [sweep-10-3] 16757 pos 33.4% + 33432 neg 66.6% = 50189 sched 100.0% ret 0
c [sweep-10-3] 27522692 steps 2899 queries 1021.13 avg class size
c [sweep-10-3] 55680 decisions 2896 SAT calls 30.01 avg env size
c [sweep-10-3] 16351 variables remain 33% (33799 retained 67%)
c [decomp-43] removed 85 variables
c [sweep-10-3] removed 85 vars (0 failed, 14 eqs, 6 impls)
c [sweep-10] removed 141 vars in TOTAL (3 rounds, 18489 queries)
c [sort-queue-15] sorted 31271 enqueued variables after 3169354 conflicts
c [score-dist-15] active 18833 (38%), one 0 (0%), zero 31271 (62%)
c [score-dist-15] max exp 543, different 39 (7%)
c [score-dist-15] median active exp 523, avg 524.0
c [simplification-15] removed 241 variables 0.5% (50104 remain 12%)
c [simplification-15] removed 1979 irredundant clauses 0.5% (364681 remain 28%)
c [simplification-15] maximum reduction of 1% = max (0%, 1%)
c [simplification-15] geometric conflict interval increment 472500 = 945000 / 2
c [simplification-15] conflict interval soft limit 1000000 reached
c [simplification-15] new conflict interval 1000000
c [simplification-15] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-15] hard conflict limit 4669354 (soft 4169354 + delta 500000)
c [simplification-15] new conflict limit 4169354 (hard 4669354)
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 -  974.6   50104   364681   3199529   74466  25509  4502   60    64   76  94%   1024   -4   61   54  114%
c -  998.2   50104   364681   3270156   76220  25509  4502   46    71   77  65%   1024    5   41   53   77%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 402 basic ate = 167 trn 42% + 235 lrg 58% in 2 updates
c bcas: 11 count, 592 added (770 skipped), 3490194 steps
c bkwd: tried 144315 clauses, 286775 lits, 1.99 lits/clause
c bkwd: checked 87170143 occs, 604.03 occs/clause, 303.97 occs/lit
c bkwd: subsumed 0 binary, 39 ternary, 955 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 1827 large (0% self)
c blkd: 5 bces, 19785 removed, 14089022 resolutions, 35788048 steps
c blkd: 5476 blocking literals 1%, 2080 pure
c bump: 3250930 bumped seen, 670472190 lits 206.2 on average
c card: 5 count, 0 units, 8 am1, 31771514 steps
c card: 30 rescheduled, 256 eliminated, 51129 resolved, 9517 subsumed
c card: 702 at-most-one constraints found, average size 3.14
c card: 702 at-most-one constraints used 100%, average size 3.14
c card: 272 at-most-two constraints found, average size 4.00
c card: 271 at-most-two constraints used 100%, average size 4.00
c cces: 4 cces, 14301 eliminated, 14033 ate 98%, 268 abce 2%
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: 4305712 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 90 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 43 decompositions, 1794 equivalent 0%
c deco: 405 decision-only clauses 0%, 53% reduction
c decs: 17959048 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 9 elims, 374244 eliminated 86%, 230 pure 0%
c elms: 15 rounds, 1.7 rounds/bve
c elms: 353236 small 94%, 18698 large 5%
c elms: 461224 tried small, 353236 succeeded 77%, 107988 failed 23%
c elms: 4963 subsumed, 4707 strengthened, 15 blocked
c elms: 12040089 copies, 21301686 resolutions, 8519052 ipos
c elms: 11170606 subchks, 9636532 strchks
c gaus: 4 extractions, 70966 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 18939284 steps, 9469642 extr 50%, 9548268 elim 50%
c glue: 49.4 orig avg, 49.4 real avg, 6.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 18783 = 3010 simple 16% + 14756 trn 79% + 1017 lrg 5%, 1637 sub 9%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3250929 clauses, 87.1 length
c lrnd: 283250187 lits = 494618979 orig - 211368792 removed 43%
c lrnd: 693638 uips 21%, 1533752 flips 47%
c mins: 3245540 mins 100%, 198 bin 0%, 4783 size 0%
c mins: 413829424 poisoned searches, 50335240 hits, 12% hit rate
c mins: 854694850 used twice searches, 112211883 hits, 13% hit rate
c move: moved 15028, 3335 bin 22%, 11693 trn 78%
c otfs: 26779 driving 45%, 32747 restarting 55%
c otfs: str 59526, 59352 red 100%, 174 irr 0%
c otfs: str 59526, 0 bin 0%, 160 trn 0%, 59366 lrg 100%
c otfs: sub 5091, 5085 red 100%, 6 irr 0%
c otfs: sub 5091, 0 bin 0%, 18 trn 0%, 5073 lrg 100%
c phas: 4 computed, 189771 set, 59974 pos (32%), 129797 neg (68%)
c prbs: 3 basic, 416289 probed, 449 failed, 397 lifted
c prbs: 4 simple, 703461 probed, 19 failed, 300 eqs
c prbs: 4 treelook, 2666 probed, 35 failed, 0 lifted
c prom: 148580 locked 2% out of 8754353 tried
c prps: 1571662642 props, 87 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 11 count, 14835 quat, 3294 self1, 21 self2, 222 dup
c queu: 15 sorted, 17959048 next (624155 steps 0.03)
c queu: 671659229 enq (973833395 steps 1.45), 670472190 deq 100%
c redc: 2156 clauses 3%, 68079 tried 2%, 4 sat 0%
c redc: 2850 lits 0%, 799357 tried 0%, 4 sat 0%
c redc: 58 times jump level reduced, 16.2 levels on average
c reds: 61 count, 53659.5 conflicts per reduce
c reds: 0 memlim 0%, 61 arith 100%
c reds: 2440366 collected 90%, 273156 retired 10%
c rmbd: 1389 removed, 1010 red 73%
c rsts: 18040 restarts 89%, 2264 skipped 11%
c rsts: 2264 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: 15 count, 15 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3250929 count (7719922 tried 2.4), 449452 sub out of 3249006 (13.8%)
c swps: 10 count, 14 rounds, 43470 queries (3105.0/round)
c swps: 43435 sat calls, 224 unsat (0.1% success rate)
c swps: 626240 decisions 14.4, 4478 conflicts 0.1
c swps; 1034.1 avg class size, 21.7 avg environment size
c swps: 0 failed, 164 impls, 252 equivs
c swp0: 14486 type 0 queries, 1120 unsat (7.7%), 14434 sat (99.6%)
c swp1: 28984 type 1 queries, 6800 unsat (23.5%), 28784 sat (99.3%)
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: 42420290 calls to obtain time
c tops: 7459 fixed 2%, 11 its, 297566.45 confs/it
c trds: 11 transitive reductions, 2310 removed, 17 failed
c trds: 1143180 nodes, 584789 edges, 8080957 steps
c trim: 3731887 words, 14.2 MB
c trnr: 11 count, 1497 bin, 42518 trn, 347798946 steps
c unhd: 11 count, 12 rounds, 44868909 steps
c unhd: 2198 non-trivial sccs of average size 2.6
c unhd: 18 units, 18 bin, 0 trn, 0 lrg
c unhd: 124 failed, 122 stamp, 0 lits, 0 bin, 2 trn, 0 lrg
c unhd: 10514 tauts, 173 bin 2%, 5950 trn 57%, 2698 lrg 26%
c unhd: 10514 tauts, 1693 stamp 16%, 7313 red 70%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 317176 str, 18 bin 0%, 1838 trn 1%, 315320 lrg 99%, 286493 red 90%
c vars: 50104 remaining 12% and 383497 removed 88% out of 433601
c vars: 7459 fixed 2%, 374244 eliminated 86%, 1794 equivalent 0%
c vsts: 35147525770 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 22.4 search visits per propagation, 10698.9 per conflict
c wchs: 4963746161 pushed, 58249923 enlarged, 148 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3263841       2440366        273156     189174287      57950010       2176689
c 
c  0 0         42542   1      2920   0         0   0  83008300  44  14612105  25    352083  16     0.9
c  1 5         18892   1      5691   0      8749   3  15200388   8   4312561   7     66042   3     0.2
c  2 6        114137   3     52717   2     26309  10  31386036  17< 10193037  18    153500   7     1.0
c  3 9        249134   8    106677   4     27449  10  26385095  14   8772032  15<   211161  10     2.4
c  4 14       197132   6    108301   4     25541   9  12490781   7   5744899  10    223992  10     3.5
c  5 21       181281   6    139153   6     23409   9   6744497   4   3927013   7    238482  11<    3.1
c  6 30       231114   7    188030   8     22941   8<  4342690   2   2764152   5    213411  10     3.8
c  7 41       523547  16<   442649  18<    34325  13   4677633   2   3572401   6    380900  17     9.1
c  8 54       968397  30    764950  31     69888  26   2926126   2   2422569   4    200191   9    31.4
c  9 69       674287  21    575287  24     32916  12   1898984   1   1532862   3    131831   6    15.1
c 10 86        63035   2     53931   2      1566   1    113005   0     96120   0      5088   0    15.8
c 11 126         343   0        60   0        63   0       752   0       259   0         8   0     0.2
c 
c avg                  6.8           7.2           5.9           1.8           2.9           4.5
c std                  2.2           1.9           2.5           2.1           2.6           2.8
c 
c   85.857   9% bump
c   32.111   3% sweep
c   29.644   3% elim
c   15.326   2% cce
c   11.456   1% decide
c   10.539   1% probe
c    6.010   1% unhide
c    3.814   0% block
c 
c   12.281 < 1% rest (below)
c 
c    3.273   0% ternres
c    2.964   0% bca
c    2.900   0% quatres
c    1.771   0% gauss
c    0.726   0% card
c    0.646   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    7.552   1% preprocessing     6%
c  109.285  11% inprocessing     94%
c ==================================
c  116.837  12% simplifying
c  882.375  88% search
c ==================================
c  999.220 100% all
c 
c       3273231 conflicts,        3275.8 confs/sec
c           457 ternaries,        7162.4 confs/ternary
c            52 binaries,        62946.8 confs/binary
c            11 iterations,     297566.5 confs/iteration
c 
c            61 reductions,          0.1 redus/sec,  53659.5 confs/reduction
c         18040 restarts,           18.1 rests/sec,    181.4 confs/restart
c      17959048 decisions,       17973.1 decis/sec,      5.5 decis/conflict
c    1571662642 propagations,  1572889.6 props/sec,     87.5 props/decision
c 
c 999.2 seconds, 152.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
