c launch: /data/cnf/sc2014/app/countbitssrl032.cnf.bz2
c host: atom18
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/countbitssrl032.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/countbitssrl032.cnf.bz2
c no embedded options
c found 'p cnf 18607 55724' header
c read 18607 variables, 55724 clauses, 130020 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=4
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 18605 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   18605    55722         0       0      0     0    0     0    3   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 2 variables
c [simpleprobe-1] all 18605 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 192 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 192 variables, found 105 hbrs, 37 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 192 units, 823 failed, 2136 tauts, 0 hbrs, 936 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 17679 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 11632 variables 66% in round 1 in 2845415 steps
c [elim-1-1] backward subsumption/strengthening limit 2845400
c [elim-1-1-1] backward checking 12570 touched variables 71%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 192 and strengthened 288 clauses in 940181 steps
c [elim-1-1] rescheduled 575 variables 3% by backward subsumption
c [elim-1-2] eliminated 24 variables 0% in round 2 in 222559 steps
c [elim-1-2] backward subsumption/strengthening limit 222500
c [elim-1-2-1] backward checking 247 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 10 and strengthened 39 clauses in 160764 steps
c [elim-1-2] rescheduled 116 variables 1% by backward subsumption
c [elim-1-3] eliminated 18 variables 0% in round 3 in 51417 steps
c [elim-1-3] backward subsumption/strengthening limit 51400
c [elim-1-3-1] backward checking 119 touched variables 1%
c [elim-1-3-1] incomplete backward checking 0 remain 0%
c [elim-1-3] subsumed 2 and strengthened 23 clauses in 51401 steps
c [elim-1] incomplete 25 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 11706 = 66% variables out of 17679 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 27681 negative 92.5% of 29923 except 2242 7.5%
c [phase-count-1] 25737 positive 86.0% of 29923 except 4186 14.0%
c [phase-1] phase bias: 1103 positive 18%, 4870 negative 82%
c [sort-queue-1] sorted 5973 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5973 (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 12632 variables 67.9% (5973 remain 32%)
c [simplification-1] removed 25799 irredundant clauses 46.3% (29923 remain 54%)
c [simplification-1] maximum reduction of 68% = max (68%, 46%)
c [simplification-1] large reduction 68% >= 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    0.5    5972    29923         6       4      0    30    0     0    4  81%      0    0    1    0 25253%
c i    0.5    5966    29923         7       4      0    30    0     0    4  81%      0    0    1    0 25155%
c i    0.5    5965    29923        13       4      0    35    0     0    4  81%      0    0    1    0 24589%
c i    0.5    5964    29923        14       4      0    35    0     0    4  81%      0    0    1    0 24493%
c i    0.5    5961    29923        15       4      0    35    0     0    4  81%      0    0    1    0 24398%
c i    0.5    5960    29923        16       4      0    35    0     0    4  81%      0    0    1    0 24303%
c i    0.5    5959    29923        34      12      2    40    0     0    4  59%      0    0    1    0 23128%
c i    0.5    5947    29923        35      12      2    40    0     0    4  59%      0    0    1    0 23038%
c i    0.5    5930    29923        38      13      2    41    0     0    4  59%      0    0    1    0 22809%
c i    0.5    5914    29923        39      13      2    41    0     0    4  59%      0    0    1    0 22721%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 321 variables
c [simpleprobe-2] all 5652 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 478 variables
c [simpleprobe-2] 261 variables remain 5% (4913 retained 95%)
c [simpleprobe-2] removed 478 variables, found 1740 hbrs, 107 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 10348 literals 100%
c [treelook-1] scheduling used 109652 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 331955 steps
c [treelook-1] 10306 literals remain 100%
c [treelook-1] 5173 variables remain to probed next time 100%
c [decomp-5] removed 3 variables
c [treelook-1] removed 4 variables, found 1579 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1199 probes remain 24% after last round
c [basicprobe-1-0] 36 units = 36 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 121 variables, found 1829 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 42 failed, 1625 tauts, 0 hbrs, 2113 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 5009 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 536 variables 11% in round 1 in 2661305 steps
c [elim-2-1] backward subsumption/strengthening limit 2661300
c [elim-2-1-1] backward checking 1962 touched variables 39%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 17 and strengthened 128 clauses in 443387 steps
c [elim-2-1] rescheduled 287 variables 6% by backward subsumption
c [elim-2-2] eliminated 40 variables 1% in round 2 in 637099 steps
c [elim-2-2] backward subsumption/strengthening limit 637000
c [elim-2-2-1] backward checking 219 touched variables 4%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 0 and strengthened 43 clauses in 150811 steps
c [elim-2-2] rescheduled 60 variables 1% by backward subsumption
c [elim-2-3] eliminated 1 variables 0% in round 3 in 177720 steps
c [elim-2-3] backward subsumption/strengthening limit 177700
c [elim-2-3-1] backward checking 27 touched variables 1%
c [elim-2-3-1] fully completed backward checking in 1 rounds
c [elim-2-3] subsumed 0 and strengthened 6 clauses in 42106 steps
c [elim-2] incomplete 8 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 592 = 12% variables out of 5009 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 373 enqueued variables after 39 conflicts
c [score-dist-2] active 4044 (92%), one 0 (0%), zero 373 (8%)
c [score-dist-2] max exp 505, different 5 (1%)
c [score-dist-2] median active exp 504, avg 503.9
c [simplification-2] removed 1474 variables 25.0% (4417 remain 24%)
c [simplification-2] removed 6355 irredundant clauses 21.2% (23568 remain 42%)
c [simplification-2] maximum reduction of 25% = max (25%, 21%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1065 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1065 conflicts (hard 11000) hit after 1065 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 67 at-most-one constraints of average size 3.0
c [card-2] found 2 at-most-two constraints of average size 4.5
c [card-2] using previous limit 1000000 for elimination
c [card-2] 69 out of 69 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 26 at-most-one constraints, 24 used 92%
c [card-2] exported 24 binary clauses, 1.0 per/constraint
c [decomp-6] removed 236 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 8362 literals 100%
c [treelook-2] scheduling used 100327 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 305110 steps
c [treelook-2] 8292 literals remain 99%
c [treelook-2] 4181 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 639 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 2 failed, 66 tauts, 0 hbrs, 1844 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 4179 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 124 variables 3% in round 1 in 4670378 steps
c [elim-3-1] backward subsumption/strengthening limit 4670300
c [elim-3-1-1] backward checking 751 touched variables 18%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 3 and strengthened 20 clauses in 245797 steps
c [elim-3-1] rescheduled 68 variables 2% by backward subsumption
c [elim-3-2] eliminated 4 variables 0% in round 2 in 233001 steps
c [elim-3-2] backward subsumption/strengthening limit 233000
c [elim-3-2-1] backward checking 47 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 0 and strengthened 0 clauses in 24913 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 128 = 3% variables out of 4179 scheduled
c [score-dist-3] active 4051 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-3] max exp 509, different 10 (2%)
c [score-dist-3] median active exp 506, avg 505.4
c [simplification-3] removed 366 variables 8.3% (4051 remain 22%)
c [simplification-3] removed 810 irredundant clauses 3.4% (22758 remain 41%)
c [simplification-3] maximum reduction of 8% = max (8%, 3%)
c [simplification-3] large reduction 8% >= 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 13065 (soft 3065 + delta 10000)
c [simplification-3] new conflict limit 3065 (hard 13065)
c 
c [simplification-4] limit 3065 conflicts (hard 13065) hit after 3065 conflicts
c [decomp-8] removed 34 variables
c [basicprobe-2] limit 1000969 penalty 0 = 0 + 0
c [basicprobe-2-0] 1067 sched 27%, 20 failed, 0 lifted, 774 hbrs
c [decomp-9] removed 116 variables
c [basicprobe-2-1] 2096 sched 54%, 19 failed, 0 lifted, 223 hbrs
c [decomp-10] removed 37 variables
c [basicprobe-2-2] 1928 probes remain 50% after last round
c [basicprobe-2-2] 42 units = 42 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 156 variables, found 1009 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 1 failed, 706 tauts, 0 hbrs, 13025 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 3858 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 105 blocked clauses
c [block-1] 105 < 1/100 * 21938 = 219 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 32
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-1-1] eliminated 1 clauses out of 4 (25%) of length 14
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-1-1] eliminated 4 clauses out of 14 (29%) of length 7
c [cce-1-1] eliminated 2 clauses out of 134 (1%) of length 6
c [cce-1-1] eliminated 76 clauses out of 2506 (3%) of length 5
c [cce-1-1] eliminated 137 clauses out of 6282 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 223 large clauses in 14828710 steps
c [cce-1-1] allowing another 7414355 steps for small clauses
c [cce-1-1] scheduling 8689 clauses = 4371 binary + 4318 ternary
c [cce-1-1] tried to eliminate 6694 small clauses 77%
c [cce-1-1] eliminated 83 binary clauses 2%
c [cce-1-1] eliminated 186 ternary clauses 4%
c [cce-1-1] eliminated 269 small clauses 3%
c [cce-1-1] eliminated 269 small clauses in 30000079 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 492 covered clauses in round 1
c [cce-1] eliminated 492 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3858 variables 100%
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 97 variables 3% in round 1 in 4390389 steps
c [elim-4-1] backward subsumption/strengthening limit 4390300
c [elim-4-1-1] backward checking 549 touched variables 14%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 5 clauses in 284519 steps
c [elim-4-1] rescheduled 17 variables 0% by backward subsumption
c [elim-4-2] eliminated 1 variables 0% in round 2 in 129336 steps
c [elim-4-2] backward subsumption/strengthening limit 129300
c [elim-4-2-1] backward checking 9 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 14380 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 98 = 3% variables out of 3858 scheduled
c [bca-1] limit of 10000000 steps and 42818 added (scaled 2)
c [bca-1] 4792 out of 7522 literals actually usable 64%
c [bca-1] added 12 blocked clauses in 12051 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2110 pos 56.1% + 1650 neg 43.9% = 3760 sched 100.0% ret 0
c [sweep-1-1] 1013998 steps 194 queries 71.36 avg class size
c [sweep-1-1] 2352 decisions 191 SAT calls 26.60 avg env size
c [sweep-1-1] 898 variables remain 24% (2861 retained 76%)
c [decomp-11] removed 18 variables
c [sweep-1-1] removed 18 vars (0 failed, 3 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 18 vars in TOTAL (1 rounds, 193 queries)
c [score-dist-4] active 3742 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 510, different 10 (2%)
c [score-dist-4] median active exp 509, avg 509.1
c [simplification-4] removed 309 variables 7.6% (3742 remain 20%)
c [simplification-4] removed 1648 irredundant clauses 7.2% (21110 remain 38%)
c [simplification-4] maximum reduction of 8% = max (8%, 7%)
c [simplification-4] large reduction 8% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15065 (soft 5065 + delta 10000)
c [simplification-4] new conflict limit 5065 (hard 15065)
c 
c [simplification-5] limit 5065 conflicts (hard 15065) hit after 5066 conflicts
c [quatres-1] found 6319 quaternary clauses 68% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 7 single-self-subsuming ternary resolvents
c [quatres-1-2] added 199 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 3742 free variables schedulable
c [ternres-1] 2413 ternary resolvents (32 bin, 2381 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4752 xors of average arity 3.0
c [gauss-1] connected 14208 occurrences of 831 variables (average 17.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-12] removed 12 variables
c [gauss-1] exported 0 unary, 1 binary and 19 ternary equations
c [simpleprobe-3] 91 schedulable variables 2%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-14] removed 6 variables
c [simpleprobe-3] 39 variables remain 1% (3685 retained 99%)
c [simpleprobe-3] removed 6 variables, found 1955 hbrs, 0 units
c [unhide-5] limit 100000 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 36 tauts, 0 hbrs, 7235 literals
c [transred-1] limit 335125 with penalty 0 = 0 + 0
c [transred-1] removed 225 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 9
c [cce-2-1] eliminated 1 clauses out of 14 (7%) of length 7
c [cce-2-1] eliminated 6 clauses out of 2436 (0%) of length 5
c [cce-2-1] eliminated 18 clauses out of 6211 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 28 large clauses in 14209218 steps
c [cce-2-1] allowing another 7104609 steps for small clauses
c [cce-2-1] scheduling 8157 clauses = 4074 binary + 4083 ternary
c [cce-2-1] tried to eliminate 6966 small clauses 85%
c [cce-2-1] eliminated 18 binary clauses 0%
c [cce-2-1] eliminated 61 ternary clauses 1%
c [cce-2-1] eliminated 79 small clauses 1%
c [cce-2-1] eliminated 79 small clauses in 30000003 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 107 covered clauses in round 1
c [cce-2] eliminated 107 covered clauses in TOTAL during 1 rounds
c [cce-2] 107 < 1/100 * 21049 = 210 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3724 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 35 variables 1% in round 1 in 4419808 steps
c [elim-5-1] backward subsumption/strengthening limit 4419800
c [elim-5-1-1] backward checking 261 touched variables 7%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 1 and strengthened 22 clauses in 176587 steps
c [elim-5-1] rescheduled 65 variables 2% by backward subsumption
c [elim-5-2] eliminated 10 variables 0% in round 2 in 366816 steps
c [elim-5-2] backward subsumption/strengthening limit 366800
c [elim-5-2-1] backward checking 59 touched variables 2%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 2 clauses in 34155 steps
c [elim-5-2] rescheduled 7 variables 0% by backward subsumption
c [elim-5-3] eliminated 1 variables 0% in round 3 in 10733 steps
c [elim-5-3] backward subsumption/strengthening limit 10700
c [elim-5-3-1] backward checking 13 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 0 and strengthened 5 clauses in 10701 steps
c [elim-5] incomplete 8 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 46 = 1% variables out of 3724 scheduled
c [bca-2] limit of 10000000 steps and 42184 added (scaled 2)
c [bca-2] 3535 out of 7358 literals actually usable 48%
c [bca-2] added 14 blocked clauses in 10838 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 625 pos 72.4% + 238 neg 27.6% = 863 sched 23.5% ret 2815
c [sweep-2-1] 1012196 steps 99 queries 49.46 avg class size
c [sweep-2-1] 1284 decisions 97 SAT calls 25.13 avg env size
c [sweep-2-1] 284 variables remain 8% (3394 retained 92%)
c [decomp-15] removed 3 variables
c [sweep-2-1] removed 3 vars (0 failed, 1 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 3 vars in TOTAL (1 rounds, 98 queries)
c [score-dist-5] active 3675 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-5] max exp 510, different 13 (3%)
c [score-dist-5] median active exp 508, avg 507.8
c [simplification-5] removed 67 variables 1.8% (3675 remain 20%)
c [simplification-5] removed 278 irredundant clauses 1.3% (20832 remain 37%)
c [simplification-5] maximum reduction of 2% = max (2%, 1%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 6666
c [simplification-5] penalized conflict interval 6666 = 1 * 6666
c [simplification-5] hard conflict limit 21732 (soft 11732 + delta 10000)
c [simplification-5] new conflict limit 11732 (hard 21732)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    6.1    3674    20832      7012    4154   2615  4313   26    37    5  69%     89   34   29    3  932%
c 
c [simplification-6] limit 11732 conflicts (hard 21732) hit after 11734 conflicts
c [quatres-2] found 6582 quaternary clauses 67% in total
c [quatres-2-2] added 17 single-self-subsuming ternary resolvents
c [quatres-2-2] added 114 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3674 free variables schedulable
c [ternres-2] 330 ternary resolvents (1 bin, 329 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 38 at-most-one constraints of average size 3.0
c [card-3] found 6 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 44 out of 44 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 15 at-most-one constraints, 5 used 33%
c [card-3] exported 5 binary clauses, 1.0 per/constraint
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 4571 xors of average arity 3.0
c [gauss-2] connected 13715 occurrences of 782 variables (average 17.5)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-2] limit 1089548 with penalty 0 = 0 + 0
c [transred-2] removed 200 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3674 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 3674 variables 100%
c [elim-6] limit of 21790968 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 10 variables 0% in round 1 in 4406367 steps
c [elim-6-1] backward subsumption/strengthening limit 4406300
c [elim-6-1-1] backward checking 150 touched variables 4%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 2 and strengthened 10 clauses in 94726 steps
c [elim-6-1] rescheduled 37 variables 1% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 309791 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 10 = 0% variables out of 3674 scheduled
c [elim-6] 10 < 1/100 * 3674 = 36 considered unsuccessful
c [bca-3] limit of 10000000 steps and 42111 added (scaled 2)
c [bca-3] 3430 out of 7330 literals actually usable 47%
c [bca-3] added 2 blocked clauses in 11839 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 149 pos 53.0% + 132 neg 47.0% = 281 sched 7.7% ret 3383
c [sweep-3-1] 1016949 steps 110 queries 13.69 avg class size
c [sweep-3-1] 1601 decisions 105 SAT calls 26.97 avg env size
c [sweep-3-1] 30 variables remain 1% (3633 retained 99%)
c [decomp-17] removed 17 variables
c [sweep-3-1] removed 17 vars (0 failed, 8 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 17 vars in TOTAL (1 rounds, 109 queries)
c [score-dist-6] active 3647 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 510, different 18 (4%)
c [score-dist-6] median active exp 509, avg 508.4
c [simplification-6] removed 27 variables 0.7% (3647 remain 20%)
c [simplification-6] removed 70 irredundant clauses 0.3% (20762 remain 37%)
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 16666
c [simplification-6] penalized conflict interval 16666 = 1 * 16666
c [simplification-6] hard conflict limit 38400 (soft 28400 + delta 10000)
c [simplification-6] new conflict limit 28400 (hard 38400)
c 
c [simplification-7] limit 28400 conflicts (hard 38400) hit after 28404 conflicts
c [quatres-3] found 6764 quaternary clauses 65% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 25 single-self-subsuming ternary resolvents
c [quatres-3-2] added 78 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3647 free variables schedulable
c [ternres-3] 121 ternary resolvents (2 bin, 119 trn)
c [ternres-3] fully completed ternary resolution
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 7294 literals 100%
c [treelook-3] scheduling used 134079 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 151064 steps
c [treelook-3] 7278 literals remain 100%
c [treelook-3] 3647 variables remain to probed next time 100%
c [treelook-3] removed 0 variables, found 271 hbrs
c [unhide-6] limit 268710 with penalty 1 = 1 + 0
c [unhide-6-6] 0 units, 17 failed, 2285 tauts, 0 hbrs, 34130 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 184 transitive binary clauses
c [transred-3] found 1 units
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 19
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 18
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 13
c [cce-3-1] eliminated 1 clauses out of 10 (10%) of length 7
c [cce-3-1] eliminated 12 clauses out of 139 (9%) of length 6
c [cce-3-1] eliminated 56 clauses out of 2222 (3%) of length 5
c [cce-3-1] eliminated 70 clauses out of 6188 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 146 large clauses in 14476101 steps
c [cce-3-1] allowing another 7238050 steps for small clauses
c [cce-3-1] scheduling 8094 clauses = 4098 binary + 3996 ternary
c [cce-3-1] tried to eliminate 3915 small clauses 48%
c [cce-3-1] eliminated 15 binary clauses 0%
c [cce-3-1] eliminated 46 ternary clauses 1%
c [cce-3-1] eliminated 61 small clauses 1%
c [cce-3-1] eliminated 87 small clauses in 15000124 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 233 covered clauses in round 1
c [cce-3] eliminated 233 covered clauses in TOTAL during 1 rounds
c [bca-4] limit of 10000000 steps and 41518 added (scaled 2)
c [bca-4] 2873 out of 7282 literals actually usable 39%
c [bca-4] added 18 blocked clauses in 18862 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 15 pos 55.6% + 12 neg 44.4% = 27 sched 0.7% ret 3613
c [sweep-4-1] 179281 steps 18 queries 6.17 avg class size
c [sweep-4-1] 285 decisions 16 SAT calls 30.50 avg env size
c [sweep-4-1] fully completed sweeping round
c [decomp-20] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-4-2] 1750 pos 48.1% + 1888 neg 51.9% = 3638 sched 100.0% ret 0
c [sweep-4-2] 842652 steps 47 queries 201.53 avg class size
c [sweep-4-2] 1160 decisions 45 SAT calls 55.47 avg env size
c [sweep-4-2] 2767 variables remain 76% (871 retained 24%)
c [decomp-21] removed 2 variables
c [sweep-4-2] removed 2 vars (0 failed, 1 eqs, 2 impls)
c [sweep-4] removed 4 vars in TOTAL (2 rounds, 63 queries)
c [score-dist-7] active 3636 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 510, different 23 (5%)
c [score-dist-7] median active exp 509, avg 508.6
c [simplification-7] removed 11 variables 0.3% (3636 remain 20%)
c [simplification-7] removed 262 irredundant clauses 1.3% (20500 remain 37%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 26666
c [simplification-7] penalized conflict interval 26666 = 1 * 26666
c [simplification-7] hard conflict limit 68403 (soft 55070 + delta 13333)
c [simplification-7] new conflict limit 55070 (hard 68403)
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   32.0    3635    20500     54380   26944   2692  2698   21    25   13  83%    516   10   23   12  185%
c 
c [simplification-8] limit 55070 conflicts (hard 68403) hit after 55074 conflicts
c [quatres-4] found 6689 quaternary clauses 65% in total
c [quatres-4-2] added 26 single-self-subsuming ternary resolvents
c [quatres-4-2] added 56 quaternary resolvents
c [ternres-4] limit 6111819 with penalty 0 = 0 + 0
c [ternres-4] all 3630 free variables schedulable
c [ternres-4] 196 ternary resolvents (4 bin, 192 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 4552 xors of average arity 3.0
c [gauss-3] connected 13652 occurrences of 769 variables (average 17.8)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 3 ternary equations
c [decomp-22] removed 2 variables
c [basicprobe-3] limit 30559096 penalty 0 = 0 + 0
c [basicprobe-3-0] 1873 sched 52%, 5 failed, 0 lifted, 286 hbrs
c [decomp-23] removed 10 variables
c [basicprobe-3-1] 1995 sched 55%, 2 failed, 0 lifted, 40 hbrs
c [decomp-24] removed 2 variables
c [basicprobe-3-2] 1997 sched 55%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-3-3] 1996 sched 55%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-4] 1996 sched 55%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-3-5] 1996 sched 55%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-6] 1996 sched 55%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-6] fully completed probing
c [basicprobe-3-6] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-3-6] removed 12 variables, found 349 hbrs
c [bate-1] eliminated 17 asymmetric tautologies during probing
c [unhide-7] limit 1222363 with penalty 0 = 0 + 0
c [unhide-7-9] 0 units, 0 failed, 945 tauts, 0 hbrs, 91860 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 156 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 305590960 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-4-1] eliminated 2 clauses out of 109 (2%) of length 6
c [cce-4-1] eliminated 3 clauses out of 2101 (0%) of length 5
c [cce-4-1] eliminated 6 clauses out of 6052 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 12 large clauses in 13539571 steps
c [cce-4-1] allowing another 6769785 steps for small clauses
c [cce-4-1] scheduling 8122 clauses = 4148 binary + 3974 ternary
c [cce-4-1] tried to eliminate 8122 small clauses 100%
c [cce-4-1] eliminated 16 binary clauses 0%
c [cce-4-1] eliminated 87 ternary clauses 2%
c [cce-4-1] eliminated 103 small clauses 1%
c [cce-4-1] eliminated 103 small clauses in 31506242 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 115 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 6717505 steps for small clauses
c [cce-4-2] scheduling 8019 clauses = 4132 binary + 3887 ternary
c [cce-4-2] tried to eliminate 8019 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 115 covered clauses in TOTAL during 2 rounds
c [cce-4] 115 < 1/100 * 20366 = 203 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 3616 variables 100%
c [elim-7] limit of 61118192 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 48 variables 1% in round 1 in 3972474 steps
c [elim-7-1] backward subsumption/strengthening limit 3972400
c [elim-7-1-1] backward checking 297 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 33 clauses in 129317 steps
c [elim-7-1] rescheduled 81 variables 2% by backward subsumption
c [elim-7-2] eliminated 3 variables 0% in round 2 in 207522 steps
c [elim-7-2] backward subsumption/strengthening limit 207500
c [elim-7-2-1] backward checking 54 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 21345 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 51 = 1% variables out of 3616 scheduled
c [bca-5] limit of 10000000 steps and 40709 added (scaled 2)
c [bca-5] 2446 out of 7132 literals actually usable 34%
c [bca-5] added 21 blocked clauses in 30666 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 18335450 penalty 0 = 0 + 0
c [sweep-5-1] 1495 pos 55.3% + 1209 neg 44.7% = 2704 sched 75.8% ret 861
c [sweep-5-1] 7657655 steps 218 queries 33.50 avg class size
c [sweep-5-1] 4997 decisions 212 SAT calls 47.55 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-29] removed 10 variables
c [sweep-5-1] removed 10 vars (0 failed, 8 eqs, 5 impls)
c [sweep-5-2] 1781 pos 50.1% + 1774 neg 49.9% = 3555 sched 100.0% ret 0
c [sweep-5-2] 6320820 steps 232 queries 35.27 avg class size
c [sweep-5-2] 5196 decisions 226 SAT calls 51.54 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-30] removed 7 variables
c [sweep-5-2] removed 7 vars (0 failed, 7 eqs, 12 impls)
c [sweep-5-3] 1777 pos 50.1% + 1771 neg 49.9% = 3548 sched 100.0% ret 0
c [sweep-5-3] 4361655 steps 96 queries 88.83 avg class size
c [sweep-5-3] 2757 decisions 94 SAT calls 72.65 avg env size
c [sweep-5-3] 1053 variables remain 30% (2495 retained 70%)
c [decomp-31] removed 1 variables
c [sweep-5-3] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-5] removed 18 vars in TOTAL (3 rounds, 543 queries)
c [score-dist-8] active 3547 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 512, different 9 (2%)
c [score-dist-8] median active exp 509, avg 509.2
c [simplification-8] removed 83 variables 2.3% (3547 remain 19%)
c [simplification-8] removed 415 irredundant clauses 2.0% (20085 remain 36%)
c [simplification-8] maximum reduction of 2% = max (2%, 2%)
c [simplification-8] geometric conflict interval increment 8888 = 26666 / 3
c [simplification-8] new conflict interval 35554
c [simplification-8] penalized conflict interval 35554 = 1 * 35554
c [simplification-8] hard conflict limit 108405 (soft 90628 + delta 17777)
c [simplification-8] new conflict limit 90628 (hard 108405)
c 
c [simplification-9] limit 90628 conflicts (hard 108405) hit after 90630 conflicts
c [quatres-5] found 6772 quaternary clauses 61% in total
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 48 single-self-subsuming ternary resolvents
c [quatres-5-2] added 101 quaternary resolvents
c [ternres-5] limit 11739347 with penalty 0 = 0 + 0
c [ternres-5] all 3547 free variables schedulable
c [ternres-5] 389 ternary resolvents (7 bin, 382 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 2347869 penalty 0 = 0 + 0
c [gauss-4] extracted 4448 xors of average arity 3.0
c [gauss-4] connected 13334 occurrences of 747 variables (average 17.9)
c [gauss-4] limit 2347869 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 39 schedulable variables 1%
c [simpleprobe-4] limit 46957390 penalty 0 = 0 + 0
c [decomp-33] removed 3 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 3 variables, found 281 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 298 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3544 variables 100%
c [block-3] limit of 29348368 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 9 blocked clauses
c [block-3] 9 < 1/100 * 20047 = 200 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 3544 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4695739020 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 16 variables 0% in round 1 in 4344168 steps
c [elim-8-1] backward subsumption/strengthening limit 4344100
c [elim-8-1-1] backward checking 217 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 2 and strengthened 25 clauses in 192169 steps
c [elim-8-1] rescheduled 64 variables 2% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 693647 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 16 = 0% variables out of 3544 scheduled
c [elim-8] 16 < 1/100 * 3544 = 35 considered unsuccessful
c [bca-6] limit of 10000000 steps and 40417 added (scaled 2)
c [bca-6] 1776 out of 7058 literals actually usable 25%
c [bca-6] added 0 blocked clauses in 51759 steps
c [sweep-6] limit 3521804 penalty 0 = 0 + 0
c [sweep-6-1] 534 pos 51.3% + 506 neg 48.7% = 1040 sched 29.5% ret 2488
c [sweep-6-1] 4228109 steps 33 queries 134.24 avg class size
c [sweep-6-1] 1480 decisions 31 SAT calls 101.35 avg env size
c [sweep-6-1] 779 variables remain 22% (2749 retained 78%)
c [decomp-34] removed 1 variables
c [sweep-6-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-6] 1 < 1/1000 * 3528 = 3 considered unsuccessful
c [sweep-6] removed 1 vars in TOTAL (1 rounds, 32 queries)
c [score-dist-9] active 3527 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 510, different 13 (3%)
c [score-dist-9] median active exp 508, avg 507.8
c [simplification-9] removed 20 variables 0.6% (3527 remain 19%)
c [simplification-9] removed 143 irredundant clauses 0.7% (19942 remain 36%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 17777 = 35554 / 2
c [simplification-9] new conflict interval 53331
c [simplification-9] penalized conflict interval 53331 = 1 * 53331
c [simplification-9] hard conflict limit 170626 (soft 143961 + delta 26665)
c [simplification-9] new conflict limit 143961 (hard 170626)
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 -   60.5    3527    19942    100522   26421   2820  2798   20    22   10  92%    401    2   21   17  124%
c -   87.5    3527    19942    149218   28765   2828  2799   16    19   15  82%    728   -1   20   17  113%
c 
c [simplification-10] limit 143961 conflicts (hard 170626) hit after 149643 conflicts
c [quatres-6] found 6854 quaternary clauses 59% in total
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 21 single-self-subsuming ternary resolvents
c [quatres-6-2] added 38 quaternary resolvents
c [ternres-6] limit 21736536 with penalty 0 = 0 + 0
c [ternres-6] all 3527 free variables schedulable
c [ternres-6] 135 ternary resolvents (8 bin, 127 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1358533 penalty 3 = 3 + 0
c [card-4] found 39 at-most-one constraints of average size 3.1
c [card-4] found 42 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1358533 for elimination
c [card-4] 80 out of 81 constraints (99%) meet size limits
c [card-4] no units found
c [card-4] generated 43 at-most-one constraints, 9 used 21%
c [card-4] exported 9 binary clauses, 1.0 per/constraint
c [unhide-8] limit 2173653 with penalty 1 = 1 + 0
c [unhide-8-13] 0 units, 0 failed, 1067 tauts, 0 hbrs, 74286 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 132 transitive binary clauses
c [cce-5] limit of 54341342 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 31
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-5-1] eliminated 2 clauses out of 8 (25%) of length 7
c [cce-5-1] eliminated 8 clauses out of 92 (9%) of length 6
c [cce-5-1] eliminated 32 clauses out of 1927 (2%) of length 5
c [cce-5-1] eliminated 83 clauses out of 5898 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 133 large clauses in 14202400 steps
c [cce-5-1] allowing another 7101200 steps for small clauses
c [cce-5-1] scheduling 7942 clauses = 4058 binary + 3884 ternary
c [cce-5-1] tried to eliminate 7942 small clauses 100%
c [cce-5-1] eliminated 59 binary clauses 1%
c [cce-5-1] eliminated 57 ternary clauses 1%
c [cce-5-1] eliminated 116 small clauses 1%
c [cce-5-1] eliminated 116 small clauses in 21977899 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 249 covered clauses in round 1
c [cce-5-2] eliminated 5 clauses out of 1895 (0%) of length 5
c [cce-5-2] eliminated 9 clauses out of 5815 (0%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 14 large clauses in 13636511 steps
c [cce-5-2] allowing another 6818255 steps for small clauses
c [cce-5-2] scheduling 7826 clauses = 3999 binary + 3827 ternary
c [cce-5-2] tried to eliminate 7826 small clauses 100%
c [cce-5-2] eliminated 2 binary clauses 0%
c [cce-5-2] eliminated 2 small clauses 0%
c [cce-5-2] eliminated 2 small clauses in 21255620 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 16 covered clauses in round 2
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] allowing another 5553970 steps for small clauses
c [cce-5-3] scheduling 7824 clauses = 3997 binary + 3827 ternary
c [cce-5-3] tried to eliminate 2917 small clauses 37%
c [cce-5-3] incomplete small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 265 covered clauses in TOTAL during 3 rounds
c [score-dist-10] active 3527 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 510, different 23 (5%)
c [score-dist-10] median active exp 508, avg 506.6
c [simplification-10] removed 0 variables 0.0% (3527 remain 19%)
c [simplification-10] removed 303 irredundant clauses 1.5% (19639 remain 35%)
c [simplification-10] maximum reduction of 2% = max (0%, 2%)
c [simplification-10] geometric conflict interval increment 17777 = 53331 / 3
c [simplification-10] new conflict interval 71108
c [simplification-10] penalized conflict interval 71108 = 1 * 71108
c [simplification-10] hard conflict limit 256305 (soft 220751 + delta 35554)
c [simplification-10] new conflict limit 220751 (hard 256305)
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 -  120.7    3527    19639    220031   29292   2601  2011   14    14   17  97%    923   -4   13   16   83%
c 
c [simplification-11] limit 220751 conflicts (hard 256305) hit after 224641 conflicts
c [quatres-7] found 6683 quaternary clauses 58% in total
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 26 single-self-subsuming ternary resolvents
c [quatres-7-2] added 34 quaternary resolvents
c [ternres-7] limit 33287112 with penalty 0 = 0 + 0
c [ternres-7] all 3527 free variables schedulable
c [ternres-7] 76 ternary resolvents (6 bin, 70 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-5] limit 3328711 penalty 1 = 1 + 0
c [gauss-5] extracted 4428 xors of average arity 3.0
c [gauss-5] connected 13284 occurrences of 737 variables (average 18.0)
c [gauss-5] limit 3328711 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 68 transitive binary clauses
c [cce-6] limit of 166435564 steps penalty 0 = 0 + 0
c [cce-6-1] completed large round (ATE)
c [cce-6-1] allowing another 6577778 steps for small clauses
c [cce-6-1] scheduling 8014 clauses = 3997 binary + 4017 ternary
c [cce-6-1] tried to eliminate 8014 small clauses 100%
c [cce-6-1] eliminated 69 ternary clauses 2%
c [cce-6-1] eliminated 69 small clauses 1%
c [cce-6-1] eliminated 69 small clauses in 30143897 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 69 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 6565942 steps for small clauses
c [cce-6-2] scheduling 7945 clauses = 3997 binary + 3948 ternary
c [cce-6-2] tried to eliminate 7945 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 69 covered clauses in TOTAL during 2 rounds
c [cce-6] 69 < 1/100 * 19639 = 196 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 3527 variables 100%
c [elim-9] limit of 332871128 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 36 variables 1% in round 1 in 3903577 steps
c [elim-9-1] backward subsumption/strengthening limit 3903500
c [elim-9-1-1] backward checking 203 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 1 and strengthened 18 clauses in 107711 steps
c [elim-9-1] rescheduled 63 variables 2% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 103245 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 36 = 1% variables out of 3527 scheduled
c [bca-7] limit of 10000000 steps and 39503 added (scaled 2)
c [bca-7] 2202 out of 6984 literals actually usable 32%
c [bca-7] added 41 blocked clauses in 34860 steps
c [sweep-7] limit 4993066 penalty 1 = 1 + 0
c [sweep-7-1] 513 pos 66.9% + 254 neg 33.1% = 767 sched 22.0% ret 2724
c [sweep-7-1] 1806369 steps 134 queries 19.41 avg class size
c [sweep-7-1] 1244 decisions 130 SAT calls 30.21 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-37] removed 5 variables
c [sweep-7-1] removed 5 vars (0 failed, 5 eqs, 5 impls)
c [sweep-7-2] 1866 pos 53.5% + 1620 neg 46.5% = 3486 sched 100.0% ret 0
c [sweep-7-2] 3204046 steps 163 queries 48.10 avg class size
c [sweep-7-2] 3036 decisions 160 SAT calls 48.23 avg env size
c [sweep-7-2] 320 variables remain 9% (3166 retained 91%)
c [decomp-38] removed 6 variables
c [sweep-7-2] removed 6 vars (0 failed, 4 eqs, 4 impls)
c [sweep-7] removed 11 vars in TOTAL (2 rounds, 295 queries)
c [score-dist-11] active 3480 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-11] max exp 511, different 17 (3%)
c [score-dist-11] median active exp 508, avg 507.8
c [simplification-11] removed 47 variables 1.3% (3480 remain 19%)
c [simplification-11] removed 157 irredundant clauses 0.8% (19482 remain 35%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 35554 = 71108 / 2
c [simplification-11] new conflict interval 106662
c [simplification-11] penalized conflict interval 106662 = 1 * 106662
c [simplification-11] hard conflict limit 384634 (soft 331303 + delta 53331)
c [simplification-11] new conflict limit 331303 (hard 384634)
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 -  148.1    3480    19482    278143   29141   2657  2134   12    16   15  78%    983   -2   13   15   86%
c -  166.2    3480    19482    329259   30839   2672  2134   13    16   16  85%   1005   -2   13   14   91%
c 
c [simplification-12] limit 331303 conflicts (hard 384634) hit after 384634 conflicts
c [quatres-8] found 6789 quaternary clauses 52% in total
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 27 single-self-subsuming ternary resolvents
c [quatres-8-2] added 64 quaternary resolvents
c [ternres-8] limit 54601451 with penalty 0 = 0 + 0
c [ternres-8] all 3480 free variables schedulable
c [ternres-8] 360 ternary resolvents (9 bin, 351 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-39] removed 1 variables
c [treelook-4] limit 1365036 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 6958 literals 100%
c [treelook-4] scheduling used 193089 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1365036 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 1365433 steps
c [treelook-4] 6200 literals remain 89%
c [treelook-4] 3456 variables remain to probed next time 99%
c [decomp-40] removed 2 variables
c [treelook-4] removed 2 variables, found 2945 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 235 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 3477 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 12 variables 0% in round 1 in 4221377 steps
c [elim-10-1] backward subsumption/strengthening limit 4221300
c [elim-10-1-1] backward checking 96 touched variables 3%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 2 clauses in 70695 steps
c [elim-10-1] rescheduled 41 variables 1% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 253024 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 12 = 0% variables out of 3477 scheduled
c [elim-10] 12 < 1/100 * 3477 = 34 considered unsuccessful
c [bca-8] limit of 10000000 steps and 39340 added (scaled 2)
c [bca-8] 1950 out of 6932 literals actually usable 28%
c [bca-8] added 4 blocked clauses in 47425 steps
c [sweep-8] limit 16380435 penalty 0 = 0 + 0
c [sweep-8-1] 223 pos 71.0% + 91 neg 29.0% = 314 sched 9.1% ret 3151
c [sweep-8-1] 3363954 steps 96 queries 11.48 avg class size
c [sweep-8-1] 1726 decisions 95 SAT calls 49.54 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-41] removed 8 variables
c [sweep-8-1] removed 8 vars (0 failed, 4 eqs, 2 impls)
c [sweep-8-2] 1693 pos 49.0% + 1764 neg 51.0% = 3457 sched 100.0% ret 0
c [sweep-8-2] 6782943 steps 220 queries 34.40 avg class size
c [sweep-8-2] 4211 decisions 218 SAT calls 70.17 avg env size
c [sweep-8-2] fully completed sweeping round
c [decomp-42] removed 5 variables
c [sweep-8-2] removed 5 vars (0 failed, 4 eqs, 4 impls)
c [sweep-8-3] 1693 pos 49.0% + 1759 neg 51.0% = 3452 sched 100.0% ret 0
c [sweep-8-3] 5958190 steps 216 queries 40.29 avg class size
c [sweep-8-3] 4347 decisions 215 SAT calls 53.73 avg env size
c [sweep-8-3] fully completed sweeping round
c [decomp-43] removed 4 variables
c [sweep-8-3] removed 4 vars (0 failed, 3 eqs, 4 impls)
c [sweep-8] removed 17 vars in TOTAL (3 rounds, 529 queries)
c [score-dist-12] active 3448 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-12] max exp 512, different 16 (3%)
c [score-dist-12] median active exp 508, avg 507.8
c [simplification-12] removed 32 variables 0.9% (3448 remain 19%)
c [simplification-12] removed 120 irredundant clauses 0.6% (19362 remain 35%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 53331 = 106662 / 2
c [simplification-12] new conflict interval 159993
c [simplification-12] penalized conflict interval 159993 = 1 * 159993
c [simplification-12] hard conflict limit 624623 (soft 544627 + delta 79996)
c [simplification-12] new conflict limit 544627 (hard 624623)
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 -  210.6    3448    19362    421052   32519   3094  4929   18    20   16  89%   1019    3   20   15  134%
c -  235.7    3448    19362    468931   32650   3095  4930   17    18   16  96%   1022    0   18   15  114%
c -  271.4    3448    19362    530460   33285   3101  4930   13    15   16  90%   1023   -2   12   15   78%
c 
c [simplification-13] limit 544627 conflicts (hard 624623) hit after 544629 conflicts
c [quatres-9] found 6958 quaternary clauses 47% in total
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 34 single-self-subsuming ternary resolvents
c [quatres-9-2] added 37 quaternary resolvents
c [ternres-9] limit 83188531 with penalty 0 = 0 + 0
c [ternres-9] all 3448 free variables schedulable
c [ternres-9] 981 ternary resolvents (2 bin, 979 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 1822 sched 53%, 0 failed, 0 lifted, 127 hbrs
c [basicprobe-4-1] 1817 sched 53%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-2] 1818 sched 53%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-3] 1818 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-4] 1818 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-4] fully completed probing
c [basicprobe-4-4] removed 0 variables, found 133 hbrs
c [bate-2] eliminated 5 asymmetric tautologies during probing
c [unhide-9] limit 4159426 with penalty 2 = 2 + 0
c [unhide-9-19] 0 units, 0 failed, 1862 tauts, 0 hbrs, 127208 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 123 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3448 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 6 blocked clauses
c [block-4] 6 < 1/100 * 19205 = 192 considered unsuccessful
c [cce-7] limit of 207971328 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 28
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 27
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 26
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 12
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 8
c [cce-7-1] eliminated 5 clauses out of 68 (7%) of length 6
c [cce-7-1] eliminated 17 clauses out of 1675 (1%) of length 5
c [cce-7-1] eliminated 80 clauses out of 5599 (1%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 118 large clauses in 13448900 steps
c [cce-7-1] allowing another 6724450 steps for small clauses
c [cce-7-1] scheduling 7924 clauses = 4069 binary + 3855 ternary
c [cce-7-1] tried to eliminate 7924 small clauses 100%
c [cce-7-1] eliminated 130 binary clauses 3%
c [cce-7-1] eliminated 81 ternary clauses 2%
c [cce-7-1] eliminated 211 small clauses 3%
c [cce-7-1] eliminated 211 small clauses in 25293584 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 329 covered clauses in round 1
c [cce-7-2] eliminated 3 clauses out of 63 (5%) of length 6
c [cce-7-2] eliminated 4 clauses out of 1658 (0%) of length 5
c [cce-7-2] eliminated 11 clauses out of 5519 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 18 large clauses in 12305475 steps
c [cce-7-2] allowing another 6152737 steps for small clauses
c [cce-7-2] scheduling 7713 clauses = 3939 binary + 3774 ternary
c [cce-7-2] tried to eliminate 7713 small clauses 100%
c [cce-7-2] eliminated 1 binary clauses 0%
c [cce-7-2] eliminated 7 ternary clauses 0%
c [cce-7-2] eliminated 8 small clauses 0%
c [cce-7-2] eliminated 8 small clauses in 23760877 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 26 covered clauses in round 2
c [cce-7-3] eliminated 6 clauses out of 5508 (0%) of length 4
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] eliminated 6 large clauses in 12277390 steps
c [cce-7-3] allowing another 6138695 steps for small clauses
c [cce-7-3] scheduling 7705 clauses = 3938 binary + 3767 ternary
c [cce-7-3] tried to eliminate 7705 small clauses 100%
c [cce-7-3] eliminated 1 binary clauses 0%
c [cce-7-3] eliminated 1 small clauses 0%
c [cce-7-3] eliminated 1 small clauses in 23721721 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 7 covered clauses in round 3
c [cce-7] eliminated 362 covered clauses in TOTAL during 3 rounds
c [bca-9] limit of 10000000 steps and 38230 added (scaled 2)
c [bca-9] 1852 out of 6898 literals actually usable 27%
c [bca-9] added 31 blocked clauses in 45292 steps
c [sweep-9] limit 24956559 penalty 0 = 0 + 0
c [sweep-9-1] 1628 pos 47.2% + 1820 neg 52.8% = 3448 sched 100.0% ret 0
c [sweep-9-1] 8543084 steps 186 queries 42.48 avg class size
c [sweep-9-1] 3749 decisions 182 SAT calls 60.08 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-49] removed 7 variables
c [sweep-9-1] removed 7 vars (0 failed, 7 eqs, 2 impls)
c [sweep-9-2] 1627 pos 47.3% + 1814 neg 52.7% = 3441 sched 100.0% ret 0
c [sweep-9-2] 5180851 steps 191 queries 60.36 avg class size
c [sweep-9-2] 3483 decisions 191 SAT calls 50.80 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-50] removed 2 variables
c [sweep-9-2] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-9-3] 1627 pos 47.3% + 1812 neg 52.7% = 3439 sched 100.0% ret 0
c [sweep-9-3] 5788935 steps 202 queries 33.28 avg class size
c [sweep-9-3] 4214 decisions 201 SAT calls 50.55 avg env size
c [sweep-9-3] fully completed sweeping round
c [decomp-51] removed 2 variables
c [sweep-9-3] removed 2 vars (0 failed, 2 eqs, 2 impls)
c [sweep-9] removed 11 vars in TOTAL (3 rounds, 576 queries)
c [score-dist-13] active 3437 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-13] max exp 512, different 11 (2%)
c [score-dist-13] median active exp 509, avg 508.8
c [simplification-13] removed 11 variables 0.3% (3437 remain 18%)
c [simplification-13] removed 543 irredundant clauses 2.8% (18819 remain 34%)
c [simplification-13] maximum reduction of 3% = max (0%, 3%)
c [simplification-13] geometric conflict interval increment 39998 = 159993 / 4
c [simplification-13] new conflict interval 199991
c [simplification-13] penalized conflict interval 199991 = 1 * 199991
c [simplification-13] hard conflict limit 844615 (soft 744620 + delta 99995)
c [simplification-13] new conflict limit 744620 (hard 844615)
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 -  302.3    3437    18819    594738   34020   3761  3672   12    14   16  81%   1024   -2   13   14   92%
c -  329.7    3437    18819    676625   37024   3770  3672   13    13   20  96%   1024   -1   13   13  100%
c 
c [simplification-14] limit 744620 conflicts (hard 844615) hit after 758255 conflicts
c [quatres-10] found 6987 quaternary clauses 43% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 88 single-self-subsuming ternary resolvents
c [quatres-10-2] added 60 quaternary resolvents
c [ternres-10] limit 113069626 with penalty 0 = 0 + 0
c [ternres-10] all 3437 free variables schedulable
c [ternres-10] 895 ternary resolvents (12 bin, 883 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-6] limit 5653481 penalty 2 = 2 + 0
c [gauss-6] extracted 4296 xors of average arity 3.0
c [gauss-6] connected 12894 occurrences of 705 variables (average 18.3)
c [gauss-6] limit 5653481 penalty 2 = 2 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 5 ternary equations
c [simpleprobe-5] all 3437 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-53] removed 1 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1 variables, found 2339 hbrs, 1 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 186 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 5653481330 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 31
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-8-1] eliminated 1 clauses out of 1642 (0%) of length 5
c [cce-8-1] eliminated 19 clauses out of 5451 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 23 large clauses in 11950557 steps
c [cce-8-1] allowing another 5975278 steps for small clauses
c [cce-8-1] scheduling 7771 clauses = 3876 binary + 3895 ternary
c [cce-8-1] tried to eliminate 7771 small clauses 100%
c [cce-8-1] eliminated 30 binary clauses 1%
c [cce-8-1] eliminated 18 ternary clauses 0%
c [cce-8-1] eliminated 48 small clauses 1%
c [cce-8-1] eliminated 48 small clauses in 17936694 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 71 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 5910269 steps for small clauses
c [cce-8-2] scheduling 7723 clauses = 3846 binary + 3877 ternary
c [cce-8-2] tried to eliminate 7723 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 71 covered clauses in TOTAL during 2 rounds
c [cce-8] 71 < 1/100 * 18737 = 187 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 3436 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 63 variables 2% in round 1 in 4273166 steps
c [elim-11-1] backward subsumption/strengthening limit 4273100
c [elim-11-1-1] backward checking 416 touched variables 12%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 20 clauses in 231872 steps
c [elim-11-1] rescheduled 34 variables 1% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 275264 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 63 = 2% variables out of 3436 scheduled
c [bca-10] limit of 10000000 steps and 37603 added (scaled 2)
c [bca-10] 1706 out of 6748 literals actually usable 25%
c [bca-10] added 5 blocked clauses in 65477 steps
c [sweep-10] limit 33920887 penalty 0 = 0 + 0
c [sweep-10-1] 1879 pos 55.7% + 1494 neg 44.3% = 3373 sched 100.0% ret 0
c [sweep-10-1] 9247651 steps 199 queries 41.82 avg class size
c [sweep-10-1] 4372 decisions 199 SAT calls 68.33 avg env size
c [sweep-10-1] fully completed sweeping round
c [sweep-10-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-10-2] 1879 pos 55.7% + 1494 neg 44.3% = 3373 sched 100.0% ret 0
c [sweep-10-2] 9579219 steps 209 queries 36.14 avg class size
c [sweep-10-2] 4011 decisions 208 SAT calls 52.12 avg env size
c [sweep-10-2] fully completed sweeping round
c [sweep-10-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-10-3] 1879 pos 55.7% + 1494 neg 44.3% = 3373 sched 100.0% ret 0
c [sweep-10-3] 9041476 steps 207 queries 35.49 avg class size
c [sweep-10-3] 3900 decisions 207 SAT calls 66.36 avg env size
c [sweep-10-3] fully completed sweeping round
c [decomp-56] removed 3 variables
c [sweep-10-3] removed 3 vars (0 failed, 2 eqs, 1 impls)
c [sweep-10] removed 3 vars in TOTAL (3 rounds, 612 queries)
c [sort-queue-3] sorted 4 enqueued variables after 758255 conflicts
c [score-dist-14] active 3366 (100%), one 4 (0%), zero 0 (0%)
c [score-dist-14] max exp 512, different 13 (3%)
c [score-dist-14] median active exp 507, avg 507.5
c [simplification-14] removed 67 variables 1.9% (3370 remain 18%)
c [simplification-14] removed 309 irredundant clauses 1.6% (18510 remain 33%)
c [simplification-14] maximum reduction of 2% = max (2%, 2%)
c [simplification-14] geometric conflict interval increment 66663 = 199991 / 3
c [simplification-14] new conflict interval 266654
c [simplification-14] penalized conflict interval 266654 = 1 * 266654
c [simplification-14] hard conflict limit 1158236 (soft 1024909 + delta 133327)
c [simplification-14] new conflict limit 1024909 (hard 1158236)
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 -  365.4    3370    18510    765821   38018   4123  4382   18    20   10  91%   1024    7   19   13  142%
c -  391.7    3370    18510    811476   37600   4124  4382   16    19   16  84%   1024    2   15   15   98%
c -  429.0    3370    18510    879196   39358   4130  4382   16    17   18  93%   1024   -1   15   17   88%
c -  467.9    3370    18510    956053   38539   4135  4382   13    14   22  94%   1024   -2   12   15   81%
c 
c [simplification-15] limit 1024909 conflicts (hard 1158236) hit after 1050244 conflicts
c [quatres-11] found 7103 quaternary clauses 42% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 58 single-self-subsuming ternary resolvents
c [quatres-11-2] added 134 quaternary resolvents
c [ternres-11] limit 166673465 with penalty 0 = 0 + 0
c [ternres-11] all 3370 free variables schedulable
c [ternres-11] 444 ternary resolvents (4 bin, 440 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 5208545 penalty 4 = 4 + 0
c [card-5] found 198 at-most-one constraints of average size 3.2
c [card-5] found 90 at-most-two constraints of average size 4.0
c [card-5] using previous limit 5208545 for elimination
c [card-5] 286 out of 288 constraints (99%) meet size limits
c [card-5] no units found
c [card-5] generated 85 at-most-one constraints, 6 used 7%
c [card-5] exported 6 binary clauses, 1.0 per/constraint
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 145 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 3370 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 11 variables 0% in round 1 in 4269255 steps
c [elim-12-1] backward subsumption/strengthening limit 4269200
c [elim-12-1-1] backward checking 94 touched variables 3%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 2 and strengthened 3 clauses in 51175 steps
c [elim-12-1] rescheduled 14 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 6191 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 11 = 0% variables out of 3370 scheduled
c [elim-12] 11 < 1/100 * 3370 = 33 considered unsuccessful
c [bca-11] limit of 10000000 steps and 37536 added (scaled 2)
c [bca-11] 1429 out of 6720 literals actually usable 21%
c [bca-11] added 1 blocked clauses in 72477 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 500020390 penalty 0 = 0 + 0
c [sweep-11-1] 1562 pos 46.5% + 1797 neg 53.5% = 3359 sched 100.0% ret 0
c [sweep-11-1] 10796097 steps 191 queries 54.07 avg class size
c [sweep-11-1] 4173 decisions 191 SAT calls 72.93 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-58] removed 2 variables
c [sweep-11-1] removed 2 vars (0 failed, 0 eqs, 3 impls)
c [sweep-11-2] 1562 pos 46.5% + 1795 neg 53.5% = 3357 sched 100.0% ret 0
c [sweep-11-2] 10321906 steps 196 queries 50.56 avg class size
c [sweep-11-2] 4502 decisions 197 SAT calls 71.95 avg env size
c [sweep-11-2] fully completed sweeping round
c [sweep-11-2] removed 0 vars (0 failed, 1 eqs, 1 impls)
c [sweep-11-3] 1562 pos 46.5% + 1795 neg 53.5% = 3357 sched 100.0% ret 0
c [sweep-11-3] 10750189 steps 193 queries 64.96 avg class size
c [sweep-11-3] 4302 decisions 191 SAT calls 70.26 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-60] removed 3 variables
c [sweep-11-3] removed 3 vars (0 failed, 3 eqs, 4 impls)
c [sweep-11] removed 5 vars in TOTAL (3 rounds, 577 queries)
c [sort-queue-4] sorted 7 enqueued variables after 1050244 conflicts
c [score-dist-15] active 3347 (100%), one 7 (0%), zero 0 (0%)
c [score-dist-15] max exp 513, different 17 (3%)
c [score-dist-15] median active exp 508, avg 508.1
c [simplification-15] removed 16 variables 0.5% (3354 remain 18%)
c [simplification-15] removed 30 irredundant clauses 0.2% (18480 remain 33%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 266654
c [simplification-15] new conflict interval 533308
c [simplification-15] penalized conflict interval 533308 = 1 * 533308
c [simplification-15] hard conflict limit 1850206 (soft 1583552 + delta 266654)
c [simplification-15] new conflict limit 1583552 (hard 1850206)
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 -  515.3    3354    18480   1052767   41548   4586  4378   14    16   11  89%   1024    2   16   14  118%
c -  547.2    3354    18480   1126525   42306   4590  4378   13    14   19  95%   1024   -2   14   14   94%
c -  588.9    3354    18480   1225212   42852   4593  4378   13    13   19  96%   1024   -2   12   14   90%
c -  640.0    3354    18480   1346625   42745   4598  4378   12    13   24  98%   1024   -1   15   13  113%
c -  700.8    3354    18480   1491016   44353   4599  4378   13    13   32  97%   1024    0   12   13   98%
c 
c [simplification-16] limit 1583552 conflicts (hard 1850206) hit after 1585647 conflicts
c [quatres-12] found 7363 quaternary clauses 39% in total
c [quatres-12-1] removed 4 duplicate quaternary clauses
c [quatres-12-1] added 6 double-self-subsuming ternary resolvents
c [quatres-12-2] added 30 single-self-subsuming ternary resolvents
c [quatres-12-2] added 64 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 3354 free variables schedulable
c [ternres-12] 339 ternary resolvents (7 bin, 332 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-7] limit 25000000 penalty 1 = 1 + 0
c [gauss-7] extracted 4044 xors of average arity 3.0
c [gauss-7] connected 12128 occurrences of 648 variables (average 18.7)
c [gauss-7] limit 25000000 penalty 1 = 1 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-61] removed 1 variables
c [treelook-5] limit 12602891 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 6705 literals 100%
c [treelook-5] scheduling used 254393 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 12602891 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 7040784 steps
c [treelook-5] fully completed tree based probing
c [treelook-5] removed 0 variables, found 5385 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 330 transitive binary clauses
c [cce-9] limit of 630144562 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 3 clauses out of 87 (3%) of length 6
c [cce-9-1] eliminated 16 clauses out of 1624 (1%) of length 5
c [cce-9-1] eliminated 57 clauses out of 5501 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 76 large clauses in 13215195 steps
c [cce-9-1] allowing another 6607597 steps for small clauses
c [cce-9-1] scheduling 7474 clauses = 3756 binary + 3718 ternary
c [cce-9-1] tried to eliminate 7474 small clauses 100%
c [cce-9-1] eliminated 15 binary clauses 0%
c [cce-9-1] eliminated 61 ternary clauses 2%
c [cce-9-1] eliminated 76 small clauses 1%
c [cce-9-1] eliminated 76 small clauses in 24843086 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 152 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 84 (1%) of length 6
c [cce-9-2] eliminated 1 clauses out of 1608 (0%) of length 5
c [cce-9-2] eliminated 5 clauses out of 5444 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 7 large clauses in 12997526 steps
c [cce-9-2] allowing another 6498763 steps for small clauses
c [cce-9-2] scheduling 7398 clauses = 3741 binary + 3657 ternary
c [cce-9-2] tried to eliminate 7398 small clauses 100%
c [cce-9-2] eliminated 1 binary clauses 0%
c [cce-9-2] eliminated 1 small clauses 0%
c [cce-9-2] eliminated 1 small clauses in 24377151 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 8 covered clauses in round 2
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] allowing another 6491864 steps for small clauses
c [cce-9-3] scheduling 7397 clauses = 3740 binary + 3657 ternary
c [cce-9-3] tried to eliminate 7397 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 0 covered clauses in round 3
c [cce-9] eliminated 160 covered clauses in TOTAL during 3 rounds
c [cce-9] 160 < 1/100 * 18475 = 184 considered unsuccessful
c [bca-12] limit of 10000000 steps and 37204 added (scaled 2)
c [bca-12] 1313 out of 6708 literals actually usable 20%
c [bca-12] added 1 blocked clauses in 70404 steps
c [sweep-12] limit 75617347 penalty 0 = 0 + 0
c [sweep-12-1] 1642 pos 49.0% + 1711 neg 51.0% = 3353 sched 100.0% ret 0
c [sweep-12-1] 11105329 steps 197 queries 36.48 avg class size
c [sweep-12-1] 4995 decisions 195 SAT calls 87.94 avg env size
c [sweep-12-1] fully completed sweeping round
c [sweep-12-1] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-12-2] 1642 pos 49.0% + 1711 neg 51.0% = 3353 sched 100.0% ret 0
c [sweep-12-2] 13346537 steps 207 queries 36.09 avg class size
c [sweep-12-2] 4856 decisions 206 SAT calls 75.91 avg env size
c [sweep-12-2] fully completed sweeping round
c [decomp-64] removed 4 variables
c [sweep-12-2] removed 4 vars (0 failed, 4 eqs, 2 impls)
c [sweep-12-3] 1641 pos 49.0% + 1708 neg 51.0% = 3349 sched 100.0% ret 0
c [sweep-12-3] 9097069 steps 192 queries 40.14 avg class size
c [sweep-12-3] 4212 decisions 189 SAT calls 65.15 avg env size
c [sweep-12-3] fully completed sweeping round
c [decomp-65] removed 4 variables
c [sweep-12-3] removed 4 vars (0 failed, 3 eqs, 3 impls)
c [sweep-12] removed 8 vars in TOTAL (3 rounds, 593 queries)
c [sort-queue-5] sorted 3 enqueued variables after 1585647 conflicts
c [score-dist-16] active 3342 (100%), one 3 (0%), zero 0 (0%)
c [score-dist-16] max exp 513, different 15 (3%)
c [score-dist-16] median active exp 509, avg 508.5
c [simplification-16] removed 9 variables 0.3% (3345 remain 18%)
c [simplification-16] removed 179 irredundant clauses 1.0% (18301 remain 33%)
c [simplification-16] maximum reduction of 1% = max (0%, 1%)
c [simplification-16] geometric conflict interval increment 266654 = 533308 / 2
c [simplification-16] new conflict interval 799962
c [simplification-16] penalized conflict interval 799962 = 1 * 799962
c [simplification-16] hard conflict limit 2785590 (soft 2385609 + delta 399981)
c [simplification-16] new conflict limit 2385609 (hard 2785590)
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 -  750.8    3345    18301   1608596   44841   5099  7762   15    16   13  96%   1024    2   14   13  107%
c -  785.7    3345    18301   1703418   46242   5101  7762   13    13   23  95%   1024   -0   13   13  104%
c -  820.5    3345    18301   1799896   47434   5103  7762   10    11   23  94%   1024   -2   10   12   85%
c -  850.7    3345    18301   1885275   47313   5103  7762   11    12   23  94%   1024   -0   11   12   93%
c -  878.1    3345    18301   1966302   48730   5115  7762   11    11   23  96%   1024   -1   10   11   89%
c -  905.0    3345    18301   2041827   47655   5122  7762   18    21   19  87%   1024    8   15   12  127%
c -  949.8    3345    18301   2150393   48061   5124  7762   13    14   24  94%   1024   -0   12   13   95%
c -  986.1    3345    18301   2254553   49282   5129  7762   11    12   23  95%   1024   -1   14   12  116%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 22 basic ate = 20 trn 91% + 2 lrg 9% in 2 updates
c bcas: 12 count, 150 added (8 skipped), 471950 steps
c bkwd: tried 82191 clauses, 163693 lits, 1.99 lits/clause
c bkwd: checked 1994264 occs, 24.26 occs/clause, 12.18 occs/lit
c bkwd: subsumed 98 binary, 99 ternary, 40 large
c bkwd: strengthened 3 binary, 0 ternary (0% self), 689 large (0% self)
c blkd: 4 bces, 120 removed, 417329 resolutions, 1039038 steps
c blkd: 245 blocking literals 1%, 0 pure
c bump: 2318150 bumped seen, 1341262303 lits 578.6 on average
c card: 5 count, 0 units, 44 am1, 14020466 steps
c card: 39 rescheduled, 356 eliminated, 101767 resolved, 2791 subsumed
c card: 342 at-most-one constraints found, average size 3.10
c card: 342 at-most-one constraints used 100%, average size 3.10
c card: 140 at-most-two constraints found, average size 4.01
c card: 137 at-most-two constraints used 98%, average size 4.01
c cces: 9 cces, 1848 eliminated, 1666 ate 90%, 182 abce 10%
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: 185744 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 98 gcs, 0 rescored clauses, 8984 rescored vars
c dcps: 65 decompositions, 1131 equivalent 6%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2652073 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 12722 eliminated 68%, 0 pure 0%
c elms: 33 rounds, 2.8 rounds/bve
c elms: 12408 small 98%, 314 large 2%
c elms: 31099 tried small, 12408 succeeded 40%, 18691 failed 60%
c elms: 930 subsumed, 1818 strengthened, 135 blocked
c elms: 1404996 copies, 1628580 resolutions, 1266578 ipos
c elms: 379453 subchks, 343054 strchks
c gaus: 7 extractions, 31091 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 1 binary and 28 ternary equations
c gaus: 0 gc, 11263592 steps, 5631796 extr 50%, 1100701 elim 10%
c glue: 13.8 orig avg, 13.8 real avg, 3.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 23450 = 6420 simple 27% + 13350 trn 57% + 3680 lrg 16%, 1186 sub 5%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2318150 clauses, 28.2 length
c lrnd: 65473084 lits = 412853508 orig - 347380424 removed 84%
c lrnd: 182510 uips 8%, 2080802 flips 90%
c mins: 2315685 mins 100%, 211 bin 0%, 2254 size 0%
c mins: 766121831 poisoned searches, 16105541 hits, 2% hit rate
c mins: 1160539566 used twice searches, 6900710 hits, 1% hit rate
c move: moved 1897, 394 bin 21%, 1503 trn 79%
c otfs: 1192 driving 24%, 3814 restarting 76%
c otfs: str 5006, 4896 red 98%, 110 irr 2%
c otfs: str 5006, 0 bin 0%, 58 trn 1%, 4948 lrg 99%
c otfs: sub 411, 411 red 100%, 0 irr 0%
c otfs: sub 411, 0 bin 0%, 6 trn 1%, 405 lrg 99%
c phas: 1 computed, 5973 set, 1103 pos (18%), 4870 neg (82%)
c prbs: 4 basic, 55839 probed, 85 failed, 0 lifted
c prbs: 5 simple, 59391 probed, 145 failed, 994 eqs
c prbs: 5 treelook, 7584 probed, 1 failed, 0 lifted
c prom: 201502 locked 1% out of 31508240 tried
c prps: 1524116457 props, 572 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 12 count, 979 quat, 407 self1, 16 self2, 13 dup
c queu: 5 sorted, 2652073 next (201804 steps 0.08)
c queu: 1371616367 enq (1935977717 steps 1.41), 1341262303 deq 98%
c redc: 14281 clauses 29%, 49529 tried 2%, 0 sat 0%
c redc: 22211 lits 4%, 605830 tried 0%, 0 sat 0%
c redc: 53 times jump level reduced, 3.4 levels on average
c reds: 27 count, 85207.7 conflicts per reduce
c reds: 0 memlim 0%, 27 arith 100%
c reds: 850565 collected 95%, 48636 retired 5%
c rmbd: 1173 removed, 979 red 83%
c rsts: 6744 restarts 49%, 6940 skipped 51%
c rsts: 6940 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: 16 count, 15 confs 94%, 0 vars 0%
c simp: 1 its 6%, 0 bin 0%, 0 trns 0%
c subl: 2318150 count (3321573 tried 1.4), 1332707 sub out of 2316817 (57.5%)
c swps: 12 count, 26 rounds, 4220 queries (162.3/round)
c swps: 4192 sat calls, 49 unsat (4.5% success rate)
c swps: 86445 decisions 20.6, 18735 conflicts 4.5
c swps; 45.2 avg class size, 58.2 avg environment size
c swps: 0 failed, 72 impls, 76 equivs
c swp0: 1397 type 0 queries, 201 unsat (14.4%), 1377 sat (98.6%)
c swp1: 2823 type 1 queries, 451 unsat (16.0%), 2767 sat (98.0%)
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: 9958756 calls to obtain time
c tops: 1409 fixed 8%, 12 its, 191717.25 confs/it
c trds: 12 transitive reductions, 2282 removed, 1 failed
c trds: 84572 nodes, 60315 edges, 4267587 steps
c trim: 9497674 words, 36.2 MB
c trnr: 12 count, 94 bin, 6585 trn, 40390036 steps
c unhd: 9 count, 19 rounds, 9461930 steps
c unhd: 230 non-trivial sccs of average size 4.0
c unhd: 193 units, 193 bin, 0 trn, 0 lrg
c unhd: 885 failed, 883 stamp, 0 lits, 1 bin, 1 trn, 0 lrg
c unhd: 10728 tauts, 66 bin 1%, 3444 trn 32%, 68 lrg 1%
c unhd: 10728 tauts, 7150 stamp 67%, 9198 red 86%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 352637 str, 193 bin 0%, 1419 trn 0%, 351025 lrg 100%, 348787 red 99%
c vars: 3345 remaining 18% and 15262 removed 82% out of 18607
c vars: 1409 fixed 8%, 12722 eliminated 68%, 1131 equivalent 6%
c vsts: 37637006062 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 24.7 search visits per propagation, 16289.0 per conflict
c wchs: 5025381699 pushed, 4354386 enlarged, 190 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2317796        850565         48636     219594805     127689488       1128727
c 
c  0 0         18373   1      1902   0         0   0 109702724  50  58392923  46    215253  19     0.5
c  1 5         15805   1      7056   1      2679   6  41860608  19< 23885767  19<    78743   7     0.3
c  2 6        135514   6     70802   8     12615  26  53429555  24  33352959  26    203319  18<    2.1
c  3 9       1043627  45<   351890  41<    22414  46< 12072924   5   9679101   8    462155  41     8.1
c  4 14       943885  41    348602  41      8503  17   2258168   1   2143907   2    156914  14     7.3
c  5 21       143019   6     64608   8      2100   4    240395   0    210360   0     10889   1     3.6
c  6 30        15145   1      5470   1       295   1     26286   0     21204   0      1268   0     0.9
c  7 41         1510   0       234   0        30   0      2858   0      2301   0       163   0     0.1
c  8 54          914   0         1   0         0   0      1283   0       962   0        21   0     0.2
c  9 69            4   0         0   0         0   0         4   0         4   0         2   0     0.0
c 
c avg                  3.5           3.5           2.9           0.9           1.0           2.3
c std                  0.8           0.8           0.9           1.0           1.1           1.4
c 
c  259.422  26% bump
c    6.917   1% sweep
c    6.390   1% cce
c 
c    8.737 < 1% rest (below)
c 
c    3.352   0% rescore
c    2.029   0% elim
c    2.024   0% unhide
c    1.442   0% probe
c    1.350   0% decide
c    0.459   0% transred
c    0.332   0% gauss
c    0.274   0% bca
c    0.267   0% quatres
c    0.252   0% ternres
c    0.189   0% card
c    0.117   0% block
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.495   0% preprocessing     2%
c   20.862   2% inprocessing     98%
c ==================================
c   21.357   2% simplifying
c  978.708  98% search
c ==================================
c 1000.066 100% all
c 
c       2300607 conflicts,        2300.5 confs/sec
c           268 ternaries,        8584.4 confs/ternary
c            42 binaries,        54776.4 confs/binary
c            12 iterations,     191717.2 confs/iteration
c 
c            27 reductions,          0.0 redus/sec,  85207.7 confs/reduction
c          6744 restarts,            6.7 rests/sec,    341.1 confs/restart
c       2652073 decisions,        2651.9 decis/sec,      1.2 decis/conflict
c    1524116457 propagations,  1524015.8 props/sec,    574.7 props/decision
c 
c 1000.1 seconds, 47.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
